April 2020 - Spot

Walking through BDD formula in python
by Ayrat Khalimov 26 May '21

26 May '21

hi! With the aid of SPOT I am developing a counter-example guided synthesizer in python. See [1] if interested for details. My question is: I am trying to parse twa_run in python, namely, parse the labels of the each step (`spot.impl.step`). Is there a python way to walk through BDD? (The label is a simple cube expressed in BDD, and I need to convert it into my internal structure) (yes, this is rather a question about python interface for buddy) (no, that is not feature request:) if not possible, I will simply print the label and parse the string, that is not crucial) [1] The idea is - guess the model, - then model check it and get a counter-example - then encode the counter-example into the "guesser" (which uses an SMT solver) thanks, Ayrat

2 5

Segfault when postprocessing large automaton
by Reed Oei 20 Apr '20

20 Apr '20

Hello, I am encountering a bug where Spot segfaults when I try to postprocess a relatively large automaton. I have uploaded the file to http://reedoei.com/files/smaller-inner.aut.zip; it has 113930 states and 1537155 edges. I tried to come up with a smaller example but was having trouble doing so. Below is the sequence of commands, using the Python bindings, to reproduce this bug for me: import spot A = spot.automaton('smaller-inner.aut') B = A.postprocess('BA', 'Deterministic', 'Low') # Crashes here B.save('postprocessed.aut') I also tried using various other others for postprocess such as Small and Low, or Any and High (because Any and Low/Medium does nothing). I am using Ubuntu 18.04, Python 3.6.9, and Spot 2.8.7 (but also tried with 2.8.6). Thank you, Reed Oei

2 3

accepting_run() returning words containing false
by Jens Kreber 10 Apr '20

10 Apr '20

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

2 2