[tlaplus] Need help proving a temporal property

[Pablo Fernandez <fernandezpablo85@xxxxxxxxx>]

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.