Re: [tlaplus] How to fix "TLC cannot handle the temporal formula"?

\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 => <>G

so 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.

Stephan

On 29 Nov 2023, at 09:07, myeongjin son <sonmyeongjin9@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
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.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/70c9b443-a61d-4c1e-9bde-ab7304339361n%40googlegroups.com.