(* Susanne Graf : cache_e1_I_fonc.lotos *)

(* Scenario for the verification of property S1 :
   two processes, one element e1
   PI is complete and writes e1
   PJ has no local variable and may not write e1   
*)

(* Composition expression of the global cache memory system
   using adt definitions of ELEM_E1_I.lib (one elem, 2 processes, PI writes)
   and process definitions MEMORY_FONC_T, PI_FONC_T_NDET, PJ_SSVAR_EPS
*)

specification cache [diag, w, r, mw, cu, mr, cl] : noexit

   library
      BOOLEAN, NATURAL, TYPES_COMMON, ELEM_E1_I
   endlib

behaviour

   hide sync in
      MEMORY [sync, mw, mr] (empt_m)
      |[sync, mw, mr]|
      (
         PI [diag, sync, w, r, mw, cu, mr, cl] (1 of index, empt_s, empt_m, empt_b, empt_b)
         |[sync, mw, w, r, cu, mr, cl]|
         PJ [sync, w, r, mw, cu, mr, cl] (2 of index)
      )
where
   library
      MEMORY_FONC_T, PI_FONC_T_NDET, PJ_SSVAR_EPS
   endlib
endspec