-- Scenario for the verification of property S3:
-- * two processes, two elements e1 and e2
-- * PI is complete and may write both elements (in any order)
-- * PJ has no local variable and may write neither e1 nor e2

-- functional non deterministic version
-- process PJ complete
-- using types and functions of ELEM_E12_I.lnt and
-- process definitions MEMORY_FONC_T, PI_FONC_T_NDET, and PJ_SSVAR_EPS

module cache_e12_I_fonc (MEMORY_FONC_T, PI_FONC_T_NDET, PJ_SSVAR_EPS, ELEM_E12_I) is

process MAIN [diag : BUF_NAT_CHANNEL,
              w, r, mw, cu, mr, cl : INDEX_ELEM_CHANNEL] is
   hide sync : NONE in
      par sync, mw, mr in
         MEMORY [sync, mw, mr] (empt_m)
       ||
         par sync, mw, w, r, cu, mr, cl in
            PI [diag, sync, w, r, mw, cu, mr, cl] (1 of INDEX)
          ||
            PJ [sync, w, r, mw, cu, mr, cl] (2 of INDEX)
         end par
      end par
   end hide
end process

end module