diff --git a/ChangeLog b/ChangeLog index a710d6d6d..40b10f0fc 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2004-05-07 Alexandre Duret-Lutz + + * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument + branching_postponement. + * src/tgbaalgos/ltl2tgba_fm.cc (fill_dests): New function, extracted + from ltl_to_tgba_fm(). + (ltl_to_tgba_fm): Implement the branching_postponement optimization. + * src/tgbatest/ltl2tgba.cc: Add the -p option. + * src/tgbatest/spotlbtt.test: Exercise branching postponement. + * wrap/python/cgi/ltl2tgba.in: Make it an option. + 2004-05-04 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba_fm.cc: Add a superfluous return to pacify diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index b5f1202d7..d6e224a46 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -396,9 +396,57 @@ namespace spot } + typedef std::map prom_map; + typedef Sgi::hash_map > dest_map; + typedef std::map succ_to_formula; + + static void + fill_dests(translate_dict& d, bool symb_merge, + std::set& formulae_seen, + succ_to_formula& canonical_succ, ltl_trad_visitor& v, + dest_map& dests, bdd label, formula* dest) + { + // If we already know a state with the same successors, + // use it in lieu of the current one. (See the comments + // for canonical_succ.) We need to do this only for new + // destinations. + if (symb_merge + && formulae_seen.find(dest) == formulae_seen.end()) + { + dest->accept(v); + bdd succbdd = v.result(); + succ_to_formula::iterator cs = + canonical_succ.find(succbdd); + if (cs != canonical_succ.end()) + { + destroy(dest); + dest = clone(cs->second); + } + else + { + canonical_succ[succbdd] = clone(dest); + } + } + + bdd promises = bdd_existcomp(label, d.a_set); + bdd conds = bdd_existcomp(label, d.var_set); + + dest_map::iterator i = dests.find(dest); + if (i == dests.end()) + { + dests[dest][promises] = conds; + } + else + { + i->second[promises] |= conds; + destroy(dest); + } + } + + tgba_explicit* ltl_to_tgba_fm(const formula* f, bdd_dict* dict, - bool exprop, bool symb_merge) + bool exprop, bool symb_merge, bool branching_postponement) { // Normalize the formula. We want all the negations on // the atomic propositions. We also suppress logic @@ -414,7 +462,6 @@ namespace spot // We do this because many formulae (such as `aR(bRc)' and // `aR(bRc).(bRc)') are equivalent, and are trivially identified // by looking at the set of successors. - typedef std::map succ_to_formula; succ_to_formula canonical_succ; translate_dict d(dict); @@ -435,8 +482,8 @@ namespace spot // Translate it into a BDD to simplify it. // FIXME: Currently the same formula can be converted into a - // BDD twice. Once in the symb_merge block below, and then - // once here. + // BDD twice. Once in the symb_merge block in fill_dests, + // and then once here. f->accept(v); bdd res = v.result(); succ_to_formula::iterator cs = canonical_succ.find(res); @@ -474,10 +521,6 @@ namespace spot // // In `exprop' mode, considering all possible combinations of // outgoing propositions generalizes the above trick. - - typedef std::map prom_map; - typedef Sgi::hash_map > - dest_map; dest_map dests; // Compute all outgoing arcs. @@ -497,50 +540,43 @@ namespace spot bdd one_prop_set = exprop ? bdd_satoneset(all_props, var_set, bddtrue) : bddtrue; all_props -= one_prop_set; + + typedef std::map succ_map; + succ_map succs; + minato_isop isop(res & one_prop_set); bdd cube; while ((cube = isop.next()) != bddfalse) { - const formula* dest = + bdd label = bdd_exist(cube, d.next_set); + formula* dest = d.conj_bdd_to_formula(bdd_existcomp(cube, d.next_set)); - // If we already know a state with the same successors, - // use it in lieu of the current one. (See the comments - // for canonical_succ.) We need to do this only for new - // destinations. - if (symb_merge - && formulae_seen.find(dest) == formulae_seen.end()) + // If we are not postponing the branching, we can + // declare the outgoing transitions immediately. + // Otherwise, we merge transitions with identical + // label, and declare the outgoing transitions in a + // second loop. + if (!branching_postponement) { - dest->accept(v); - bdd succbdd = v.result(); - succ_to_formula::iterator cs = - canonical_succ.find(succbdd); - if (cs != canonical_succ.end()) - { - destroy(dest); - dest = clone(cs->second); - } - else - { - canonical_succ[succbdd] = clone(dest); - } - } - - bdd promises = bdd_existcomp(cube, d.a_set); - bdd conds = - exprop ? one_prop_set : bdd_existcomp(cube, var_set); - - dest_map::iterator i = dests.find(dest); - if (i == dests.end()) - { - dests[dest][promises] = conds; + fill_dests(d, symb_merge, formulae_seen, canonical_succ, + v, dests, label, dest); } else { - i->second[promises] |= conds; - destroy(dest); + succ_map::iterator si = succs.find(label); + if (si == succs.end()) + succs[label] = dest; + else + si->second = multop::instance(multop::Or, + si->second, dest); } } + 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); } // Check for an arc going to 1 (True). Register it first, that diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index dc0832102..9ea269ad2 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -46,19 +46,43 @@ namespace spot /// month = {September}, /// isbn = {3-540-66587-0} /// } + /// \endverbatim /// /// If \a exprop is set, the algorithm will consider all properties /// combinations possible on each state, in an attempt to reduce /// the non-determinism. The automaton will have the same size as /// without this option, but because the transition will be more - /// deterministic product automaton will be smaller (or, at worse, equal). + /// deterministic, the product automaton will be smaller (or, at worse, + /// equal). /// /// If \a symb_merge is set to false, states with the same symbolic /// representation (these are equivalent formulae) will not be /// merged. + /// + /// If \a branching_postponement is set, several transitions leaving + /// from the same state with the same label (i.e., condition + acceptance + /// conditions) will be merged. This correspond to an optimization + /// described in the following paper. + /// \verbatim + /// @InProceedings{ sebastiani.03.charme, + /// author = {Roberto Sebastiani and Stefano Tonetta}, + /// title = {"More Deterministic" vs. "Smaller" B{\"u}chi Automata for + /// Efficient LTL Model Checking}, + /// booktitle = {Proceedings for the 12th Advanced Research Working + /// Conference on Correct Hardware Design and Verification + /// Methods (CHARME'03)}, + /// pages = {126--140}, + /// year = {2003}, + /// editor = {G. Goos and J. Hartmanis and J. van Leeuwen}, + /// volume = {2860}, + /// series = {Lectures Notes in Computer Science}, + /// month = {October}, + /// publisher = {Springer-Verlag} + /// } /// \endverbatim tgba_explicit* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict, - bool exprop = false, bool symb_merge = true); + bool exprop = false, bool symb_merge = true, + bool branching_postponement = false); } #endif // SPOT_TGBA_LTL2TGBA_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index db6a663ad..c80dc80b9 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -72,6 +72,7 @@ syntax(char* prog) << std::endl << " -N display the never clain for Spin " << "(implies -D)" << std::endl + << " -p branching postponement (implies -f)" << std::endl << " -r display the relation BDD, not the reachability graph" << std::endl << " -R same as -r, but as a set" << std::endl @@ -111,6 +112,7 @@ main(int argc, char** argv) bool magic_many = false; bool expect_counter_example = false; bool from_file = false; + bool post_branching = false; for (;;) { @@ -194,6 +196,11 @@ main(int argc, char** argv) degeneralize_opt = true; output = 8; } + else if (!strcmp(argv[formula_index], "-p")) + { + post_branching = true; + fm_opt = true; + } else if (!strcmp(argv[formula_index], "-r")) { output = 1; @@ -300,7 +307,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); + fm_symb_merge_opt, + post_branching); 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 afa30a16f..0f965453c 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -119,6 +119,27 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- FM post_branch + exprop)" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -p -t'" + Enabled = yes +} + +Algorithm +{ + Name = "Spot (Couvreur -- FM post_branch + exprop), degeneralized" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -p -x -t -D'" + Enabled = yes +} + +Algorithm +{ + Name = "Spot (Couvreur -- FM exprop + post_branch), fake" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -p -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 47f1658d8..36098c94d 100644 --- a/wrap/python/cgi/ltl2tgba.in +++ b/wrap/python/cgi/ltl2tgba.in @@ -211,6 +211,7 @@ options_trans_fm = [ ('opt_exprop', 'optimize determinism', 1), ('opt_symb_merge', 'merge states with same symbolic successor representation', 1), + ('opt_branch_post', 'branching postponement', 0), ] options_trans_lacim = [ ('show_relation_set', @@ -407,11 +408,16 @@ if opt_symb_merge: symb_merge = 1 else: symb_merge = 0 +if opt_branch_post: + branching_postponement = 1 +else: + branching_postponement = 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) + automaton = spot.ltl_to_tgba_fm(f, dict, + exprop, symb_merge, branching_postponement) print 'done.

' sys.stdout.flush()