---------------------------- MODULE Philosphers ----------------------------
EXTENDS Integers, Sequences, TLC
CONSTANTS PHIL
(***************************************************************************
Operator to return tupple containing allowed forks to a philoshper.
A philospher with id=i, should have access to forks i and i+1. In case of
pid = N, <<N,1> is returned
Where N is the max number of philospers.
There is no ordering on output.
Also no input checking is being performed.
***************************************************************************)
GetAllowedForks(pid) == IF pid = PHIL
THEN <<pid,1>>
ELSE <<pid,pid+1>>
(* --algorithm dine
(***************************************************************************
fork:0 means the fork is not acquired.
fork:pid means the fork is acquired by pid
***************************************************************************)
variables forks = [ f1 \in 1..PHIL |-> 0]
process phil \in 1..PHIL
variables allowed = GetAllowedForks(self), hungry = TRUE;
begin
PICK_FORKS:
while hungry do
PICK_ONE:
if forks[allowed[1]] = 0
then
forks[allowed[1]] := self;
end if;
PICK_TWO:
if forks[allowed[2]] = 0
then
forks[allowed[2]] := self;
end if;
EAT:
\* Run if philoshper owns both the forks
if forks = <<self,self>>
then
hungry := FALSE;
\* free the forks please
forks[allowed[1]] := 0 || forks[allowed[2]] := 0;
end if;
end while;
end process;
end algorithm; *)
\* BEGIN TRANSLATION
VARIABLES forks, pc, allowed, hungry
vars == << forks, pc, allowed, hungry >>
ProcSet == (1..PHIL)
Init == (* Global variables *)
/\ forks = [ f1 \in 1..PHIL |-> 0]
(* Process phil *)
/\ allowed = [self \in 1..PHIL |-> GetAllowedForks(self)]
/\ hungry = [self \in 1..PHIL |-> TRUE]
/\ pc = [self \in ProcSet |-> "PICK_FORKS"]
PICK_FORKS(self) == /\ pc[self] = "PICK_FORKS"
/\ IF hungry[self]
THEN /\ pc' = [pc EXCEPT ![self] = "PICK_ONE"]
ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED << forks, allowed, hungry >>
PICK_ONE(self) == /\ pc[self] = "PICK_ONE"
/\ IF forks[allowed[self][1]] = 0
THEN /\ forks' = [forks EXCEPT ![allowed[self][1]] = self]
ELSE /\ TRUE
/\ forks' = forks
/\ pc' = [pc EXCEPT ![self] = "PICK_TWO"]
/\ UNCHANGED << allowed, hungry >>
PICK_TWO(self) == /\ pc[self] = "PICK_TWO"
/\ IF forks[allowed[self][2]] = 0
THEN /\ forks' = [forks EXCEPT ![allowed[self][2]] = self]
ELSE /\ TRUE
/\ forks' = forks
/\ pc' = [pc EXCEPT ![self] = "EAT"]
/\ UNCHANGED << allowed, hungry >>
EAT(self) == /\ pc[self] = "EAT"
/\ IF forks = <<self,self>>
THEN /\ hungry' = [hungry EXCEPT ![self] = FALSE]
/\ forks' = [forks EXCEPT ![allowed[self][1]] = 0,
![allowed[self][2]] = 0]
ELSE /\ TRUE
/\ UNCHANGED << forks, hungry >>
/\ pc' = [pc EXCEPT ![self] = "PICK_FORKS"]
/\ UNCHANGED allowed
phil(self) == PICK_FORKS(self) \/ PICK_ONE(self) \/ PICK_TWO(self)
\/ EAT(self)
Next == (\E self \in 1..PHIL: phil(self))
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
=============================================================================