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

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