21 Nov
2019
21 Nov
'19
3:40 p.m.
On Thu, Nov 21, 2019, 4:34 AM Alexandre Duret-Lutz <adl(a)lrde.epita.fr> wrote:
On Thu, Nov 21, 2019 at 4:59 AM Dominick Pastore
<dpastore(a)seas.upenn.edu> wrote:
I apologize for the ambiguity. (1) is indeed what we wanted, and this
is perfect. Thank you very much!
Dominick
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?
Hi Dominick,
The monitor for Ga & Fb is one self-loop labeled by a, since Fb is not
monitorable. I'm not sure what you mean by "preserve the atomic
propositions". Do you want
(1) to list "b" has part of the atomic propositions registered for the
automaton (i.e., just the output of aut.ap()), or
(2) to split the edge labeled by the Boolean formula "a" as two
separate edges labeled by "a&!b" and "a&b"?
In any case, (1) is necessary for (2). Attached document shows how to do both.
--
Alexandre Duret-Lutz