September 2018 - 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

Potential Bug in Spot?
by Andreas Tollkötter 25 Sep '18

25 Sep '18

Hello, with the currently newest version of Spot 2.6.1, the following behavior occurred for me, which I would call a bug. I attached a DOT file of a deterministic parity automaton which was written by "autfilt --dot --highlight-languages". What is notable that (among other pairs), states 10 and 66 are marked as language-equivalent states. Their "a1"-successors, 30 and 62 are not equivalent however, so something must be wrong here. I assume a potential cause is that there are a total of 18 non-trivial equivalence classes but only 16 different colors defined to be used by Spot, so some are used for multiple classes? If that is the case, I feel like there should be at least a warning output by "autfilt" when this happens. Best regards, Andreas Tollkötter

2 1

ltlfilt does not exhaustively simplify when --remove-wm is enabled
by Simon Jantsch 23 Sep '18

23 Sep '18

Hello, I am confused by the fact that the following two commands do not produce the same result: ltlfilt --simplify=3 --remove-wm --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“ ltlfilt --simplify=3 --remove-wm --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“ | ltlfilt --lbt --lbt-input --simplify=3 The first command gives the same formula as: ltlfilt --simplify=3 --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“ | ltlfilt --lbt --lbt-input --remove-wm which makes me believe that simplification is done before removing the operators M and W. I would expect ltlfilt to first remove the operators and then simplify exhaustively. Is this behavior intended and if it is, what is the best way to get an exhaustively simplified formula without certain operators? Best regards, Simon

2 1