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

Re: [tlaplus] Re: Reproducing deadlock in TLA+

On 15.11.19 17:10, Leslie Lamport wrote:
> Deadlock means reaching a state in which Next is not enabled.  A little
> simple logic shows that, for all t in Thread, in any state in which
> wasVictim[t] and owner[t] are Booleans, at least one of BecomeVictim(t),
> AcquireLock(t), and ReleaseLock(t) is enabled.

For such a small model, the Toolbox can also visualize the state graph
that shows no deadlock states.


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/d64cf80a-43d0-e114-1f53-29aa49762034%40lemmster.de.

Attachment: Model_1.png
Description: PNG image