--
-- Alternating Bit Protocol
--
-- Sender wants to deliver natural numbers 0,1,2,... to Receiver.
-- Number n denotes the nth packet.
-- But available channels are somehow unreliable. 
-- Packets being sent can be lost and duplicated, but cannot be reordered. 
-- 
-- Sender and Receiver share two channels, say fifo1 and fifo2.
-- fifo1 is used for Sender's sending packets to Receiver.
-- fifo2 is used for Receier's returning acks to Sender.
-- Sender uses a variable, say tag1 that could be up and down as its value.
-- Receier uses a variable, say tag2 that could be up and down as its value.
--
-- Initially both fifo1 and fifo2 are empty, and both tag1 and tag2 are up.
-- Two more variables are used. 
-- One is next denoting the number Sender wants to deliver to Receiver next.
-- The other is list denoting tha list of numbers received by Receiver.
--
-- Sender repeatedly puts the pair of tag1 and next into fifo1 until she
-- gets an ack that equals tag1 from fifo2.
-- If so, Sender flips tag1 and increments next, and repeates the above.
--
-- Receiver repeatedly puts tag2 into fifo2 until she gets an pair <tag,num>
-- such that tag is different from tag2.
-- If so, Receiver puts num into list and flips tag2, and repeates the above. 
--
-- The architecture looks like this
--
--                            + ------+
--                     -----> | fifo1 | ----->
--                            +-------+           
--   Sender(tag1,next)                         Reveiver(tag2,list)  
--                            + ------+        
--                      <---- | fifo2 | <-----
--                            +-------+
--
-- How to model the unreliablity of a channel? 
-- What id affected by the unreliablity can be observed only by getting 
-- the top element of the channel.
-- Therefore, it is sufficient to drop and duplicate the top element of the channel 
-- nondeterministically.
-- You can think that if an element in the middle of the channel is dropped or duplicated, 
-- the effect is delayed until the element becomes top.
--
-- A formal model of the system:
--  - a set of observable values:
--    * 'fifo1' denotes the Sender-to-Receiver channel, initially empty.
--    * 'fifo2' denotes the Receiver-to-Sender channel, initially empty.
--    * 'tag1'  denotes variable tag1, initially up.
--    * 'tag2'  denotes variable tag2, initially up.
--    * 'next'  denotes the number Sender wants to deliver to Receiver next, initially 0.
--    * 'list'  denotes the list of the numbers received by Receiver, initially nil.
--  - a set of transition rules:
--    * 'send1' denotes Sender's putting a pair into fifo1.
--    * 'rec1'  denotes Sender's getting a tag from fifo2.
--    * 'send2' denotes Receiver's putting a tag into fifo2.
--    * 'rec2'  denotes Receiver's getting a pair from fifo1.
--    * 'drop1' denotes the loss of the top pair in fifo1.
--    * 'dup1'  denotes the duplication of the top pair in fifo1.
--    * 'drop2' denotes the loss of the top pair in fifo2.
--    * 'dup2'  denotes the duplication of the top pair in fifo2.
--
--  - The definition of the rules look like this:
--    * send1 : put <tag1,next> into fifo1
--
--    * rec1 : if fifo2 is not empty then
--               let tag be the top in fifo2;
--               remove the top from fifo2;
--               if tag1 != tag then tag1 := tag; next := next + 1;
--               any other values are not changed
--             else
--               any values are not changed
--             fi
--
--    * send2 : put tag2 into fifo2
--
--    * rec2 : if fifo1 is not empty then
--               let <tag,num> be the top in fifo1;
--               remove the top from fifo1;
--               if tag2 = tag then tag2 := flip(tag); put num into list;
--               any other values are not changed
--             else
--               any values are not changed
--             fi
--
--    * drop1 : if fifo1 is not empty then
--                remove the top from fifo1;
--                any other values are not changed
--              else
--                any values are not changed
--              fi
--
--    * dup1 : if fifo1 is not empty then
--               let pair be the top in fifo1;
--               put pair into fifo1;
--               any other values are not changed
--             else
--               any values are not changed
--             fi
--                 
--    * drop2 : if fifo2 is not empty then
--                remove the top from fifo2;
--                any other values are not changed
--              else
--                any values are not changed
--              fi
--
--    * dup2 : if fifo2 is not empty then
--               let tag be the top in fifo2;
--               put tag into fifo2;
--               any other values are not changed
--             else
--               any values are not changed
--             fi
--                 
-- The property that we want to prove is that
--
--   if tag1 = tag2,  then list = [next-1, ..., 0] and
--   if tag1 != tag2, then list = [next, next-1, ..., 0].
--
-- which means that Receiver has really recevied the numbers Sender
-- expects to be received by Receiver in the same order as the
-- numbers have been sent.
--
-- But this doesn't guarantee that the numbers sent by Sender will be
-- eventually received by Receiver, which is a liveness property.
-- To prove this liveness one, we should restrict packet loss and duplication. 
-- Unbounded packet loss and duplication should be prohibited.
--
-- In the literature, you can find proofs that ABP implements a reliable fifo.
-- Usually such a refinement only guarantees that safety properties are
-- preserved, which means that if a specification has a safety property, then 
-- so does an implementation.
--
-- There is a refinement (simulation) relation that preserves liveness
-- properties. 
-- See 'Distributed Algorithms' by Nacy A. Lunch.
--

