* src/tgbaalgos/minimizerun.hh, src/tgbaalgos/minimizerun.cc: New

files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them/
* src/tgbatest/randtgba.cc, src/tgbatest/ltl2tgba.cc: Add option -m.
* src/tgbatest/emptchkr.test: Use -m.

ChangeLog

+2004-11-27  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+	    Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>
+
+	* src/tgbaalgos/minimizerun.hh, src/tgbaalgos/minimizerun.cc: New
+	files.
+	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
+	libtgbaalgos_la_SOURCES): Add them/
+	* src/tgbatest/randtgba.cc, src/tgbatest/ltl2tgba.cc: Add option -m.
+	* src/tgbatest/emptchkr.test: Use -m.
+
 2004-11-25  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>
 
 	* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,

src/tgbaalgos/Makefile.am

@@ -38,6 +38,7 @@ tgbaalgos_HEADERS = \
   ltl2tgba_fm.hh \
   ltl2tgba_lacim.hh \
   magic.hh \
+  minimizerun.hh \
   neverclaim.hh \
   powerset.hh \
   projrun.hh \
@@ -65,6 +66,7 @@ libtgbaalgos_la_SOURCES = \
   ltl2tgba_fm.cc \
   ltl2tgba_lacim.cc \
   magic.cc \
+  minimizerun.cc \
   neverclaim.cc \
   powerset.cc \
   projrun.cc \

src/tgbaalgos/minimizerun.cc

+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// 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.
+
+#include "misc/hash.hh"
+#include "emptiness.hh"
+#include "tgba/tgba.hh"
+#include "bfssteps.hh"
+#include "minimizerun.hh"
+
+namespace spot
+{
+  namespace
+  {
+    typedef Sgi::hash_set<const state*,
+			  state_ptr_hash, state_ptr_equal> state_set;
+    class shortest_path: public bfs_steps
+    {
+    public:
+      shortest_path(const tgba* a)
+        : bfs_steps(a), target(0)
+      {
+      }
+
+      ~shortest_path()
+      {
+        state_set::const_iterator i = seen.begin();
+        while (i != seen.end())
+          {
+            const state* ptr = *i;
+            ++i;
+            delete ptr;
+          }
+      }
+
+      void
+      set_target(const state_set* t)
+      {
+        target = t;
+      }
+
+      const state*
+      search(const state* start, tgba_run::steps& l)
+      {
+	return this->bfs_steps::search(filter(start), l);
+      }
+
+      const state*
+      filter(const state* s)
+      {
+        state_set::const_iterator i = seen.find(s);
+        if (i==seen.end())
+          seen.insert(s);
+        else
+          {
+            delete s;
+            s = *i;
+          }
+        return s;
+      }
+
+      bool
+      match(tgba_run::step&, const state* dest)
+      {
+        return target->find(dest) != target->end();
+      }
+
+    private:
+      state_set seen;
+      const state_set* target;
+    };
+  }
+
+  tgba_run*
+  minimize_run(const tgba* a, const tgba_run* org)
+  {
+    tgba_run* res = new tgba_run;
+    state_set ss;
+    shortest_path shpath(a);
+    shpath.set_target(&ss);
+
+    // We want to find a short segment of the original cycle that
+    // contains all acceptance conditions.
+
+    const state* segment_start; // The initial state of the segment.
+    const state* segment_next; // The state immediately after the segment.
+
+    // Start from the end of the original cycle, and rewind until all
+    // acceptance conditions have been seen.
+    bdd seen_acc = bddfalse;
+    bdd all_acc = a->all_acceptance_conditions();
+    tgba_run::steps::const_iterator seg = org->cycle.end();
+    do
+      {
+        assert(seg != org->cycle.begin());
+	--seg;
+        seen_acc |= seg->acc;
+      }
+    while (seen_acc != all_acc);
+    segment_start = seg->s;
+
+    // Now go forward and ends the segment as soon as we have seen all
+    // acceptance conditions, cloning it in our result along the way.
+    seen_acc = bddfalse;
+    do
+      {
+        assert(seg != org->cycle.end());
+        seen_acc |= seg->acc;
+
+	tgba_run::step st = { seg->s->clone(), seg->label, seg->acc };
+	res->cycle.push_back(st);
+
+	++seg;
+      }
+    while (seen_acc != all_acc);
+    segment_next = seg == org->cycle.end() ? org->cycle.front().s : seg->s;
+
+    // Close this cycle if needed, that is, compute a cycle going
+    // from the state following the segment to its starting state.
+    if (segment_start != segment_next)
+      {
+        ss.insert(segment_start);
+        const state* s = shpath.search(segment_next->clone(), res->cycle);
+        ss.clear();
+        assert(s->compare(segment_start) == 0);
+      }
+
+    // Compute the prefix: it's the shortest path from the initial
+    // state of the automata to any state of the cycle.
+
+    // Register all states from the cycle as target of the BFS.
+    for (tgba_run::steps::const_iterator i = res->cycle.begin();
+	 i != res->cycle.end(); ++i)
+      ss.insert(i->s);
+
+    const state* prefix_start = a->get_init_state();
+    // There are two cases: either the initial state is already on
+    // the cycle, or it is not.  If it is, we will have to rotate
+    // the cycle so it begins on this position.  Otherwise we will shift
+    // the cycle so it begins on the state that follows the prefix.
+    // cycle_entry_point is that state.
+    const state* cycle_entry_point;
+    state_set::const_iterator ps = ss.find(prefix_start);
+    if (ps != ss.end())
+      {
+	// The initial state is on the cycle.
+	delete prefix_start;
+	cycle_entry_point = *ps;
+      }
+    else
+      {
+	// This initial state is outside the cycle.  Compute the prefix.
+        cycle_entry_point = shpath.search(prefix_start, res->prefix);
+      }
+
+    // Locate cycle_entry_point on the cycle.
+    tgba_run::steps::iterator cycle_ep_it;
+    for (cycle_ep_it = res->cycle.begin();
+	 cycle_ep_it != res->cycle.end()
+	   && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it)
+      continue;
+    assert(cycle_ep_it != res->cycle.end());
+
+    // Now shift the cycle so it starts on cycle_entry_point.
+    res->cycle.splice(res->cycle.end(), res->cycle,
+		      res->cycle.begin(), cycle_ep_it);
+    res->cycle.erase(res->cycle.begin(), cycle_ep_it);
+
+    return res;
+  }
+}

