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

Speedup construction of transitions in ltl_to_tgba_fm.

Browse source 
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate,
ltl_to_tgba_fm): Do not convert labels as Boolean formulas before
creating transitions.  Use the bdd directly, and register the used
transitions later.
This commit is contained in:
Alexandre Duret-Lutz 2011-11-12 00:16:44 +01:00
parent b67852a5ff
commit 4ba60dad28
1 changed files with 23 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -938,13 +938,21 @@ namespace spot
bool seen = a->has_state(dest); bool seen = a->has_state(dest);
state_explicit_formula::transition* t = state_explicit_formula::transition* t =
a->create_transition(now, dest); a->create_transition(now, dest);
a->add_condition(t, dict_.bdd_to_formula(label)); t->condition = label;
if (!seen) if (!seen)
formulae_to_translate.insert(dest); formulae_to_translate.insert(dest);
else else
dest->destroy(); dest->destroy();
} }
} }
// Register all known propositions for a. This may contain
// proposition from other parts of the formula being translated,
// but this is not really important as this automaton will be
// short-lived. (Maybe it would even work without this line.)
dict_.dict->register_propositions(dict_.var_set, a);
//dotty_reachable(std::cerr, a); //dotty_reachable(std::cerr, a);
// The following code trims the automaton in a crude way by // The following code trims the automaton in a crude way by
@ -1808,12 +1816,17 @@ namespace spot
return f; return f;
} }
bdd used_vars()
{
return d_.var_set;
}
private: private:
// Map a representation of successors to a canonical formula. // Map a representation of successors to a canonical formula.
// We do this because many formulae (such as `aR(bRc)' and // We do this because many formulae (such as `aR(bRc)' and
// `aR(bRc).(bRc)') are equivalent, and are trivially identified // `aR(bRc).(bRc)') are equivalent, and are trivially identified
// by looking at the set of successors. // by looking at the set of successors.
typedef std::map<bdd, const formula*, bdd_less_than> bdd_to_formula_map; typedef Sgi::hash_map<bdd, const formula*, bdd_hash> bdd_to_formula_map;
bdd_to_formula_map b2f_; bdd_to_formula_map b2f_;
// Map each formula to its associated bdd. This speed things up when // Map each formula to its associated bdd. This speed things up when
// the same formula is translated several times, which especially // the same formula is translated several times, which especially
@ -2116,7 +2129,7 @@ namespace spot
formulae_to_translate.insert(constant::true_instance()); formulae_to_translate.insert(constant::true_instance());
state_explicit_formula::transition* t = state_explicit_formula::transition* t =
a->create_transition(now, constant::true_instance()); a->create_transition(now, constant::true_instance());
a->add_condition(t, d.bdd_to_formula(cond_for_true)); t->condition = cond_for_true;
} }
// Register other transitions. // Register other transitions.
for (i = dests.begin(); i != dests.end(); ++i) for (i = dests.begin(); i != dests.end(); ++i)
@ -2140,7 +2153,7 @@ namespace spot
continue; continue;
state_explicit_formula::transition* t = state_explicit_formula::transition* t =
a->create_transition(now, dest); a->create_transition(now, dest);
a->add_condition(t, d.bdd_to_formula(cond)); t->condition = cond;
d.conj_bdd_to_acc(a, j->first, t); d.conj_bdd_to_acc(a, j->first, t);
reachable = true; reachable = true;
} }
@ -2157,11 +2170,14 @@ namespace spot
} }
} }
if (!simplifier) dict->register_propositions(fc.used_vars(), a);
delete s;
// Turn all promises into real acceptance conditions. // Turn all promises into real acceptance conditions.
a->complement_all_acceptance_conditions(); a->complement_all_acceptance_conditions();
if (!simplifier)
// This should not be deleted before we have registered all propositions.
delete s;
return a; return a;
} }