resource philosopher
   import dining_server
body philosopher(i : int; dcap : cap dining_server; thinking, eating: int)
   write("philosopher", i, "alive, max think eat delays", thinking, eating)

   procedure think()
      var napping : int
      napping := int(random(1000*thinking))
      writes("age=",age(),", philosopher ",i," thinking for ",napping," ms\n")
      nap(napping)
   end think

   procedure eat()
      var napping : int
      napping := int(random(1000*eating))
      writes("age=",age(),", philosopher ",i," eating for ",napping," ms\n")
      nap(napping)
   end eat

   process phil
      do true ->
         think()
         writes("age=", age(), ", philosopher ", i, " is hungry\n")
         dcap.take_forks(i)
         writes("age=", age(), ", philosopher ", i, " has taken forks\n")
         eat()
         dcap.put_forks(i)
         writes("age=", age(), ", philosopher ", i, " has returned forks\n")
      od
   end phil
end philosopher

resource dining_server
   op take_forks(i : int), put_forks(i : int)
body dining_server(num_phil : int)
   write("dining server for", num_phil, "philosophers is alive")
   sem mutex := 1
   type states = enum(thinking, hungry, eating)
   var state[1:num_phil] : states := ([num_phil] thinking)
   sem phil[1:num_phil] := ([num_phil] 0)

   procedure left(i : int) returns lft : int
      if i=1 -> lft := num_phil [] else -> lft := i-1 fi
   end left

   procedure right(i : int) returns rgh : int
      if i=num_phil -> rgh := 1 [] else -> rgh := i+1 fi
   end right

   procedure test(i : int)
      if state[i] = hungry and state[left(i)] ~= eating
            and state[right(i)] ~= eating ->
         state[i] := eating
         V(phil[i])
      fi
   end test

   proc take_forks(i)
      P(mutex)
      state[i] := hungry
      test(i)
      V(mutex)
      P(phil[i])
   end take_forks

   proc put_forks(i)
      P(mutex)
      state[i] := thinking
      test(left(i)); test(right(i))
      V(mutex)
   end put_forks
end dining_server

resource start()
   import philosopher, dining_server
   var num_phil : int := 5, run_time : int := 60
   getarg(1, num_phil); getarg(2, run_time)
   var max_think_delay[1:num_phil] : int := ([num_phil] 5)
   var max_eat_delay[1:num_phil] : int := ([num_phil] 2)
   fa i := 1 to num_phil ->
      getarg(2*i+1, max_think_delay[i]); getarg(2*i+2, max_eat_delay[i])
   af

   var dcap : cap dining_server
   write(num_phil, "dining philosophers running", run_time, "seconds")
   dcap := create dining_server(num_phil)
   fa i := 1 to num_phil ->
      create philosopher(i, dcap, max_think_delay[i], max_eat_delay[i])
   af
   nap(1000*run_time); write("must stop now"); stop
end start

