Guest User

Untitled

a guest
Feb 4th, 2020
176
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. ------------------------------ MODULE Addition ------------------------------
  2. (*
  3. A specification for the addition service in the Aneris paper.
  4. We assume that there are no duplicate messages, and that the set
  5. of clients is fixed.
  6. *)
  7. EXTENDS Integers
  8.  
  9. CONSTANT CLIENT \* the set of clients
  10.  
  11. VARIABLES
  12. serverSt, \* the state of the server
  13. clientSt, \* clientSt[i] is the state of client i
  14. msgs \* the set of messages currently in-flight
  15.  
  16. (* The set of client messages and server responses. *)
  17. ClientMsgs == [type : {"query"}, from : CLIENT, a : Int, b : Int ]
  18.  
  19. ServerMsgs == [type : {"response"}, to : CLIENT, res: Int]
  20.  
  21. Messages == ClientMsgs \cup ServerMsgs
  22.  
  23. (* Type-correctness invariant *)
  24. TypesOK ==
  25. /\ serverSt \in {"idle", [status : {"processing"}, from : CLIENT, a : Int, b : Int]}
  26. /\ clientSt \in [CLIENT -> {"idle", [status : {"waiting"}, a : Int, b : Int]}]
  27. /\ msgs \subseteq Messages
  28.  
  29. (* Initial predicate *)
  30. Init ==
  31. /\ serverSt = "idle"
  32. /\ clientSt = [c \in CLIENT |-> "idle"]
  33. /\ msgs = {}
  34.  
  35. (* Server actions *)
  36.  
  37. ServerReceive == \* server receives a request
  38. /\ serverSt = "idle"
  39. /\ \E msg \in msgs :
  40. /\ serverSt' = [status |-> "processing", from |-> msg.from, a |-> msg.a, b |-> msg.b]
  41. /\ msgs' = msgs \ {msg}
  42. /\ UNCHANGED <<clientSt>>
  43.  
  44.  
  45. ServerResponse == \* server responds
  46. /\ \E fromV \in CLIENT, aV \in Int, bV \in Int :
  47. /\ serverSt = [status |-> "processing", from |-> fromV, a |-> aV, b |-> bV]
  48. /\ serverSt' = "idle"
  49. /\ msgs' = msgs \cup {[type |-> "response", to |-> fromV, res |-> (aV + bV)]}
  50. /\ UNCHANGED <<clientSt>>
  51.  
  52. (* Client actions *)
  53.  
  54. ClientSend(c) == \* client c sends an addition request
  55. /\ clientSt[c] = "idle"
  56. /\ \E a, b \in Int :
  57. /\ clientSt' = [clientSt EXCEPT ![c] = [status |-> "waiting", a |-> a, b |-> b]]
  58. /\ msgs' = msgs \cup {[type |-> "query", from |-> c, a |-> a, b |-> b]}
  59. /\ UNCHANGED <<serverSt>>
  60.  
  61. ClientReceive(c) == \* client c receives a response from the server
  62. /\ \E a, b \in Int :
  63. /\ clientSt[c] = [status |-> "waiting", a |-> a, b |-> b]
  64. /\ \E m \in (msgs \intersect ServerMsgs) :
  65. /\ m.to = c
  66. /\ msgs' = msgs \ {m}
  67. /\ clientSt' = [clientSt EXCEPT ![c] = "idle"]
  68. /\ UNCHANGED <<serverSt>>
  69.  
  70. Next == \/ ServerReceive
  71. \/ ServerResponse
  72. \/ \E c \in CLIENT :
  73. \/ ClientSend(c)
  74. \/ ClientReceive(c)
  75.  
  76. =============================================================================
  77. \* Modification History
  78. \* Last modified Tue Feb 04 13:02:55 CET 2020 by au648539
  79. \* Created Tue Feb 04 10:26:13 CET 2020 by au648539
RAW Paste Data