include "sequence_aux.csp"

--------------------------------------------------------------------
-- The maximum size of the buffer is a strictly positive constant.
maxbuff = 4

-- The values buffered are numbers.
Value = {0..2}

-- It takes its inputs and supplies its outputs on two different
-- typed channels.
channel input, output: Value

ABuffer =
  let BufferState(s)= #s > 0 & output!head(s) -> BufferState(tail(s))
                      []
                      #s < maxbuff & input?x -> BufferState(s ^ <x>)

  within
    BufferState(<>)

--------------------------------------------------------------------
--------------------------------------------------------------------
-- A controller and a ring
--------------------------------------------------------------------
--------------------------------------------------------------------
-- We decompose the original process into two: a controller and a
-- centralised ring.
--------------------------------------------------------------------

--------------------------------------------------------------------
-- The ring
--------------------------------------------------------------------
-- The ring is a circular array, modelled as a sequence whose two
-- ends are considered to be joined.

-- The constant maxring, defined as (maxbuff - 1), gives the bound for
-- the ring.
maxring = maxbuff - 1

-- The communication is bi-directional
datatype Direction = req | ack

CellId = {1 .. maxring}

channel write, read: CellId . Direction . Value

Ring =
  let RingState(s) = write?i.req?x -> write.i.ack.x -> RingState(insert(s,i,x))
                     []
                     read?i.req!at(s,i) -> read.i.ack.at(s,i) -> RingState(s)
  within
    -- The initial state of the ring is actually irrelevant.
    RingState(zeroSeq(maxring))

--------------------------------------------------------------------
-- The controller
--------------------------------------------------------------------
-- The controller keeps a cache, the size of the buffer, and two
-- indices into the ring circular array:~a bottom and a top, to
-- delimit the relevant values.
--
-- There is a subtle situation when the bottom and the top
-- indices coincide; in this case it is not possible to distinguish
-- whether the ring has reached its maximum storage capacity or
-- whether it is empty.  As a consequence, we need to keep a separate
-- record of the size of the buffer, and consequently of the ring.

Controller =
 let ControllerState(cache,size,top,bot) =
       InputController(cache,size,top,bot) [] OutputController(cache,size,top,bot)

     InputController(cache,size,top,bot) =
       size < maxbuff & input?x -> (size == 0 & ControllerState(x,1,top,bot)
                                    []
                                    size > 0 & write.top.req!x -> write.top.ack?dumb ->  ControllerState(cache,size+1,(top%maxring)+1,bot))

     OutputController(cache,size,top,bot) =
       size > 0 & output!cache -> (size > 1 &
-- A requisição de leitura não ser uma "escolha externa (via input on dumb)" para que o processo seja Strong Output Decisive
--                                        read.bot.req?dumb -> read.bot.ack?x -> ControllerState(x,size-1,top,(bot%maxring)+1)
                                        (|~| dumb:Value @ read.bot.req.dumb -> read.bot.ack?x -> ControllerState(x,size-1,top,(bot%maxring)+1))
                                   []
                                   size == 1 & ControllerState(cache,0,top,bot))

 within
 --  The initial value of the cache is irrelevant, since the size is 0.
   ControllerState(0,0,1,1)

--------------------------------------------------------------------
-- The new buffer
--------------------------------------------------------------------

-- The buffer process becomes the parallel composition of the
-- Controller and the Ring.
-- Without hiding the refinement is not caliv

CRBuffer = (Controller [ write <-> write , read <-> read ] Ring) \ {| write, read |}

--------------------------------------------------------------------
-- Asserts
--------------------------------------------------------------------
--assert ABuffer [FD= CRBuffer
--assert CRBuffer [FD= ABuffer

--------------------------------------------------------------------
--------------------------------------------------------------------
-- Distributed buffer
--------------------------------------------------------------------
--------------------------------------------------------------------
-- Each ring cell is implemented as an independent process.

--------------------------------------------------------------------
-- The new ring
--------------------------------------------------------------------
-- A generic cell
channel rd, wrt: Direction . Value

RingCell =
  let CellState(val) =
    rd.req?dumb -> rd.ack!val -> CellState(val) [] wrt.req?x -> wrt.ack?dumb -> CellState(x)
  within
    |~| v:Value @ CellState(v)

-- A generic cell
channel rd_i, wrt_i: CellId . Direction . Value

-- An indexed cell
IRCell(i) = RingCell [[rd <- rd_i.i, wrt <- wrt_i.i]]

-- The distributed ring
DRing = ||| i: CellId @ IRCell(i)

--------------------------------------------------------------------
-- The final buffer
--------------------------------------------------------------------
--DBuffer = (Controller [ write <-> wrt_i , read <-> rd_i ] DRing)
ControllerR = Controller[[ read <- rd_i, write <- wrt_i]]
DBuffer = (ControllerR [| {| rd_i, wrt_i |} |] DRing) \ {| rd_i, wrt_i |}

assert ABuffer [FD= DBuffer
assert DBuffer [FD= ABuffer