diff --git a/ChangeLog b/ChangeLog index 490d4561f..cd715ad9e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2005-05-04 Alexandre Duret-Lutz + + * src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_fm.cc: Add + the reduce_ltl argument. + * src/tgbatest/ltl2tgba.cc: Add options -fr1, -fr2, -fr3, and -fr4. + * src/tgbatest/spotlbtt.test, bench/ltl2tgba/algorithms: Test -fr4. + * bench/ltl2tgba/parseout.pl: Suppress Perl warnings on disabled + algorithms. + 2005-04-19 Alexandre Duret-Lutz * bench/ltl2tgba/README: More instructions. diff --git a/bench/ltl2tgba/algorithms b/bench/ltl2tgba/algorithms index b6727683a..6d2a9d25e 100644 --- a/bench/ltl2tgba/algorithms +++ b/bench/ltl2tgba/algorithms @@ -63,6 +63,14 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "FM, degen, +symb_merge, +exprop, +INpre, +post, +flapprox" + Path = "$LBTT_TRANSLATE" + Parameters = "--spot '$LTL2TGBA -fr4 -R1q -R1t -R3 -L -t -x -D -F'" + Enabled = yes +} + Algorithm { Name = "FM, degen, +symb_merge, +exprop, +pre, +post, +flapprox, +post_branch" @@ -71,6 +79,14 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "FM, degen, +symb_merge, +exprop, +INpre, +post, +flapprox, +post_branch" + Path = "$LBTT_TRANSLATE" + Parameters = "--spot '$LTL2TGBA -fr4 -R1q -R1t -R3 -L -t -x -D -p -F'" + Enabled = yes +} + Algorithm { Name = "FM, degen, +symb_merge, +exprop, +post_branch, LTLopt" @@ -208,6 +224,14 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "FM, gen, +symb_merge, +exprop, +INpre, +post, +flapprox" + Path = "$LBTT_TRANSLATE" + Parameters = "--spot '$LTL2TGBA -fr4 -R1q -R1t -R3 -L -t -x -F'" + Enabled = yes +} + Algorithm { Name = "FM, gen, +symb_merge, +exprop, +pre, +post, +flapprox, +post_branch" @@ -216,6 +240,13 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "FM, gen, +symb_merge, +exprop, +INpre, +post, +flapprox, +post_branch" + Path = "$LBTT_TRANSLATE" + Parameters = "--spot '$LTL2TGBA -fr4 -R1q -R1t -R3 -L -t -x -p -F'" + Enabled = yes +} Algorithm { diff --git a/bench/ltl2tgba/parseout.pl b/bench/ltl2tgba/parseout.pl index ab55c5878..d88dcb112 100755 --- a/bench/ltl2tgba/parseout.pl +++ b/bench/ltl2tgba/parseout.pl @@ -52,7 +52,7 @@ while (<>) if (/Pos\. formulae \|\s*([^|]*?)\s*\|\s*([^|]*?)\s*\|$/) { $acc = $1; - $time = $2; + $time = $2 || 0; } next unless /Pos\. formulae \|\s*(.*?)\s*\|\s*(.*?)\s*\|\s*(.*?)\s*\|/; if ($line % 2) diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 348580c4f..0d57162ff 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -637,7 +637,8 @@ namespace spot tgba_explicit* ltl_to_tgba_fm(const formula* f, bdd_dict* dict, bool exprop, bool symb_merge, bool branching_postponement, - bool fair_loop_approx, const ltl::atomic_prop_set* unobs) + bool fair_loop_approx, const atomic_prop_set* unobs, + int reduce_ltl) { possible_fair_loop_checker pflc; @@ -649,6 +650,14 @@ namespace spot formula* f2 = negative_normal_form(f1); destroy(f1); + // Simplify the formula, if requested. + if (reduce_ltl) + { + formula* tmp = reduce(f2, reduce_ltl); + destroy(f2); + f2 = tmp; + } + typedef std::set set_type; set_type formulae_seen; set_type formulae_to_translate; @@ -675,8 +684,8 @@ namespace spot if (unobs) { bdd neg_events = bddtrue; - std::auto_ptr aps(ltl::atomic_prop_collect(f)); - for (ltl::atomic_prop_set::const_iterator i = aps->begin(); + std::auto_ptr aps(atomic_prop_collect(f)); + for (atomic_prop_set::const_iterator i = aps->begin(); i != aps->end(); ++i) { int p = d.register_proposition(*i); @@ -685,7 +694,7 @@ namespace spot observable_events = (observable_events & neg) | (neg_events & pos); neg_events &= neg; } - for (ltl::atomic_prop_set::const_iterator i = unobs->begin(); + for (atomic_prop_set::const_iterator i = unobs->begin(); i != unobs->end(); ++i) { int p = d.register_proposition(*i); @@ -790,6 +799,17 @@ namespace spot bdd dest_bdd = bdd_existcomp(cube, d.next_set); const formula* dest = d.conj_bdd_to_formula(dest_bdd); + // Simplify the formula, if requested. + if (reduce_ltl) + { + formula* tmp = reduce(dest, reduce_ltl); + destroy(dest); + dest = tmp; + // Ignore the arc if the destination reduces to false. + if (dest == constant::false_instance()) + continue; + } + // If we already know a state with the same // successors, use it in lieu of the current one. if (symb_merge) diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index e28569507..fc14e38a6 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -25,6 +25,7 @@ #include "ltlast/formula.hh" #include "tgba/tgbaexplicit.hh" #include "ltlvisit/apcollect.hh" +#include "ltlvisit/reduce.hh" namespace spot { @@ -95,12 +96,36 @@ namespace spot /// are interpreted as events that exclude each other. The events in the /// formula are observable events, and \c unobs can be filled with /// additional unobservable events. + /// + /// \param reduce_ltl If this parameter is set, the LTL formulae representing + /// each state of the automaton will be simplified using spot::ltl::reduce() + /// before computing the successor. \a reduce_ltl should specify the type + /// of reduction to apply as documented for spot::ltl::reduce(). + /// This idea is taken from the following paper. + /// \verbatim + /// @InProceedings{ thirioux.02.fmics, + /// author = {Xavier Thirioux}, + /// title = {Simple and Efficient Translation from {LTL} Formulas to + /// {B\"u}chi Automata}, + /// booktitle = {Proceedings of the 7th International ERCIM Workshop in + /// Formal Methods for Industrial Critical Systems (FMICS'02)}, + /// series = {Electronic Notes in Theoretical Computer Science}, + /// volume = {66(2)}, + /// publisher = {Elsevier}, + /// editor = {Rance Cleaveland and Hubert Garavel}, + /// year = {2002}, + /// month = jul, + /// address = {M{\'a}laga, Spain} + /// } + /// \endverbatim + /// /// \return A spot::tgba_explicit that recognizes the language of \a f. 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 fair_loop_approx = false, - const ltl::atomic_prop_set* unobs = 0); + const ltl::atomic_prop_set* unobs = 0, + int reduce_ltl = ltl::Reduce_None); } #endif // SPOT_TGBAALGOS_LTL2TGBA_FM_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 5f8033ec3..311511bac 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -74,6 +74,10 @@ syntax(char* prog) << std::endl << " -f use Couvreur's FM algorithm for translation" << 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 + << " -fr3 use -r3 (see below) at each step of FM" << std::endl + << " -fr4 use -r4 (see below) at each step of FM" << std::endl << " -F read the formula from the file" << std::endl << " -g graph the accepting run on the automaton (requires -e)" << std::endl @@ -144,6 +148,7 @@ main(int argc, char** argv) bool paper_opt = false; enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen; bool fm_opt = false; + int fm_red = spot::ltl::Reduce_None; bool fm_exprop_opt = false; bool fm_symb_merge_opt = true; bool file_opt = false; @@ -246,6 +251,26 @@ main(int argc, char** argv) { fm_opt = true; } + else if (!strcmp(argv[formula_index], "-fr1")) + { + fm_opt = true; + fm_red |= spot::ltl::Reduce_Basics; + } + else if (!strcmp(argv[formula_index], "-fr2")) + { + fm_opt = true; + fm_red |= spot::ltl::Reduce_Eventuality_And_Universality; + } + else if (!strcmp(argv[formula_index], "-fr3")) + { + fm_opt = true; + fm_red |= spot::ltl::Reduce_Syntactic_Implications; + } + else if (!strcmp(argv[formula_index], "-fr4")) + { + fm_opt = true; + fm_red |= spot::ltl::Reduce_All; + } else if (!strcmp(argv[formula_index], "-F")) { file_opt = true; @@ -472,7 +497,8 @@ main(int argc, char** argv) to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt, fm_symb_merge_opt, post_branching, - fair_loop_approx, unobservables); + fair_loop_approx, unobservables, + fm_red); 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 f087a71c9..4c8b2f180 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# 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. # @@ -100,6 +100,14 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- FM), reduction of formula in FM" + Path = "${LBTT_TRANSLATE}" + Parameters = "--spot './ltl2tgba -fr4 -F -f -t'" + Enabled = yes +} + Algorithm { Name = "Spot (Couvreur -- FM), post reduction with direct simulation" @@ -156,38 +164,6 @@ Algorithm Enabled = yes } -Algorithm -{ - Name = "Spot (Couvreur -- FM), fake" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot './ltl2tgba -F -f -T'" - Enabled = no -} - -Algorithm -{ - Name = "Spot (Couvreur -- FM), reduction of formula, fake" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot './ltl2tgba -r4 -F -f -T'" - Enabled = no -} - -Algorithm -{ - Name = "Spot (Couvreur -- FM), without symb_merge, fake" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot './ltl2tgba -F -f -y -T'" - Enabled = no -} - -Algorithm -{ - Name = "Spot (Couvreur -- FM), fake, LTL simplifications by ltl2ba" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '${srcdir}/ltl2baw.pl --spot=\"-f -T\" -F'" - Enabled = no -} - Algorithm { Name = "Spot (Couvreur -- FM exprop)" @@ -244,167 +220,6 @@ Algorithm Enabled = yes } -Algorithm -{ - Name = "Spot (Couvreur -- FM exprop + post_branch), fake" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot './ltl2tgba -F -f -x -p -T'" - Enabled = no -} - -Algorithm -{ - Name = "Spot (Couvreur -- FM exprop + flapprox), fake" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot './ltl2tgba -F -f -x -L -T'" - Enabled = no -} - -Algorithm -{ - Name = "Spot (Couvreur -- FM exprop + post_branch + flapprox), fake" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot './ltl2tgba -F -f -x -p -L -T'" - Enabled = no -} - -Algorithm -{ - Name = "Spot (Couvreur -- FM exprop), fake" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot './ltl2tgba -F -f -x -T'" - Enabled = no -} - -Algorithm -{ - Name = "Spot (Couvreur -- FM exprop), without symb_merge, fake" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot './ltl2tgba -F -f -x -y -T'" - Enabled = no -} - -Algorithm -{ - Name = "Spot (Couvreur -- FM exprop), fake, LTL simplifications by ltl2ba" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '${srcdir}/ltl2baw.pl --spot=\"-f -x -T\" -F'" - Enabled = no -} - -Algorithm -{ - Name = "Spin" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spin spin" - Enabled = no -} - -Algorithm -{ - Name = "LBT" - Path = "${LBTT_TRANSLATE}" - Parameters = "--lbt lbt" - Enabled = no -} - -Algorithm -{ - Name = "LTL2BA" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spin ltl2ba" - Enabled = no -} - -Algorithm -{ - Name = "LTL2BA, generalized fake" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '${srcdir}/ltl2baw.pl -F'" - Enabled = no -} - -Algorithm -{ - Name = "LTL2BA without LTL and SCC simplifications" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spin 'ltl2ba -l -c'" - Enabled = no -} - -Algorithm -{ - Name = "LTL2BA without LTL and SCC simplifications, generalized fake" - Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '${srcdir}/ltl2baw.pl -l -c -F'" - Enabled = no -} - -Algorithm -{ - Name = "Wring (GPVW)" - Path = "sh" - Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt --0'" - Enabled = no -} - -Algorithm -{ - Name = "Wring (GPVW+)" - Path = "sh" - Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt --1'" - Enabled = no -} - -Algorithm -{ - Name = "Wring (LTL2AUT)" - Path = "sh" - Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt --2'" - Enabled = no -} - -Algorithm -{ - Name = "Wring (Wring RewRule)" - Path = "sh" - Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt --3'" - Enabled = no -} - -Algorithm -{ - Name = "Wring (Wring RewRule+BoolOpt)" - Path = "sh" - Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt --4'" - Enabled = no -} - -Algorithm -{ - Name = "Wring (Wring RewRule+BoolOpt+AutSempl)" - Path = "sh" - Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt --5'" - Enabled = no -} - -Algorithm -{ - Name = "Wring (Wring BoolOpt)" - Path = "sh" - Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt --6'" - Enabled = no -} - -Algorithm -{ - Name = "Wring (Wring RewRule+BoolOpt), degeneralized" - Path = "sh" - Parameters = "-c 'cd ~/src/wring2lbtt && ./wring2lbtt -d --4'" - Enabled = no -} - - GlobalOptions { Rounds = 100