diff --git a/ChangeLog b/ChangeLog index 04482c08d..891c0f383 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,13 @@ 2004-02-16 Alexandre Duret-Lutz + * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add the + symb_merge argument. + * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Likewise. + * src/tgbatest/ltl2tgba.cc (main): Rename -fx as -x, and add -y + to unset symb_merge. + * wrap/python/cgi/ltl2tgba.in: Remove the exprop version + of the FM translator, make exprop and symb_merge options. + * src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor::visit) : suppress the GFy optimisation introduced on 2003-11-26, it is generalized by the identification of states with same symbolic diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index fa84cbc65..1a61985a4 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -435,7 +435,8 @@ namespace spot } tgba_explicit* - ltl_to_tgba_fm(const formula* f, bdd_dict* dict, bool exprop) + ltl_to_tgba_fm(const formula* f, bdd_dict* dict, + bool exprop, bool symb_merge) { // Normalize the formula. We want all the negations on // the atomic propositions. We also suppress logic @@ -530,7 +531,8 @@ namespace spot // use it in lieu of the current one. (See the comments // for canonical_succ.) We need to do this only for new // destinations. - if (formulae_seen.find(dest) == formulae_seen.end()) + if (symb_merge + && formulae_seen.find(dest) == formulae_seen.end()) { dest->accept(v); bdd succbdd = v.result(); diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index a72b1b6f2..dc0832102 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -49,10 +49,16 @@ namespace spot /// /// 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 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). + /// + /// If \a symb_merge is set to false, states with the same symbolic + /// representation (these are equivalent formulae) will not be + /// merged. /// \endverbatim tgba_explicit* ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict, - bool exprop = false); + bool exprop = false, bool symb_merge = true); } #endif // SPOT_TGBA_LTL2TGBA_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index e82488feb..cf58aff48 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -61,8 +61,6 @@ syntax(char* prog) << "counter-example " << std::endl << " -f use Couvreur's FM algorithm for translation" << std::endl - << " -fx use Couvreur's FM algorithm, with exploded properties" - << std::endl << " -F read the formula from the file" << std::endl << " -m magic-search (implies -D), expect a counter-example" << std::endl @@ -82,8 +80,12 @@ syntax(char* prog) << "acceptance conditions" << std::endl << " -v display the BDD variables used by the automaton" << std::endl + << " -x try to produce a more deterministic automata " + << "(implies -f)" << std::endl << " -X do not compute an automaton, read it from a file" - << std::endl; + << std::endl + << " -y do not merge states with same symbolic representation " + << "(implies -f)" << std::endl; exit(2); } @@ -96,6 +98,7 @@ main(int argc, char** argv) bool degeneralize_opt = false; bool fm_opt = false; bool fm_exprop_opt = false; + bool fm_symb_merge_opt = true; bool file_opt = false; int output = 0; int formula_index = 0; @@ -156,11 +159,6 @@ main(int argc, char** argv) { fm_opt = true; } - else if (!strcmp(argv[formula_index], "-fx")) - { - fm_opt = true; - fm_exprop_opt = true; - } else if (!strcmp(argv[formula_index], "-F")) { file_opt = true; @@ -215,10 +213,20 @@ main(int argc, char** argv) { output = 5; } + else if (!strcmp(argv[formula_index], "-x")) + { + fm_opt = true; + fm_exprop_opt = true; + } else if (!strcmp(argv[formula_index], "-X")) { from_file = true; } + else if (!strcmp(argv[formula_index], "-y")) + { + fm_opt = true; + fm_symb_merge_opt = false; + } else { break; @@ -282,7 +290,8 @@ main(int argc, char** argv) else { if (fm_opt) - to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt); + to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt, + fm_symb_merge_opt); else to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); spot::ltl::destroy(f); diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 008f71e83..4aa8d6ee6 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -56,6 +56,13 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- FM), without symb_merge" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -y -t'" + Enabled = yes +} + Algorithm { Name = "Spot (Couvreur -- FM), degeneralized" @@ -70,6 +77,13 @@ Algorithm Enabled = no } +Algorithm +{ + Name = "Spot (Couvreur -- FM), without symb_merge, fake" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -y -T'" + Enabled = no +} + Algorithm { Name = "Spot (Couvreur -- FM), fake, LTL simplifications by ltl2ba" @@ -80,28 +94,42 @@ Algorithm Algorithm { Name = "Spot (Couvreur -- FM exprop)" - Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -fx -t'" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -t'" + Enabled = yes +} + +Algorithm +{ + Name = "Spot (Couvreur -- FM exprop), without symb_merge" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -y -t'" Enabled = yes } Algorithm { Name = "Spot (Couvreur -- FM exprop), degeneralized" - Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -fx -t -D'" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -t -D'" Enabled = yes } Algorithm { Name = "Spot (Couvreur -- FM exprop), fake" - Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -fx -T'" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -T'" + Enabled = no +} + +Algorithm +{ + Name = "Spot (Couvreur -- FM exprop), without symb_merge, fake" + Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -F -f -x -y -T'" Enabled = no } Algorithm { Name = "Spot (Couvreur -- FM exprop), fake, LTL simplifications by ltl2ba" - Path = "${LBTT_TRANSLATE} --spot '${srcdir}/ltl2baw.pl --spot=\"-fx -T\" -F'" + Path = "${LBTT_TRANSLATE} --spot '${srcdir}/ltl2baw.pl --spot=\"-f -x -T\" -F'" Enabled = no } diff --git a/wrap/python/cgi/ltl2tgba.in b/wrap/python/cgi/ltl2tgba.in index 75f293ecf..12c057816 100644 --- a/wrap/python/cgi/ltl2tgba.in +++ b/wrap/python/cgi/ltl2tgba.in @@ -162,6 +162,9 @@ LTL-to-Büchi translator""" formula = form.getfirst('formula', '') options = [ + ('opt_exprop', 'optimize determinism (FM only)', 1), + ('opt_symb_merge', + 'merge states with same symbolic successor representation (FM only)', 1), ('show_parse', 'show traces during parsing', 0), ('show_formula_dot', 'print the formula as .dot', 0), ('show_formula_gif', 'draw the formula', 0), @@ -188,7 +191,6 @@ options = [ default_translator = 'trans_fm'; translators = [ ('trans_fm', 'Convreur/FM'), - ('trans_fm_exprop', 'Convreur/FM - exploded properties'), ('trans_lacim', 'Convreur/LaCIM'), ] @@ -339,12 +341,19 @@ dict = spot.bdd_dict() print '

Building automaton...', sys.stdout.flush() +if opt_exprop: + exprop = 1 +else: + exprop = 0 +if opt_symb_merge: + symb_merge = 1 +else: + symb_merge = 0 + if trans_lacim: automaton = spot.ltl_to_tgba_lacim(f, dict) elif trans_fm: - automaton = spot.ltl_to_tgba_fm(f, dict) -elif trans_fm_exprop: - automaton = spot.ltl_to_tgba_fm(f, dict, True) + automaton = spot.ltl_to_tgba_fm(f, dict, exprop, symb_merge) print 'done.

' sys.stdout.flush()