diff --git a/src/ltlvisit/apcollect.cc b/src/ltlvisit/apcollect.cc index 1c4636f71..ab58a60bd 100644 --- a/src/ltlvisit/apcollect.cc +++ b/src/ltlvisit/apcollect.cc @@ -24,6 +24,8 @@ #include "apcollect.hh" #include "ltlvisit/postfix.hh" +#include "tgba/tgba.hh" +#include "tgba/bdddict.hh" namespace spot { @@ -63,6 +65,19 @@ namespace spot return s; } + bdd + atomic_prop_collect_as_bdd(const formula* f, tgba* a) + { + spot::ltl::atomic_prop_set aps; + atomic_prop_collect(f, &aps); + bdd_dict* 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)); + return res; + } + } } diff --git a/src/ltlvisit/apcollect.hh b/src/ltlvisit/apcollect.hh index 3cf12f337..e8bc8d221 100644 --- a/src/ltlvisit/apcollect.hh +++ b/src/ltlvisit/apcollect.hh @@ -27,9 +27,12 @@ #include #include "ltlast/atomic_prop.hh" +#include "bdd.h" namespace spot { + class tgba; + namespace ltl { /// \addtogroup ltl_misc @@ -50,6 +53,14 @@ namespace spot atomic_prop_set* atomic_prop_collect(const formula* f, atomic_prop_set* s = 0); + /// \brief Return the set of atomic propositions occurring in a formula, as a BDD. + /// + /// \param f the formula to inspect + /// \param a that automaton that should register the BDD variables used. + /// \return A conjunction the atomic propositions. + bdd + atomic_prop_collect_as_bdd(const formula* f, tgba* a); + /// @} } } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index a8138027b..ee5be9e7e 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1101,18 +1101,7 @@ main(int argc, char** argv) //TA, STA, GTA, SGTA and TGTA if (ta_opt || tgta_opt) { - spot::ltl::atomic_prop_set* aps = atomic_prop_collect(f, 0); - - bdd atomic_props_set_bdd = bddtrue; - for (spot::ltl::atomic_prop_set::const_iterator i = aps->begin(); i - != aps->end(); ++i) - { - bdd atomic_prop = bdd_ithvar((a->get_dict())->var_map[*i]); - - atomic_props_set_bdd &= atomic_prop; - - } - delete aps; + bdd atomic_props_set_bdd = atomic_prop_collect_as_bdd(f, a); if (ta_opt) {