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
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
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