mod! PNAT {
  [Nat]
  op 0 : -> Nat 
  op s : Nat -> Nat 
  op _=_ : Nat Nat -> Bool {comm}
  vars X Y : Nat 
  eq (X = X) = true .
  eq (0 = 0) = true .
  eq (0 = s(X)) = false .
  eq (s(X) = s(Y)) = (X = Y) .
}

mod! TAGVALUE {
  [Tagvalue]
  ops up down : -> Tagvalue 
  op flip : Tagvalue -> Tagvalue
  op _=_ : Tagvalue Tagvalue -> Bool {comm}
  var V : Tagvalue 
  eq flip(up) = down .
  eq flip(down) = up .
  eq (V = V) = true .
  eq (up = down) = false .
--
  eq (flip(V) = V) = false .
}

mod* EQTRIV {
  [Elt]
  op _=_ : Elt Elt -> Bool {comm}
}
 
mod! PAIR(D1 :: EQTRIV, D2 :: EQTRIV) principal-sort Pair {
  [Pair]
  op <_,_> : Elt.D1 Elt.D2 -> Pair
  op 1st : Pair -> Elt.D1
  op 2nd : Pair -> Elt.D2
  op _=_ : Pair Pair -> Bool {comm}
  var X : Elt.D1
  var Y : Elt.D2
  vars P P1 P2 : Pair
  eq 1st(< X , Y >) = X .
  eq 2nd(< X , Y >) = Y .
  eq (P = P) = true .
  eq (P1 = P2) = (1st(P1) = 1st(P2) and 2nd(P1) = 2nd(P2)) .
}

mod! FIFO(D :: EQTRIV) {
  [Fifo]
-- data constructors
  op empty : -> Fifo 
  op _|_ : Elt.D Fifo -> Fifo
-- operators  
  op put : Fifo Elt.D -> Fifo
  op get : Fifo -> Fifo
  op top : Fifo -> Elt.D
  op empty? : Fifo -> Bool
  op _\in_ : Elt.D Fifo -> Bool
  op _=_ : Fifo Fifo -> Bool {comm}
  op _@_ : Fifo Fifo -> Fifo           -- concatenate two fifos
  op del : Fifo -> Fifo                -- delete the last element
--
  vars X Y Z : Elt.D
  vars F F1 F2 : Fifo
  eq put(empty,X) = X | empty .
  eq put((Y | F),X) = Y |  put(F,X) .
  eq get(X | F) = F .
  eq top(X | F) = X .
  eq empty?(empty) = true .
  eq empty?(X | F) = false .
  eq X \in empty = false .
  ceq X \in (Y | F) = true    if X = Y .
  ceq X \in (Y | F) = X \in F if not(X = Y) .
  eq (F = F) = true .
  eq (empty = (X | F)) = false .
  eq ((X | F1) = (Y | F2)) = (X = Y and F1 = F2) .
  eq empty @ F = F .
  eq (X | F1) @ F2 = X | (F1 @ F2) .
  eq del(put(F,X)) = F .
  eq del(X | empty) = empty .
  eq del(X | Y | F) = X | del(Y | F) .
  eq del(F1 @ (X | F2)) = F1 @ del(X | F2) .
--
  ceq X \in put(F,Y) = true  if X \in F or X = Y .
  ceq X \in put(F,Y) = false if not(X \in F or X = Y) .
  eq put(F1 @ F2,X) = F1 @ put(F2,X) .
  eq empty?(F1 @ F2) = empty?(F1) and empty?(F2) .
  eq (empty = (F1 @ F2)) = (empty = F1) and (empty = F2) .
  eq ((Z | empty) = (F1 @ (X | Y | F2))) = false .
}

