[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 10 Feb 2021 15:48:14 +0100*References*: <979b04c6-736f-4722-b986-72edea346f7bn@googlegroups.com>

Hello, two quick remarks. 1. The definition of your next-state relation is
Also, the body of that formula asserts that either a philosopher starts thinking or that she starts and stops eating simultaneously. Again, this is certainly wrong. One could imagine that thinking and eating alternate, so "start thinking" doesn't need to be a separate transition (because a philosopher starts thinking as soon as she stops eating), but starting and stopping eating should not occur simultaneously. 2. The real challenge in the problem is to avoid the deadlock situation that occurs when each philosopher holds one fork but cannot acquire the second one because it is held by her neighbor. You trivialized that problem by having each philosopher take up and lay down both forks simultaneously. The original formulation of the problem states that forks are taken up individually (see also [1]). This is what makes the problem interesting. Stephan [1] https://en.wikipedia.org/wiki/Dining_philosophers_problem
--
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/45721D1C-F0C7-458F-9679-1241B12FC7BC%40gmail.com. |

**Follow-Ups**:

**References**:**[tlaplus] Modelling the Philosophers Dining Problem***From:*Younes

- Prev by Date:
**[tlaplus] Modelling the Philosophers Dining Problem** - Next by Date:
**[tlaplus] AND operator** - Previous by thread:
**[tlaplus] Modelling the Philosophers Dining Problem** - Next by thread:
**Re: [tlaplus] Modelling the Philosophers Dining Problem** - Index(es):