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

But much more fundamentally, I believe that your TLA+ spec is broken because you do not update your variables O and S.

Stephan

On 29 Nov 2023, at 09:56, myeongjin son <sonmyeongjin9@xxxxxxxxx> wrote:

Thank you for your response.

I'm going to try to write a small specification for Liveness, so here's the simplest I could come up with.

Liveness ==
\E o \in O :
  o.st = "none" => <> (o.st = "complete")

However, even in that case, all I got was "TLC cannot handle the temporal formula". Is there some kind of syntax that TLC can't understand when you write TLA+ code like the above and want to use Temporal Logic?

2023년 11월 29일 수요일 오전 8시 33분 2초 UTC에 Stephan Merz님이 작성:
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 => <>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 <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
  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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/70c9b443-a61d-4c1e-9bde-ab7304339361n%40googlegroups.com.

--
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/c0921449-0038-4922-85ac-782f52fc7992n%40googlegroups.com.