module DATAP is

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

type Reference is
   range 0 ... 2 of Nat
   with == !library, != !library, <= !library
end type

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

type Product is
   range 0 ... 2 of Nat
   with == !library, != !library, <=
end type

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

type Amount is
   range 0 ... 255 of Nat
   with == !library, != !library, < !library, <=, >, >= !library
end type

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

function + (n1, n2: Amount) : Amount is
   -- returns (n1 + n2) mod 256, to imitate the original LOTOS specification
   var n: Nat in
      n := (Nat (n1) + Nat (n2)) mod 256;
      return Amount (n)
   end var
end function

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

function - (n1, n2: Amount) : Amount is
   if n1 > n2 then
      return Amount (Nat (n1) - Nat (n2))
   else
      return 0 of Amount
   end if
end function

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

type Status is
   None, Pending, Invoiced
   with ==, != !library
end type

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

end module