relabeling Boolean subformulas despite overlaping atomic propositions
Yann Thierry-Mieg reports that before using ltl2tgba
in the Model-Checking Contest (MCC), he relabels all Boolean subformulas using fresh atomic propositions. Once he has the automaton build by ltl2tgba
, he simply performs the opposite relabeling. Doing so might create "false" edges that he ignores.
This procedure is very similar to the relabeling job that is already done in spot::translator
when there are more that 4 atomic propositions. However the difference is that Spot uses relabel_bse()
instead, and this does not relabel subformulas that have an overlapping set of atomic propositions.
It turns out that the MCC formulas are randomly generated, use many atomic propositions, and Boolean formula usually overlap. It might make sense to implement this more aggressive relabeling in spot::translator
when the first one still produce a lot of atomic propositions.
Attached is a list of 16 examples provided by Yann in his email. It seems that even parsing the first formula takes a while, so maybe we have other optimizations opportunities in the parser. However the file contains some weird inputs, with some ?
characters that I do not understand, and the last 8 formulas seem very small.