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

wdba_minimization: make the reverse check first

Browse source 
* spot/twaalgos/minimize.cc (minimize_obligation): When
needed (i.e. in the non-deterministic case), make the reverse check
before the forward check, because it does not require translating the
negated formula.
This commit is contained in:
Alexandre Duret-Lutz 2017-11-15 15:06:13 +01:00
parent f0735d4d86
commit 18b4566762
1 changed files with 17 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

31
spot/twaalgos/minimize.cc
View file

@ -603,7 +603,7 @@ namespace spot
// If the input automaton was already weak and deterministic, the // If the input automaton was already weak and deterministic, the
// output is necessary correct. // output is necessary correct.
if (aut_f->prop_weak() && aut_f->prop_universal()) if (aut_f->prop_weak() && is_deterministic(aut_f))
return min_aut_f; return min_aut_f;
// if f is a syntactic obligation formula, the WDBA minimization // if f is a syntactic obligation formula, the WDBA minimization
@ -616,6 +616,17 @@ namespace spot
if (is_terminal_automaton(aut_f)) if (is_terminal_automaton(aut_f))
return min_aut_f; return min_aut_f;
// If the input was deterministic, then by construction
// min_aut_f accepts at least all the words of aut_f, so we do
// not need the reverse check. Otherwise, complement the
// minimized WDBA to test the reverse inclusion.
// (remove_fin() has a special handling of weak automata, and
// dualize also has a special handling of deterministic
// automata, so all these steps are quite efficient.)
if (!is_deterministic(aut_f)
&& !product(aut_f, remove_fin(dualize(min_aut_f)))->is_empty())
return std::const_pointer_cast<twa_graph>(aut_f);
// Build negation automaton if not supplied. // Build negation automaton if not supplied.
if (!aut_neg_f) if (!aut_neg_f)
{ {
@ -645,26 +656,16 @@ namespace spot
if (is_terminal_automaton(aut_neg_f)) if (is_terminal_automaton(aut_neg_f))
return min_aut_f; return min_aut_f;
bool ok = false;
// Make sure the minimized WDBA does not accept more words than // Make sure the minimized WDBA does not accept more words than
// the input. // the input.
if (product(min_aut_f, aut_neg_f)->is_empty()) if (product(min_aut_f, aut_neg_f)->is_empty())
{ {
assert((bool)min_aut_f->prop_weak()); assert((bool)min_aut_f->prop_weak());
// If the input was deterministic, then by construction
// min_aut_f accepts at least all the words of aut_f, so we do
// not need the reverse check. Otherwise, complement the
// minimized WDBA to test the reverse inclusion.
// (remove_fin() has a special handling of weak automata, and
// dualize also has a special handling of deterministic
// automata, so all these steps are quite efficient.)
ok = is_deterministic(aut_f)
|| product(aut_f, remove_fin(dualize(min_aut_f)))->is_empty();
}
if (ok)
return min_aut_f; return min_aut_f;
}
else
{
return std::const_pointer_cast<twa_graph>(aut_f); return std::const_pointer_cast<twa_graph>(aut_f);
} }
} }
}