12 Dec
2022
12 Dec
'22
6:24 p.m.
"Pert, Charles" <c.pert22(a)imperial.ac.uk> writes:
I am specifically trying to generate unsatisfiable LTL
formulae using
the randltl tool in Spot. I am struggling because the default tool is
so much more likely to produce consistent and satisfiable formulae.
Have you got any tips on how I can alter the generation to produce
these types of formulae?
Hi Charles,
I'm not surprised that random formulas are very often satisfiable. With
the current state of the tool, I don't know how to build unsatisfiable
formulas more efficiently.
However https://gitlab.lre.epita.fr/spot/spot/-/issues/400 links to a
paper where they build their benchmark by doing conjunctions of known
patterns, and claim to have 50% of unsatisfiable cases. This is a
feature we would like to have at some point, but unfortunately not very
high priority at the moment.
Alexandre