"Too many acceptance sets used." when called with `--medium`, but works with `--high` or with version 2.11.6
hi Alexandre,
Ruediger discovered another problematic formula with his fuzz tester. On version 35fca490 from Nov 14:
./ltl2tgba --medium --colored-parity="min even" -D -C -f "(((~(( G v1) & X ( F v5 & ~( G F v13 | v9))) U v3))& ((v1 | G v11))) -> ( F G (~ F G ( G F ~v5 & v1) & ( F v15 | ( F G ~ v15 | v13))))"
./ltl2tgba: Too many acceptance sets used. The limit is 32.
(Ruediger says even 1024 is not enough)
With --high
it works:
/ltl2tgba --high --colored-parity="min even" -D -C -f "(((~(( G v1) & X ( F v5 & ~( G F v13 | v9))) U v3))& ((v1 | G v11))) -> ( F G (~ F G ( G F ~v5 & v1) & ( F v15 | ( F G ~ v15 | v13))))"
HOA: v1
name: "((Gv1 & X(!v9 & Fv5 & FG!v13)) R !v3) | (!v1 & F!v11) | GF(!v1 | Gv5)"
States: 18
Start: 0
AP: 6 "v1" "v11" "v3" "v9" "v5" "v13"
acc-name: parity min even 3
[clipped]
This a newly introduced problem: the last released version 2.11.6
handles that formula fine with --medium
and also with --high
. Thanks.