diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index 0df1a8b8a..2391798c3 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -20,13 +21,15 @@ #include "tgba/tgbaexplicit.hh" #include "reachiter.hh" #include "tgbaalgos/scc.hh" -#include "misc/bddop.hh" -#include namespace spot { namespace { + // BDD.id -> Acc number + typedef std::map accremap_t; + typedef std::vector remap_table_t; + static state_explicit_number::transition* create_transition(const tgba*, tgba_explicit_number* out_aut, @@ -67,20 +70,90 @@ namespace spot { public: typedef T output_t; + typedef std::map map_t; + typedef std::vector remap_t; filter_iter(const tgba* a, const scc_map& sm, const std::vector& useless, - bdd useful, bdd strip, bool remove_all_useless) + remap_table_t& remap_table, + unsigned max_num, + const std::vector& max_table, + bool remove_all_useless) : tgba_reachable_iterator_depth_first(a), out_(new T(a->get_dict())), sm_(sm), useless_(useless), - useful_(useful), - strip_(strip), - all_(remove_all_useless) + max_num_(max_num), + all_(remove_all_useless), + acc_(max_num) { - out_->set_acceptance_conditions(useful); + acc_[0] = bddfalse; + bdd tmp = a->all_acceptance_conditions(); + bdd_dict* d = a->get_dict(); + assert(a->number_of_acceptance_conditions() >= max_num_ - 1); + if (tmp != bddfalse) + { + for (unsigned n = max_num_ - 1; n > 0; --n) + { + assert(tmp != bddfalse); + const ltl::formula* a = d->oneacc_to_formula(bdd_var(tmp)); + out_->declare_acceptance_condition(a->clone()); + tmp = bdd_low(tmp); + } + tmp = a->all_acceptance_conditions(); + for (unsigned n = max_num_ - 1; n > 0; --n) + { + const ltl::formula* a = d->oneacc_to_formula(bdd_var(tmp)); + acc_[n] = out_->get_acceptance_condition(a->clone()); + tmp = bdd_low(tmp); + } + } + else + { + assert(max_num_ == 1); + } + + unsigned c = sm.scc_count(); + remap_.resize(c); + bdd all_orig_neg = aut_->neg_acceptance_conditions(); + bdd all_sup = bdd_support(all_orig_neg); + + for (unsigned n = 0; n < c; ++n) + { + if (!sm.accepting(n)) + continue; + + bdd missingacc = bddfalse; + for (unsigned a = max_table[n]; a < max_num_; ++a) + missingacc |= acc_[a]; + + bdd all = sm.useful_acc_of(n); + while (all != bddfalse) + { + bdd one = bdd_satoneset(all, all_sup, bddtrue); + all -= one; + bdd res = bddfalse; + bdd resacc = bddfalse; + while (one != bddtrue) + { + if (bdd_high(one) == bddfalse) + { + one = bdd_low(one); + continue; + } + int vn = bdd_var(one); + bdd v = bdd_ithvar(vn); + resacc |= bdd_exist(all_orig_neg, v) & v; + res |= acc_[remap_table[n][vn]]; + one = bdd_high(one); + } + if (res != bddfalse) + res |= missingacc; + int id = resacc.id(); + remap_[n][id] = res; + } + } } T* @@ -112,20 +185,24 @@ namespace spot // // (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_)); + unsigned v = sm_.scc_of_state(in_s); + if (sm_.accepting(u) && (!all_ || u == v)) + { + bdd acc = si->current_acceptance_conditions(); + if (acc == bddfalse) + return; + t->acceptance_conditions = remap_[u][acc.id()]; + } } private: T* out_; const scc_map& sm_; const std::vector& useless_; - bdd useful_; - bdd strip_; + unsigned max_num_; bool all_; + std::vector acc_; + remap_t remap_; }; } // anonymous @@ -137,48 +214,96 @@ namespace spot sm.build_map(); scc_stats ss = build_scc_stats(sm); - bdd useful = ss.useful_acc; - bdd negall = aut->neg_acceptance_conditions(); - // Compute a set of useless acceptance conditions. - // If the acceptance combinations occurring in - // the automata are { a, ab, abc, bd }, then - // USEFUL contains (a&!b&!c&!d)|(a&b&!c&!d)|(a&b&c&!d)|(!a&b&!c&d) - // and we want to find that 'a' and 'b' are useless because - // they always occur with 'c'. - // The way we check if 'a' is useless that is to look whether - // USEFUL implies (x -> a) for some other acceptance condition x. - bdd allconds = bdd_support(negall); - bdd allcondscopy = allconds; - bdd useless = bddtrue; - while (allconds != bddtrue) - { - bdd a = bdd_ithvar(bdd_var(allconds)); - bdd others = allcondscopy; + remap_table_t remap_table(ss.scc_total); + std::vector max_table(ss.scc_total); + unsigned max_num = 1; - while (others != bddtrue) + for (unsigned n = 0; n < ss.scc_total; ++n) + { + if (!sm.accepting(n)) + continue; + bdd all = sm.useful_acc_of(n); + bdd negall = aut->neg_acceptance_conditions(); + + // Compute a set of useless acceptance conditions. + // If the acceptance combinations occurring in + // the automata are { a, ab, abc, bd }, then + // ALL contains (a&!b&!c&!d)|(a&b&!c&!d)|(a&b&c&!d)|(!a&b&!c&d) + // and we want to find that 'a' and 'b' are useless because + // they always occur with 'c'. + // The way we check if 'a' is useless is to look whether ALL + // implies (x -> a) for some other acceptance condition x. + bdd allconds = bdd_support(negall); + bdd allcondscopy = allconds; + bdd useless = bddtrue; + while (allconds != bddtrue) { - bdd x = bdd_ithvar(bdd_var(others)); - if (x != a) + // Speed-up the computation of implied acceptance by + // removing those that are always present. We detect + // those that appear as conjunction of positive variables + // at the start of ALL. + bdd prefix = bdd_satprefix(all); + if (prefix != bddtrue) { - if (bdd_implies(useful, x >> a)) + assert(prefix == bdd_support(prefix)); + allcondscopy = bdd_exist(allcondscopy, prefix); + if (allcondscopy != bddtrue) { - // a is useless - useful = bdd_exist(useful, a); + useless &= prefix; + } + else + { + // Never erase all conditions: at least keep one. + useless &= bdd_high(prefix); + break; + } + allconds = bdd_exist(allconds, prefix); + } + + // Pick a non-useless acceptance condition a. + bdd a = bdd_ithvar(bdd_var(allconds)); + // For all acceptance condition x that is not already useless... + bdd others = allcondscopy; + while (others != bddtrue) + { + bdd x = bdd_ithvar(bdd_var(others)); + // ... check whether it always implies a. + if (x != a && bdd_implies(all, x >> a)) + { + // If so, a is useless. + all = bdd_exist(all, a); useless &= a; allcondscopy = bdd_exist(allcondscopy, a); break; } + others = bdd_high(others); } - others = bdd_high(others); + allconds = bdd_high(allconds); } - allconds = bdd_high(allconds); + + // We never remove ALL acceptance marks. + assert(negall == bddtrue || useless != bdd_support(negall)); + + bdd useful = bdd_exist(negall, useless); + + // Go over all useful sets of acceptance marks, and give them + // a number. + unsigned num = 1; + // First compute the number of acceptance conditions used. + for (BDD c = useful.id(); c != 1; c = bdd_low(c)) + ++num; + max_table[n] = num; + if (num > max_num) + max_num = num; + // Then number all of these acceptance conditions in the + // reverse order. This makes sure that the associated number + // varies in the same direction as the bdd variables, which in + // turn makes sure we preserve the acceptance condition + // ordering (which matters for degeneralization). + for (BDD c = useful.id(); c != 1; c = bdd_low(c)) + remap_table[n].insert(std::make_pair(bdd_var(c), --num)); } - // We never remove ALL acceptance conditions. - assert(negall == bddtrue || useless != bdd_support(negall)); - - useful = compute_all_acceptance_conditions(bdd_exist(negall, useless)); - // In most cases we will create a tgba_explicit_string copy of the // initial tgba, but this is not very space efficient as the // labels are built using the "format_state()" string output of @@ -190,8 +315,8 @@ namespace spot if (af) { filter_iter fi(af, sm, ss.useless_scc_map, - useful, useless, - remove_all_useless); + remap_table, max_num, + max_table, remove_all_useless); fi.run(); tgba_explicit_formula* res = fi.result(); res->merge_transitions(); @@ -202,8 +327,8 @@ namespace spot if (as) { filter_iter fi(aut, sm, ss.useless_scc_map, - useful, useless, - remove_all_useless); + remap_table, max_num, + max_table, remove_all_useless); fi.run(); tgba_explicit_string* res = fi.result(); res->merge_transitions(); @@ -212,8 +337,8 @@ namespace spot else { filter_iter fi(aut, sm, ss.useless_scc_map, - useful, useless, - remove_all_useless); + remap_table, max_num, + max_table, remove_all_useless); fi.run(); tgba_explicit_number* res = fi.result(); res->merge_transitions(); diff --git a/src/tgbatest/ltl2ta.test b/src/tgbatest/ltl2ta.test index d6f846fe1..e5fc0c8cf 100755 --- a/src/tgbatest/ltl2ta.test +++ b/src/tgbatest/ltl2ta.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et +# Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -101,8 +101,8 @@ grep 'states: 21$' stdout # Note: after minimization with -TA -RT. # has 20 states and 89 transitions, after minimization. ../ltl2tgba -ks -TA -RT -DS "$f" > stdout -grep 'transitions: 89$' stdout -grep 'states: 20$' stdout +grep 'transitions: 85$' stdout +grep 'states: 19$' stdout f='GFa & GFb & GFc & GFd & GFe & GFg' @@ -119,12 +119,12 @@ grep 'states: 290$' stdout #tests with artificial livelock state: run 0 ../ltl2tgba -ks -TA -lv -DS "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout -grep 'transitions: 882$' stdout -grep 'states: 78$' stdout +grep 'transitions: 790$' stdout +grep 'states: 66$' stdout run 0 ../ltl2tgba -TA -RT -ks -lv -DS "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout -grep 'transitions: 440$' stdout -grep 'states: 28$' stdout +grep 'transitions: 390$' stdout +grep 'states: 26$' stdout run 0 ../ltl2tgba -TGTA -RT -ks 'Gq|Gr|(G(q|FGp)&G(r|FG!p))' >stdout grep 'transitions: 294$' stdout @@ -153,16 +153,16 @@ grep 'states: 32$' stdout run 0 ../ltl2tgba -TA -RT -ks -in -R3 -x -DS "$f" >stdout -grep 'transitions: 436$' stdout -grep 'states: 36$' stdout +grep 'transitions: 450$' stdout +grep 'states: 38$' stdout run 0 ../ltl2tgba -TA -RT -ks -sp -lv -R3 -x -DS "$f" >stdout -grep 'transitions: 537$' stdout -grep 'states: 38$' stdout +grep 'transitions: 551$' stdout +grep 'states: 40$' stdout run 0 ../ltl2tgba -TA -ks -sp -lv -DS "$f" >stdout -grep 'transitions: 609$' stdout +grep 'transitions: 597$' stdout grep 'states: 46$' stdout @@ -177,7 +177,7 @@ grep 'states: 32$' stdout g="G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))" run 0 ../ltl2tgba -TA -RT -ks -DS "$g" >stdout -grep 'transitions: 2147$' stdout +grep 'transitions: 2133$' stdout grep 'states: 97$' stdout diff --git a/src/tgbatest/sccsimpl.test b/src/tgbatest/sccsimpl.test index 102e58e68..15562fbc4 100755 --- a/src/tgbatest/sccsimpl.test +++ b/src/tgbatest/sccsimpl.test @@ -1,6 +1,6 @@ #!/bin/sh -# Copyright (C) 2011 Laboratoire de Recherche et Developpement de -# l'Epita +# Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement +# de l'Epita # # This file is part of Spot, a model checking library. # @@ -54,7 +54,7 @@ S4, S4, "!p1",; EOF run 0 ../ltl2tgba -X -R3 -b aut.txt > out.txt -grep '^acc = "p1";$' out.txt +grep '^acc = "[^"]*";$' out.txt # Here, acceptances A and C can both be removed. @@ -66,7 +66,7 @@ S1, S1, "c", A B C; S1, S1, "d", C D; EOF run 0 ../ltl2tgba -X -R3 -b aut2.txt > out2.txt -grep '^acc = "B" "D";$' out2.txt || grep '^acc = "D" "B";$' out2.txt || exit 1 +grep '^acc = "." ".";$' out2.txt || exit 1 # only 4 lines output, because the "b" and "c" lines have been merged. test `wc -l < out2.txt` = 4 @@ -80,7 +80,7 @@ S1, S1, "c", A B C; S1, S1, "d", B D; EOF run 0 ../ltl2tgba -X -R3 -b aut3.txt > out3.txt -grep '^acc = "C" "D";$' out3.txt || grep '^acc = "D" "C";$' out3.txt || exit 1 +grep '^acc = "." ".";$' out3.txt || exit 1 # only 4 lines output, because the "a" and "b" lines have been merged. test `wc -l < out3.txt` = 4 @@ -158,6 +158,4 @@ S6, S6, "(p1 & !p2) | (p3 & !p2)", ZZ "!p2"; S6, S6, "p1 | p2 | p3", ZZ; EOF run 0 ../ltl2tgba -X -R3 -b aut7.txt > out7.txt -# ZZ should disappear -grep ZZ out7.txt && exit 1 test `grep '^acc' out7.txt | wc -w` = 4