From 85c5c870db423a5be824d171f66fbb1e9590148a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 13 Jul 2006 18:42:55 +0000 Subject: [PATCH] * src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Add a new option "containment_checks" to enable some language containment checks (via emptiness checks) during the translation. This first attempt currently only use containment checks to merge states bisimulating each other. * src/tgbatest/ltl2tgba.cc: Bind this to option "-c". * src/tgbatest/spotlbtt.test: Check it. --- ChangeLog | 8 ++ src/tgbaalgos/ltl2tgba_fm.cc | 157 ++++++++++++++++++++++++++++++++--- src/tgbaalgos/ltl2tgba_fm.hh | 9 +- src/tgbatest/ltl2tgba.cc | 10 ++- src/tgbatest/spotlbtt.test | 19 ++++- 5 files changed, 186 insertions(+), 17 deletions(-) diff --git a/ChangeLog b/ChangeLog index 9c5a012a4..aad2cf114 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,13 @@ 2006-07-13 Alexandre Duret-Lutz + * src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_fm.cc + (ltl_to_tgba_fm): Add a new option "containment_checks" to enable + some language containment checks (via emptiness checks) during the + translation. This first attempt currently only use containment + checks to merge states bisimulating each other. + * src/tgbatest/ltl2tgba.cc: Bind this to option "-c". + * src/tgbatest/spotlbtt.test: Check it. + * src/tgba/bdddict.cc (bdd_dict::unregister_variable): Correctly call release_n(), not remove() to repopulated the freelist of anonymous BDD variables. New code I'm working on triggered an diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index f70adcf91..80e884f3c 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// 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. // // This file is part of Spot, a model checking library. // @@ -33,8 +33,9 @@ #include "ltlvisit/apcollect.hh" #include #include -#include "tgba/tgbabddconcretefactory.hh" #include "ltl2tgba_fm.hh" +#include "tgba/tgbaproduct.hh" +#include "tgbaalgos/gtec/gtec.hh" namespace spot { @@ -537,14 +538,118 @@ namespace spot pfl_map pfl_; }; + // Keep a map of the TGBA translation of all subformulae and their + // negations, for easy language containment check. + class language_containment_checker + { + struct record_ + { + const tgba* translation; + typedef std::set incomp_map; + incomp_map incompatible; + }; + typedef Sgi::hash_map trans_map; + public: + language_containment_checker(bdd_dict* dict, bool exprop, + bool symb_merge, + bool branching_postponement, + bool fair_loop_approx) + : dict_(dict), exprop_(exprop), symb_merge_(symb_merge), + branching_postponement_(branching_postponement), + fair_loop_approx_(fair_loop_approx) + { + } + + ~language_containment_checker() + { + + while (!translated_.empty()) + { + trans_map::iterator i = translated_.begin(); + delete i->second.translation; + const formula* f = i->first; + translated_.erase(i); + destroy(f); + } + } + + // Check whether L(l) is a subset of L(g). + bool + contained(const formula* l, const formula* g) + { + const record_* rl = register_formula_(l); + const formula* ng = unop::instance(unop::Not, clone(g)); + const record_* rng = register_formula_(ng); + destroy(ng); + bool res = rl->incompatible.find(rng) != rl->incompatible.end(); + return res; + } + + // Check whether L(l) = L(g). + bool + equal(const formula* l, const formula* g) + { + return contained(l,g) && contained(g,l); + } + + protected: + const record_* + register_formula_(const formula* f) + { + trans_map::iterator i = translated_.find(f); + if (i != translated_.end()) + return &i->second; + + const tgba_explicit* e = ltl_to_tgba_fm(f, dict_, exprop_, symb_merge_, + branching_postponement_, + fair_loop_approx_); + record_& r = translated_[clone(f)]; + r.translation = e; + + // Check the emptiness of the product of this formula with any + // other registered formula. + for (i = translated_.begin(); i != translated_.end(); ++i) + { + if (f == i->first) + continue; + const tgba* p = new tgba_product(e, i->second.translation); + emptiness_check* ec = couvreur99(p); + emptiness_check_result* ecr = ec->check(); + if (!ecr) + { + r.incompatible.insert(&i->second); + i->second.incompatible.insert(&r); + } + else + delete ecr; + delete ec; + delete p; + } + return &r; + } + + private: + /* Translation options */ + bdd_dict* dict_; + bool exprop_; + bool symb_merge_; + bool branching_postponement_; + bool fair_loop_approx_; + /* Translation Maps */ + trans_map translated_; + }; + class formula_canonizer { public: 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), 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 // not register an equivalent formula first. @@ -563,13 +668,16 @@ namespace spot } bdd - translate(const formula* f) + translate(const formula* f, bool* new_flag = 0) { // Use the cached result if available. formula_to_bdd_map::const_iterator i = f2b_.find(f); if (i != f2b_.end()) return i->second; + if (new_flag) + *new_flag = true; + // Perform the actual translation. f->accept(v_); bdd res = v_.result(); @@ -596,17 +704,36 @@ namespace spot const formula* canonize(const formula* f) { - bdd b = translate(f); + bool new_variable = false; + bdd b = translate(f, &new_variable); bdd_to_formula_map::iterator i = b2f_.find(b); - // Since we have just translated the formula, it is necessary in b2f_. + // Since we have just translated the formula, it is + // necessarily in b2f_. assert(i != b2f_.end()); if (i->second != f) { + // The translated bdd maps to an already seen formula. destroy(f); f = clone(i->second); } + 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; + destroy(f); + f = clone(i->second); + break; + } + } return f; } @@ -627,6 +754,7 @@ namespace spot possible_fair_loop_checker pflc_; bool fair_loop_approx_; bdd all_promises_; + language_containment_checker* lcc_; }; } @@ -657,8 +785,10 @@ 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) + int reduce_ltl, bool containment_checks) { + 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 @@ -691,7 +821,12 @@ namespace spot all_promises = pv.result(); } - formula_canonizer fc(d, fair_loop_approx, all_promises); + 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); // 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 fc14e38a6..0b7725115 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -1,6 +1,6 @@ -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// 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. // // This file is part of Spot, a model checking library. // @@ -125,7 +125,8 @@ namespace spot bool branching_postponement = false, bool fair_loop_approx = false, 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 diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 1369e3620..cacd6a2bc 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -65,6 +65,8 @@ syntax(char* prog) << " -A same as -a, but as a set" << std::endl << " -b display the automaton in the format of spot" << std::endl + << " -c enable language containment checks (implies -f)" + << std::endl << " -d turn on traces during parsing" << std::endl << " -D degeneralize the automaton as a TBA" << std::endl << " -DS degeneralize the automaton as an SBA" << std::endl @@ -169,6 +171,7 @@ main(int argc, char** argv) bool graph_run_opt = false; bool graph_run_tgba_opt = false; bool opt_reduce = false; + bool containment = false; spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* unobservables = 0; spot::tgba_explicit* system = 0; @@ -199,6 +202,11 @@ main(int argc, char** argv) { output = 7; } + else if (!strcmp(argv[formula_index], "-c")) + { + containment = true; + fm_opt = true; + } else if (!strcmp(argv[formula_index], "-d")) { debug_opt = true; @@ -499,7 +507,7 @@ main(int argc, char** argv) fm_symb_merge_opt, post_branching, fair_loop_approx, unobservables, - fm_red); + fm_red, containment); else to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); } diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 4c8b2f180..8a168758c 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +# 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. # @@ -68,6 +68,14 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- FM) containments" + Path = "${LBTT_TRANSLATE}" + Parameters = "--spot './ltl2tgba -F -f -c -t'" + Enabled = yes +} + Algorithm { Name = "Spot (Couvreur -- FM), basic reduction of formula" @@ -100,6 +108,15 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- FM) containments + reduction of formula (pre reduction)" + Path = "${LBTT_TRANSLATE}" + Parameters = "--spot './ltl2tgba -r4 -F -f -c -t'" + Enabled = yes +} + + Algorithm { Name = "Spot (Couvreur -- FM), reduction of formula in FM"