30 Dec
2022
30 Dec
'22
12:27 p.m.
Dear spot Team,
I think I have found a bug in the emptiness checker of spot.
When I use the following automation:
HOA: v1
States: 8
Start: 0
Start: 1
AP: 0
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
--BODY--
State: 0 {0}
[(t)] 2
[(t)] 3
State: 1 {0}
[(t)] 4
[(t)] 5
State: 2 {0}
[(t)] 2
[(t)] 3
State: 3 {0}
[(t)] 6
[(t)] 7
State: 4 {1}
[(t)] 4
[(t)] 5
State: 5 {1}
[(t)] 6
[(t)] 7
State: 6
[(t)] 6
[(t)] 7
State: 7
[(t)] 6
[(t)] 7
--END--
And invoke "autfilt --is-empty aut.hoa” (where aut.hoa contains the above automaton)
I get the following error:
autfilt: print_hoa(): automaton has transition-based acceptance despite
prop_state_acc()==true
This seems to be related to a similar bug that was fixed in version 2.7.1, so should
(hopefully) be easy to fix.
I used version 2.11.3 on a MacBook Pro with M1 Pro CPU.
All the best,
Raven