Fix a nondeterministic behavior of the degeneralization algorithm.

Reported by Tomáš Babiak <xbabiak@fi.muni.cz>.

* 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

@@ -1,3 +1,16 @@
+2011-08-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Fix a nondeterministic behavior of the degeneralization algorithm.
+
+	Reported by Tomáš Babiak <xbabiak@fi.muni.cz>.
+
+	* 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  <adl@lrde.epita.fr>
 
 	* src/tgbatest/ltl2tgba.cc (syntax): -N implies -DS, not -D.

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

src/tgba/tgbatba.cc

@@ -108,7 +108,21 @@ namespace spot
 
     typedef std::pair<const state_tba_proxy*, bool> state_ptr_bool_t;
 
-    struct state_ptr_bool_less_than:
+    struct state_ptr_bool_hash:
+      public std::unary_function<const state_ptr_bool_t&,
+				 size_t>
+    {
+      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<const state_ptr_bool_t&,
 				  const state_ptr_bool_t&, bool>
     {
@@ -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;
+	  return false;
-	assert(left.first);
+	return left.first->compare(right.first) == 0;
-	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<state_ptr_bool_t,
+      typedef Sgi::hash_map<state_ptr_bool_t, bdd,
-		       bdd,
+			    state_ptr_bool_hash,
-		       spot::state_ptr_bool_less_than> transmap_t;
+			    state_ptr_bool_equal> transmap_t;
       transmap_t transmap_;
-      transmap_t::const_iterator it_;
+      typedef transmap_t::const_iterator mapit_t;
+      typedef std::list<mapit_t> 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)

src/tgbatest/Makefile.am

@@ -91,6 +91,7 @@ TESTS = \
   tripprod.test \
   mixprod.test \
   dupexp.test \
+  degendet.test \
   kv.test \
   reduccmp.test \
   reductgba.test \

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