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,
We are using the Python bindings in Spot to translate LTL to monitors, as
described at https://spot.lrde.epita.fr/tut11.html.
We have a question: Is it possible to set an option that will preserve all
the atomic propositions, even when they cannot affect the automaton? For
example, with the formula "Ga & Fb", the resulting monitor would not
include "b".
Is there a way to do this?
Thanks,
Dominick
Hi Alexandre,
Suppose one calls ltl2tgba with the option --check=stutter-invariant. Would it be possible to print a warning with diagnostics, like the online tool does? Something like:
Warning: The property is stutter-sensitive - the following words are a proof, as they differ only by some stuttering:
Accepted word: a & b; a & b; cycle{!a & !b}
Rejected word: a & b; cycle{!a & !b}
Motivation:
* by passing the option --check=stutter-invariant the user tells the tool that stutter-invariance is important for them, hence a warning/diagnostics is desirable if the check fails (this warning does not have to be printed if this option is not passed)
* it's not easy to get these traces from the final automaton - my understanding is that some potentially costly operations are required, which are performed during the check anyway
* the current way of getting this diagnostics (python + libraries; maybe there is a better way I don't know about?) creates many dependencies, thus making it difficult to integrate this functionality into toolchains - ideally one would want just a single executable ltl2tgba
* my (perhaps naive) understanding is that this is not difficult to implement and does not incur much extra run-time as the check has to be performed anyway
Best regards,
Victor.
