Hello, I am a student learning TLA+.
I am implementing Liveness using temporal logic in TLA+.
Below is the Liveness condition I have written.
Liveness ==
\E o \in O :
\E s \in S :
/\ o.oid \in s.cnfl => <> (<<"write", o.oid>> \in s.Auth)
But when I put that Liveness in Properties to operate the TLC model, I get the following error.
"TLC cannot handle the temporal formula"
------ Under example is my TLA+ code.
EXTENDS Sequences, TLC, Integers
VARIABLES O, S
vars == <<O, S>>
SubjectIDs == {0, 1, 2, 3, 4, 5}
ObjectIDs == {1, 2}
ConfidLevels == {-1, 1, 2}
participates == {-1, 1, 2}
Confid == [oid |-> ObjectIDs]
Rights == {"read", "write"}
GrantedRights == [r |-> Rights, GrantObj |-> ObjectIDs]
ObjectStates == {"none", "distrib", "complete"}
Subject == [sid : SubjectIDs, cnfl : Confid, owner : SubjectIDs, Auth : GrantedRights]
Object == [oid : ObjectIDs, owner : SubjectIDs, participate : participates, st : ObjectStates]
s0 == [sid |-> 0, cnfl |-> {1, 2}, owner |-> 0, Auth |-> {<<"read", 1>>, <<"read", 2>>, <<"write", 1>>, <<"write", 2>>}]
s1 == [sid |-> 1, cnfl |-> {-1}, owner |-> 0]
s2 == [sid |-> 2, cnfl |-> {-1}, owner |-> 0]
s3 == [sid |-> 3, cnfl |-> {-1}, owner |-> 3]
s4 == [sid |-> 4, cnfl |-> {-1}, owner |-> 4]
o1 == [oid |-> 1, owner |-> 0, participate |-> -1, st |-> "none"]
o2 == [oid |-> 2, owner |-> 0, participate |-> -1, st |-> "none"]
Init == /\ O = {o1, o2}
/\ S = {s0, s1, s2, s3, s4}
DefCnfl ==
/\ \E s \in S:
IF (s.owner = 0) /\ (s.sid # s.owner)
THEN s'.cnfl = s.cnfl \union {s.sid}
ELSE S' = S
/\ O' = O
DefObjOP ==
/\ \E o \in O:
\/ o.owner = 0
=> o' = [o EXCEPT !.participate = o.oid]
/\ S' = S
GrantRole(s, o) ==
IF o.oid \in s.cnfl
THEN
s' = [s EXCEPT ![s.Auth] = {<<"read", o.oid>>, <<"write", o.oid>>}]
ELSE
s' = [s EXCEPT ![s.Auth] = {<<"read", o.oid>>}]
GrantRoleAll ==
/\ \A s \in S:
/\ \A o \in O:
o.st = "distrib" => GrantRole(s, o)
/\ O' = O
/\ S' = S
ChangeSt(o) ==
IF o.st = "none"
/\ \E s \in S:
o.participate = s.sid
THEN
"distrib"
ELSE
IF o.st = "distrib"
THEN
"complete"
/\ \A s \in S:
s' = [s EXCEPT ![s.Auth] = {<<"read", o.oid>>}]
ELSE
o.st
ChangeStAll ==
/\ \A o \in O:
o.st' = ChangeSt(o)
/\ O' = O
/\ S' = S
NEXT ==
\/ DefCnfl
\/ DefObjOP
\/ GrantRoleAll
\/ ChangeStAll
Spec == /\ Init /\ [][NEXT]_vars
-----
How do I fix my Liveness condition?
Thanks.