Dear spot team,
It seems like there is a bug in the current version of spot, that occurs under certain combinations of multiple initial states and states without any successors.
In the example below, the automaton is clearly not empty, yet autfilt claims it is (tested with versions 2.14.1 and 2.12)
$ cat foo.hoa
HOA: v1
States: 3
Start: 1
Start: 2
AP: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[(t)] 0
State: 1
[(t)] 0
State: 2
--END--
$ autfilt --is-empty foo.hoa
HOA: v1
States: 3
Start: 2
AP: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0 {0}
[t] 0
State: 1
State: 2
--END--
If I add some useless self-loop to state 2, or remove state 2 from the list of initial states, autfilt’s output is correct again.
This seems very similar to a bug I reported a while ago (28.06.2024), not sure if this helps.
FYI: the bug was found while using AutoHyper, leading to erroneous model-checking results. In AutoHyper, automata of the above form (multiple initial states and states without outgoing edges) occur quite frequently.
Thanks,
Raven
