Dining Philosophers - specification
Dining Philosophers - specification
DINERS = PHIL0 || ... || PHIL5 || CHOP0 || ... || CHOP5
PHILi = (i.think
® i.get.i ® i.get.(i~1)
® i.eat
® i.put.i ® i.put.(i~1)
® PHILi)
CHOPi = (( i.get.i ® i.put.i [] (iÅ1).get.i ® (iÅ1).put.I )
® CHOPi )
where i~1 = (i+5-1)%5 and iÅ1 = (i+1)%5