diff --git a/ChangeLog b/ChangeLog index 716521fcc..efb27fc7e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,9 @@ 2004-11-15 Alexandre Duret-Lutz + * 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. diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index a43d93491..d32a26294 100644 --- a/src/tgbatest/Makefile.am +++ b/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 diff --git a/src/tgbatest/emptchkr.test b/src/tgbatest/emptchkr.test new file mode 100755 index 000000000..5da9970c4 --- /dev/null +++ b/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 diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index b8ef45fd1..1e7ce787f 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -21,6 +21,7 @@ #include #include +#include #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]" - << std::endl + << " [0.5]" << 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) - dotty_reachable(std::cout, a); - else - tgba_save_reachable(std::cout, a); + std::set failed_seeds; + do + { + 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 ec_obj; + std::vector ec_name; + std::vector 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::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; }