library BOOLEAN, NATURAL endlib

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

type RENAMED_NATURAL is NATURAL
renamedby
   sortnames Nat_8 for Nat
   opnnames Plus for +
endtype

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

type NATURAL_8 is BOOLEAN, RENAMED_NATURAL

opns 
   _+_ : Nat_8, Nat_8 -> Nat_8

eqns
   forall n1, n2 : Nat_8

   ofsort Nat_8
      n1 + n2 = (n1 Plus n2) mod 8;
endtype

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

type PROCESS_ID is NATURAL
renamedby sortnames Identity for Nat 
endtype

type TOPOLOGY is BOOLEAN, PROCESS_ID, NATURAL, NATURAL_8

sorts Identity_List

opns
   Nil (*! constructor *) : -> Identity_List
   Cons (*! constructor *),
   Insert : Identity, Identity_List -> Identity_List
   Length : Identity_List -> Nat
   Member : Identity, Identity_List -> Bool

   Connect, Neighbour : Identity, Identity -> Bool
   Number_Neighbours : Identity -> Nat
   Number_Neighbours_Aux : Identity, Identity -> Nat
   Weight : Identity -> Nat_8

eqns
   forall id1, id2 : Identity,
          ids : Identity_List

   ofsort Identity_List
      (* Insert keeps Identity_List canonical by sorting its elements *)
      Insert (id1, Nil) = Cons (id1, Nil);
      id1 lt id2 =>
         Insert (id1, Cons (id2, ids)) = 
            Cons (id1, Cons (id2, ids));
      Insert (id1, Cons (id2, ids)) = 
         Cons (id2, Insert (id1, ids));

   ofsort Nat
      Length (Nil) = 0 of Nat;
      Length (Cons (id1, ids)) = Length (ids) + 1 of Nat;

   ofsort Bool
      Member (id1, Nil) = false;
      id1 eq id2 => 
         Member (id1, Cons (id2, ids)) = true;
      Member (id1, Cons (id2, ids)) = Member (id1, ids);

   ofsort Nat
      Number_Neighbours (id1) = Number_Neighbours_Aux (id1, 0 of Identity);

   ofsort Nat
      id2 ge 6 of Identity =>
         Number_Neighbours_Aux (id1, id2) = 0 of Nat;
      Neighbour (id1, id2) =>
         Number_Neighbours_Aux (id1, id2) = 
            1 of Nat + Number_Neighbours_Aux (id1, Succ (id2));
      Number_Neighbours_Aux (id1, id2) =
         Number_Neighbours_Aux (id1, Succ (id2));

   ofsort Bool
      (* 
       * do not modify this definition, change the Connect() operation instead
       * Neighbour() is the symmetrical and anti-reflexive closure of Connect()
       *)
      id1 eq id2 =>
         Neighbour (id1, id2) = false;
      Connect (id1, id2) or Connect (id2, id1) =>
         Neighbour (id1, id2) = true;
      Neighbour (id1, id2) = false;

   (**************************************************************************)
   (*                         Instance parameters                            *)
   (**************************************************************************)

   ofsort Nat_8
      (* you can modify the following definition; make sure that Weight()
       * is defined for all objects (id1 in 0..5) 
       *)
      Weight (id1) = 1 of Nat_8; (* all objects have weight 1 *)

   ofsort Bool
      (* you can modify the following definition *)
      (id1 eq 0) and (id2 ge 1) and (id2 le 5) =>
         Connect (id1, id2) = true;
      (id1 gt 0) and (id1 le 5) and (id2 eq Succ (id1 mod 5)) =>
         Connect (id1, id2) = true;
      (* do not move, modify, or delete the following line *)
      Connect (id1, id2) = false;
endtype

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