ltl3tela does not compile with the current development version of Spot

[adl]

I recently changed spot::formula::operator bool() to become an explicit conversion operator.

This apparently prevents ltl3tela from compiling.

automaton.cpp: In instantiation of ‘void Automaton<T>::add_edge(unsigned int, bdd, std::set<unsigned int>, std::set<unsigned int>) [with T = spot::
formula]’:
automaton.cpp:22:16:   required from here
automaton.cpp:115:28: error: no match for ‘operator[]’ (operand types are ‘std::vector<std::set<unsigned int> >’ and ‘spot::formula’)
  115 |      (*spot_id_to_slaa_set)[state_name(*(e_this->get_targets().begin()))],
      |      ~~~~~~~~~~~~~~~~~~~~~~^

If I understand correctly, *spot_id_to_slaa_set is a vector, but Automaton<spot:formula>::state_name() returns a formula, which is not a valid index for a vector. It worked so far because spot::formula was implicitly convertible to bool, which could then be promoted to int, but really this looks like a bug waiting to happen and I'm glad this is now rejected.

I suspect that this part of the function is really only used on Automaton<unsigned> and not Automaton<spot::formula>, so probably it should be defined only for the correct type?

[adl]

Here is a possible fix, updating the language requirement to C++17, since Spot will soon require that anyway.

diff --git a/Makefile b/Makefile
index 044f7b4..65d62c4 100644
--- a/Makefile
+++ b/Makefile
@@ -18,7 +18,7 @@
 FILES = alternating.cpp nondeterministic.cpp automaton.cpp utils.cpp spotela.cpp main.cpp

 ltl3tela: $(FILES)
-   g++ -std=c++14 -o ltl3tela $(FILES) -lspot -lbddx
+   g++ -std=c++17 -O2 -o ltl3tela $(FILES) -lspot -lbddx

 clean:
    rm ltl3tela
diff --git a/automaton.cpp b/automaton.cpp
index 1669882..87a73e9 100644
--- a/automaton.cpp
+++ b/automaton.cpp
@@ -108,7 +108,7 @@ template<typename T> void Automaton<T>::add_edge(unsigned from, bdd label, std::
            auto e_other = get_edge(*e_other_it);

            int dom_level;
-           if (spot_id_to_slaa_set == nullptr) {
+           if constexpr (! std::is_same<T, unsigned>::value) {
                dom_level = e_this->dominates(e_other, get_inf_marks());
            } else {
                dom_level = e_this->dominates(e_other,
@@ -150,7 +150,7 @@ template<typename T> void Automaton<T>::add_edge(unsigned from, bdd label, std::
        for (auto& e_other_id : state_edges[from]) {
            auto e_other = get_edge(e_other_id);
            int dom_level;
-           if (spot_id_to_slaa_set == nullptr) {
+           if constexpr (! std::is_same<T, unsigned>::value) {
                dom_level = e_other->dominates(e_this, get_inf_marks());
            } else {
                dom_level = e_other->dominates(e_this,