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
