diff --git a/NEWS b/NEWS index af80b72c3..d476b16ac 100644 --- a/NEWS +++ b/NEWS @@ -55,8 +55,9 @@ New in spot 2.0.3a (not yet released) future. * is_deterministic(), is_terminal(), is_weak(), and - is_inherently_weak() will update the corresponding properties of - the automaton as a side-effect of their check. + is_inherently_weak(), count_nondet_states() will update the + corresponding properties of the automaton as a side-effect of + their check. * language_containment_checker now has default values for all parameters of its constructor. diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index e44fbef89..c1160fe0c 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -1008,12 +1008,8 @@ namespace problems += prob; // If the automaton is deterministic, compute its complement - // as well. Note that if we have computed statistics - // already, there is no need to call is_deterministic() - // again. - if (!no_complement && pos[n] - && ((want_stats && !(*pstats)[n].nondeterministic) - || (!want_stats && is_deterministic(pos[n])))) + // as well. + if (!no_complement && pos[n] && is_deterministic(pos[n])) comp_pos[n] = dtwa_complement(pos[n]); } @@ -1048,12 +1044,8 @@ namespace problems += prob; // If the automaton is deterministic, compute its - // complement as well. Note that if we have computed - // statistics already, there is no need to call - // is_deterministic() again. - if (!no_complement && neg[n] - && ((want_stats && !(*nstats)[n].nondeterministic) - || (!want_stats && is_deterministic(neg[n])))) + // complement as well. + if (!no_complement && neg[n] && is_deterministic(neg[n])) comp_neg[n] = dtwa_complement(neg[n]); } } diff --git a/spot/twaalgos/isdet.cc b/spot/twaalgos/isdet.cc index afae5348b..72897cff0 100644 --- a/spot/twaalgos/isdet.cc +++ b/spot/twaalgos/isdet.cc @@ -50,6 +50,8 @@ namespace spot if (!count && nondet_states) break; } + std::const_pointer_cast(aut) + ->prop_deterministic(!nondet_states); return nondet_states; } } @@ -57,6 +59,8 @@ namespace spot unsigned count_nondet_states(const const_twa_graph_ptr& aut) { + if (aut->prop_deterministic()) + return 0; return count_nondet_states_aux(aut); } @@ -66,9 +70,7 @@ namespace spot trival d = aut->prop_deterministic(); if (d.is_known()) return d.is_true(); - bool res = !count_nondet_states_aux(aut); - std::const_pointer_cast(aut)->prop_deterministic(res); - return res; + return !count_nondet_states_aux(aut); } bool