November 2019 - Spot

Walking through BDD formula in python
by Ayrat Khalimov 26 May '21

26 May '21

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

2 5

Keep all APs when translating LTL?
by Dominick Pastore 21 Nov '19

21 Nov '19

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

2 2

ltl2tgba: diagnostics for stutter-sensitive properties
by Victor Khomenko 21 Nov '19

21 Nov '19

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.

2 1