Commit 098e121a authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Ignore sub-"SERE" that have been proved useless already.

* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate): Do not
translate a subformula if we have already proved it useless in
a previous rational expression.
* src/tgbatest/ltl2tgba.test: Add an example, although that
test does not ensure the subformula is ignored early in the
translation.  I.e., it would still work without the patch.
parent b6702fc2
......@@ -935,6 +935,14 @@ namespace spot
const formula* dest =
dict_.bdd_to_formula(bdd_exist(res & label, dict_.var_set));
f2a_t::const_iterator i = f2a_.find(dest);
if (i != f2a_.end() && i->second == 0)
{
// This state is useless. Ignore it.
dest->destroy();
continue;
}
bool seen = a->has_state(dest);
state_explicit_formula::transition* t =
a->create_transition(now, dest);
......
......@@ -103,6 +103,10 @@ check_psl '{[*]; start && comp_data_en; !comp_data_en && good_comp;
# before it is used in the translation.
check_psl '{{b[*];c} | {{a && !a}}[=2]}'
check_psl '{((a&!b);((!a&!b)*))&&(!b*;(!a&b))}'
# When translating this formula, we expect the translator to ignore
# `a;(f&!f)[=2];c' on one side because it as already seen it on the
# other side.
check_psl '{c;a;(f&!f)[=2];c}|{b;a;(!f&f)[=2];c}'
# Make sure 'a U (b U c)' has 3 states and 6 transitions,
# before and after degeneralization.
......
Supports Markdown
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