alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

isdet: update prop_deterministic in count_nondet_states()

Browse source 
* spot/twaalgos/isdet.cc: Here.
* bin/ltlcross.cc: Simplify.
* NEWS: Update.
This commit is contained in:
Alexandre Duret-Lutz 2016-07-13 15:09:32 +02:00
parent a2f0b22810
commit fafb135c87
3 changed files with 12 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

5
NEWS
View file

@ -55,8 +55,9 @@ New in spot 2.0.3a (not yet released)
future. future.
* is_deterministic(), is_terminal(), is_weak(), and * is_deterministic(), is_terminal(), is_weak(), and
is_inherently_weak() will update the corresponding properties of is_inherently_weak(), count_nondet_states() will update the
the automaton as a side-effect of their check. corresponding properties of the automaton as a side-effect of
their check.
* language_containment_checker now has default values for all * language_containment_checker now has default values for all
parameters of its constructor. parameters of its constructor.

16
bin/ltlcross.cc
View file

@ -1008,12 +1008,8 @@ namespace
problems += prob; problems += prob;
// If the automaton is deterministic, compute its complement // If the automaton is deterministic, compute its complement
// as well. Note that if we have computed statistics // as well.
// already, there is no need to call is_deterministic() if (!no_complement && pos[n] && is_deterministic(pos[n]))
// again.
if (!no_complement && pos[n]
&& ((want_stats && !(*pstats)[n].nondeterministic)
|| (!want_stats && is_deterministic(pos[n]))))
comp_pos[n] = dtwa_complement(pos[n]); comp_pos[n] = dtwa_complement(pos[n]);
} }
@ -1048,12 +1044,8 @@ namespace
problems += prob; problems += prob;
// If the automaton is deterministic, compute its // If the automaton is deterministic, compute its
// complement as well. Note that if we have computed // complement as well.
// statistics already, there is no need to call if (!no_complement && neg[n] && is_deterministic(neg[n]))
// is_deterministic() again.
if (!no_complement && neg[n]
&& ((want_stats && !(*nstats)[n].nondeterministic)
|| (!want_stats && is_deterministic(neg[n]))))
comp_neg[n] = dtwa_complement(neg[n]); comp_neg[n] = dtwa_complement(neg[n]);
} }
} }

8
spot/twaalgos/isdet.cc
View file

@ -50,6 +50,8 @@ namespace spot
if (!count && nondet_states) if (!count && nondet_states)
break; break;
} }
std::const_pointer_cast<twa_graph>(aut)
->prop_deterministic(!nondet_states);
return nondet_states; return nondet_states;
} }
} }
@ -57,6 +59,8 @@ namespace spot
unsigned unsigned
count_nondet_states(const const_twa_graph_ptr& aut) count_nondet_states(const const_twa_graph_ptr& aut)
{ {
if (aut->prop_deterministic())
return 0;
return count_nondet_states_aux<true>(aut); return count_nondet_states_aux<true>(aut);
} }
@ -66,9 +70,7 @@ namespace spot
trival d = aut->prop_deterministic(); trival d = aut->prop_deterministic();
if (d.is_known()) if (d.is_known())
return d.is_true(); return d.is_true();
bool res = !count_nondet_states_aux<false>(aut); return !count_nondet_states_aux<false>(aut);
std::const_pointer_cast<twa_graph>(aut)->prop_deterministic(res);
return res;
} }
bool bool