Skip to content

remove_fin should not return f

Since f is encoded in Spot as Fin({}), it's a bit dubious to ever consider it as Fin-less. Remove fin should never return such an acceptance as in:

% ltl2tgba false | sed 's/0 t/1 Fin(0)/' | autfilt --remove-fin
HOA: v1
States: 1
Start: 0
AP: 0
acc-name: none
Acceptance: 0 f
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant terminal
--BODY--
State: 0
--END--

In this case, returning Acceptance 0 t would be better.