Commit 20c3f9f8 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

Simplify the construction of TA.

* src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh: Add a version
that builds a BDD.
* src/tgbatest/ltl2tgba.cc: Use it.
parent 8e1438c9
......@@ -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;
}
}
}
......@@ -27,9 +27,12 @@
#include <set>
#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);
/// @}
}
}
......
......@@ -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)
{
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment