home *** CD-ROM | disk | FTP | other *** search
/ cs.rhul.ac.uk / www.cs.rhul.ac.uk.zip / www.cs.rhul.ac.uk / pub / CS375 / peterson2.fdr2 < prev    next >
Text File  |  1999-02-10  |  2KB  |  55 lines
  1. -- Peterson's Algorithm in CSP: version 2
  2.  
  3. channel flag1set, flag1read, flag2set, flag2read:{1..2}.{|false,true|}
  4. channel turnset, turnread:{1..2}.{1..2}
  5. channel enter, critical, leave:{1..2}
  6.  
  7. FLAG1(v) =  flag1set?x?y -> FLAG1(y)
  8.          [] flag1read.1.v -> FLAG1(v)
  9.          [] flag1read.2.v -> FLAG1(v)
  10.  
  11. FLAG2(v) =  flag2set?x?y -> FLAG2(y)
  12.          [] flag2read.1.v -> FLAG2(v)
  13.          [] flag2read.2.v -> FLAG2(v)
  14.  
  15. TURN(v) =  turnset?x?y -> TURN(y)
  16.         [] turnread.1.v -> TURN(v)
  17.         [] turnread.2.v -> TURN(v)
  18.  
  19. P1 = flag1set.1.true -> turnset.1.2 -> P1WAIT
  20.  
  21. P1WAIT =  flag2read.1.true -> (turnread.1.2 -> P1WAIT
  22.                             [] turnread.1.1 -> P1ENTER)
  23.        [] flag2read.1.false -> P1ENTER
  24.  
  25. P1ENTER = enter.1 -> critical.1 -> leave.1 -> flag1set.1.false -> P1
  26.  
  27. P2 = flag2set.2.true -> turnset.2.1 -> P2WAIT
  28.  
  29. P2WAIT =  flag1read.2.true -> (turnread.2.1 -> P2WAIT
  30.                             [] turnread.2.2 -> P2ENTER)
  31.        [] flag1read.2.false -> P2ENTER
  32.  
  33. P2ENTER = enter.2 -> critical.2 -> leave.2 -> flag2set.2.false -> P2
  34.  
  35. aP1 = {| flag1set.1, flag1read.1, flag2set.1, flag2read.1,
  36.          turnset.1, turnread.1, enter.1, critical.1, leave.1 |}
  37.  
  38. aP2 = {| flag1set.2, flag1read.2, flag2set.2, flag2read.2,
  39.          turnset.2, turnread.2, enter.2, critical.2, leave.2 |}
  40.  
  41. aF1 = {| flag1set,flag1read |}
  42.  
  43. aF2 = {| flag2set,flag2read |}
  44.  
  45. aT  = {| turnset,turnread |}
  46.  
  47. PROCS = P1 [ aP1 || aP2 ] P2
  48.  
  49. FLAGS = FLAG1(false) [ aF1 || aF2 ] FLAG2(false)
  50.  
  51. VARS = FLAGS [ union(aF1,aF2) || aT ] TURN(1)
  52.  
  53. SYSTEM = PROCS [ union(aP1,aP2) || union(union(aF1,aF2),aT) ] VARS
  54.  
  55.