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,
If I have a deterministic automata and an LTL or python function which gets
a word and return T/F.
Is it possible to set model checking for the dfa? to get a counterexample
which distinguishes the dfa and the LTL/ python target function?
Regards,
Phillip
HI,
My name is Roei Nahum. I recently got to know SPOT, and first of all, I want to thank you for this great platform. I'm having an issue and I'll appreciate if you can assist.
I use SPOT in order to translate temporal formulas into automata. To do so, I downloaded spot, and wrote a C++ program based on SPOT API.
The program I wrote is basically like this:
...get the formula...
spot::parsed_formula cex_pf = spot::parse_infix_psl(formula);
if(cex_pf.format_errors(std::cerr)){
cout << "Invalid formula syntax: " << formula << endl;
exit(1)
}
spot::translator trans;
trans.set_type(spot::postprocessor::BA);
trans.set_pref(spot::postprocessor::Small);
twa_graph_ptr aut = trans.run(cex_pf.f);
...print the automata...
I tried running this code on several formulas, and it works great.
The problems started when I processed this formula:
G({(a)} |=> {(b)[*32]})
The code is running for a long time (more than a hour) without giving a result.
Did it get stuck? Is there any way I can make it work?
Thanks,
Roei Nahum
