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

[Jeenu Viswambharan <jeenuv@xxxxxxxxx>]

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.