%% author: Shien Jin Ong %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Number of nodes limited to 5.  %
% Write/Memory values = [1, 100] %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%--- 1. type declarations ---%
uses NonDet

type Message = enumeration of read, OK, nil
type Invocation = union of val: Nat, msg: Message

%--- 2. CentralMem ---%
automaton CentralMem
  signature
    input invoke(v: Invocation, n: Nat)       % invocation from client n
    output respond(r: Invocation, n: Nat)     % response to client n
    internal perform(n: Nat)
  states
    mem:  Nat := 0,
    req:  Array[Nat, Invocation] := constant(msg(nil)),
    resp: Array[Nat, Invocation] := constant(msg(nil))
  transitions
    input invoke(v, n)
      eff req[n] := v
    output respond(r, n)
      pre resp[n] = r /\ resp[n] ~= msg(nil)
      eff req[n] := msg(nil);
          resp[n] := msg(nil)
    internal perform(n)
      pre req[n] ~= msg(nil) /\ resp[n] = msg(nil)
      eff if req[n] = msg(read) then resp[n] := val(mem)
          else mem := req[n].val;
               resp[n] := msg(OK)
          fi
  schedule
    states
      die: Nat,
      Node: Nat,                              % represents a client
      read_write: Bool,                       % whether to read or to write
      value: Nat                              % the value to write
    do
      while true do
        die := randomNat(1,2);
        Node := randomNat(1,5);
        read_write := randomBool;
        value := randomNat(1,100);
        if die = 1 /\ req[Node] = msg(nil) then
          if read_write then fire input invoke(msg(read), Node)
          else fire input invoke(val(value), Node)
          fi
        elseif die = 2 /\ resp[Node] ~= msg(nil) then
          fire output respond(resp[Node], Node)
        elseif req[Node] ~= msg(nil) /\ resp[Node] = msg(nil) then
          fire internal perform(Node) 
        fi
      od
    od

%--- 3. StrongCache ---%
automaton StrongCache
  signature
    input invoke(v: Invocation, n: Nat)
    output respond(r: Invocation, n: Nat)
    internal perform(n: Nat), copy(n: Nat), drop(n: Nat)
  states
    mem: Nat := 0,
    cache: Array[Nat, Invocation] := constant(msg(nil)),
    req: Array[Nat, Invocation] := constant(msg(nil)),
    resp: Array[Nat, Invocation] := constant(msg(nil))
  transitions
    input invoke(v, n)
      eff req[n] := v
    output respond(r, n)
      pre resp[n] = r /\ resp[n] ~= msg(nil)
      eff req[n] := msg(nil);
          resp[n] := msg(nil)
    internal copy(n)
      eff cache[n] := val(mem)
    internal drop(n)
      eff cache[n] := msg(nil)
    internal perform(n)
      pre req[n] ~= msg(nil) /\ resp[n] = msg(nil) 
          /\ (req[n] ~= msg(read) \/ cache[n] ~= msg(nil)) 
      eff if req[n] = msg(read) then resp[n] := cache[n]
          else mem := req[n].val;
               resp[n] := msg(OK);
               cache := constant(msg(nil))
          fi
  schedule
    states
      die: Nat,
      Node: Nat,                              % represents a client
      read_write: Bool,                       % whether to read or to write
      value: Nat                              % the value to write
    do
      while true do
         die := randomNat(1,4);
         Node := randomNat(1,5);
         read_write := randomBool;
         value := randomNat(1,100);
         if die = 1 /\ req[Node] = msg(nil) then
            if read_write then fire input invoke(msg(read), Node)
            else fire input invoke(val(value), Node)
            fi
         elseif die = 2 /\ resp[Node] ~= msg(nil) then
            fire output respond(resp[Node], Node)
         elseif req[Node] ~= msg(nil) /\ resp[Node] = msg(nil) 
                /\ (req[Node] ~= msg(read) \/ cache[Node] ~= msg(nil))
            then fire internal perform(Node) 
         elseif die = 3 then
            fire internal copy(Node)
         elseif die = 4 then
            fire internal drop(Node)
         fi
      od
    od


%--- 4. simulation relation, with proof block ---%
forward simulation from StrongCache to CentralMem:
   StrongCache.mem  = CentralMem.mem
/\ StrongCache.resp = CentralMem.resp
/\ StrongCache.req  = CentralMem.req
/\ (StrongCache.cache[1] = msg(nil) \/ StrongCache.cache[1].val = CentralMem.mem)
/\ (StrongCache.cache[2] = msg(nil) \/ StrongCache.cache[2].val = CentralMem.mem)
/\ (StrongCache.cache[3] = msg(nil) \/ StrongCache.cache[3].val = CentralMem.mem)
/\ (StrongCache.cache[4] = msg(nil) \/ StrongCache.cache[4].val = CentralMem.mem)
/\ (StrongCache.cache[5] = msg(nil) \/ StrongCache.cache[5].val = CentralMem.mem)
% \A n: Nat (StrongCache.cache[n] = msg(nil) \/ StrongCache.cache[n] = CentralMem.mem)

proof
  initially
    CentralMem.mem  := 0;
    CentralMem.req  := constant(msg(nil));
    CentralMem.resp := constant(msg(nil))

  for input invoke(v: Invocation, n: Nat)
      do fire input invoke(v, n) od
  for output respond(r: Invocation, n: Nat)
      do fire output respond(r, n) od

  for internal copy(n: Nat) ignore
  for internal drop(n: Nat) ignore
  for internal perform(n: Nat)
      do fire internal perform(n) od

%--- 5. simulation relation, with proof block ---%
forward simulation from CentralMem to StrongCache:
   StrongCache.mem  = CentralMem.mem
/\ StrongCache.resp = CentralMem.resp
/\ StrongCache.req  = CentralMem.req
/\ (StrongCache.cache[1] = msg(nil) \/ StrongCache.cache[1].val = CentralMem.mem)
/\ (StrongCache.cache[2] = msg(nil) \/ StrongCache.cache[2].val = CentralMem.mem)
/\ (StrongCache.cache[3] = msg(nil) \/ StrongCache.cache[3].val = CentralMem.mem)
/\ (StrongCache.cache[4] = msg(nil) \/ StrongCache.cache[4].val = CentralMem.mem)
/\ (StrongCache.cache[5] = msg(nil) \/ StrongCache.cache[5].val = CentralMem.mem)
% ideally, \A n: Nat (StrongCache.cache[n] = msg(nil) \/
%                     StrongCache.cache[n] = CentralMem.mem)

proof
  initially
    StrongCache.mem  := 0;
    StrongCache.req  := constant(msg(nil));
    StrongCache.resp := constant(msg(nil));
    StrongCache.cache := constant(msg(nil))
  for input invoke(v: Invocation, n: Nat)
      do fire input invoke(v, n) od
  for output respond(r: Invocation, n: Nat)
      do fire output respond(r, n) od
  for internal perform(n: Nat)
      do fire internal copy(n);
         fire internal perform(n);
         fire internal drop(n)
      od