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'd like to thank the developers for the awesome Spot's online LTL
toolset! It's helping me a lot with my model checking project with Spin.
This is exactly how formal methods should look like in the 2020'ies...
If I may be so bold to request a feature, would it be possible to encode
the input formula into URL, so that I could share a link with my fellow
students?
Best regards,
John Lång
Hi there,
In a preprocessing step, I want to flush a few states from a TωA. The one
method that seems to be available is defrag_states, the description of
which having the expected semantics.
However, after defrag, it sometimes happens that the dst of some
transitions points to delete states (-1U). The code of defrag_states in
graph.hh removes the outgoing transitions of deleted states but does not
seem to flush the transitions *pointing to* deleted states—is this the
expected behavior?
Cheers,
M.
