diff --git a/ChangeLog b/ChangeLog index 7b5112f4d..89fd64daa 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,26 @@ +2010-03-06 Alexandre Duret-Lutz + + Keep acceptance conditions on transitions going to accepting SCCs + by default in scc_filter(). + + Doing so helps the degeneralization algorithm, because it will + have more opportunity to be in an accepting level when it reaches + the accepting SCCs. + + * src/tgbaalgos/sccfilter.cc (filter_iter::filter_iter): Take a + remove_all_useless argument. + (filter_iter::process_link): Use the flag to decide whether to + filter acceptance conditions going to accepting SCCs. + (scc_filter): Take a remove_all_useless argument and pass it to + filter_iter. + * src/tgbaalgos/sccfilter.hh (filter_iter): Add the new argument + and document the function. + * src/tgbatest/tgbatests/ltl2tgba.cc (main): Add option use -R3 + for remove_all_useless=false and add -R3f for + remove_all_useless=true. + * src/tgbatest/ltl2tgba.test: Show one case where -R3f makes + the degeneralization worse than -R3. + 2010-03-05 Alexandre Duret-Lutz Simplify F(a)|F(b) as F(a|b). Add similar rule for G(a)&G(b). diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index 64930aa23..8f42479fc 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -64,13 +64,14 @@ namespace spot filter_iter(const tgba* a, const scc_map& sm, const std::vector& useless, - bdd useful, bdd strip) + bdd useful, bdd strip, bool remove_all_useless) : tgba_reachable_iterator_depth_first(a), out_(new T(a->get_dict())), sm_(sm), useless_(useless), useful_(useful), - strip_(strip) + strip_(strip), + all_(remove_all_useless) { out_->set_acceptance_conditions(useful); } @@ -96,10 +97,16 @@ namespace spot create_transition(this->automata_, out_, in_s, in, out_s, out); out_->add_conditions(t, si->current_condition()); - // Do not output any acceptance condition if either the source or - // the destination state do not belong to an accepting state. - if (sm_.accepting(sm_.scc_of_state(in_s)) - && sm_.accepting(sm_.scc_of_state(out_s))) + // Regardless of all_, do not output any acceptance condition + // if the destination is not in an accepting SCC. + // + // If all_ is set, do not output any acceptance condition if the + // source is not in the same SCC as dest. + // + // (See the documentation of scc_filter() for a rational.) + unsigned u = sm_.scc_of_state(out_s); + if (sm_.accepting(u) + && (!all_ || u == sm_.scc_of_state(in_s))) out_->add_acceptance_conditions (t, (bdd_exist(si->current_acceptance_conditions(), strip_) & useful_)); @@ -111,12 +118,13 @@ namespace spot const std::vector& useless_; bdd useful_; bdd strip_; + bool all_; }; } // anonymous - tgba* scc_filter(const tgba* aut) + tgba* scc_filter(const tgba* aut, bool remove_all_useless) { scc_map sm(aut); sm.build_map(); @@ -160,7 +168,8 @@ namespace spot if (af) { filter_iter fi(af, sm, ss.useless_scc_map, - useful, strip); + useful, strip, + remove_all_useless); fi.run(); tgba_explicit_formula* res = fi.result(); res->merge_transitions(); @@ -169,7 +178,8 @@ namespace spot else { filter_iter fi(aut, sm, ss.useless_scc_map, - useful, strip); + useful, strip, + remove_all_useless); fi.run(); tgba_explicit_string* res = fi.result(); res->merge_transitions(); @@ -177,6 +187,4 @@ namespace spot } } - - } diff --git a/src/tgbaalgos/sccfilter.hh b/src/tgbaalgos/sccfilter.hh index ad4492931..47822080c 100644 --- a/src/tgbaalgos/sccfilter.hh +++ b/src/tgbaalgos/sccfilter.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -26,8 +26,28 @@ namespace spot { - // Prune unaccepting SCCs and remove superfluous acceptance conditions. - tgba* scc_filter(const tgba* aut); + /// \brief Prune unaccepting SCCs and remove superfluous acceptance + /// conditions. + /// + /// This functions will explore the SCCs of the automaton and remove + /// dead SCCs (unaccepting, and with no exit path leading to an + /// accepting SCC). + /// + /// Additionally, this will try to remove useless acceptance + /// conditions. This operation may diminish the number of + /// acceptance condition of the automaton, for instance when two + /// acceptance conditions are always used together we only keep one + /// (but it will never remove all acceptance conditions, even if it + /// would be OK to have zero). + /// + /// Acceptance conditions on transitions going to non-accepting SCC + /// are all removed. Acceptance conditions going to an accepting + /// SCC and coming from another SCC are only removed if \a + /// remove_all_useless is set. The default value of \a + /// remove_all_useless is \c false because some algorithms (like the + /// degeneralization) will work better if transition going to an + /// accepting SCC are accepting. + tgba* scc_filter(const tgba* aut, bool remove_all_useless = false); } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index d4c8b4753..295d7923b 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -195,6 +195,10 @@ syntax(char* prog) << " -R2t remove transitions using delayed simulation" << std::endl << " -R3 use SCC to reduce the automata" << std::endl + << " -R3f clean more acceptance conditions that -R3" << std::endl + << " " + << "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)" + << std::endl << " -Rd display the simulation relation" << std::endl << " -RD display the parity game (dot format)" << std::endl << std::endl @@ -280,6 +284,7 @@ main(int argc, char** argv) bool from_file = false; int reduc_aut = spot::Reduce_None; int redopt = spot::ltl::Reduce_None; + bool scc_filter_all = false; bool symbolic_scc_pruning = false; bool display_reduce_form = false; bool display_rel_sim = false; @@ -560,6 +565,11 @@ main(int argc, char** argv) { reduc_aut |= spot::Reduce_Scc; } + else if (!strcmp(argv[formula_index], "-R3f")) + { + reduc_aut |= spot::Reduce_Scc; + scc_filter_all = true; + } else if (!strcmp(argv[formula_index], "-R3b")) { symbolic_scc_pruning = true; @@ -806,7 +816,7 @@ main(int argc, char** argv) if (reduc_aut & spot::Reduce_Scc) { tm.start("reducing A_f w/ SCC"); - a = aut_scc = spot::scc_filter(a); + a = aut_scc = spot::scc_filter(a, scc_filter_all); tm.stop("reducing A_f w/ SCC"); } diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 390d5bb2b..e5d9e1197 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -75,3 +75,17 @@ for opt in '' -D -DS; do grep 'transitions: 6$' stdout grep 'states: 4$' stdout done + +# Make sure '(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))' +# has 6 states and 15 transitions, before and after degeneralization. +f='(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))' +for opt in '' -D -DS; do + ../ltl2tgba -k -f -R3 $opt "$f" > stdout + grep 'transitions: 15$' stdout + grep 'states: 6$' stdout +done + +# Note: this is worse with -R3f. +../ltl2tgba -k -f -R3f -DS "$f" > stdout +grep 'transitions: 17$' stdout +grep 'states: 7$' stdout