/* ............... Example compile and run(s)

% sr -o dphi dphi.sr
% ./dphi 5 10
5 dining philosophers running 10 seconds
dining server for 5 philosophers is alive
philosopher 1 alive, max think eat delays 5 2
age=37, philosopher 1 thinking for 491 ms
philosopher 2 alive, max think eat delays 5 2
age=50, philosopher 2 thinking for 2957 ms
philosopher 3 alive, max think eat delays 5 2
age=62, philosopher 3 thinking for 1374 ms
philosopher 4 alive, max think eat delays 5 2
age=74, philosopher 4 thinking for 1414 ms
philosopher 5 alive, max think eat delays 5 2
age=87, philosopher 5 thinking for 1000 ms
age=537, philosopher 1 is hungry
age=541, philosopher 1 has taken forks
age=544, philosopher 1 eating for 1351 ms
age=1097, philosopher 5 is hungry
age=1447, philosopher 3 is hungry
age=1451, philosopher 3 has taken forks
age=1454, philosopher 3 eating for 1226 ms
age=1497, philosopher 4 is hungry
age=1898, philosopher 1 has returned forks
age=1901, philosopher 1 thinking for 2042 ms
age=1902, philosopher 5 has taken forks
age=1903, philosopher 5 eating for 1080 ms
age=2687, philosopher 3 has returned forks
age=2691, philosopher 3 thinking for 2730 ms
age=2988, philosopher 5 has returned forks
age=2991, philosopher 5 thinking for 3300 ms
age=2992, philosopher 4 has taken forks
age=2993, philosopher 4 eating for 1818 ms
age=3017, philosopher 2 is hungry
age=3020, philosopher 2 has taken forks
age=3021, philosopher 2 eating for 1393 ms
age=3947, philosopher 1 is hungry
age=4418, philosopher 2 has returned forks
age=4421, philosopher 2 thinking for 649 ms
age=4423, philosopher 1 has taken forks
age=4424, philosopher 1 eating for 1996 ms
age=4817, philosopher 4 has returned forks
age=4821, philosopher 4 thinking for 742 ms
age=5077, philosopher 2 is hungry
age=5427, philosopher 3 is hungry
age=5431, philosopher 3 has taken forks
age=5432, philosopher 3 eating for 857 ms
age=5569, philosopher 4 is hungry
age=6298, philosopher 3 has returned forks
age=6301, philosopher 3 thinking for 1309 ms
age=6302, philosopher 5 is hungry
age=6304, philosopher 4 has taken forks
age=6305, philosopher 4 eating for 498 ms
age=6428, philosopher 1 has returned forks
age=6430, philosopher 1 thinking for 1517 ms
age=6432, philosopher 2 has taken forks
age=6433, philosopher 2 eating for 133 ms
age=6567, philosopher 2 has returned forks
age=6570, philosopher 2 thinking for 3243 ms
age=6808, philosopher 4 has returned forks
age=6810, philosopher 4 thinking for 2696 ms
age=6812, philosopher 5 has taken forks
age=6813, philosopher 5 eating for 1838 ms
age=7617, philosopher 3 is hungry
age=7621, philosopher 3 has taken forks
age=7622, philosopher 3 eating for 1251 ms
age=7957, philosopher 1 is hungry
age=8658, philosopher 5 has returned forks
age=8661, philosopher 5 thinking for 4755 ms
age=8662, philosopher 1 has taken forks
age=8664, philosopher 1 eating for 1426 ms
age=8877, philosopher 3 has returned forks
age=8880, philosopher 3 thinking for 2922 ms
age=9507, philosopher 4 is hungry
age=9511, philosopher 4 has taken forks
age=9512, philosopher 4 eating for 391 ms
age=9817, philosopher 2 is hungry
age=9908, philosopher 4 has returned forks
age=9911, philosopher 4 thinking for 3718 ms
age=10098, philosopher 1 has returned forks
age=10100, philosopher 1 thinking for 2541 ms
must stop now
age=10109, philosopher 2 has taken forks
age=10110, philosopher 2 eating for 206 ms
% ./dphi 5 10 1 10 10 1 1 10 10 1 10 1
5 dining philosophers running 10 seconds
dining server for 5 philosophers is alive
philosopher 1 alive, max think eat delays 1 10
age=34, philosopher 1 thinking for 762 ms
philosopher 2 alive, max think eat delays 10 1
age=49, philosopher 2 thinking for 5965 ms
philosopher 3 alive, max think eat delays 1 10
age=61, philosopher 3 thinking for 657 ms
philosopher 4 alive, max think eat delays 10 1
age=74, philosopher 4 thinking for 8930 ms
philosopher 5 alive, max think eat delays 10 1
age=86, philosopher 5 thinking for 5378 ms
age=726, philosopher 3 is hungry
age=731, philosopher 3 has taken forks
age=732, philosopher 3 eating for 3511 ms
age=804, philosopher 1 is hungry
age=808, philosopher 1 has taken forks
age=809, philosopher 1 eating for 3441 ms
age=4246, philosopher 3 has returned forks
age=4250, philosopher 3 thinking for 488 ms
age=4252, philosopher 1 has returned forks
age=4253, philosopher 1 thinking for 237 ms
age=4495, philosopher 1 is hungry
age=4498, philosopher 1 has taken forks
age=4499, philosopher 1 eating for 8682 ms
age=4745, philosopher 3 is hungry
age=4748, philosopher 3 has taken forks
age=4749, philosopher 3 eating for 2095 ms
age=5475, philosopher 5 is hungry
age=6025, philosopher 2 is hungry
age=6855, philosopher 3 has returned forks
age=6859, philosopher 3 thinking for 551 ms
age=7415, philosopher 3 is hungry
age=7420, philosopher 3 has taken forks
age=7421, philosopher 3 eating for 1765 ms
age=9015, philosopher 4 is hungry
age=9196, philosopher 3 has returned forks
age=9212, philosopher 3 thinking for 237 ms
age=9217, philosopher 4 has taken forks
age=9218, philosopher 4 eating for 775 ms
age=9455, philosopher 3 is hungry
age=9997, philosopher 4 has returned forks
age=10000, philosopher 4 thinking for 2451 ms
age=10002, philosopher 3 has taken forks
age=10004, philosopher 3 eating for 9456 ms
must stop now
                                              */