src/tgbaalgos/minimizerun.hh

+// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// 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.
+
+#ifndef SPOT_TGBAALGOS_MINIMIZERUN_HH
+# define SPOT_TGBAALGOS_MINIMIZERUN_HH
+
+namespace spot
+{
+  class tgba;
+  class tgba_run;
+
+  /// \brief Minimize an accepting run.
+  ///
+  /// Return a run which is accepting for \a and that is no longer
+  /// that \a org.
+  tgba_run* minimize_run(const tgba* a, const tgba_run* org);
+}
+
+#endif // SPOT_TGBAALGOS_MINIMIZERUN_HH

src/tgbatest/emptchkr.test

@@ -28,24 +28,24 @@ set -e
 
 # With no acceptance condition, everyone should agree and find a run.
 # Do not spend to much time checking this.
-run 0 ./randtgba -e 10 -s 0 -r
+run 0 ./randtgba -e 10 -s 0 -r -m
 
 # One acceptance condition
-run 0 ./randtgba -e 100 -s   0 -r -a 1 0.1 -d 0.01
-run 0 ./randtgba -e 100 -s  50 -r -a 1 0.1 -d 0.02
-run 0 ./randtgba -e 100 -s 100 -r -a 1 0.1 -d 0.04
-run 0 ./randtgba -e 100 -s 150 -r -a 1 0.1 -d 0.08
+run 0 ./randtgba -e 100 -s   0 -r -m -a 1 0.1 -d 0.01
+run 0 ./randtgba -e 100 -s  50 -r -m -a 1 0.1 -d 0.02
+run 0 ./randtgba -e 100 -s 100 -r -m -a 1 0.1 -d 0.04
+run 0 ./randtgba -e 100 -s 150 -r -m -a 1 0.1 -d 0.08
 
 # Four acceptance conditions
