From 6724f4bfbb2ec8b5927c5179401c3d923cc052b2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 26 Nov 2004 23:54:53 +0000 Subject: [PATCH] * 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 | 10 ++ src/tgbaalgos/Makefile.am | 2 + src/tgbaalgos/minimizerun.cc | 188 ++++++++++++++++++++++++++++++++ src/tgbaalgos/minimizerun.hh | 37 +++++++ src/tgbatest/emptchkr.test | 30 +++--- src/tgbatest/ltl2tgba.cc | 15 +++ src/tgbatest/randtgba.cc | 200 ++++++++++++++++++++++------------- 7 files changed, 392 insertions(+), 90 deletions(-) create mode 100644 src/tgbaalgos/minimizerun.cc create mode 100644 src/tgbaalgos/minimizerun.hh diff --git a/ChangeLog b/ChangeLog index b77560050..c9daa64cd 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2004-11-27 Alexandre Duret-Lutz + Denis Poitrenaud + + * 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 * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 519ca30b3..bdd139d5d 100644 --- a/src/tgbaalgos/Makefile.am +++ b/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 \ diff --git a/src/tgbaalgos/minimizerun.cc b/src/tgbaalgos/minimizerun.cc new file mode 100644 index 000000000..71474a8e1 --- /dev/null +++ b/src/tgbaalgos/minimizerun.cc @@ -0,0 +1,188 @@ +// 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 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; + } +} diff --git a/src/tgbaalgos/minimizerun.hh b/src/tgbaalgos/minimizerun.hh new file mode 100644 index 000000000..7bf897a6e --- /dev/null +++ b/src/tgbaalgos/minimizerun.hh @@ -0,0 +1,37 @@ +// 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 diff --git a/src/tgbatest/emptchkr.test b/src/tgbatest/emptchkr.test index 201a8d144..c11fa6eaa 100755 --- a/src/tgbatest/emptchkr.test +++ b/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 diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 76c89c8fb..693582856 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/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); diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 53bb88d50..0a8195089 100644 --- a/src/tgbatest/randtgba.cc +++ b/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 ec_stats_type; +ec_stats_type ec_stats; + +typedef std::map 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(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(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(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 ec_stats_type; - ec_stats_type ec_stats; - - typedef std::map 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(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(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 (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_run - << " " - << std::setw(6) - << static_cast(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; - + std::cout << std::endl + << "Statistics about accepting runs:" << std::endl; + print_ar_stats(ar_stats); + } + if (!mar_stats.empty()) + { + std::cout << std::endl + << "Statistics about minimized accepting runs:" << std::endl; + print_ar_stats(mar_stats); } if (!failed_seeds.empty())