[tlaplus] Need help in debugging/understanding concurrency concept

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 26.07.2018 18:41, Maneet Bansal wrote:

I was following Hillel's blog to learn TLA+ (Thanks Hillel for creating this). I tried to use the concepts to write "Dining Philosophers" problem https://learntla.com/concurrency/processes/ by myself.

Surprisingly I am not getting the expected deadlock. Can you please help in debugging? Following is what I have written.

Hi Maneet,

why do you expect your specification to deadlock?  If both of the processes fail to acquire their respective second fork, each process will still repeatedly execute its while loops (they essentially livelock).

You probably want to read up on the semantics of "with" [1] to better understand the specification given in learntla.com and why it deadlocks (Next not being enabled).

Hope this helps

Markus

[1] https://lamport.azurewebsites.net/tla/p-manual.pdf  (page 23)