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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 23 Feb 2021 15:08:59 +0100*References*: <979b04c6-736f-4722-b986-72edea346f7bn@googlegroups.com> <45721D1C-F0C7-458F-9679-1241B12FC7BC@gmail.com> <5c61177a-49c9-4a1a-a25e-74945d9e9809n@googlegroups.com>

Hello, sorry for the late reply. Did you use TLC to check your spec? It tells you that it is deadlocked in the initial state. The reason is the definition ChangeStatus(p) == /\ LET status == IF Cardinality(PhiloStatus[p].forks) = 2 THEN "Eating" ELSE "Thinking" IN /\ PhiloStatus' = [ PhiloStatus EXCEPT ![p].status = status ] PickForkP(f,p) == /\ \A ph \in Philosophers : f \notin PhiloStatus[ph].forks \* fork f isn't used by anyone /\ PhiloStatus[p].status = "Thinking" /\ PhiloStatus' = [ PhiloStatus EXCEPT ![p].forks = @ \cup {f} ] /\ ChangeStatus(p) Here you are trying to do two updates to PhiloStatus, this is not going to work. Some minor remarks: - Why do you declare Philosophers, Forks, and Statuses as constant parameters when they can be defined? - Why even record the thinking or eating status of a philosopher in the state: we can just assume that a philosopher is "eating" if she holds two forks and "thinking" otherwise (or if you prefer, "thinking" is she holds no fork and "waiting" if she hold one fork)? I simplified your spec based on these ideas, see the attached module. Now TLC gives me the following results (for Max=5): - when disabling deadlock checking and verifying type correctness, it generates 243 distinct states (so the state space is not trivial anymore), - when verifying the predicate NeverEat, it produces a counter-example showing that philosophers are indeed able to eat, - however, when checking for deadlocks, it shows the deadlock state where each philosopher holds one fork and cannot acquire the second one. Now you'll have to find a way to avoid this deadlock state. Only then worry about verifying liveness properties. Stephan 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/963685A6-8C00-4DE5-B643-68B36067BD64%40gmail.com. |

**Attachment:
Dining.tla**

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/963685A6-8C00-4DE5-B643-68B36067BD64%40gmail.com. |

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

**Re: [tlaplus] Modelling the Philosophers Dining Problem***From:*Stephan Merz

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

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