The class of temporal formulas that TLC can handle is described in section 14.2.4 of Specifying Systems. In particular, your quantifiers should range over constant-level expressions, not over the variables O and S.Looking at your specification, I see several antipatterns:- O and S are declared as variables but do not seem to be changed by the actions. In contrast, you write formulas such as\E o \in O:\/ o.owner = 0=> o' = [o EXCEPT !.participate = o.oid]Here, the value of O in the successor state is not determined by the action, but you attempt to modify o. Since o is introduced using the quantifier \E, it is a constant-level _expression_, so o' = o, and assuming that o.oid is different from o.participate, the formula is simply contradictory. (Note also that the lone disjunction symbol is superfluous.)- The property that you are trying to verify is of the form\E vars : F => <>Gso it is true if F is false in the initial state for some value of vars. Looking at the initial condition, we have o1 \in O, s1 \in S, and o1.oid \notin s1.cnfl, which makes the property trivially true.I encourage you to start with a small specification and to validate that specification using simulation and checking invariants that you expect to be true and that you expect to be false before starting to verify liveness properties for larger specifications.StephanOn 29 Nov 2023, at 09:07, myeongjin son <sonmye...@xxxxxxxxx> wrote: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
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.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/70c9b443-a61d-4c1e-9bde-ab7304339361n%40googlegroups.com.