Module System

type PhilosopherState = {thinking,eating}
type ForkState = {available,nonavailable}
macro NumOfPhilosophers = 5
macro NumOfForks = 5
local philosophers : array [0..-1] of PhilosopherState where Forall i:[0..-1] . (philosophers[i] = thinking)
local forks : array [0..-1] of ForkState where Forall i:[0..-1] . (forks[i] = available)


Module Philosopher :
external out i : int 


Transition PickUpForks NoFairness:
enable ((philosophers[i]=thinking)/\(forks[i]=available)/\(forks[(i+1) mod NumOfForks]=available))
assign philosophers[i] := eating,forks[i] := nonavailable,forks[(i+1) mod NumOfForks] := nonavailable

Transition ReturnForks NoFairness:
enable philosophers[i]=eating
assign philosophers[i] := thinking,forks[i] := available,forks[(i+1) mod NumOfForks] := available
EndModule


Module SYSTEM :
local p0 : int where p0 = 0
local p1 : int where p1 = 1
local p2 : int where p2 = 2
local p3 : int where p3 = 3
local p4 : int where p4 = 4

include Philosopher : ( Philosopher where out i = p0)
 || Philosopher : ( Philosopher where out i = p1)
 || Philosopher : ( Philosopher where out i = p2)
 || Philosopher : ( Philosopher where out i = p3)
 || Philosopher : ( Philosopher where out i = p4)
EndModule