hwayne / learntla

A TLA+ guide
http://www.learntla.com
Creative Commons Attribution 4.0 International
278 stars 57 forks source link

Dining philosophers with 1 diner has Deadlock #97

Closed mikeazo closed 2 years ago

mikeazo commented 3 years ago

I've taken the model from here and run it with only 1 philosopher.

Supposedly this should work just fine. When I run it, I end up with "Deadlock reached." Here is the Error Trace

<<
[
 _TEAction |-> [
   position |-> 1,
   name |-> "Initial predicate",
   location |-> "Unknown location"
 ],
 forks |-> <<0>>,
 hungry |-> <<TRUE>>,
 pc |-> <<"P">>
],
[
 _TEAction |-> [
   position |-> 2,
   name |-> "P",
   location |-> "line 64, col 12 to line 71, col 30 of module Playground"
 ],
 forks |-> <<1>>,
 hungry |-> <<TRUE>>,
 pc |-> <<"Eat">>
],
[
 _TEAction |-> [
   position |-> 3,
   name |-> "Eat",
   location |-> "line 73, col 14 to line 80, col 47 of module Playground"
 ],
 forks |-> <<1>>,
 hungry |-> <<TRUE>>,
 pc |-> <<"P">>
]
>>
hwayne commented 2 years ago

I think the model shouldn't work with 1 philosopher, since there's only one fork. So the guide is wrong.