Liveness == []<> ready
TLC will tell you that this property does not hold for your specification, and it will produce a counterexample where the epoch has reached MaxEpoch and the buffer is filled with recent requests. This is essentially an artefact of bounding epochs: in the actual system, time would continue ticking, and eventually the process would unblock.
There are two ways around this, i.e. to verify that all counterexamples involve such boundary cases:
1. Introduce a state constraint that tells TLC to disregard states where epoch has reached its max value. You'll get a warning that liveness checking with state constraints is dangerous. You can convince yourself that in this case the warning can be ignored, but this requires a detailed understanding of how model checking works, and it may (rightly) scare you off.
2. Check a property that asserts that whenever "ready" stays FALSE, there must be too many recent requests w.r.t. MaxEpoch:
NoStopBeforeMaxEpoch == [](([]~ready) => TooManyRequests(mem, MaxEpoch))
In both cases, TLC succeeds in verifying the property. See attached module and configuration file.
Notes:
- It is actually enough to require weak fairness for both processes ("fair process" instead of "fair+ process").
- I changed the requester process to perform an infinite loop so that it doesn't stop when MaxEpoch has been reached. This is closer to the real system, and it is OK because it cannot result in an infinite state space. It also avoids spurious counter-examples where the loop stops prematurely.
Stephan