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

never: fix output of accepting initial states

Browse source 
* src/tgbaalgos/neverclaim.cc: Make sure the any accepting initial state
is not output as an accept_all state.  This bug caused ltl2dstar.test to
fail.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-13 18:02:13 +01:00
parent f3f4305150
commit 7c55500d0e
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tgbaalgos/neverclaim.cc
View file

@ -126,7 +126,8 @@ namespace spot
void process_state(unsigned n) void process_state(unsigned n)
{ {
if (aut_->state_is_accepting(n) && is_sink(n)) if (aut_->state_is_accepting(n) && is_sink(n)
&& n != aut_->get_init_state_number())
{ {
// We want the accept_all state at the end of the never claim. // We want the accept_all state at the end of the never claim.
need_accept_all_ = true; need_accept_all_ = true;