-run 0 ./randtgba -e 100 -s 200 -r -a 4 0.1 -d 0.01
-run 0 ./randtgba -e 100 -s 250 -r -a 4 0.1 -d 0.02
-run 0 ./randtgba -e 100 -s 300 -r -a 4 0.1 -d 0.04
-run 0 ./randtgba -e 100 -s 350 -r -a 4 0.1 -d 0.08
-run 0 ./randtgba -e 100 -s 400 -r -a 4 0.2 -d 0.01
-run 0 ./randtgba -e 100 -s 450 -r -a 4 0.2 -d 0.02
-run 0 ./randtgba -e 100 -s 500 -r -a 4 0.2 -d 0.04
-run 0 ./randtgba -e 100 -s 550 -r -a 4 0.2 -d 0.08
+run 0 ./randtgba -e 100 -s 200 -r -m -a 4 0.1 -d 0.01
+run 0 ./randtgba -e 100 -s 250 -r -m -a 4 0.1 -d 0.02
+run 0 ./randtgba -e 100 -s 300 -r -m -a 4 0.1 -d 0.04
+run 0 ./randtgba -e 100 -s 350 -r -m -a 4 0.1 -d 0.08
+run 0 ./randtgba -e 100 -s 400 -r -m -a 4 0.2 -d 0.01
+run 0 ./randtgba -e 100 -s 450 -r -m -a 4 0.2 -d 0.02
+run 0 ./randtgba -e 100 -s 500 -r -m -a 4 0.2 -d 0.04
+run 0 ./randtgba -e 100 -s 550 -r -m -a 4 0.2 -d 0.08
 
 # Bigger automata.  With valgrind this is slow, so we do less.
-run 0 ./randtgba -e 10 -s 0 -n 500 -r -a 1 0.0003 -d 0.01
-run 0 ./randtgba -e 10 -s 0 -n 500 -r -a 4 0.0003 -d 0.01
+run 0 ./randtgba -e 10 -s 0 -n 500 -r -m -a 1 0.0003 -d 0.01
+run 0 ./randtgba -e 10 -s 0 -n 500 -r -m -a 4 0.0003 -d 0.01

src/tgbatest/ltl2tgba.cc

@@ -37,6 +37,7 @@
 #include "tgba/tgbatba.hh"
 #include "tgbaalgos/gv04.hh"
 #include "tgbaalgos/magic.hh"
+#include "tgbaalgos/minimizerun.hh"
 #include "tgbaalgos/se05.hh"
 #include "tgbaalgos/tau03.hh"
 #include "tgbaalgos/tau03opt.hh"
@@ -74,6 +75,8 @@ syntax(char* prog)
 	    << "  -g    graph the accepting run on the automaton (requires -e)"
 	    << std::endl
             << "  -L    fair-loop approximation (implies -f)" << std::endl
+	    << "  -m    try to minimize accepting runs, in a second pass"
+	    << std::endl
 	    << "  -N    display the never clain for Spin "
 	    << "(implies -D)" << std::endl
             << "  -p    branching postponement (implies -f)" << std::endl
@@ -166,6 +169,7 @@ main(int argc, char** argv)
   bool post_branching = false;
   bool fair_loop_approx = false;
   bool graph_run_opt = false;
+  bool opt_minim = false;
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::atomic_prop_set* unobservables = 0;
 
@@ -241,6 +245,10 @@ main(int argc, char** argv)
 	  fair_loop_approx = true;
 	  fm_opt = true;
 	}
+      else if (!strcmp(argv[formula_index], "-m"))
+	{
+	  opt_minim = true;
+	}
       else if (!strcmp(argv[formula_index], "-N"))
 	{
 	  degeneralize_opt = DegenSBA;
@@ -725,6 +733,13 @@ main(int argc, char** argv)
 		    }
 		  else
 		    {
+		      if (opt_minim)
+			{
+			  spot::tgba_run* mini =
+			    spot::minimize_run(res->automaton(), run);
+			  delete run;
+			  run = mini;
+			}
 		      if (graph_run_opt)
 			{
 			  spot::tgba_run_dotty_decorator deco(run);

src/tgbatest/randtgba.cc

@@ -39,6 +39,7 @@
 #include "tgbaalgos/gtec/gtec.hh"
 #include "tgbaalgos/gv04.hh"
 #include "tgbaalgos/magic.hh"
+#include "tgbaalgos/minimizerun.hh"
 #include "tgbaalgos/se05.hh"
 #include "tgbaalgos/tau03.hh"
 #include "tgbaalgos/tau03opt.hh"
@@ -60,13 +61,15 @@ syntax(char* prog)
 	    << "  -e N    compare result of all "
 	    << "emptiness checks on N randomly generated graphs" << std::endl
 	    << "  -g      output in dot format" << std::endl
+	    << "  -m      try to minimize runs, in a second pass (implies -r)"
+	    << std::endl
 	    << "  -n N    number of nodes of the graph [20]" << std::endl
 	    << "  -r      compute and replay acceptance runs (implies -e)"
 	    << std::endl
 	    << "  -s N    seed for the random number generator" << std::endl
 	    << "  -t F    probability of the atomic propositions to be true"
 	    << " [0.5]" << std::endl
-	    << "  -z      display statistics about computed counter-examples"
+	    << "  -z      display statistics about computed accepting runs"
 	    << std::endl
 	    << "  -Z      like -z, but print extra statistics after the run"
 	    << " of each algorithm" << std::endl
@@ -149,7 +152,7 @@ struct ec_stat
   }
 };
 
