[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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?


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.