home *** CD-ROM | disk | FTP | other *** search
/ cs.rhul.ac.uk / www.cs.rhul.ac.uk.zip / www.cs.rhul.ac.uk / pub / CS375 / comm.fdr2 < prev    next >
Text File  |  1999-12-08  |  1KB  |  48 lines
  1. -- Question 4 from Coursework 3
  2.  
  3. datatype message = StartReq | StartAck | StopReq | StopAck
  4.  
  5. channel a, b, c, d : message
  6.  
  7. -- For simplicity, we write out the whole definition of each process,
  8. -- rather than use relabelling
  9.  
  10. P_STOPPED =  a.StartReq -> P_STARTING
  11.           [] b.StartReq -> P_WILLSTART
  12.  
  13. P_STARTING =  b.StartAck -> P_STARTED
  14.  
  15. P_STARTED =  a.StopReq -> P_STOPPING
  16.           [] b.StopReq -> P_WILLSTOP
  17.  
  18. P_STOPPING = b.StopAck -> P_STOPPED
  19.  
  20. P_WILLSTART = a.StartAck -> P_STARTED
  21.  
  22. P_WILLSTOP = a.StopAck -> P_STOPPED
  23.  
  24. Q_STOPPED =  c.StartReq -> Q_STARTING
  25.           [] d.StartReq -> Q_WILLSTART
  26.  
  27. Q_STARTING =  d.StartAck -> Q_STARTED
  28.  
  29. Q_STARTED =  c.StopReq -> Q_STOPPING
  30.           [] d.StopReq -> Q_WILLSTOP
  31.  
  32. Q_STOPPING = d.StopAck -> Q_STOPPED
  33.  
  34. Q_WILLSTART = c.StartAck -> Q_STARTED
  35.  
  36. Q_WILLSTOP = c.StopAck -> Q_STOPPED
  37.  
  38. CHAN1 = a?x -> c!x -> CHAN1
  39.  
  40. CHAN2 = d?x -> b!x -> CHAN2
  41.  
  42. PROCS = P_STOPPED [ {| a,b |} || {| c,d |} ] Q_STOPPED
  43.  
  44. CHANS = CHAN1 [ {| a,c |} || {| b,d |} ] CHAN2
  45.  
  46. SYSTEM = PROCS [ {| a,b,c,d |} || {| a,b,c,d |} ] CHANS
  47.  
  48.