accepting_run() returning words containing false
Hello, 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. I'd find point 2 alone totally okay, but I think point 1 is actually problematic since the trace I'm looking for exists, but isn't returned. So my question is whether I'm using spot incorrectly somehow or if this is actually a bug. I also attached a small list of formulas and traces with the described behavior. BTW I'm on Linux, Ubuntu 16.04, using spot 2.8.7 compiled from the tar.gz. I'm looking forward to your responses! Regards, Jens Kreber
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
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
participants (2)
-
Alexandre Duret-Lutz -
Jens Kreber