module DATA is

type CHECK is
   bottom, check
   with =, <>
end type

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

type DATA is
   d1 -- , d2, ... for verification, this type is restricted to a single value
   with =, <>
end type

function crc (d: DATA): CHECK is
   use d; -- this parameter was not used in the LOTOS specification
   return check
end function

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

type HEADER is
   h1 -- , h2, ... for verification, this type is restricted to a single value
   with =, <>
end type

function crc (h: HEADER): CHECK is
   use h; -- this parameter was not used in the LOTOS specification
   return check
end function

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

type ACK is
   a1 -- , a2, ... for verification, this type is restricted to a single value
   with =, <>
end type

function crc (a: ACK): CHECK is
   use a; -- this parameter was not used in the LOTOS specification
   return check
end function

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

type BOC is
   release, hold, no_op
   with =
end type

type PHY_AREQ is
   fair, immediate
   with =
end type

type PHY_ACONF is
   won, lost
   with =
end type

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

type SIGNAL is
   destsig (dest: Nat),
   headsig (head: HEADER, crc: CHECK),
   datasig (data: DATA, crc: CHECK),
   acksig (ack: ACK, crc: CHECK),
   dhead,
   Start,
   End,
   Prefix,
   subactgap,
   Dummy
   with =, <>, get, set
end type

function is_dest (s: SIGNAL) : Bool is
   case s in
      destsig (any nat) -> return true
   |  any -> return false
   end case
end function

function is_header (s: SIGNAL) : Bool is
   case s in
      headsig (any HEADER, any CHECK) -> return true
   |  any -> return false
   end case
end function

function is_data (s: SIGNAL) : Bool is
   case s in
      datasig (any DATA, any CHECK) -> return true
   |  any -> return false
   end case
end function

function is_ack (s: SIGNAL) : Bool is
   case s in
      acksig (any ACK, any CHECK) -> return true
   |  any -> return false
   end case
end function

function is_physig (s: SIGNAL) : Bool is
   case s in
      Start | End | Prefix | subactgap -> return true
   |  any -> return false
   end case
end function

function valid_hpart (s: SIGNAL) : Bool is
   return is_header (s) and then (s.crc = check)
end function

function valid_ack (s: SIGNAL) : Bool is
   return is_ack (s) and then (s.crc = check)
end function

function getdest (s: SIGNAL) : Nat is
   return s .[UNEXPECTED] dest
end function

function getdcrc (s: SIGNAL) : CHECK is
   assert is_data (s);
   return s .[UNEXPECTED] crc
end function

function getdata (s: SIGNAL) : DATA is
   return s .[UNEXPECTED] data
end function

function gethead (s: SIGNAL) : HEADER is
   return s .[UNEXPECTED] head
end function

function getack (s: SIGNAL) : ACK is
   return s .[UNEXPECTED] ack
end function

function corrupt (s: SIGNAL) : SIGNAL is
   case s in
      headsig (any HEADER, any CHECK) -> return s.{crc -> bottom}
   |  datasig (any DATA, any CHECK) -> return s.{crc -> bottom}
   |  acksig (any ACK, any CHECK) -> return s.{crc -> bottom}
   |  any -> raise UNEXPECTED
   end case
end function

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

type SIG_TUPLE is
   quadruple (dh, dest, header, data: SIGNAL),
   void
   with get
end type

function is_void (s: SIG_TUPLE) : Bool is
   case s in
      void -> return true
   |  any -> return false
   end case
end function

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

type LIN_DCONF is
   ackrec (a: ACK),
   ackmiss,
   broadsent
end type

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

type LIN_DIND is
   good (h: HEADER, d: DATA),
   broadrec (h: HEADER, d: DATA),
   dcrc_err (h: HEADER)
end type

function is_broadrec (x: LIN_DIND) : Bool is
   case x in
      broadrec (any HEADER, any DATA) -> return true
   |  any -> return false
   end case
end function

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

type BoolTABLE is
   empty,
   btable (index: Nat, value: Bool, next: BoolTABLE)
   with =, get
end type

function init (n: Nat) : BoolTABLE is
   -- returns a table of size n initialized to false
   if n = 0 then
      return empty
   else
      return btable (n - 1, false, init (n - 1))
   end if
end function

function zero (t: BoolTABLE) : Bool is
   -- returns true iff no value in t is true
   if t = empty then
      return true
   elsif t.value then
      return false
   else
      return zero (t.next)
   end if
end function

function one (t: BoolTABLE) : Bool is
   -- returns true iff exactly one value in t is true
   if t = empty then
      return false
   elsif t.value then
      return zero (t.next)
   else
      return one (t.next)
   end if
end function

function more (t: BoolTABLE) : Bool is
   -- returns true iff more than one value in t is true
   return not (zero (t)) and not (one (t))
end function

function get (n: Nat, t: BoolTABLE) : Bool is
   -- returns the value associated with index n in t
   if t = empty then
      raise UNEXPECTED
   elsif t.index = n then
      return t.value
   else
      return get (n, t.next)
   end if
end function

function invert (n: Nat, t: BoolTABLE) : BoolTABLE is
   -- returns in which the value associated with index n is negated
   if t = empty then
      return empty
   elsif t.index = n then
      return btable (t.index, not (t.value), t.next)
   else
      return btable (t.index, t.value, invert (n, t.next))
   end if
end function

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

type Version is
   ko, ok
end type

type Scenario is
   scenario_1, scenario_2, scenario_3_2, scenario_3_3, scenario_3_4
   with =
end type

function requests (s: Scenario): Nat is
   case s in
      scenario_3_2 -> return 2
   |  scenario_3_3 -> return 3
   |  scenario_3_4 -> return 4
   |  any -> raise UNEXPECTED
   end case
end function

end module