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.fdr2 < prev    next >
Text File  |  1999-02-19  |  1KB  |  40 lines
  1. -- The dining philosophers with deadlock.
  2.  
  3. -- It's more convenient to call the events pickup.1.2 etc, 
  4. -- instead of 1.pickup.2 as in the notes.
  5.  
  6. channel pickup:{0..4}.{0..4}
  7. channel putdown:{0..4}.{0..4}
  8. channel sitdown:{0..4}
  9. channel getup:{0..4}
  10.  
  11. -- Define addition and subtraction mod 5
  12.  
  13. inc(x) = (x + 1) % 5
  14. dec(x) = (x - 1) % 5
  15.  
  16. -- The definitions of the philosophers and the forks are just as in
  17. -- the notes.
  18.  
  19. PHIL(i) =  sitdown.i -> pickup.i.inc(i) -> pickup.i.i -> 
  20.            putdown.i.inc(i) -> putdown.i.i -> getup.i -> PHIL(i)
  21.  
  22. FORK(i) = pickup.i.i -> putdown.i.i -> FORK(i)
  23.         [] pickup.dec(i).i -> putdown.dec(i).i -> FORK(i)
  24.  
  25. -- Notice the use of indexed parallel here.
  26.  
  27. PHILS = || i:{0..4} @ [{|pickup.i.i, pickup.i.inc(i),
  28.                          putdown.i.i, putdown.i.inc(i), 
  29.                          sitdown.i, getup.i|}]          
  30.                     PHIL(i)
  31.  
  32. FORKS = || i:{0..4} @ [{|pickup.i.i, putdown.i.i, 
  33.                          pickup.dec(i).i, putdown.dec(i).i|}] 
  34.                     FORK(i)
  35.  
  36. COLLEGE = PHILS [ {|pickup,putdown,sitdown,getup|} || 
  37.                                    {|pickup,putdown|} ] FORKS
  38.  
  39.  
  40.