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