-struct ce_stat
+struct ar_stat
 {
   int min_prefix;
   int max_prefix;
@@ -161,7 +164,7 @@ struct ce_stat
   int max_run;
   int n;
 
-  ce_stat()
+  ar_stat()
     : n(0)
   {
   }
@@ -191,6 +194,74 @@ struct ce_stat
   }
 };
 
+typedef std::map<std::string, ec_stat> ec_stats_type;
+ec_stats_type ec_stats;
+
+typedef std::map<std::string, ar_stat> ar_stats_type;
+ar_stats_type ar_stats;		// Statistics about accepting runs.
+ar_stats_type mar_stats;        // ... about minimized accepting runs.
+
+void
+print_ar_stats(ar_stats_type& ar_stats)
+{
+      std::cout << std::setw(32) << ""
+		<< " |       prefix      |       cycle       |"
+		<< std::endl << std::setw(32) << "algorithm"
+		<< " |  min < mean < max |  min < mean < max |   n "
+		<< std::endl
+		<< std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
+		<< std::endl << std::setprecision(3);
+      for (ar_stats_type::const_iterator i = ar_stats.begin();
+	   i != ar_stats.end(); ++i)
+	std::cout << std::setw(32) << i->first << " |"
+		  << std::setw(5) << i->second.min_prefix
+		  << " "
+		  << std::setw(6)
+		  << static_cast<float>(i->second.tot_prefix) / i->second.n
+		  << " "
+		  << std::setw(5) << i->second.max_prefix
+		  << " |"
+		  << std::setw(5) << i->second.min_cycle
+		  << " "
+		  << std::setw(6)
+		  << static_cast<float>(i->second.tot_cycle) / i->second.n
+		  << " "
+		  << std::setw(5) << i->second.max_cycle
+		  << " |"
+		  << std::setw(5) << i->second.n
+		  << std::endl;
+      std::cout << std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
+		<< std::endl
+		<< std::setw(32) << ""
+		<< " |        runs       |       total      |"
+		<< std::endl << std::setw(32) << "algorithm"
+		<< " |  min < mean < max | pre.  cyc.  runs |   n "
+		<< std::endl
+		<< std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
+		<< std::endl;
+      for (ar_stats_type::const_iterator i = ar_stats.begin();
+	   i != ar_stats.end(); ++i)
+	std::cout << std::setw(32) << i->first << " |"
+		  << std::setw(5)
+		  << i->second.min_run
+		  << " "
+		  << std::setw(6)
+		  << static_cast<float>(i->second.tot_prefix
+					+ i->second.tot_cycle) / i->second.n
+		  << " "
+		  << std::setw(5)
+		  << i->second.max_run
+		  << " |"
+		  << std::setw(5) << i->second.tot_prefix
+		  << " "
+		  << std::setw(5) << i->second.tot_cycle
+		  << " "
+		  << std::setw(5) << i->second.tot_prefix + i->second.tot_cycle
+		  << " |"
+		  << std::setw(5) << i->second.n
+		  << std::endl;
+}
+
 int
 main(int argc, char** argv)
 {
@@ -206,18 +277,13 @@ main(int argc, char** argv)
   bool opt_dot = false;
   int opt_ec = 0;
   int opt_ec_seed = 0;
+  bool opt_minim = false;
   bool opt_replay = false;
   bool opt_degen = false;
   int argn = 0;
 
   int exit_code = 0;
 
-  typedef std::map<std::string, ec_stat> ec_stats_type;
-  ec_stats_type ec_stats;
-
-  typedef std::map<std::string, ce_stat> ce_stats_type;
-  ce_stats_type ce_stats;
-
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set;
 
@@ -255,6 +321,13 @@ main(int argc, char** argv)
 	{
 	  opt_dot = true;
 	}
+      else if (!strcmp(argv[argn], "-m"))
+	{
+	  opt_minim = true;
+	  opt_replay = true;
+	  if (!opt_ec)
+	    opt_ec = 1;
+	}
       else if (!strcmp(argv[argn], "-n"))
 	{
 	  if (argc < argn + 2)
@@ -340,11 +413,11 @@ main(int argc, char** argv)
 	      spot::tgba* d = opt_n_acc > 1 ? degen : a;
 
 	      ec_obj.push_back(spot::explicit_magic_search(d));
-	      ec_name.push_back("explicit_magic");
+	      ec_name.push_back("explicit_magic_search");
 	      ec_safe.push_back(true);
 
 	      ec_obj.push_back(spot::bit_state_hashing_magic_search(d, 4096));
-	      ec_name.push_back("bit_state_hashing_magic");
+	      ec_name.push_back("bit_state_hashing_magic_search");
 	      ec_safe.push_back(false);
 
 	      ec_obj.push_back(spot::explicit_se05_search(d));
@@ -390,7 +463,7 @@ main(int argc, char** argv)
 		ec_stats[algo].count(ecs);
 	      if (res)
 		{
-		  std::cout << "accepting run exists";
+		  std::cout << "acc. run";
 		  ++n_non_empty;
 		  if (opt_replay)
 		    {
@@ -405,19 +478,45 @@ main(int argc, char** argv)
 			    }
 			  else
 			    {
-			      std::cout << ", computed OK";
+			      std::cout << ", computed";
 			      if (opt_z)
-				ce_stats[algo].count(run);
+				ar_stats[algo].count(run);
 			    }
 			  if (opt_z)
 			    std::cout << " [" << run->prefix.size()
-				      << " + " << run->cycle.size()
+				      << "+" << run->cycle.size()
 				      << "]";
+
+			  if (opt_minim)
+			    {
+			      spot::tgba_run* minrun =
+				spot::minimize_run(a, run);
+			      if (!spot::replay_tgba_run(s, res->automaton(),
+							 minrun))
+				{
+				  std::cout << ", but could not replay "
+					    << "its minimization (ERROR!)";
+				  failed_seeds.insert(opt_ec_seed);
+				}
+			      else
+				{
+				  std::cout << ", minimized";
+				  if (opt_z)
+				    mar_stats[algo].count(minrun);
+				}
+			      if (opt_z)
+				{
+				  std::cout << " [" << minrun->prefix.size()
+					    << "+" << minrun->cycle.size()
+					    << "]";
+				}
+			      delete minrun;
+			    }
 			  delete run;
 			}
 		      else
 			{
-			  std::cout << ", not computed";
+			  std::cout << " exists, not computed";
 			}
 		    }
 		  std::cout << std::endl;
@@ -519,66 +618,17 @@ main(int argc, char** argv)
 		  << std::endl;
     }
 
