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

minimize: t acceptance is compatible with wdba-minimization

Browse source 
* spot/twaalgos/minimize.cc (minimize_obligation_garanteed_to_work):
Skip some tests when the acceptance is "t".
* tests/core/det.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2024-03-22 16:08:32 +01:00
parent 7e228e86ee
commit 26a62c8b68
2 changed files with 22 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

24
spot/twaalgos/minimize.cc
View file

@ -611,11 +611,25 @@ namespace spot
formula f)
{
// WDBA-minimization necessarily work for obligations
return ((f && f.is_syntactic_obligation())
// Weak deterministic automata are obligations
|| (aut_f->prop_weak().is_true() && is_deterministic(aut_f))
// Guarantee automata are obligations as well.
|| is_terminal_automaton(aut_f));
if (f && f.is_syntactic_obligation())
return true;
// we can minimize automata with t acceptance
if (aut_f->acc().is_t())
return true;
if (aut_f->prop_weak().is_false())
return false;
// Weak deterministic automata are obligations
if (aut_f->prop_weak().is_true() && is_deterministic(aut_f))
return true;
scc_info si(aut_f);
check_strength(std::const_pointer_cast<twa_graph>(aut_f), &si);
// Check again, now that the strength is known
if (aut_f->prop_weak().is_true() && is_deterministic(aut_f))
return true;
// Guarantee automata are obligations as well.
if (is_terminal_automaton(aut_f, &si))
return true;
return false;
}
twa_graph_ptr

6
tests/core/det.test
View file

@ -149,7 +149,7 @@ AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc !complete
properties: !deterministic exist-branch
properties: !deterministic exist-branch very-weak
spot.highlight.states: 0 1
spot.highlight.edges: 1 2 2 2
--BODY--
@ -174,7 +174,7 @@ AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc !complete
properties: !deterministic exist-branch
properties: !deterministic exist-branch very-weak
spot.highlight.states: 1 1
--BODY--
State: 0 {0}
@ -198,7 +198,7 @@ AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc !complete
properties: !deterministic exist-branch
properties: !deterministic exist-branch very-weak
spot.highlight.states: 1 5
spot.highlight.edges: 2 5 3 5
--BODY--