Re: [tlaplus] Need help proving a temporal property

Hello,

ideally you want to check the property

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

--
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/94C85D58-42CB-48DA-AC13-CEBB6DEF3A72%40gmail.com.

Attachment: throttler.cfg
Description: Binary data

Attachment: throttler.tla
Description: Binary data

On 1 Mar 2023, at 21:42, Pablo Fernandez <fernandezpablo85@xxxxxxxxx> wrote:

I have the following spec that represents a throttling strategy:

https://gist.github.com/fernandezpablo85/18d2a52797e6e3fd2be0167699f7b7ce

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.