* tgbatest/randtgba.cc: Add options -e and -r.

* tgbatest/emptchkr.test: New file.
* src/tgbatest/Makefile.am (TESTS, XFAIL_TESTS): Add emptchkr.test.

ChangeLog

@@ -1,5 +1,9 @@
 2004-11-15  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* tgbatest/randtgba.cc: Add options -e and -r.
+	* tgbatest/emptchkr.test: New file.
+	* src/tgbatest/Makefile.am (TESTS, XFAIL_TESTS): Add emptchkr.test.
+
 	* src/tgbaalgos/replayrun.cc (replay_tgba_run): Fix a memory leak
 	if debug==false.
 

src/tgbatest/Makefile.am

@@ -83,7 +83,9 @@ TESTS = \
   emptchk.test \
   emptchke.test \
   dfs.test \
+  emptchkr.test \
   spotlbtt.test
+XFAIL_TESTS = emptchkr.test
 
 EXTRA_DIST = $(TESTS) ltl2baw.pl
 

src/tgbatest/emptchkr.test

@@ -0,0 +1,51 @@
+#!/bin/sh
+# 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.
+
+# Emptiness check on randomly generated state spaces.
+
+. ./defs
+
+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
+
+# 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
+
+# Two 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
+
+# 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

src/tgbatest/randtgba.cc

@@ -21,6 +21,7 @@
 
 #include <cstdlib>
 #include <iostream>
+#include <sstream>
 #include "ltlvisit/apcollect.hh"
 #include "ltlvisit/destroy.hh"
 #include "tgbaalgos/randomgraph.hh"
@@ -30,6 +31,11 @@
 #include "tgbaalgos/dotty.hh"
 #include "misc/random.hh"
 
+#include "tgbaalgos/emptiness.hh"
+#include "tgbaalgos/gtec/gtec.hh"
+#include "tgbaalgos/magic.hh"
+#include "tgbaalgos/replayrun.hh"
+
 void
 syntax(char* prog)
 {
@@ -39,12 +45,15 @@ syntax(char* prog)
 	    << "  -a N F  number of accepence conditions a propability that"
 	    << " one is true [0 0.0]" << std::endl
 	    << "  -d F    density of the graph [0.2]" << std::endl
+	    << "  -e N    compare result of all "
+	    << "emptiness checks on N randomly generated graphs" << std::endl
 	    << "  -g      output in dot format" << 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]"
+	    << " [0.5]" << std::endl
-	    << std::endl
 	    << "Where:" << std::endl
 	    << "  F      are floats between 0.0 and 1.0 inclusive" << std::endl
 	    << "  N      are positive integers" << std::endl
@@ -89,9 +98,14 @@ main(int argc, char** argv)
   float opt_t = 0.5;
 
   bool opt_dot = false;
+  int opt_ec = 0;
+  int opt_ec_seed = 0;
+  bool opt_replay = false;
 
   int argn = 0;
 
+  int exit_code = 0;
+
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set;
 
@@ -109,29 +123,42 @@ main(int argc, char** argv)
 	}
       else if (!strcmp(argv[argn], "-d"))
 	{
-	  if (argc < argn + 1)
+	  if (argc < argn + 2)
 	    syntax(argv[0]);
 	  opt_d = to_float(argv[++argn]);
 	}
+      else if (!strcmp(argv[argn], "-e"))
+	{
+	  if (argc < argn + 2)
+	    syntax(argv[0]);
+	  opt_ec = to_int(argv[++argn]);
+	}
       else if (!strcmp(argv[argn], "-g"))
 	{
 	  opt_dot = true;
 	}
       else if (!strcmp(argv[argn], "-n"))
 	{
-	  if (argc < argn + 1)
+	  if (argc < argn + 2)
 	    syntax(argv[0]);
 	  opt_n = to_int(argv[++argn]);
 	}
+      else if (!strcmp(argv[argn], "-r"))
+	{
+	  opt_replay = true;
+	  if (!opt_ec)
+	    opt_ec = 1;
+	}
       else if (!strcmp(argv[argn], "-s"))
 	{
-	  if (argc < argn + 1)
+	  if (argc < argn + 2)
 	    syntax(argv[0]);
-	  spot::srand(to_int(argv[++argn]));
+	  opt_ec_seed = to_int(argv[++argn]);
+	  spot::srand(opt_ec_seed);
 	}
       else if (!strcmp(argv[argn], "-t"))
 	{
-	  if (argc < argn + 1)
+	  if (argc < argn + 2)
 	    syntax(argv[0]);
 	  opt_t = to_float(argv[++argn]);
 	}
@@ -144,20 +171,149 @@ main(int argc, char** argv)
 
   spot::bdd_dict* dict = new spot::bdd_dict();
 
-  spot::tgba* a = spot::random_graph(opt_n, opt_d, ap, dict,
-				     opt_n_acc, opt_a, opt_t, &env);
 
