resource Philosopher import Servant body Philosopher(myservant : cap Servant; id, thinking, eating: int) process phil do true -> nap(int(random(thinking))) write(age(), "philosopher", id, "is hungry") myservant.getforks() nap(int(random(eating))) myservant.relforks() od end phil end Philosopher resource Servant op getforks(), relforks() op needL(), needR(), passL(), passR() op links(l, r : cap Servant) op forks(haveL, dirtyL, haveR, dirtyR : bool) body Servant(id : int) var l, r : cap Servant var haveL, dirtyL, haveR, dirtyR : bool op hungry(), eat() proc getforks() send hungry(); receive eat() end process server receive links(l, r) receive forks(haveL, dirtyL, haveR, dirtyR) do true-> in hungry() -> if ~haveR -> send r.needL() [] else -> write(age(), "philosopher", id, "has right fork") fi if ~haveL -> send l.needR() [] else -> write(age(), "philosopher", id, "has left fork") fi do ~(haveL & haveR) -> in passL() -> haveL := true; dirtyL := false write(age(), "philosopher", id, "got left fork") [] passR() -> haveR := true; dirtyR := false write(age(), "philosopher", id, "got right fork") [] needR() st dirtyR -> haveR := false; dirtyR := false send r.passL(); send r.needL() write(age(), "philosopher", id, "sends dirty right fork") [] needL() st dirtyL -> haveL := false; dirtyL := false send l.passR(); send l.needR() write(age(), "philosopher", id, "sends dirty left fork") ni od write(age(), "philosopher", id, "has both forks") send eat(); dirtyL := true; dirtyR := true receive relforks() write(age(), "philosopher", id, "is finished eating") [] needR() -> haveR := false; dirtyR := false; send r.passL() write(age(), "philosopher", id, "sends right fork") [] needL() -> haveL := false; dirtyL := false; send l.passR() write(age(), "philosopher", id, "sends left fork") ni od end server end Servant resource Main() import Philosopher, Servant var num_phil := 5; getarg(1, num_phil) var run_time : int := 60; getarg(2, run_time) var s[1:num_phil] : cap Servant, p[1:num_phil] : cap Philosopher var think[1:num_phil] : int := ([num_phil] 5) var eat[1:num_phil] : int := ([num_phil] 2) fa i := 1 to num_phil -> getarg(2*i+1, think[i]); getarg(2*i+2, eat[i]) af fa i := 1 to num_phil -> s[i] := create Servant(i) create Philosopher(s[i], i, 1000*think[i], 1000*eat[i]) af printf("%4d philosophers created; think, eat times in seconds:\n", num_phil) fa i := 1 to num_phil -> printf("%4d", think[i]) af; printf("\n") fa i := 1 to num_phil -> printf("%4d", eat[i]) af; printf("\n") fa i := 1 to num_phil -> send s[i].links(s[((i-2) mod num_phil)+1], s[(i mod num_phil)+1]) af send s[1].forks(true, true, true, true) fa i := 2 to num_phil-1 -> send s[i].forks(false, false, true, false) af send s[num_phil].forks(false, false, false, false) nap(1000*run_time); write("must stop now"); stop end Main /* ............... Example compile and run(s) % sr -o didp didp.sr % ./didp 5 10 5 philosophers created; think, eat times in seconds: 5 5 5 5 5 2 2 2 2 2 622 philosopher 2 is hungry 626 philosopher 2 has right fork 629 philosopher 1 sends right fork 632 philosopher 2 got left fork 635 philosopher 2 has both forks 652 philosopher 4 is hungry 655 philosopher 4 has right fork 663 philosopher 3 sends right fork 671 philosopher 4 got left fork 674 philosopher 4 has both forks 1653 philosopher 2 is finished eating 1893 philosopher 4 is finished eating 3312 philosopher 2 is hungry 3317 philosopher 2 has right fork 3318 philosopher 2 has left fork 3319 philosopher 2 has both forks 3442 philosopher 5 is hungry 3445 philosopher 1 sends left fork 3447 philosopher 4 sends right fork 3448 philosopher 5 got right fork 3449 philosopher 5 got left fork 3450 philosopher 5 has both forks 3592 philosopher 3 is hungry 3595 philosopher 4 sends left fork 3597 philosopher 3 got right fork 3922 philosopher 1 is hungry 4143 philosopher 5 is finished eating 4146 philosopher 5 sends right fork 4147 philosopher 1 got left fork 4913 philosopher 2 is finished eating 4916 philosopher 2 sends right fork 4917 philosopher 2 sends left fork 4919 philosopher 3 got left fork 4920 philosopher 3 has both forks 4921 philosopher 1 got right fork 4922 philosopher 1 has both forks 5382 philosopher 4 is hungry 5386 philosopher 5 sends left fork 5388 philosopher 4 got right fork 5842 philosopher 1 is finished eating 5912 philosopher 3 is finished eating 5915 philosopher 3 sends right fork 5917 philosopher 4 got left fork 5918 philosopher 4 has both forks 6452 philosopher 5 is hungry 6456 philosopher 1 sends left fork 6458 philosopher 5 got right fork 6979 philosopher 4 is finished eating 6990 philosopher 4 sends right fork 6992 philosopher 5 got left fork 6994 philosopher 5 has both forks 7123 philosopher 4 is hungry 7133 philosopher 4 has left fork 8143 philosopher 3 is hungry 8147 philosopher 5 is finished eating 8148 philosopher 5 sends left fork 8149 philosopher 3 has left fork 8151 philosopher 4 got right fork 8152 philosopher 4 has both forks 9372 philosopher 2 is hungry 9376 philosopher 3 sends dirty left fork 9378 philosopher 1 sends right fork 9379 philosopher 2 got right fork 9380 philosopher 2 got left fork 9381 philosopher 2 has both forks 9432 philosopher 2 is finished eating 9436 philosopher 2 sends right fork 9438 philosopher 3 got left fork 9592 philosopher 4 is finished eating 9595 philosopher 4 sends left fork 9597 philosopher 3 got right fork 9598 philosopher 3 has both forks 9783 philosopher 3 is finished eating must stop now */