(******************************************************************************
 *             Sequentially consistent, distributed cache memory
 *-----------------------------------------------------------------------------
 *   INRIA - Unite de Recherche Rhone-Alpes
 *   655, avenue de l'Europe
 *   38330 Montbonnot Saint Martin
 *   FRANCE
 *-----------------------------------------------------------------------------
 *   Module       :       TYPES_COMMON.lnt
 *   Authors      :       A. Kriouile, W. Serwe, H. Garavel, and F. Lang
 *   Version      :       1.2
 *   Date         :       2023/10/08 15:03:54
 *****************************************************************************)
(**
 *  Part of the  abstract data type definitions used in the cache memory that 
 *  are common to all scenarii; concerns 
 *   - operations on sets of pairs (address,data)
 *   - operations on memories
 *   - operations on buffers of triples (address, data, boolean) where the
 *     boolean is not always meaningful
 *  
 *  For all relations such as append, update, etc. used in the program, we
 *  added (if necessary and possible) a function with the same effect; this is
 *  the point, which makes the execution impossible for a type ELEM containing
 *  two elements e1 and e2
 *
 *  The variable part of the data type definitions defining the number of 
 *  processes involved in the scenario (type INDEX) and the particular data
 *  abstraction of pairs (address, datum) (type ELEM) is in a separate file, 
 *  one for each scenario
 *)

module TYPES_COMMON (GENERIC_ELEMENT) is
-- the GENERIC_ELEMENT module will be instantiated in the "demo.svl" file

(*****************************************************************************)

-- type SET_OF_ELEM implementing sets of elements of type ELEM

type SET_OF_ELEM is 
   empt_s, Add (S : SET_OF_ELEM, e : ELEM)
   with ==
end type

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

function Insert (S : SET_OF_ELEM, x : ELEM) : SET_OF_ELEM is
   -- inserts x into the set S according to the order "<"
   var S1 : SET_OF_ELEM, y : ELEM in
      case x in
         eps -> return S
       | any -> case S in
                   empt_s      -> return Add (empt_s, x)
                 | Add (S1, y) -> if y == x  then return S
                                  elsif y < x then return Add (S, x)
                                  else return Add (Insert (S1, x), y)
                                  end if
                end case
      end case
   end var
end function

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

function IsIn (S : SET_OF_ELEM, x : ELEM) : Bool is
   -- returns "true" iff (x is an element of S) or (x is eps and S not empty)
   case S 
      var S1 : SET_OF_ELEM, y : ELEM
   in
      empt_s      -> return false
   |  Add (S1, y) -> if x == eps then return true
                     elsif x == y then return true
                     else return IsIn (S1, x)
                     end if
   end case
end function

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

function notIsIn (S : SET_OF_ELEM, x : ELEM) : Bool is
   -- returns "true" iff
   --    (x is not an element of S) or (x is eps and S not empty)
   -- note: in general, notIsIn(S,x) is not the negation of IsIn(S,x)
   case S in
      empt_s -> return true
    | any    -> case x in
                   eps -> return true
                 | any -> return not (IsIn (S, x))
                end case
   end case
end function 

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

function allowed (S : SET_OF_ELEM, x : ELEM, Sp : SET_OF_ELEM) : Bool is
   -- predicate used in PI : true if a given element is not yet in a given set
   -- and if its insertion into it yields the second given set
   return notIsIn (S, x) and (Sp == Insert (S, x))
end function            

(*****************************************************************************)

-- type MEMORY

type MEM_OF_ELEM is
   empt_m (* empty memory *),
   Add (M : MEM_OF_ELEM, x : ELEM)
   with ==
end type

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

