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!
I know Spot doesn't provide much support for LTLf (LTL with finite trace
semantics) but I need to simplify some LTLf formulas. I was wondering which
tl_simplifier_options, if any, would simplify according to the semantics of
LTLf, i.e reduce_basics, synt_impl, etc. I know that using all the
rewritings wouldn't work since many of them only apply to LTL and not LTLf
but I'd like to use any rewritings that do apply to LTLf. Would anyone be
able to point me in the right direction? Alternatively do you know of
another software package that might do LTLf simplification?
Thanks!
Homer
