--sat-minimize should remove the sink state if -C is not used
This is confusing:
adl@couscous:~$ ltl2tgba a
HOA: v1
name: "a"
States: 2
Start: 1
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant terminal
--BODY--
State: 0 {0}
[t] 0
State: 1
[0] 0
--END--
adl@couscous:~$ ltl2tgba a | autfilt --sat-minimize
HOA: v1
States: 3
Start: 1
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0 {0}
[t] 0
State: 1
[0] 0
[!0] 2
State: 2
[t] 2
--END--
The 2-state automaton should not become a 3-state automaton once it is minimized, even if --sat-minimize
works with complete automata.
Let's remove the sink unless autfilt
is called with -C
. (ltl2tgba -x sat-minimize a
does it already.)