Deterministic Automata for the same LTL property have different languages when using "--medium"
It looks like using "--medium" changes the languages of the deterministic automata for some LTL properties (when using "ltl2tgba").
The command
/path/to/spot-2.11.6.dev/bin$ ./ltl2tgba --medium --colored-parity="min even" -D -C --hoaf=t -f "(~ v1 U ~ v5) | G(F v9 & F G v1) | G F(~ v7 | G v7 | G v3)"
yields the following automaton:
HOA: v1
name: "(!v1 U !v5) | G(Fv9 & FGv1) | GF(!v7 | Gv7 | Gv3)"
States: 3
Start: 1
AP: 2 "v1" "v5"
acc-name: parity min even 2
Acceptance: 2 Inf(0) | Fin(1)
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0
[t] 0 {0}
State: 1
[!1] 0 {1}
[!0&1] 1 {1}
[0&1] 2 {1}
State: 2
[t] 2 {1}
--END--
while when running with full optimization:
/path/to/spot-2.11.6.dev/bin$ ./ltl2tgba --colored-parity="min even" -D -C --hoaf=t -f "(~ v1 U ~ v5) | G(F v9 & F G v1) | G F(~ v7 | G v7 | G v3)" -d > /tmp/small.dot
I am getting an automaton for the universal language.
Unless I am mistaken, the latter is correct. This was tried on a clean install using the version obtained with https://gitlab.lre.epita.fr/spot/spot/-/jobs/artifacts/next/download?job=make-dist on the 4th of November at 9pm. Thanks for the script for compiling the latest spot version easily - seems to work very well!