[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Understanding why specification hits deadlock upon initialization
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
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))
ELSE wState' = wState
However TLC successfully evaluated the spec "DLSpec" without catching the violation of fairness expression for "w1" worker. Why so?