function Insert (M : MEM_OF_ELEM, x : ELEM) : MEM_OF_ELEM is
   -- inserts x into M; uses the function first of ELEM in order to decide if x
   -- must be added or replaces one element already in M; uses the order less on
   -- ELEM in order to have a normal form
   var M1 : MEM_OF_ELEM, y : ELEM in
      case x in
         eps -> return M
       | any -> case M in
                   empt_m     -> return Add (empt_m, x)
                 | Add (M1,y) -> if first (x, y) then
                                    return Add (M1, x)
                                 elsif (not (first (x, y))) and (y < x) then
                                    return Add (M, x)
                                 else
                                    return Add (Insert (M1, x), y)
                                 end if
                end case
      end case
   end var
end function

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

function cl (M : MEM_OF_ELEM, x : ELEM) : MEM_OF_ELEM is
   -- eliminates a given (address, datum) pair from memory M
   case M
      var M1 : MEM_OF_ELEM, y : ELEM
   in
      empt_m      -> return empt_m
   |  Add (M1, y) -> if x == eps then return M
                     elsif first (y, x) then return M1
                     else return Add (cl (M1, x), y)
                     end if
   end case
end function

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

function ok (M : MEM_OF_ELEM, x : ELEM) : Bool is
   -- tests if a given pair (address, datum) is in memory M
   var M1 : MEM_OF_ELEM, y : ELEM in
      case x in
         eps -> return true
       | any -> case M in
                   empt_m      -> return false
                 | Add (M1, y) -> if y == x then return true
                                  elsif first (x, y) then return false
                                  else return ok (M1, x)
                                  end if
                end case
      end case
   end var
end function

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

function update (M : MEM_OF_ELEM, x : ELEM, Mp : MEM_OF_ELEM) : Bool is
   -- predicate representing function Insert
   return Mp == Insert (M, x)
end function

-------------------------------------------------------------------------------
 
function clear (M : MEM_OF_ELEM, x : ELEM, Mp : MEM_OF_ELEM) : Bool is
   -- predicate representing function cl
   require ok (M, x);
   return Mp == cl (M, x)
end function

(*****************************************************************************)

function max_Card : NAT is
   -- number of non-empty elements in ELEM; used to define type BUFFER
   return ord (last of ELEM)
end function

(*****************************************************************************)

-- type BUFFER implementing functions and predicates on buffers containing
-- triples ((address, datum), boolean), where the pair (address, elem) is
-- represented by an elemet of ELEM

type BUF_OF_ELEM is
   empt_b,
   overflow (* non expected buffer; too long *), 
   Add (B : BUF_OF_ELEM, x : ELEM, bit : Bool)
   with ==, <>
end type

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

function Enqueue (B : BUF_OF_ELEM, x : ELEM, bit : Bool) : BUF_OF_ELEM is
   -- particular function enqueue on buffers: eliminates consecutive elements 
   -- distinguished at most by the boolean (true wins over false)
   var B1 : BUF_OF_ELEM, y : ELEM, bit2 : Bool in 
      case x in
         eps -> return B
       | any -> case B in
                   empt_b            -> return Add (empt_b, x, bit)
                 | overflow          -> return overflow
                 | Add (B1, y, bit2) -> if y == x then
                                           if bit2 == bit then return B
                                           else return Add (B1, x, true)
                                           end if 
                                        elsif Card (B) < max_Card then
                                           return Add (B, x, bit)
                                        else
                                           return overflow
                                        end if
                end case
      end case      
   end var
end function

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

function Dequeue (B : BUF_OF_ELEM) : BUF_OF_ELEM is
   -- function dequeue on buffers; undefined for empt_b
   require B <> empt_b;
   var B1 : BUF_OF_ELEM, x : ELEM, bit : Bool in
      case B in
         empt_b                           -> raise UNEXPECTED 
       | overflow                         -> return overflow
       | Add (empt_b, any ELEM, any Bool) -> return empt_b
       | Add (B1, x, bit)                 -> return Add (Dequeue (B1), x, bit)
      end case
   end var
end function

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

