Understanding why specification hits deadlock upon initialization

[Somesh Chandra <chandra...@xxxxxxxxx>]

Hello,

I am attempting to write my first example specification using TLA+, for which TLC immediately reports deadlock at the initial state.

My specification is pasted below and i provided following input.

workers: { "w1" , "w2" }
locks: { "l1", "l2" }

---------------------------- MODULE Liveness ----------------------------
\* Specification for multiple workers, which will attempt to acquire all free locks.
\* We need to ensure that
\* 1) Safety: At most one worker can acquire all locks at any give time.
\* 2) Liveness: All workers should eventualy acquire all locks.
EXTENDS TLC, FiniteSets

CONSTANT workers, locks       \* The set of participating resources
VARIABLE wState, lState, lOwner \* Track state of resources.

DLTypeOK == \A w \in workers : wState[w] \in { "free", "acquired" } /\
            \A l1 \in locks : lState[l1] \in { "free", "acquired" } /\
            \A l2 \in locks : lOwner[l2] \in workers \cup { "none" }
           
DLInit == wState = [ w \in workers |-> "free" ] /\
          lState = [ l \in locks |-> "free" ] /\
          lOwner = [ l \in locks |-> "none" ]
          
CanAcquire(w,l) == lState[l] = "free" \/    \* Lock is free to be acquired by any worker
                   (lState[l] = "acquired" /\ lOwner[l] = w ) \* Renew: Lock re-acquired by same worker. 

AcquiredAllLocks(w) == wState' = [wState EXCEPT ![w] = "acquired"]

AcquireLock(w,l) == CanAcquire(w,l) /\
                    lState' = [lState EXCEPT ![l] = "acquired"] /\
                    lOwner' = [lOwner EXCEPT ![l] = w] /\
                    IF (\A l1 \in locks: (\/ lOwner[l1] = w))
                            THEN AcquiredAllLocks(w)
                            ELSE wState' = wState
                            
ReleaseLock(w,l) == lOwner[l] = w /\
                    lOwner' = [lOwner EXCEPT ![l] = "none"] /\
                    lState' = [lState EXCEPT ![l] = "free"] /\
                    wState' = [wState EXCEPT ![w] = "free"]  \* As soon as a single lock is released, we should assume that the worker is free.

\* One or more worker can attempt to acquire or release all locks, if possible.
DLNext == \/ \E w \in workers : \A l \in locks : (\/ AcquireLock(w,l) \/ ReleaseLock(w,l))
          
\* No 2 workers can be in "acquired" state at the same time
DLMutualExclusion == \A w1, w2 \in workers : ~ ([](/\ w1 # w2
                                                /\ wState[w1] = "acquired"
                                                /\ wState[w2] = "acquired"))

\* Eventually all workers should get a chance to acquire lock
\* TODO: How should TLC be told to check this?
DLStarvationFree == \A w \in workers : []<>(wState[w] = "acquired")

DLFairness == \A w \in workers : WF_<<wState>>(AcquiredAllLocks(w))

Vars == <<wState, lState, lOwner>>

DLSpec == /\ DLInit
          /\ [][DLNext]_Vars
          /\ DLStarvationFree
=============================================================================

My assumption is that TLC should pick first worker and then attempt to acquire all locks and then release all locks, and repeat the same for second worker. 

What am i doing wrong to hit a deadlock during the init state itself?

Thanks
Somesh