Skip to content

--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.)