(* Susanne Graf: cache_e12_I_fonc.lotos *)

(* Scenario for the verification of property S3:
   - two processes, two elements e1, e2 
   - PI is complete and may write both elements (in any order)
   - PJ has no local variable and may not write e1, e2
*)
 
(* Functional non deterministic version
   process PJ complete 
   using adt definitions of ELEM_E12_I.lib
   and process definitions MEMORY_FONC_T, PI_FONC_T_NDET, and PJ_SSVAR_EPS
*)

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

   library
      BOOLEAN, NATURAL, TYPES_COMMON, ELEM_E12_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