From 78e63d032457a68921b730d29004cda380c49f00 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 Feb 2015 18:55:52 +0100 Subject: [PATCH] nra2nba: Fix initial state construction. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- THANKS | 1 + src/dstarparse/nra2nba.cc | 6 +++++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/THANKS b/THANKS index 89d52b874..89654bba6 100644 --- a/THANKS +++ b/THANKS @@ -4,6 +4,7 @@ suggestions. Akim Demaille Caroline Lemieux Christian Dax +David Müller Ernesto Posse Étienne Renault Fabrice Kordon diff --git a/src/dstarparse/nra2nba.cc b/src/dstarparse/nra2nba.cc index 4a2c5c25c..37796bbd4 100644 --- a/src/dstarparse/nra2nba.cc +++ b/src/dstarparse/nra2nba.cc @@ -48,7 +48,11 @@ namespace spot out_->set_single_acceptance_set(); out_->prop_state_based_acc(); 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