10 Dec
2022
10 Dec
'22
9 a.m.
Hi,
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?
Best wishes,
Charles Pert
12 Dec
12 Dec
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
932
days inactive
934
days old
1 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Pert, Charles