[tlaplus] Modelling the Philosophers Dining Problem

[Younes <younesagma@xxxxxxxxx>]

Hi everyone,

I'm new to TLA+ and I'm trying to model the Philosophers Dining Problem.

My initial setup puts all philosophers into "thinking" and all forks to be "available".

I have a deadlock in my current model, and I think, it is because :

The Next action describes : the alternation (\/) of Thinking and Eating actions. This state of the system (all philosophers are thinking) can occur indefinitely.

How do I combine alternation of the actions (think & eat) in the system whilst avoiding a deadlock ? An intermediate state ? I'm confused.

Also, I will be grateful to take any remarks/comments about the design, or the approach. I am really looking forward into getting your critics / reviews.

TLA+ Source Code :

https://gist.github.com/YounesTea/35f52a52e50db114e18366bf73da564f#file-diningproblem-tla

Thank you all

-- 
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/979b04c6-736f-4722-b986-72edea346f7bn%40googlegroups.com.