module TYPES is

-------------------------------------------------------------------------------
-- type Nat3
-------------------------------------------------------------------------------

type Nat3 is
   0, 1, 2
   with ==, <>, <, <=, >, >=
end type

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

function + (n1, n2: Nat3) : Nat3 is
   case n1, n2 var m: Nat3 in
      m, 0 -> return m
   |  0, m -> return m
   |  1, 1 -> return 2
   |  1, 2 -> return 0  -- 1 + 2 reaches 0 again
   |  2, 1 -> return 0  -- 2 + 1 reaches 0 again
   |  any, any -> raise UNEXPECTED
   end case
end function

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

function - (n1, n2: Nat3) : Nat3 is
   case n1, n2 var m: Nat3 in
      m, 0 -> return m
   |  1, 1 -> return 0
   |  2, 1 -> return 1
   |  2, 2 -> return 0
   |  any, any -> raise UNEXPECTED
   end case
end function

-------------------------------------------------------------------------------
-- type Message1
-------------------------------------------------------------------------------

type Message1 is
   init_leader,
   final_leader,
   bus_reset_start,
   bus_reset_end,
   bus_reset_event,
   power_change,
   GUID_list,
   empty
end type

-------------------------------------------------------------------------------
-- type Message2
-------------------------------------------------------------------------------

type Message2 is
   DMInitRequest,
   DMInitReply
   with ==, <>
end type

-------------------------------------------------------------------------------
-- type MesFrame (only used by the asynchronous specification HAVi_asyn)
-------------------------------------------------------------------------------

type MesFrame is
   consm (msg: Message2, Id: Nat3, UrlCapable: bool)
   with get
end type

-------------------------------------------------------------------------------
-- type Node
-------------------------------------------------------------------------------

type Node is
   consn (val: bool)
   with get
end type

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

function count_up (n: Node) : Nat3 is
   case n.val of bool in
      true -> return 1
   |  false -> return 0
   end case
end function

-------------------------------------------------------------------------------
-- type Network
-------------------------------------------------------------------------------

type Network is
   consnet (n1, n2: Node)
   with get
end type

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

function net_down: Network is
   return consnet (consn (false), consn (false))
end function
-------------------------------------------------------------------------------

function nr_uphosts (nt: Network) : Nat3 is
   return count_up (nt.n1) + count_up (nt.n2)
end function

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

function flip (n: Nat3, nt: Network) : Network is
   case n in
      0 -> raise UNEXPECTED
   |  1 -> return consnet (consn (not (nt.n1.val)), nt.n2)
   |  2 -> return consnet (nt.n1, consn (not (nt.n2.val)))
   end case
end function

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

function i_leader (nt: Network) : Nat3 is
   if nt.n1.val then
      return 1
   elsif nt.n2.val then
      return 2
   else
      return 0
   end if
end function

-------------------------------------------------------------------------------
-- type Host
-------------------------------------------------------------------------------

type Host is
   consh (Id: Nat3, UrlCapable: bool, rec_req: bool)
   with get, ==, <>
end type

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

type Hosts is
   list of Host
   with ==, <>, head, tail
end type

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

function init_hosts (nt: Network) : Hosts is
   var r: Hosts in
      r := nil;
      if nt.n2.val then
         r := cons (consh (2, false, false), r)
      end if;
      if nt.n1.val then
         r := cons (consh (1, false, false), r)
      end if;
      return r
   end var
end function

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

function chge_rec (n: Nat3, b: bool, hl: Hosts) : Hosts is
   case hl var hd: Host, tl: Hosts in
      nil -> return nil
   |  cons (hd, tl) ->
         if n <> hd.Id then
            return cons (hd, chge_rec (n, b, tl))
         else
            return cons (consh (n, b, true), tl)
         end if
   end case
end function

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

function rec (n: Nat3, hl: Hosts) : bool is
   case hl var hd: Host, tl: Hosts in
      nil -> return true
   |  cons (hd, tl) ->
         if n <> hd.Id then
            return rec (n, tl)
         else
            return hd.rec_req
         end if
   end case
end function

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

function f_leader (n: Nat3, hl: Hosts) : Nat3 is
   case hl var hd: Host, tl: Hosts in
      nil -> return n
   |  cons (hd, tl) ->
         if not (hd.UrlCapable) then
            return f_leader (n, tl)
         else
            return hd.Id
         end if
   end case
end function

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

end module