API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Apr 23rd, 2019
151
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 7.72 KB | None | 0 0
raw download clone embed print report
  1. --------- MODULE token -----------
  2.  
  3. EXTENDS Naturals, Sequences, TLC
  4.  
  5. CONSTANT MAXP IDs == 0 .. MAXP-1
  6.  
  7. VARIABLE parent, deferred, holding, source, originator, req, pc, tok
  8.  
  9. Vars == << parent, deferred, holding, source, originator, req, pc, tok >>
  10.  
  11. Send(m,chan,i) == IF i=0 THEN chan' = chan ELSE chan' = [chan EXCEPT ![i] = Append(@,m)] \* "totalised" channel sending operation
  12.  
  13. Receive(v,chan,i) == chan[i] # << >> /\ v = Head(chan[i]) /\ chan' = [chan EXCEPT ![i] = Tail(@)] \* channel reception operation
  14.  
  15. Test(chan,i) == chan[i] # << >>
  16.  
  17. Init == /\ parent = [n \in IDs |-> n-1]
  18. /\ deferred = [n \in IDs |-> 0]
  19. /\ holding = [n \in IDs |-> IF n = 1 THEN TRUE ELSE FALSE]
  20. /\ source = [n \in IDs |-> 1]
  21. /\ originator = [n \in IDs |-> 1]
  22. /\ req = [n \in IDs |-> << >>]
  23. /\ pc = [n \in IDs |-> 0]
  24. /\ tok = [n \in IDs |-> << >>]
  25.  
  26. Driver(n) == /\ pc[n] = 0
  27. /\ IF Test(req,n) THEN pc' = [pc EXCEPT ![n] = 12] ELSE pc' = [pc EXCEPT ![n] = 1]
  28. /\ UNCHANGED(<<tok, parent, deferred, holding, source, originator, req >>) \*removed tok, critical from argument list
  29.  
  30. Proc1(n) == /\ pc[n] = 1
  31. /\ pc' = [pc EXCEPT ![n] = 2]
  32. /\ UNCHANGED <<tok, parent, deferred, holding, source, originator, req>>
  33.  
  34. Proc2(n) == /\ pc[n] = 2
  35. /\ ( \/ ( /\ holding[n] = FALSE
  36. /\ pc' = [pc EXCEPT ![n] = 3])
  37. \/ ( /\ holding[n] = TRUE
  38. /\ pc' = [pc EXCEPT ![n] = 6]))
  39. /\ UNCHANGED <<tok, parent, deferred, holding, source, originator, req >>
  40.  
  41. Proc3(n) == /\ pc[n] = 3
  42. /\ Send([sender |-> n, origin |-> n], req, parent[n])
  43. /\ pc' = [pc EXCEPT ![n] = 4]
  44. /\ UNCHANGED <<tok, parent, deferred, holding, source, originator >>
  45.  
  46. Proc4(n) == /\ pc[n] = 4
  47. /\ parent' = [parent EXCEPT ![n] = 0]
  48. /\ pc' = [pc EXCEPT ![n] = 5]
  49. /\ UNCHANGED <<tok, deferred, holding, source, originator, req >>
  50.  
  51. Proc5(n) == /\ pc[n] = 5
  52. /\ Receive(0, tok, n)
  53. /\ pc' = [pc EXCEPT ![n] = 6]
  54. /\ UNCHANGED << parent, deferred, holding, source, originator, req >>
  55.  
  56. Proc6(n) == /\ pc[n] = 6
  57. /\ holding' = [holding EXCEPT ![n] = FALSE]
  58. /\ pc' = [pc EXCEPT ![n] = 7]
  59. /\ UNCHANGED <<tok, parent, deferred, source, originator, req >>
  60.  
  61. Proc7(n) == /\ pc[n] = 7
  62. /\ pc' = [pc EXCEPT ![n] = 8]
  63. /\ UNCHANGED <<tok, parent, deferred, holding, source, originator, req >>
  64.  
  65. Proc8(n) == /\ pc[n] = 8
  66. /\ ( \/ ( /\ deferred[n] # 0
  67. /\ pc' = [pc EXCEPT ![n] = 9])
  68. \/ ( /\ deferred[n] = 0
  69. /\ pc' = [pc EXCEPT ![n] = 11]))
  70. /\ UNCHANGED <<deferred, tok, parent, holding, source, originator, req >>
  71.  
  72. Proc9(n) == /\ pc[n] = 9
  73. /\ Send(0,tok,deferred[n])
  74. /\ pc' = [pc EXCEPT ![n] = 4]
  75. /\ UNCHANGED <<parent, holding, deferred, source, originator >>
  76.  
  77. Proc10(n) == /\ pc[n] = 10
  78. /\ deferred' = [deferred EXCEPT ![n] = 0]
  79. /\ pc' = [pc EXCEPT ![n] = 0]
  80. /\ UNCHANGED <<tok, parent, holding, source, originator, req>>
  81.  
  82. Proc11(n) == /\ pc[n] = 11
  83. /\ holding' = [holding EXCEPT ![n] = TRUE]
  84. /\ pc' = [pc EXCEPT ![n] = 0]
  85. /\ UNCHANGED <<tok, parent, deferred, source, originator, req>>
  86.  
  87. Proc12(n) == /\ pc[n] = 12
  88. /\ (\E v \in [sender: IDs, origin: IDs]:
  89. /\ Receive(v,req,n)
  90. /\ source' = [source EXCEPT ![n] = v.sender]
  91. /\ originator' = [originator EXCEPT ![n] = v.origin])
  92. /\ pc' = [pc EXCEPT ![n] = 13]
  93. /\ UNCHANGED <<holding, tok, parent, deferred >>
  94.  
  95. Proc13(n) == /\ pc[n] = 13
  96. /\ ( \/ ( /\ parent[n] = 0
  97. /\ pc' = [pc EXCEPT ![n] = 14])
  98. \/ ( /\ parent[n] # 0
  99. /\ pc' = [pc EXCEPT ![n] = 18]))
  100. /\ UNCHANGED <<deferred, tok, parent, holding, source, originator, req >>
  101.  
  102. Proc14(n) == /\ pc[n] = 14
  103. /\ ( \/ ( /\ holding[n] = TRUE
  104. /\ pc' = [pc EXCEPT ![n] = 15])
  105. \/ ( /\ holding[n] = FALSE
  106. /\ pc' = [pc EXCEPT ![n] = 17]))
  107. /\ UNCHANGED <<deferred, tok, parent, holding, source, originator, req >>
  108.  
  109. Proc15(n) == /\ pc[n] = 15
  110. /\ Send(0,tok,originator[n])
  111. /\ pc' = [pc EXCEPT ![n] = 16]
  112. /\ UNCHANGED <<req, parent, deferred, holding, source, originator >>
  113.  
  114. Proc16(n) == /\ pc[n] = 16
  115. /\ holding' = [holding EXCEPT ![n] = FALSE]
  116. /\ pc' = [pc EXCEPT ![n] = 19]
  117. /\ UNCHANGED <<tok, parent, deferred, source, originator, req >>
  118.  
  119. Proc17(n) == /\ pc[n] = 17
  120. /\ deferred' = [deferred EXCEPT ![n] = originator[n]]
  121. /\ pc' = [pc EXCEPT ![n] = 19]
  122. /\ UNCHANGED <<tok, parent, holding, source, originator, req >>
  123.  
  124. Proc18(n) == /\ pc[n] = 18
  125. /\ Send([sender |-> n, origin |-> originator[n]],req,parent[n])
  126. /\ pc' = [pc EXCEPT ![n] = 19]
  127. /\ UNCHANGED <<holding, tok, parent, deferred, source, originator >>
  128.  
  129. Proc19(n) == /\ pc[n] = 19
  130. /\ parent' = [parent EXCEPT ![n] = source[n]]
  131. /\ pc' = [pc EXCEPT ![n] = 0]
  132. /\ UNCHANGED <<req, tok, holding, deferred, source, originator >>
  133.  
  134. NextMain(n) == \/ Proc1(n)
  135. \/ Proc2(n)
  136. \/ Proc3(n)
  137. \/ Proc4(n)
  138. \/ Proc5(n)
  139. \/ Proc6(n)
  140. \/ Proc7(n)
  141. \/ Proc8(n)
  142. \/ Proc9(n)
  143. \/ Proc10(n)
  144. \/ Proc11(n)
  145.  
  146. NextReceive(n) == \/ Proc12(n)
  147. \/ Proc13(n)
  148. \/ Proc14(n)
  149. \/ Proc15(n)
  150. \/ Proc16(n)
  151. \/ Proc17(n)
  152. \/ Proc18(n)
  153. \/ Proc19(n)
  154.  
  155. Algorithm(n) == \/ NextReceive(n)
  156. \/ NextMain(n)
  157. \/ Driver(n)
  158.  
  159. Next == (\E n \in IDs: Algorithm(n))
  160.  
  161. Spec == Init /\ [] [Next]_Vars /\ WF_Vars(Next)
  162. =======
  163. (*
  164. CONSTANT MAXP IDs == 0 .. MAXP-1
  165.  
  166. VARIABLE phone, chan, pc
  167.  
  168. TypeInv == phone \in [IDs -> BOOLEAN]
  169. /\ chan \in [IDs -> 0 .. 1]
  170. /\ pc \in [IDs -> 0 .. 4]
  171.  
  172. Init == phone = [p \in IDs |-> FALSE]
  173. /\ chan = [[p \in IDs |-> 0] EXCEPT ![0] = 1]
  174. /\ pc = [p \in IDs |-> 1]
  175.  
  176. Proc1(n) == pc[n] = 1
  177. /\ chan[n] = 1
  178. /\ pc' = [pc EXCEPT ![n]=2]
  179. /\ UNCHANGED <<chan, phone>>
  180.  
  181. Proc2(n) == pc[n] = 2
  182. /\ phone' = [phone EXCEPT ![n] = TRUE]
  183. /\ pc' = [pc EXCEPT ![n]=3]
  184. /\ UNCHANGED <<chan>>
  185.  
  186. Proc3(n) == pc[n] = 3
  187. /\ phone' = [phone EXCEPT ![n] = FALSE]
  188. /\ pc' = [pc EXCEPT ![n]=4]
  189. /\ UNCHANGED <<chan>>
  190.  
  191. Proc4(n) == pc[n] = 4
  192. /\ chan' = [chan EXCEPT ![n] = 0, ![(n+1) % MAXP] = 1]
  193. /\ pc' = [pc EXCEPT ![n]=1]
  194. /\ UNCHANGED <<phone>>
  195.  
  196. Proc(n) == Proc1(n) \/ Proc2(n) \/ Proc3(n) \/ Proc4(n)
  197.  
  198. Next == \E n \in IDs : Proc(n)
  199.  
  200. vars == <<phone, chan, pc>>
  201.  
  202. Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
  203.  
  204. \* Wait for token. Receive token (chan,token). Pick up phone(phone) Hang up phone(phone). Send token(chan,token)
  205. \*node(x) ==
  206.  
  207. ========
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!