module TYPES is

type Nat_8 is
    range 0 .. 7 of Nat
end type

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

function + (n1: Nat_8, n2: Nat_8): Nat_8 is
     return Nat_8 ((Nat (n1) + Nat (n2)) mod 8)
end function

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

type Identity is
     n: Nat
     with ==, <, <=, >, >=
end type

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

function Succ (id: Identity) : Identity is
     return Identity (Nat (id) + 1)
end function

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

type Identity_List is
     sorted list of Identity with length, member
end type

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

function Number_Neighbours (id1: Identity): Nat is
     var id2: Identity, r: Nat in
          r := 0;
          for id2 := (0 of Identity) while id2 < (6 of Identity) by id2 := Succ (id2) loop
               if Neighbour (id1, id2) then
                    r := r + 1
               end if
          end loop;
          return r
     end var
end function

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

function Neighbour (id1: Identity, id2: Identity): Bool is
     if id1 == id2 then
          return false
     else
          return Connect (id1, id2) or else Connect (id2, id1)
     end if
end function

-----------------------------------------------------------------------------
-- Instance parameters
-----------------------------------------------------------------------------

function Weight (id: Identity): Nat_8 is
     use id;
     return 1 of Nat_8 -- all objects have weight 1
end function

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

function Connect (id1: Identity, id2: Identity): Bool is
     if (id1 == 0 of Identity) and (id2 >= 1 of Identity) and (id2 <= 5 of Identity) then
          return true
     elsif (id1 > 0 of Identity) and (id1 <= 5 of Identity) and (id2 == Identity ((Nat (id1) mod 5) + 1)) then
          return true
     else
          return false
     end if
end function

end module