add a quick simplification pass before LTL relabeling
The following command is instantaneous:
genltl --and-fg=32 | ltlfilt -r1 | ltl2tgba -G -D
However using
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.