diff --git a/ChangeLog b/ChangeLog index 811a30d1d..560c7ca06 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,18 @@ +2009-09-04 Damien Lefortier + + Add an algorithm (from Couvreur) working on BDDs to reduce the + size of TGBAs represented as BDDs by deleting unaccepting SCCs. + + * src/eltlparse/eltlparse.yy: Remove a warning. + * src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh, + src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh: Add a + new function delete_unaccepting_scc in both classes. + * src/tgbatest/eltl2tgba.cc, src/tgbatest/spotlbtt.test: Use this + new function in LaCIM for ELTL and bench it. + * src/tgbatest/defs.in: Fix it. + * bench/ltl2tgba/algorithms, bench/ltl2tgba/defs.in: Add LaCIM for + ELTL in benchs. + 2009-09-01 Alexandre Duret-Lutz Fix path to libtool in test suites. diff --git a/bench/ltl2tgba/algorithms b/bench/ltl2tgba/algorithms index 6d2a9d25e..5aa78d95a 100644 --- a/bench/ltl2tgba/algorithms +++ b/bench/ltl2tgba/algorithms @@ -31,6 +31,22 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "LACIM, eltl" + Path = "$LBTT_TRANSLATE" + Parameters = "--spot '$ELTL2TGBA -LW'" + Enabled = yes +} + +Algorithm +{ + Name = "LACIM, eltl, +delete_unaccepting_scc" + Path = "$LBTT_TRANSLATE" + Parameters = "--spot '$ELTL2TGBA -L'" + Enabled = yes +} + Algorithm { Name = "FM, degen, +symb_merge, +exprop, LTLopt" diff --git a/bench/ltl2tgba/defs.in b/bench/ltl2tgba/defs.in index 5c1451892..20729104f 100644 --- a/bench/ltl2tgba/defs.in +++ b/bench/ltl2tgba/defs.in @@ -40,6 +40,7 @@ LBTT_TRANSLATE="@LBTT_TRANSLATE@" LTL2BA='@LTL2BA@' LTL2NBA='@LTL2NBA@' LTL2TGBA='@top_builddir@/src/tgbatest/ltl2tgba@EXEEXT@' +ELTL2TGBA='@top_builddir@/src/tgbatest/eltl2tgba@EXEEXT@' MODELLA='@MODELLA@' SPIN='@SPIN@' WRING2LBTT='@WRING2LBTT@' diff --git a/src/eltlparse/eltlparse.yy b/src/eltlparse/eltlparse.yy index 9ec813185..080979e59 100644 --- a/src/eltlparse/eltlparse.yy +++ b/src/eltlparse/eltlparse.yy @@ -368,7 +368,7 @@ nfa_arg: ARG aliasmap::const_iterator i = amap.find(*$1); if (i != amap.end()) { - int arity = formula_tree::arity(i->second); + unsigned arity = formula_tree::arity(i->second); CHECK_ARITY(@1, $1, $3->children.size(), arity); // Hack to return the right type without screwing with the diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc index 075e93ffa..df3bb08fc 100644 --- a/src/tgba/tgbabddconcrete.cc +++ b/src/tgba/tgbabddconcrete.cc @@ -164,4 +164,11 @@ namespace spot return data_; } + void + tgba_bdd_concrete::delete_unaccepting_scc() + { + data_.delete_unaccepting_scc(init_); + set_init_state(init_); + } + } diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh index ffa9bca32..0d42d154a 100644 --- a/src/tgba/tgbabddconcrete.hh +++ b/src/tgba/tgbabddconcrete.hh @@ -79,6 +79,10 @@ namespace spot virtual bdd all_acceptance_conditions() const; virtual bdd neg_acceptance_conditions() const; + /// \brief Delete SCCs (Strongly Connected Components) from the + /// TGBA which cannot be accepting. + void delete_unaccepting_scc(); + protected: virtual bdd compute_support_conditions(const state* state) const; virtual bdd compute_support_variables(const state* state) const; diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc index a43ed8a03..7a633b120 100644 --- a/src/tgba/tgbabddcoredata.cc +++ b/src/tgba/tgbabddcoredata.cc @@ -130,4 +130,67 @@ namespace spot acc_set &= acc; negacc_set &= !acc; } + + void + tgba_bdd_core_data::delete_unaccepting_scc(bdd init) + { + bdd er = bdd_exist(relation, var_set); /// existsRelation + bdd s0 = bddfalse; + bdd s1 = bdd_exist(bdd_exist(init & relation, var_set), now_set); + s1 = bdd_replace(s1, dict->next_to_now); + + /// Find all reachable states + while (s0 != s1) + { + s0 = s1; + /// Compute s1 = succ(s0) | s + s1 = bdd_replace(bdd_exist(s0 & er, now_set), dict->next_to_now) | s0; + } + + /// Find states which can be visited infinitely often while seeing + /// all acceptance conditions + s0 = bddfalse; + while (s0 != s1) + { + s0 = s1; + bdd all = all_acceptance_conditions; + while (all != bddfalse) + { + bdd next = bdd_satone(all); + all -= next; + s1 = infinitely_often(s1, next, er); + } + } + + relation = s0 & (relation & bdd_replace(s0, dict->now_to_next)); + } + + bdd + tgba_bdd_core_data::infinitely_often(bdd s, bdd acc, bdd er) + { + bdd ar = acc & (relation & acceptance_conditions); /// accRelation + bdd s0 = bddfalse; + bdd s1 = s; + + while (s0 != s1) + { + s0 = s1; + bdd as = bdd_replace(s0, dict->now_to_next) & ar; + as = bdd_exist(bdd_exist(as, next_set), var_set) & s0; + + /// Do predStar + bdd s0_ = bddfalse; + bdd s1_ = bdd_exist(as, acc_set); + while (s0_ != s1_) + { + s0_ = s1_; + /// Compute s1_ = pred(s0_) | s0_ + s1_ = bdd_exist(er & bdd_replace(s0_, dict->now_to_next), next_set); + s1_ = (s1_ & s0) | s0_; + } + s1 = s0_; + } + + return s0; + } } diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh index 4b668ea38..0db119bff 100644 --- a/src/tgba/tgbabddcoredata.hh +++ b/src/tgba/tgbabddcoredata.hh @@ -142,6 +142,13 @@ namespace spot /// \brief Update the variable sets to take a new acceptance condition /// into account. void declare_acceptance_condition(bdd prom); + + /// \brief Delete SCCs (Strongly Connected Components) from the + /// relation which cannot be accepting. + void delete_unaccepting_scc(bdd init); + + private: + bdd infinitely_often(bdd s, bdd acc, bdd er); }; } diff --git a/src/tgbatest/defs.in b/src/tgbatest/defs.in index bf45bea6a..aff453e9c 100644 --- a/src/tgbatest/defs.in +++ b/src/tgbatest/defs.in @@ -50,7 +50,7 @@ mkdir $testSubDir cd $testSubDir DOT='@DOT@' -top_builddir='@top_builddir@' +top_builddir='../@top_builddir@' LBTT="@LBTT@" LBTT_TRANSLATE="@LBTT_TRANSLATE@" VALGRIND='@VALGRIND@' diff --git a/src/tgbatest/eltl2tgba.cc b/src/tgbatest/eltl2tgba.cc index b4a168ac9..a5d604d58 100644 --- a/src/tgbatest/eltl2tgba.cc +++ b/src/tgbatest/eltl2tgba.cc @@ -36,14 +36,18 @@ void syntax(char* prog) { - std::cerr << "Usage: " << prog << " [OPTIONS...] formula [file]" << std::endl - << " " << prog << " -F [OPTIONS...] file [file]" << std::endl - << " " << prog << " -L [OPTIONS...] file [file]" << std::endl + std::cerr << "Usage: " << prog << " [OPTIONS...] formula [file]" << std::endl + << " " << prog << " -F [OPTIONS...] file [file]" << std::endl + << " " << prog << " -L [OPTIONS...] file [file]" << std::endl + << " " << prog << " -LW [OPTIONS...] file [file]" << std::endl << std::endl << "Options:" << std::endl << " -F read the formula from the file (extended input format)" << std::endl << " -L read the formula from an LBTT-compatible file" + << std::endl + << " -LW read the formula from an LBTT-compatible file" + << " (with no reduction)" << std::endl; } @@ -76,14 +80,16 @@ main(int argc, char** argv) spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::formula* f = 0; int formula_index = 0; + int reduce = 1; if (strcmp(argv[1], "-F") == 0) { f = spot::eltl::parse_file(argv[2], p, env, false); formula_index = 2; } - if (strcmp(argv[1], "-L") == 0) + if (strcmp(argv[1], "-L") == 0 || strcmp(argv[1], "-LW") == 0) { + reduce = strcmp(argv[1], "-LW") == 0 ? 0 : 1; std::string input; std::ifstream ifs(argv[2]); std::getline(ifs, input, '\0'); @@ -118,8 +124,10 @@ main(int argc, char** argv) spot::bdd_dict* dict = new spot::bdd_dict(); spot::tgba_bdd_concrete* concrete = spot::eltl_to_tgba_lacim(f, dict); + if (reduce == 1) + concrete->delete_unaccepting_scc(); - if (strcmp(argv[1], "-L") == 0) + if (strcmp(argv[1], "-L") == 0 || strcmp(argv[1], "-LW") == 0) spot::lbtt_reachable(std::cout, concrete); else { diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 74b61c4b7..7629932e8 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -64,6 +64,14 @@ Algorithm { Name = "Spot (Couvreur -- LaCIM), eltl" Path = "${LBTT_TRANSLATE}" + Parameters = "--spot '../eltl2tgba -LW'" + Enabled = yes +} + +Algorithm +{ + Name = "Spot (Couvreur -- LaCIM), eltl + delete_unaccepting_scc" + Path = "${LBTT_TRANSLATE}" Parameters = "--spot '../eltl2tgba -L'" Enabled = yes }