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

Use tgba_explicit_formula instead of tgba_explicit_string in FM.

Browse source 
This gives a nice speedup (>1.4) in the ltlcounter benchmark,
because we no longer have to generate a copy the string
representations of the LTL formulae.

* src/tgbaalgos/ltl2tgba_fm.cc: Adjust.  Also get rid of the
formulae_seen map, since we can now ask the tgba_explicit_formula
if it knows the state.
This commit is contained in:
Alexandre Duret-Lutz 2009-11-10 16:57:08 +01:00
parent 32a4647d03
commit 007e2bd0b9
2 changed files with 30 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

12
ChangeLog
View file

@ -1,3 +1,15 @@
2009-11-10 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Use tgba_explicit_formula instead of tgba_explicit_string in FM.
This gives a nice speedup (>1.4) in the ltlcounter benchmark,
because we no longer have to generate a copy the string
representations of the LTL formulae.
* src/tgbaalgos/ltl2tgba_fm.cc: Adjust. Also get rid of the
formulae_seen map, since we can now ask the tgba_explicit_formula
if it knows the state.
2009-11-10 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2009-11-10 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Ease debugging of LTL formulae leaks. Ease debugging of LTL formulae leaks.

47
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -195,7 +195,7 @@ namespace spot
} }
void void
conj_bdd_to_acc(tgba_explicit_string* a, bdd b, conj_bdd_to_acc(tgba_explicit_formula* a, bdd b,
tgba_explicit::transition* t) tgba_explicit::transition* t)
{ {
assert(b != bddfalse); assert(b != bddfalse);
@ -717,7 +717,6 @@ namespace spot
} }
typedef std::set<const formula*, formula_ptr_less_than> set_type; typedef std::set<const formula*, formula_ptr_less_than> set_type;
set_type formulae_seen;
set_type formulae_to_translate; set_type formulae_to_translate;
translate_dict d(dict); translate_dict d(dict);
@ -773,32 +772,29 @@ namespace spot
} }
bdd all_events = observable_events | unobservable_events; bdd all_events = observable_events | unobservable_events;
formulae_seen.insert(f2);
tgba_explicit_formula* a = new tgba_explicit_formula(dict);
formulae_to_translate.insert(f2); formulae_to_translate.insert(f2);
a->set_init_state(f2);
tgba_explicit_string* a = new tgba_explicit_string(dict);
a->set_init_state(to_string(f2));
while (!formulae_to_translate.empty()) while (!formulae_to_translate.empty())
{ {
// Pick one formula. // Pick one formula.
const formula* f = *formulae_to_translate.begin(); const formula* now = *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.
bdd res = fc.translate(f); bdd res = fc.translate(now);
// Handle exclusive events. // Handle exclusive events.
if (unobs) if (unobs)
{ {
res &= observable_events; res &= observable_events;
int n = d.register_next_variable(f); int n = d.register_next_variable(now);
res |= unobservable_events & bdd_ithvar(n) & all_promises; res |= unobservable_events & bdd_ithvar(n) & all_promises;
} }
std::string now = to_string(f);
// We used to factor only Next and A variables while computing // We used to factor only Next and A variables while computing
// prime implicants, with // prime implicants, with
// minato_isop isop(res, d.next_set & d.a_set); // minato_isop isop(res, d.next_set & d.a_set);
@ -940,8 +936,10 @@ namespace spot
assert(fair_loop_approx || j->first == bddtrue); assert(fair_loop_approx || j->first == bddtrue);
cond_for_true = j->second; cond_for_true = j->second;
} }
if (!a->has_state(constant::true_instance()))
formulae_to_translate.insert(constant::true_instance());
tgba_explicit::transition* t = tgba_explicit::transition* t =
a->create_transition(now, constant::true_instance()->val_name()); a->create_transition(now, constant::true_instance());
a->add_condition(t, d.bdd_to_formula(cond_for_true)); a->add_condition(t, d.bdd_to_formula(cond_for_true));
} }
// Register other transitions. // Register other transitions.
@ -953,9 +951,11 @@ namespace spot
// whether a formula is actually reachable. // whether a formula is actually reachable.
bool reachable = false; bool reachable = false;
// Will this be a new state?
bool seen = a->has_state(dest);
if (dest != constant::true_instance()) if (dest != constant::true_instance())
{ {
std::string next = to_string(dest);
for (prom_map::const_iterator j = i->second.begin(); for (prom_map::const_iterator j = i->second.begin();
j != i->second.end(); ++j) j != i->second.end(); ++j)
{ {
@ -963,7 +963,7 @@ namespace spot
if (cond == bddfalse) // Skip false transitions. if (cond == bddfalse) // Skip false transitions.
continue; continue;
tgba_explicit::transition* t = tgba_explicit::transition* t =
a->create_transition(now, next); a->create_transition(now, dest);
a->add_condition(t, d.bdd_to_formula(cond)); a->add_condition(t, d.bdd_to_formula(cond));
d.conj_bdd_to_acc(a, j->first, t); d.conj_bdd_to_acc(a, j->first, t);
reachable = true; reachable = true;
@ -974,24 +974,13 @@ namespace spot
// "1" is reachable. // "1" is reachable.
reachable = true; reachable = true;
} }
if (reachable if (reachable && !seen)
&& formulae_seen.find(dest) == formulae_seen.end()) formulae_to_translate.insert(dest);
{
formulae_seen.insert(dest);
formulae_to_translate.insert(dest);
}
else else
{ dest->destroy();
dest->destroy();
}
} }
} }
// Free all formulae.
for (std::set<const formula*>::iterator i = formulae_seen.begin();
i != formulae_seen.end(); ++i)
(*i)->destroy();
// Turn all promises into real acceptance conditions. // Turn all promises into real acceptance conditions.
a->complement_all_acceptance_conditions(); a->complement_all_acceptance_conditions();
return a; return a;