------------------------------ MODULE Addition ------------------------------
(*
A specification for the addition service in the Aneris paper.
We assume that there are no duplicate messages, and that the set
of clients is fixed.
*)
EXTENDS Integers

CONSTANT CLIENT \* the set of clients

VARIABLES
  serverSt,  \* the state of the server
  clientSt,  \* clientSt[i] is the state of client i
  msgs       \* the set of messages currently in-flight

(* The set of client messages and server responses. *)
ClientMsgs == [type : {"query"}, from : CLIENT, a : Int, b : Int ]

ServerMsgs == [type : {"response"}, to : CLIENT, res: Int]

Messages == ClientMsgs \cup ServerMsgs

(* Type-correctness invariant *)
TypesOK ==
  /\ serverSt \in {"idle", [status : {"processing"}, from : CLIENT, a : Int, b : Int]}
  /\ clientSt \in [CLIENT -> {"idle", [status : {"waiting"}, a : Int, b : Int]}]
  /\ msgs \subseteq Messages

(* Initial predicate *)
Init ==
  /\ serverSt = "idle"
  /\ clientSt = [c \in CLIENT |-> "idle"]
  /\ msgs = {}

(* Server actions *)

ServerReceive == \* server receives a request
  /\ serverSt = "idle"
  /\ \E msg \in msgs :
        /\ serverSt' = [status |-> "processing", from |-> msg.from, a |-> msg.a, b |-> msg.b]
        /\ msgs' = msgs \ {msg}
  /\ UNCHANGED <<clientSt>>


ServerResponse == \* server responds
  /\ \E fromV \in CLIENT, aV \in Int, bV \in Int :
       /\ serverSt = [status |-> "processing", from |-> fromV, a |-> aV, b |-> bV]
       /\ serverSt' = "idle"
       /\ msgs' = msgs \cup {[type |-> "response", to |-> fromV, res |-> (aV + bV)]}
  /\ UNCHANGED <<clientSt>>

(* Client actions *)

ClientSend(c) == \* client c sends an addition request
  /\ clientSt[c] = "idle"
  /\ \E a, b \in Int :
       /\ clientSt' = [clientSt EXCEPT ![c] = [status |-> "waiting", a |-> a, b |-> b]]
       /\ msgs' = msgs \cup {[type |-> "query", from |-> c, a |-> a, b |-> b]}
  /\ UNCHANGED <<serverSt>>

ClientReceive(c) == \* client c receives a response from the server
  /\ \E a, b \in Int :
       /\ clientSt[c] = [status |-> "waiting", a |-> a, b |-> b]
       /\ \E m \in (msgs \intersect ServerMsgs) :
           /\ m.to = c
           /\ msgs' = msgs \ {m}
           /\ clientSt' = [clientSt EXCEPT ![c] = "idle"]
  /\ UNCHANGED <<serverSt>>

Next == \/ ServerReceive
        \/ ServerResponse
        \/ \E c \in CLIENT :
                \/ ClientSend(c)
                \/ ClientReceive(c)

=============================================================================
\* Modification History
\* Last modified Tue Feb 04 13:02:55 CET 2020 by au648539
\* Created Tue Feb 04 10:26:13 CET 2020 by au648539