add a quick simplification pass before LTL relabeling
The following command is instantaneous:
genltl --and-fg=32 | ltlfilt -r1 | ltl2tgba -G -D
genltl --and-fg=32 | ltl2tgba -G -D
takes ages (I'm not even trying to wait for the result).
The reason is that
ltl2tgba performs Boolean sub-formulas rewriting before LTL simplifications.
The input formula
FGp1 & FGp2 & ... & FGp32 has no Boolean subformula that are "rewrite-worthy", while the simplified formula
FG(p1 & p2 & ... & p32) can be rewritten as a single
FG(p). Note that using
ltlfilt -r3 would be slow because this involves translations. We should probably use a quick simplification pass before LTL relabeling, at least when the number of AP seems large.