| According to the TLA+ module in the original post, you define Spec == Init /\ [][Next]_<<victim, owner, wasVictim>> /\ EventualSuccess Since it is part of the specification, the property EventualSuccess can never be violated. ––– By adding a counter variable that can be incremented without bound, you get an infinite state space, so model checking will not finish. You could add a state constraint to instruct TLC to ignore states where the value of the counter exceeds some bound, but it is not clear to me what exactly you are trying to achieve with this extra variable. ––– Adding variable `dead' may be useful. However, nothing in the original specification requires a thread to initiate the process of acquiring a lock (through action BecomeVictim). So, again it is not clear to me why this would be the right way to proceed. ––– I suspect that you want to change your specification so that instead of the conjunct EventualSuccess, it only includes lower-level liveness conditions (typically, fairness hypotheses on actions), and then check property EventualSuccess for that modified specification. A starting point could be to conjoin the formula Fairness defined as Fairness == /\ \A t \in Thread : WF_vars(AcquireLock(t)) /\ \A t \in Thread : WF_vars(ReleaseLock(t)) where vars is the tuple formed of the three variables declared in the module. Hope this helps, Stephan
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3D60E68D-F4D2-4156-A51A-C9F90514CD96%40gmail.com. |