datatype Msg = M1 | M2 | M3 | M4 | M5

nametype Bit = {0, 1}

channel send, transmit: Bit.Msg
channel ack, resp: Bit

channel in, out: Msg


-- Specification to be satisfied: overall, the system behaves like a buffer
SPEC = in?x -> out!x -> SPEC

------------------------------------------------------------------------
-- The communication medium
------------------------------------------------------------------------

-- A generic definition of an unreliable channel

UC(l,r) = l?x -> UC'(l,r,x)

UC'(l,r,x) =    r!x -> UC(l,r)            -- correct transmission
           |~|  r!x -> UC'(l,r,x)         -- message duplication 
           |~|  UC(l,r)                   -- message loss

-- The communication medium comprises two unreliable channels.

C1 = UC(send,transmit)
C2 = UC(resp,ack)

CommMedium = C1 ||| C2

------------------------------------------------------------------------
-- The sender and receiver
------------------------------------------------------------------------

-- The sender, wanting to transmit a message using bit b

S(b) = in?x -> send.b.x -> S'(b,x)

S'(b,x) = send.b.x -> S'(b,x)
       [] ack.(1-b) -> send.b.x -> S'(b,x)
       [] ack.b -> S(1-b)

-- The receiver, expecting a message with bit b

R(b) = transmit.(1-b)?x -> resp.(1-b) -> R(b)
    [] transmit.b?x -> (resp.b -> out.x -> R(1-b)
                        []
                        out.x -> resp.b -> R(1-b) )


------------------------------------------------------------------------
-- The System
------------------------------------------------------------------------

--       Both sender & receiver start out using bit 0

SA = {| send, ack |}          -- sender's possible interactions
TR = {| transmit, resp|}      -- receiver's possible interactions


System =  S(0) [| SA |] (CommMedium [| TR |] R(0) )

-- The system, with only in and out events visible
HideSystem = System\ diff(Events,{|in,out|})


------------------------------------------------------------------------
------------------------------------------------------------------------
--  Finally, what we want to prove!
------------------------------------------------------------------------
------------------------------------------------------------------------

-- The following assertion states: The system behaves like a buffer
assert SPEC [T= HideSystem

-- The following assertion states: The system doesn't deadlock
assert System :[ deadlock free ]