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

* src/tgbaalgos/compsusp.cc: Ignore useless suspendable subformulae.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2014-04-06 08:26:10 +02:00
parent 92eed08261
commit 2c36ef54c0
1 changed files with 11 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/tgbaalgos/compsusp.cc
View file

@ -387,13 +387,19 @@ namespace spot
res = sim; res = sim;
} }
// Create a map of suspended formulae to BDD variables.
spot::formula_bdd_map susp; spot::formula_bdd_map susp;
ltl_suspender_visitor::fmap_t::const_iterator it; for (auto& it: g2s)
for (it = g2s.begin(); it != g2s.end(); ++it)
{ {
bdd_dict::fv_map::const_iterator j = dict->var_map.find(it->first); auto j = dict->var_map.find(it.first);
assert(j != dict->var_map.end()); // If no BDD variable of this suspended formula exist in the
susp[it->second] = bdd_ithvar(j->second); // BDD dict, it means the suspended subformulae was never
// actually used in the automaton. Just skip it. FIXME: It
// would be better if we had a way to check that the variable
// is used in this automaton, and not in some automaton
// (sharing the same dictionary.)
if (j != dict->var_map.end())
susp[it.second] = bdd_ithvar(j->second);
} }
// Remove suspendable formulae from non-accepting SCCs. // Remove suspendable formulae from non-accepting SCCs.