Re: [tlaplus] How to check Deadlock

[Stephan Merz <stepha...@xxxxxxxxx>]

Once you have specified your algorithm in a TLA+ module, you need to create a model that provides concrete values for parameters etc. In the TLA+ Toolbox, click on TLC Model Checker -> New Model. The rest should be fairly obvious. Also please make sure that you watch at least some of the TLA+ videos and/or read the relevant parts of the Hyperbook, all available from the TLA+ Web page.

Stephan

On 5 Oct 2018, at 08:37, yashmeh...@xxxxxxxxx wrote:

I have implemented an Algorithm in TLC, I know it should lead to a deadlocked state at some point. How do I verify?

--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.