module DATA is

!update "2021-b"

------------------------------------------------------------------------------

type ADR is
   range 1..3 of NAT
end type

------------------------------------------------------------------------------

type MSG is
   range 1..3 of NAT
   with ==, >, >=
end type

------------------------------------------------------------------------------

function N: MSG is
   return 3 of MSG
end function

------------------------------------------------------------------------------

function <+> (X, Y: MSG): MSG is
   var RESULT: NAT in
      RESULT := NAT (X) + NAT (Y);
      assert RESULT <= 2 * NAT (N);
      if RESULT > NAT (N) then
         RESULT := RESULT - NAT (N)
      end if;
      return MSG (RESULT)
   end var
end function

------------------------------------------------------------------------------

function <-> (X, Y: MSG): MSG is
   var RESULT: NAT in
      RESULT := NAT (X);
      if RESULT <= NAT (Y) then
         RESULT := RESULT + NAT (N)
      end if;
      return MSG (RESULT - NAT (Y))
   end var
end function

------------------------------------------------------------------------------

type TYPEMSG is
   FIRST, SECOND
end type

-------------------------------------------------------------------------------

channel DEP_CHANNEL is
   (M: MSG)
end channel

-------------------------------------------------------------------------------

channel CRH_CHANNEL is
   (A: ADR)
end channel

-------------------------------------------------------------------------------

channel GET_CHANNEL is
   (A: ADR, M: MSG)
end channel

-------------------------------------------------------------------------------

channel MSG_CHANNEL is
   (M: MSG, T: TYPEMSG)
end channel

-------------------------------------------------------------------------------

end module