
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