From e58743dbb7a24ec8f88a4d816f89880cc129fb82 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 29 Nov 2004 10:01:08 +0000 Subject: [PATCH] * src/tgbaalgos/minimizerun.cc, src/tgbaalgos/minimizerun.hh (minimize_run): Rename as ... * src/tgbaalgos/reducerun.cc, src/tgbaalgos/reducerun.hh: (reduce_run): ... this. * src/tgbaalgos/Makefile.am, src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Adjust all references. --- ChangeLog | 7 +++++ src/tgbaalgos/Makefile.am | 4 +-- .../{minimizerun.cc => reducerun.cc} | 4 +-- .../{minimizerun.hh => reducerun.hh} | 11 ++++---- src/tgbatest/ltl2tgba.cc | 16 +++++------ src/tgbatest/randtgba.cc | 28 +++++++++---------- 6 files changed, 39 insertions(+), 31 deletions(-) rename src/tgbaalgos/{minimizerun.cc => reducerun.cc} (98%) rename src/tgbaalgos/{minimizerun.hh => reducerun.hh} (82%) diff --git a/ChangeLog b/ChangeLog index 6f634ce09..5ff87ce75 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,12 @@ 2004-11-29 Alexandre Duret-Lutz + * src/tgbaalgos/minimizerun.cc, src/tgbaalgos/minimizerun.hh + (minimize_run): Rename as ... + * src/tgbaalgos/reducerun.cc, src/tgbaalgos/reducerun.hh: + (reduce_run): ... this. + * src/tgbaalgos/Makefile.am, src/tgbatest/ltl2tgba.cc, + src/tgbatest/randtgba.cc: Adjust all references. + * src/tgbatest/emptchkr.test: Try degeneralized automata. * src/tgbatest/randtgba.cc (main): Pass the correct automaton to minimize_run(). diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index bdd139d5d..70ddafccf 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -38,12 +38,12 @@ tgbaalgos_HEADERS = \ ltl2tgba_fm.hh \ ltl2tgba_lacim.hh \ magic.hh \ - minimizerun.hh \ neverclaim.hh \ powerset.hh \ projrun.hh \ randomgraph.hh \ reachiter.hh \ + reducerun.hh \ replayrun.hh \ rundotdec.hh \ save.hh \ @@ -66,12 +66,12 @@ libtgbaalgos_la_SOURCES = \ ltl2tgba_fm.cc \ ltl2tgba_lacim.cc \ magic.cc \ - minimizerun.cc \ neverclaim.cc \ powerset.cc \ projrun.cc \ randomgraph.cc \ reachiter.cc \ + reducerun.cc \ replayrun.cc \ rundotdec.cc \ save.cc \ diff --git a/src/tgbaalgos/minimizerun.cc b/src/tgbaalgos/reducerun.cc similarity index 98% rename from src/tgbaalgos/minimizerun.cc rename to src/tgbaalgos/reducerun.cc index 750276602..acd446670 100644 --- a/src/tgbaalgos/minimizerun.cc +++ b/src/tgbaalgos/reducerun.cc @@ -23,7 +23,7 @@ #include "emptiness.hh" #include "tgba/tgba.hh" #include "bfssteps.hh" -#include "minimizerun.hh" +#include "reducerun.hh" namespace spot { @@ -89,7 +89,7 @@ namespace spot } tgba_run* - minimize_run(const tgba* a, const tgba_run* org) + reduce_run(const tgba* a, const tgba_run* org) { tgba_run* res = new tgba_run; state_set ss; diff --git a/src/tgbaalgos/minimizerun.hh b/src/tgbaalgos/reducerun.hh similarity index 82% rename from src/tgbaalgos/minimizerun.hh rename to src/tgbaalgos/reducerun.hh index 7bf897a6e..ef1b542bc 100644 --- a/src/tgbaalgos/minimizerun.hh +++ b/src/tgbaalgos/reducerun.hh @@ -19,19 +19,20 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#ifndef SPOT_TGBAALGOS_MINIMIZERUN_HH -# define SPOT_TGBAALGOS_MINIMIZERUN_HH +#ifndef SPOT_TGBAALGOS_REDUCERUN_HH +# define SPOT_TGBAALGOS_REDUCERUN_HH namespace spot { class tgba; class tgba_run; - /// \brief Minimize an accepting run. + /// \brief Reduce an accepting run. + /// \ingroup tgba_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); + tgba_run* reduce_run(const tgba* a, const tgba_run* org); } -#endif // SPOT_TGBAALGOS_MINIMIZERUN_HH +#endif // SPOT_TGBAALGOS_REDUCERUN_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index d5faa95f9..19936972e 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -37,7 +37,7 @@ #include "tgba/tgbatba.hh" #include "tgbaalgos/gv04.hh" #include "tgbaalgos/magic.hh" -#include "tgbaalgos/minimizerun.hh" +#include "tgbaalgos/reducerun.hh" #include "tgbaalgos/se05.hh" #include "tgbaalgos/tau03.hh" #include "tgbaalgos/tau03opt.hh" @@ -75,7 +75,7 @@ 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" + << " -m try to reduce accepting runs, in a second pass" << std::endl << " -N display the never clain for Spin " << "(implies -D)" << std::endl @@ -170,7 +170,7 @@ main(int argc, char** argv) bool post_branching = false; bool fair_loop_approx = false; bool graph_run_opt = false; - bool opt_minim = false; + bool opt_reduce = false; spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* unobservables = 0; @@ -248,7 +248,7 @@ main(int argc, char** argv) } else if (!strcmp(argv[formula_index], "-m")) { - opt_minim = true; + opt_reduce = true; } else if (!strcmp(argv[formula_index], "-N")) { @@ -734,12 +734,12 @@ main(int argc, char** argv) } else { - if (opt_minim) + if (opt_reduce) { - spot::tgba_run* mini = - spot::minimize_run(res->automaton(), run); + spot::tgba_run* redrun = + spot::reduce_run(res->automaton(), run); delete run; - run = mini; + run = redrun; } if (graph_run_opt) { diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index d166c073b..8f8c8dfbc 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -39,7 +39,7 @@ #include "tgbaalgos/gtec/gtec.hh" #include "tgbaalgos/gv04.hh" #include "tgbaalgos/magic.hh" -#include "tgbaalgos/minimizerun.hh" +#include "tgbaalgos/reducerun.hh" #include "tgbaalgos/se05.hh" #include "tgbaalgos/tau03.hh" #include "tgbaalgos/tau03opt.hh" @@ -61,7 +61,7 @@ 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)" + << " -m try to reduce 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)" @@ -278,7 +278,7 @@ main(int argc, char** argv) bool opt_dot = false; int opt_ec = 0; int opt_ec_seed = 0; - bool opt_minim = false; + bool opt_reduce = false; bool opt_replay = false; bool opt_degen = false; int argn = 0; @@ -324,7 +324,7 @@ main(int argc, char** argv) } else if (!strcmp(argv[argn], "-m")) { - opt_minim = true; + opt_reduce = true; opt_replay = true; if (!opt_ec) opt_ec = 1; @@ -488,12 +488,12 @@ main(int argc, char** argv) << "+" << run->cycle.size() << "]"; - if (opt_minim) + if (opt_reduce) { - spot::tgba_run* minrun = - spot::minimize_run(res->automaton(), run); + spot::tgba_run* redrun = + spot::reduce_run(res->automaton(), run); if (!spot::replay_tgba_run(s, res->automaton(), - minrun)) + redrun)) { std::cout << ", but could not replay " << "its minimization (ERROR!)"; @@ -501,17 +501,17 @@ main(int argc, char** argv) } else { - std::cout << ", minimized"; + std::cout << ", reduced"; if (opt_z) - mar_stats[algo].count(minrun); + mar_stats[algo].count(redrun); } if (opt_z) { - std::cout << " [" << minrun->prefix.size() - << "+" << minrun->cycle.size() + std::cout << " [" << redrun->prefix.size() + << "+" << redrun->cycle.size() << "]"; } - delete minrun; + delete redrun; } delete run; } @@ -628,7 +628,7 @@ main(int argc, char** argv) if (!mar_stats.empty()) { std::cout << std::endl - << "Statistics about minimized accepting runs:" << std::endl; + << "Statistics about reduced accepting runs:" << std::endl; print_ar_stats(mar_stats); }