remember that you are trying to check an implication of the form
DLSpec => Property
I am assuming that the liveness property that you are interested in is DLStarvationFree, which asserts that for every worker w, infinitely often you have wState[w] = "acquired". Your fairness property DLFairness is expressed in terms of the action AcquiredAllLocks(w), defined as
AcquiredAllLocks(w) == wState' = [wState EXCEPT ![w] = "acquired"]
Note that this action has a trivial enabledness condition, hence the fairness condition boils down to
\A w \in workers : <><< wState' = [wState EXCEPT ![w] = "acquired"] >>_wState
and this trivially implies property DLStarvationFree, whatever the rest of your specification may be.
The problem is that your fairness condition is too strong: you wouldn't know how to implement it in the actual system. It is good practice to assert only fairness conditions that appear as disjuncts of the next-state relation. In your example, a reasonable fairness condition could be
/\ \A w \in workers, l \in locks : WF_Vars(AcquireLock(w,l))
/\ \A w \in workers, l \in locks : WF_Vars(ReleaseLock(w,l))
When you use this, TLC will generate a useful (though quite obvious) counter-example, even for the unmodified specification.