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