10 Apr
2020
10 Apr
'20
10:23 a.m.
On Fri, Apr 10, 2020 at 9:26 AM Jens Kreber
<kreber(a)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