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
On Thu, Nov 21, 2019 at 4:59 AM Dominick Pastore dpastore@seas.upenn.edu wrote:
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.
On Thu, Nov 21, 2019, 4:34 AM Alexandre Duret-Lutz adl@lrde.epita.fr wrote:
On Thu, Nov 21, 2019 at 4:59 AM Dominick Pastore dpastore@seas.upenn.edu wrote:
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
I apologize for the ambiguity. (1) is indeed what we wanted, and this is perfect. Thank you very much!
Dominick
-
Alexandre Duret-Lutz -
Dominick Pastore