(****************************************************************************** * Sequentially consistent, distributed cache memory *----------------------------------------------------------------------------- * INRIA - Unite de Recherche Rhone-Alpes * 655, avenue de l'Europe * 38330 Montbonnot Saint Martin * FRANCE *----------------------------------------------------------------------------- * Module : cache_e12_I_fonc.lnt * Authors : A. Kriouile and W. Serwe * Version : 1.1 * Date : 2016/01/08 11:30:15 *****************************************************************************) -- 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) 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