Skip to content

"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.