Commit a5b6865c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltl2ta: fix a crash with --ta.

* src/taalgos/tgba2ta.cc: Do not assume the input is an sba.
* src/tgbatest/ltl2ta2.test: New file.
* src/tgbatest/Makefile.am: Add it.
* NEWS: Mention the fix.
parent c4307e21
......@@ -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)
......
// -*- 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<state_ta_explicit*> todo;
const tgba* tgba_ = ta->get_tgba();
const sba* sba_ = down_cast<const sba*>(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)
......
......@@ -96,6 +96,7 @@ TESTS = \
ltl2neverclaim.test \
ltl2neverclaim-lbtt.test \
ltl2ta.test \
ltl2ta2.test \
ltlprod.test \
bddprod.test \
explprod.test \
......
#!/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 <http://www.gnu.org/licenses/>.
. ./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))'
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment