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
