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
Hi all,
Do you know any tools that can convert universal co-buchi automata into
universal safety automata via bounding the number of visits to the final
states?
(I.e., go to absorbing bad state if visit a final state k times)
(Alternatively, convert NBW into nondet finite automaton: accept a word if
it visits a final state k times)
(I am just trying to avoid work that may have already be done:)
Thanks,
Ayrat
hi,
Is there a way to get more than one accepting run of the product automaton?
Ideally would be to have all simple accepting runs,
but some cheap heuristics would also do.
I wanted to implement some heuristics [1], but got stuck with the following:
how to map edges of the accepting run to the edges of the original product?
(or: states of the accepting run to states of the product?)
thanks!:)
ayrat
[1]
An heuristics:
- get an accepting run,
- forbid one edge of that run in the original product (for example, by
setting its label to bddfalse),
- ask for another accepting run on the thus modified product,
- restore that edge and change another edge,
and so on.
Hello dear spot devs,
I need to know which construction is used when I'm translating an LTL
formula into a monitor automaton. By that I mean:
/spot::formula some_ltl;
spot::translator trans;/
/trans.set_type(spot::postprocessor::Monitor)
spot::const_twa_graph_ptr aut = trans.run(some_ltl)/
I couldn't find documentation about this, besides some rather informal
description.
It would be great if you could point me to some more useful
documentation about the algorithm or even better a paper on it.
Best,
Marvin Stenger
