module DATA is

!library

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

type FRAME is
   -- message frames
   TOKEN, CLAIM
end type

type STATE is
   -- state values
   ALPHA, BETA, GAMMA
   with ==, !=
end type

type ADDR is
   -- addresses of stations
   A1, A2, A3
   with ==, !=, <, >, <=, >=
end type

type ADDR_SET is
   set of ADDR
   with ==, member, remove
end type

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

function WHOLE_SET : ADDR_SET is
   return { A1, A2, A3 }
end function

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

channel ACCESS is
   (A : ADDR)
end channel

channel PORT is
   (F : FRAME),
   (F : FRAME, A : ADDR),
   (F : FRAME, A : ADDR, B : BOOL)
end channel

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

end module