Hi Alexandre, thank you very much for the quick response! The workaround seems to work perfectly, for both cases. Thanks for investigating the issue! Regards, Jens Kreber Am 10.04.20 um 10:23 schrieb Alexandre Duret-Lutz:
On Fri, Apr 10, 2020 at 9:26 AM Jens Kreber <kreber@react.uni-saarland.de> wrote:
I am using spot to check randomly generated LTL formulas for satisfiability and extract traces / words fulfilling the formula if satisfiable. I have come across behavior which I do not understand and am therefore asking on this list about it. I would be very happy if you could help me with the issue.
I'm using the python interface and call some_formula.translate().accepting_run()
which usually either returns None if unsatisfiable or a valid trace, which I then convert using spot.twa_word() and inspect afterwards. Most of the time, this works as expected, but I've experienced several cases now where the produced trace contains a False (0) literal. Here, two cases must be distinguished:
1. The formula is satisfiable There exist formulas like "!b & e U (a & b & c)" which are quite obviously satisfiable, but still accepting_run() returns a trace with 0 in it, although there are other valid traces without False in them.
2. The formula is unsatisfiable There also exist formulas like "X!c & X(b & c & d & a U e)" which are unsatisfiable, and accepting_run() returns a trace with 0 in it. Normally, for unsatisfiable formulas (like "a & !a") it just returns None. Hi Jens,
Thanks for the bug report. This seems to be the combination of three different bugs, and fixing any of them would make the issue disappear: 1) emptiness checks in Spot assume they are run on automata without false edges 2) an optimization, added in Spot 2.4, will rewrite "!b & e U (a & b & c)" as "!p0 & (p1 U p2)" before translation to reduce the number of variables, and then change the propositions of the resulting automaton back to their original form. For the translation procedure, !p0 & p2 is satisfiable, so it can output an edge with such a label, however after the final rewriting it becomes !b & (a & b & c) = false, and the edge is not removed. 3) the rewriting of "!b & e U (a & b & c)" to "!p0 & (p1 U p2)" [with p2=a&b&c] should not have occurred, I was expecting to get "!p0 & (p1 U (p0 & p2))" [with p2=a&c]
I'll try to fix those three issues ASAP.
As a temporary workaround, you can do
a = spot.translate("!b & e U (a & b & c)") a.merge_edges() # Add this, this should remove false edges. a.accepting_run()
Best regards -- Alexandre Duret-Lutz