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
> > Could you add a command-line option for ltl2tgba to invert the input
> formula before computing the automaton?
>
> Done.
> https://gitlab.lrde.epita.fr/spot/spot/commit/7f21d3ff29ad3a513f261025c5
> 75e4676a14cc50
Great - many thanks!
> Any opinion on what passing --negate twice should do?
A really good and nerdy one - twice the smiley face! :-) :-)
Cheers,
Victor.
Hi,
Could you add a command-line option for ltl2tgba to invert the input formula before computing the automaton?
Yes, it's trivial to do externally, but there are good reasons to have this option:
* this would remove an extra step from model checking toolchains (where the automaton is built for the negation of a formula)
* if the formula goes through a toolchain, it's better to keep equivalence all the way through to the automata, so that the user can easily see that the property has not been broken by transformations, and also comprehend any formula-related diagnostics logged by the tools.
Thanks,
Victor.
Dear Spot developers,
I am Yong Li from Chinese Academy of Sciences and I am writing to you to
ask a question about parsing LTLf (LTL over finite traces) formulas.
Spot supports LTL with finite semantics (LTLf) but I found out that Spot
eagerly simplifies the input formulas with LTL semantics.
For instance, if I use command line ltlfilt --from-ltlf -f "a U !(X
True)", Spot immediately gives me 0.
This is not correct since the input formula should be satisfiable in
LTLf semantics.
I wonder whether there is a way to get around it?
Is there a an option I can use to make Spot parse the formula without
simplying it?
Regards,
Yong