-  if (!ce_stats.empty())
+  if (!ar_stats.empty())
     {
-      std::cout << "Statistics about counter-examples:" << std::endl;
-      std::cout << std::setw(32) << ""
-		<< " |       prefix      |       cycle       |"
-		<< std::endl << std::setw(32) << "algorithm"
-		<< " |  min < mean < max |  min < mean < max |   n "
-		<< std::endl
-		<< std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
-		<< std::endl << std::setprecision(3);
-      for (ce_stats_type::const_iterator i = ce_stats.begin();
-                                                i != ce_stats.end(); ++i)
-	std::cout << std::setw(32) << i->first << " |"
-		  << std::setw(5) << i->second.min_prefix
-		  << " "
-		  << std::setw(6)
-		  << static_cast<float>(i->second.tot_prefix) / i->second.n
-		  << " "
-		  << std::setw(5) << i->second.max_prefix
-		  << " |"
-		  << std::setw(5) << i->second.min_cycle
-		  << " "
-		  << std::setw(6)
-		  << static_cast<float>(i->second.tot_cycle) / i->second.n
-		  << " "
-		  << std::setw(5) << i->second.max_cycle
-		  << " |"
-		  << std::setw(5) << i->second.n
-		  << std::endl;
-      std::cout << std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
-		<< std::endl
-		<< std::setw(32) << ""
-		<< " |        runs       |       total      |"
-		<< std::endl << std::setw(32) << "algorithm"
-		<< " |  min < mean < max | pre.  cyc.  runs |   n "
-		<< std::endl
-		<< std::setw(79) << std::setfill('-') << "" << std::setfill(' ')
-		<< std::endl;