Re: [tlaplus] Help with trivial spec: set generation

Disabling deadlock checking is standard practice when verifying algorithms whose executions are expected to terminate. Checking for deadlocks is mainly useful for algorithms that are expected to run forever, which is the case for many distributed algorithms.

Also, I suggested adding the fairness condition for verifying the liveness properties that you stated in the original version, in particular for verifying termination, i.e. the property <> done. It won't have an effect on deadlock checking: note that absence of deadlock is a safety property.

Stephan

On 22 Aug 2021, at 19:13, Jeenu Viswambharan <jeenuv@xxxxxxxxx> wrote:

Ah, that I could lose fills when adding to a set was completely lost on me. Thanks! For brevity, I choose to keep the quantity in a separate variable than to re-compute. With that, I got TLC completing its run (repo updated).

It bothers me that I still have to pass -deadlock on the command line, though, without which TLC still calls out deadlock. I tried specifying weak fairness, as you suggested, as a conjunct to the spec formula, but that didn't change anything.

Is it a bad thing that I've to specify the -deadlock flag? Do you reckon it's a property of how this particular spec is written, or any spec that has a terminal state?

Jeenu

--
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/b7417987-5e60-4f4f-ab96-f9a4c71d50c2n%40googlegroups.com.

--
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/F1C552A0-0B28-4022-A3BE-EF14664B554F%40gmail.com.