diff --git a/ChangeLog b/ChangeLog index 0177c0f8f..30a7bef75 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2010-01-30 Alexandre Duret-Lutz + + Remove the theoretically bogus "containment" option of ltl2tgba_fm. + + * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh: + Remove the containment option. + * src/tgbafromfile.cc, src/tgbafromfile.hh: Remove the + containment_ member. + * src/tgbatest/ltl2tgba.cc (syntax): Remove -c option for + FM algorithm, use it exclusively for TAA. + 2010-01-30 Alexandre Duret-Lutz * src/tgba/tgbasafracomplement.hh: Add missing copyright and diff --git a/src/tgba/tgbafromfile.cc b/src/tgba/tgbafromfile.cc index 5895988f0..9907e6e6b 100644 --- a/src/tgba/tgbafromfile.cc +++ b/src/tgba/tgbafromfile.cc @@ -1,6 +1,5 @@ -// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire -// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis -// Coopératifs (SRC), Université Pierre et Marie Curie. +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -36,7 +35,6 @@ namespace spot fm_symb_merge_opt_ = true; post_branching_ = false; fair_loop_approx_ = false; - containment_ = false; unobservables_ = 0; fm_red_ = ltl::Reduce_None; } @@ -79,7 +77,7 @@ namespace spot a = spot::ltl_to_tgba_fm(f_, dict_, fm_exprop_opt_, fm_symb_merge_opt_, post_branching_, fair_loop_approx_, unobservables_, - fm_red_, containment_); + fm_red_); return a; } diff --git a/src/tgba/tgbafromfile.hh b/src/tgba/tgbafromfile.hh index fd48a1f48..2d47703a4 100644 --- a/src/tgba/tgbafromfile.hh +++ b/src/tgba/tgbafromfile.hh @@ -1,6 +1,5 @@ -// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire -// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis -// Coopératifs (SRC), Université Pierre et Marie Curie. +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -53,7 +52,6 @@ namespace spot bool fm_symb_merge_opt_; bool post_branching_; bool fair_loop_approx_; - bool containment_; ltl::atomic_prop_set* unobservables_; int fm_red_; }; diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index a92a29f03..91e26b4d0 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -557,12 +557,10 @@ namespace spot { public: formula_canonizer(translate_dict& d, - bool fair_loop_approx, bdd all_promises, - language_containment_checker* lcc) + bool fair_loop_approx, bdd all_promises) : v_(d), fair_loop_approx_(fair_loop_approx), - all_promises_(all_promises), - lcc_(lcc) + all_promises_(all_promises) { // For cosmetics, register 1 initially, so the algorithm will // not register an equivalent formula first. @@ -631,22 +629,6 @@ namespace spot f->destroy(); f = i->second->clone(); } - else if (new_variable && lcc_) - { - // It's a new bdd for a new formula. Let's see if we can - // find an equivalent formula with language containment - // checks. - for (formula_to_bdd_map::const_iterator j = f2b_.begin(); - j != f2b_.end(); ++j) - if (f != j->first && lcc_->equal(f, j->first)) - { - f2b_[f] = j->second; - i->second = j->first; - f->destroy(); - f = i->second->clone(); - break; - } - } return f; } @@ -667,7 +649,6 @@ namespace spot possible_fair_loop_checker pflc_; bool fair_loop_approx_; bdd all_promises_; - language_containment_checker* lcc_; }; } @@ -698,10 +679,8 @@ namespace spot ltl_to_tgba_fm(const formula* f, bdd_dict* dict, bool exprop, bool symb_merge, bool branching_postponement, bool fair_loop_approx, const atomic_prop_set* unobs, - int reduce_ltl, bool containment_checks) + int reduce_ltl) { - symb_merge |= containment_checks; - // Normalize the formula. We want all the negations on // the atomic propositions. We also suppress logic // abbreviations such as <=>, =>, or XOR, since they @@ -733,12 +712,7 @@ namespace spot all_promises = pv.result(); } - language_containment_checker lcc(dict, exprop, symb_merge, - branching_postponement, - fair_loop_approx); - - formula_canonizer fc(d, fair_loop_approx, all_promises, - containment_checks ? &lcc : 0); + formula_canonizer fc(d, fair_loop_approx, all_promises); // These are used when atomic propositions are interpreted as // events. There are two kinds of events: observable events are diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index 0b7725115..61d657816 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -1,3 +1,5 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -125,8 +127,7 @@ namespace spot bool branching_postponement = false, bool fair_loop_approx = false, const ltl::atomic_prop_set* unobs = 0, - int reduce_ltl = ltl::Reduce_None, - bool containment_checks = false); + int reduce_ltl = ltl::Reduce_None); } #endif // SPOT_TGBAALGOS_LTL2TGBA_FM_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 68ddec072..5214a3332 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -121,8 +121,6 @@ syntax(char* prog) << std::endl << "Options for Couvreur's FM algorithm (-f):" << std::endl - << " -c enable language containment checks (implies -f)" - << std::endl << " -fr1 use -r1 (see below) at each step of FM" << std::endl << " -fr2 use -r2 (see below) at each step of FM" << std::endl << " -fr3 use -r3 (see below) at each step of FM" << std::endl @@ -159,7 +157,7 @@ syntax(char* prog) << "Options for Tauriainen's TAA-based algorithm (-taa):" << std::endl - << " -c enable language containment checks" << std::endl + << " -c enable language containment checks (implies -taa)" << std::endl << "Formula simplification (before translation):" @@ -329,8 +327,7 @@ main(int argc, char** argv) else if (!strcmp(argv[formula_index], "-c")) { containment = true; - if (translation != TransTAA) - translation = TransFM; + translation = TransTAA; } else if (!strcmp(argv[formula_index], "-d")) { @@ -764,7 +761,7 @@ main(int argc, char** argv) post_branching, fair_loop_approx, unobservables, - fm_red, containment); + fm_red); break; case TransTAA: a = spot::ltl_to_taa(f, dict, containment);