a case where propagation would improve determinization
The first two of the following three equivalent automata came up in https://gitlab.lrde.epita.fr/spot/spot/-/commit/792aaca0ba0c77cb305f4a3267afee5c72d24404#note_19768
HOA: v1 States: 2 Start: 0 AP: 1 "p0" Acceptance: 1 Inf(0)
--BODY-- State: 0 [0] 1 State: 1 [0] 0 {0} [t] 1 --END--
HOA: v1 States: 2 Start: 0 AP: 1 "p0" Acceptance: 1 Inf(0)
--BODY-- State: 0 [0] 1 {0} State: 1 [0] 0 [t] 1 --END--
HOA: v1 States: 2 Start: 0 AP: 1 "p0" Acceptance: 1 Inf(0)
--BODY-- State: 0 [0] 1 {0} State: 1 [0] 0 {0} [t] 1 --END--
The first one is obtained by applying the BDD-based simulation reduction on genaut --m-nba=1
. The second one is obtained by applying @jdubois' matrix-based faster simulation on genaut --m-nba=1
. The last one was handcrafted as a combination of both. All these automata have the same structure, and differ only by the location of the acceptance mark. However after they are determinimized and reduced by the BDD-based simulation, we get different output:
I suspect that it should be in tgba_determinize()
's interest to have propagate_marks_here()
called first, however I have fuzzy memories of trying to use propagate_marks_vector()
and that it wasn't a clear improvement. (Currently the degeneralization is built in tgba_determinize()
and propagate_marks_here()
should be called afterwards, so it will have to be done inside tgba_determinize()
.)