| Hello, 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. Regards, Stephan
|