diff --git a/NEWS b/NEWS index e53749d6c..b4fcd0617 100644 --- a/NEWS +++ b/NEWS @@ -11,6 +11,9 @@ New in spot 1.2.3a (not yet released) * Bug fixes: - Change the Python bindings to make them compatible with Swig 3.0. + - "ltl2tgta --ta" could crash in certain conditions due to the + introduction of a simulation-based reduction after + degeneralization. New in spot 1.2.3 (2014-02-11) diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index fb619caf4..d326f7dd6 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -1,6 +1,6 @@ // -*- coding utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -431,35 +431,31 @@ namespace spot std::stack todo; const tgba* tgba_ = ta->get_tgba(); - const sba* sba_ = down_cast(tgba_); - assert(!degeneralized || sba_); // build Initial states set: state* tgba_init_state = tgba_->get_init_state(); bdd tgba_condition = tgba_->support_conditions(tgba_init_state); + bool is_acc = false; + if (degeneralized) + { + tgba_succ_iterator* it = tgba_->succ_iter(tgba_init_state); + it->first(); + if (!it->done()) + is_acc = it->current_acceptance_conditions() != bddfalse; + delete it; + } + bdd satone_tgba_condition; while ((satone_tgba_condition = bdd_satoneset(tgba_condition, atomic_propositions_set_, bddtrue)) != bddfalse) { tgba_condition -= satone_tgba_condition; - state_ta_explicit* init_state; - if (degeneralized) - { - init_state = new - state_ta_explicit(tgba_init_state->clone(), - satone_tgba_condition, true, - sba_->state_is_accepting(tgba_init_state)); - } - else - { - init_state = new - state_ta_explicit(tgba_init_state->clone(), - satone_tgba_condition, true, false); - } - + state_ta_explicit* init_state = new + state_ta_explicit(tgba_init_state->clone(), + satone_tgba_condition, true, is_acc); state_ta_explicit* s = ta->add_state(init_state); assert(s == init_state); ta->add_to_initial_states_set(s); @@ -492,6 +488,17 @@ namespace spot bdd all_props = bddtrue; bdd dest_condition; + + bool is_acc = false; + if (degeneralized) + { + tgba_succ_iterator* it = tgba_->succ_iter(tgba_state); + it->first(); + if (!it->done()) + is_acc = it->current_acceptance_conditions() != bddfalse; + delete it; + } + if (satone_tgba_condition == source->get_tgba_condition()) while ((dest_condition = bdd_satoneset(all_props, @@ -499,21 +506,9 @@ namespace spot != bddfalse) { all_props -= dest_condition; - state_ta_explicit* new_dest; - if (degeneralized) - { - new_dest = new state_ta_explicit - (tgba_state->clone(), - dest_condition, - false, - sba_->state_is_accepting(tgba_state)); - } - else - { - new_dest = new state_ta_explicit - (tgba_state->clone(), - dest_condition, false, false); - } + state_ta_explicit* new_dest = + new state_ta_explicit(tgba_state->clone(), + dest_condition, false, is_acc); state_ta_explicit* dest = ta->add_state(new_dest); if (dest != new_dest) diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 7e2e674d9..e9fff81f8 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -96,6 +96,7 @@ TESTS = \ ltl2neverclaim.test \ ltl2neverclaim-lbtt.test \ ltl2ta.test \ + ltl2ta2.test \ ltlprod.test \ bddprod.test \ explprod.test \ diff --git a/src/tgbatest/ltl2ta2.test b/src/tgbatest/ltl2ta2.test new file mode 100755 index 000000000..eed0c9739 --- /dev/null +++ b/src/tgbatest/ltl2ta2.test @@ -0,0 +1,27 @@ +#!/bin/sh +# Copyright (C) 2014 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + + +. ./defs + +set -e + +# This used to trigger an assert because of BA simulation not +# returning an instance of spot::sba. +run 0 ../../bin/ltl2tgta --ta 'G(F(a U b) U (c M d))'