From d10e772d3514f596fe70668b2077584580485e09 Mon Sep 17 00:00:00 2001 From: Thomas Badie Date: Tue, 13 Nov 2012 22:10:18 +0100 Subject: [PATCH] Fix non determinism in the simulation. * src/tgbaalgos/simulation.cc: Fix non determinism. * src/tgbatest/simdet.test: Test that the behavior is now correct. * src/tgbatest/Makefile.am (TESTS): Add the new test to the test-suite. --- src/tgbaalgos/simulation.cc | 20 +++++++++++++------ src/tgbatest/Makefile.am | 1 + src/tgbatest/simdet.test | 40 +++++++++++++++++++++++++++++++++++++ 3 files changed, 55 insertions(+), 6 deletions(-) create mode 100755 src/tgbatest/simdet.test diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 381cf105f..95b354cb3 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -147,8 +147,10 @@ namespace spot map_state_unsigned::const_iterator i = state2int.find(s); if (i == state2int.end()) { - i = state2int.insert(std::make_pair(s, ++current_max)).first; - previous_class_[out_->add_state(current_max)] = bddfalse; + i = state2int.insert(std::make_pair(s, ++current_max)).first; + const state* to_add = out_->add_state(current_max); + previous_class_[to_add] = bddfalse; + order_.push_back(to_add); } return i->second; } @@ -192,6 +194,7 @@ namespace spot size_t size; tgba_explicit_number* out_; map_state_bdd previous_class_; + std::list order_; private: const tgba* ea_; @@ -262,6 +265,8 @@ namespace spot } relation_[init] = init; + + order_ = acc_compl.order_; } @@ -369,11 +374,11 @@ namespace spot // all the reachable states of this automaton. We do not // have to make (again) a traversal. We just have to run // through this map. - for (map_state_bdd::iterator it = previous_class_.begin(); - it != previous_class_.end(); - ++it) + for (std::list::const_iterator it = order_.begin(); + it != order_.end(); + ++it) { - const state* src = it->first; + const state* src = previous_class_.find(*it)->first; bdd_lstate_[compute_sig(src)].push_back(src); } @@ -711,6 +716,9 @@ namespace spot state* initial_state; automaton_size stat; + + // The order of the state. + std::list order_; }; } // End namespace anonymous. diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 2b122e3a3..008f87c1d 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -69,6 +69,7 @@ tripprod_SOURCES = tripprod.cc # because such failures will be easier to diagnose and fix. TESTS = \ intvcomp.test \ + simdet.test \ eltl2tgba.test \ explicit.test \ explicit2.test \ diff --git a/src/tgbatest/simdet.test b/src/tgbatest/simdet.test new file mode 100755 index 000000000..db27431a1 --- /dev/null +++ b/src/tgbatest/simdet.test @@ -0,0 +1,40 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2012 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 + +run 0 ../ltl2tgba -R3 -RIS \ +'G("P_1.p2" <-> (F"P_1.p3" & ("P_0.p3" | (X"P_1.CS" U "P_1.p2")))) U G"P_1.p2"'\ + > exp +run 0 ../ltl2tgba -R3 -RIS \ +'G("P_1.p2" <-> (F"P_1.p3" & ("P_0.p3" | (X"P_1.CS" U "P_1.p2")))) U G"P_1.p2"'\ + > out + +diff exp out + +run 0 ../ltl2tgba -R3 -RIS \ +'G("P_1.p2" <-> (F"P_1.p3" & ("P_0.p3" | (X"P_1.CS" U "P_1.p2")))) U G"P_1.p2"'\ + > out + +diff exp out + +rm exp out +