diff --git a/src/twaalgos/safra.cc b/src/twaalgos/safra.cc index 345820226..95d72f89f 100644 --- a/src/twaalgos/safra.cc +++ b/src/twaalgos/safra.cc @@ -37,8 +37,8 @@ namespace spot size_t i = 0; for (; i < m; ++i) { - if (lhs[i] < rhs[i]) - return true; + if (lhs[i] != rhs[i]) + return lhs[i] < rhs[i]; } return lhs.size() > rhs.size(); } @@ -255,7 +255,7 @@ namespace spot return nodes_ < other.nodes_; } - void safra_state::print_debug(unsigned state_id) + void safra_state::print_debug(unsigned state_id) const { std::cerr << "State: " << state_id << "{ "; for (auto& n: nodes_) diff --git a/src/twaalgos/safra.hh b/src/twaalgos/safra.hh index 3ccf5912a..09078a22c 100644 --- a/src/twaalgos/safra.hh +++ b/src/twaalgos/safra.hh @@ -43,7 +43,8 @@ namespace spot typedef std::vector> succs_t; bool operator<(const safra_state& other) const; // Print each sub-state with their associated braces of a safra state - void print_debug(unsigned state_id); + void print_debug(unsigned state_id) const; + // Printh the number of states in each brace safra_state(unsigned state_number, bool init_state = false); // Given a certain transition_label, compute all the successors of that // label, and return that new node.