Hello,--ideally you want to check the propertyLiveness == []<> readyTLC 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
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/8b6ezffeMTY/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/94C85D58-42CB-48DA-AC13-CEBB6DEF3A72%40gmail.com.
--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/8b6ezffeMTY/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/94C85D58-42CB-48DA-AC13-CEBB6DEF3A72%40gmail.com.
--On 1 Mar 2023, at 21:42, Pablo Fernandez <fernandezpablo85@xxxxxxxxx> wrote:I have the following spec that represents a throttling strategy:The idea is that we allow a maximum of `RequestLimit` requests over the last `TimeSpan`, epoch works as a logical clock.What I'm trying to prove and can't on the `RequestsEventuallyUnblock` is that a "requester" may became temporary blocked (ready = FALSE) but eventually unblocks (ready = TRUE).Any idea how to check that? I was trying to get the opposite to fail ("blocked clients stay blocked") but couldn't.Thanks!PS: Any indications on how to improve the spec are also welcome! I'm in the process of learning TLA+. Thanks Again.--
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/d004d41d-70e5-4b14-8c83-8c5b597ffee4n%40googlegroups.com.
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/8b6ezffeMTY/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/94C85D58-42CB-48DA-AC13-CEBB6DEF3A72%40gmail.com.