mod! LIST {
  pr(PNAT)
  [List]
  op nil : -> List
  op __ : Nat List -> List
  op hd : List -> Nat
  op tl : List -> List 
  op mk : Nat -> List 
  op _=_ : List List -> Bool {comm}
  vars L L1 L2 : List
  vars X Y : Nat
  eq hd(X L) = X .
  eq tl(X L) = L .
  eq mk(0) = 0 nil .
  eq mk(s(X)) = s(X) mk(X) .
  eq (L = L) = true .
  eq (nil = nil) = true .
  eq (nil = X L) = false .
  eq (X L1 = Y L2) = (X = Y and L1 = L2) .
}

mod* ABP {
  pr(PNAT + LIST)
  pr(FIFO(TAGVALUE) * {sort Fifo -> BFifo})
  pr(FIFO(PAIR(TAGVALUE,PNAT)) * {sort Fifo -> PFifo})
  *[System]*
-- any initial state
  op init : -> System
-- observations
  bop fifo1 : System -> PFifo     -- Sender to Receiver channel
  bop fifo2 : System -> BFifo     -- Receiver to Sender channel
  bop tag1  : System -> Tagvalue  -- Sender's tag
  bop tag2  : System -> Tagvalue  -- Receiver's tag
  bop next  : System -> Nat       -- the number Sender wants to deliver 
  bop list  : System -> List      -- the numbers received by Receiver
-- actions
  bop send1 : System -> System -- Sender's sending numbers
  bop rec1  : System -> System -- Sender's receiving acks
  bop send2 : System -> System -- Receiver's sending acks
  bop rec2  : System -> System -- Receiver's receiving numbers
  bop drop1 : System -> System -- drop the 1st of fifo1
  bop dup1  : System -> System -- duplicate the 1st of fifo1
  bop drop2 : System -> System -- drop the 1st of fifo2
  bop dup2  : System -> System -- duplicate the 1st of fifo2
-- CafeOBJ variables
  var S : System
-- for initial state
  eq fifo1(init) = empty .
  eq fifo2(init) = empty .
  eq tag1(init)  = up .
  eq tag2(init)  = up .
  eq next(init)  = 0 .
  eq list(init)  = nil .
-- send1
  eq fifo1(send1(S)) = put(fifo1(S),< tag1(S) , next(S) >) .
  eq fifo2(send1(S)) = fifo2(S) .
  eq tag1(send1(S))  = tag1(S) .
  eq tag2(send1(S))  = tag2(S) .
  eq next(send1(S))  = next(S) .
  eq list(send1(S))  = list(S) .
-- rec1
  op c-rec1 : System -> Bool {strat: (0 1)}
  eq c-rec1(S) = not empty?(fifo2(S)) .
  --
  eq  fifo1(rec1(S)) = fifo1(S) .
  ceq fifo2(rec1(S)) = get(fifo2(S)) if c-rec1(S) .
  ceq tag1(rec1(S))
      = (if tag1(S) = top(fifo2(S)) then tag1(S) else top(fifo2(S)) fi)
      if c-rec1(S) .
  eq  tag2(rec1(S))  = tag2(S) .
  ceq next(rec1(S))  
      = (if tag1(S) = top(fifo2(S)) then next(S) else s(next(S)) fi)
      if c-rec1(S) .
  eq  list(rec1(S))  = list(S) .
  ceq rec1(S)        = S if not c-rec1(S) .
-- send2
  eq fifo1(send2(S)) = fifo1(S) .
  eq fifo2(send2(S)) = put(fifo2(S),tag2(S)) .
  eq tag1(send2(S))  = tag1(S) .
  eq tag2(send2(S))  = tag2(S) .
  eq next(send2(S))  = next(S) .
  eq list(send2(S))  = list(S) .
-- rec2
  op c-rec2 : System -> Bool {strat: (0 1)}
  eq c-rec2(S) = not empty?(fifo1(S)) .
  --
  ceq fifo1(rec2(S)) = get(fifo1(S)) if c-rec2(S) .
  eq  fifo2(rec2(S)) = fifo2(S) .
  eq  tag1(rec2(S))  = tag1(S) .
  ceq tag2(rec2(S))  
      = (if tag2(S) = 1st(top(fifo1(S))) then flip(1st(top(fifo1(S)))) else tag2(S) fi)
      if c-rec2(S) .
  eq  next(rec2(S))  = next(S) .
  ceq list(rec2(S))  
      = (if tag2(S) = 1st(top(fifo1(S))) then (2nd(top(fifo1(S))) list(S)) else list(S) fi) 
      if c-rec2(S) .
  ceq rec2(S)        = S if not c-rec2(S) .
-- drop1
  op c-drop1 : System -> Bool {strat: (0 1)}
  eq c-drop1(S) = not empty?(fifo1(S)) .
  --
  ceq fifo1(drop1(S)) = get(fifo1(S)) if c-drop1(S) .
  eq  fifo2(drop1(S)) = fifo2(S) .
  eq  tag1(drop1(S))  = tag1(S) .
  eq  tag2(drop1(S))  = tag2(S) .
  eq  next(drop1(S))  = next(S) .
  eq  list(drop1(S))  = list(S) .
  ceq drop1(S)        = S if not c-drop1(S) .
-- dup1
  op c-dup1 : System -> Bool {strat: (0 1)}
  eq c-dup1(S) = not empty?(fifo1(S)) .
  --
  ceq fifo1(dup1(S)) = top(fifo1(S)) | fifo1(S) if c-dup1(S) .
  eq  fifo2(dup1(S)) = fifo2(S) .
  eq  tag1(dup1(S))  = tag1(S) .
  eq  tag2(dup1(S))  = tag2(S) .
  eq  next(dup1(S))  = next(S) .
  eq  list(dup1(S))  = list(S) .
  ceq dup1(S)        = S if not c-dup1(S) .
-- drop2
  op c-drop2 : System -> Bool {strat: (0 1)}
  eq c-drop2(S) = not empty?(fifo2(S)) .
  --
  eq  fifo1(drop2(S)) = fifo1(S) .
  ceq fifo2(drop2(S)) = get(fifo2(S)) if c-drop2(S) .
  eq  tag1(drop2(S))  = tag1(S) .
  eq  tag2(drop2(S))  = tag2(S) .
  eq  next(drop2(S))  = next(S) .
  eq  list(drop2(S))  = list(S) .
  ceq drop2(S)        = S if not c-drop2(S) .
-- dup2
  op c-dup2 : System -> Bool {strat: (0 1)}
  eq c-dup2(S) = not empty?(fifo2(S)) .
  --
  eq  fifo1(dup2(S)) = fifo1(S) .
  ceq fifo2(dup2(S)) = top(fifo2(S)) | fifo2(S) if c-dup2(S) .
  eq  tag1(dup2(S))  = tag1(S) .
  eq  tag2(dup2(S))  = tag2(S) .
  eq  next(dup2(S))  = next(S) .
  eq  list(dup2(S))  = list(S) .
  ceq dup2(S)        = S if not c-dup2(S) .
}

eof

--
-- simulations
--
open ABP
  op s1 : -> System .
  eq s1 = send1(rec1(send2(rec2(send1(rec1(send2(rec2(send1(init))))))))) .
  red fifo1(s1) .
  red fifo2(s1) .
  red tag1(s1) .
  red tag2(s1) .
  red next(s1) .
  red list(s1) .
close