Re: [tlaplus] Understanding why specification hits deadlock upon initialization

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

Thanks. That makes sense and fixed the problem. While the safety checks work now, i don't think the liveness check is working as expected.'

In the same spec, i have the following function to ensure that eventually all workers should have acquired all locks.

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

I have the fairness check added in the spec as following.
   DLSpec == /\ DLInit
          /\ [][DLNext]_Vars
          /\ DLFairnes

I intentionally added a bug in the AcquireLock function to skip "w1" 
   AcquireLock(w,l) == CanAcquire(w,l) /\
                    w # "w1" /\  \* Intentional bug to verify liveness check
                    lState' = [lState EXCEPT ![l] = "acquired"] /\
                    lOwner' = [lOwner EXCEPT ![l] = w] /\
                    IF (\A l1 \in locks: (\/ lOwner[l1] = w))
                            THEN AcquiredAllLocks(w)
                            ELSE wState' = wState

However TLC successfully evaluated the spec "DLSpec" without catching the violation of fairness expression for "w1" worker. Why so?