24 Sep
2020
24 Sep
'20
9:44 a.m.
Dear Zhen,
On Thu, Sep 24, 2020 at 8:58 AM Zhen Dong <zhen.dong(a)comp.nus.edu.sg> wrote:
What I do not understand is that the proposition on
the transition from state 0 to state 2 is iB & oW. How can I interpret it?
Spot uses LTL over atomic propositions, not letters.
It thinks of iH, oZ, iH, oR, etc. as electric signals, or system
properties, but not letters. At each step of the execution of the
system, each signal is either true or false: they are not mutually
exclusive. The iB&oW transition should be used when both signals are
true.
In the case where you want iH, oZ, iH, oR, etc. to be interpreted as
mutually exclusive events, you could encode this constraint into the
formula. Spot has some tools to automate this, although it requires
some manual work:
1. Add the mutually exclusive constraint to the formula:
% ltlfilt -f '(0 R(!iB|(1 U (oW&X(1 U oP)))))' --exclusive-ap=iB,oW,oP
(0 R(!iB|(1 U (oW&X(1 U oP)))))&G(!(iB&oW)&!(iB&oP)&!(oP&oW))
2. Convert it into Büchi, and then (optionally) simplify the labels of
the resulting automaton by removing unnecessary checks.
% ltl2tgba -B '(0 R(!iB|(1 U (oW&X(1 U
oP)))))&G(!(iB&oW)&!(iB&oP)&!(oP&oW))' |
autfilt -B --exclusive-ap=iB,oW,oP --simplify-exclusive-ap
this gives the attached automaton, which I hope will will more natural
for your use case.
For more information about those two steps, you can look at
https://www.lrde.epita.fr/~adl/dl/adl/blahoudek.15.spin.pdf
The first step of the above example corresponds to r_κ() and the second
to ls().
--
Alexandre Duret-Lutz
