diff --git a/src/nfa/nfa.cc b/src/nfa/nfa.cc index 38c51350c..26028502b 100644 --- a/src/nfa/nfa.cc +++ b/src/nfa/nfa.cc @@ -20,6 +20,7 @@ #include #include #include +#include // MATA headers #include "mata/utils/sparse-set.hh" @@ -329,7 +330,11 @@ BoolVector Nfa::get_useful_states(bool stop_at_first_useful_state) const { // propagate usefulness to the closed SCC for(const State& st : scc) useful[st] = true; // propagate usefulness to predecessors in @p tarjan_stack - for(const State& st : tarjan_stack) useful[st] = true; + for(const State& st :std::views::reverse(tarjan_stack)) { + if (useful[st]) + break; + useful[st] = true; + } } } // all successors have been processed, we can remove act_state from the program stack