Commit dd71e37d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 7cc2776d
2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.fr> 2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/tgba/tgbasafracomplement.hh: Add missing copyright and * src/tgba/tgbasafracomplement.hh: Add missing copyright and
......
// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire // Copyright (C) 2009, 2010 Laboratoire de Recherche et Dveloppement
// d'Informatique de Paris 6 (LIP6), dpartement Systmes Rpartis // de l'Epita (LRDE).
// Coopratifs (SRC), Universit Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -36,7 +35,6 @@ namespace spot ...@@ -36,7 +35,6 @@ namespace spot
fm_symb_merge_opt_ = true; fm_symb_merge_opt_ = true;
post_branching_ = false; post_branching_ = false;
fair_loop_approx_ = false; fair_loop_approx_ = false;
containment_ = false;
unobservables_ = 0; unobservables_ = 0;
fm_red_ = ltl::Reduce_None; fm_red_ = ltl::Reduce_None;
} }
...@@ -79,7 +77,7 @@ namespace spot ...@@ -79,7 +77,7 @@ namespace spot
a = spot::ltl_to_tgba_fm(f_, dict_, fm_exprop_opt_, a = spot::ltl_to_tgba_fm(f_, dict_, fm_exprop_opt_,
fm_symb_merge_opt_, post_branching_, fm_symb_merge_opt_, post_branching_,
fair_loop_approx_, unobservables_, fair_loop_approx_, unobservables_,
fm_red_, containment_); fm_red_);
return a; return a;
} }
......
// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire // Copyright (C) 2009, 2010 Laboratoire de Recherche et Dveloppement
// d'Informatique de Paris 6 (LIP6), dpartement Systmes Rpartis // de l'Epita (LRDE).
// Coopratifs (SRC), Universit Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -53,7 +52,6 @@ namespace spot ...@@ -53,7 +52,6 @@ namespace spot
bool fm_symb_merge_opt_; bool fm_symb_merge_opt_;
bool post_branching_; bool post_branching_;
bool fair_loop_approx_; bool fair_loop_approx_;
bool containment_;
ltl::atomic_prop_set* unobservables_; ltl::atomic_prop_set* unobservables_;
int fm_red_; int fm_red_;
}; };
......
...@@ -557,12 +557,10 @@ namespace spot ...@@ -557,12 +557,10 @@ namespace spot
{ {
public: public:
formula_canonizer(translate_dict& d, formula_canonizer(translate_dict& d,
bool fair_loop_approx, bdd all_promises, bool fair_loop_approx, bdd all_promises)
language_containment_checker* lcc)
: v_(d), : v_(d),
fair_loop_approx_(fair_loop_approx), fair_loop_approx_(fair_loop_approx),
all_promises_(all_promises), all_promises_(all_promises)
lcc_(lcc)
{ {
// For cosmetics, register 1 initially, so the algorithm will // For cosmetics, register 1 initially, so the algorithm will
// not register an equivalent formula first. // not register an equivalent formula first.
...@@ -631,22 +629,6 @@ namespace spot ...@@ -631,22 +629,6 @@ namespace spot
f->destroy(); f->destroy();
f = i->second->clone(); 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; return f;
} }
...@@ -667,7 +649,6 @@ namespace spot ...@@ -667,7 +649,6 @@ namespace spot
possible_fair_loop_checker pflc_; possible_fair_loop_checker pflc_;
bool fair_loop_approx_; bool fair_loop_approx_;
bdd all_promises_; bdd all_promises_;
language_containment_checker* lcc_;
}; };
} }
...@@ -698,10 +679,8 @@ namespace spot ...@@ -698,10 +679,8 @@ namespace spot
ltl_to_tgba_fm(const formula* f, bdd_dict* dict, ltl_to_tgba_fm(const formula* f, bdd_dict* dict,
bool exprop, bool symb_merge, bool branching_postponement, bool exprop, bool symb_merge, bool branching_postponement,
bool fair_loop_approx, const atomic_prop_set* unobs, 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 // Normalize the formula. We want all the negations on
// the atomic propositions. We also suppress logic // the atomic propositions. We also suppress logic
// abbreviations such as <=>, =>, or XOR, since they // abbreviations such as <=>, =>, or XOR, since they
...@@ -733,12 +712,7 @@ namespace spot ...@@ -733,12 +712,7 @@ namespace spot
all_promises = pv.result(); all_promises = pv.result();
} }
language_containment_checker lcc(dict, exprop, symb_merge, formula_canonizer fc(d, fair_loop_approx, all_promises);
branching_postponement,
fair_loop_approx);
formula_canonizer fc(d, fair_loop_approx, all_promises,
containment_checks ? &lcc : 0);
// These are used when atomic propositions are interpreted as // These are used when atomic propositions are interpreted as
// events. There are two kinds of events: observable events are // events. There are two kinds of events: observable events are
......
// Copyright (C) 2010 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
...@@ -125,8 +127,7 @@ namespace spot ...@@ -125,8 +127,7 @@ namespace spot
bool branching_postponement = false, bool branching_postponement = false,
bool fair_loop_approx = false, bool fair_loop_approx = false,
const ltl::atomic_prop_set* unobs = 0, const ltl::atomic_prop_set* unobs = 0,
int reduce_ltl = ltl::Reduce_None, int reduce_ltl = ltl::Reduce_None);
bool containment_checks = false);
} }
#endif // SPOT_TGBAALGOS_LTL2TGBA_FM_HH #endif // SPOT_TGBAALGOS_LTL2TGBA_FM_HH
...@@ -121,8 +121,6 @@ syntax(char* prog) ...@@ -121,8 +121,6 @@ syntax(char* prog)
<< std::endl << std::endl
<< "Options for Couvreur's FM algorithm (-f):" << 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 << " -fr1 use -r1 (see below) at each step of FM" << std::endl
<< " -fr2 use -r2 (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 << " -fr3 use -r3 (see below) at each step of FM" << std::endl
...@@ -159,7 +157,7 @@ syntax(char* prog) ...@@ -159,7 +157,7 @@ syntax(char* prog)
<< "Options for Tauriainen's TAA-based algorithm (-taa):" << "Options for Tauriainen's TAA-based algorithm (-taa):"
<< std::endl << std::endl
<< " -c enable language containment checks" << std::endl << " -c enable language containment checks (implies -taa)"
<< std::endl << std::endl
<< "Formula simplification (before translation):" << "Formula simplification (before translation):"
...@@ -329,8 +327,7 @@ main(int argc, char** argv) ...@@ -329,8 +327,7 @@ main(int argc, char** argv)
else if (!strcmp(argv[formula_index], "-c")) else if (!strcmp(argv[formula_index], "-c"))
{ {
containment = true; containment = true;
if (translation != TransTAA) translation = TransTAA;
translation = TransFM;
} }
else if (!strcmp(argv[formula_index], "-d")) else if (!strcmp(argv[formula_index], "-d"))
{ {
...@@ -764,7 +761,7 @@ main(int argc, char** argv) ...@@ -764,7 +761,7 @@ main(int argc, char** argv)
post_branching, post_branching,
fair_loop_approx, fair_loop_approx,
unobservables, unobservables,
fm_red, containment); fm_red);
break; break;
case TransTAA: case TransTAA:
a = spot::ltl_to_taa(f, dict, containment); a = spot::ltl_to_taa(f, dict, containment);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment