simulation missed reduction
The following picture, stolen from @jdubois' internship report, suggests that current the implementation of the "don't care reduction for trivial SCCs" could be improved.
However I'm not able to reproduce it from the picture:
import spot
aut = spot.automaton("""HOA: v1
States: 9
Start: 0
AP: 4 "p0" "p1" "p2" "p3"
Acceptance: 2 Fin(0)&Fin(1)
Alias: @p 0&1&!2&3
--BODY--
State: 0
[@p] 1 {0 1}
[@p] 2 {0 1}
State: 1
[@p] 2 {0 1}
State: 2
[@p] 2
[@p] 3 {0}
[@p] 4 {1}
State: 3
[@p] 5 {0 1}
[@p] 6 {0}
State: 4
[@p] 7 {0 1}
[@p] 8 {1}
State: 5
[@p] 8 {0 1}
State: 6
[@p] 2 {0}
[@p] 4 {0 1}
State: 7
[@p] 6 {0 1}
State: 8
[@p] 2 {1}
[@p] 3 {0 1}
--END--""")
aut = spot.simulation(aut)
print(aut.to_str())
outputs
HOA: v1
States: 1
Start: 0
AP: 4 "p0" "p1" "p2" "p3"
Acceptance: 2 Fin(0) & Fin(1)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[0&1&!2&3] 0
--END--
@jdubois any hint?