From 11b9ada2bb2fb88e22cc4c822a6b5626db32325d Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Tue, 21 Jul 2015 17:30:56 +0200 Subject: [PATCH] Ease atomic proposition manipulation for twa. * doc/org/tut22.org, src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh, src/parseaut/parseaut.yy, src/tests/ikwiad.cc, src/tests/tgbagraph.test, src/tests/twagraph.cc, src/twa/twa.cc, src/twa/twa.hh, src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/randomgraph.cc, src/twaalgos/relabel.cc, src/twaalgos/stutter.cc, src/twaalgos/stutter.hh: here. --- doc/org/tut22.org | 16 ++++--------- src/ltlvisit/apcollect.cc | 7 ++---- src/ltlvisit/apcollect.hh | 2 +- src/parseaut/parseaut.yy | 5 ++-- src/tests/ikwiad.cc | 2 +- src/tests/tgbagraph.test | 2 ++ src/tests/twagraph.cc | 15 ++++-------- src/twa/twa.cc | 3 +++ src/twa/twa.hh | 46 +++++++++++++++++++++++++++++++++++++ src/twaalgos/ltl2tgba_fm.cc | 33 +++++++++++++++++++++----- src/twaalgos/randomgraph.cc | 2 +- src/twaalgos/relabel.cc | 4 ++-- src/twaalgos/stutter.cc | 28 +++++----------------- src/twaalgos/stutter.hh | 4 ++-- 14 files changed, 104 insertions(+), 65 deletions(-) diff --git a/doc/org/tut22.org b/doc/org/tut22.org index b8b499993..acfe651c4 100644 --- a/doc/org/tut22.org +++ b/doc/org/tut22.org @@ -20,19 +20,11 @@ The interface // This creates an empty automaton that we have yet to fill. spot::twa_graph_ptr aut = make_twa_graph(dict); - // The current way to associate a BDD to an atomic proposition is - // not really nice, and should be improved in the future. Currently - // the string first have to be converted into (LTL) formulas... - spot::ltl::environment& e = spot::ltl::default_environment::instance(); - const spot::ltl::formula* f1 = e.require("p1"); - const spot::ltl::formula* f2 = e.require("p2"); - // ...and then those formula can be registered to the BDD dict. The - // BDD dict wants to keep track of which automaton uses which BDD - // variable, so we supply that pointer to aut. The - // register_proposition() function returns a BDD variable number + // Since a BDD is associated to every atomic proposition, the + // register_ap() function returns a BDD variable number // that can be converted into a BDD using bdd_ithvar(). - bdd p1 = bdd_ithvar(dict->register_proposition(f1, aut)); - bdd p2 = bdd_ithvar(dict->register_proposition(f2, aut)); + bdd p1 = bdd_ithvar(aut->register_ap("p1")); + bdd p2 = bdd_ithvar(aut->register_ap("p2")); // Set the acceptance condition of the automaton to Inf(0)&Inf(1) aut->set_generalized_buchi(2); diff --git a/src/ltlvisit/apcollect.cc b/src/ltlvisit/apcollect.cc index ca6286d6a..d1c092d7d 100644 --- a/src/ltlvisit/apcollect.cc +++ b/src/ltlvisit/apcollect.cc @@ -85,18 +85,15 @@ namespace spot } bdd - atomic_prop_collect_as_bdd(const formula* f, const const_twa_ptr& a) + atomic_prop_collect_as_bdd(const formula* f, const twa_ptr& a) { spot::ltl::atomic_prop_set aps; atomic_prop_collect(f, &aps); - auto d = a->get_dict(); bdd res = bddtrue; for (atomic_prop_set::const_iterator i = aps.begin(); i != aps.end(); ++i) - res &= bdd_ithvar(d->register_proposition(*i, a)); + res &= bdd_ithvar(a->register_ap(*i)); return res; } - } - } diff --git a/src/ltlvisit/apcollect.hh b/src/ltlvisit/apcollect.hh index ed92714be..dab6052c1 100644 --- a/src/ltlvisit/apcollect.hh +++ b/src/ltlvisit/apcollect.hh @@ -68,7 +68,7 @@ namespace spot /// \return A conjunction the atomic propositions. SPOT_API bdd atomic_prop_collect_as_bdd(const formula* f, - const const_twa_ptr& a); + const twa_ptr& a); /// @} } diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy index e78374013..0539188c9 100644 --- a/src/parseaut/parseaut.yy +++ b/src/parseaut/parseaut.yy @@ -555,7 +555,6 @@ ap-name: STRING if (!res.ignore_more_ap) { auto f = res.env->require(*$1); - auto d = res.h->aut->get_dict(); int b = 0; if (f == nullptr) { @@ -564,11 +563,11 @@ ap-name: STRING error(@1, out.str()); f = spot::ltl::default_environment::instance() .require("$unknown$"); - b = d->register_proposition(f, res.h->aut); + b = res.h->aut->register_ap(f); } else { - b = d->register_proposition(f, res.h->aut); + b = res.h->aut->register_ap(f); if (!res.ap_set.emplace(b).second) { std::ostringstream out; diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index c0dbc61ff..6b504be67 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -1255,7 +1255,7 @@ checked_main(int argc, char** argv) if (opt_stutterize) { - a = sl(ensure_digraph(a), f); + a = sl(ensure_digraph(a)); } if (opt_monitor) diff --git a/src/tests/tgbagraph.test b/src/tests/tgbagraph.test index ac5d60025..cb8fe8230 100755 --- a/src/tests/tgbagraph.test +++ b/src/tests/tgbagraph.test @@ -33,6 +33,8 @@ set -e run 0 ../tgbagraph | tee stdout cat >expected <register_proposition(f1, tg)); - bdd p2 = bdd_ithvar(d->register_proposition(f2, tg)); + bdd p1 = bdd_ithvar(tg->register_ap("p1")); + bdd p2 = bdd_ithvar(tg->register_ap("p2")); tg->acc().add_sets(2); - f1->destroy(); - f2->destroy(); + + for (auto *f: tg->ap()) + std::cout << f->name() << '\n'; auto s1 = tg->new_state(); auto s2 = tg->new_state(); diff --git a/src/twa/twa.cc b/src/twa/twa.cc index 3718d8efd..6627b6c3f 100644 --- a/src/twa/twa.cc +++ b/src/twa/twa.cc @@ -34,10 +34,13 @@ namespace spot last_support_conditions_input_(0) { props = 0U; + bddaps_ = bddtrue; } twa::~twa() { + for (auto* ap: aps_) + ap->destroy(); if (last_support_conditions_input_) last_support_conditions_input_->destroy(); delete iter_cache_; diff --git a/src/twa/twa.hh b/src/twa/twa.hh index 1d5956e25..a82161fa8 100644 --- a/src/twa/twa.hh +++ b/src/twa/twa.hh @@ -30,8 +30,10 @@ #include #include #include +#include #include "misc/casts.hh" #include "misc/hash.hh" +#include "ltlast/atomic_prop.hh" namespace spot { @@ -590,6 +592,46 @@ namespace spot return dict_; } + /// \brief Register an atomic proposition designated by formula \a ap. + /// + /// \return The variable number inside of the BDD. + int register_ap(const ltl::formula* ap) + { + aps_.push_back(dynamic_cast(ap)); + ap->clone(); + int res = dict_->register_proposition(ap, this); + bddaps_ &= bdd_ithvar(res); + return res; + } + + /// \brief Register an atomic proposition designated by string \a ap. + /// + /// This string is converted into a formula and registered + /// inside of the BDD manager. + /// + /// \return The variable number inside of the BDD. + int register_ap(std::string name, + ltl::environment& e = ltl::default_environment::instance()) + { + auto* ap = e.require(name); + aps_.push_back(dynamic_cast(ap)); + int res = dict_->register_proposition(ap, this); + bddaps_ &= bdd_ithvar(res); + return res; + } + + /// \brief Get the vector of atomic propositions used by this + /// automaton. + const std::vector& ap() const + { + return aps_; + } + + bdd ap_var() const + { + return bddaps_; + } + /// \brief Format the state as a string for printing. /// /// This formating is the responsability of the automata @@ -688,6 +730,8 @@ namespace spot void copy_ap_of(const const_twa_ptr& a) { get_dict()->register_all_propositions_of(a, this); + for (auto *f: a->ap()) + this->register_ap(f); } void set_generalized_buchi(unsigned num) @@ -710,6 +754,8 @@ namespace spot mutable const state* last_support_conditions_input_; private: mutable bdd last_support_conditions_output_; + std::vector aps_; + bdd bddaps_; protected: diff --git a/src/twaalgos/ltl2tgba_fm.cc b/src/twaalgos/ltl2tgba_fm.cc index 73ebc0c5a..fedd6950b 100644 --- a/src/twaalgos/ltl2tgba_fm.cc +++ b/src/twaalgos/ltl2tgba_fm.cc @@ -139,11 +139,13 @@ namespace spot { public: - translate_dict(const bdd_dict_ptr& dict, + translate_dict(twa_graph_ptr& a, + const bdd_dict_ptr& dict, acc_cond& acc, ltl_simplifier* ls, bool exprop, bool single_acc, bool unambiguous) - : dict(dict), + : a_(a), + dict(dict), ls(ls), a_set(bddtrue), var_set(bddtrue), @@ -168,6 +170,7 @@ namespace spot j++->first.f->destroy(); } + twa_graph_ptr& a_; bdd_dict_ptr dict; ltl_simplifier* ls; mark_tools mt; @@ -418,6 +421,26 @@ namespace spot { bdd res = ls->as_bdd(f); var_set &= bdd_support(res); + + bdd all = var_set; + while (all != bddfalse) + { + bdd one = bdd_satone(all); + all -= one; + while (one != bddtrue) + { + int v = bdd_var(one); + auto *f = var_to_formula(v); + a_->register_ap(f); + f->destroy(); + if (bdd_high(one) == bddfalse) + one = bdd_low(one); + else + one = bdd_high(one); + } + } + + return res; } @@ -2301,7 +2324,8 @@ namespace spot twa_graph_ptr a = make_twa_graph(dict); auto namer = a->create_namer(); - translate_dict d(dict, a->acc(), s, exprop, f->is_syntactic_persistence(), + translate_dict d(a, dict, a->acc(), s, exprop, + f->is_syntactic_persistence(), unambiguous); // Compute the set of all promises that can possibly occur @@ -2568,10 +2592,7 @@ namespace spot // Set the following to true to preserve state names. a->release_formula_namer(namer, false); - dict->register_propositions(fc.used_vars(), a); - auto& acc = a->acc(); - unsigned ns = a->num_states(); for (unsigned s = 0; s < ns; ++s) for (auto& t: a->out(s)) diff --git a/src/twaalgos/randomgraph.cc b/src/twaalgos/randomgraph.cc index 30c2b2d3a..47eb2e801 100644 --- a/src/twaalgos/randomgraph.cc +++ b/src/twaalgos/randomgraph.cc @@ -139,7 +139,7 @@ namespace spot int pi = 0; for (auto i: *ap) - props[pi++] = dict->register_proposition(i, res); + props[pi++] = res->register_ap(i); res->set_generalized_buchi(n_accs); diff --git a/src/twaalgos/relabel.cc b/src/twaalgos/relabel.cc index 00330aa65..d5643b343 100644 --- a/src/twaalgos/relabel.cc +++ b/src/twaalgos/relabel.cc @@ -30,8 +30,8 @@ namespace spot vars.reserve(relmap->size()); for (auto& p: *relmap) { - int oldv = d->register_proposition(p.first, aut); - int newv = d->register_proposition(p.second, aut); + int oldv = aut->register_ap(p.first); + int newv = aut->register_ap(p.second); bdd_setpair(pairs, oldv, newv); vars.push_back(oldv); } diff --git a/src/twaalgos/stutter.cc b/src/twaalgos/stutter.cc index 99989d4ba..10a855543 100644 --- a/src/twaalgos/stutter.cc +++ b/src/twaalgos/stutter.cc @@ -281,34 +281,18 @@ namespace spot // Queue of state to be processed. typedef std::deque queue_t; - - static bdd - get_all_ap(const const_twa_graph_ptr& a) - { - bdd res = bddtrue; - for (auto& i: a->edges()) - res &= bdd_support(i.cond); - return res; - } - } twa_graph_ptr - sl(const const_twa_graph_ptr& a, const ltl::formula* f) + sl(const twa_graph_ptr& a) { - bdd aps = f - ? atomic_prop_collect_as_bdd(f, a) - : get_all_ap(a); - return sl(a, aps); + return sl(a, a->ap_var()); } twa_graph_ptr - sl2(const const_twa_graph_ptr& a, const ltl::formula* f) + sl2(const twa_graph_ptr& a) { - bdd aps = f - ? atomic_prop_collect_as_bdd(f, a) - : get_all_ap(a); - return sl2(a, aps); + return sl2(a, a->ap_var()); } twa_graph_ptr @@ -379,7 +363,7 @@ namespace spot sl2(twa_graph_ptr&& a, bdd atomic_propositions) { if (atomic_propositions == bddfalse) - atomic_propositions = get_all_ap(a); + atomic_propositions = a->ap_var(); unsigned num_states = a->num_states(); unsigned num_edges = a->num_edges(); std::vector selfloops(num_states, bddfalse); @@ -666,7 +650,7 @@ namespace spot } is_stut = is_stutter_invariant(make_twa_graph(aut, twa::prop_set::all()), - std::move(neg), get_all_ap(aut)); + std::move(neg), aut->ap_var()); aut->prop_stutter_invariant(is_stut); aut->prop_stutter_sensitive(!is_stut); return is_stut; diff --git a/src/twaalgos/stutter.hh b/src/twaalgos/stutter.hh index 487f176a6..5be5d0164 100644 --- a/src/twaalgos/stutter.hh +++ b/src/twaalgos/stutter.hh @@ -24,13 +24,13 @@ namespace spot { SPOT_API twa_graph_ptr - sl(const const_twa_graph_ptr&, const ltl::formula* = nullptr); + sl(const twa_graph_ptr&); SPOT_API twa_graph_ptr sl(const const_twa_graph_ptr&, bdd); SPOT_API twa_graph_ptr - sl2(const const_twa_graph_ptr&, const ltl::formula* = nullptr); + sl2(const twa_graph_ptr&); SPOT_API twa_graph_ptr sl2(const const_twa_graph_ptr&, bdd);