diff --git a/ChangeLog b/ChangeLog index 40b10f0fc..bef63a605 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2004-05-10 Alexandre Duret-Lutz + + * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument + fair_loop_approx. + * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Implement the + fair_loop_approx optimization. + (ltl_promise_visitor, ltl_possible_fair_loop_visitor, + possible_fair_loop_checker): New classes. + * src/tgbatest/ltl2tgba.cc: Add the -L option. + * src/tgbatest/spotlbtt.test: Exercise fair_loop_approx. + * wrap/python/cgi/ltl2tgba.in: Make it an option. + 2004-05-07 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index d6e224a46..e67aa5ddd 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -29,6 +29,7 @@ #include "ltlvisit/nenoform.hh" #include "ltlvisit/destroy.hh" #include "ltlvisit/tostring.hh" +#include "ltlvisit/postfix.hh" #include #include "tgba/tgbabddconcretefactory.hh" @@ -213,7 +214,7 @@ namespace spot { formula* ac = var_to_formula(var); - if (! a->has_acceptance_condition(ac)) + if (!a->has_acceptance_condition(ac)) a->declare_acceptance_condition(clone(ac)); a->add_acceptance_condition(t, ac); b = high; @@ -224,6 +225,50 @@ namespace spot }; + + // Gather all promises of a formula. These are the + // right-hand sides of U or F operators. + class ltl_promise_visitor: public postfix_visitor + { + public: + ltl_promise_visitor(translate_dict& dict) + : dict_(dict), res_(bddtrue) + { + } + + virtual + ~ltl_promise_visitor() + { + } + + bdd + result() const + { + return res_; + } + + using postfix_visitor::doit; + + virtual void + doit(unop* node) + { + if (node->op() == unop::F) + res_ &= bdd_ithvar(dict_.register_a_variable(node->child())); + } + + virtual void + doit(binop* node) + { + if (node->op() == binop::U) + res_ &= bdd_ithvar(dict_.register_a_variable(node->second())); + } + + private: + translate_dict& dict_; + bdd res_; + }; + + // The rewrite rules used here are adapted from Jean-Michel // Couvreur's FM paper. class ltl_trad_visitor: public const_visitor @@ -239,7 +284,8 @@ namespace spot { } - bdd result() const + bdd + result() const { return res_; } @@ -394,6 +440,105 @@ namespace spot bdd res_; }; + + // Check whether a formula has a R or G operator at its top-level + // (preceding logical operators do not count). + class ltl_possible_fair_loop_visitor: public const_visitor + { + public: + ltl_possible_fair_loop_visitor() + : res_(false) + { + } + + virtual + ~ltl_possible_fair_loop_visitor() + { + } + + bool + result() const + { + return res_; + } + + void + visit(const atomic_prop*) + { + } + + void + visit(const constant*) + { + } + + void + visit(const unop* node) + { + if (node->op() == unop::G) + res_ = true; + } + + void + visit(const binop* node) + { + switch (node->op()) + { + // r(f1 logical-op f2) = r(f1) logical-op r(f2) + case binop::Xor: + case binop::Implies: + case binop::Equiv: + node->first()->accept(*this); + if (!res_) + node->second()->accept(*this); + return; + case binop::U: + return; + case binop::R: + res_ = true; + return; + } + /* Unreachable code. */ + assert(0); + } + + void + visit(const multop* node) + { + unsigned s = node->size(); + for (unsigned n = 0; n < s && !res_; ++n) + { + node->nth(n)->accept(*this); + } + } + + private: + bool res_; + }; + + // Check whether a formula can be part of a fair loop. + // Cache the result for efficiency. + class possible_fair_loop_checker + { + public: + bool + check(const formula* f) + { + pfl_map::const_iterator i = pfl.find(f); + if (i != pfl.end()) + return i->second; + ltl_possible_fair_loop_visitor v; + f->accept(v); + bool rel = v.result(); + pfl[f] = rel; + return rel; + } + + private: + typedef Sgi::hash_map > pfl_map; + pfl_map pfl; + }; + } typedef std::map prom_map; @@ -428,8 +573,16 @@ namespace spot } } - bdd promises = bdd_existcomp(label, d.a_set); bdd conds = bdd_existcomp(label, d.var_set); + bdd promises = bdd_existcomp(label, d.a_set); + + // Clear the promises if the destination is the True state. + // (Normally this is already the case unless the fair_loop_approx + // optimization is used, because this can get confused by formulae + // like X(1): it doesn't know that X(1) is equivalent to 1, so it + // puts all promises on arcs going to X(1).) + if (dest == constant::true_instance()) + promises = bddtrue; dest_map::iterator i = dests.find(dest); if (i == dests.end()) @@ -446,8 +599,11 @@ namespace spot tgba_explicit* 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) { + possible_fair_loop_checker pflc; + // Normalize the formula. We want all the negations on // the atomic propositions. We also suppress logic // abbreviations such as <=>, =>, or XOR, since they @@ -463,10 +619,22 @@ namespace spot // `aR(bRc).(bRc)') are equivalent, and are trivially identified // by looking at the set of successors. succ_to_formula canonical_succ; + // For cosmetics, register 1 initially, so the algorithm will not + // register an equivalent formula first. + canonical_succ[bddtrue] = constant::true_instance(); translate_dict d(dict); ltl_trad_visitor v(d); + // Compute the set of all promises occurring inside the formula. + bdd all_promises = bddtrue; + if (fair_loop_approx) + { + ltl_promise_visitor pv(d); + f2->accept(pv); + all_promises = pv.result(); + } + formulae_seen.insert(f2); formulae_to_translate.insert(f2); @@ -549,8 +717,14 @@ namespace spot while ((cube = isop.next()) != bddfalse) { bdd label = bdd_exist(cube, d.next_set); - formula* dest = - d.conj_bdd_to_formula(bdd_existcomp(cube, d.next_set)); + bdd dest_bdd = bdd_existcomp(cube, d.next_set); + formula* dest = d.conj_bdd_to_formula(dest_bdd); + + // If the destination cannot possibly be part of a fair + // loop, make all possible promises. + if (fair_loop_approx + && dest_bdd != bddtrue && !pflc.check(dest)) + label &= all_promises; // If we are not postponing the branching, we can // declare the outgoing transitions immediately. @@ -575,8 +749,8 @@ namespace spot if (branching_postponement) for (succ_map::const_iterator si = succs.begin(); si != succs.end(); ++si) - fill_dests (d, symb_merge, formulae_seen, canonical_succ, v, - dests, si->first, si->second); + fill_dests(d, symb_merge, formulae_seen, canonical_succ, v, + dests, si->first, si->second); } // Check for an arc going to 1 (True). Register it first, that @@ -602,11 +776,11 @@ namespace spot bdd cond_for_true = bddfalse; if (i != dests.end()) { - // Transitions going to 1 (true) are not expected to make - // any promises. + // There should be only one transition going to 1 (true) ... assert(i->second.size() == 1); - prom_map::const_iterator j = i->second.find(bddtrue); - assert(j != i->second.end()); + prom_map::const_iterator j = i->second.begin(); + // ... and it is not expected to make any promises. + assert(j->first == bddtrue); cond_for_true = j->second; tgba_explicit::transition* t = diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index 9ea269ad2..9c24d2d6e 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -80,9 +80,14 @@ namespace spot /// publisher = {Springer-Verlag} /// } /// \endverbatim + /// + /// If \a fair_loop_approx is set, a really simple characterization of + /// unstable state is used to suppress all acceptance conditions from + /// incoming transitions. tgba_explicit* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict, bool exprop = false, bool symb_merge = true, - bool branching_postponement = false); + bool branching_postponement = false, + bool fair_loop_approx = false); } #endif // SPOT_TGBA_LTL2TGBA_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index c80dc80b9..d2020eec1 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -64,6 +64,7 @@ syntax(char* prog) << " -f use Couvreur's FM algorithm for translation" << std::endl << " -F read the formula from the file" << std::endl + << " -L fair-loop approximation (implies -f)" << std::endl << " -m magic-search (implies -D), expect a counter-example" << std::endl << " -M magic-search (implies -D), expect no counter-example" @@ -113,6 +114,7 @@ main(int argc, char** argv) bool expect_counter_example = false; bool from_file = false; bool post_branching = false; + bool fair_loop_approx = false; for (;;) { @@ -169,6 +171,11 @@ main(int argc, char** argv) { file_opt = true; } + else if (!strcmp(argv[formula_index], "-L")) + { + fair_loop_approx = true; + fm_opt = true; + } else if (!strcmp(argv[formula_index], "-m")) { echeck = MagicSearch; @@ -308,7 +315,8 @@ main(int argc, char** argv) if (fm_opt) to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt, fm_symb_merge_opt, - post_branching); + post_branching, + fair_loop_approx); 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 0f965453c..81cd3751c 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -126,6 +126,13 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- FM post_branch + exprop + flapprox)" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -p -L -t'" + Enabled = yes +} + Algorithm { Name = "Spot (Couvreur -- FM post_branch + exprop), degeneralized" @@ -133,6 +140,13 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- FM post_branch + exprop + flapprox), degeneralized" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -p -x -t -L -D'" + Enabled = yes +} + Algorithm { Name = "Spot (Couvreur -- FM exprop + post_branch), fake" @@ -140,6 +154,20 @@ Algorithm Enabled = no } +Algorithm +{ + Name = "Spot (Couvreur -- FM exprop + flapprox), fake" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -L -T'" + Enabled = no +} + +Algorithm +{ + Name = "Spot (Couvreur -- FM exprop + post_branch + flapprox), fake" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -p -L -T'" + Enabled = no +} + Algorithm { Name = "Spot (Couvreur -- FM exprop), fake" diff --git a/wrap/python/cgi/ltl2tgba.in b/wrap/python/cgi/ltl2tgba.in index 36098c94d..347957f63 100644 --- a/wrap/python/cgi/ltl2tgba.in +++ b/wrap/python/cgi/ltl2tgba.in @@ -212,6 +212,7 @@ options_trans_fm = [ ('opt_symb_merge', 'merge states with same symbolic successor representation', 1), ('opt_branch_post', 'branching postponement', 0), + ('opt_fair_loop_approx','fair-loop approximations', 0), ] options_trans_lacim = [ ('show_relation_set', @@ -412,12 +413,17 @@ if opt_branch_post: branching_postponement = 1 else: branching_postponement = 0 +if opt_fair_loop_approx: + fair_loop_approx = 1 +else: + fair_loop_approx = 0 if trans_lacim: automaton = spot.ltl_to_tgba_lacim(f, dict) elif trans_fm: automaton = spot.ltl_to_tgba_fm(f, dict, - exprop, symb_merge, branching_postponement) + exprop, symb_merge, branching_postponement, + fair_loop_approx) print 'done.

' sys.stdout.flush()