From 03aabf9a3afd39eb511cb812b0992edc3eab3a51 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 17 Aug 2011 15:27:39 +0200 Subject: [PATCH] Fix a nondeterministic behavior of the degeneralization algorithm. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reported by Tomáš Babiak . * src/tgba/tgbatba.cc (tgba_tba_proxy): Replace the std::map used to record outgoing transitions by an Sgi::hash_map, and keep the order of these transitions in a separate list. * src/tgbatest/degendet.test: New file. * src/tgbatest/Makefile.am (TESTS): Add it. * THANKS: Add Tomáš and convert to utf8. --- ChangeLog | 13 ++++++++ THANKS | 5 +-- src/tgba/tgbatba.cc | 66 +++++++++++++++++++++++++++----------- src/tgbatest/Makefile.am | 1 + src/tgbatest/degendet.test | 39 ++++++++++++++++++++++ 5 files changed, 104 insertions(+), 20 deletions(-) create mode 100755 src/tgbatest/degendet.test diff --git a/ChangeLog b/ChangeLog index 679def516..c5b28be2c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,16 @@ +2011-08-17 Alexandre Duret-Lutz + + Fix a nondeterministic behavior of the degeneralization algorithm. + + Reported by Tomáš Babiak . + + * src/tgba/tgbatba.cc (tgba_tba_proxy): Replace the std::map used + to record outgoing transitions by an Sgi::hash_map, and keep the + order of these transitions in a separate list. + * src/tgbatest/degendet.test: New file. + * src/tgbatest/Makefile.am (TESTS): Add it. + * THANKS: Add Tomáš and convert to utf8. + 2011-08-17 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (syntax): -N implies -DS, not -D. diff --git a/THANKS b/THANKS index 7c39bb65b..d9eb79096 100644 --- a/THANKS +++ b/THANKS @@ -3,9 +3,10 @@ suggestions. Heikki Tauriainen Jean-Michel Couvreur -Jean-Michel Ilié +Jean-Michel Ilié Kristin Y. Rozier Michael Weber -Rüdiger Ehlers +Rüdiger Ehlers Silien Hong +Tomáš Babiak Yann Thierry-Mieg diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc index 6eb19351d..0293e942e 100644 --- a/src/tgba/tgbatba.cc +++ b/src/tgba/tgbatba.cc @@ -108,7 +108,21 @@ namespace spot typedef std::pair state_ptr_bool_t; - struct state_ptr_bool_less_than: + struct state_ptr_bool_hash: + public std::unary_function + { + size_t + operator()(const state_ptr_bool_t& s) const + { + if (s.second) + return s.first->hash() ^ 12421; + else + return s.first->hash(); + } + }; + + struct state_ptr_bool_equal: public std::binary_function { @@ -116,12 +130,9 @@ namespace spot operator()(const state_ptr_bool_t& left, const state_ptr_bool_t& right) const { - // Order accepting transitions first, so that - // they are processed early during emptiness-check. if (left.second != right.second) - return left.second > right.second; - assert(left.first); - return left.first->compare(right.first) < 0; + return false; + return left.first->compare(right.first) == 0; } }; @@ -199,7 +210,23 @@ namespace spot transmap_t::iterator id = transmap_.find(key); if (id == transmap_.end()) // No { - transmap_[key] = it->current_condition(); + mapit_t pos = transmap_ + .insert(std::make_pair(key, it->current_condition())).first; + // Keep the order of the transitions in the + // degeneralized automaton related to the order of the + // transitions in the input automaton: in the past we + // used to simply iterate over transmap_ in whatever + // order the transitions were stored, but the output + // would change between different runs depending on + // the memory address of the states. Now we keep the + // order using translist_. We only arrange it + // slightly so that accepting transitions come first: + // this way they are processed early during + // emptiness-check. + if (accepting) + translist_.push_front(pos); + else + translist_.push_back(pos); } else // Yes, combine labels. { @@ -228,7 +255,7 @@ namespace spot void first() { - it_ = transmap_.begin(); + it_ = translist_.begin(); } void @@ -240,7 +267,7 @@ namespace spot bool done() const { - return it_ == transmap_.end(); + return it_ == translist_.end(); } // inspection @@ -248,29 +275,32 @@ namespace spot state_tba_proxy* current_state() const { - return it_->first.first->clone(); + return (*it_)->first.first->clone(); } bdd current_condition() const { - return it_->second; + return (*it_)->second; } bdd current_acceptance_conditions() const { - return it_->first.second ? the_acceptance_cond_ : bddfalse; + return (*it_)->first.second ? the_acceptance_cond_ : bddfalse; } protected: const bdd the_acceptance_cond_; - typedef std::map transmap_t; + typedef Sgi::hash_map transmap_t; transmap_t transmap_; - transmap_t::const_iterator it_; + typedef transmap_t::const_iterator mapit_t; + typedef std::list translist_t; + translist_t translist_; + translist_t::const_iterator it_; }; } // anonymous @@ -294,9 +324,9 @@ namespace spot // // The order is arbitrary, but it turns out that using // push_back instead of push_front often gives better results - // because acceptance conditions and the beginning if the + // because acceptance conditions at the beginning if the // cycle are more often used in the automaton. (This - // surprising fact is probably related to order in which we + // surprising fact is probably related to the order in which we // declare the BDD variables during the translation.) bdd all = a_->all_acceptance_conditions(); while (all != bddfalse) diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index a68f8d637..276873f1a 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -91,6 +91,7 @@ TESTS = \ tripprod.test \ mixprod.test \ dupexp.test \ + degendet.test \ kv.test \ reduccmp.test \ reductgba.test \ diff --git a/src/tgbatest/degendet.test b/src/tgbatest/degendet.test new file mode 100755 index 000000000..df1aace0e --- /dev/null +++ b/src/tgbatest/degendet.test @@ -0,0 +1,39 @@ +#!/bin/sh +# Copyright (C) 2011 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 2 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 Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + + +. ./defs + +set -e + +# The following command, reported by Tomáš Babiak, used to output many +# different automata, because state addresses were used to order the +# successors in the degeneralization. + +# Make sure all these runs output the same automaton. + +# With valgrind +run 0 ../ltl2tgba -r7 -x -R3 -N "XF(Gp2 | F(p0 U (p1 & (! p4 | p3))))" > out1 +# Without valgrind +for i in 2 3 4 5; do + ../ltl2tgba -r7 -x -R3 -N "XF(Gp2 | F(p0 U (p1 & (! p4 | p3))))" > out + cmp out out1 || exit 1 +done