type My_Natural is Boolean
   sorts Nat 
   opns 0 (*! constructor *),
        1 (*! constructor *), 
        2 (*! constructor *) : -> Nat
        _+_ ,
        _-_ : Nat, Nat -> Nat
	_==_ ,
        _<>_ ,
	_<_ ,
	_<=_ ,
	_>_ ,
	_>=_ : Nat, Nat -> Bool
   eqns
      forall m, n : Nat
      ofsort Nat
         m + 0 = m;
         0 + m = m;
         1 + 1 = 2;
         1 + 2 = 0;  (* 1 + 2 reaches 0 again *)
         2 + 1 = 0;  (* 2 + 1 reaches 0 again *)
      ofsort Nat
         m - 0 = m;
         1 - 1 = 0;
         2 - 1 = 1;
         2 - 2 = 0;
         (* otherwise: no equation => run-time exception *)
      ofsort Bool
         m == m             = true;
         (* otherwise *)
         m == n             = false;
      ofsort Bool
         m <> n             = not (m == n);
      ofsort Bool
         0 < 1              = true;
         0 < 2              = true;
         1 < 2              = true;
         (* otherwise *)
         m < n              = false;
      ofsort Bool
         m <= n             = (m < n) or (m == n);
      ofsort Bool
         m >= n             = not (m < n);
      ofsort Bool
         m > n              = not (m <= n);
endtype

(* ------------------------------------------------------------------------- *)

type MessageConstructors is BOOLEAN, MY_NATURAL
   sorts Message1, Message2
   opns
     init_leader     (*! constructor *),
     final_leader    (*! constructor *),
     bus_reset_start (*! constructor *),
     bus_reset_end   (*! constructor *),
     bus_reset_event (*! constructor *),
     power_change    (*! constructor *),
     GUID_list       (*! constructor *),
     empty           (*! constructor *) : -> Message1

     DMInitRequest (*! constructor *) : -> Message2
     DMInitReply     (*! constructor *) : -> Message2
endtype

(* ------------------------------------------------------------------------- *)

type Node is BOOLEAN, MY_NATURAL
   sorts Node
   opns
     consn (*! constructor *) : Bool -> Node
     up   : Node -> Bool
     count_up : Node -> Nat
   
   eqns forall n:Node, b1,b2:Bool
        ofsort Bool
           up(consn(b2)) = b2;
        ofsort Nat
           up(n) => count_up(n) = 1;
           not(up(n)) => count_up(n) = 0;
endtype

(* ------------------------------------------------------------------------- *)

type NodeTuple is Node
  sorts Network
  opns
    consnet (*! constructor *) : Node, Node -> Network
    firstn  : Network -> Node
    secondn : Network -> Node

  eqns forall   l : Network,
                n1,n2 : Node
       ofsort Node
          firstn(consnet(n1,n2))  = n1;
          secondn(consnet(n1,n2))  = n2;
endtype

(* ------------------------------------------------------------------------- *)

type EnrichedNodeTuple is NodeTuple
   opns
     nr_uphosts : Network -> Nat
     flip : Nat, Network -> Network
     i_leader: Network -> Nat
   eqns forall n1,n2: Node
        ofsort Network
           flip(1,consnet(n1,n2))
               = consnet(consn(not(up(n1))),n2);
           flip(2,consnet(n1,n2))
               = consnet(n1,consn(not(up(n2))));
        ofsort Nat
           nr_uphosts(consnet(n1,n2))
               = count_up(n1) + count_up(n2);
           up(n1) => i_leader(consnet(n1,n2)) = 1;
           not(up(n1)) and up(n2) => i_leader(consnet(n1,n2)) = 2;
           not(up(n1)) and not(up(n2)) =>
               i_leader(consnet(n1,n2)) = 0;
endtype

(* ------------------------------------------------------------------------- *)

type Host is BOOLEAN, MY_NATURAL
   sorts Host
   opns
     consh (*! constructor *) : Nat, Bool, Bool -> Host
     id      : Host -> Nat
     UrlCapable   : Host -> Bool
     rec_req : Host -> Bool
   
   eqns forall n:Nat, b1:Bool, b2:Bool
        ofsort Nat
           id(consh(n,b1,b2)) = n
        ofsort Bool
           UrlCapable(consh(n,b1,b2)) = b1;
           rec_req(consh(n,b1,b2)) = b2
endtype

(* ------------------------------------------------------------------------- *)

type HostList is Host
  sorts Hosts
  opns
    emptyh  (*! constructor *) : -> Hosts
    addh    (*! constructor *) : Host, Hosts -> Hosts
    headh   : Hosts -> Host
    tailh   : Hosts -> Hosts

  eqns forall   l : Hosts,
                e : Host

       ofsort Host
          headh(addh(e,l))  = e

       ofsort Hosts
          tailh(emptyh)     = emptyh;
          tailh(addh(e,l))  = l
endtype

(* ------------------------------------------------------------------------- *)

type EnrichedHostList is HostList, EnrichedNodeTuple
   opns
     _==_: Hosts, Hosts -> Bool
     _<>_: Hosts, Hosts -> Bool
     init_hosts: Network -> Hosts
     chge_rec: Nat, Bool, Hosts -> Hosts
     rec: Nat, Hosts -> Bool
     f_leader: Nat, Hosts -> Nat
   eqns forall host,host1,host2: Host, hosts,hosts1,hosts2: Hosts,
               n1,n2:Node, n:Nat, b:Bool
        ofsort Bool
           emptyh == emptyh = true;
           addh(host,hosts) == emptyh = false;
           emptyh == addh(host,hosts) = false;
           addh(host1,hosts1) == addh(host2,hosts2)
           = ((id(host1)==id(host2)) and ((UrlCapable(host1) iff UrlCapable(host2))
             and ((rec_req(host1) iff rec_req(host2)) and (hosts1==hosts2))));
           hosts1 <> hosts2 = not(hosts1 == hosts2);
        ofsort Hosts
           not(up(n1)) and not(up(n2)) =>
             init_hosts(consnet(n1,n2))
               = emptyh;
           not(up(n1)) and up(n2) =>
             init_hosts(consnet(n1,n2))
               = addh(consh(2,false,false),emptyh);
           up(n1) and not(up(n2)) =>
             init_hosts(consnet(n1,n2))
               = addh(consh(1,false,false),emptyh);
           up(n1) and up(n2) =>
             init_hosts(consnet(n1,n2))
               = addh(consh(1,false,false),
                 addh(consh(2,false,false),emptyh));
           chge_rec(n,b,emptyh) = emptyh;
           (n <> id(host)) =>
               chge_rec(n,b,addh(host,hosts)) = addh(host,chge_rec(n,b,hosts));
           (n == id(host)) =>
               chge_rec(n,b,addh(host,hosts)) = addh(consh(n,b,true),hosts)
        ofsort Bool
               rec(n,emptyh) = true;	
           (n<>id(host)) =>
               rec(n,addh(host,hosts)) = rec(n,hosts);
           (n==id(host)) =>
               rec(n,addh(host,hosts)) = rec_req(host)
        ofsort Nat
           f_leader(n,emptyh) = n;
           not(UrlCapable(host)) =>
               f_leader(n,addh(host,hosts)) = f_leader(n,hosts);
           UrlCapable(host) =>
               f_leader(n,addh(host,hosts)) = id(host)
endtype

(* ------------------------------------------------------------------------- *)