--
-- Let us consider the following system.
-- The system consists of three processes: Sender, Receiver and
-- Stealer.
-- Sender wants to deliver natural numbers 0,1,2,... to Receiver.
-- Sender sends the numbers to Recevier via a cell.
-- Sender puts a number in the cell, and Receiver gets a number from
-- the cell if the cell is not empty. 
-- But Stealer can steal a number from the cell.
-- Can Sender deliver the numbers to Receiver without any loss and
-- any duplication? 
--
-- Sender and Receiver share a boolena variable, say flag.
-- flag is initially false.
-- Sender repeatedly puts a number in the cell while flag is false.
-- If Sender gets a number from the cell, it sets flag to true.
-- If flag is true, Sender picks the next number and sets flag to
-- false.
--
-- A formal model of the system:
--  - a set of observable values:
--    * 'cell' denotes the cell, initially empty.
--    * 'flag' denotes variable flag, initially false.
--    * 'next' denotes the number Sender wants to deliver to Receiver next.
--    * 'list' denotes the list of the numbers received by Receiver.
--  - a set of transition rules:
--    * 'send'    denotes Sender's putting a number in the cell.
--    * 'receive' denotes Receiver's getting a number from the cell.
--    * 'steal'   denotes Stealer's stealing a number from the cell.
--    * 'update'  denotes Sender's choosing the next number.
--
--  - The effective conditions of the rules:
--    * 'c-send'    : flag is false.
--    * 'c-receive' : cell is not empty.
--    * 'c-steal'   : cell is not empty.
--    * 'c-update'  : flag is true.
--
--  - The definitions of the rules look like this:
--    * send : if not flag then
--               put next in cell;
--               any other values are not changed.
--             else
--               any values are not changed
--             fi
--
--    * receive : if cell is not empty then
--                  get the number from cell;
--                  flag := true;
--                  put the number in list;
--                  any other values are not changed
--                else
--                  any values are not changed
--                fi
--
--    * steal : if cell is not empty then
--                get the number from the cell;
--                any other values are not changed
--              else
--                any values are not changed
--              fi
--
--    * update : if flag then
--                 flag := false;
--                 next := next + 1;
--                 any other values are not changed
--               else
--                 any values are not changed
--               fi
--
-- The property that we want to prove is that
--
--   if flag is true,  then list = [next, next-1, ..., 0] and
--   if flag is false, then list = [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.
--
-- This protocol is a very simplified Alternating Bit Protocol.
--

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! CELL {
  pr(PNAT)
  [Cell]
  op empty : -> Cell
  op c : Nat -> Cell
  op content : Cell -> Nat
  op empty? : Cell -> Bool
  op _=_ : Cell Cell -> Bool {comm}
  var C : Cell
  vars X Y : Nat
  eq content(c(X)) = X .
  eq empty?(empty) = true .
  eq empty?(c(X)) = false .
  eq (C = C) = true .
  eq (empty = empty) = true .
  eq (empty = c(X)) = false .
  eq (c(X) = c(Y)) = (X = Y) .
}

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* SP {
  pr(PNAT + CELL + LIST)
  *[System]*
-- any initial state
  op init : -> System
-- observations
  bop cell : System -> Cell
  bop flag : System -> Bool
  bop next : System -> Nat
  bop list : System -> List
-- actions
  bop send    : System -> System
  bop receive : System -> System
  bop steal   : System -> System
  bop update  : System -> System
-- CafeOBJ variables
  var S : System
-- for any initial state
  eq cell(init) = empty .
  eq flag(init) = false .
  eq next(init) = 0 .
  eq list(init) = nil .
-- send
  op c-send : System -> Bool {strat: (0 1)}
  eq c-send(S) = not flag(S) .
  --
  ceq cell(send(S)) = c(next(S)) if c-send(S) .
  eq  flag(send(S)) = flag(S) .
  eq  next(send(S)) = next(S) .
  eq  list(send(S)) = list(S) .
  ceq send(S)       = S          if not c-send(S) .
-- receive
  op c-receive : System -> Bool {strat: (0 1)}
  eq c-receive(S) = not empty?(cell(S)) .
  --
  ceq cell(receive(S)) = empty                    if c-receive(S) .
  ceq flag(receive(S)) = true                     if c-receive(S) .
  eq  next(receive(S)) = next(S) .
  ceq list(receive(S)) = content(cell(S)) list(S) if c-receive(S) .
  ceq receive(S)       = S                        if not c-receive(S) .
-- steal
  op c-steal : System -> Bool {strat: (0 1)}
  eq c-steal(S) = not empty?(cell(S)) .
  --
  ceq cell(steal(S)) = empty if c-steal(S) .
  eq  flag(steal(S)) = flag(S) .
  eq  next(steal(S)) = next(S) .
  eq  list(steal(S)) = list(S) .
  ceq steal(S)       = S     if not c-steal(S) .
-- update
  op c-update : System -> Bool {strat: (0 1)}
  eq c-update(S) = flag(S) .
  --
  eq  cell(update(S)) = cell(S) .
  ceq flag(update(S)) = false      if c-update(S) .
  ceq next(update(S)) = s(next(S)) if c-update(S) .
  eq  list(update(S)) = list(S) .
  ceq update(S)       = S          if not c-update(S) .
}

eof

--
-- Simulations
--
open SP
  ops s1 s2 : -> System .
  eq s1 = send(receive(steal(send(update(receive(send(init))))))) .
  eq s2 = receive(steal(send(update(receive(s1))))) .
  red next(s1) .
  red list(s1) .
  red next(s2) .
  red list(s2) .
close