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. M. -- 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
