alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor::visit) <G>:

Browse source 
Optimize translation of GFy.
This commit is contained in:
Alexandre Duret-Lutz 2003-11-26 18:02:51 +00:00
parent 7e81306d45
commit 334ae6e757
2 changed files with 55 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

3
ChangeLog
View file

@ -1,5 +1,8 @@
2003-11-26 Alexandre Duret-Lutz <adl@src.lip6.fr> 2003-11-26 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor::visit) <G>:
Optimize translation of GFy.
* src/tgba/bddprint.cc (print_accset_handler, bdd_print_accset): New * src/tgba/bddprint.cc (print_accset_handler, bdd_print_accset): New
functions. functions.
* src/tgba/bddprint.cc (bdd_print_accset): Declare it. * src/tgba/bddprint.cc (bdd_print_accset): Declare it.

89
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -63,18 +63,18 @@ namespace spot
{ {
fv_map::iterator i; fv_map::iterator i;
for (i = a_map.begin(); i != a_map.end(); ++i) for (i = a_map.begin(); i != a_map.end(); ++i)
ltl::destroy(i->first); destroy(i->first);
for (i = var_map.begin(); i != var_map.end(); ++i) for (i = var_map.begin(); i != var_map.end(); ++i)
ltl::destroy(i->first); destroy(i->first);
for (i = next_map.begin(); i != next_map.end(); ++i) for (i = next_map.begin(); i != next_map.end(); ++i)
ltl::destroy(i->first); destroy(i->first);
} }
/// Formula-to-BDD-variable maps. /// Formula-to-BDD-variable maps.
typedef Sgi::hash_map<const ltl::formula*, int, typedef Sgi::hash_map<const formula*, int,
ptr_hash<ltl::formula> > fv_map; ptr_hash<formula> > fv_map;
/// BDD-variable-to-formula maps. /// BDD-variable-to-formula maps.
typedef Sgi::hash_map<int, const ltl::formula*> vf_map; typedef Sgi::hash_map<int, const formula*> vf_map;
fv_map a_map; ///< Maps formulae to "a" BDD variables fv_map a_map; ///< Maps formulae to "a" BDD variables
vf_map a_formula_map; ///< Maps "a" BDD variables to formulae vf_map a_formula_map; ///< Maps "a" BDD variables to formulae
@ -88,7 +88,7 @@ namespace spot
bdd next_set; bdd next_set;
int int
register_proposition(const ltl::formula* f) register_proposition(const formula* f)
{ {
int num; int num;
// Do not build a variable that already exists. // Do not build a variable that already exists.
@ -109,7 +109,7 @@ namespace spot
} }
int int
register_a_variable(const ltl::formula* f) register_a_variable(const formula* f)
{ {
int num; int num;
// Do not build an accepting variable that already exists. // Do not build an accepting variable that already exists.
@ -130,7 +130,7 @@ namespace spot
} }
int int
register_next_variable(const ltl::formula* f) register_next_variable(const formula* f)
{ {
int num; int num;
// Do not build a Next variable that already exists. // Do not build a Next variable that already exists.
@ -175,35 +175,35 @@ namespace spot
return os; return os;
} }
ltl::formula* formula*
var_to_formula(int var) const var_to_formula(int var) const
{ {
vf_map::const_iterator isi = next_formula_map.find(var); vf_map::const_iterator isi = next_formula_map.find(var);
if (isi != next_formula_map.end()) if (isi != next_formula_map.end())
return ltl::clone(isi->second); return clone(isi->second);
isi = a_formula_map.find(var); isi = a_formula_map.find(var);
if (isi != a_formula_map.end()) if (isi != a_formula_map.end())
return ltl::clone(isi->second); return clone(isi->second);
isi = var_formula_map.find(var); isi = var_formula_map.find(var);
if (isi != var_formula_map.end()) if (isi != var_formula_map.end())
return ltl::clone(isi->second); return clone(isi->second);
assert(0); assert(0);
} }
ltl::formula* formula*
conj_bdd_to_formula(bdd b) conj_bdd_to_formula(bdd b)
{ {
if (b == bddfalse) if (b == bddfalse)
return ltl::constant::false_instance(); return constant::false_instance();
ltl::multop::vec* v = new ltl::multop::vec; multop::vec* v = new multop::vec;
while (b != bddtrue) while (b != bddtrue)
{ {
int var = bdd_var(b); int var = bdd_var(b);
ltl::formula* res = var_to_formula(var); formula* res = var_to_formula(var);
bdd high = bdd_high(b); bdd high = bdd_high(b);
if (high == bddfalse) if (high == bddfalse)
{ {
res = ltl::unop::instance(ltl::unop::Not, res); res = unop::instance(unop::Not, res);
b = bdd_low(b); b = bdd_low(b);
} }
else else
@ -214,14 +214,14 @@ namespace spot
assert(b != bddfalse); assert(b != bddfalse);
v->push_back(res); v->push_back(res);
} }
return ltl::multop::instance(ltl::multop::And, v); return multop::instance(multop::And, v);
} }
const formula* const formula*
bdd_to_formula(bdd f) bdd_to_formula(bdd f)
{ {
if (f == bddfalse) if (f == bddfalse)
return ltl::constant::false_instance(); return constant::false_instance();
multop::vec* v = new multop::vec; multop::vec* v = new multop::vec;
@ -248,13 +248,13 @@ namespace spot
} }
else else
{ {
ltl::formula* ac = var_to_formula(var); formula* ac = var_to_formula(var);
if (! a->has_accepting_condition(ac)) if (! a->has_accepting_condition(ac))
a->declare_accepting_condition(ltl::clone(ac)); a->declare_accepting_condition(clone(ac));
a->add_accepting_condition(t, ac); a->add_accepting_condition(t, ac);
ltl::atomic_prop::instance_count(); atomic_prop::instance_count();
b = high; b = high;
} }
assert(b != bddfalse); assert(b != bddfalse);
@ -321,10 +321,25 @@ namespace spot
} }
case unop::G: case unop::G:
{ {
// r(Gy) = r(y)r(XGy) const formula* child = node->child();
bdd y = recurse(node->child());
int x = dict_.register_next_variable(node); int x = dict_.register_next_variable(node);
res_ = y & bdd_ithvar(x); // GFy is pretty frequent and easy to optimize, to we
// want to detect it.
const unop* Fy = dynamic_cast<const unop*>(child);
if (Fy && Fy->op() == unop::F)
{
// r(GFy) = (r(y) + a(y))r(XGFy)
const formula* child = Fy->child();
bdd y = recurse(child);
int a = dict_.register_a_variable(child);
res_ = (y | bdd_ithvar(a)) & bdd_ithvar(x);
}
else
{
// r(Gy) = r(y)r(XGy)
bdd y = recurse(child);
res_ = y & bdd_ithvar(x);
}
return; return;
} }
case unop::Not: case unop::Not:
@ -420,18 +435,18 @@ namespace spot
} }
tgba_explicit* tgba_explicit*
ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict) ltl_to_tgba_fm(const formula* f, bdd_dict* dict)
{ {
// Normalize the formula. We want all the negations on // Normalize the formula. We want all the negations on
// the atomic propositions. We also suppress logic // the atomic propositions. We also suppress logic
// abbreviations such as <=>, =>, or XOR, since they // abbreviations such as <=>, =>, or XOR, since they
// would involve negations at the BDD level. // would involve negations at the BDD level.
ltl::formula* f1 = ltl::unabbreviate_logic(f); formula* f1 = unabbreviate_logic(f);
ltl::formula* f2 = ltl::negative_normal_form(f1); formula* f2 = negative_normal_form(f1);
ltl::destroy(f1); destroy(f1);
std::set<ltl::formula*> formulae_seen; std::set<formula*> formulae_seen;
std::set<ltl::formula*> formulae_to_translate; std::set<formula*> formulae_to_translate;
formulae_seen.insert(f2); formulae_seen.insert(f2);
formulae_to_translate.insert(f2); formulae_to_translate.insert(f2);
@ -443,7 +458,7 @@ namespace spot
while (!formulae_to_translate.empty()) while (!formulae_to_translate.empty())
{ {
// Pick one formula. // Pick one formula.
ltl::formula* f = *formulae_to_translate.begin(); formula* f = *formulae_to_translate.begin();
formulae_to_translate.erase(formulae_to_translate.begin()); formulae_to_translate.erase(formulae_to_translate.begin());
// Translate it into a BDD to simplify it. // Translate it into a BDD to simplify it.
@ -458,7 +473,7 @@ namespace spot
bdd cube; bdd cube;
while ((cube = isop.next()) != bddfalse) while ((cube = isop.next()) != bddfalse)
{ {
ltl::formula* dest = formula* dest =
d.conj_bdd_to_formula(bdd_existcomp(cube, d.next_set)); d.conj_bdd_to_formula(bdd_existcomp(cube, d.next_set));
std::string next = to_string(dest); std::string next = to_string(dest);
@ -476,15 +491,15 @@ namespace spot
} }
else else
{ {
ltl::destroy(dest); destroy(dest);
} }
} }
} }
// Free all formulae. // Free all formulae.
for (std::set<ltl::formula*>::iterator i = formulae_seen.begin(); for (std::set<formula*>::iterator i = formulae_seen.begin();
i != formulae_seen.end(); ++i) i != formulae_seen.end(); ++i)
ltl::destroy(*i); destroy(*i);
// Turn all promises into real accepting conditions. // Turn all promises into real accepting conditions.
a->complement_all_accepting_conditions(); a->complement_all_accepting_conditions();