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
Dear Spot team,
Thanks for developing the nice tool Spot. I am a researcher at
National University of Singapore using Spot in my research.
I have a question about translating LTL to buechi automata using spot.
My LTL properties are constraints over input/output sequences of a program,
e.g.,
output W, output P always responds to input B
(false R (! iB | (true U (oW & X (true U oP)))))
where iB indicates that input B and oP indicates output P.
The buechi automata of the negation of above formula given by Spot is in
the following:
[image: image.png]
Here is a input/output trace to be evaluated:
iH oZ iH oR iC oR iH oX iC oR iH oX iD oZ iJ oT iD oT iF oR iH oP iH oR iH
oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH oR iH oP iH
*What I do not understand is that the proposition on the transition from
state 0 to state 2 is iB & oW. How can I interpret it?*
Given the input/output trace, there is no element that is iB and at the
same time is oW. I assume the verification feeds element in the trace to
the automata one by one.
Do I miss something e.g., wrong configuration on the translation or some
basic knowledge about verification? Can you give me some advice on this
issue?
Thank you very much.
Best regards
Zhen
--
Zhen Dong
Senior Research Fellow
National University of Singapore
https://www.comp.nus.edu.sg/~dongz/
