1		package(load_event_b_project([event_b_model(none,'FENCEM7',[sees(none,['GC1','GC1a','GC2','GC3','FENCEC4','FENCEC5','FENCEC6','FENCEC7']),refines(none,'FENCEM6'),variables(none,[identifier(none,after),identifier(none,ahead),identifier(none,coverage),identifier(none,issued),identifier(none,issuedfence),identifier(none,lastobservedvalue),identifier(none,observed),identifier(none,observers),identifier(none,registerfile)]),invariant(none,[member(rodinpos('FENCEM7',inv1,'_gpfVsepmEeSvO6bvOrqan1'),identifier(none,coverage),relations(none,identifier(none,'REGCOVER'),identifier(none,'REGCOVER')))]),theorems(none,[]),events(none,[event(rodinpos('FENCEM7','INITIALISATION','_gpfVsepmEeSvO6bvOrqam~'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('FENCEM7',act1,'_VLR-g-TrEeSu4vk92SnwFw'),[identifier(none,issued)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('FENCEM7',act2,'_VLR-hOTrEeSu4vk92SnwFw'),[identifier(none,observed)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('FENCEM7',act3,'_VLSlkOTrEeSu4vk92SnwFw'),[identifier(none,lastobservedvalue)],[cartesian_product(none,identifier(none,'MASTER'),set_extension(none,[cartesian_product(none,identifier(none,'ADDR'),set_extension(none,[identifier(none,'V0')]))]))]),assign(rodinpos('FENCEM7',act4,'_VLSlkeTrEeSu4vk92SnwFw'),[identifier(none,observers)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'TRN'),pow_subset(none,identifier(none,'MASTER')))))]),assign(rodinpos('FENCEM7',act5,'\''),[identifier(none,issuedfence)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('FENCEM7',act6,'('),[identifier(none,ahead)],[cartesian_product(none,identifier(none,'FENCE'),set_extension(none,[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]))]),assign(rodinpos('FENCEM7',act7,')'),[identifier(none,after)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'TRN'),pow_subset(none,identifier(none,'TRN')))))]),assign(rodinpos('FENCEM7',act8,act1),[identifier(none,registerfile)],[cartesian_product(none,identifier(none,'MASTER'),set_extension(none,[cartesian_product(none,identifier(none,'REG'),set_extension(none,[identifier(none,'V0')]))]))]),assign(rodinpos('FENCEM7',act9,'\''),[identifier(none,coverage)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,pow_subset(none,cartesian_product(none,identifier(none,'REG'),identifier(none,'VALUE'))),pow_subset(none,cartesian_product(none,identifier(none,'REG'),identifier(none,'VALUE'))))))])],[]),event(rodinpos('FENCEM7','IssueLoad','_gpfVsepmEeSvO6bvOrqan\''),'IssueLoad',ordinary(none),['IssueLoad'],[identifier(rodinpos('FENCEM7',[],'_VLSlk-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM7',[],grd3),m),identifier(rodinpos('FENCEM7',[],')'),n),identifier(rodinpos('FENCEM7',[],'('),p)],[not_member(rodinpos('FENCEM7',grd1,'_VLSllOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM7',grd2,'_VLSlleTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),equal(rodinpos('FENCEM7',grd3,grd2),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),equal(rodinpos('FENCEM7',grd4,'*'),identifier(none,p),function(none,identifier(none,'PROGRAM'),[identifier(none,m)])),member(rodinpos('FENCEM7',grd5,'+'),identifier(none,n),domain(none,identifier(none,p))),equal(rodinpos('FENCEM7',grd6,','),function(none,identifier(none,p),[identifier(none,n)]),identifier(none,l)),forall(rodinpos('FENCEM7',grd7,grd1),[identifier(none,i)],implication(none,conjunct(none,member(none,identifier(none,i),integer_set(none)),conjunct(none,not_equal(none,identifier(none,i),identifier(none,n)),conjunct(none,member(none,identifier(none,i),domain(none,identifier(none,p))),not_member(none,function(none,identifier(none,p),[identifier(none,i)]),union(none,identifier(none,issued),identifier(none,issuedfence)))))),less(none,identifier(none,n),identifier(none,i))))],[],[assign(rodinpos('FENCEM7',act1,'_VLTMoOTrEeSu4vk92SnwFw'),[identifier(none,issued)],[union(none,identifier(none,issued),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM7',act2,'_VLTMoeTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),typeof(none,empty_set(none),pow_subset(none,identifier(none,'MASTER')))])]))])],[]),event(rodinpos('FENCEM7','IssueStore','_gpfVsepmEeSvO6bvOrqan('),'IssueStore',ordinary(none),['IssueStore'],[identifier(rodinpos('FENCEM7',[],'_VLTMo-TrEeSu4vk92SnwFw'),s),identifier(rodinpos('FENCEM7',[],grd5),m),identifier(rodinpos('FENCEM7',[],')'),n),identifier(rodinpos('FENCEM7',[],'('),p)],[not_member(rodinpos('FENCEM7',grd1,'_VLTMpOTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM7',grd2,'_VLTMpeTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM7',grd3,grd6),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,s)])),equal(rodinpos('FENCEM7',grd4,grd1),identifier(none,p),function(none,identifier(none,'PROGRAM'),[identifier(none,m)])),member(rodinpos('FENCEM7',grd5,grd2),identifier(none,n),domain(none,identifier(none,p))),equal(rodinpos('FENCEM7',grd6,grd3),function(none,identifier(none,p),[identifier(none,n)]),identifier(none,s)),forall(rodinpos('FENCEM7',grd7,grd4),[identifier(none,i)],implication(none,conjunct(none,member(none,identifier(none,i),integer_set(none)),conjunct(none,not_equal(none,identifier(none,i),identifier(none,n)),conjunct(none,member(none,identifier(none,i),domain(none,identifier(none,p))),not_member(none,function(none,identifier(none,p),[identifier(none,i)]),identifier(none,issued))))),less(none,identifier(none,n),identifier(none,i))))],[],[assign(rodinpos('FENCEM7',act1,'_VLTzsOTrEeSu4vk92SnwFw'),[identifier(none,issued)],[union(none,identifier(none,issued),set_extension(none,[identifier(none,s)]))]),assign(rodinpos('FENCEM7',act2,'_VLTzseTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,s),typeof(none,empty_set(none),pow_subset(none,identifier(none,'MASTER')))])]))]),assign(rodinpos('FENCEM7',act3,'_VLTzseTrEeSu4vk92SnwFx'),[identifier(none,after)],[overwrite(none,identifier(none,after),set_extension(none,[couple(none,[identifier(none,s),typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))])]))])],[]),event(rodinpos('FENCEM7','ObserveLoadAfterStore','_gpfVsepmEeSvO6bvOrqan)'),'ObserveLoadAfterStore',ordinary(none),['ObserveLoadAfterStore'],[identifier(rodinpos('FENCEM7',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM7',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM7',[],'_VLUawuTrEeSu4vk92SnwF{'),s)],[member(rodinpos('FENCEM7',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM7',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM7',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM7',grd4,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),forall(rodinpos('FENCEM7',grd5,'_VLUawuTrEeSu4vk92SnwFz'),[identifier(none,f)],implication(none,conjunct(none,member(none,identifier(none,f),identifier(none,'TRN')),member(none,identifier(none,f),identifier(none,issuedfence))),not_equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])))),member(rodinpos('FENCEM7',grd6,grd1),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM7',grd7,grd2),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM7',grd8,grd3),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),member(rodinpos('FENCEM7',grd9,grd4),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),member(rodinpos('FENCEM7',grd10,grd5),identifier(none,s),domain(none,identifier(none,after))),member(rodinpos('FENCEM7',grd11,act3),function(none,identifier(none,address),[identifier(none,l)]),domain(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)])))],[],[assign(rodinpos('FENCEM7',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM7',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))]),assign(rodinpos('FENCEM7',act3,act1),[identifier(none,after)],[overwrite(none,identifier(none,after),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,after),[identifier(none,s)]),set_extension(none,[identifier(none,l)]))])]))]),assign(rodinpos('FENCEM7',act4,act2),[identifier(none,registerfile)],[overwrite(none,identifier(none,registerfile),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,registerfile),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,register),[identifier(none,l)]),function(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),[function(none,identifier(none,address),[identifier(none,l)])])])]))])]))])],[]),event(rodinpos('FENCEM7','ObserveLoad','_gpfVsepmEeSvO6bvOrqan*'),'ObserveLoad',ordinary(none),['ObserveLoad'],[identifier(rodinpos('FENCEM7',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM7',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM7',[],'_VLUawuTrEeSu4vk92SnwF{'),s)],[member(rodinpos('FENCEM7',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM7',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM7',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM7',grd4,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),forall(rodinpos('FENCEM7',grd5,'_VLUawuTrEeSu4vk92SnwFz'),[identifier(none,f)],implication(none,conjunct(none,member(none,identifier(none,f),identifier(none,'TRN')),member(none,identifier(none,f),identifier(none,issuedfence))),not_equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])))),member(rodinpos('FENCEM7',grd6,grd1),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM7',grd7,grd2),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),implication(rodinpos('FENCEM7',grd8,grd3),member(none,identifier(none,s),identifier(none,observed)),not_member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)]))),member(rodinpos('FENCEM7',grd9,act3),function(none,identifier(none,address),[identifier(none,l)]),domain(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)])))],[],[assign(rodinpos('FENCEM7',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM7',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))]),assign(rodinpos('FENCEM7',act3,act2),[identifier(none,registerfile)],[overwrite(none,identifier(none,registerfile),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,registerfile),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,register),[identifier(none,l)]),function(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),[function(none,identifier(none,address),[identifier(none,l)])])])]))])]))])],[]),event(rodinpos('FENCEM7','ObserveLoadFenceAfterStore','_gpfVsepmEeSvO6bvOrqan+'),'ObserveLoadFenceAfterStore',ordinary(none),['ObserveLoadFenceAfterStore'],[identifier(rodinpos('FENCEM7',[],'_VLUawuTrEeSu4vk92SnwFx'),f),identifier(rodinpos('FENCEM7',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM7',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM7',[],'_VLUawuTrEeSu4vk92SnwF}'),s)],[member(rodinpos('FENCEM7',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM7',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM7',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM7',grd4,'_VLUawuTrEeSu4vk92SnwF{'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),member(rodinpos('FENCEM7',grd5,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,f),identifier(none,issuedfence)),equal(rodinpos('FENCEM7',grd6,'_VLUawuTrEeSu4vk92SnwF|'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),implication(rodinpos('FENCEM7',grd7,'_VLUawuTrEeSu4vk92SnwFz'),not_member(none,identifier(none,l),function(none,identifier(none,ahead),[identifier(none,f)])),forall(none,[identifier(none,a)],implication(none,conjunct(none,member(none,identifier(none,a),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,a),function(none,identifier(none,ahead),[identifier(none,f)])),member(none,identifier(none,a),domain(none,identifier(none,observers))))),member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,a)]))))),member(rodinpos('FENCEM7',grd8,'_VLUawuTrEeSu4vk92SnwF~'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM7',grd9,'_VLUawuTrEeSu4vk92SnwG\''),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM7',grd10,'_VLUawuTrEeSu4vk92SnwG('),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),member(rodinpos('FENCEM7',grd11,'_VLUawuTrEeSu4vk92SnwG)'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),member(rodinpos('FENCEM7',grd12,'_VLUawuTrEeSu4vk92SnwG*'),identifier(none,s),domain(none,identifier(none,after))),member(rodinpos('FENCEM7',grd13,grd1),function(none,identifier(none,address),[identifier(none,l)]),domain(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)])))],[],[assign(rodinpos('FENCEM7',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM7',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))]),assign(rodinpos('FENCEM7',act3,'_VLUawuTrEeSu4vk92SnwG+'),[identifier(none,after)],[overwrite(none,identifier(none,after),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,after),[identifier(none,s)]),set_extension(none,[identifier(none,l)]))])]))]),assign(rodinpos('FENCEM7',act4,act1),[identifier(none,registerfile)],[overwrite(none,identifier(none,registerfile),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,registerfile),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,register),[identifier(none,l)]),function(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),[function(none,identifier(none,address),[identifier(none,l)])])])]))])]))])],[]),event(rodinpos('FENCEM7','ObserveLoadFence','_gpfVsepmEeSvO6bvOrqan,'),'ObserveLoadFence',ordinary(none),['ObserveLoadFence'],[identifier(rodinpos('FENCEM7',[],'_VLUawuTrEeSu4vk92SnwFx'),f),identifier(rodinpos('FENCEM7',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM7',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM7',[],'_VLUawuTrEeSu4vk92SnwF}'),s)],[member(rodinpos('FENCEM7',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM7',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM7',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM7',grd4,'_VLUawuTrEeSu4vk92SnwF{'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),member(rodinpos('FENCEM7',grd5,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,f),identifier(none,issuedfence)),equal(rodinpos('FENCEM7',grd6,'_VLUawuTrEeSu4vk92SnwF|'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),implication(rodinpos('FENCEM7',grd7,'_VLUawuTrEeSu4vk92SnwFz'),not_member(none,identifier(none,l),function(none,identifier(none,ahead),[identifier(none,f)])),forall(none,[identifier(none,a)],implication(none,conjunct(none,member(none,identifier(none,a),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,a),function(none,identifier(none,ahead),[identifier(none,f)])),member(none,identifier(none,a),domain(none,identifier(none,observers))))),member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,a)]))))),member(rodinpos('FENCEM7',grd8,'_VLUawuTrEeSu4vk92SnwF~'),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM7',grd9,'_VLUawuTrEeSu4vk92SnwG\''),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),implication(rodinpos('FENCEM7',grd10,'_VLUawuTrEeSu4vk92SnwG('),member(none,identifier(none,s),identifier(none,observed)),conjunct(none,not_member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),equal(none,function(none,identifier(none,after),[identifier(none,s)]),typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))))),member(rodinpos('FENCEM7',grd11,grd1),function(none,identifier(none,address),[identifier(none,l)]),domain(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)])))],[],[assign(rodinpos('FENCEM7',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM7',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))]),assign(rodinpos('FENCEM7',act3,act1),[identifier(none,registerfile)],[overwrite(none,identifier(none,registerfile),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,registerfile),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,register),[identifier(none,l)]),function(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),[function(none,identifier(none,address),[identifier(none,l)])])])]))])]))])],[]),event(rodinpos('FENCEM7','ObserveStore','_gpfVsepmEeSvO6bvOrqan-'),'ObserveStore',ordinary(none),['ObserveStore'],[identifier(rodinpos('FENCEM7',[],'_VLVB0OTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM7',[],'_VLUaxeTrEeSu4vk92SnwFw'),s)],[member(rodinpos('FENCEM7',grd1,'_VLVB0eTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM7',grd2,'_VLVB0uTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE')),not_member(rodinpos('FENCEM7',grd3,'_VLVB0-TrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),forall(rodinpos('FENCEM7',grd4,grd1),[identifier(none,f)],implication(none,conjunct(none,member(none,identifier(none,f),identifier(none,'TRN')),member(none,identifier(none,f),identifier(none,issuedfence))),not_equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)]))))],[],[assign(rodinpos('FENCEM7',act1,'_VLVB1OTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,s)]))]),assign(rodinpos('FENCEM7',act2,'_VLVB1eTrEeSu4vk92SnwFw'),[identifier(none,lastobservedvalue)],[overwrite(none,identifier(none,lastobservedvalue),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,value),[identifier(none,s)])])]))])]))]),assign(rodinpos('FENCEM7',act3,'_VLVo4OTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,observers),[identifier(none,s)]),set_extension(none,[identifier(none,m)]))])]))])],[]),event(rodinpos('FENCEM7','ObserveStoreFence','_gpfVsepmEeSvO6bvOrqan.'),'ObserveStoreFence',ordinary(none),['ObserveStoreFence'],[identifier(rodinpos('FENCEM7',[],'_VLVo4OTrEeSu4vk92SnwFx'),f),identifier(rodinpos('FENCEM7',[],'_VLVB0OTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM7',[],'_VLUaxeTrEeSu4vk92SnwFw'),s)],[member(rodinpos('FENCEM7',grd1,'_VLVB0eTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM7',grd2,'_VLVB0uTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE')),not_member(rodinpos('FENCEM7',grd3,'_VLVB0-TrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),member(rodinpos('FENCEM7',grd4,grd1),identifier(none,f),identifier(none,issuedfence)),equal(rodinpos('FENCEM7',grd5,grd2),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),implication(rodinpos('FENCEM7',grd6,grd3),not_member(none,identifier(none,s),function(none,identifier(none,ahead),[identifier(none,f)])),forall(none,[identifier(none,a)],implication(none,conjunct(none,member(none,identifier(none,a),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,a),function(none,identifier(none,ahead),[identifier(none,f)])),member(none,identifier(none,a),domain(none,identifier(none,observers))))),member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,a)])))))],[],[assign(rodinpos('FENCEM7',act1,'_VLVB1OTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,s)]))]),assign(rodinpos('FENCEM7',act2,'_VLVB1eTrEeSu4vk92SnwFw'),[identifier(none,lastobservedvalue)],[overwrite(none,identifier(none,lastobservedvalue),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,value),[identifier(none,s)])])]))])]))]),assign(rodinpos('FENCEM7',act3,'_VLVo4OTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,observers),[identifier(none,s)]),set_extension(none,[identifier(none,m)]))])]))])],[]),event(rodinpos('FENCEM7','IssueFence','_gpfVsepmEeSvO6bvOrqan/'),'IssueFence',ordinary(none),['IssueFence'],[identifier(rodinpos('FENCEM7',[],'\''),f),identifier(rodinpos('FENCEM7',[],'*'),m),identifier(rodinpos('FENCEM7',[],grd6),n),identifier(rodinpos('FENCEM7',[],grd5),p)],[member(rodinpos('FENCEM7',grd1,'('),identifier(none,f),identifier(none,'FENCE')),member(rodinpos('FENCEM7',grd2,'+'),identifier(none,m),identifier(none,'MASTER')),equal(rodinpos('FENCEM7',grd3,','),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),not_member(rodinpos('FENCEM7',grd4,'-'),identifier(none,f),identifier(none,issuedfence)),equal(rodinpos('FENCEM7',grd5,grd1),identifier(none,p),function(none,identifier(none,'PROGRAM'),[identifier(none,m)])),member(rodinpos('FENCEM7',grd6,grd2),identifier(none,n),domain(none,identifier(none,p))),equal(rodinpos('FENCEM7',grd7,grd3),function(none,identifier(none,p),[identifier(none,n)]),identifier(none,f)),forall(rodinpos('FENCEM7',grd8,grd4),[identifier(none,i)],implication(none,conjunct(none,member(none,identifier(none,i),integer_set(none)),conjunct(none,not_equal(none,identifier(none,i),identifier(none,n)),conjunct(none,member(none,identifier(none,i),domain(none,identifier(none,p))),not_member(none,function(none,identifier(none,p),[identifier(none,i)]),identifier(none,issued))))),less(none,identifier(none,n),identifier(none,i))))],[],[assign(rodinpos('FENCEM7',act1,')'),[identifier(none,issuedfence)],[union(none,identifier(none,issuedfence),set_extension(none,[identifier(none,f)]))]),assign(rodinpos('FENCEM7',act2,'.'),[identifier(none,ahead)],[overwrite(none,identifier(none,ahead),set_extension(none,[couple(none,[identifier(none,f),event_b_comprehension_set(none,[identifier(none,t)],identifier(none,t),conjunct(none,member(none,identifier(none,t),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,t),identifier(none,issued)),equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,t)])))))])]))])],[]),event(rodinpos('FENCEM7','CoverRegisterValues','_gpfVsepmEeSvO6bvOrqan2'),'CoverRegisterValues',ordinary(none),[],[identifier(rodinpos('FENCEM7',[],'\''),rm3),identifier(rodinpos('FENCEM7',[],'('),rm4)],[member(rodinpos('FENCEM7',grd1,')'),identifier(none,rm3),identifier(none,'REGCOVER')),member(rodinpos('FENCEM7',grd2,'+'),identifier(none,rm4),identifier(none,'REGCOVER')),equal(rodinpos('FENCEM7',grd3,','),function(none,identifier(none,registerfile),[identifier(none,'M3')]),identifier(none,rm3)),equal(rodinpos('FENCEM7',grd4,'-'),function(none,identifier(none,registerfile),[identifier(none,'M4')]),identifier(none,rm4)),not_member(rodinpos('FENCEM7',grd5,'.'),couple(none,[identifier(none,rm3),identifier(none,rm4)]),identifier(none,coverage)),subset(rodinpos('FENCEM7',grd6,'/'),set_extension(none,[identifier(none,'I31'),identifier(none,'I33'),identifier(none,'I41'),identifier(none,'I43')]),identifier(none,observed))],[],[assign(rodinpos('FENCEM7',act1,'*'),[identifier(none,coverage)],[union(none,identifier(none,coverage),set_extension(none,[couple(none,[identifier(none,rm3),identifier(none,rm4)])]))])],[])])]),event_b_model(none,'FENCEM6',[sees(none,['GC1','GC1a','GC2','GC3','FENCEC4','FENCEC5','FENCEC6']),refines(none,'FENCEM5'),variables(none,[identifier(none,after),identifier(none,ahead),identifier(none,issued),identifier(none,issuedfence),identifier(none,lastobservedvalue),identifier(none,observed),identifier(none,observers),identifier(none,registerfile)]),invariant(none,[implication(rodinpos('FENCEM6',inv1,'_gpfVsepmEeSvO6bvOrqan/'),subset(none,set_extension(none,[identifier(none,'I31'),identifier(none,'I33'),identifier(none,'I41'),identifier(none,'I43')]),identifier(none,observed)),negation(none,conjunct(none,equal(none,function(none,function(none,identifier(none,registerfile),[identifier(none,'M3')]),[identifier(none,'R1')]),identifier(none,'V1')),conjunct(none,equal(none,function(none,function(none,identifier(none,registerfile),[identifier(none,'M3')]),[identifier(none,'R2')]),identifier(none,'V0')),conjunct(none,equal(none,function(none,function(none,identifier(none,registerfile),[identifier(none,'M4')]),[identifier(none,'R1')]),identifier(none,'V1')),equal(none,function(none,function(none,identifier(none,registerfile),[identifier(none,'M4')]),[identifier(none,'R2')]),identifier(none,'V0')))))))]),theorems(none,[]),events(none,[event(rodinpos('FENCEM6','INITIALISATION','_gpfVsepmEeSvO6bvOrqam~'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('FENCEM6',act1,'_VLR-g-TrEeSu4vk92SnwFw'),[identifier(none,issued)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('FENCEM6',act2,'_VLR-hOTrEeSu4vk92SnwFw'),[identifier(none,observed)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('FENCEM6',act3,'_VLSlkOTrEeSu4vk92SnwFw'),[identifier(none,lastobservedvalue)],[cartesian_product(none,identifier(none,'MASTER'),set_extension(none,[cartesian_product(none,identifier(none,'ADDR'),set_extension(none,[identifier(none,'V0')]))]))]),assign(rodinpos('FENCEM6',act4,'_VLSlkeTrEeSu4vk92SnwFw'),[identifier(none,observers)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'TRN'),pow_subset(none,identifier(none,'MASTER')))))]),assign(rodinpos('FENCEM6',act5,'\''),[identifier(none,issuedfence)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('FENCEM6',act6,'('),[identifier(none,ahead)],[cartesian_product(none,identifier(none,'FENCE'),set_extension(none,[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]))]),assign(rodinpos('FENCEM6',act7,')'),[identifier(none,after)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'TRN'),pow_subset(none,identifier(none,'TRN')))))]),assign(rodinpos('FENCEM6',act8,act1),[identifier(none,registerfile)],[cartesian_product(none,identifier(none,'MASTER'),set_extension(none,[cartesian_product(none,identifier(none,'REG'),set_extension(none,[identifier(none,'V0')]))]))])],[]),event(rodinpos('FENCEM6','IssueLoad','_gpfVsepmEeSvO6bvOrqan\''),'IssueLoad',ordinary(none),['IssueLoad'],[identifier(rodinpos('FENCEM6',[],'_VLSlk-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM6',[],grd3),m),identifier(rodinpos('FENCEM6',[],')'),n),identifier(rodinpos('FENCEM6',[],'('),p)],[not_member(rodinpos('FENCEM6',grd1,'_VLSllOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM6',grd2,'_VLSlleTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),equal(rodinpos('FENCEM6',grd3,grd2),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),equal(rodinpos('FENCEM6',grd4,'*'),identifier(none,p),function(none,identifier(none,'PROGRAM'),[identifier(none,m)])),member(rodinpos('FENCEM6',grd5,'+'),identifier(none,n),domain(none,identifier(none,p))),equal(rodinpos('FENCEM6',grd6,','),function(none,identifier(none,p),[identifier(none,n)]),identifier(none,l)),forall(rodinpos('FENCEM6',grd7,grd1),[identifier(none,i)],implication(none,conjunct(none,member(none,identifier(none,i),integer_set(none)),conjunct(none,not_equal(none,identifier(none,i),identifier(none,n)),conjunct(none,member(none,identifier(none,i),domain(none,identifier(none,p))),not_member(none,function(none,identifier(none,p),[identifier(none,i)]),union(none,identifier(none,issued),identifier(none,issuedfence)))))),less(none,identifier(none,n),identifier(none,i))))],[],[assign(rodinpos('FENCEM6',act1,'_VLTMoOTrEeSu4vk92SnwFw'),[identifier(none,issued)],[union(none,identifier(none,issued),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM6',act2,'_VLTMoeTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),typeof(none,empty_set(none),pow_subset(none,identifier(none,'MASTER')))])]))])],[]),event(rodinpos('FENCEM6','IssueStore','_gpfVsepmEeSvO6bvOrqan('),'IssueStore',ordinary(none),['IssueStore'],[identifier(rodinpos('FENCEM6',[],'_VLTMo-TrEeSu4vk92SnwFw'),s),identifier(rodinpos('FENCEM6',[],grd5),m),identifier(rodinpos('FENCEM6',[],')'),n),identifier(rodinpos('FENCEM6',[],'('),p)],[not_member(rodinpos('FENCEM6',grd1,'_VLTMpOTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM6',grd2,'_VLTMpeTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM6',grd3,grd6),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,s)])),equal(rodinpos('FENCEM6',grd4,grd1),identifier(none,p),function(none,identifier(none,'PROGRAM'),[identifier(none,m)])),member(rodinpos('FENCEM6',grd5,grd2),identifier(none,n),domain(none,identifier(none,p))),equal(rodinpos('FENCEM6',grd6,grd3),function(none,identifier(none,p),[identifier(none,n)]),identifier(none,s)),forall(rodinpos('FENCEM6',grd7,grd4),[identifier(none,i)],implication(none,conjunct(none,member(none,identifier(none,i),integer_set(none)),conjunct(none,not_equal(none,identifier(none,i),identifier(none,n)),conjunct(none,member(none,identifier(none,i),domain(none,identifier(none,p))),not_member(none,function(none,identifier(none,p),[identifier(none,i)]),identifier(none,issued))))),less(none,identifier(none,n),identifier(none,i))))],[],[assign(rodinpos('FENCEM6',act1,'_VLTzsOTrEeSu4vk92SnwFw'),[identifier(none,issued)],[union(none,identifier(none,issued),set_extension(none,[identifier(none,s)]))]),assign(rodinpos('FENCEM6',act2,'_VLTzseTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,s),typeof(none,empty_set(none),pow_subset(none,identifier(none,'MASTER')))])]))]),assign(rodinpos('FENCEM6',act3,'_VLTzseTrEeSu4vk92SnwFx'),[identifier(none,after)],[overwrite(none,identifier(none,after),set_extension(none,[couple(none,[identifier(none,s),typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))])]))])],[]),event(rodinpos('FENCEM6','ObserveLoadAfterStore','_gpfVsepmEeSvO6bvOrqan)'),'ObserveLoadAfterStore',ordinary(none),['ObserveLoadAfterStore'],[identifier(rodinpos('FENCEM6',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM6',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM6',[],'_VLUawuTrEeSu4vk92SnwF{'),s)],[member(rodinpos('FENCEM6',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM6',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM6',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM6',grd4,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),forall(rodinpos('FENCEM6',grd5,'_VLUawuTrEeSu4vk92SnwFz'),[identifier(none,f)],implication(none,conjunct(none,member(none,identifier(none,f),identifier(none,'TRN')),member(none,identifier(none,f),identifier(none,issuedfence))),not_equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])))),member(rodinpos('FENCEM6',grd6,grd1),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM6',grd7,grd2),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM6',grd8,grd3),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),member(rodinpos('FENCEM6',grd9,grd4),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),member(rodinpos('FENCEM6',grd10,grd5),identifier(none,s),domain(none,identifier(none,after))),member(rodinpos('FENCEM6',grd11,act3),function(none,identifier(none,address),[identifier(none,l)]),domain(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)])))],[],[assign(rodinpos('FENCEM6',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM6',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))]),assign(rodinpos('FENCEM6',act3,act1),[identifier(none,after)],[overwrite(none,identifier(none,after),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,after),[identifier(none,s)]),set_extension(none,[identifier(none,l)]))])]))]),assign(rodinpos('FENCEM6',act4,act2),[identifier(none,registerfile)],[overwrite(none,identifier(none,registerfile),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,registerfile),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,register),[identifier(none,l)]),function(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),[function(none,identifier(none,address),[identifier(none,l)])])])]))])]))])],[]),event(rodinpos('FENCEM6','ObserveLoad',evt1),'ObserveLoad',ordinary(none),['ObserveLoad'],[identifier(rodinpos('FENCEM6',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM6',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM6',[],'_VLUawuTrEeSu4vk92SnwF{'),s)],[member(rodinpos('FENCEM6',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM6',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM6',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM6',grd4,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),forall(rodinpos('FENCEM6',grd5,'_VLUawuTrEeSu4vk92SnwFz'),[identifier(none,f)],implication(none,conjunct(none,member(none,identifier(none,f),identifier(none,'TRN')),member(none,identifier(none,f),identifier(none,issuedfence))),not_equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])))),member(rodinpos('FENCEM6',grd6,grd1),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM6',grd7,grd2),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),implication(rodinpos('FENCEM6',grd8,grd3),member(none,identifier(none,s),identifier(none,observed)),not_member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)]))),member(rodinpos('FENCEM6',grd9,act3),function(none,identifier(none,address),[identifier(none,l)]),domain(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)])))],[],[assign(rodinpos('FENCEM6',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM6',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))]),assign(rodinpos('FENCEM6',act3,act2),[identifier(none,registerfile)],[overwrite(none,identifier(none,registerfile),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,registerfile),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,register),[identifier(none,l)]),function(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),[function(none,identifier(none,address),[identifier(none,l)])])])]))])]))])],[]),event(rodinpos('FENCEM6','ObserveLoadFenceAfterStore','_gpfVsepmEeSvO6bvOrqan*'),'ObserveLoadFenceAfterStore',ordinary(none),['ObserveLoadFenceAfterStore'],[identifier(rodinpos('FENCEM6',[],'_VLUawuTrEeSu4vk92SnwFx'),f),identifier(rodinpos('FENCEM6',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM6',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM6',[],'_VLUawuTrEeSu4vk92SnwF}'),s)],[member(rodinpos('FENCEM6',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM6',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM6',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM6',grd4,'_VLUawuTrEeSu4vk92SnwF{'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),member(rodinpos('FENCEM6',grd5,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,f),identifier(none,issuedfence)),equal(rodinpos('FENCEM6',grd6,'_VLUawuTrEeSu4vk92SnwF|'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),implication(rodinpos('FENCEM6',grd7,'_VLUawuTrEeSu4vk92SnwFz'),not_member(none,identifier(none,l),function(none,identifier(none,ahead),[identifier(none,f)])),forall(none,[identifier(none,a)],implication(none,conjunct(none,member(none,identifier(none,a),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,a),function(none,identifier(none,ahead),[identifier(none,f)])),member(none,identifier(none,a),domain(none,identifier(none,observers))))),member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,a)]))))),member(rodinpos('FENCEM6',grd8,'_VLUawuTrEeSu4vk92SnwF~'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM6',grd9,'_VLUawuTrEeSu4vk92SnwG\''),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM6',grd10,'_VLUawuTrEeSu4vk92SnwG('),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),member(rodinpos('FENCEM6',grd11,'_VLUawuTrEeSu4vk92SnwG)'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),member(rodinpos('FENCEM6',grd12,'_VLUawuTrEeSu4vk92SnwG*'),identifier(none,s),domain(none,identifier(none,after))),member(rodinpos('FENCEM6',grd13,grd1),function(none,identifier(none,address),[identifier(none,l)]),domain(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)])))],[],[assign(rodinpos('FENCEM6',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM6',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))]),assign(rodinpos('FENCEM6',act3,'_VLUawuTrEeSu4vk92SnwG+'),[identifier(none,after)],[overwrite(none,identifier(none,after),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,after),[identifier(none,s)]),set_extension(none,[identifier(none,l)]))])]))]),assign(rodinpos('FENCEM6',act4,act1),[identifier(none,registerfile)],[overwrite(none,identifier(none,registerfile),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,registerfile),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,register),[identifier(none,l)]),function(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),[function(none,identifier(none,address),[identifier(none,l)])])])]))])]))])],[]),event(rodinpos('FENCEM6','ObserveLoadFence','_gpfVsepmEeSvO6bvOrqan+'),'ObserveLoadFence',ordinary(none),['ObserveLoadFence'],[identifier(rodinpos('FENCEM6',[],'_VLUawuTrEeSu4vk92SnwFx'),f),identifier(rodinpos('FENCEM6',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM6',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM6',[],'_VLUawuTrEeSu4vk92SnwF}'),s)],[member(rodinpos('FENCEM6',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM6',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM6',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM6',grd4,'_VLUawuTrEeSu4vk92SnwF{'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),member(rodinpos('FENCEM6',grd5,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,f),identifier(none,issuedfence)),equal(rodinpos('FENCEM6',grd6,'_VLUawuTrEeSu4vk92SnwF|'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),implication(rodinpos('FENCEM6',grd7,'_VLUawuTrEeSu4vk92SnwFz'),not_member(none,identifier(none,l),function(none,identifier(none,ahead),[identifier(none,f)])),forall(none,[identifier(none,a)],implication(none,conjunct(none,member(none,identifier(none,a),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,a),function(none,identifier(none,ahead),[identifier(none,f)])),member(none,identifier(none,a),domain(none,identifier(none,observers))))),member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,a)]))))),member(rodinpos('FENCEM6',grd8,'_VLUawuTrEeSu4vk92SnwF~'),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM6',grd9,'_VLUawuTrEeSu4vk92SnwG\''),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),implication(rodinpos('FENCEM6',grd10,'_VLUawuTrEeSu4vk92SnwG('),member(none,identifier(none,s),identifier(none,observed)),conjunct(none,not_member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),equal(none,function(none,identifier(none,after),[identifier(none,s)]),typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))))),member(rodinpos('FENCEM6',grd11,grd1),function(none,identifier(none,address),[identifier(none,l)]),domain(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)])))],[],[assign(rodinpos('FENCEM6',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM6',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))]),assign(rodinpos('FENCEM6',act3,act1),[identifier(none,registerfile)],[overwrite(none,identifier(none,registerfile),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,registerfile),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,register),[identifier(none,l)]),function(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),[function(none,identifier(none,address),[identifier(none,l)])])])]))])]))])],[]),event(rodinpos('FENCEM6','ObserveStore','_gpfVsepmEeSvO6bvOrqan,'),'ObserveStore',ordinary(none),['ObserveStore'],[identifier(rodinpos('FENCEM6',[],'_VLVB0OTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM6',[],'_VLUaxeTrEeSu4vk92SnwFw'),s)],[member(rodinpos('FENCEM6',grd1,'_VLVB0eTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM6',grd2,'_VLVB0uTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE')),not_member(rodinpos('FENCEM6',grd3,'_VLVB0-TrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),forall(rodinpos('FENCEM6',grd4,grd1),[identifier(none,f)],implication(none,conjunct(none,member(none,identifier(none,f),identifier(none,'TRN')),member(none,identifier(none,f),identifier(none,issuedfence))),not_equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)]))))],[],[assign(rodinpos('FENCEM6',act1,'_VLVB1OTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,s)]))]),assign(rodinpos('FENCEM6',act2,'_VLVB1eTrEeSu4vk92SnwFw'),[identifier(none,lastobservedvalue)],[overwrite(none,identifier(none,lastobservedvalue),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,value),[identifier(none,s)])])]))])]))]),assign(rodinpos('FENCEM6',act3,'_VLVo4OTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,observers),[identifier(none,s)]),set_extension(none,[identifier(none,m)]))])]))])],[]),event(rodinpos('FENCEM6','ObserveStoreFence','_gpfVsepmEeSvO6bvOrqan-'),'ObserveStoreFence',ordinary(none),['ObserveStoreFence'],[identifier(rodinpos('FENCEM6',[],'_VLVo4OTrEeSu4vk92SnwFx'),f),identifier(rodinpos('FENCEM6',[],'_VLVB0OTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM6',[],'_VLUaxeTrEeSu4vk92SnwFw'),s)],[member(rodinpos('FENCEM6',grd1,'_VLVB0eTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM6',grd2,'_VLVB0uTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE')),not_member(rodinpos('FENCEM6',grd3,'_VLVB0-TrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),member(rodinpos('FENCEM6',grd4,grd1),identifier(none,f),identifier(none,issuedfence)),equal(rodinpos('FENCEM6',grd5,grd2),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),implication(rodinpos('FENCEM6',grd6,grd3),not_member(none,identifier(none,s),function(none,identifier(none,ahead),[identifier(none,f)])),forall(none,[identifier(none,a)],implication(none,conjunct(none,member(none,identifier(none,a),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,a),function(none,identifier(none,ahead),[identifier(none,f)])),member(none,identifier(none,a),domain(none,identifier(none,observers))))),member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,a)])))))],[],[assign(rodinpos('FENCEM6',act1,'_VLVB1OTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,s)]))]),assign(rodinpos('FENCEM6',act2,'_VLVB1eTrEeSu4vk92SnwFw'),[identifier(none,lastobservedvalue)],[overwrite(none,identifier(none,lastobservedvalue),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,value),[identifier(none,s)])])]))])]))]),assign(rodinpos('FENCEM6',act3,'_VLVo4OTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,observers),[identifier(none,s)]),set_extension(none,[identifier(none,m)]))])]))])],[]),event(rodinpos('FENCEM6','IssueFence','_gpfVsepmEeSvO6bvOrqan.'),'IssueFence',ordinary(none),['IssueFence'],[identifier(rodinpos('FENCEM6',[],'\''),f),identifier(rodinpos('FENCEM6',[],'*'),m),identifier(rodinpos('FENCEM6',[],grd6),n),identifier(rodinpos('FENCEM6',[],grd5),p)],[member(rodinpos('FENCEM6',grd1,'('),identifier(none,f),identifier(none,'FENCE')),member(rodinpos('FENCEM6',grd2,'+'),identifier(none,m),identifier(none,'MASTER')),equal(rodinpos('FENCEM6',grd3,','),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),not_member(rodinpos('FENCEM6',grd4,'-'),identifier(none,f),identifier(none,issuedfence)),equal(rodinpos('FENCEM6',grd5,grd1),identifier(none,p),function(none,identifier(none,'PROGRAM'),[identifier(none,m)])),member(rodinpos('FENCEM6',grd6,grd2),identifier(none,n),domain(none,identifier(none,p))),equal(rodinpos('FENCEM6',grd7,grd3),function(none,identifier(none,p),[identifier(none,n)]),identifier(none,f)),forall(rodinpos('FENCEM6',grd8,grd4),[identifier(none,i)],implication(none,conjunct(none,member(none,identifier(none,i),integer_set(none)),conjunct(none,not_equal(none,identifier(none,i),identifier(none,n)),conjunct(none,member(none,identifier(none,i),domain(none,identifier(none,p))),not_member(none,function(none,identifier(none,p),[identifier(none,i)]),identifier(none,issued))))),less(none,identifier(none,n),identifier(none,i))))],[],[assign(rodinpos('FENCEM6',act1,')'),[identifier(none,issuedfence)],[union(none,identifier(none,issuedfence),set_extension(none,[identifier(none,f)]))]),assign(rodinpos('FENCEM6',act2,'.'),[identifier(none,ahead)],[overwrite(none,identifier(none,ahead),set_extension(none,[couple(none,[identifier(none,f),event_b_comprehension_set(none,[identifier(none,t)],identifier(none,t),conjunct(none,member(none,identifier(none,t),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,t),identifier(none,issued)),equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,t)])))))])]))])],[])])]),event_b_model(none,'FENCEM5',[sees(none,['GC1','GC1a','GC2','GC3','FENCEC4','FENCEC5']),refines(none,'FENCEM4'),variables(none,[identifier(none,after),identifier(none,ahead),identifier(none,issued),identifier(none,issuedfence),identifier(none,lastobservedvalue),identifier(none,observed),identifier(none,observers),identifier(none,registerfile)]),invariant(none,[member(rodinpos('FENCEM5',inv1,'_gpfVsepmEeSvO6bvOrqam~'),identifier(none,registerfile),partial_function(none,identifier(none,'MASTER'),total_function(none,identifier(none,'REG'),identifier(none,'VALUE')))),forall(rodinpos('FENCEM5',inv2,'_gpfVsepmEeSvO6bvOrqan\''),[identifier(none,m)],implication(none,conjunct(none,member(none,identifier(none,m),identifier(none,'MASTER')),member(none,identifier(none,m),identifier(none,'MASTER'))),member(none,identifier(none,m),domain(none,identifier(none,registerfile)))))]),theorems(none,[]),events(none,[event(rodinpos('FENCEM5','INITIALISATION','_gpfVsepmEeSvO6bvOrqamt'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('FENCEM5',act1,'_VLR-g-TrEeSu4vk92SnwFw'),[identifier(none,issued)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('FENCEM5',act2,'_VLR-hOTrEeSu4vk92SnwFw'),[identifier(none,observed)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('FENCEM5',act3,'_VLSlkOTrEeSu4vk92SnwFw'),[identifier(none,lastobservedvalue)],[cartesian_product(none,identifier(none,'MASTER'),set_extension(none,[cartesian_product(none,identifier(none,'ADDR'),set_extension(none,[identifier(none,'V0')]))]))]),assign(rodinpos('FENCEM5',act4,'_VLSlkeTrEeSu4vk92SnwFw'),[identifier(none,observers)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'TRN'),pow_subset(none,identifier(none,'MASTER')))))]),assign(rodinpos('FENCEM5',act5,'\''),[identifier(none,issuedfence)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('FENCEM5',act6,'('),[identifier(none,ahead)],[cartesian_product(none,identifier(none,'FENCE'),set_extension(none,[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]))]),assign(rodinpos('FENCEM5',act7,')'),[identifier(none,after)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'TRN'),pow_subset(none,identifier(none,'TRN')))))]),assign(rodinpos('FENCEM5',act8,act1),[identifier(none,registerfile)],[cartesian_product(none,identifier(none,'MASTER'),set_extension(none,[cartesian_product(none,identifier(none,'REG'),set_extension(none,[identifier(none,'V0')]))]))])],[]),event(rodinpos('FENCEM5','IssueLoad','_gpfVsepmEeSvO6bvOrqamu'),'IssueLoad',ordinary(none),['IssueLoad'],[identifier(rodinpos('FENCEM5',[],'_VLSlk-TrEeSu4vk92SnwFw'),l)],[not_member(rodinpos('FENCEM5',grd1,'_VLSllOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM5',grd2,'_VLSlleTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD'))],[],[assign(rodinpos('FENCEM5',act1,'_VLTMoOTrEeSu4vk92SnwFw'),[identifier(none,issued)],[union(none,identifier(none,issued),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM5',act2,'_VLTMoeTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),typeof(none,empty_set(none),pow_subset(none,identifier(none,'MASTER')))])]))])],[]),event(rodinpos('FENCEM5','IssueStore','_gpfVsepmEeSvO6bvOrqamv'),'IssueStore',ordinary(none),['IssueStore'],[identifier(rodinpos('FENCEM5',[],'_VLTMo-TrEeSu4vk92SnwFw'),s)],[not_member(rodinpos('FENCEM5',grd1,'_VLTMpOTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM5',grd2,'_VLTMpeTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE'))],[],[assign(rodinpos('FENCEM5',act1,'_VLTzsOTrEeSu4vk92SnwFw'),[identifier(none,issued)],[union(none,identifier(none,issued),set_extension(none,[identifier(none,s)]))]),assign(rodinpos('FENCEM5',act2,'_VLTzseTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,s),typeof(none,empty_set(none),pow_subset(none,identifier(none,'MASTER')))])]))]),assign(rodinpos('FENCEM5',act3,'_VLTzseTrEeSu4vk92SnwFx'),[identifier(none,after)],[overwrite(none,identifier(none,after),set_extension(none,[couple(none,[identifier(none,s),typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))])]))])],[]),event(rodinpos('FENCEM5','ObserveLoadAfterStore','_gpfVsepmEeSvO6bvOrqamw'),'ObserveLoadAfterStore',ordinary(none),['ObserveLoadAfterStore'],[identifier(rodinpos('FENCEM5',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM5',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM5',[],'_VLUawuTrEeSu4vk92SnwF{'),s)],[member(rodinpos('FENCEM5',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM5',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM5',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM5',grd4,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),forall(rodinpos('FENCEM5',grd5,'_VLUawuTrEeSu4vk92SnwFz'),[identifier(none,f)],implication(none,conjunct(none,member(none,identifier(none,f),identifier(none,'TRN')),member(none,identifier(none,f),identifier(none,issuedfence))),not_equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])))),member(rodinpos('FENCEM5',grd6,grd1),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM5',grd7,grd2),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM5',grd8,grd3),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),member(rodinpos('FENCEM5',grd9,grd4),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),member(rodinpos('FENCEM5',grd10,grd5),identifier(none,s),domain(none,identifier(none,after))),member(rodinpos('FENCEM5',grd11,act3),function(none,identifier(none,address),[identifier(none,l)]),domain(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)])))],[],[assign(rodinpos('FENCEM5',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM5',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))]),assign(rodinpos('FENCEM5',act3,act1),[identifier(none,after)],[overwrite(none,identifier(none,after),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,after),[identifier(none,s)]),set_extension(none,[identifier(none,l)]))])]))]),assign(rodinpos('FENCEM5',act4,act2),[identifier(none,registerfile)],[overwrite(none,identifier(none,registerfile),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,registerfile),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,register),[identifier(none,l)]),function(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),[function(none,identifier(none,address),[identifier(none,l)])])])]))])]))])],[]),event(rodinpos('FENCEM5','ObserveLoad',evt1),'ObserveLoad',ordinary(none),['ObserveLoad'],[identifier(rodinpos('FENCEM5',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM5',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM5',[],'_VLUawuTrEeSu4vk92SnwF{'),s)],[member(rodinpos('FENCEM5',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM5',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM5',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM5',grd4,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),forall(rodinpos('FENCEM5',grd5,'_VLUawuTrEeSu4vk92SnwFz'),[identifier(none,f)],implication(none,conjunct(none,member(none,identifier(none,f),identifier(none,'TRN')),member(none,identifier(none,f),identifier(none,issuedfence))),not_equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])))),member(rodinpos('FENCEM5',grd6,grd1),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM5',grd7,grd2),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),implication(rodinpos('FENCEM5',grd8,grd3),member(none,identifier(none,s),identifier(none,observed)),not_member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)]))),member(rodinpos('FENCEM5',grd9,act3),function(none,identifier(none,address),[identifier(none,l)]),domain(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)])))],[],[assign(rodinpos('FENCEM5',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM5',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))]),assign(rodinpos('FENCEM5',act3,act2),[identifier(none,registerfile)],[overwrite(none,identifier(none,registerfile),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,registerfile),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,register),[identifier(none,l)]),function(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),[function(none,identifier(none,address),[identifier(none,l)])])])]))])]))])],[]),event(rodinpos('FENCEM5','ObserveLoadFenceAfterStore','_gpfVsepmEeSvO6bvOrqamx'),'ObserveLoadFenceAfterStore',ordinary(none),['ObserveLoadFenceAfterStore'],[identifier(rodinpos('FENCEM5',[],'_VLUawuTrEeSu4vk92SnwFx'),f),identifier(rodinpos('FENCEM5',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM5',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM5',[],'_VLUawuTrEeSu4vk92SnwF}'),s)],[member(rodinpos('FENCEM5',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM5',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM5',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM5',grd4,'_VLUawuTrEeSu4vk92SnwF{'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),member(rodinpos('FENCEM5',grd5,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,f),identifier(none,issuedfence)),equal(rodinpos('FENCEM5',grd6,'_VLUawuTrEeSu4vk92SnwF|'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),implication(rodinpos('FENCEM5',grd7,'_VLUawuTrEeSu4vk92SnwFz'),not_member(none,identifier(none,l),function(none,identifier(none,ahead),[identifier(none,f)])),forall(none,[identifier(none,a)],implication(none,conjunct(none,member(none,identifier(none,a),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,a),function(none,identifier(none,ahead),[identifier(none,f)])),member(none,identifier(none,a),domain(none,identifier(none,observers))))),member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,a)]))))),member(rodinpos('FENCEM5',grd8,'_VLUawuTrEeSu4vk92SnwF~'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM5',grd9,'_VLUawuTrEeSu4vk92SnwG\''),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM5',grd10,'_VLUawuTrEeSu4vk92SnwG('),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),member(rodinpos('FENCEM5',grd11,'_VLUawuTrEeSu4vk92SnwG)'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),member(rodinpos('FENCEM5',grd12,'_VLUawuTrEeSu4vk92SnwG*'),identifier(none,s),domain(none,identifier(none,after))),member(rodinpos('FENCEM5',grd13,grd1),function(none,identifier(none,address),[identifier(none,l)]),domain(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)])))],[],[assign(rodinpos('FENCEM5',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM5',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))]),assign(rodinpos('FENCEM5',act3,'_VLUawuTrEeSu4vk92SnwG+'),[identifier(none,after)],[overwrite(none,identifier(none,after),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,after),[identifier(none,s)]),set_extension(none,[identifier(none,l)]))])]))]),assign(rodinpos('FENCEM5',act4,act1),[identifier(none,registerfile)],[overwrite(none,identifier(none,registerfile),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,registerfile),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,register),[identifier(none,l)]),function(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),[function(none,identifier(none,address),[identifier(none,l)])])])]))])]))])],[]),event(rodinpos('FENCEM5','ObserveLoadFence','_gpfVsepmEeSvO6bvOrqamy'),'ObserveLoadFence',ordinary(none),['ObserveLoadFence'],[identifier(rodinpos('FENCEM5',[],'_VLUawuTrEeSu4vk92SnwFx'),f),identifier(rodinpos('FENCEM5',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM5',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM5',[],'_VLUawuTrEeSu4vk92SnwF}'),s)],[member(rodinpos('FENCEM5',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM5',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM5',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM5',grd4,'_VLUawuTrEeSu4vk92SnwF{'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),member(rodinpos('FENCEM5',grd5,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,f),identifier(none,issuedfence)),equal(rodinpos('FENCEM5',grd6,'_VLUawuTrEeSu4vk92SnwF|'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),implication(rodinpos('FENCEM5',grd7,'_VLUawuTrEeSu4vk92SnwFz'),not_member(none,identifier(none,l),function(none,identifier(none,ahead),[identifier(none,f)])),forall(none,[identifier(none,a)],implication(none,conjunct(none,member(none,identifier(none,a),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,a),function(none,identifier(none,ahead),[identifier(none,f)])),member(none,identifier(none,a),domain(none,identifier(none,observers))))),member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,a)]))))),member(rodinpos('FENCEM5',grd8,'_VLUawuTrEeSu4vk92SnwF~'),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM5',grd9,'_VLUawuTrEeSu4vk92SnwG\''),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),implication(rodinpos('FENCEM5',grd10,'_VLUawuTrEeSu4vk92SnwG('),member(none,identifier(none,s),identifier(none,observed)),conjunct(none,not_member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),equal(none,function(none,identifier(none,after),[identifier(none,s)]),typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))))),member(rodinpos('FENCEM5',grd11,grd1),function(none,identifier(none,address),[identifier(none,l)]),domain(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)])))],[],[assign(rodinpos('FENCEM5',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM5',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))]),assign(rodinpos('FENCEM5',act3,act1),[identifier(none,registerfile)],[overwrite(none,identifier(none,registerfile),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,registerfile),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,register),[identifier(none,l)]),function(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),[function(none,identifier(none,address),[identifier(none,l)])])])]))])]))])],[]),event(rodinpos('FENCEM5','ObserveStore','_gpfVsepmEeSvO6bvOrqamz'),'ObserveStore',ordinary(none),['ObserveStore'],[identifier(rodinpos('FENCEM5',[],'_VLVB0OTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM5',[],'_VLUaxeTrEeSu4vk92SnwFw'),s)],[member(rodinpos('FENCEM5',grd1,'_VLVB0eTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM5',grd2,'_VLVB0uTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE')),not_member(rodinpos('FENCEM5',grd3,'_VLVB0-TrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),forall(rodinpos('FENCEM5',grd4,grd1),[identifier(none,f)],implication(none,conjunct(none,member(none,identifier(none,f),identifier(none,'TRN')),member(none,identifier(none,f),identifier(none,issuedfence))),not_equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)]))))],[],[assign(rodinpos('FENCEM5',act1,'_VLVB1OTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,s)]))]),assign(rodinpos('FENCEM5',act2,'_VLVB1eTrEeSu4vk92SnwFw'),[identifier(none,lastobservedvalue)],[overwrite(none,identifier(none,lastobservedvalue),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,value),[identifier(none,s)])])]))])]))]),assign(rodinpos('FENCEM5',act3,'_VLVo4OTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,observers),[identifier(none,s)]),set_extension(none,[identifier(none,m)]))])]))])],[]),event(rodinpos('FENCEM5','ObserveStoreFence','_gpfVsepmEeSvO6bvOrqam{'),'ObserveStoreFence',ordinary(none),['ObserveStoreFence'],[identifier(rodinpos('FENCEM5',[],'_VLVo4OTrEeSu4vk92SnwFx'),f),identifier(rodinpos('FENCEM5',[],'_VLVB0OTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM5',[],'_VLUaxeTrEeSu4vk92SnwFw'),s)],[member(rodinpos('FENCEM5',grd1,'_VLVB0eTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM5',grd2,'_VLVB0uTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE')),not_member(rodinpos('FENCEM5',grd3,'_VLVB0-TrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),member(rodinpos('FENCEM5',grd4,grd1),identifier(none,f),identifier(none,issuedfence)),equal(rodinpos('FENCEM5',grd5,grd2),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),implication(rodinpos('FENCEM5',grd6,grd3),not_member(none,identifier(none,s),function(none,identifier(none,ahead),[identifier(none,f)])),forall(none,[identifier(none,a)],implication(none,conjunct(none,member(none,identifier(none,a),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,a),function(none,identifier(none,ahead),[identifier(none,f)])),member(none,identifier(none,a),domain(none,identifier(none,observers))))),member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,a)])))))],[],[assign(rodinpos('FENCEM5',act1,'_VLVB1OTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,s)]))]),assign(rodinpos('FENCEM5',act2,'_VLVB1eTrEeSu4vk92SnwFw'),[identifier(none,lastobservedvalue)],[overwrite(none,identifier(none,lastobservedvalue),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,value),[identifier(none,s)])])]))])]))]),assign(rodinpos('FENCEM5',act3,'_VLVo4OTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,observers),[identifier(none,s)]),set_extension(none,[identifier(none,m)]))])]))])],[]),event(rodinpos('FENCEM5','IssueFence','_gpfVsepmEeSvO6bvOrqam|'),'IssueFence',ordinary(none),['IssueFence'],[identifier(rodinpos('FENCEM5',[],'\''),f),identifier(rodinpos('FENCEM5',[],'*'),m)],[member(rodinpos('FENCEM5',grd1,'('),identifier(none,f),identifier(none,'FENCE')),member(rodinpos('FENCEM5',grd2,'+'),identifier(none,m),identifier(none,'MASTER')),equal(rodinpos('FENCEM5',grd3,','),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),not_member(rodinpos('FENCEM5',grd4,'-'),identifier(none,f),identifier(none,issuedfence))],[],[assign(rodinpos('FENCEM5',act1,')'),[identifier(none,issuedfence)],[union(none,identifier(none,issuedfence),set_extension(none,[identifier(none,f)]))]),assign(rodinpos('FENCEM5',act2,'.'),[identifier(none,ahead)],[overwrite(none,identifier(none,ahead),set_extension(none,[couple(none,[identifier(none,f),event_b_comprehension_set(none,[identifier(none,t)],identifier(none,t),conjunct(none,member(none,identifier(none,t),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,t),identifier(none,issued)),equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,t)])))))])]))])],[])])]),event_b_model(none,'FENCEM4',[sees(none,['GC1','GC1a','GC2','GC3','FENCEC4']),refines(none,'GM3'),variables(none,[identifier(none,after),identifier(none,ahead),identifier(none,issued),identifier(none,issuedfence),identifier(none,lastobservedvalue),identifier(none,observed),identifier(none,observers)]),invariant(none,[subset(rodinpos('FENCEM4',inv1,'_gpfVsepmEeSvO6bvOrqamo'),identifier(none,issuedfence),identifier(none,'FENCE')),member(rodinpos('FENCEM4',inv2,'_gpfVsepmEeSvO6bvOrqamq'),identifier(none,ahead),total_function(none,identifier(none,'FENCE'),pow_subset(none,identifier(none,'MEMACCESS')))),forall(rodinpos('FENCEM4',inv3,'_gpfVsepmEeSvO6bvOrqamr'),[identifier(none,f)],implication(none,conjunct(none,member(none,identifier(none,f),identifier(none,'TRN')),member(none,identifier(none,f),identifier(none,'FENCE'))),member(none,identifier(none,f),domain(none,identifier(none,ahead))))),member(rodinpos('FENCEM4',inv4,'_gpfVsepmEeSvO6bvOrqamt'),identifier(none,after),partial_function(none,identifier(none,'STORE'),pow_subset(none,identifier(none,'LOAD')))),forall(rodinpos('FENCEM4',inv5,'_gpfVsepmEeSvO6bvOrqamu'),[identifier(none,i)],implication(none,conjunct(none,member(none,identifier(none,i),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,i),identifier(none,issued)),member(none,identifier(none,i),identifier(none,'STORE')))),member(none,identifier(none,i),domain(none,identifier(none,after)))))]),theorems(none,[]),events(none,[event(rodinpos('FENCEM4','INITIALISATION','_gpfVsepmEeSvO6bvOrqamh'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('FENCEM4',act1,'_VLR-g-TrEeSu4vk92SnwFw'),[identifier(none,issued)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('FENCEM4',act2,'_VLR-hOTrEeSu4vk92SnwFw'),[identifier(none,observed)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('FENCEM4',act3,'_VLSlkOTrEeSu4vk92SnwFw'),[identifier(none,lastobservedvalue)],[cartesian_product(none,identifier(none,'MASTER'),set_extension(none,[cartesian_product(none,identifier(none,'ADDR'),set_extension(none,[identifier(none,'V0')]))]))]),assign(rodinpos('FENCEM4',act4,'_VLSlkeTrEeSu4vk92SnwFw'),[identifier(none,observers)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'TRN'),pow_subset(none,identifier(none,'MASTER')))))]),assign(rodinpos('FENCEM4',act5,'\''),[identifier(none,issuedfence)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('FENCEM4',act6,'('),[identifier(none,ahead)],[cartesian_product(none,identifier(none,'FENCE'),set_extension(none,[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]))]),assign(rodinpos('FENCEM4',act7,')'),[identifier(none,after)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'TRN'),pow_subset(none,identifier(none,'TRN')))))])],[]),event(rodinpos('FENCEM4','IssueLoad','_gpfVsepmEeSvO6bvOrqami'),'IssueLoad',ordinary(none),['IssueLoad'],[identifier(rodinpos('FENCEM4',[],'_VLSlk-TrEeSu4vk92SnwFw'),l)],[not_member(rodinpos('FENCEM4',grd1,'_VLSllOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM4',grd2,'_VLSlleTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD'))],[],[assign(rodinpos('FENCEM4',act1,'_VLTMoOTrEeSu4vk92SnwFw'),[identifier(none,issued)],[union(none,identifier(none,issued),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM4',act2,'_VLTMoeTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),typeof(none,empty_set(none),pow_subset(none,identifier(none,'MASTER')))])]))])],[]),event(rodinpos('FENCEM4','IssueStore','_gpfVsepmEeSvO6bvOrqamj'),'IssueStore',ordinary(none),['IssueStore'],[identifier(rodinpos('FENCEM4',[],'_VLTMo-TrEeSu4vk92SnwFw'),s)],[not_member(rodinpos('FENCEM4',grd1,'_VLTMpOTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM4',grd2,'_VLTMpeTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE'))],[],[assign(rodinpos('FENCEM4',act1,'_VLTzsOTrEeSu4vk92SnwFw'),[identifier(none,issued)],[union(none,identifier(none,issued),set_extension(none,[identifier(none,s)]))]),assign(rodinpos('FENCEM4',act2,'_VLTzseTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,s),typeof(none,empty_set(none),pow_subset(none,identifier(none,'MASTER')))])]))]),assign(rodinpos('FENCEM4',act3,'_VLTzseTrEeSu4vk92SnwFx'),[identifier(none,after)],[overwrite(none,identifier(none,after),set_extension(none,[couple(none,[identifier(none,s),typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))])]))])],[]),event(rodinpos('FENCEM4','ObserveLoadAfterStore','_gpfVsepmEeSvO6bvOrqamk'),'ObserveLoadAfterStore',ordinary(none),['ObserveLoad'],[identifier(rodinpos('FENCEM4',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM4',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM4',[],'_VLUawuTrEeSu4vk92SnwF{'),s)],[member(rodinpos('FENCEM4',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM4',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM4',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM4',grd4,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),forall(rodinpos('FENCEM4',grd5,'_VLUawuTrEeSu4vk92SnwFz'),[identifier(none,f)],implication(none,conjunct(none,member(none,identifier(none,f),identifier(none,'TRN')),member(none,identifier(none,f),identifier(none,issuedfence))),not_equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])))),member(rodinpos('FENCEM4',grd6,grd1),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM4',grd7,grd2),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM4',grd8,grd3),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),member(rodinpos('FENCEM4',grd9,grd4),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),member(rodinpos('FENCEM4',grd10,grd5),identifier(none,s),domain(none,identifier(none,after)))],[],[assign(rodinpos('FENCEM4',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM4',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))]),assign(rodinpos('FENCEM4',act3,act1),[identifier(none,after)],[overwrite(none,identifier(none,after),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,after),[identifier(none,s)]),set_extension(none,[identifier(none,l)]))])]))])],[]),event(rodinpos('FENCEM4','ObserveLoad',evt4),'ObserveLoad',ordinary(none),['ObserveLoad'],[identifier(rodinpos('FENCEM4',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM4',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM4',[],'_VLUawuTrEeSu4vk92SnwF{'),s)],[member(rodinpos('FENCEM4',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM4',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM4',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM4',grd4,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),forall(rodinpos('FENCEM4',grd5,'_VLUawuTrEeSu4vk92SnwFz'),[identifier(none,f)],implication(none,conjunct(none,member(none,identifier(none,f),identifier(none,'TRN')),member(none,identifier(none,f),identifier(none,issuedfence))),not_equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])))),member(rodinpos('FENCEM4',grd6,grd1),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM4',grd7,grd2),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),implication(rodinpos('FENCEM4',grd8,grd3),member(none,identifier(none,s),identifier(none,observed)),not_member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])))],[],[assign(rodinpos('FENCEM4',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM4',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))])],[]),event(rodinpos('FENCEM4','ObserveLoadFenceAfterStore',evt1),'ObserveLoadFenceAfterStore',ordinary(none),['ObserveLoad'],[identifier(rodinpos('FENCEM4',[],'_VLUawuTrEeSu4vk92SnwFx'),f),identifier(rodinpos('FENCEM4',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM4',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM4',[],'_VLUawuTrEeSu4vk92SnwF}'),s)],[member(rodinpos('FENCEM4',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM4',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM4',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM4',grd4,'_VLUawuTrEeSu4vk92SnwF{'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),member(rodinpos('FENCEM4',grd5,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,f),identifier(none,issuedfence)),equal(rodinpos('FENCEM4',grd6,'_VLUawuTrEeSu4vk92SnwF|'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),implication(rodinpos('FENCEM4',grd7,'_VLUawuTrEeSu4vk92SnwFz'),not_member(none,identifier(none,l),function(none,identifier(none,ahead),[identifier(none,f)])),forall(none,[identifier(none,a)],implication(none,conjunct(none,member(none,identifier(none,a),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,a),function(none,identifier(none,ahead),[identifier(none,f)])),member(none,identifier(none,a),domain(none,identifier(none,observers))))),member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,a)]))))),member(rodinpos('FENCEM4',grd8,'_VLUawuTrEeSu4vk92SnwF~'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM4',grd9,'_VLUawuTrEeSu4vk92SnwG\''),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM4',grd10,'_VLUawuTrEeSu4vk92SnwG('),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),member(rodinpos('FENCEM4',grd11,'_VLUawuTrEeSu4vk92SnwG)'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),member(rodinpos('FENCEM4',grd12,'_VLUawuTrEeSu4vk92SnwG*'),identifier(none,s),domain(none,identifier(none,after)))],[],[assign(rodinpos('FENCEM4',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM4',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))]),assign(rodinpos('FENCEM4',act3,'_VLUawuTrEeSu4vk92SnwG+'),[identifier(none,after)],[overwrite(none,identifier(none,after),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,after),[identifier(none,s)]),set_extension(none,[identifier(none,l)]))])]))])],[]),event(rodinpos('FENCEM4','ObserveLoadFence',evt2),'ObserveLoadFence',ordinary(none),['ObserveLoad'],[identifier(rodinpos('FENCEM4',[],'_VLUawuTrEeSu4vk92SnwFx'),f),identifier(rodinpos('FENCEM4',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('FENCEM4',[],'_VLTztOTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM4',[],'_VLUawuTrEeSu4vk92SnwF}'),s)],[member(rodinpos('FENCEM4',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('FENCEM4',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('FENCEM4',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)])),equal(rodinpos('FENCEM4',grd4,'_VLUawuTrEeSu4vk92SnwF{'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,l)])),member(rodinpos('FENCEM4',grd5,'_VLUawuTrEeSu4vk92SnwFy'),identifier(none,f),identifier(none,issuedfence)),equal(rodinpos('FENCEM4',grd6,'_VLUawuTrEeSu4vk92SnwF|'),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),implication(rodinpos('FENCEM4',grd7,'_VLUawuTrEeSu4vk92SnwFz'),not_member(none,identifier(none,l),function(none,identifier(none,ahead),[identifier(none,f)])),forall(none,[identifier(none,a)],implication(none,conjunct(none,member(none,identifier(none,a),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,a),function(none,identifier(none,ahead),[identifier(none,f)])),member(none,identifier(none,a),domain(none,identifier(none,observers))))),member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,a)]))))),member(rodinpos('FENCEM4',grd8,'_VLUawuTrEeSu4vk92SnwF~'),identifier(none,s),identifier(none,'STORE')),equal(rodinpos('FENCEM4',grd9,'_VLUawuTrEeSu4vk92SnwG\''),function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,address),[identifier(none,l)])),implication(rodinpos('FENCEM4',grd10,'_VLUawuTrEeSu4vk92SnwG('),member(none,identifier(none,s),identifier(none,observed)),conjunct(none,not_member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),equal(none,function(none,identifier(none,after),[identifier(none,s)]),typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN'))))))],[],[assign(rodinpos('FENCEM4',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('FENCEM4',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))])],[]),event(rodinpos('FENCEM4','ObserveStore','_gpfVsepmEeSvO6bvOrqaml'),'ObserveStore',ordinary(none),['ObserveStore'],[identifier(rodinpos('FENCEM4',[],'_VLVB0OTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM4',[],'_VLUaxeTrEeSu4vk92SnwFw'),s)],[member(rodinpos('FENCEM4',grd1,'_VLVB0eTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM4',grd2,'_VLVB0uTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE')),not_member(rodinpos('FENCEM4',grd3,'_VLVB0-TrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),forall(rodinpos('FENCEM4',grd4,grd1),[identifier(none,f)],implication(none,conjunct(none,member(none,identifier(none,f),identifier(none,'TRN')),member(none,identifier(none,f),identifier(none,issuedfence))),not_equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)]))))],[],[assign(rodinpos('FENCEM4',act1,'_VLVB1OTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,s)]))]),assign(rodinpos('FENCEM4',act2,'_VLVB1eTrEeSu4vk92SnwFw'),[identifier(none,lastobservedvalue)],[overwrite(none,identifier(none,lastobservedvalue),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,value),[identifier(none,s)])])]))])]))]),assign(rodinpos('FENCEM4',act3,'_VLVo4OTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,observers),[identifier(none,s)]),set_extension(none,[identifier(none,m)]))])]))])],[]),event(rodinpos('FENCEM4','ObserveStoreFence',evt3),'ObserveStoreFence',ordinary(none),['ObserveStore'],[identifier(rodinpos('FENCEM4',[],'_VLVo4OTrEeSu4vk92SnwFx'),f),identifier(rodinpos('FENCEM4',[],'_VLVB0OTrEeSu4vk92SnwFw'),m),identifier(rodinpos('FENCEM4',[],'_VLUaxeTrEeSu4vk92SnwFw'),s)],[member(rodinpos('FENCEM4',grd1,'_VLVB0eTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('FENCEM4',grd2,'_VLVB0uTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE')),not_member(rodinpos('FENCEM4',grd3,'_VLVB0-TrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)])),member(rodinpos('FENCEM4',grd4,grd1),identifier(none,f),identifier(none,issuedfence)),equal(rodinpos('FENCEM4',grd5,grd2),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),implication(rodinpos('FENCEM4',grd6,grd3),not_member(none,identifier(none,s),function(none,identifier(none,ahead),[identifier(none,f)])),forall(none,[identifier(none,a)],implication(none,conjunct(none,member(none,identifier(none,a),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,a),function(none,identifier(none,ahead),[identifier(none,f)])),member(none,identifier(none,a),domain(none,identifier(none,observers))))),member(none,identifier(none,m),function(none,identifier(none,observers),[identifier(none,a)])))))],[],[assign(rodinpos('FENCEM4',act1,'_VLVB1OTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,s)]))]),assign(rodinpos('FENCEM4',act2,'_VLVB1eTrEeSu4vk92SnwFw'),[identifier(none,lastobservedvalue)],[overwrite(none,identifier(none,lastobservedvalue),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,value),[identifier(none,s)])])]))])]))]),assign(rodinpos('FENCEM4',act3,'_VLVo4OTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,observers),[identifier(none,s)]),set_extension(none,[identifier(none,m)]))])]))])],[]),event(rodinpos('FENCEM4','IssueFence','_gpfVsepmEeSvO6bvOrqamm'),'IssueFence',ordinary(none),[],[identifier(rodinpos('FENCEM4',[],'\''),f),identifier(rodinpos('FENCEM4',[],'*'),m)],[member(rodinpos('FENCEM4',grd1,'('),identifier(none,f),identifier(none,'FENCE')),member(rodinpos('FENCEM4',grd2,'+'),identifier(none,m),identifier(none,'MASTER')),equal(rodinpos('FENCEM4',grd3,','),identifier(none,m),function(none,identifier(none,issuer),[identifier(none,f)])),not_member(rodinpos('FENCEM4',grd4,'-'),identifier(none,f),identifier(none,issuedfence))],[],[assign(rodinpos('FENCEM4',act1,')'),[identifier(none,issuedfence)],[union(none,identifier(none,issuedfence),set_extension(none,[identifier(none,f)]))]),assign(rodinpos('FENCEM4',act2,'.'),[identifier(none,ahead)],[overwrite(none,identifier(none,ahead),set_extension(none,[couple(none,[identifier(none,f),event_b_comprehension_set(none,[identifier(none,t)],identifier(none,t),conjunct(none,member(none,identifier(none,t),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,t),identifier(none,issued)),equal(none,identifier(none,m),function(none,identifier(none,issuer),[identifier(none,t)])))))])]))])],[])])]),event_b_model(none,'GM3',[sees(none,['GC1','GC1a','GC2','GC3']),refines(none,'GM2'),variables(none,[identifier(none,issued),identifier(none,lastobservedvalue),identifier(none,observed),identifier(none,observers)]),invariant(none,[member(rodinpos('GM3',inv1,'_VLRXdOTrEeSu4vk92SnwFw'),identifier(none,lastobservedvalue),partial_function(none,identifier(none,'MASTER'),partial_function(none,identifier(none,'ADDR'),identifier(none,'VALUE')))),member(rodinpos('GM3',inv2,'_VLR-gOTrEeSu4vk92SnwFw'),identifier(none,observers),partial_function(none,identifier(none,'MEMACCESS'),pow_subset(none,identifier(none,'MASTER')))),forall(rodinpos('GM3',inv3,'_VLR-geTrEeSu4vk92SnwFw'),[identifier(none,i)],implication(none,conjunct(none,member(none,identifier(none,i),identifier(none,'TRN')),conjunct(none,member(none,identifier(none,i),identifier(none,issued)),member(none,identifier(none,i),identifier(none,'MEMACCESS')))),member(none,identifier(none,i),domain(none,identifier(none,observers))))),forall(rodinpos('GM3',inv4,'_VLR-guTrEeSu4vk92SnwFw'),[identifier(none,m)],implication(none,conjunct(none,member(none,identifier(none,m),identifier(none,'MASTER')),member(none,identifier(none,m),identifier(none,'MASTER'))),member(none,identifier(none,m),domain(none,identifier(none,lastobservedvalue)))))]),theorems(none,[]),events(none,[event(rodinpos('GM3','INITIALISATION','_SuFYwuTqEeSu4vk92SnwFx'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('GM3',act1,'_VLR-g-TrEeSu4vk92SnwFw'),[identifier(none,issued)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('GM3',act2,'_VLR-hOTrEeSu4vk92SnwFw'),[identifier(none,observed)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('GM3',act3,'_VLSlkOTrEeSu4vk92SnwFw'),[identifier(none,lastobservedvalue)],[cartesian_product(none,identifier(none,'MASTER'),set_extension(none,[cartesian_product(none,identifier(none,'ADDR'),set_extension(none,[identifier(none,'V0')]))]))]),assign(rodinpos('GM3',act4,'_VLSlkeTrEeSu4vk92SnwFw'),[identifier(none,observers)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'TRN'),pow_subset(none,identifier(none,'MASTER')))))])],[]),event(rodinpos('GM3','IssueLoad','_SuFYwuTqEeSu4vk92SnwFy'),'IssueLoad',ordinary(none),['IssueLoad'],[identifier(rodinpos('GM3',[],'_VLSlk-TrEeSu4vk92SnwFw'),l)],[not_member(rodinpos('GM3',grd1,'_VLSllOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('GM3',grd2,'_VLSlleTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD'))],[],[assign(rodinpos('GM3',act1,'_VLTMoOTrEeSu4vk92SnwFw'),[identifier(none,issued)],[union(none,identifier(none,issued),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('GM3',act2,'_VLTMoeTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),typeof(none,empty_set(none),pow_subset(none,identifier(none,'MASTER')))])]))])],[]),event(rodinpos('GM3','IssueStore','_SuFYwuTqEeSu4vk92SnwFz'),'IssueStore',ordinary(none),['IssueStore'],[identifier(rodinpos('GM3',[],'_VLTMo-TrEeSu4vk92SnwFw'),s)],[not_member(rodinpos('GM3',grd1,'_VLTMpOTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('GM3',grd2,'_VLTMpeTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE'))],[],[assign(rodinpos('GM3',act1,'_VLTzsOTrEeSu4vk92SnwFw'),[identifier(none,issued)],[union(none,identifier(none,issued),set_extension(none,[identifier(none,s)]))]),assign(rodinpos('GM3',act2,'_VLTzseTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,s),typeof(none,empty_set(none),pow_subset(none,identifier(none,'MASTER')))])]))])],[]),event(rodinpos('GM3','ObserveLoad','_SuFYwuTqEeSu4vk92SnwF{'),'ObserveLoad',ordinary(none),['ObserveLoad'],[identifier(rodinpos('GM3',[],'_VLTzs-TrEeSu4vk92SnwFw'),l),identifier(rodinpos('GM3',[],'_VLTztOTrEeSu4vk92SnwFw'),m)],[member(rodinpos('GM3',grd1,'_VLTzteTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('GM3',grd2,'_VLUawOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD')),not_member(rodinpos('GM3',grd3,'_VLUaweTrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,l)]))],[],[assign(rodinpos('GM3',act1,'_VLUawuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))]),assign(rodinpos('GM3',act2,'_VLUaw-TrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,l),union(none,function(none,identifier(none,observers),[identifier(none,l)]),set_extension(none,[identifier(none,m)]))])]))])],[]),event(rodinpos('GM3','ObserveStore','_SuFYwuTqEeSu4vk92SnwF|'),'ObserveStore',ordinary(none),['ObserveStore'],[identifier(rodinpos('GM3',[],'_VLVB0OTrEeSu4vk92SnwFw'),m),identifier(rodinpos('GM3',[],'_VLUaxeTrEeSu4vk92SnwFw'),s)],[member(rodinpos('GM3',grd1,'_VLVB0eTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('GM3',grd2,'_VLVB0uTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE')),not_member(rodinpos('GM3',grd3,'_VLVB0-TrEeSu4vk92SnwFw'),identifier(none,m),function(none,identifier(none,observers),[identifier(none,s)]))],[],[assign(rodinpos('GM3',act1,'_VLVB1OTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,s)]))]),assign(rodinpos('GM3',act2,'_VLVB1eTrEeSu4vk92SnwFw'),[identifier(none,lastobservedvalue)],[overwrite(none,identifier(none,lastobservedvalue),set_extension(none,[couple(none,[identifier(none,m),overwrite(none,function(none,identifier(none,lastobservedvalue),[identifier(none,m)]),set_extension(none,[couple(none,[function(none,identifier(none,address),[identifier(none,s)]),function(none,identifier(none,value),[identifier(none,s)])])]))])]))]),assign(rodinpos('GM3',act3,'_VLVo4OTrEeSu4vk92SnwFw'),[identifier(none,observers)],[overwrite(none,identifier(none,observers),set_extension(none,[couple(none,[identifier(none,s),union(none,function(none,identifier(none,observers),[identifier(none,s)]),set_extension(none,[identifier(none,m)]))])]))])],[])])]),event_b_model(none,'GM2',[sees(none,['GC1','GC1a','GC2']),refines(none,'GM1'),variables(none,[identifier(none,issued),identifier(none,observed)]),invariant(none,[]),theorems(none,[]),events(none,[event(rodinpos('GM2','INITIALISATION','_SuFYwuTqEeSu4vk92SnwFx'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('GM2',act1,'_AkgHwOTrEeSu4vk92SnwFw'),[identifier(none,issued)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('GM2',act2,'_AkgHweTrEeSu4vk92SnwFw'),[identifier(none,observed)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))])],[]),event(rodinpos('GM2','IssueLoad','_Akgu0OTrEeSu4vk92SnwFw'),'IssueLoad',ordinary(none),['Issue'],[identifier(rodinpos('GM2',[],'_Akgu0uTrEeSu4vk92SnwFw'),l)],[not_member(rodinpos('GM2',grd1,'_Akgu0-TrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('GM2',grd2,'_AkhV4OTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD'))],[],[assign(rodinpos('GM2',act1,'_AkhV4uTrEeSu4vk92SnwFw'),[identifier(none,issued)],[union(none,identifier(none,issued),set_extension(none,[identifier(none,l)]))])],[witness(none,identifier(none,ma),equal(rodinpos('GM2',ma,'_AkhV4eTrEeSu4vk92SnwFw'),identifier(none,ma),identifier(none,l)))]),event(rodinpos('GM2','IssueStore','_AkhV4-TrEeSu4vk92SnwFw'),'IssueStore',ordinary(none),['Issue'],[identifier(rodinpos('GM2',[],'_Akh88eTrEeSu4vk92SnwFw'),s)],[not_member(rodinpos('GM2',grd1,'_Akh88uTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('GM2',grd2,'_Akh88-TrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE'))],[],[assign(rodinpos('GM2',act1,'_AkikAeTrEeSu4vk92SnwFw'),[identifier(none,issued)],[union(none,identifier(none,issued),set_extension(none,[identifier(none,s)]))])],[witness(none,identifier(none,ma),equal(rodinpos('GM2',ma,'_AkikAOTrEeSu4vk92SnwFw'),identifier(none,ma),identifier(none,s)))]),event(rodinpos('GM2','ObserveLoad','_AkikAuTrEeSu4vk92SnwFw'),'ObserveLoad',ordinary(none),['Observe'],[identifier(rodinpos('GM2',[],'_AkikBOTrEeSu4vk92SnwFw'),l)],[member(rodinpos('GM2',grd1,'_AkikBeTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,issued)),member(rodinpos('GM2',grd2,'_AkjLEOTrEeSu4vk92SnwFw'),identifier(none,l),identifier(none,'LOAD'))],[],[assign(rodinpos('GM2',act1,'_AkjLEuTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,l)]))])],[witness(none,identifier(none,ma),equal(rodinpos('GM2',ma,'_AkjLEeTrEeSu4vk92SnwFw'),identifier(none,ma),identifier(none,l)))]),event(rodinpos('GM2','ObserveStore','_AkjLE-TrEeSu4vk92SnwFw'),'ObserveStore',ordinary(none),['Observe'],[identifier(rodinpos('GM2',[],'_AkjyIeTrEeSu4vk92SnwFw'),s)],[member(rodinpos('GM2',grd1,'_AkjyIuTrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,issued)),member(rodinpos('GM2',grd2,'_AkjyI-TrEeSu4vk92SnwFw'),identifier(none,s),identifier(none,'STORE'))],[],[assign(rodinpos('GM2',act1,'_AkjyJeTrEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,s)]))])],[witness(none,identifier(none,ma),equal(rodinpos('GM2',ma,'_AkjyJOTrEeSu4vk92SnwFw'),identifier(none,ma),identifier(none,s)))])])]),event_b_model(none,'GM1',[sees(none,['GC1']),variables(none,[identifier(none,issued),identifier(none,observed)]),invariant(none,[subset(rodinpos('GM1',inv1,'_SuFYw-TqEeSu4vk92SnwFw'),identifier(none,issued),identifier(none,'MEMACCESS')),subset(rodinpos('GM1',inv2,'_SuF_0OTqEeSu4vk92SnwFw'),identifier(none,observed),identifier(none,issued))]),theorems(none,[]),events(none,[event(rodinpos('GM1','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('GM1',act1,'_SuGm4OTqEeSu4vk92SnwFw'),[identifier(none,issued)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))]),assign(rodinpos('GM1',act2,'_SuGm4eTqEeSu4vk92SnwFw'),[identifier(none,observed)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'TRN')))])],[]),event(rodinpos('GM1','Issue','_SuHN8OTqEeSu4vk92SnwFw'),'Issue',ordinary(none),[],[identifier(rodinpos('GM1',[],'_SuHN8eTqEeSu4vk92SnwFw'),ma)],[not_member(rodinpos('GM1',grd1,'_SuH1AOTqEeSu4vk92SnwFw'),identifier(none,ma),identifier(none,issued)),member(rodinpos('GM1',grd2,'_SuH1AeTqEeSu4vk92SnwFw'),identifier(none,ma),identifier(none,'MEMACCESS'))],[],[assign(rodinpos('GM1',act1,'_SuH1AuTqEeSu4vk92SnwFw'),[identifier(none,issued)],[union(none,identifier(none,issued),set_extension(none,[identifier(none,ma)]))])],[]),event(rodinpos('GM1','Observe','_SuIcEOTqEeSu4vk92SnwFw'),'Observe',ordinary(none),[],[identifier(rodinpos('GM1',[],'_SuIcEeTqEeSu4vk92SnwFw'),ma)],[member(rodinpos('GM1',grd1,'_SuJDIOTqEeSu4vk92SnwFw'),identifier(none,ma),identifier(none,issued))],[],[assign(rodinpos('GM1',act1,'_SuJDIeTqEeSu4vk92SnwFw'),[identifier(none,observed)],[union(none,identifier(none,observed),set_extension(none,[identifier(none,ma)]))])],[])])])],[event_b_context(none,'GC1',[extends(none,[]),constants(none,[identifier(none,'MEMACCESS')]),abstract_constants(none,[]),axioms(none,[subset(rodinpos('GC1',axm1,'_ITLgIeTqEeSu4vk92SnwFw'),identifier(none,'MEMACCESS'),identifier(none,'TRN'))]),theorems(none,[]),sets(none,[deferred_set(none,'TRN')])]),event_b_context(none,'GC1a',[extends(none,['GC1']),constants(none,[identifier(none,issuer)]),abstract_constants(none,[]),axioms(none,[member(rodinpos('GC1a',axm1,'*'),identifier(none,issuer),total_function(none,identifier(none,'TRN'),identifier(none,'MASTER')))]),theorems(none,[]),sets(none,[deferred_set(none,'MASTER')])]),event_b_context(none,'GC2',[extends(none,['GC1a']),constants(none,[identifier(none,'LOAD'),identifier(none,'STORE')]),abstract_constants(none,[]),axioms(none,[subset(rodinpos('GC2',axm1,'_H1JD0-TrEeSu4vk92SnwFw'),identifier(none,'LOAD'),identifier(none,'MEMACCESS')),subset(rodinpos('GC2',axm2,'_H1Jq4OTrEeSu4vk92SnwFw'),identifier(none,'STORE'),identifier(none,'MEMACCESS')),partition(rodinpos('GC2',axm3,'_H1Jq4eTrEeSu4vk92SnwFw'),identifier(none,'MEMACCESS'),[identifier(none,'STORE'),identifier(none,'LOAD')])]),theorems(none,[]),sets(none,[])]),event_b_context(none,'GC3',[extends(none,['GC2']),constants(none,[identifier(none,'V0'),identifier(none,'V1'),identifier(none,address),identifier(none,value)]),abstract_constants(none,[]),axioms(none,[member(rodinpos('GC3',axm1,'_bk82V-TrEeSu4vk92SnwFw'),identifier(none,address),total_function(none,identifier(none,'MEMACCESS'),identifier(none,'ADDR'))),member(rodinpos('GC3',axm2,'_bk9dYOTrEeSu4vk92SnwFw'),identifier(none,value),total_function(none,identifier(none,'STORE'),identifier(none,'VALUE'))),member(rodinpos('GC3',axm3,'_bk9dYeTrEeSu4vk92SnwFw'),identifier(none,'V0'),identifier(none,'VALUE')),member(rodinpos('GC3',axm4,'_bk9dYuTrEeSu4vk92SnwFw'),identifier(none,'V1'),identifier(none,'VALUE')),not_equal(rodinpos('GC3',axm5,'_bk9dY-TrEeSu4vk92SnwFw'),identifier(none,'V0'),identifier(none,'V1'))]),theorems(none,[]),sets(none,[deferred_set(none,'ADDR'),deferred_set(none,'VALUE')])]),event_b_context(none,'FENCEC4',[extends(none,['GC3']),constants(none,[identifier(none,'FENCE')]),abstract_constants(none,[]),axioms(none,[partition(rodinpos('FENCEC4',axm1,')'),identifier(none,'TRN'),[identifier(none,'MEMACCESS'),identifier(none,'FENCE')])]),theorems(none,[]),sets(none,[])]),event_b_context(none,'FENCEC5',[extends(none,['FENCEC4']),constants(none,[identifier(none,register)]),abstract_constants(none,[]),axioms(none,[member(rodinpos('FENCEC5',axm1,'*'),identifier(none,register),total_function(none,identifier(none,'LOAD'),identifier(none,'REG')))]),theorems(none,[]),sets(none,[deferred_set(none,'REG')])]),event_b_context(none,'FENCEC6',[extends(none,['FENCEC5']),constants(none,[identifier(none,'A1'),identifier(none,'A2'),identifier(none,'I11'),identifier(none,'I21'),identifier(none,'I31'),identifier(none,'I32'),identifier(none,'I33'),identifier(none,'I41'),identifier(none,'I42'),identifier(none,'I43'),identifier(none,'M1'),identifier(none,'M2'),identifier(none,'M3'),identifier(none,'M4'),identifier(none,'P1'),identifier(none,'P2'),identifier(none,'P3'),identifier(none,'P4'),identifier(none,'PROGRAM'),identifier(none,'R1'),identifier(none,'R2')]),abstract_constants(none,[]),axioms(none,[member(rodinpos('FENCEC6',axm1,cst23),identifier(none,'I11'),identifier(none,'STORE')),member(rodinpos('FENCEC6',axm2,axm1),identifier(none,'I21'),identifier(none,'STORE')),member(rodinpos('FENCEC6',axm3,axm2),identifier(none,'I31'),identifier(none,'LOAD')),member(rodinpos('FENCEC6',axm4,axm3),identifier(none,'I32'),identifier(none,'FENCE')),member(rodinpos('FENCEC6',axm5,cst24),identifier(none,'I33'),identifier(none,'LOAD')),member(rodinpos('FENCEC6',axm6,axm4),identifier(none,'I41'),identifier(none,'LOAD')),member(rodinpos('FENCEC6',axm7,axm5),identifier(none,'I42'),identifier(none,'FENCE')),member(rodinpos('FENCEC6',axm8,cst25),identifier(none,'I43'),identifier(none,'LOAD')),partition(rodinpos('FENCEC6',axm9,axm6),identifier(none,'TRN'),[set_extension(none,[identifier(none,'I11')]),set_extension(none,[identifier(none,'I21')]),set_extension(none,[identifier(none,'I31')]),set_extension(none,[identifier(none,'I32')]),set_extension(none,[identifier(none,'I33')]),set_extension(none,[identifier(none,'I41')]),set_extension(none,[identifier(none,'I42')]),set_extension(none,[identifier(none,'I43')])]),equal(rodinpos('FENCEC6',axm10,axm7),identifier(none,'P1'),set_extension(none,[couple(none,[integer(none,1),identifier(none,'I11')])])),equal(rodinpos('FENCEC6',axm11,axm8),identifier(none,'P2'),set_extension(none,[couple(none,[integer(none,1),identifier(none,'I21')])])),equal(rodinpos('FENCEC6',axm12,axm9),identifier(none,'P3'),set_extension(none,[couple(none,[integer(none,1),identifier(none,'I31')]),couple(none,[integer(none,2),identifier(none,'I32')]),couple(none,[integer(none,3),identifier(none,'I33')])])),equal(rodinpos('FENCEC6',axm13,axm10),identifier(none,'P4'),set_extension(none,[couple(none,[integer(none,1),identifier(none,'I41')]),couple(none,[integer(none,2),identifier(none,'I42')]),couple(none,[integer(none,3),identifier(none,'I43')])])),member(rodinpos('FENCEC6',axm14,axm11),identifier(none,'M1'),identifier(none,'MASTER')),member(rodinpos('FENCEC6',axm16,axm13),identifier(none,'M3'),identifier(none,'MASTER')),member(rodinpos('FENCEC6',axm17,axm14),identifier(none,'M4'),identifier(none,'MASTER')),partition(rodinpos('FENCEC6',axm18,axm15),identifier(none,'MASTER'),[set_extension(none,[identifier(none,'M1')]),set_extension(none,[identifier(none,'M2')]),set_extension(none,[identifier(none,'M3')]),set_extension(none,[identifier(none,'M4')])]),equal(rodinpos('FENCEC6',axm19,axm16),identifier(none,'PROGRAM'),set_extension(none,[couple(none,[identifier(none,'M1'),identifier(none,'P1')]),couple(none,[identifier(none,'M2'),identifier(none,'P2')]),couple(none,[identifier(none,'M3'),identifier(none,'P3')]),couple(none,[identifier(none,'M4'),identifier(none,'P4')])])),equal(rodinpos('FENCEC6',axm20,axm17),identifier(none,issuer),set_extension(none,[couple(none,[identifier(none,'I11'),identifier(none,'M1')]),couple(none,[identifier(none,'I21'),identifier(none,'M2')]),couple(none,[identifier(none,'I31'),identifier(none,'M3')]),couple(none,[identifier(none,'I32'),identifier(none,'M3')]),couple(none,[identifier(none,'I33'),identifier(none,'M3')]),couple(none,[identifier(none,'I41'),identifier(none,'M4')]),couple(none,[identifier(none,'I42'),identifier(none,'M4')]),couple(none,[identifier(none,'I43'),identifier(none,'M4')])])),equal(rodinpos('FENCEC6',axm21,axm18),identifier(none,address),set_extension(none,[couple(none,[identifier(none,'I11'),identifier(none,'A1')]),couple(none,[identifier(none,'I21'),identifier(none,'A2')]),couple(none,[identifier(none,'I31'),identifier(none,'A1')]),couple(none,[identifier(none,'I33'),identifier(none,'A2')]),couple(none,[identifier(none,'I41'),identifier(none,'A2')]),couple(none,[identifier(none,'I43'),identifier(none,'A1')])])),equal(rodinpos('FENCEC6',axm22,axm19),identifier(none,value),set_extension(none,[couple(none,[identifier(none,'I11'),identifier(none,'V1')]),couple(none,[identifier(none,'I21'),identifier(none,'V1')])])),equal(rodinpos('FENCEC6',axm23,axm20),identifier(none,register),set_extension(none,[couple(none,[identifier(none,'I31'),identifier(none,'R1')]),couple(none,[identifier(none,'I33'),identifier(none,'R2')]),couple(none,[identifier(none,'I41'),identifier(none,'R1')]),couple(none,[identifier(none,'I43'),identifier(none,'R2')])])),partition(rodinpos('FENCEC6',axm24,axm21),identifier(none,'ADDR'),[set_extension(none,[identifier(none,'A1')]),set_extension(none,[identifier(none,'A2')])]),partition(rodinpos('FENCEC6',axm25,'cst2?'),identifier(none,'REG'),[set_extension(none,[identifier(none,'R1')]),set_extension(none,[identifier(none,'R2')])]),not_equal(rodinpos('FENCEC6',axm26,'cst2>'),identifier(none,'R1'),identifier(none,'R2'))]),theorems(none,[member(rodinpos('FENCEC6',axm15,axm12),identifier(none,'M2'),identifier(none,'MASTER'))]),sets(none,[])]),event_b_context(none,'FENCEC7',[extends(none,['FENCEC6']),constants(none,[identifier(none,'C0'),identifier(none,'C1'),identifier(none,'C2'),identifier(none,'C3'),identifier(none,'REGCOVER')]),abstract_constants(none,[]),axioms(none,[equal(rodinpos('FENCEC7',axm1,'.'),identifier(none,'C0'),set_extension(none,[couple(none,[identifier(none,'R1'),identifier(none,'V0')]),couple(none,[identifier(none,'R2'),identifier(none,'V0')])])),equal(rodinpos('FENCEC7',axm2,axm1),identifier(none,'C1'),set_extension(none,[couple(none,[identifier(none,'R1'),identifier(none,'V0')]),couple(none,[identifier(none,'R2'),identifier(none,'V1')])])),equal(rodinpos('FENCEC7',axm3,axm2),identifier(none,'C2'),set_extension(none,[couple(none,[identifier(none,'R1'),identifier(none,'V1')]),couple(none,[identifier(none,'R2'),identifier(none,'V0')])])),equal(rodinpos('FENCEC7',axm4,axm3),identifier(none,'C3'),set_extension(none,[couple(none,[identifier(none,'R1'),identifier(none,'V1')]),couple(none,[identifier(none,'R2'),identifier(none,'V1')])])),equal(rodinpos('FENCEC7',axm5,'axm;'),identifier(none,'REGCOVER'),set_extension(none,[identifier(none,'C0'),identifier(none,'C1'),identifier(none,'C2'),identifier(none,'C3')]))]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po('FENCEM7','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po('FENCEM7','Well-definedness of Guard',[guard(grd3),event('CoverRegisterValues')],true),po('FENCEM7','Well-definedness of Guard',[guard(grd4),event('CoverRegisterValues')],true),po('FENCEM7','Invariant preservation',[event('CoverRegisterValues'),invariant(inv1)],true),po('FENCEM6','Well-definedness of Invariant',[invariant(inv1)],true),po('FENCEM6','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po('FENCEM6','Well-definedness of Guard',[guard(grd3),event('IssueLoad')],true),po('FENCEM6','Well-definedness of Guard',[guard(grd4),event('IssueLoad')],true),po('FENCEM6','Well-definedness of Guard',[guard(grd6),event('IssueLoad')],true),po('FENCEM6','Well-definedness of Guard',[guard(grd7),event('IssueLoad')],true),po('FENCEM6','Well-definedness of Guard',[guard(grd3),event('IssueStore')],true),po('FENCEM6','Well-definedness of Guard',[guard(grd4),event('IssueStore')],true),po('FENCEM6','Well-definedness of Guard',[guard(grd6),event('IssueStore')],true),po('FENCEM6','Well-definedness of Guard',[guard(grd7),event('IssueStore')],true),po('FENCEM6','Invariant preservation',[event('ObserveLoadAfterStore'),event('ObserveLoadAfterStore'),invariant(inv1)],false),po('FENCEM6','Invariant preservation',[event('ObserveLoad'),event('ObserveLoad'),invariant(inv1)],false),po('FENCEM6','Invariant preservation',[event('ObserveLoadFenceAfterStore'),event('ObserveLoadFenceAfterStore'),invariant(inv1)],false),po('FENCEM6','Invariant preservation',[event('ObserveLoadFence'),event('ObserveLoadFence'),invariant(inv1)],false),po('FENCEM6','Invariant preservation',[event('ObserveStore'),event('ObserveStore'),invariant(inv1)],false),po('FENCEM6','Invariant preservation',[event('ObserveStoreFence'),event('ObserveStoreFence'),invariant(inv1)],false),po('FENCEM6','Well-definedness of Guard',[guard(grd5),event('IssueFence')],true),po('FENCEM6','Well-definedness of Guard',[guard(grd7),event('IssueFence')],true),po('FENCEM6','Well-definedness of Guard',[guard(grd8),event('IssueFence')],true),po('FENCEM5','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po('FENCEM5','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po('FENCEM5','Well-definedness of Guard',[guard(grd11),event('ObserveLoadAfterStore')],true),po('FENCEM5','Invariant preservation',[event('ObserveLoadAfterStore'),event('ObserveLoadAfterStore'),invariant(inv1)],true),po('FENCEM5','Invariant preservation',[event('ObserveLoadAfterStore'),event('ObserveLoadAfterStore'),invariant(inv2)],true),po('FENCEM5','Well-definedness of action',[action(act4)],true),po('FENCEM5','Well-definedness of Guard',[guard(grd9),event('ObserveLoad')],true),po('FENCEM5','Invariant preservation',[event('ObserveLoad'),event('ObserveLoad'),invariant(inv1)],true),po('FENCEM5','Invariant preservation',[event('ObserveLoad'),event('ObserveLoad'),invariant(inv2)],true),po('FENCEM5','Well-definedness of action',[action(act3)],true),po('FENCEM5','Well-definedness of Guard',[guard(grd13),event('ObserveLoadFenceAfterStore')],true),po('FENCEM5','Invariant preservation',[event('ObserveLoadFenceAfterStore'),event('ObserveLoadFenceAfterStore'),invariant(inv1)],true),po('FENCEM5','Invariant preservation',[event('ObserveLoadFenceAfterStore'),event('ObserveLoadFenceAfterStore'),invariant(inv2)],true),po('FENCEM5','Well-definedness of action',[action(act4)],true),po('FENCEM5','Well-definedness of Guard',[guard(grd11),event('ObserveLoadFence')],true),po('FENCEM5','Invariant preservation',[event('ObserveLoadFence'),event('ObserveLoadFence'),invariant(inv1)],true),po('FENCEM5','Invariant preservation',[event('ObserveLoadFence'),event('ObserveLoadFence'),invariant(inv2)],true),po('FENCEM5','Well-definedness of action',[action(act3)],true),po('FENCEM4','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po('FENCEM4','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po('FENCEM4','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po('FENCEM4','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4)],true),po('FENCEM4','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],true),po('FENCEM4','Invariant preservation',[event('IssueLoad'),event('IssueLoad'),invariant(inv5)],true),po('FENCEM4','Invariant preservation',[event('IssueStore'),event('IssueStore'),invariant(inv4)],true),po('FENCEM4','Invariant preservation',[event('IssueStore'),event('IssueStore'),invariant(inv5)],true),po('FENCEM4','Well-definedness of Guard',[guard(grd4),event('ObserveLoadAfterStore')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd5),event('ObserveLoadAfterStore')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd8),event('ObserveLoadAfterStore')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd9),event('ObserveLoadAfterStore')],true),po('FENCEM4','Invariant preservation',[event('ObserveLoad'),event('ObserveLoadAfterStore'),invariant(inv4)],true),po('FENCEM4','Invariant preservation',[event('ObserveLoad'),event('ObserveLoadAfterStore'),invariant(inv5)],true),po('FENCEM4','Well-definedness of action',[action(act3)],true),po('FENCEM4','Well-definedness of Guard',[guard(grd4),event('ObserveLoad')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd5),event('ObserveLoad')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd7),event('ObserveLoad')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd8),event('ObserveLoad')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd4),event('ObserveLoadFenceAfterStore')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd6),event('ObserveLoadFenceAfterStore')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd7),event('ObserveLoadFenceAfterStore')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd10),event('ObserveLoadFenceAfterStore')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd11),event('ObserveLoadFenceAfterStore')],true),po('FENCEM4','Invariant preservation',[event('ObserveLoad'),event('ObserveLoadFenceAfterStore'),invariant(inv4)],true),po('FENCEM4','Invariant preservation',[event('ObserveLoad'),event('ObserveLoadFenceAfterStore'),invariant(inv5)],true),po('FENCEM4','Well-definedness of action',[action(act3)],true),po('FENCEM4','Well-definedness of Guard',[guard(grd4),event('ObserveLoadFence')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd6),event('ObserveLoadFence')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd7),event('ObserveLoadFence')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd9),event('ObserveLoadFence')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd10),event('ObserveLoadFence')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd4),event('ObserveStore')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd5),event('ObserveStoreFence')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd6),event('ObserveStoreFence')],true),po('FENCEM4','Well-definedness of Guard',[guard(grd3),event('IssueFence')],true),po('FENCEM4','Invariant preservation',[event('IssueFence'),invariant(inv1)],true),po('FENCEM4','Invariant preservation',[event('IssueFence'),invariant(inv2)],true),po('FENCEM4','Invariant preservation',[event('IssueFence'),invariant(inv3)],true),po('FENCEM4','Well-definedness of action',[action(act2)],true),po('GM3','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po('GM3','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po('GM3','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po('GM3','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4)],true),po('GM3','Invariant preservation',[event('IssueLoad'),event('IssueLoad'),invariant(inv2)],true),po('GM3','Invariant preservation',[event('IssueLoad'),event('IssueLoad'),invariant(inv3)],true),po('GM3','Invariant preservation',[event('IssueStore'),event('IssueStore'),invariant(inv2)],true),po('GM3','Invariant preservation',[event('IssueStore'),event('IssueStore'),invariant(inv3)],true),po('GM3','Well-definedness of Guard',[guard(grd3),event('ObserveLoad')],true),po('GM3','Invariant preservation',[event('ObserveLoad'),event('ObserveLoad'),invariant(inv2)],true),po('GM3','Invariant preservation',[event('ObserveLoad'),event('ObserveLoad'),invariant(inv3)],true),po('GM3','Well-definedness of action',[action(act2)],true),po('GM3','Well-definedness of Guard',[guard(grd3),event('ObserveStore')],true),po('GM3','Invariant preservation',[event('ObserveStore'),event('ObserveStore'),invariant(inv1)],true),po('GM3','Invariant preservation',[event('ObserveStore'),event('ObserveStore'),invariant(inv2)],true),po('GM3','Invariant preservation',[event('ObserveStore'),event('ObserveStore'),invariant(inv3)],true),po('GM3','Invariant preservation',[event('ObserveStore'),event('ObserveStore'),invariant(inv4)],true),po('GM3','Well-definedness of action',[action(act2)],true),po('GM3','Well-definedness of action',[action(act3)],true),po('GM2','Guard strengthening (split)',[event('Issue'),guard(grd1),event('Issue'),event('IssueLoad')],true),po('GM2','Guard strengthening (split)',[event('Issue'),guard(grd2),event('Issue'),event('IssueLoad')],true),po('GM2','Action simulation',[event('Issue'),action(act1),event('IssueLoad')],true),po('GM2','Guard strengthening (split)',[event('Issue'),guard(grd1),event('Issue'),event('IssueStore')],true),po('GM2','Guard strengthening (split)',[event('Issue'),guard(grd2),event('Issue'),event('IssueStore')],true),po('GM2','Action simulation',[event('Issue'),action(act1),event('IssueStore')],true),po('GM2','Guard strengthening (split)',[event('Observe'),guard(grd1),event('Observe'),event('ObserveLoad')],true),po('GM2','Action simulation',[event('Observe'),action(act1),event('ObserveLoad')],true),po('GM2','Guard strengthening (split)',[event('Observe'),guard(grd1),event('Observe'),event('ObserveStore')],true),po('GM2','Action simulation',[event('Observe'),action(act1),event('ObserveStore')],true),po('GM1','Invariant establishment',[event('INITIALISATION'),invariant(inv1)],true),po('GM1','Invariant establishment',[event('INITIALISATION'),invariant(inv2)],true),po('GM1','Invariant preservation',[event('Issue'),invariant(inv1)],true),po('GM1','Invariant preservation',[event('Issue'),invariant(inv2)],true),po('GM1','Invariant preservation',[event('Observe'),invariant(inv2)],true)],_Error)).
2