[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] How to Avoid Attempted to check set membership in a tuple value.

The problem appears to be that the variable `Locks' holds a sequence but several actions contain guards of the form

  LockObj \in Locks

As TLC tells you, you cannot test for membership in tuples and sequences. You can rewrite the above test as

  \E i \in 1 .. Len(Locks) : Locks[i] = LockObj

However, from what I understand from your specification, the order of the elements in the sequence `Locks' does not seem to matter and you may consider using a set instead. Not only will the specification become simpler, but TLC will also have less states to explore because states that differ only with respect to the order of elements in `Locks' will be identified.

Stephan


On 27 Jan 2019, at 01:28, Steven Yu <renyu2...@xxxxxxxxx> wrote:

I write below spec, but it failed to run because Attempted to check set membership in a tuple value.

------------------------------ MODULE DeadLock ------------------------------
EXTENDS Integers, Sequences

CONSTANT Threads, Resources

RECURSIVE Remove(_, _)
  Remove(seq, item) == 
  IF seq = << >> THEN << >>
                 ELSE (IF Head(seq) = item THEN << >> ELSE <<Head(seq)>>) 
                      \o Remove(Tail(seq), item) 

VARIABLES Locks, LockObj, ResourceThreadWaitToLock, ResourceLocked, WaitingThreads

Init == /\ Locks = << >>
        /\ LockObj \in Threads \X Resources
        /\ ResourceThreadWaitToLock = << >>
        /\ ResourceLocked = { }
        /\ WaitingThreads = { }
        
TypeOK == /\ Threads # WaitingThreads

LockResource == /\ \E t \in Threads : \E r \in Resources : /\ LockObj' =  << t, r >>
                                                           /\ UNCHANGED << Locks, ResourceThreadWaitToLock, ResourceLocked, WaitingThreads >>
                                                                                                                       
AcquireLock == \/ /\ LockObj \notin Locks
                  /\ {LockObj[2]} \notin ResourceLocked
                  /\ Locks' = Append(Locks, LockObj)
                  /\ ResourceLocked' = ResourceLocked \cup {LockObj[2]}
                  /\ ResourceThreadWaitToLock' = Remove(ResourceThreadWaitToLock, LockObj)
                  /\ WaitingThreads' = WaitingThreads \ {LockObj[1]}
               \/ /\ LockObj \in Locks
                  /\ UNCHANGED << Locks, ResourceThreadWaitToLock, ResourceLocked, WaitingThreads >>
               
Wait == /\ LockObj \notin Locks
        /\ LockObj[2] \in ResourceLocked
        /\ ResourceThreadWaitToLock' = Append(ResourceThreadWaitToLock, LockObj)
        /\ WaitingThreads' = WaitingThreads \cup LockObj[1]
        /\ UNCHANGED << Locks, ResourceLocked >>
                                                                 
ReleaseLock == /\ LockObj \in Locks
               /\ Locks' = Remove(Locks, LockObj)
               /\ ResourceLocked' = ResourceLocked \ LockObj[2]
               /\ UNCHANGED << LockObj, ResourceThreadWaitToLock, WaitingThreads >>

Next == \/ LockResource
        \/ AcquireLock
        \/ ReleaseLock
        \/ Wait

=============================================================================
\* Modification History
\* Last modified Sat Jan 26 16:20:46 PST 2019 by renyu
\* Created Sat Jan 26 14:08:31 PST 2019 by renyu


--
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 post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.