home *** CD-ROM | disk | FTP | other *** search
/ cs.rhul.ac.uk / www.cs.rhul.ac.uk.zip / www.cs.rhul.ac.uk / pub / CS375 / peterson1.fdr2 < prev    next >
Text File  |  1999-01-22  |  3KB  |  94 lines
  1. channel p1setflag1, p1resetflag1, p2setflag1, p2resetflag1,
  2.         p1gettrueflag1, p1getfalseflag1, p2gettrueflag1, p2getfalseflag1,
  3.         p1setflag2, p1resetflag2, p2setflag2, p2resetflag2,
  4.         p1gettrueflag2, p1getfalseflag2, p2gettrueflag2, p2getfalseflag2,
  5.         p1set1turn, p1set2turn, p2set1turn, p2set2turn,
  6.         p1get1turn, p1get2turn, p2get1turn, p2get2turn,
  7.         p1enter, p1critical, p1leave,
  8.         p2enter, p2critical, p2leave
  9.  
  10. FLAG1 = FLAG1FALSE
  11. FLAG1FALSE =  p1getfalseflag1 -> FLAG1FALSE
  12.            [] p2getfalseflag1 -> FLAG1FALSE
  13.            [] p1setflag1 -> FLAG1TRUE
  14.            [] p2setflag1 -> FLAG1TRUE
  15.            [] p1resetflag1 -> FLAG1FALSE
  16.            [] p2resetflag1 -> FLAG1FALSE
  17. FLAG1TRUE  =  p1gettrueflag1 -> FLAG1TRUE
  18.            [] p2gettrueflag1 -> FLAG1TRUE
  19.            [] p1resetflag1 -> FLAG1FALSE
  20.            [] p2resetflag1 -> FLAG1FALSE
  21.            [] p1setflag1 -> FLAG1TRUE
  22.            [] p2setflag1 -> FLAG1TRUE
  23.  
  24. FLAG2 = FLAG2FALSE
  25. FLAG2FALSE =  p1getfalseflag2 -> FLAG2FALSE
  26.            [] p2getfalseflag2 -> FLAG2FALSE
  27.            [] p1setflag2 -> FLAG2TRUE
  28.            [] p2setflag2 -> FLAG2TRUE
  29.            [] p1resetflag2 -> FLAG2FALSE
  30.            [] p2resetflag2 -> FLAG2FALSE
  31. FLAG2TRUE  =  p1gettrueflag2 -> FLAG2TRUE
  32.            [] p2gettrueflag2 -> FLAG2TRUE
  33.            [] p1resetflag2 -> FLAG2FALSE
  34.            [] p2resetflag2 -> FLAG2FALSE
  35.            [] p1setflag2 -> FLAG2TRUE
  36.            [] p2setflag2 -> FLAG2TRUE
  37.  
  38. TURN = TURNONE
  39. TURNONE =  p1get1turn -> TURNONE
  40.         [] p2get1turn -> TURNONE
  41.         [] p1set1turn -> TURNONE
  42.         [] p2set1turn -> TURNONE
  43.         [] p1set2turn -> TURNTWO
  44.         [] p2set2turn -> TURNTWO
  45. TURNTWO =  p1get2turn -> TURNTWO
  46.         [] p2get2turn -> TURNTWO
  47.         [] p1set1turn -> TURNONE
  48.         [] p2set1turn -> TURNONE
  49.         [] p1set2turn -> TURNTWO
  50.         [] p2set2turn -> TURNTWO
  51.  
  52. P1 = p1setflag1 -> p1set2turn -> P1WAIT
  53.  
  54. P1WAIT =  p1gettrueflag2 -> (p1get2turn -> P1WAIT
  55.                             [] p1get1turn -> P1ENTER)
  56.        [] p1getfalseflag2 -> P1ENTER
  57.  
  58. P1ENTER = p1enter -> p1critical -> p1leave -> p1resetflag1 -> P1
  59.  
  60. P2 = p2setflag2 -> p2set1turn -> P2WAIT
  61.  
  62. P2WAIT =  p2gettrueflag1 -> (p2get1turn -> P2WAIT
  63.                             [] p2get2turn -> P2ENTER)
  64.        [] p2getfalseflag1 -> P2ENTER
  65.  
  66. P2ENTER = p2enter -> p2critical -> p2leave -> p2resetflag2 -> P2
  67.  
  68. aP1 = {| p1setflag1,p1resetflag1,p1gettrueflag1,p1getfalseflag1,
  69.          p1setflag2,p1resetflag2,p1gettrueflag2,p1getfalseflag2,
  70.          p1set1turn,p1set2turn,p1get1turn,p1get2turn,
  71.          p1enter,p1critical,p1leave |}
  72.  
  73. aP2 = {| p2setflag1,p2resetflag1,p2gettrueflag1,p2getfalseflag1,
  74.          p2setflag2,p2resetflag2,p2gettrueflag2,p2getfalseflag2,
  75.          p2set1turn,p2set2turn,p2get1turn,p2get2turn,
  76.          p2enter,p2critical,p2leave |}
  77.  
  78. aF1 = {| p1setflag1,p1resetflag1,p1gettrueflag1,p1getfalseflag1,
  79.          p2setflag1,p2resetflag1,p2gettrueflag1,p2getfalseflag1 |}
  80.  
  81. aF2 = {| p1setflag2,p1resetflag2,p1gettrueflag2,p1getfalseflag2,
  82.          p2setflag2,p2resetflag2,p2gettrueflag2,p2getfalseflag2 |}
  83.  
  84. aT  = {| p1set1turn,p1set2turn,p1get1turn,p1get2turn,
  85.          p2set1turn,p2set2turn,p2get1turn,p2get2turn |}
  86.  
  87. PROCS = P1 [ aP1 || aP2 ] P2
  88.  
  89. FLAGS = FLAG1 [ aF1 || aF2 ] FLAG2
  90.  
  91. VARS = FLAGS [ union(aF1,aF2) || aT ] TURN
  92.  
  93. SYSTEM = PROCS [ union(aP1,aP2) || union(union(aF1,aF2),aT) ] VARS
  94.