sbacc suboptimal construction
The following behavior, extracted from some benchmark made by Jérôme Dubois, looks like a bug to me:
a = spot.automaton("""HOA: v1
States: 2
Start: 0
AP: 12 "p1" "p2" "p3" "p4" "p5" "a" "b" "c" "d" "e" "f" "g"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[5] 0 {0}
[6] 1
State: 1
[6] 1 {0}
--END--""")
It looks like output state 0
corresponds to (0,{})
, and that output state 1
corresponds to (0,{0})
. However sbacc()
was free to start in (0,{0})
, and I believe it has some code for this purpose. Why is this not working?