-  if (opt_dot)
+  std::set<int> failed_seeds;
-    dotty_reachable(std::cout, a);
+  do
-  else
+    {
-    tgba_save_reachable(std::cout, a);
+      if (opt_ec)
+	{
+	  std::cout << "seed: " << opt_ec_seed << std::endl;
+	  spot::srand(opt_ec_seed);
+	}
+
+      spot::tgba* a = spot::random_graph(opt_n, opt_d, ap, dict,
+					 opt_n_acc, opt_a, opt_t, &env);
+
+      if (!opt_ec)
+	{
+	  if (opt_dot)
+	    dotty_reachable(std::cout, a);
+	  else
+	    tgba_save_reachable(std::cout, a);
+	}
+      else
+	{
+	  std::vector<spot::emptiness_check*> ec_obj;
+	  std::vector<std::string> ec_name;
+	  std::vector<bool> ec_safe;
+
+	  ec_obj.push_back(new spot::couvreur99_check(a));
+	  ec_name.push_back("couvreur99");
+	  ec_safe.push_back(true);
+
+	  ec_obj.push_back(new spot::couvreur99_check_shy(a));
+	  ec_name.push_back("couvreur99_shy");
+	  ec_safe.push_back(true);
+
+	  if (opt_n_acc <= 1)
+	    {
+	      ec_obj.push_back(spot::explicit_magic_search(a));
+	      ec_name.push_back("explicit_magic_search");
+	      ec_safe.push_back(true);
+
+	      ec_obj.push_back(spot::bit_state_hashing_magic_search(a, 4096));
+	      ec_name.push_back("bit_state_hashing_magic_search");
+	      ec_safe.push_back(false);
+
+	      ec_obj.push_back(spot::explicit_se05_search(a));
+	      ec_name.push_back("explicit_se05");
+	      ec_safe.push_back(true);
+
+	      ec_obj.push_back(spot::bit_state_hashing_se05_search(a, 4096));
+	      ec_name.push_back("bit_state_hashing_se05_search");
+	      ec_safe.push_back(false);
+	    }
+
+	  int n_ec = ec_obj.size();
+	  int n_empty = 0;
+	  int n_non_empty = 0;
+	  int n_maybe_empty = 0;
+
+	  for (int i = 0; i < n_ec; ++i)
+	    {
+	      std::cout.width(32);
+	      std::cout << ec_name[i] << ": ";
+	      spot::emptiness_check_result* res = ec_obj[i]->check();
+	      if (res)
+		{
+		  std::cout << "accepting run exists";
+		  ++n_non_empty;
+		  if (opt_replay)
+		    {
+		      spot::tgba_run* run = res->accepting_run();
+		      if (run)
+			{
+			  std::ostringstream s;
+			  if (!spot::replay_tgba_run(s, a, run))
+			    {
+			      std::cout << ", but could not replay it (ERROR!)";
+			      failed_seeds.insert(opt_ec_seed);
+			    }
+			  else
+			    {
+			      std::cout << ", computed OK";
+			    }
+			  delete run;
+			}
+		      else
+			{
+			  std::cout << ", not computed";
+			}
+		    }
+		  std::cout << std::endl;
+		  delete res;
+		}
+	      else
+		{
+		  if (ec_safe[i])
+		    {
+		      std::cout << "empty language" << std::endl;
+		      ++n_empty;
+		    }
+		  else
+		    {
+		      std::cout << "maybe empty language" << std::endl;
+		      ++n_maybe_empty;
+		    }
+
+		}
+	      delete ec_obj[i];
+	    }
+
+	  assert(n_empty + n_non_empty + n_maybe_empty == n_ec);
+
+	  if ((n_empty == 0 && (n_non_empty + n_maybe_empty) != n_ec)
+	      || (n_empty != 0 && n_non_empty != 0))
+	    {
+	      std::cout << "ERROR: not all algorithms agree" << std::endl;
+	      failed_seeds.insert(opt_ec_seed);
+	    }
+	}
+
+      delete a;
+
+      if (opt_ec)
+	{
+	  --opt_ec;
+	  ++opt_ec_seed;
+	}
+    }
+  while (opt_ec);
+  if (!failed_seeds.empty())
+    {
+      exit_code = 1;
+      std::cout << "The check failed for the following seeds:";
+      for (std::set<int>::const_iterator i = failed_seeds.begin();
+	   i != failed_seeds.end(); ++i)
+	std::cout << " " << *i;
+      std::cout << std::endl;
+    }
 
   for (spot::ltl::atomic_prop_set::iterator i = ap->begin();
        i != ap->end(); ++i)
     spot::ltl::destroy(*i);
 
-  delete a;
-  delete dict;
   delete ap;
-  return 0;
+  delete dict;
+  return exit_code;
 }