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

nra2nba: Fix initial state construction.

Browse source 
This bug caused tgbatest/ltl2dstar.test to fail but because I had
no ltl2dstar on my computer for a while, I only discovered it after
David Müller and Joachim Klein reported a bug against ltlcross.
It might be the case that their bug is different (I can't reproduce it
using their format), but I hope it was caused by this as well.

* src/dstarparse/nra2nba.cc: Revert 57cda2d9, with a comment.
* THANKS: Add David.
This commit is contained in:
Alexandre Duret-Lutz 2015-02-05 18:55:52 +01:00
parent 856adef9a8
commit 78e63d0324
2 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
THANKS
View file

@ -4,6 +4,7 @@ suggestions.
Akim Demaille Akim Demaille
Caroline Lemieux Caroline Lemieux
Christian Dax Christian Dax
David Müller
Ernesto Posse Ernesto Posse
Étienne Renault Étienne Renault
Fabrice Kordon Fabrice Kordon

6
src/dstarparse/nra2nba.cc
View file

@ -48,7 +48,11 @@ namespace spot
out_->set_single_acceptance_set(); out_->set_single_acceptance_set();
out_->prop_state_based_acc(); out_->prop_state_based_acc();
out_->new_states(num_states_ * (d_->accpair_count + 1)); out_->new_states(num_states_ * (d_->accpair_count + 1));
out_->set_init_state(a->aut->get_init_state_number()); // This converts the initial state of aut (not a->aut) into a
// state number in a->aut.
auto i = aut->get_init_state();
out_->set_init_state(a->aut->state_number(i));
i->destroy();
} }
tgba_digraph_ptr tgba_digraph_ptr