function Card (B : BUF_OF_ELEM) : NAT is
   -- length of the buffer; the maximal allowed length depends on the cardinality
   -- of type ELEM and the scenario
   var B1 : BUF_OF_ELEM in
      case B in
         empt_b                       -> return 0
       | overflow                     -> return max_Card + 1
       | Add (B1, any ELEM, any Bool) -> return 1 + Card (B1)
      end case
   end var
end function

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

function empty (B : BUF_OF_ELEM) : Bool is
   -- emptiness test on buffers
   case B in
      empt_b -> return true
    | any    -> return false
   end case
end function

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

function empty_true (B : BUF_OF_ELEM) : Bool is
   -- returns "true" if buffer B contains no element with boolean = true
   var B1 : BUF_OF_ELEM in
      case B in
         empt_b                                -> return true
       | overflow                              -> return false (* or true *)
       | Add (any BUF_OF_ELEM, any ELEM, true) -> return false
       | Add (B1, any ELEM, false)             -> return empty_true (B1)
      end case
   end var
end function

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

function NotIn (B : BUF_OF_ELEM, x : ELEM) : Bool is
   -- returns "true" if there exists a triple in buffer B containing element x
   var B1 : BUF_OF_ELEM, y : ELEM in
      if x == eps then return true
      else
         case B in
            overflow              -> return false
          | empt_b                -> return true
          | Add (B1, y, any Bool) -> if y == x then return false
                                     else return NotIn (B1, x)
                                     end if
         end case
      end if
   end var
end function

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

function ff (B : BUF_OF_ELEM, x : ELEM) : Bool is
   -- predicate "is first element of" on buffers
   var B1 : BUF_OF_ELEM, y : ELEM in
      case B in
         empt_b                       -> return false
       | overflow                     -> return false
       | Add (empt_b, y, any Bool)    -> if y == x then return true
                                         else return false
                                         end if
       | Add (B1, any ELEM, any Bool) -> return ff (B1, x)
      end case
   end var
end function

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

function first (B : BUF_OF_ELEM, x : ELEM) : Bool is
   -- predicate "is first element of" on abstract buffers
   case x in
      eps -> return true
    | any -> case B in
                overflow -> return true
              | any      -> return ff (B, x)
             end case
   end case
end function  

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

function append (B : BUF_OF_ELEM, x : ELEM, bit: Bool, Bp : BUF_OF_ELEM) : Bool
is
   -- predicate defining function Enqueue
   return Bp == Enqueue (B, x, bit)
end function

-------------------------------------------------------------------------------
              
function tail(B : BUF_OF_ELEM, x : ELEM, Bp : BUF_OF_ELEM) : Bool is
   -- predicate defining the inverse function of Enqueue (that means the
   -- dequeued element may or may not be eliminated)
   if (x == eps) and (B == Bp) then
      return true
   elsif (B == overflow) and
         ((Bp == overflow) or (Card (Bp) == max_Card))
   then 
      return true
   elsif ff (B, x) then 
      return (B == Bp) or (Bp == Dequeue (B))
   else
      return false
   end if
end function

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

-- A problem: in the buffer Out Dequeue (Out, x, Out) is not allowed; this
-- leads to overflow of buffer Inn; moreover, as each element is written at
-- ost once, this looks reasonnable

-- The functional version of Append is simply Enqueue, and the functional
-- version of tail is to replace each actual transition by
--    1) one transition replacing Bp by B
--    2) one transition replacing B by dequeue (B) under the condition that
--       not (empty (B) or (B == overflow)) and ff (B, x)

-- This forbids the successors of overflow above max_Card, but it is not
-- a problem as the value overflow should occur

-- The solution of the above problem: 2 transitions for Inn and 1 transition
-- for Out

(*****************************************************************************)

channel INDEX_ELEM_CHANNEL is
   (IND : INDEX, E : ELEM)
end channel

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

channel BUF_NAT_CHANNEL is
   (BUF : BUF_OF_ELEM, N : NAT)
end channel

(*****************************************************************************)

end module