home *** CD-ROM | disk | FTP | other *** search
/ cs.rhul.ac.uk / www.cs.rhul.ac.uk.zip / www.cs.rhul.ac.uk / pub / CS375 / dphil_butler.fdr2 < prev    next >
Text File  |  1999-02-19  |  1KB  |  38 lines
  1. -- The dining philosophers with a butler.
  2.  
  3. channel pickup:{0..4}.{0..4}
  4. channel putdown:{0..4}.{0..4}
  5. channel sitdown:{0..4}
  6. channel getup:{0..4}
  7.  
  8. inc(x) = (x + 1) % 5
  9. dec(x) = (x - 1) % 5
  10.  
  11. PHIL(i) =  sitdown.i -> pickup.i.inc(i) -> pickup.i.i -> 
  12.            putdown.i.inc(i) -> putdown.i.i -> getup.i -> PHIL(i)
  13.  
  14. FORK(i) = pickup.i.i -> putdown.i.i -> FORK(i)
  15.         [] pickup.dec(i).i -> putdown.dec(i).i -> FORK(i)
  16.  
  17. PHILS = || i:{0..4} @ [{|pickup.i.i, pickup.i.inc(i),
  18.                          putdown.i.i, putdown.i.inc(i), 
  19.                          sitdown.i, getup.i|}]          
  20.                     PHIL(i)
  21.  
  22. FORKS = || i:{0..4} @ [{|pickup.i.i, putdown.i.i, 
  23.                          pickup.dec(i).i, putdown.dec(i).i|}] 
  24.                     FORK(i)
  25.  
  26. COLLEGE = PHILS [ {|pickup,putdown,sitdown,getup|} ||
  27.                   {|pickup,putdown|} ]  FORKS
  28.  
  29. BUTLER(i) = if i == 0 
  30.             then sitdown?x -> BUTLER(1)
  31.             else if i == 4
  32.                  then getup?y -> BUTLER(3)
  33.                  else (  sitdown?x -> BUTLER(i+1)
  34.                       [] getup?y -> BUTLER(i-1) )
  35.  
  36. NEWCOLLEGE = COLLEGE [ {|pickup,putdown,sitdown,getup|} ||
  37.                        {|sitdown,getup|} ] BUTLER(0)
  38.