21 Nov
2019
21 Nov
'19
4:59 a.m.
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
21 Nov
21 Nov
10:34 a.m.
On Thu, Nov 21, 2019 at 4:59 AM Dominick Pastore
<dpastore(a)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
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
1903
days inactive
1903
days old
2 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Dominick Pastore