1		package(load_event_b_project([event_b_model(none,s4_mch9_schedule,[sees(none,[s1_ctx0_blocks,s1_ctx1_blocks,s1_ctx2_signal,s1_ctx3_trains]),refines(none,s3_mch8_switch),variables(none,[identifier(none,'ENTRY_SIGNAL'),identifier(none,'EXIT_SIGNAL'),identifier(none,'IN_SWITCH'),identifier(none,'OCC'),identifier(none,'OUT_SWITCH'),identifier(none,'POS'),identifier(none,entry_signal_snsr),identifier(none,exit_signal_snsr),identifier(none,in_signal_act),identifier(none,in_switch),identifier(none,in_switch_act),identifier(none,in_switch_sig),identifier(none,occ_snsr),identifier(none,out_signal_act),identifier(none,out_switch),identifier(none,out_switch_act),identifier(none,out_switch_sig)]),invariant(none,[subset(rodinpos(s4_mch9_schedule,inv1,'_oK_Fwy6wEd-XL95EVwlwxw'),identifier(none,'OCC'),identifier(none,'BLOCK')),member(rodinpos(s4_mch9_schedule,inv1,'_Rx3RMC68Ed-0PKStM0XZhg'),identifier(none,'IN_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s4_mch9_schedule,inv2,'_Rx34QC68Ed-0PKStM0XZhg'),identifier(none,'OUT_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s4_mch9_schedule,inv1,'_XmqRsjB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,'ACCESS')),member(rodinpos(s4_mch9_schedule,inv2,'_XmqRszB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,'ACCESS')),disjunct(rodinpos(s4_mch9_schedule,inv3,'_Xmq4wDB6Ed-6kJpHxFX5oA'),not_equal(none,identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed)),not_member(none,identifier(none,'IN_SWITCH'),identifier(none,'OCC'))),disjunct(rodinpos(s4_mch9_schedule,inv4,'_Xmq4wTB6Ed-6kJpHxFX5oA'),not_equal(none,identifier(none,'EXIT_SIGNAL'),identifier(none,allowed)),not_member(none,identifier(none,ext_pnt),identifier(none,'OCC'))),member(rodinpos(s4_mch9_schedule,inv1,'_oecFITCQEd-6kJpHxFX5oA'),identifier(none,'POS'),partial_function(none,identifier(none,'TRAIN'),identifier(none,'BLOCK'))),equal(rodinpos(s4_mch9_schedule,inv2,'_oecsMTCQEd-6kJpHxFX5oA'),range(none,identifier(none,'POS')),identifier(none,'OCC')),forall(rodinpos(s4_mch9_schedule,inv3,'_oecsMjCQEd-6kJpHxFX5oA'),[identifier(none,t1),identifier(none,t2)],implication(none,conjunct(none,member(none,identifier(none,t1),domain(none,identifier(none,'POS'))),conjunct(none,member(none,identifier(none,t2),domain(none,identifier(none,'POS'))),equal(none,function(none,identifier(none,'POS'),[identifier(none,t1)]),function(none,identifier(none,'POS'),[identifier(none,t2)])))),equal(none,identifier(none,t1),identifier(none,t2)))),member(rodinpos(s4_mch9_schedule,inv1,'_bwbBEk7yEd-P0eLWrKaUUw'),identifier(none,in_switch_act),identifier(none,'PLATFORM')),member(rodinpos(s4_mch9_schedule,inv2,'_uoN3AVOTEd-qwcKa_9mK8w'),identifier(none,out_switch_act),identifier(none,'PLATFORM')),implication(rodinpos(s4_mch9_schedule,inv3,'_8YCswFOCEd-_lt3WaRv46A'),equal(none,identifier(none,in_switch_sig),boolean_true(none)),equal(none,identifier(none,'ENTRY_SIGNAL'),identifier(none,forbidden))),implication(rodinpos(s4_mch9_schedule,inv4,'_uoN3AlOTEd-qwcKa_9mK8w'),equal(none,identifier(none,out_switch_sig),boolean_true(none)),equal(none,identifier(none,'EXIT_SIGNAL'),identifier(none,forbidden))),member(rodinpos(s4_mch9_schedule,inv1,'_oXseslOUEd-qwcKa_9mK8w'),identifier(none,in_signal_act),bool_set(none)),member(rodinpos(s4_mch9_schedule,inv2,'_oXses1OUEd-qwcKa_9mK8w'),identifier(none,out_signal_act),bool_set(none)),disjunct(rodinpos(s4_mch9_schedule,inv5,'_9Z6K4FOtEd-qwcKa_9mK8w'),equal(none,identifier(none,in_signal_act),boolean_false(none)),not_member(none,identifier(none,'IN_SWITCH'),range(none,identifier(none,'POS')))),disjunct(rodinpos(s4_mch9_schedule,inv6,'_9Z6K4VOtEd-qwcKa_9mK8w'),equal(none,identifier(none,out_signal_act),boolean_false(none)),not_member(none,identifier(none,ext_pnt),range(none,identifier(none,'POS')))),disjunct(rodinpos(s4_mch9_schedule,inv7,'_9Z6K4lOtEd-qwcKa_9mK8w'),equal(none,identifier(none,in_signal_act),boolean_false(none)),equal(none,identifier(none,in_switch_sig),boolean_false(none))),disjunct(rodinpos(s4_mch9_schedule,inv8,'_9Z6K41OtEd-qwcKa_9mK8w'),equal(none,identifier(none,out_signal_act),boolean_false(none)),equal(none,identifier(none,out_switch_sig),boolean_false(none))),equal(rodinpos(s4_mch9_schedule,inv1,'_ofEk0VeAEd-YX5Y88L2F0U'),identifier(none,entry_signal_snsr),identifier(none,'ENTRY_SIGNAL')),equal(rodinpos(s4_mch9_schedule,inv2,'_ofEk0VeAEd-YX5Y88L2F0W'),identifier(none,exit_signal_snsr),identifier(none,'EXIT_SIGNAL')),equal(rodinpos(s4_mch9_schedule,inv1,'_ofEk0VeAEd-YX5Y88L2F0U'),identifier(none,occ_snsr),identifier(none,'OCC'))]),theorems(none,[member(rodinpos(s4_mch9_schedule,thm4,'_Yh0z0DEGEd-pyqeHaVRg2g'),identifier(none,'POS'),partial_injection(none,identifier(none,'TRAIN'),identifier(none,'BLOCK')))]),events(none,[event(rodinpos(s4_mch9_schedule,'INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(s4_mch9_schedule,act1,'_oLAT4C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[empty_set(none)]),becomes_such(rodinpos(s4_mch9_schedule,act2,'_Rx34QS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH'),identifier(none,in_switch)],conjunct(none,member(none,identifier(none,'IN_SWITCH\''),identifier(none,'PLATFORM')),equal(none,identifier(none,'IN_SWITCH\''),identifier(none,'in_switch\'')))),becomes_such(rodinpos(s4_mch9_schedule,act3,'_Rx34Qi68Ed-0PKStM0XZhg'),[identifier(none,'OUT_SWITCH'),identifier(none,out_switch)],conjunct(none,member(none,identifier(none,'OUT_SWITCH\''),identifier(none,'PLATFORM')),equal(none,identifier(none,'OUT_SWITCH\''),identifier(none,'out_switch\'')))),assign(rodinpos(s4_mch9_schedule,act4,'_Xmrf0DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s4_mch9_schedule,act5,'_Xmrf0TB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s4_mch9_schedule,act6,'_oedTQDCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[empty_set(none)]),becomes_element_of(rodinpos(s4_mch9_schedule,act7,'_Rs-R4FYTEd-rnu8Rug219Q'),[identifier(none,in_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s4_mch9_schedule,act8,internal1),[identifier(none,in_switch_sig)],[boolean_false(none)]),becomes_element_of(rodinpos(s4_mch9_schedule,act9,'_gcPBME74Ed-P0eLWrKaUUw'),[identifier(none,out_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s4_mch9_schedule,act10,'_gcPBMU74Ed-P0eLWrKaUUw'),[identifier(none,out_switch_sig)],[boolean_false(none)]),assign(rodinpos(s4_mch9_schedule,act11,internal2),[identifier(none,in_signal_act)],[boolean_false(none)]),assign(rodinpos(s4_mch9_schedule,act12,'_uoPFIFOTEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_false(none)]),assign(rodinpos(s4_mch9_schedule,act13,internal3),[identifier(none,entry_signal_snsr)],[identifier(none,forbidden)]),assign(rodinpos(s4_mch9_schedule,act14,internal4),[identifier(none,exit_signal_snsr)],[identifier(none,forbidden)]),assign(rodinpos(s4_mch9_schedule,act15,internal5),[identifier(none,occ_snsr)],[empty_set(none)])],[]),event(rodinpos(s4_mch9_schedule,'ARRIVE','_oLAT4i6wEd-XL95EVwlwxw'),'ARRIVE',anticipated(none),['ARRIVE'],[identifier(rodinpos(s4_mch9_schedule,[],'_oedTQjCQEd-6kJpHxFX5oA'),t)],[not_member(rodinpos(s4_mch9_schedule,grd1,'_oLAT4y6wEd-XL95EVwlwxw'),identifier(none,ent_pnt),identifier(none,'OCC')),not_member(rodinpos(s4_mch9_schedule,grd2,'_oed6UDCQEd-6kJpHxFX5oA'),identifier(none,t),domain(none,identifier(none,'POS')))],[],[assign(rodinpos(s4_mch9_schedule,act1,'_oLA68C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s4_mch9_schedule,act3,'_oed6UTCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,ent_pnt)])]))]),assign(rodinpos(s4_mch9_schedule,act4,'('),[identifier(none,occ_snsr)],[union(none,identifier(none,occ_snsr),set_extension(none,[identifier(none,ent_pnt)]))])],[]),event(rodinpos(s4_mch9_schedule,'LEAVE','_oLA68i6wEd-XL95EVwlwxw'),'LEAVE',anticipated(none),['LEAVE'],[identifier(rodinpos(s4_mch9_schedule,[],'_oed6UzCQEd-6kJpHxFX5oA'),t)],[member(rodinpos(s4_mch9_schedule,grd1,'_oeehYTCQEd-6kJpHxFX5oB'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s4_mch9_schedule,grd2,'_oeehYDCQEd-6kJpHxFX5oA'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,ext_pnt))],[],[assign(rodinpos(s4_mch9_schedule,act1,'_oLA69C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)]))]),assign(rodinpos(s4_mch9_schedule,act2,'_oeehYTCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[domain_subtraction(none,set_extension(none,[identifier(none,t)]),identifier(none,'POS'))]),assign(rodinpos(s4_mch9_schedule,act4,'('),[identifier(none,occ_snsr)],[set_subtraction(none,identifier(none,occ_snsr),set_extension(none,[identifier(none,ext_pnt)]))])],[]),event(rodinpos(s4_mch9_schedule,'MOVE_IN_PLATFORM','_oLBiAC6wEd-XL95EVwlwxw'),'MOVE_IN_PLATFORM',anticipated(none),['MOVE_IN_PLATFORM'],[identifier(rodinpos(s4_mch9_schedule,[],'_Yh2pATEGEd-pyqeHaVRg2g'),t)],[equal(rodinpos(s4_mch9_schedule,grd1,'_XmsG4jB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed)),member(rodinpos(s4_mch9_schedule,grd2,'_Yh2pAjEGEd-pyqeHaVRg2g'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s4_mch9_schedule,grd3,'_Yh3QEDEGEd-pyqeHaVRg2g'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,ent_pnt)),equal(rodinpos(s4_mch9_schedule,grd4,'_9Z7ZAlOtEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_false(none))],[],[assign(rodinpos(s4_mch9_schedule,act1,'_XmsG4zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,'IN_SWITCH')])),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s4_mch9_schedule,act2,'_XmsG5DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s4_mch9_schedule,act3,'_Yh3QETEGEd-pyqeHaVRg2g'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,'IN_SWITCH')])]))]),assign(rodinpos(s4_mch9_schedule,act4,'('),[identifier(none,entry_signal_snsr)],[identifier(none,forbidden)]),assign(rodinpos(s4_mch9_schedule,act5,'('),[identifier(none,occ_snsr)],[set_subtraction(none,union(none,identifier(none,occ_snsr),set_extension(none,[identifier(none,'IN_SWITCH')])),set_extension(none,[identifier(none,ent_pnt)]))])],[]),event(rodinpos(s4_mch9_schedule,'MOVE_OUT_PLATFORM','_oLBiBC6wEd-XL95EVwlwxw'),'MOVE_OUT_PLATFORM',anticipated(none),['MOVE_OUT_PLATFORM'],[identifier(rodinpos(s4_mch9_schedule,[],'_Yh3QEzEGEd-pyqeHaVRg2g'),t)],[equal(rodinpos(s4_mch9_schedule,grd1,'_Xmst8jB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,allowed)),member(rodinpos(s4_mch9_schedule,grd2,'_Yh3QFDEGEd-pyqeHaVRg2g'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s4_mch9_schedule,grd3,'_Yh3QFTEGEd-pyqeHaVRg2g'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,'OUT_SWITCH')),equal(rodinpos(s4_mch9_schedule,grd4,'_NQysYVYREd-rnu8Rug219Q'),identifier(none,out_signal_act),boolean_false(none))],[],[assign(rodinpos(s4_mch9_schedule,act1,'_Xmst8zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)])),set_extension(none,[identifier(none,'OUT_SWITCH')]))]),assign(rodinpos(s4_mch9_schedule,act2,'_Xmst9DB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s4_mch9_schedule,act3,'_Yh33IDEGEd-pyqeHaVRg2g'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,ext_pnt)])]))]),assign(rodinpos(s4_mch9_schedule,act4,'('),[identifier(none,exit_signal_snsr)],[identifier(none,forbidden)]),assign(rodinpos(s4_mch9_schedule,act5,'('),[identifier(none,occ_snsr)],[set_subtraction(none,union(none,identifier(none,occ_snsr),set_extension(none,[identifier(none,ext_pnt)])),set_extension(none,[identifier(none,'OUT_SWITCH')]))])],[]),event(rodinpos(s4_mch9_schedule,'TURN_IN_SWITCH','_bwercU7yEd-P0eLWrKaUUw'),'TURN_IN_SWITCH',anticipated(none),['TURN_IN_SWITCH'],[],[equal(rodinpos(s4_mch9_schedule,grd1,'_XmtVATB6Ed-6kJpHxFX5oA'),identifier(none,in_switch_sig),boolean_true(none))],[],[assign(rodinpos(s4_mch9_schedule,act1,'_Rx5GYS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],[identifier(none,in_switch_act)]),assign(rodinpos(s4_mch9_schedule,act2,'_8YJacFOCEd-_lt3WaRv46A'),[identifier(none,in_switch_sig)],[boolean_false(none)])],[]),event(rodinpos(s4_mch9_schedule,'TURN_OUT_SWITCH','_5TLaUFOSEd-qwcKa_9mK8w'),'TURN_OUT_SWITCH',anticipated(none),['TURN_OUT_SWITCH'],[],[equal(rodinpos(s4_mch9_schedule,grd1,'_uoSvglOTEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_true(none))],[],[assign(rodinpos(s4_mch9_schedule,act1,'_uoSvg1OTEd-qwcKa_9mK8w'),[identifier(none,'OUT_SWITCH')],[identifier(none,out_switch_act)]),assign(rodinpos(s4_mch9_schedule,act2,'_uoSvhFOTEd-qwcKa_9mK8w'),[identifier(none,out_switch_sig)],[boolean_false(none)])],[]),event(rodinpos(s4_mch9_schedule,'ALLOW_ENTRANCE','_oXviA1OUEd-qwcKa_9mK8w'),'ALLOW_ENTRANCE',anticipated(none),['ALLOW_ENTRANCE'],[],[equal(rodinpos(s4_mch9_schedule,grd1,'_oXwJEVOUEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_true(none))],[],[assign(rodinpos(s4_mch9_schedule,act1,'_Xmt8ETB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,allowed)]),assign(rodinpos(s4_mch9_schedule,act2,'_oXwJElOUEd-qwcKa_9mK8w'),[identifier(none,in_signal_act)],[boolean_false(none)]),assign(rodinpos(s4_mch9_schedule,act3,'('),[identifier(none,entry_signal_snsr)],[identifier(none,allowed)])],[]),event(rodinpos(s4_mch9_schedule,'ALLOW_DEPARTURE','_oXwJE1OUEd-qwcKa_9mK8w'),'ALLOW_DEPARTURE',anticipated(none),['ALLOW_DEPARTURE'],[],[equal(rodinpos(s4_mch9_schedule,grd1,'_oXwJFVOUEd-qwcKa_9mK8w'),identifier(none,out_signal_act),boolean_true(none))],[],[assign(rodinpos(s4_mch9_schedule,act1,'_Xmt8FDB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,allowed)]),assign(rodinpos(s4_mch9_schedule,act2,'_oXwJFlOUEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_false(none)]),assign(rodinpos(s4_mch9_schedule,act3,'('),[identifier(none,exit_signal_snsr)],[identifier(none,allowed)])],[]),event(rodinpos(s4_mch9_schedule,trigger_in_switch,'_bweEYk7yEd-P0eLWrKaUUw'),trigger_in_switch,anticipated(none),[trigger_in_switch],[identifier(rodinpos(s4_mch9_schedule,[],'_ofKrcFeAEd-YX5Y88L2F0T'),p)],[equal(rodinpos(s4_mch9_schedule,grd1,'_gcSEgE74Ed-P0eLWrKaUUw'),identifier(none,entry_signal_snsr),identifier(none,forbidden)),equal(rodinpos(s4_mch9_schedule,grd2,'_gcSEgk74Ed-P0eLWrKaUUw'),identifier(none,in_switch_sig),boolean_false(none)),equal(rodinpos(s4_mch9_schedule,grd3,'_ofKrcFeAEd-YX5Y88L2F0R'),identifier(none,in_signal_act),boolean_false(none)),member(rodinpos(s4_mch9_schedule,grd4,'_ofKrcFeAEd-YX5Y88L2F0S'),identifier(none,p),identifier(none,'PLATFORM')),member(rodinpos(s4_mch9_schedule,grd5,'_ofKrcFeAEd-YX5Y88L2F0U'),identifier(none,ent_pnt),identifier(none,occ_snsr)),not_member(rodinpos(s4_mch9_schedule,grd6,'_ofKrcFeAEd-YX5Y88L2F0Z'),identifier(none,p),identifier(none,occ_snsr)),not_equal(rodinpos(s4_mch9_schedule,grd7,'_ofKrcFeAEd-YX5Y88L2F0['),identifier(none,p),identifier(none,in_switch))],[],[assign(rodinpos(s4_mch9_schedule,act1,'_bweEY07yEd-P0eLWrKaUUw'),[identifier(none,in_switch_act)],[identifier(none,p)]),assign(rodinpos(s4_mch9_schedule,act2,'_bwercE7yEd-P0eLWrKaUUw'),[identifier(none,in_switch_sig)],[boolean_true(none)]),assign(rodinpos(s4_mch9_schedule,act3,'_ofKrcFeAEd-YX5Y88L2F0U'),[identifier(none,in_switch)],[identifier(none,p)])],[]),event(rodinpos(s4_mch9_schedule,trigger_out_switch,'_5TMBZFOSEd-qwcKa_9mK8w'),trigger_out_switch,anticipated(none),[trigger_out_switch],[identifier(rodinpos(s4_mch9_schedule,[],'_uoSIcFOTEd-qwcKa_9mK8y'),p)],[equal(rodinpos(s4_mch9_schedule,grd1,'_uoRhYVOTEd-qwcKa_9mK8w'),identifier(none,exit_signal_snsr),identifier(none,forbidden)),equal(rodinpos(s4_mch9_schedule,grd2,'_uoRhYlOTEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_false(none)),equal(rodinpos(s4_mch9_schedule,grd3,'_ofL5kFeAEd-YX5Y88L2F0R'),identifier(none,out_signal_act),boolean_false(none)),member(rodinpos(s4_mch9_schedule,grd4,'_uoSIcFOTEd-qwcKa_9mK8x'),identifier(none,p),identifier(none,'PLATFORM')),not_member(rodinpos(s4_mch9_schedule,grd5,'_uoSIcFOTEd-qwcKa_9mK8z'),identifier(none,ext_pnt),identifier(none,occ_snsr)),member(rodinpos(s4_mch9_schedule,grd6,'_uoSIcFOTEd-qwcKa_9mK8|'),identifier(none,p),identifier(none,occ_snsr)),not_equal(rodinpos(s4_mch9_schedule,grd7,'_uoSIcFOTEd-qwcKa_9mK8~'),identifier(none,p),identifier(none,out_switch))],[],[assign(rodinpos(s4_mch9_schedule,act1,'_uoRhY1OTEd-qwcKa_9mK8w'),[identifier(none,out_switch_act)],[identifier(none,p)]),assign(rodinpos(s4_mch9_schedule,act2,'_uoSIcFOTEd-qwcKa_9mK8w'),[identifier(none,out_switch_sig)],[boolean_true(none)]),assign(rodinpos(s4_mch9_schedule,act3,'_uoSIcFOTEd-qwcKa_9mK8z'),[identifier(none,out_switch)],[identifier(none,p)])],[]),event(rodinpos(s4_mch9_schedule,allow_entrance,'_XmtVBDB6Ed-6kJpHxFX5oA'),allow_entrance,anticipated(none),[allow_entrance],[],[equal(rodinpos(s4_mch9_schedule,grd1,'_oXu68VOUEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_false(none)),not_member(rodinpos(s4_mch9_schedule,grd2,'_9Z9OMFOtEd-qwcKa_9mK8w'),identifier(none,in_switch),identifier(none,occ_snsr)),equal(rodinpos(s4_mch9_schedule,grd3,'__cteMFOvEd-qwcKa_9mK8w'),identifier(none,in_switch_sig),boolean_false(none)),member(rodinpos(s4_mch9_schedule,grd4,'('),identifier(none,ent_pnt),identifier(none,occ_snsr)),equal(rodinpos(s4_mch9_schedule,grd5,')'),identifier(none,entry_signal_snsr),identifier(none,forbidden))],[],[assign(rodinpos(s4_mch9_schedule,act1,'_oXu681OUEd-qwcKa_9mK8w'),[identifier(none,in_signal_act)],[boolean_true(none)])],[]),event(rodinpos(s4_mch9_schedule,allow_departure,'_Xmt8EjB6Ed-6kJpHxFX5oA'),allow_departure,anticipated(none),[allow_departure],[],[equal(rodinpos(s4_mch9_schedule,grd1,'_oXviAFOUEd-qwcKa_9mK8w'),identifier(none,out_signal_act),boolean_false(none)),not_member(rodinpos(s4_mch9_schedule,grd2,'_9Z91QFOtEd-qwcKa_9mK8w'),identifier(none,ext_pnt),identifier(none,occ_snsr)),equal(rodinpos(s4_mch9_schedule,grd3,'__cuFQFOvEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_false(none)),member(rodinpos(s4_mch9_schedule,grd4,'('),identifier(none,out_switch),identifier(none,occ_snsr)),equal(rodinpos(s4_mch9_schedule,grd5,')'),identifier(none,exit_signal_snsr),identifier(none,forbidden))],[],[assign(rodinpos(s4_mch9_schedule,act1,'_oXviAlOUEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_true(none)])],[])])]),event_b_model(none,s3_mch8_switch,[sees(none,[s1_ctx0_blocks,s1_ctx1_blocks,s1_ctx2_signal,s1_ctx3_trains]),refines(none,s3_mch7_track_sensor),variables(none,[identifier(none,'ENTRY_SIGNAL'),identifier(none,'EXIT_SIGNAL'),identifier(none,'IN_SWITCH'),identifier(none,'OCC'),identifier(none,'OUT_SWITCH'),identifier(none,'POS'),identifier(none,entry_signal_snsr),identifier(none,exit_signal_snsr),identifier(none,in_signal_act),identifier(none,in_switch),identifier(none,in_switch_act),identifier(none,in_switch_sig),identifier(none,occ_snsr),identifier(none,out_signal_act),identifier(none,out_switch),identifier(none,out_switch_act),identifier(none,out_switch_sig)]),invariant(none,[subset(rodinpos(s3_mch8_switch,inv1,'_oK_Fwy6wEd-XL95EVwlwxw'),identifier(none,'OCC'),identifier(none,'BLOCK')),member(rodinpos(s3_mch8_switch,inv1,'_Rx3RMC68Ed-0PKStM0XZhg'),identifier(none,'IN_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s3_mch8_switch,inv2,'_Rx34QC68Ed-0PKStM0XZhg'),identifier(none,'OUT_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s3_mch8_switch,inv1,'_XmqRsjB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,'ACCESS')),member(rodinpos(s3_mch8_switch,inv2,'_XmqRszB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,'ACCESS')),disjunct(rodinpos(s3_mch8_switch,inv3,'_Xmq4wDB6Ed-6kJpHxFX5oA'),not_equal(none,identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed)),not_member(none,identifier(none,'IN_SWITCH'),identifier(none,'OCC'))),disjunct(rodinpos(s3_mch8_switch,inv4,'_Xmq4wTB6Ed-6kJpHxFX5oA'),not_equal(none,identifier(none,'EXIT_SIGNAL'),identifier(none,allowed)),not_member(none,identifier(none,ext_pnt),identifier(none,'OCC'))),member(rodinpos(s3_mch8_switch,inv1,'_oecFITCQEd-6kJpHxFX5oA'),identifier(none,'POS'),partial_function(none,identifier(none,'TRAIN'),identifier(none,'BLOCK'))),equal(rodinpos(s3_mch8_switch,inv2,'_oecsMTCQEd-6kJpHxFX5oA'),range(none,identifier(none,'POS')),identifier(none,'OCC')),forall(rodinpos(s3_mch8_switch,inv3,'_oecsMjCQEd-6kJpHxFX5oA'),[identifier(none,t1),identifier(none,t2)],implication(none,conjunct(none,member(none,identifier(none,t1),domain(none,identifier(none,'POS'))),conjunct(none,member(none,identifier(none,t2),domain(none,identifier(none,'POS'))),equal(none,function(none,identifier(none,'POS'),[identifier(none,t1)]),function(none,identifier(none,'POS'),[identifier(none,t2)])))),equal(none,identifier(none,t1),identifier(none,t2)))),member(rodinpos(s3_mch8_switch,inv1,'_bwbBEk7yEd-P0eLWrKaUUw'),identifier(none,in_switch_act),identifier(none,'PLATFORM')),member(rodinpos(s3_mch8_switch,inv2,'_uoN3AVOTEd-qwcKa_9mK8w'),identifier(none,out_switch_act),identifier(none,'PLATFORM')),implication(rodinpos(s3_mch8_switch,inv3,'_8YCswFOCEd-_lt3WaRv46A'),equal(none,identifier(none,in_switch_sig),boolean_true(none)),equal(none,identifier(none,'ENTRY_SIGNAL'),identifier(none,forbidden))),implication(rodinpos(s3_mch8_switch,inv4,'_uoN3AlOTEd-qwcKa_9mK8w'),equal(none,identifier(none,out_switch_sig),boolean_true(none)),equal(none,identifier(none,'EXIT_SIGNAL'),identifier(none,forbidden))),member(rodinpos(s3_mch8_switch,inv1,'_oXseslOUEd-qwcKa_9mK8w'),identifier(none,in_signal_act),bool_set(none)),member(rodinpos(s3_mch8_switch,inv2,'_oXses1OUEd-qwcKa_9mK8w'),identifier(none,out_signal_act),bool_set(none)),disjunct(rodinpos(s3_mch8_switch,inv5,'_9Z6K4FOtEd-qwcKa_9mK8w'),equal(none,identifier(none,in_signal_act),boolean_false(none)),not_member(none,identifier(none,'IN_SWITCH'),range(none,identifier(none,'POS')))),disjunct(rodinpos(s3_mch8_switch,inv6,'_9Z6K4VOtEd-qwcKa_9mK8w'),equal(none,identifier(none,out_signal_act),boolean_false(none)),not_member(none,identifier(none,ext_pnt),range(none,identifier(none,'POS')))),disjunct(rodinpos(s3_mch8_switch,inv7,'_9Z6K4lOtEd-qwcKa_9mK8w'),equal(none,identifier(none,in_signal_act),boolean_false(none)),equal(none,identifier(none,in_switch_sig),boolean_false(none))),disjunct(rodinpos(s3_mch8_switch,inv8,'_9Z6K41OtEd-qwcKa_9mK8w'),equal(none,identifier(none,out_signal_act),boolean_false(none)),equal(none,identifier(none,out_switch_sig),boolean_false(none))),equal(rodinpos(s3_mch8_switch,inv1,'_ofEk0VeAEd-YX5Y88L2F0U'),identifier(none,entry_signal_snsr),identifier(none,'ENTRY_SIGNAL')),equal(rodinpos(s3_mch8_switch,inv2,'_ofEk0VeAEd-YX5Y88L2F0W'),identifier(none,exit_signal_snsr),identifier(none,'EXIT_SIGNAL')),implication(rodinpos(s3_mch8_switch,inv1,'_ofEk0VeAEd-YX5Y88L2F0U'),equal(none,identifier(none,in_switch_sig),boolean_false(none)),equal(none,identifier(none,in_switch),identifier(none,'IN_SWITCH'))),implication(rodinpos(s3_mch8_switch,inv2,'_ofEk0VeAEd-YX5Y88L2F0W'),equal(none,identifier(none,out_switch_sig),boolean_false(none)),equal(none,identifier(none,out_switch),identifier(none,'OUT_SWITCH'))),implication(rodinpos(s3_mch8_switch,inv3,'_ofEk0VeAEd-YX5Y88L2F0X'),equal(none,identifier(none,in_switch_sig),boolean_true(none)),equal(none,identifier(none,in_switch),identifier(none,in_switch_act))),implication(rodinpos(s3_mch8_switch,inv4,'_ofEk0VeAEd-YX5Y88L2F0Y'),equal(none,identifier(none,out_switch_sig),boolean_true(none)),equal(none,identifier(none,out_switch),identifier(none,out_switch_act)))]),theorems(none,[member(rodinpos(s3_mch8_switch,thm4,'_Yh0z0DEGEd-pyqeHaVRg2g'),identifier(none,'POS'),partial_injection(none,identifier(none,'TRAIN'),identifier(none,'BLOCK')))]),events(none,[event(rodinpos(s3_mch8_switch,'INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(s3_mch8_switch,act1,'_oLAT4C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[empty_set(none)]),becomes_such(rodinpos(s3_mch8_switch,act2,'_Rx34QS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH'),identifier(none,in_switch)],conjunct(none,member(none,identifier(none,'IN_SWITCH\''),identifier(none,'PLATFORM')),equal(none,identifier(none,'IN_SWITCH\''),identifier(none,'in_switch\'')))),becomes_such(rodinpos(s3_mch8_switch,act3,'_Rx34Qi68Ed-0PKStM0XZhg'),[identifier(none,'OUT_SWITCH'),identifier(none,out_switch)],conjunct(none,member(none,identifier(none,'OUT_SWITCH\''),identifier(none,'PLATFORM')),equal(none,identifier(none,'OUT_SWITCH\''),identifier(none,'out_switch\'')))),assign(rodinpos(s3_mch8_switch,act4,'_Xmrf0DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s3_mch8_switch,act5,'_Xmrf0TB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s3_mch8_switch,act6,'_oedTQDCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[empty_set(none)]),becomes_element_of(rodinpos(s3_mch8_switch,act7,'_Rs-R4FYTEd-rnu8Rug219Q'),[identifier(none,in_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s3_mch8_switch,act8,internal1),[identifier(none,in_switch_sig)],[boolean_false(none)]),becomes_element_of(rodinpos(s3_mch8_switch,act9,'_gcPBME74Ed-P0eLWrKaUUw'),[identifier(none,out_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s3_mch8_switch,act10,'_gcPBMU74Ed-P0eLWrKaUUw'),[identifier(none,out_switch_sig)],[boolean_false(none)]),assign(rodinpos(s3_mch8_switch,act11,internal2),[identifier(none,in_signal_act)],[boolean_false(none)]),assign(rodinpos(s3_mch8_switch,act12,'_uoPFIFOTEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_false(none)]),assign(rodinpos(s3_mch8_switch,act13,internal3),[identifier(none,entry_signal_snsr)],[identifier(none,forbidden)]),assign(rodinpos(s3_mch8_switch,act14,internal4),[identifier(none,exit_signal_snsr)],[identifier(none,forbidden)]),assign(rodinpos(s3_mch8_switch,act15,internal5),[identifier(none,occ_snsr)],[empty_set(none)])],[]),event(rodinpos(s3_mch8_switch,'ARRIVE','_oLAT4i6wEd-XL95EVwlwxw'),'ARRIVE',anticipated(none),['ARRIVE'],[identifier(rodinpos(s3_mch8_switch,[],'_oedTQjCQEd-6kJpHxFX5oA'),t)],[not_member(rodinpos(s3_mch8_switch,grd1,'_oLAT4y6wEd-XL95EVwlwxw'),identifier(none,ent_pnt),identifier(none,'OCC')),not_member(rodinpos(s3_mch8_switch,grd2,'_oed6UDCQEd-6kJpHxFX5oA'),identifier(none,t),domain(none,identifier(none,'POS')))],[],[assign(rodinpos(s3_mch8_switch,act1,'_oLA68C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s3_mch8_switch,act3,'_oed6UTCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,ent_pnt)])]))]),assign(rodinpos(s3_mch8_switch,act4,'('),[identifier(none,occ_snsr)],[union(none,identifier(none,occ_snsr),set_extension(none,[identifier(none,ent_pnt)]))])],[]),event(rodinpos(s3_mch8_switch,'LEAVE','_oLA68i6wEd-XL95EVwlwxw'),'LEAVE',anticipated(none),['LEAVE'],[identifier(rodinpos(s3_mch8_switch,[],'_oed6UzCQEd-6kJpHxFX5oA'),t)],[member(rodinpos(s3_mch8_switch,grd1,'_oeehYTCQEd-6kJpHxFX5oB'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s3_mch8_switch,grd2,'_oeehYDCQEd-6kJpHxFX5oA'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,ext_pnt))],[],[assign(rodinpos(s3_mch8_switch,act1,'_oLA69C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)]))]),assign(rodinpos(s3_mch8_switch,act2,'_oeehYTCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[domain_subtraction(none,set_extension(none,[identifier(none,t)]),identifier(none,'POS'))]),assign(rodinpos(s3_mch8_switch,act4,'('),[identifier(none,occ_snsr)],[set_subtraction(none,identifier(none,occ_snsr),set_extension(none,[identifier(none,ext_pnt)]))])],[]),event(rodinpos(s3_mch8_switch,'MOVE_IN_PLATFORM','_oLBiAC6wEd-XL95EVwlwxw'),'MOVE_IN_PLATFORM',anticipated(none),['MOVE_IN_PLATFORM'],[identifier(rodinpos(s3_mch8_switch,[],'_Yh2pATEGEd-pyqeHaVRg2g'),t)],[equal(rodinpos(s3_mch8_switch,grd1,'_XmsG4jB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed)),member(rodinpos(s3_mch8_switch,grd2,'_Yh2pAjEGEd-pyqeHaVRg2g'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s3_mch8_switch,grd3,'_Yh3QEDEGEd-pyqeHaVRg2g'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,ent_pnt)),equal(rodinpos(s3_mch8_switch,grd4,'_9Z7ZAlOtEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_false(none))],[],[assign(rodinpos(s3_mch8_switch,act1,'_XmsG4zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,'IN_SWITCH')])),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s3_mch8_switch,act2,'_XmsG5DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s3_mch8_switch,act3,'_Yh3QETEGEd-pyqeHaVRg2g'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,'IN_SWITCH')])]))]),assign(rodinpos(s3_mch8_switch,act4,'('),[identifier(none,entry_signal_snsr)],[identifier(none,forbidden)]),assign(rodinpos(s3_mch8_switch,act5,'('),[identifier(none,occ_snsr)],[set_subtraction(none,union(none,identifier(none,occ_snsr),set_extension(none,[identifier(none,'IN_SWITCH')])),set_extension(none,[identifier(none,ent_pnt)]))])],[]),event(rodinpos(s3_mch8_switch,'MOVE_OUT_PLATFORM','_oLBiBC6wEd-XL95EVwlwxw'),'MOVE_OUT_PLATFORM',anticipated(none),['MOVE_OUT_PLATFORM'],[identifier(rodinpos(s3_mch8_switch,[],'_Yh3QEzEGEd-pyqeHaVRg2g'),t)],[equal(rodinpos(s3_mch8_switch,grd1,'_Xmst8jB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,allowed)),member(rodinpos(s3_mch8_switch,grd2,'_Yh3QFDEGEd-pyqeHaVRg2g'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s3_mch8_switch,grd3,'_Yh3QFTEGEd-pyqeHaVRg2g'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,'OUT_SWITCH')),equal(rodinpos(s3_mch8_switch,grd4,'_NQysYVYREd-rnu8Rug219Q'),identifier(none,out_signal_act),boolean_false(none))],[],[assign(rodinpos(s3_mch8_switch,act1,'_Xmst8zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)])),set_extension(none,[identifier(none,'OUT_SWITCH')]))]),assign(rodinpos(s3_mch8_switch,act2,'_Xmst9DB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s3_mch8_switch,act3,'_Yh33IDEGEd-pyqeHaVRg2g'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,ext_pnt)])]))]),assign(rodinpos(s3_mch8_switch,act4,'('),[identifier(none,exit_signal_snsr)],[identifier(none,forbidden)]),assign(rodinpos(s3_mch8_switch,act5,'('),[identifier(none,occ_snsr)],[set_subtraction(none,union(none,identifier(none,occ_snsr),set_extension(none,[identifier(none,ext_pnt)])),set_extension(none,[identifier(none,'OUT_SWITCH')]))])],[]),event(rodinpos(s3_mch8_switch,'TURN_IN_SWITCH','_bwercU7yEd-P0eLWrKaUUw'),'TURN_IN_SWITCH',anticipated(none),['TURN_IN_SWITCH'],[],[equal(rodinpos(s3_mch8_switch,grd1,'_XmtVATB6Ed-6kJpHxFX5oA'),identifier(none,in_switch_sig),boolean_true(none))],[],[assign(rodinpos(s3_mch8_switch,act1,'_Rx5GYS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],[identifier(none,in_switch_act)]),assign(rodinpos(s3_mch8_switch,act2,'_8YJacFOCEd-_lt3WaRv46A'),[identifier(none,in_switch_sig)],[boolean_false(none)])],[]),event(rodinpos(s3_mch8_switch,'TURN_OUT_SWITCH','_5TLaUFOSEd-qwcKa_9mK8w'),'TURN_OUT_SWITCH',anticipated(none),['TURN_OUT_SWITCH'],[],[equal(rodinpos(s3_mch8_switch,grd1,'_uoSvglOTEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_true(none))],[],[assign(rodinpos(s3_mch8_switch,act1,'_uoSvg1OTEd-qwcKa_9mK8w'),[identifier(none,'OUT_SWITCH')],[identifier(none,out_switch_act)]),assign(rodinpos(s3_mch8_switch,act2,'_uoSvhFOTEd-qwcKa_9mK8w'),[identifier(none,out_switch_sig)],[boolean_false(none)])],[]),event(rodinpos(s3_mch8_switch,'ALLOW_ENTRANCE','_oXviA1OUEd-qwcKa_9mK8w'),'ALLOW_ENTRANCE',anticipated(none),['ALLOW_ENTRANCE'],[],[equal(rodinpos(s3_mch8_switch,grd1,'_oXwJEVOUEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_true(none))],[],[assign(rodinpos(s3_mch8_switch,act1,'_Xmt8ETB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,allowed)]),assign(rodinpos(s3_mch8_switch,act2,'_oXwJElOUEd-qwcKa_9mK8w'),[identifier(none,in_signal_act)],[boolean_false(none)]),assign(rodinpos(s3_mch8_switch,act3,'('),[identifier(none,entry_signal_snsr)],[identifier(none,allowed)])],[]),event(rodinpos(s3_mch8_switch,'ALLOW_DEPARTURE','_oXwJE1OUEd-qwcKa_9mK8w'),'ALLOW_DEPARTURE',anticipated(none),['ALLOW_DEPARTURE'],[],[equal(rodinpos(s3_mch8_switch,grd1,'_oXwJFVOUEd-qwcKa_9mK8w'),identifier(none,out_signal_act),boolean_true(none))],[],[assign(rodinpos(s3_mch8_switch,act1,'_Xmt8FDB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,allowed)]),assign(rodinpos(s3_mch8_switch,act2,'_oXwJFlOUEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_false(none)]),assign(rodinpos(s3_mch8_switch,act3,'('),[identifier(none,exit_signal_snsr)],[identifier(none,allowed)])],[]),event(rodinpos(s3_mch8_switch,trigger_in_switch,'_bweEYk7yEd-P0eLWrKaUUw'),trigger_in_switch,anticipated(none),[trigger_in_switch],[identifier(rodinpos(s3_mch8_switch,[],'_ofKrcFeAEd-YX5Y88L2F0T'),p)],[equal(rodinpos(s3_mch8_switch,grd1,'_gcSEgE74Ed-P0eLWrKaUUw'),identifier(none,entry_signal_snsr),identifier(none,forbidden)),equal(rodinpos(s3_mch8_switch,grd2,'_gcSEgk74Ed-P0eLWrKaUUw'),identifier(none,in_switch_sig),boolean_false(none)),equal(rodinpos(s3_mch8_switch,grd3,'_ofKrcFeAEd-YX5Y88L2F0R'),identifier(none,in_signal_act),boolean_false(none)),member(rodinpos(s3_mch8_switch,grd4,'_ofKrcFeAEd-YX5Y88L2F0S'),identifier(none,p),identifier(none,'PLATFORM'))],[],[assign(rodinpos(s3_mch8_switch,act1,'_bweEY07yEd-P0eLWrKaUUw'),[identifier(none,in_switch_act)],[identifier(none,p)]),assign(rodinpos(s3_mch8_switch,act2,'_bwercE7yEd-P0eLWrKaUUw'),[identifier(none,in_switch_sig)],[boolean_true(none)]),assign(rodinpos(s3_mch8_switch,act3,'_ofKrcFeAEd-YX5Y88L2F0U'),[identifier(none,in_switch)],[identifier(none,p)])],[]),event(rodinpos(s3_mch8_switch,trigger_out_switch,'_5TMBZFOSEd-qwcKa_9mK8w'),trigger_out_switch,anticipated(none),[trigger_out_switch],[identifier(rodinpos(s3_mch8_switch,[],'_uoSIcFOTEd-qwcKa_9mK8y'),p)],[equal(rodinpos(s3_mch8_switch,grd1,'_uoRhYVOTEd-qwcKa_9mK8w'),identifier(none,exit_signal_snsr),identifier(none,forbidden)),equal(rodinpos(s3_mch8_switch,grd2,'_uoRhYlOTEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_false(none)),equal(rodinpos(s3_mch8_switch,grd3,'_ofL5kFeAEd-YX5Y88L2F0R'),identifier(none,out_signal_act),boolean_false(none)),member(rodinpos(s3_mch8_switch,grd4,'_uoSIcFOTEd-qwcKa_9mK8x'),identifier(none,p),identifier(none,'PLATFORM'))],[],[assign(rodinpos(s3_mch8_switch,act1,'_uoRhY1OTEd-qwcKa_9mK8w'),[identifier(none,out_switch_act)],[identifier(none,p)]),assign(rodinpos(s3_mch8_switch,act2,'_uoSIcFOTEd-qwcKa_9mK8w'),[identifier(none,out_switch_sig)],[boolean_true(none)]),assign(rodinpos(s3_mch8_switch,act3,'_uoSIcFOTEd-qwcKa_9mK8z'),[identifier(none,out_switch)],[identifier(none,p)])],[]),event(rodinpos(s3_mch8_switch,allow_entrance,'_XmtVBDB6Ed-6kJpHxFX5oA'),allow_entrance,anticipated(none),[allow_entrance],[],[equal(rodinpos(s3_mch8_switch,grd1,'_oXu68VOUEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_false(none)),not_member(rodinpos(s3_mch8_switch,grd2,'_9Z9OMFOtEd-qwcKa_9mK8w'),identifier(none,in_switch),identifier(none,occ_snsr)),equal(rodinpos(s3_mch8_switch,grd3,'__cteMFOvEd-qwcKa_9mK8w'),identifier(none,in_switch_sig),boolean_false(none))],[],[assign(rodinpos(s3_mch8_switch,act1,'_oXu681OUEd-qwcKa_9mK8w'),[identifier(none,in_signal_act)],[boolean_true(none)])],[]),event(rodinpos(s3_mch8_switch,allow_departure,'_Xmt8EjB6Ed-6kJpHxFX5oA'),allow_departure,anticipated(none),[allow_departure],[],[equal(rodinpos(s3_mch8_switch,grd1,'_oXviAFOUEd-qwcKa_9mK8w'),identifier(none,out_signal_act),boolean_false(none)),not_member(rodinpos(s3_mch8_switch,grd2,'_9Z91QFOtEd-qwcKa_9mK8w'),identifier(none,ext_pnt),identifier(none,occ_snsr)),equal(rodinpos(s3_mch8_switch,grd3,'__cuFQFOvEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_false(none))],[],[assign(rodinpos(s3_mch8_switch,act1,'_oXviAlOUEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_true(none)])],[])])]),event_b_model(none,s3_mch7_track_sensor,[sees(none,[s1_ctx0_blocks,s1_ctx1_blocks,s1_ctx2_signal,s1_ctx3_trains]),refines(none,s3_mch6_signal_sensor),variables(none,[identifier(none,'ENTRY_SIGNAL'),identifier(none,'EXIT_SIGNAL'),identifier(none,'IN_SWITCH'),identifier(none,'OCC'),identifier(none,'OUT_SWITCH'),identifier(none,'POS'),identifier(none,entry_signal_snsr),identifier(none,exit_signal_snsr),identifier(none,in_signal_act),identifier(none,in_switch_act),identifier(none,in_switch_sig),identifier(none,occ_snsr),identifier(none,out_signal_act),identifier(none,out_switch_act),identifier(none,out_switch_sig)]),invariant(none,[subset(rodinpos(s3_mch7_track_sensor,inv1,'_oK_Fwy6wEd-XL95EVwlwxw'),identifier(none,'OCC'),identifier(none,'BLOCK')),member(rodinpos(s3_mch7_track_sensor,inv1,'_Rx3RMC68Ed-0PKStM0XZhg'),identifier(none,'IN_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s3_mch7_track_sensor,inv2,'_Rx34QC68Ed-0PKStM0XZhg'),identifier(none,'OUT_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s3_mch7_track_sensor,inv1,'_XmqRsjB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,'ACCESS')),member(rodinpos(s3_mch7_track_sensor,inv2,'_XmqRszB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,'ACCESS')),disjunct(rodinpos(s3_mch7_track_sensor,inv3,'_Xmq4wDB6Ed-6kJpHxFX5oA'),not_equal(none,identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed)),not_member(none,identifier(none,'IN_SWITCH'),identifier(none,'OCC'))),disjunct(rodinpos(s3_mch7_track_sensor,inv4,'_Xmq4wTB6Ed-6kJpHxFX5oA'),not_equal(none,identifier(none,'EXIT_SIGNAL'),identifier(none,allowed)),not_member(none,identifier(none,ext_pnt),identifier(none,'OCC'))),member(rodinpos(s3_mch7_track_sensor,inv1,'_oecFITCQEd-6kJpHxFX5oA'),identifier(none,'POS'),partial_function(none,identifier(none,'TRAIN'),identifier(none,'BLOCK'))),equal(rodinpos(s3_mch7_track_sensor,inv2,'_oecsMTCQEd-6kJpHxFX5oA'),range(none,identifier(none,'POS')),identifier(none,'OCC')),forall(rodinpos(s3_mch7_track_sensor,inv3,'_oecsMjCQEd-6kJpHxFX5oA'),[identifier(none,t1),identifier(none,t2)],implication(none,conjunct(none,member(none,identifier(none,t1),domain(none,identifier(none,'POS'))),conjunct(none,member(none,identifier(none,t2),domain(none,identifier(none,'POS'))),equal(none,function(none,identifier(none,'POS'),[identifier(none,t1)]),function(none,identifier(none,'POS'),[identifier(none,t2)])))),equal(none,identifier(none,t1),identifier(none,t2)))),member(rodinpos(s3_mch7_track_sensor,inv1,'_bwbBEk7yEd-P0eLWrKaUUw'),identifier(none,in_switch_act),identifier(none,'PLATFORM')),member(rodinpos(s3_mch7_track_sensor,inv2,'_uoN3AVOTEd-qwcKa_9mK8w'),identifier(none,out_switch_act),identifier(none,'PLATFORM')),implication(rodinpos(s3_mch7_track_sensor,inv3,'_8YCswFOCEd-_lt3WaRv46A'),equal(none,identifier(none,in_switch_sig),boolean_true(none)),equal(none,identifier(none,'ENTRY_SIGNAL'),identifier(none,forbidden))),implication(rodinpos(s3_mch7_track_sensor,inv4,'_uoN3AlOTEd-qwcKa_9mK8w'),equal(none,identifier(none,out_switch_sig),boolean_true(none)),equal(none,identifier(none,'EXIT_SIGNAL'),identifier(none,forbidden))),member(rodinpos(s3_mch7_track_sensor,inv1,'_oXseslOUEd-qwcKa_9mK8w'),identifier(none,in_signal_act),bool_set(none)),member(rodinpos(s3_mch7_track_sensor,inv2,'_oXses1OUEd-qwcKa_9mK8w'),identifier(none,out_signal_act),bool_set(none)),disjunct(rodinpos(s3_mch7_track_sensor,inv5,'_9Z6K4FOtEd-qwcKa_9mK8w'),equal(none,identifier(none,in_signal_act),boolean_false(none)),not_member(none,identifier(none,'IN_SWITCH'),range(none,identifier(none,'POS')))),disjunct(rodinpos(s3_mch7_track_sensor,inv6,'_9Z6K4VOtEd-qwcKa_9mK8w'),equal(none,identifier(none,out_signal_act),boolean_false(none)),not_member(none,identifier(none,ext_pnt),range(none,identifier(none,'POS')))),disjunct(rodinpos(s3_mch7_track_sensor,inv7,'_9Z6K4lOtEd-qwcKa_9mK8w'),equal(none,identifier(none,in_signal_act),boolean_false(none)),equal(none,identifier(none,in_switch_sig),boolean_false(none))),disjunct(rodinpos(s3_mch7_track_sensor,inv8,'_9Z6K41OtEd-qwcKa_9mK8w'),equal(none,identifier(none,out_signal_act),boolean_false(none)),equal(none,identifier(none,out_switch_sig),boolean_false(none))),equal(rodinpos(s3_mch7_track_sensor,inv1,'_ofEk0VeAEd-YX5Y88L2F0U'),identifier(none,occ_snsr),identifier(none,'OCC'))]),theorems(none,[member(rodinpos(s3_mch7_track_sensor,thm4,'_Yh0z0DEGEd-pyqeHaVRg2g'),identifier(none,'POS'),partial_injection(none,identifier(none,'TRAIN'),identifier(none,'BLOCK')))]),events(none,[event(rodinpos(s3_mch7_track_sensor,'INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(s3_mch7_track_sensor,act1,'_oLAT4C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[empty_set(none)]),becomes_element_of(rodinpos(s3_mch7_track_sensor,act2,'_Rx34QS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],identifier(none,'PLATFORM')),becomes_element_of(rodinpos(s3_mch7_track_sensor,act3,'_Rx34Qi68Ed-0PKStM0XZhg'),[identifier(none,'OUT_SWITCH')],identifier(none,'PLATFORM')),assign(rodinpos(s3_mch7_track_sensor,act4,'_Xmrf0DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s3_mch7_track_sensor,act5,'_Xmrf0TB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s3_mch7_track_sensor,act6,'_oedTQDCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[empty_set(none)]),becomes_element_of(rodinpos(s3_mch7_track_sensor,act7,'_Rs-R4FYTEd-rnu8Rug219Q'),[identifier(none,in_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s3_mch7_track_sensor,act8,'_oedTQDCQEd-6kJpHxFX5oA'),[identifier(none,in_switch_sig)],[boolean_false(none)]),becomes_element_of(rodinpos(s3_mch7_track_sensor,act9,'_gcPBME74Ed-P0eLWrKaUUw'),[identifier(none,out_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s3_mch7_track_sensor,act10,'_gcPBMU74Ed-P0eLWrKaUUw'),[identifier(none,out_switch_sig)],[boolean_false(none)]),assign(rodinpos(s3_mch7_track_sensor,act11,'_Rx34Qi68Ed-0PKStM0XZhg'),[identifier(none,in_signal_act)],[boolean_false(none)]),assign(rodinpos(s3_mch7_track_sensor,act12,'_uoPFIFOTEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_false(none)]),assign(rodinpos(s3_mch7_track_sensor,act13,'\''),[identifier(none,entry_signal_snsr)],[identifier(none,forbidden)]),assign(rodinpos(s3_mch7_track_sensor,act14,'('),[identifier(none,exit_signal_snsr)],[identifier(none,forbidden)]),assign(rodinpos(s3_mch7_track_sensor,act15,'\''),[identifier(none,occ_snsr)],[empty_set(none)])],[]),event(rodinpos(s3_mch7_track_sensor,'ARRIVE','_oLAT4i6wEd-XL95EVwlwxw'),'ARRIVE',anticipated(none),['ARRIVE'],[identifier(rodinpos(s3_mch7_track_sensor,[],'_oedTQjCQEd-6kJpHxFX5oA'),t)],[not_member(rodinpos(s3_mch7_track_sensor,grd1,'_oLAT4y6wEd-XL95EVwlwxw'),identifier(none,ent_pnt),identifier(none,'OCC')),not_member(rodinpos(s3_mch7_track_sensor,grd2,'_oed6UDCQEd-6kJpHxFX5oA'),identifier(none,t),domain(none,identifier(none,'POS')))],[],[assign(rodinpos(s3_mch7_track_sensor,act1,'_oLA68C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s3_mch7_track_sensor,act3,'_oed6UTCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,ent_pnt)])]))]),assign(rodinpos(s3_mch7_track_sensor,act4,'('),[identifier(none,occ_snsr)],[union(none,identifier(none,occ_snsr),set_extension(none,[identifier(none,ent_pnt)]))])],[]),event(rodinpos(s3_mch7_track_sensor,'LEAVE','_oLA68i6wEd-XL95EVwlwxw'),'LEAVE',anticipated(none),['LEAVE'],[identifier(rodinpos(s3_mch7_track_sensor,[],'_oed6UzCQEd-6kJpHxFX5oA'),t)],[member(rodinpos(s3_mch7_track_sensor,grd1,'_oeehYTCQEd-6kJpHxFX5oB'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s3_mch7_track_sensor,grd2,'_oeehYDCQEd-6kJpHxFX5oA'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,ext_pnt))],[],[assign(rodinpos(s3_mch7_track_sensor,act1,'_oLA69C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)]))]),assign(rodinpos(s3_mch7_track_sensor,act2,'_oeehYTCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[domain_subtraction(none,set_extension(none,[identifier(none,t)]),identifier(none,'POS'))]),assign(rodinpos(s3_mch7_track_sensor,act4,'('),[identifier(none,occ_snsr)],[set_subtraction(none,identifier(none,occ_snsr),set_extension(none,[identifier(none,ext_pnt)]))])],[]),event(rodinpos(s3_mch7_track_sensor,'MOVE_IN_PLATFORM','_oLBiAC6wEd-XL95EVwlwxw'),'MOVE_IN_PLATFORM',anticipated(none),['MOVE_IN_PLATFORM'],[identifier(rodinpos(s3_mch7_track_sensor,[],'_Yh2pATEGEd-pyqeHaVRg2g'),t)],[equal(rodinpos(s3_mch7_track_sensor,grd1,'_XmsG4jB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed)),member(rodinpos(s3_mch7_track_sensor,grd2,'_Yh2pAjEGEd-pyqeHaVRg2g'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s3_mch7_track_sensor,grd3,'_Yh3QEDEGEd-pyqeHaVRg2g'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,ent_pnt)),equal(rodinpos(s3_mch7_track_sensor,grd4,'_9Z7ZAlOtEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_false(none))],[],[assign(rodinpos(s3_mch7_track_sensor,act1,'_XmsG4zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,'IN_SWITCH')])),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s3_mch7_track_sensor,act2,'_XmsG5DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s3_mch7_track_sensor,act3,'_Yh3QETEGEd-pyqeHaVRg2g'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,'IN_SWITCH')])]))]),assign(rodinpos(s3_mch7_track_sensor,act4,'('),[identifier(none,entry_signal_snsr)],[identifier(none,forbidden)]),assign(rodinpos(s3_mch7_track_sensor,act5,'('),[identifier(none,occ_snsr)],[set_subtraction(none,union(none,identifier(none,occ_snsr),set_extension(none,[identifier(none,'IN_SWITCH')])),set_extension(none,[identifier(none,ent_pnt)]))])],[]),event(rodinpos(s3_mch7_track_sensor,'MOVE_OUT_PLATFORM','_oLBiBC6wEd-XL95EVwlwxw'),'MOVE_OUT_PLATFORM',anticipated(none),['MOVE_OUT_PLATFORM'],[identifier(rodinpos(s3_mch7_track_sensor,[],'_Yh3QEzEGEd-pyqeHaVRg2g'),t)],[equal(rodinpos(s3_mch7_track_sensor,grd1,'_Xmst8jB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,allowed)),member(rodinpos(s3_mch7_track_sensor,grd2,'_Yh3QFDEGEd-pyqeHaVRg2g'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s3_mch7_track_sensor,grd3,'_Yh3QFTEGEd-pyqeHaVRg2g'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,'OUT_SWITCH')),equal(rodinpos(s3_mch7_track_sensor,grd4,'_NQysYVYREd-rnu8Rug219Q'),identifier(none,out_signal_act),boolean_false(none))],[],[assign(rodinpos(s3_mch7_track_sensor,act1,'_Xmst8zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)])),set_extension(none,[identifier(none,'OUT_SWITCH')]))]),assign(rodinpos(s3_mch7_track_sensor,act2,'_Xmst9DB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s3_mch7_track_sensor,act3,'_Yh33IDEGEd-pyqeHaVRg2g'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,ext_pnt)])]))]),assign(rodinpos(s3_mch7_track_sensor,act4,'('),[identifier(none,exit_signal_snsr)],[identifier(none,forbidden)]),assign(rodinpos(s3_mch7_track_sensor,act5,'('),[identifier(none,occ_snsr)],[set_subtraction(none,union(none,identifier(none,occ_snsr),set_extension(none,[identifier(none,ext_pnt)])),set_extension(none,[identifier(none,'OUT_SWITCH')]))])],[]),event(rodinpos(s3_mch7_track_sensor,'TURN_IN_SWITCH','_bwercU7yEd-P0eLWrKaUUw'),'TURN_IN_SWITCH',anticipated(none),['TURN_IN_SWITCH'],[],[equal(rodinpos(s3_mch7_track_sensor,grd1,'_XmtVATB6Ed-6kJpHxFX5oA'),identifier(none,in_switch_sig),boolean_true(none))],[],[assign(rodinpos(s3_mch7_track_sensor,act1,'_Rx5GYS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],[identifier(none,in_switch_act)]),assign(rodinpos(s3_mch7_track_sensor,act2,'_8YJacFOCEd-_lt3WaRv46A'),[identifier(none,in_switch_sig)],[boolean_false(none)])],[]),event(rodinpos(s3_mch7_track_sensor,'TURN_OUT_SWITCH','_5TLaUFOSEd-qwcKa_9mK8w'),'TURN_OUT_SWITCH',anticipated(none),['TURN_OUT_SWITCH'],[],[equal(rodinpos(s3_mch7_track_sensor,grd1,'_uoSvglOTEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_true(none))],[],[assign(rodinpos(s3_mch7_track_sensor,act1,'_uoSvg1OTEd-qwcKa_9mK8w'),[identifier(none,'OUT_SWITCH')],[identifier(none,out_switch_act)]),assign(rodinpos(s3_mch7_track_sensor,act2,'_uoSvhFOTEd-qwcKa_9mK8w'),[identifier(none,out_switch_sig)],[boolean_false(none)])],[]),event(rodinpos(s3_mch7_track_sensor,'ALLOW_ENTRANCE','_oXviA1OUEd-qwcKa_9mK8w'),'ALLOW_ENTRANCE',anticipated(none),['ALLOW_ENTRANCE'],[],[equal(rodinpos(s3_mch7_track_sensor,grd1,'_oXwJEVOUEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_true(none))],[],[assign(rodinpos(s3_mch7_track_sensor,act1,'_Xmt8ETB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,allowed)]),assign(rodinpos(s3_mch7_track_sensor,act2,'_oXwJElOUEd-qwcKa_9mK8w'),[identifier(none,in_signal_act)],[boolean_false(none)]),assign(rodinpos(s3_mch7_track_sensor,act3,'('),[identifier(none,entry_signal_snsr)],[identifier(none,allowed)])],[]),event(rodinpos(s3_mch7_track_sensor,'ALLOW_DEPARTURE','_oXwJE1OUEd-qwcKa_9mK8w'),'ALLOW_DEPARTURE',anticipated(none),['ALLOW_DEPARTURE'],[],[equal(rodinpos(s3_mch7_track_sensor,grd1,'_oXwJFVOUEd-qwcKa_9mK8w'),identifier(none,out_signal_act),boolean_true(none))],[],[assign(rodinpos(s3_mch7_track_sensor,act1,'_Xmt8FDB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,allowed)]),assign(rodinpos(s3_mch7_track_sensor,act2,'_oXwJFlOUEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_false(none)]),assign(rodinpos(s3_mch7_track_sensor,act3,'('),[identifier(none,exit_signal_snsr)],[identifier(none,allowed)])],[]),event(rodinpos(s3_mch7_track_sensor,trigger_in_switch,'_bweEYk7yEd-P0eLWrKaUUw'),trigger_in_switch,anticipated(none),[trigger_in_switch],[],[equal(rodinpos(s3_mch7_track_sensor,grd1,'_gcSEgE74Ed-P0eLWrKaUUw'),identifier(none,entry_signal_snsr),identifier(none,forbidden)),equal(rodinpos(s3_mch7_track_sensor,grd2,'_gcSEgk74Ed-P0eLWrKaUUw'),identifier(none,in_switch_sig),boolean_false(none)),equal(rodinpos(s3_mch7_track_sensor,grd3,'_ofKrcFeAEd-YX5Y88L2F0R'),identifier(none,in_signal_act),boolean_false(none))],[],[becomes_element_of(rodinpos(s3_mch7_track_sensor,act1,'_bweEY07yEd-P0eLWrKaUUw'),[identifier(none,in_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s3_mch7_track_sensor,act2,'_bwercE7yEd-P0eLWrKaUUw'),[identifier(none,in_switch_sig)],[boolean_true(none)])],[]),event(rodinpos(s3_mch7_track_sensor,trigger_out_switch,'_5TMBZFOSEd-qwcKa_9mK8w'),trigger_out_switch,anticipated(none),[trigger_out_switch],[],[equal(rodinpos(s3_mch7_track_sensor,grd1,'_uoRhYVOTEd-qwcKa_9mK8w'),identifier(none,exit_signal_snsr),identifier(none,forbidden)),equal(rodinpos(s3_mch7_track_sensor,grd2,'_uoRhYlOTEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_false(none)),equal(rodinpos(s3_mch7_track_sensor,grd3,'_ofL5kFeAEd-YX5Y88L2F0R'),identifier(none,out_signal_act),boolean_false(none))],[],[becomes_element_of(rodinpos(s3_mch7_track_sensor,act1,'_uoRhY1OTEd-qwcKa_9mK8w'),[identifier(none,out_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s3_mch7_track_sensor,act2,'_uoSIcFOTEd-qwcKa_9mK8w'),[identifier(none,out_switch_sig)],[boolean_true(none)])],[]),event(rodinpos(s3_mch7_track_sensor,allow_entrance,'_XmtVBDB6Ed-6kJpHxFX5oA'),allow_entrance,anticipated(none),[allow_entrance],[],[equal(rodinpos(s3_mch7_track_sensor,grd1,'_oXu68VOUEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_false(none)),not_member(rodinpos(s3_mch7_track_sensor,grd2,'_9Z9OMFOtEd-qwcKa_9mK8w'),identifier(none,'IN_SWITCH'),identifier(none,occ_snsr)),equal(rodinpos(s3_mch7_track_sensor,grd3,'__cteMFOvEd-qwcKa_9mK8w'),identifier(none,in_switch_sig),boolean_false(none))],[],[assign(rodinpos(s3_mch7_track_sensor,act1,'_oXu681OUEd-qwcKa_9mK8w'),[identifier(none,in_signal_act)],[boolean_true(none)])],[]),event(rodinpos(s3_mch7_track_sensor,allow_departure,'_Xmt8EjB6Ed-6kJpHxFX5oA'),allow_departure,anticipated(none),[allow_departure],[],[equal(rodinpos(s3_mch7_track_sensor,grd1,'_oXviAFOUEd-qwcKa_9mK8w'),identifier(none,out_signal_act),boolean_false(none)),not_member(rodinpos(s3_mch7_track_sensor,grd2,'_9Z91QFOtEd-qwcKa_9mK8w'),identifier(none,ext_pnt),identifier(none,occ_snsr)),equal(rodinpos(s3_mch7_track_sensor,grd3,'__cuFQFOvEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_false(none))],[],[assign(rodinpos(s3_mch7_track_sensor,act1,'_oXviAlOUEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_true(none)])],[])])]),event_b_model(none,s3_mch6_signal_sensor,[sees(none,[s1_ctx0_blocks,s1_ctx1_blocks,s1_ctx2_signal,s1_ctx3_trains]),refines(none,s2_mch5_signal_actuator),variables(none,[identifier(none,'ENTRY_SIGNAL'),identifier(none,'EXIT_SIGNAL'),identifier(none,'IN_SWITCH'),identifier(none,'OCC'),identifier(none,'OUT_SWITCH'),identifier(none,'POS'),identifier(none,entry_signal_snsr),identifier(none,exit_signal_snsr),identifier(none,in_signal_act),identifier(none,in_switch_act),identifier(none,in_switch_sig),identifier(none,out_signal_act),identifier(none,out_switch_act),identifier(none,out_switch_sig)]),invariant(none,[subset(rodinpos(s3_mch6_signal_sensor,inv1,'_oK_Fwy6wEd-XL95EVwlwxw'),identifier(none,'OCC'),identifier(none,'BLOCK')),member(rodinpos(s3_mch6_signal_sensor,inv1,'_Rx3RMC68Ed-0PKStM0XZhg'),identifier(none,'IN_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s3_mch6_signal_sensor,inv2,'_Rx34QC68Ed-0PKStM0XZhg'),identifier(none,'OUT_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s3_mch6_signal_sensor,inv1,'_XmqRsjB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,'ACCESS')),member(rodinpos(s3_mch6_signal_sensor,inv2,'_XmqRszB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,'ACCESS')),disjunct(rodinpos(s3_mch6_signal_sensor,inv3,'_Xmq4wDB6Ed-6kJpHxFX5oA'),not_equal(none,identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed)),not_member(none,identifier(none,'IN_SWITCH'),identifier(none,'OCC'))),disjunct(rodinpos(s3_mch6_signal_sensor,inv4,'_Xmq4wTB6Ed-6kJpHxFX5oA'),not_equal(none,identifier(none,'EXIT_SIGNAL'),identifier(none,allowed)),not_member(none,identifier(none,ext_pnt),identifier(none,'OCC'))),member(rodinpos(s3_mch6_signal_sensor,inv1,'_oecFITCQEd-6kJpHxFX5oA'),identifier(none,'POS'),partial_function(none,identifier(none,'TRAIN'),identifier(none,'BLOCK'))),equal(rodinpos(s3_mch6_signal_sensor,inv2,'_oecsMTCQEd-6kJpHxFX5oA'),range(none,identifier(none,'POS')),identifier(none,'OCC')),forall(rodinpos(s3_mch6_signal_sensor,inv3,'_oecsMjCQEd-6kJpHxFX5oA'),[identifier(none,t1),identifier(none,t2)],implication(none,conjunct(none,member(none,identifier(none,t1),domain(none,identifier(none,'POS'))),conjunct(none,member(none,identifier(none,t2),domain(none,identifier(none,'POS'))),equal(none,function(none,identifier(none,'POS'),[identifier(none,t1)]),function(none,identifier(none,'POS'),[identifier(none,t2)])))),equal(none,identifier(none,t1),identifier(none,t2)))),member(rodinpos(s3_mch6_signal_sensor,inv1,'_bwbBEk7yEd-P0eLWrKaUUw'),identifier(none,in_switch_act),identifier(none,'PLATFORM')),member(rodinpos(s3_mch6_signal_sensor,inv2,'_uoN3AVOTEd-qwcKa_9mK8w'),identifier(none,out_switch_act),identifier(none,'PLATFORM')),implication(rodinpos(s3_mch6_signal_sensor,inv3,'_8YCswFOCEd-_lt3WaRv46A'),equal(none,identifier(none,in_switch_sig),boolean_true(none)),equal(none,identifier(none,'ENTRY_SIGNAL'),identifier(none,forbidden))),implication(rodinpos(s3_mch6_signal_sensor,inv4,'_uoN3AlOTEd-qwcKa_9mK8w'),equal(none,identifier(none,out_switch_sig),boolean_true(none)),equal(none,identifier(none,'EXIT_SIGNAL'),identifier(none,forbidden))),equal(rodinpos(s3_mch6_signal_sensor,inv1,'_ofEk0VeAEd-YX5Y88L2F0U'),identifier(none,entry_signal_snsr),identifier(none,'ENTRY_SIGNAL')),equal(rodinpos(s3_mch6_signal_sensor,inv2,'_ofEk0VeAEd-YX5Y88L2F0W'),identifier(none,exit_signal_snsr),identifier(none,'EXIT_SIGNAL'))]),theorems(none,[member(rodinpos(s3_mch6_signal_sensor,thm4,'_Yh0z0DEGEd-pyqeHaVRg2g'),identifier(none,'POS'),partial_injection(none,identifier(none,'TRAIN'),identifier(none,'BLOCK')))]),events(none,[event(rodinpos(s3_mch6_signal_sensor,'INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(s3_mch6_signal_sensor,act1,'_oLAT4C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[empty_set(none)]),becomes_element_of(rodinpos(s3_mch6_signal_sensor,act2,'_Rx34QS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],identifier(none,'PLATFORM')),becomes_element_of(rodinpos(s3_mch6_signal_sensor,act3,'_Rx34Qi68Ed-0PKStM0XZhg'),[identifier(none,'OUT_SWITCH')],identifier(none,'PLATFORM')),assign(rodinpos(s3_mch6_signal_sensor,act4,'_Xmrf0DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s3_mch6_signal_sensor,act5,'_Xmrf0TB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s3_mch6_signal_sensor,act6,'_oedTQDCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[empty_set(none)]),becomes_element_of(rodinpos(s3_mch6_signal_sensor,act7,'_Rs-R4FYTEd-rnu8Rug219Q'),[identifier(none,in_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s3_mch6_signal_sensor,act8,'_oedTQDCQEd-6kJpHxFX5oA'),[identifier(none,in_switch_sig)],[boolean_false(none)]),becomes_element_of(rodinpos(s3_mch6_signal_sensor,act9,'_gcPBME74Ed-P0eLWrKaUUw'),[identifier(none,out_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s3_mch6_signal_sensor,act10,'_gcPBMU74Ed-P0eLWrKaUUw'),[identifier(none,out_switch_sig)],[boolean_false(none)]),assign(rodinpos(s3_mch6_signal_sensor,act11,'_Rx34Qi68Ed-0PKStM0XZhg'),[identifier(none,in_signal_act)],[boolean_false(none)]),assign(rodinpos(s3_mch6_signal_sensor,act12,'_uoPFIFOTEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_false(none)]),assign(rodinpos(s3_mch6_signal_sensor,act13,'\''),[identifier(none,entry_signal_snsr)],[identifier(none,forbidden)]),assign(rodinpos(s3_mch6_signal_sensor,act14,'('),[identifier(none,exit_signal_snsr)],[identifier(none,forbidden)])],[]),event(rodinpos(s3_mch6_signal_sensor,'ARRIVE','_oLAT4i6wEd-XL95EVwlwxw'),'ARRIVE',anticipated(none),['ARRIVE'],[identifier(rodinpos(s3_mch6_signal_sensor,[],'_oedTQjCQEd-6kJpHxFX5oA'),t)],[not_member(rodinpos(s3_mch6_signal_sensor,grd1,'_oLAT4y6wEd-XL95EVwlwxw'),identifier(none,ent_pnt),identifier(none,'OCC')),not_member(rodinpos(s3_mch6_signal_sensor,grd2,'_oed6UDCQEd-6kJpHxFX5oA'),identifier(none,t),domain(none,identifier(none,'POS')))],[],[assign(rodinpos(s3_mch6_signal_sensor,act1,'_oLA68C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s3_mch6_signal_sensor,act3,'_oed6UTCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,ent_pnt)])]))])],[]),event(rodinpos(s3_mch6_signal_sensor,'LEAVE','_oLA68i6wEd-XL95EVwlwxw'),'LEAVE',anticipated(none),['LEAVE'],[identifier(rodinpos(s3_mch6_signal_sensor,[],'_oed6UzCQEd-6kJpHxFX5oA'),t)],[member(rodinpos(s3_mch6_signal_sensor,grd1,'_oeehYTCQEd-6kJpHxFX5oB'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s3_mch6_signal_sensor,grd2,'_oeehYDCQEd-6kJpHxFX5oA'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,ext_pnt))],[],[assign(rodinpos(s3_mch6_signal_sensor,act1,'_oLA69C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)]))]),assign(rodinpos(s3_mch6_signal_sensor,act2,'_oeehYTCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[domain_subtraction(none,set_extension(none,[identifier(none,t)]),identifier(none,'POS'))])],[]),event(rodinpos(s3_mch6_signal_sensor,'MOVE_IN_PLATFORM','_oLBiAC6wEd-XL95EVwlwxw'),'MOVE_IN_PLATFORM',anticipated(none),['MOVE_IN_PLATFORM'],[identifier(rodinpos(s3_mch6_signal_sensor,[],'_Yh2pATEGEd-pyqeHaVRg2g'),t)],[equal(rodinpos(s3_mch6_signal_sensor,grd1,'_XmsG4jB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed)),member(rodinpos(s3_mch6_signal_sensor,grd2,'_Yh2pAjEGEd-pyqeHaVRg2g'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s3_mch6_signal_sensor,grd3,'_Yh3QEDEGEd-pyqeHaVRg2g'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,ent_pnt)),equal(rodinpos(s3_mch6_signal_sensor,grd4,'_9Z7ZAlOtEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_false(none))],[],[assign(rodinpos(s3_mch6_signal_sensor,act1,'_XmsG4zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,'IN_SWITCH')])),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s3_mch6_signal_sensor,act2,'_XmsG5DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s3_mch6_signal_sensor,act3,'_Yh3QETEGEd-pyqeHaVRg2g'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,'IN_SWITCH')])]))]),assign(rodinpos(s3_mch6_signal_sensor,act4,'('),[identifier(none,entry_signal_snsr)],[identifier(none,forbidden)])],[]),event(rodinpos(s3_mch6_signal_sensor,'MOVE_OUT_PLATFORM','_oLBiBC6wEd-XL95EVwlwxw'),'MOVE_OUT_PLATFORM',anticipated(none),['MOVE_OUT_PLATFORM'],[identifier(rodinpos(s3_mch6_signal_sensor,[],'_Yh3QEzEGEd-pyqeHaVRg2g'),t)],[equal(rodinpos(s3_mch6_signal_sensor,grd1,'_Xmst8jB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,allowed)),member(rodinpos(s3_mch6_signal_sensor,grd2,'_Yh3QFDEGEd-pyqeHaVRg2g'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s3_mch6_signal_sensor,grd3,'_Yh3QFTEGEd-pyqeHaVRg2g'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,'OUT_SWITCH')),equal(rodinpos(s3_mch6_signal_sensor,grd4,'_NQysYVYREd-rnu8Rug219Q'),identifier(none,out_signal_act),boolean_false(none))],[],[assign(rodinpos(s3_mch6_signal_sensor,act1,'_Xmst8zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)])),set_extension(none,[identifier(none,'OUT_SWITCH')]))]),assign(rodinpos(s3_mch6_signal_sensor,act2,'_Xmst9DB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s3_mch6_signal_sensor,act3,'_Yh33IDEGEd-pyqeHaVRg2g'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,ext_pnt)])]))]),assign(rodinpos(s3_mch6_signal_sensor,act4,'('),[identifier(none,exit_signal_snsr)],[identifier(none,forbidden)])],[]),event(rodinpos(s3_mch6_signal_sensor,'TURN_IN_SWITCH','_bwercU7yEd-P0eLWrKaUUw'),'TURN_IN_SWITCH',anticipated(none),['TURN_IN_SWITCH'],[],[equal(rodinpos(s3_mch6_signal_sensor,grd1,'_XmtVATB6Ed-6kJpHxFX5oA'),identifier(none,in_switch_sig),boolean_true(none))],[],[assign(rodinpos(s3_mch6_signal_sensor,act1,'_Rx5GYS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],[identifier(none,in_switch_act)]),assign(rodinpos(s3_mch6_signal_sensor,act2,'_8YJacFOCEd-_lt3WaRv46A'),[identifier(none,in_switch_sig)],[boolean_false(none)])],[]),event(rodinpos(s3_mch6_signal_sensor,'TURN_OUT_SWITCH','_5TLaUFOSEd-qwcKa_9mK8w'),'TURN_OUT_SWITCH',anticipated(none),['TURN_OUT_SWITCH'],[],[equal(rodinpos(s3_mch6_signal_sensor,grd1,'_uoSvglOTEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_true(none))],[],[assign(rodinpos(s3_mch6_signal_sensor,act1,'_uoSvg1OTEd-qwcKa_9mK8w'),[identifier(none,'OUT_SWITCH')],[identifier(none,out_switch_act)]),assign(rodinpos(s3_mch6_signal_sensor,act2,'_uoSvhFOTEd-qwcKa_9mK8w'),[identifier(none,out_switch_sig)],[boolean_false(none)])],[]),event(rodinpos(s3_mch6_signal_sensor,'ALLOW_ENTRANCE','_oXviA1OUEd-qwcKa_9mK8w'),'ALLOW_ENTRANCE',anticipated(none),['ALLOW_ENTRANCE'],[],[equal(rodinpos(s3_mch6_signal_sensor,grd1,'_oXwJEVOUEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_true(none))],[],[assign(rodinpos(s3_mch6_signal_sensor,act1,'_Xmt8ETB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,allowed)]),assign(rodinpos(s3_mch6_signal_sensor,act2,'_oXwJElOUEd-qwcKa_9mK8w'),[identifier(none,in_signal_act)],[boolean_false(none)]),assign(rodinpos(s3_mch6_signal_sensor,act3,'('),[identifier(none,entry_signal_snsr)],[identifier(none,allowed)])],[]),event(rodinpos(s3_mch6_signal_sensor,'ALLOW_DEPARTURE','_oXwJE1OUEd-qwcKa_9mK8w'),'ALLOW_DEPARTURE',anticipated(none),['ALLOW_DEPARTURE'],[],[equal(rodinpos(s3_mch6_signal_sensor,grd1,'_oXwJFVOUEd-qwcKa_9mK8w'),identifier(none,out_signal_act),boolean_true(none))],[],[assign(rodinpos(s3_mch6_signal_sensor,act1,'_Xmt8FDB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,allowed)]),assign(rodinpos(s3_mch6_signal_sensor,act2,'_oXwJFlOUEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_false(none)]),assign(rodinpos(s3_mch6_signal_sensor,act3,'('),[identifier(none,exit_signal_snsr)],[identifier(none,allowed)])],[]),event(rodinpos(s3_mch6_signal_sensor,trigger_in_switch,'_bweEYk7yEd-P0eLWrKaUUw'),trigger_in_switch,anticipated(none),[trigger_in_switch],[],[equal(rodinpos(s3_mch6_signal_sensor,grd1,'_gcSEgE74Ed-P0eLWrKaUUw'),identifier(none,entry_signal_snsr),identifier(none,forbidden)),equal(rodinpos(s3_mch6_signal_sensor,grd2,'_gcSEgk74Ed-P0eLWrKaUUw'),identifier(none,in_switch_sig),boolean_false(none)),equal(rodinpos(s3_mch6_signal_sensor,grd3,'_ofKrcFeAEd-YX5Y88L2F0R'),identifier(none,in_signal_act),boolean_false(none))],[],[becomes_element_of(rodinpos(s3_mch6_signal_sensor,act1,'_bweEY07yEd-P0eLWrKaUUw'),[identifier(none,in_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s3_mch6_signal_sensor,act2,'_bwercE7yEd-P0eLWrKaUUw'),[identifier(none,in_switch_sig)],[boolean_true(none)])],[]),event(rodinpos(s3_mch6_signal_sensor,trigger_out_switch,'_5TMBZFOSEd-qwcKa_9mK8w'),trigger_out_switch,anticipated(none),[trigger_out_switch],[],[equal(rodinpos(s3_mch6_signal_sensor,grd1,'_uoRhYVOTEd-qwcKa_9mK8w'),identifier(none,exit_signal_snsr),identifier(none,forbidden)),equal(rodinpos(s3_mch6_signal_sensor,grd2,'_uoRhYlOTEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_false(none)),equal(rodinpos(s3_mch6_signal_sensor,grd3,'_ofL5kFeAEd-YX5Y88L2F0R'),identifier(none,out_signal_act),boolean_false(none))],[],[becomes_element_of(rodinpos(s3_mch6_signal_sensor,act1,'_uoRhY1OTEd-qwcKa_9mK8w'),[identifier(none,out_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s3_mch6_signal_sensor,act2,'_uoSIcFOTEd-qwcKa_9mK8w'),[identifier(none,out_switch_sig)],[boolean_true(none)])],[]),event(rodinpos(s3_mch6_signal_sensor,allow_entrance,'_XmtVBDB6Ed-6kJpHxFX5oA'),allow_entrance,anticipated(none),[allow_entrance],[],[equal(rodinpos(s3_mch6_signal_sensor,grd1,'_oXu68VOUEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_false(none)),not_member(rodinpos(s3_mch6_signal_sensor,grd2,'_9Z9OMFOtEd-qwcKa_9mK8w'),identifier(none,'IN_SWITCH'),identifier(none,'OCC')),equal(rodinpos(s3_mch6_signal_sensor,grd3,'__cteMFOvEd-qwcKa_9mK8w'),identifier(none,in_switch_sig),boolean_false(none))],[],[assign(rodinpos(s3_mch6_signal_sensor,act1,'_oXu681OUEd-qwcKa_9mK8w'),[identifier(none,in_signal_act)],[boolean_true(none)])],[]),event(rodinpos(s3_mch6_signal_sensor,allow_departure,'_Xmt8EjB6Ed-6kJpHxFX5oA'),allow_departure,anticipated(none),[allow_departure],[],[equal(rodinpos(s3_mch6_signal_sensor,grd1,'_oXviAFOUEd-qwcKa_9mK8w'),identifier(none,out_signal_act),boolean_false(none)),not_member(rodinpos(s3_mch6_signal_sensor,grd2,'_9Z91QFOtEd-qwcKa_9mK8w'),identifier(none,ext_pnt),identifier(none,'OCC')),equal(rodinpos(s3_mch6_signal_sensor,grd3,'__cuFQFOvEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_false(none))],[],[assign(rodinpos(s3_mch6_signal_sensor,act1,'_oXviAlOUEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_true(none)])],[])])]),event_b_model(none,s2_mch5_signal_actuator,[sees(none,[s1_ctx0_blocks,s1_ctx1_blocks,s1_ctx2_signal,s1_ctx3_trains]),refines(none,s2_mch4_switch_actuator),variables(none,[identifier(none,'ENTRY_SIGNAL'),identifier(none,'EXIT_SIGNAL'),identifier(none,'IN_SWITCH'),identifier(none,'OCC'),identifier(none,'OUT_SWITCH'),identifier(none,'POS'),identifier(none,in_signal_act),identifier(none,in_switch_act),identifier(none,in_switch_sig),identifier(none,out_signal_act),identifier(none,out_switch_act),identifier(none,out_switch_sig)]),invariant(none,[subset(rodinpos(s2_mch5_signal_actuator,inv1,'_oK_Fwy6wEd-XL95EVwlwxw'),identifier(none,'OCC'),identifier(none,'BLOCK')),member(rodinpos(s2_mch5_signal_actuator,inv1,'_Rx3RMC68Ed-0PKStM0XZhg'),identifier(none,'IN_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s2_mch5_signal_actuator,inv2,'_Rx34QC68Ed-0PKStM0XZhg'),identifier(none,'OUT_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s2_mch5_signal_actuator,inv1,'_XmqRsjB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,'ACCESS')),member(rodinpos(s2_mch5_signal_actuator,inv2,'_XmqRszB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,'ACCESS')),disjunct(rodinpos(s2_mch5_signal_actuator,inv3,'_Xmq4wDB6Ed-6kJpHxFX5oA'),not_equal(none,identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed)),not_member(none,identifier(none,'IN_SWITCH'),identifier(none,'OCC'))),disjunct(rodinpos(s2_mch5_signal_actuator,inv4,'_Xmq4wTB6Ed-6kJpHxFX5oA'),not_equal(none,identifier(none,'EXIT_SIGNAL'),identifier(none,allowed)),not_member(none,identifier(none,ext_pnt),identifier(none,'OCC'))),member(rodinpos(s2_mch5_signal_actuator,inv1,'_oecFITCQEd-6kJpHxFX5oA'),identifier(none,'POS'),partial_function(none,identifier(none,'TRAIN'),identifier(none,'BLOCK'))),equal(rodinpos(s2_mch5_signal_actuator,inv2,'_oecsMTCQEd-6kJpHxFX5oA'),range(none,identifier(none,'POS')),identifier(none,'OCC')),forall(rodinpos(s2_mch5_signal_actuator,inv3,'_oecsMjCQEd-6kJpHxFX5oA'),[identifier(none,t1),identifier(none,t2)],implication(none,conjunct(none,member(none,identifier(none,t1),domain(none,identifier(none,'POS'))),conjunct(none,member(none,identifier(none,t2),domain(none,identifier(none,'POS'))),equal(none,function(none,identifier(none,'POS'),[identifier(none,t1)]),function(none,identifier(none,'POS'),[identifier(none,t2)])))),equal(none,identifier(none,t1),identifier(none,t2)))),member(rodinpos(s2_mch5_signal_actuator,inv1,'_oXseslOUEd-qwcKa_9mK8w'),identifier(none,in_signal_act),bool_set(none)),member(rodinpos(s2_mch5_signal_actuator,inv2,'_oXses1OUEd-qwcKa_9mK8w'),identifier(none,out_signal_act),bool_set(none)),disjunct(rodinpos(s2_mch5_signal_actuator,inv5,'_9Z6K4FOtEd-qwcKa_9mK8w'),equal(none,identifier(none,in_signal_act),boolean_false(none)),not_member(none,identifier(none,'IN_SWITCH'),range(none,identifier(none,'POS')))),disjunct(rodinpos(s2_mch5_signal_actuator,inv6,'_9Z6K4VOtEd-qwcKa_9mK8w'),equal(none,identifier(none,out_signal_act),boolean_false(none)),not_member(none,identifier(none,ext_pnt),range(none,identifier(none,'POS')))),disjunct(rodinpos(s2_mch5_signal_actuator,inv7,'_9Z6K4lOtEd-qwcKa_9mK8w'),equal(none,identifier(none,in_signal_act),boolean_false(none)),equal(none,identifier(none,in_switch_sig),boolean_false(none))),disjunct(rodinpos(s2_mch5_signal_actuator,inv8,'_9Z6K41OtEd-qwcKa_9mK8w'),equal(none,identifier(none,out_signal_act),boolean_false(none)),equal(none,identifier(none,out_switch_sig),boolean_false(none)))]),theorems(none,[member(rodinpos(s2_mch5_signal_actuator,thm4,'_Yh0z0DEGEd-pyqeHaVRg2g'),identifier(none,'POS'),partial_injection(none,identifier(none,'TRAIN'),identifier(none,'BLOCK')))]),events(none,[event(rodinpos(s2_mch5_signal_actuator,'INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(s2_mch5_signal_actuator,act1,'_oLAT4C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[empty_set(none)]),becomes_element_of(rodinpos(s2_mch5_signal_actuator,act2,'_Rx34QS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],identifier(none,'PLATFORM')),becomes_element_of(rodinpos(s2_mch5_signal_actuator,act3,'_Rx34Qi68Ed-0PKStM0XZhg'),[identifier(none,'OUT_SWITCH')],identifier(none,'PLATFORM')),assign(rodinpos(s2_mch5_signal_actuator,act4,'_Xmrf0DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s2_mch5_signal_actuator,act5,'_Xmrf0TB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s2_mch5_signal_actuator,act6,'_oedTQDCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[empty_set(none)]),becomes_element_of(rodinpos(s2_mch5_signal_actuator,act7,'_Rs-R4FYTEd-rnu8Rug219Q'),[identifier(none,in_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s2_mch5_signal_actuator,act8,'_oedTQDCQEd-6kJpHxFX5oA'),[identifier(none,in_switch_sig)],[boolean_false(none)]),becomes_element_of(rodinpos(s2_mch5_signal_actuator,act9,'_gcPBME74Ed-P0eLWrKaUUw'),[identifier(none,out_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s2_mch5_signal_actuator,act10,'_gcPBMU74Ed-P0eLWrKaUUw'),[identifier(none,out_switch_sig)],[boolean_false(none)]),assign(rodinpos(s2_mch5_signal_actuator,act11,'_Rx34Qi68Ed-0PKStM0XZhg'),[identifier(none,in_signal_act)],[boolean_false(none)]),assign(rodinpos(s2_mch5_signal_actuator,act12,'_uoPFIFOTEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_false(none)])],[]),event(rodinpos(s2_mch5_signal_actuator,'ARRIVE','_oLAT4i6wEd-XL95EVwlwxw'),'ARRIVE',anticipated(none),['ARRIVE'],[identifier(rodinpos(s2_mch5_signal_actuator,[],'_oedTQjCQEd-6kJpHxFX5oA'),t)],[not_member(rodinpos(s2_mch5_signal_actuator,grd1,'_oLAT4y6wEd-XL95EVwlwxw'),identifier(none,ent_pnt),identifier(none,'OCC')),not_member(rodinpos(s2_mch5_signal_actuator,grd2,'_oed6UDCQEd-6kJpHxFX5oA'),identifier(none,t),domain(none,identifier(none,'POS')))],[],[assign(rodinpos(s2_mch5_signal_actuator,act1,'_oLA68C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s2_mch5_signal_actuator,act3,'_oed6UTCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,ent_pnt)])]))])],[]),event(rodinpos(s2_mch5_signal_actuator,'LEAVE','_oLA68i6wEd-XL95EVwlwxw'),'LEAVE',anticipated(none),['LEAVE'],[identifier(rodinpos(s2_mch5_signal_actuator,[],'_oed6UzCQEd-6kJpHxFX5oA'),t)],[member(rodinpos(s2_mch5_signal_actuator,grd1,'_oeehYTCQEd-6kJpHxFX5oB'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s2_mch5_signal_actuator,grd2,'_oeehYDCQEd-6kJpHxFX5oA'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,ext_pnt))],[],[assign(rodinpos(s2_mch5_signal_actuator,act1,'_oLA69C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)]))]),assign(rodinpos(s2_mch5_signal_actuator,act2,'_oeehYTCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[domain_subtraction(none,set_extension(none,[identifier(none,t)]),identifier(none,'POS'))])],[]),event(rodinpos(s2_mch5_signal_actuator,'MOVE_IN_PLATFORM','_oLBiAC6wEd-XL95EVwlwxw'),'MOVE_IN_PLATFORM',anticipated(none),['MOVE_IN_PLATFORM'],[identifier(rodinpos(s2_mch5_signal_actuator,[],'_Yh2pATEGEd-pyqeHaVRg2g'),t)],[equal(rodinpos(s2_mch5_signal_actuator,grd1,'_XmsG4jB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed)),member(rodinpos(s2_mch5_signal_actuator,grd2,'_Yh2pAjEGEd-pyqeHaVRg2g'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s2_mch5_signal_actuator,grd3,'_Yh3QEDEGEd-pyqeHaVRg2g'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,ent_pnt)),equal(rodinpos(s2_mch5_signal_actuator,grd4,'_9Z7ZAlOtEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_false(none))],[],[assign(rodinpos(s2_mch5_signal_actuator,act1,'_XmsG4zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,'IN_SWITCH')])),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s2_mch5_signal_actuator,act2,'_XmsG5DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s2_mch5_signal_actuator,act3,'_Yh3QETEGEd-pyqeHaVRg2g'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,'IN_SWITCH')])]))])],[]),event(rodinpos(s2_mch5_signal_actuator,'MOVE_OUT_PLATFORM','_oLBiBC6wEd-XL95EVwlwxw'),'MOVE_OUT_PLATFORM',anticipated(none),['MOVE_OUT_PLATFORM'],[identifier(rodinpos(s2_mch5_signal_actuator,[],'_Yh3QEzEGEd-pyqeHaVRg2g'),t)],[equal(rodinpos(s2_mch5_signal_actuator,grd1,'_Xmst8jB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,allowed)),member(rodinpos(s2_mch5_signal_actuator,grd2,'_Yh3QFDEGEd-pyqeHaVRg2g'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s2_mch5_signal_actuator,grd3,'_Yh3QFTEGEd-pyqeHaVRg2g'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,'OUT_SWITCH')),equal(rodinpos(s2_mch5_signal_actuator,grd4,'_NQysYVYREd-rnu8Rug219Q'),identifier(none,out_signal_act),boolean_false(none))],[],[assign(rodinpos(s2_mch5_signal_actuator,act1,'_Xmst8zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)])),set_extension(none,[identifier(none,'OUT_SWITCH')]))]),assign(rodinpos(s2_mch5_signal_actuator,act2,'_Xmst9DB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s2_mch5_signal_actuator,act3,'_Yh33IDEGEd-pyqeHaVRg2g'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,ext_pnt)])]))])],[]),event(rodinpos(s2_mch5_signal_actuator,'TURN_IN_SWITCH','_bwercU7yEd-P0eLWrKaUUw'),'TURN_IN_SWITCH',anticipated(none),['TURN_IN_SWITCH'],[],[equal(rodinpos(s2_mch5_signal_actuator,grd1,'_XmtVATB6Ed-6kJpHxFX5oA'),identifier(none,in_switch_sig),boolean_true(none))],[],[assign(rodinpos(s2_mch5_signal_actuator,act1,'_Rx5GYS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],[identifier(none,in_switch_act)]),assign(rodinpos(s2_mch5_signal_actuator,act2,'_8YJacFOCEd-_lt3WaRv46A'),[identifier(none,in_switch_sig)],[boolean_false(none)])],[]),event(rodinpos(s2_mch5_signal_actuator,'TURN_OUT_SWITCH','_5TLaUFOSEd-qwcKa_9mK8w'),'TURN_OUT_SWITCH',anticipated(none),['TURN_OUT_SWITCH'],[],[equal(rodinpos(s2_mch5_signal_actuator,grd1,'_uoSvglOTEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_true(none))],[],[assign(rodinpos(s2_mch5_signal_actuator,act1,'_uoSvg1OTEd-qwcKa_9mK8w'),[identifier(none,'OUT_SWITCH')],[identifier(none,out_switch_act)]),assign(rodinpos(s2_mch5_signal_actuator,act2,'_uoSvhFOTEd-qwcKa_9mK8w'),[identifier(none,out_switch_sig)],[boolean_false(none)])],[]),event(rodinpos(s2_mch5_signal_actuator,'ALLOW_ENTRANCE','_oXviA1OUEd-qwcKa_9mK8w'),'ALLOW_ENTRANCE',anticipated(none),['ALLOW_ENTRANCE'],[],[equal(rodinpos(s2_mch5_signal_actuator,grd1,'_oXwJEVOUEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_true(none))],[],[assign(rodinpos(s2_mch5_signal_actuator,act1,'_Xmt8ETB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,allowed)]),assign(rodinpos(s2_mch5_signal_actuator,act2,'_oXwJElOUEd-qwcKa_9mK8w'),[identifier(none,in_signal_act)],[boolean_false(none)])],[]),event(rodinpos(s2_mch5_signal_actuator,'ALLOW_DEPARTURE','_oXwJE1OUEd-qwcKa_9mK8w'),'ALLOW_DEPARTURE',anticipated(none),['ALLOW_DEPARTURE'],[],[equal(rodinpos(s2_mch5_signal_actuator,grd1,'_oXwJFVOUEd-qwcKa_9mK8w'),identifier(none,out_signal_act),boolean_true(none))],[],[assign(rodinpos(s2_mch5_signal_actuator,act1,'_Xmt8FDB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,allowed)]),assign(rodinpos(s2_mch5_signal_actuator,act2,'_oXwJFlOUEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_false(none)])],[]),event(rodinpos(s2_mch5_signal_actuator,trigger_in_switch,'_bweEYk7yEd-P0eLWrKaUUw'),trigger_in_switch,anticipated(none),[trigger_in_switch],[],[equal(rodinpos(s2_mch5_signal_actuator,grd1,'_gcSEgE74Ed-P0eLWrKaUUw'),identifier(none,'ENTRY_SIGNAL'),identifier(none,forbidden)),equal(rodinpos(s2_mch5_signal_actuator,grd2,'_gcSEgk74Ed-P0eLWrKaUUw'),identifier(none,in_switch_sig),boolean_false(none)),equal(rodinpos(s2_mch5_signal_actuator,grd3,'_ofKrcFeAEd-YX5Y88L2F0R'),identifier(none,in_signal_act),boolean_false(none))],[],[becomes_element_of(rodinpos(s2_mch5_signal_actuator,act1,'_bweEY07yEd-P0eLWrKaUUw'),[identifier(none,in_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s2_mch5_signal_actuator,act2,'_bwercE7yEd-P0eLWrKaUUw'),[identifier(none,in_switch_sig)],[boolean_true(none)])],[]),event(rodinpos(s2_mch5_signal_actuator,trigger_out_switch,'_5TMBZFOSEd-qwcKa_9mK8w'),trigger_out_switch,anticipated(none),[trigger_out_switch],[],[equal(rodinpos(s2_mch5_signal_actuator,grd1,'_uoRhYVOTEd-qwcKa_9mK8w'),identifier(none,'EXIT_SIGNAL'),identifier(none,forbidden)),equal(rodinpos(s2_mch5_signal_actuator,grd2,'_uoRhYlOTEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_false(none)),equal(rodinpos(s2_mch5_signal_actuator,grd3,'_ofL5kFeAEd-YX5Y88L2F0R'),identifier(none,out_signal_act),boolean_false(none))],[],[becomes_element_of(rodinpos(s2_mch5_signal_actuator,act1,'_uoRhY1OTEd-qwcKa_9mK8w'),[identifier(none,out_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s2_mch5_signal_actuator,act2,'_uoSIcFOTEd-qwcKa_9mK8w'),[identifier(none,out_switch_sig)],[boolean_true(none)])],[]),event(rodinpos(s2_mch5_signal_actuator,allow_entrance,'_XmtVBDB6Ed-6kJpHxFX5oA'),allow_entrance,anticipated(none),[],[],[equal(rodinpos(s2_mch5_signal_actuator,grd1,'_oXu68VOUEd-qwcKa_9mK8w'),identifier(none,in_signal_act),boolean_false(none)),not_member(rodinpos(s2_mch5_signal_actuator,grd2,'_9Z9OMFOtEd-qwcKa_9mK8w'),identifier(none,'IN_SWITCH'),identifier(none,'OCC')),equal(rodinpos(s2_mch5_signal_actuator,grd3,'__cteMFOvEd-qwcKa_9mK8w'),identifier(none,in_switch_sig),boolean_false(none))],[],[assign(rodinpos(s2_mch5_signal_actuator,act1,'_oXu681OUEd-qwcKa_9mK8w'),[identifier(none,in_signal_act)],[boolean_true(none)])],[]),event(rodinpos(s2_mch5_signal_actuator,allow_departure,'_Xmt8EjB6Ed-6kJpHxFX5oA'),allow_departure,anticipated(none),[],[],[equal(rodinpos(s2_mch5_signal_actuator,grd1,'_oXviAFOUEd-qwcKa_9mK8w'),identifier(none,out_signal_act),boolean_false(none)),not_member(rodinpos(s2_mch5_signal_actuator,grd2,'_9Z91QFOtEd-qwcKa_9mK8w'),identifier(none,ext_pnt),identifier(none,'OCC')),equal(rodinpos(s2_mch5_signal_actuator,grd3,'__cuFQFOvEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_false(none))],[],[assign(rodinpos(s2_mch5_signal_actuator,act1,'_oXviAlOUEd-qwcKa_9mK8w'),[identifier(none,out_signal_act)],[boolean_true(none)])],[])])]),event_b_model(none,s2_mch4_switch_actuator,[sees(none,[s1_ctx0_blocks,s1_ctx1_blocks,s1_ctx2_signal,s1_ctx3_trains]),refines(none,s1_mch3_trains),variables(none,[identifier(none,'ENTRY_SIGNAL'),identifier(none,'EXIT_SIGNAL'),identifier(none,'IN_SWITCH'),identifier(none,'OCC'),identifier(none,'OUT_SWITCH'),identifier(none,'POS'),identifier(none,in_switch_act),identifier(none,in_switch_sig),identifier(none,out_switch_act),identifier(none,out_switch_sig)]),invariant(none,[subset(rodinpos(s2_mch4_switch_actuator,inv1,'_oK_Fwy6wEd-XL95EVwlwxw'),identifier(none,'OCC'),identifier(none,'BLOCK')),member(rodinpos(s2_mch4_switch_actuator,inv1,'_Rx3RMC68Ed-0PKStM0XZhg'),identifier(none,'IN_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s2_mch4_switch_actuator,inv2,'_Rx34QC68Ed-0PKStM0XZhg'),identifier(none,'OUT_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s2_mch4_switch_actuator,inv1,'_XmqRsjB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,'ACCESS')),member(rodinpos(s2_mch4_switch_actuator,inv2,'_XmqRszB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,'ACCESS')),disjunct(rodinpos(s2_mch4_switch_actuator,inv3,'_Xmq4wDB6Ed-6kJpHxFX5oA'),not_equal(none,identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed)),not_member(none,identifier(none,'IN_SWITCH'),identifier(none,'OCC'))),disjunct(rodinpos(s2_mch4_switch_actuator,inv4,'_Xmq4wTB6Ed-6kJpHxFX5oA'),not_equal(none,identifier(none,'EXIT_SIGNAL'),identifier(none,allowed)),not_member(none,identifier(none,ext_pnt),identifier(none,'OCC'))),member(rodinpos(s2_mch4_switch_actuator,inv1,'_bwbBEk7yEd-P0eLWrKaUUw'),identifier(none,in_switch_act),identifier(none,'PLATFORM')),member(rodinpos(s2_mch4_switch_actuator,inv2,'_uoN3AVOTEd-qwcKa_9mK8w'),identifier(none,out_switch_act),identifier(none,'PLATFORM')),implication(rodinpos(s2_mch4_switch_actuator,inv3,'_8YCswFOCEd-_lt3WaRv46A'),equal(none,identifier(none,in_switch_sig),boolean_true(none)),equal(none,identifier(none,'ENTRY_SIGNAL'),identifier(none,forbidden))),implication(rodinpos(s2_mch4_switch_actuator,inv4,'_uoN3AlOTEd-qwcKa_9mK8w'),equal(none,identifier(none,out_switch_sig),boolean_true(none)),equal(none,identifier(none,'EXIT_SIGNAL'),identifier(none,forbidden)))]),theorems(none,[]),events(none,[event(rodinpos(s2_mch4_switch_actuator,'INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(s2_mch4_switch_actuator,act1,'_oLAT4C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[empty_set(none)]),becomes_element_of(rodinpos(s2_mch4_switch_actuator,act2,'_Rx34QS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],identifier(none,'PLATFORM')),becomes_element_of(rodinpos(s2_mch4_switch_actuator,act3,'_Rx34Qi68Ed-0PKStM0XZhg'),[identifier(none,'OUT_SWITCH')],identifier(none,'PLATFORM')),assign(rodinpos(s2_mch4_switch_actuator,act4,'_Xmrf0DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s2_mch4_switch_actuator,act5,'_Xmrf0TB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s2_mch4_switch_actuator,act6,'_oedTQDCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[empty_set(none)]),becomes_element_of(rodinpos(s2_mch4_switch_actuator,act7,'_Rs-R4FYTEd-rnu8Rug219Q'),[identifier(none,in_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s2_mch4_switch_actuator,act8,'_oedTQDCQEd-6kJpHxFX5oA'),[identifier(none,in_switch_sig)],[boolean_false(none)]),becomes_element_of(rodinpos(s2_mch4_switch_actuator,act9,'_gcPBME74Ed-P0eLWrKaUUw'),[identifier(none,out_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s2_mch4_switch_actuator,act10,'_gcPBMU74Ed-P0eLWrKaUUw'),[identifier(none,out_switch_sig)],[boolean_false(none)])],[]),event(rodinpos(s2_mch4_switch_actuator,'ARRIVE','_oLAT4i6wEd-XL95EVwlwxw'),'ARRIVE',anticipated(none),['ARRIVE'],[identifier(rodinpos(s2_mch4_switch_actuator,[],'_oedTQjCQEd-6kJpHxFX5oA'),t)],[not_member(rodinpos(s2_mch4_switch_actuator,grd1,'_oLAT4y6wEd-XL95EVwlwxw'),identifier(none,ent_pnt),identifier(none,'OCC')),not_member(rodinpos(s2_mch4_switch_actuator,grd2,'_oed6UDCQEd-6kJpHxFX5oA'),identifier(none,t),domain(none,identifier(none,'POS')))],[],[assign(rodinpos(s2_mch4_switch_actuator,act1,'_oLA68C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s2_mch4_switch_actuator,act3,'_oed6UTCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,ent_pnt)])]))])],[]),event(rodinpos(s2_mch4_switch_actuator,'LEAVE','_oLA68i6wEd-XL95EVwlwxw'),'LEAVE',anticipated(none),['LEAVE'],[identifier(rodinpos(s2_mch4_switch_actuator,[],'_oed6UzCQEd-6kJpHxFX5oA'),t)],[member(rodinpos(s2_mch4_switch_actuator,grd1,'_oeehYTCQEd-6kJpHxFX5oB'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s2_mch4_switch_actuator,grd2,'_oeehYDCQEd-6kJpHxFX5oA'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,ext_pnt))],[],[assign(rodinpos(s2_mch4_switch_actuator,act1,'_oLA69C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)]))]),assign(rodinpos(s2_mch4_switch_actuator,act2,'_oeehYTCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[domain_subtraction(none,set_extension(none,[identifier(none,t)]),identifier(none,'POS'))])],[]),event(rodinpos(s2_mch4_switch_actuator,'MOVE_IN_PLATFORM','_oLBiAC6wEd-XL95EVwlwxw'),'MOVE_IN_PLATFORM',anticipated(none),['MOVE_IN_PLATFORM'],[identifier(rodinpos(s2_mch4_switch_actuator,[],'_Yh2pATEGEd-pyqeHaVRg2g'),t)],[equal(rodinpos(s2_mch4_switch_actuator,grd1,'_XmsG4jB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed)),member(rodinpos(s2_mch4_switch_actuator,grd2,'_Yh2pAjEGEd-pyqeHaVRg2g'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s2_mch4_switch_actuator,grd3,'_Yh3QEDEGEd-pyqeHaVRg2g'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,ent_pnt))],[],[assign(rodinpos(s2_mch4_switch_actuator,act1,'_XmsG4zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,'IN_SWITCH')])),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s2_mch4_switch_actuator,act2,'_XmsG5DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s2_mch4_switch_actuator,act3,'_Yh3QETEGEd-pyqeHaVRg2g'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,'IN_SWITCH')])]))])],[]),event(rodinpos(s2_mch4_switch_actuator,'MOVE_OUT_PLATFORM','_oLBiBC6wEd-XL95EVwlwxw'),'MOVE_OUT_PLATFORM',anticipated(none),['MOVE_OUT_PLATFORM'],[identifier(rodinpos(s2_mch4_switch_actuator,[],'_Yh3QEzEGEd-pyqeHaVRg2g'),t)],[equal(rodinpos(s2_mch4_switch_actuator,grd1,'_Xmst8jB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,allowed)),member(rodinpos(s2_mch4_switch_actuator,grd2,'_Yh3QFDEGEd-pyqeHaVRg2g'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s2_mch4_switch_actuator,grd3,'_Yh3QFTEGEd-pyqeHaVRg2g'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,'OUT_SWITCH'))],[],[assign(rodinpos(s2_mch4_switch_actuator,act1,'_Xmst8zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)])),set_extension(none,[identifier(none,'OUT_SWITCH')]))]),assign(rodinpos(s2_mch4_switch_actuator,act2,'_Xmst9DB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s2_mch4_switch_actuator,act3,'_Yh33IDEGEd-pyqeHaVRg2g'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,ext_pnt)])]))])],[]),event(rodinpos(s2_mch4_switch_actuator,'TURN_IN_SWITCH','_bwercU7yEd-P0eLWrKaUUw'),'TURN_IN_SWITCH',anticipated(none),['TURN_IN_SWITCH'],[],[equal(rodinpos(s2_mch4_switch_actuator,grd1,'_XmtVATB6Ed-6kJpHxFX5oA'),identifier(none,in_switch_sig),boolean_true(none))],[],[assign(rodinpos(s2_mch4_switch_actuator,act1,'_Rx5GYS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],[identifier(none,in_switch_act)]),assign(rodinpos(s2_mch4_switch_actuator,act2,'_8YJacFOCEd-_lt3WaRv46A'),[identifier(none,in_switch_sig)],[boolean_false(none)])],[]),event(rodinpos(s2_mch4_switch_actuator,'TURN_OUT_SWITCH','_uoSvgFOTEd-qwcKa_9mK8w'),'TURN_OUT_SWITCH',anticipated(none),['TURN_OUT_SWITCH'],[],[equal(rodinpos(s2_mch4_switch_actuator,grd1,'_uoSvglOTEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_true(none))],[],[assign(rodinpos(s2_mch4_switch_actuator,act1,'_uoSvg1OTEd-qwcKa_9mK8w'),[identifier(none,'OUT_SWITCH')],[identifier(none,out_switch_act)]),assign(rodinpos(s2_mch4_switch_actuator,act2,'_uoSvhFOTEd-qwcKa_9mK8w'),[identifier(none,out_switch_sig)],[boolean_false(none)])],[]),event(rodinpos(s2_mch4_switch_actuator,'ALLOW_ENTRANCE','_XmtVBDB6Ed-6kJpHxFX5oA'),'ALLOW_ENTRANCE',anticipated(none),['ALLOW_ENTRANCE'],[],[not_member(rodinpos(s2_mch4_switch_actuator,grd1,'_Xmt8EDB6Ed-6kJpHxFX5oA'),identifier(none,'IN_SWITCH'),identifier(none,'OCC')),equal(rodinpos(s2_mch4_switch_actuator,grd2,'_uoTWkVOTEd-qwcKa_9mK8w'),identifier(none,in_switch_sig),boolean_false(none))],[],[assign(rodinpos(s2_mch4_switch_actuator,act1,'_Xmt8ETB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,allowed)])],[]),event(rodinpos(s2_mch4_switch_actuator,'ALLOW_DEPARTURE','_Xmt8EjB6Ed-6kJpHxFX5oA'),'ALLOW_DEPARTURE',anticipated(none),['ALLOW_DEPARTURE'],[],[not_member(rodinpos(s2_mch4_switch_actuator,grd1,'_Xmt8EzB6Ed-6kJpHxFX5oA'),identifier(none,ext_pnt),identifier(none,'OCC')),equal(rodinpos(s2_mch4_switch_actuator,grd2,'_uoTWk1OTEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_false(none))],[],[assign(rodinpos(s2_mch4_switch_actuator,act1,'_Xmt8FDB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,allowed)])],[]),event(rodinpos(s2_mch4_switch_actuator,trigger_in_switch,'_bweEYk7yEd-P0eLWrKaUUw'),trigger_in_switch,anticipated(none),[],[],[equal(rodinpos(s2_mch4_switch_actuator,grd1,'_gcSEgE74Ed-P0eLWrKaUUw'),identifier(none,'ENTRY_SIGNAL'),identifier(none,forbidden)),equal(rodinpos(s2_mch4_switch_actuator,grd2,'_gcSEgk74Ed-P0eLWrKaUUw'),identifier(none,in_switch_sig),boolean_false(none))],[],[becomes_element_of(rodinpos(s2_mch4_switch_actuator,act1,'_bweEY07yEd-P0eLWrKaUUw'),[identifier(none,in_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s2_mch4_switch_actuator,act2,'_bwercE7yEd-P0eLWrKaUUw'),[identifier(none,in_switch_sig)],[boolean_true(none)])],[]),event(rodinpos(s2_mch4_switch_actuator,trigger_out_switch,'_uoRhYFOTEd-qwcKa_9mK8w'),trigger_out_switch,anticipated(none),[],[],[equal(rodinpos(s2_mch4_switch_actuator,grd1,'_uoRhYVOTEd-qwcKa_9mK8w'),identifier(none,'EXIT_SIGNAL'),identifier(none,forbidden)),equal(rodinpos(s2_mch4_switch_actuator,grd2,'_uoRhYlOTEd-qwcKa_9mK8w'),identifier(none,out_switch_sig),boolean_false(none))],[],[becomes_element_of(rodinpos(s2_mch4_switch_actuator,act1,'_uoRhY1OTEd-qwcKa_9mK8w'),[identifier(none,out_switch_act)],identifier(none,'PLATFORM')),assign(rodinpos(s2_mch4_switch_actuator,act2,'_uoSIcFOTEd-qwcKa_9mK8w'),[identifier(none,out_switch_sig)],[boolean_true(none)])],[])])]),event_b_model(none,s1_mch3_trains,[sees(none,[s1_ctx0_blocks,s1_ctx1_blocks,s1_ctx2_signal,s1_ctx3_trains]),refines(none,s1_mch2_signals),variables(none,[identifier(none,'ENTRY_SIGNAL'),identifier(none,'EXIT_SIGNAL'),identifier(none,'IN_SWITCH'),identifier(none,'OCC'),identifier(none,'OUT_SWITCH'),identifier(none,'POS')]),invariant(none,[subset(rodinpos(s1_mch3_trains,inv1,'_oK_Fwy6wEd-XL95EVwlwxw'),identifier(none,'OCC'),identifier(none,'BLOCK')),member(rodinpos(s1_mch3_trains,inv1,'_Rx3RMC68Ed-0PKStM0XZhg'),identifier(none,'IN_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s1_mch3_trains,inv2,'_Rx34QC68Ed-0PKStM0XZhg'),identifier(none,'OUT_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s1_mch3_trains,inv1,'_oecFITCQEd-6kJpHxFX5oA'),identifier(none,'POS'),partial_function(none,identifier(none,'TRAIN'),identifier(none,'BLOCK'))),equal(rodinpos(s1_mch3_trains,inv2,'_oecsMTCQEd-6kJpHxFX5oA'),range(none,identifier(none,'POS')),identifier(none,'OCC')),forall(rodinpos(s1_mch3_trains,inv3,'_oecsMjCQEd-6kJpHxFX5oA'),[identifier(none,t1),identifier(none,t2)],implication(none,conjunct(none,member(none,identifier(none,t1),domain(none,identifier(none,'POS'))),conjunct(none,member(none,identifier(none,t2),domain(none,identifier(none,'POS'))),equal(none,function(none,identifier(none,'POS'),[identifier(none,t1)]),function(none,identifier(none,'POS'),[identifier(none,t2)])))),equal(none,identifier(none,t1),identifier(none,t2))))]),theorems(none,[member(rodinpos(s1_mch3_trains,thm4,'_Yh0z0DEGEd-pyqeHaVRg2g'),identifier(none,'POS'),partial_injection(none,identifier(none,'TRAIN'),identifier(none,'BLOCK')))]),events(none,[event(rodinpos(s1_mch3_trains,'INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(s1_mch3_trains,act1,'_oLAT4C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[empty_set(none)]),becomes_element_of(rodinpos(s1_mch3_trains,act2,'_Rx34QS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],identifier(none,'PLATFORM')),becomes_element_of(rodinpos(s1_mch3_trains,act3,'_Rx34Qi68Ed-0PKStM0XZhg'),[identifier(none,'OUT_SWITCH')],identifier(none,'PLATFORM')),assign(rodinpos(s1_mch3_trains,act4,'_Xmrf0DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s1_mch3_trains,act5,'_Xmrf0TB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s1_mch3_trains,act6,'_oedTQDCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[empty_set(none)])],[]),event(rodinpos(s1_mch3_trains,'ARRIVE','_oLAT4i6wEd-XL95EVwlwxw'),'ARRIVE',anticipated(none),['ARRIVE'],[identifier(rodinpos(s1_mch3_trains,[],'_oedTQjCQEd-6kJpHxFX5oA'),t)],[not_member(rodinpos(s1_mch3_trains,grd1,'_oLAT4y6wEd-XL95EVwlwxw'),identifier(none,ent_pnt),identifier(none,'OCC')),not_member(rodinpos(s1_mch3_trains,grd2,'_oed6UDCQEd-6kJpHxFX5oA'),identifier(none,t),domain(none,identifier(none,'POS')))],[],[assign(rodinpos(s1_mch3_trains,act1,'_oLA68C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s1_mch3_trains,act3,'_oed6UTCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,ent_pnt)])]))])],[]),event(rodinpos(s1_mch3_trains,'LEAVE','_oLA68i6wEd-XL95EVwlwxw'),'LEAVE',anticipated(none),['LEAVE'],[identifier(rodinpos(s1_mch3_trains,[],'_oed6UzCQEd-6kJpHxFX5oA'),t)],[member(rodinpos(s1_mch3_trains,grd1,'_oeehYTCQEd-6kJpHxFX5oB'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s1_mch3_trains,grd2,'_oeehYDCQEd-6kJpHxFX5oA'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,ext_pnt))],[],[assign(rodinpos(s1_mch3_trains,act1,'_oLA69C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)]))]),assign(rodinpos(s1_mch3_trains,act2,'_oeehYTCQEd-6kJpHxFX5oA'),[identifier(none,'POS')],[domain_subtraction(none,set_extension(none,[identifier(none,t)]),identifier(none,'POS'))])],[]),event(rodinpos(s1_mch3_trains,'MOVE_IN_PLATFORM','_oLBiAC6wEd-XL95EVwlwxw'),'MOVE_IN_PLATFORM',anticipated(none),['MOVE_IN_PLATFORM'],[identifier(rodinpos(s1_mch3_trains,[],'_Yh2pATEGEd-pyqeHaVRg2g'),t)],[equal(rodinpos(s1_mch3_trains,grd1,'_XmsG4jB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed)),member(rodinpos(s1_mch3_trains,grd2,'_Yh2pAjEGEd-pyqeHaVRg2g'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s1_mch3_trains,grd3,'_Yh3QEDEGEd-pyqeHaVRg2g'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,ent_pnt))],[],[assign(rodinpos(s1_mch3_trains,act1,'_XmsG4zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,'IN_SWITCH')])),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s1_mch3_trains,act2,'_XmsG5DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s1_mch3_trains,act3,'_Yh3QETEGEd-pyqeHaVRg2g'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,'IN_SWITCH')])]))])],[]),event(rodinpos(s1_mch3_trains,'MOVE_OUT_PLATFORM','_oLBiBC6wEd-XL95EVwlwxw'),'MOVE_OUT_PLATFORM',anticipated(none),['MOVE_OUT_PLATFORM'],[identifier(rodinpos(s1_mch3_trains,[],'_Yh3QEzEGEd-pyqeHaVRg2g'),t)],[equal(rodinpos(s1_mch3_trains,grd1,'_Xmst8jB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,allowed)),member(rodinpos(s1_mch3_trains,grd2,'_Yh3QFDEGEd-pyqeHaVRg2g'),identifier(none,t),domain(none,identifier(none,'POS'))),equal(rodinpos(s1_mch3_trains,grd3,'_Yh3QFTEGEd-pyqeHaVRg2g'),function(none,identifier(none,'POS'),[identifier(none,t)]),identifier(none,'OUT_SWITCH'))],[],[assign(rodinpos(s1_mch3_trains,act1,'_Xmst8zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)])),set_extension(none,[identifier(none,'OUT_SWITCH')]))]),assign(rodinpos(s1_mch3_trains,act2,'_Xmst9DB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s1_mch3_trains,act3,'_Yh33IDEGEd-pyqeHaVRg2g'),[identifier(none,'POS')],[overwrite(none,identifier(none,'POS'),set_extension(none,[couple(none,[identifier(none,t),identifier(none,ext_pnt)])]))])],[]),event(rodinpos(s1_mch3_trains,'TURN_IN_SWITCH','_Rx5GYC68Ed-0PKStM0XZhg'),'TURN_IN_SWITCH',anticipated(none),['TURN_IN_SWITCH'],[],[equal(rodinpos(s1_mch3_trains,grd1,'_XmtVATB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,forbidden))],[],[becomes_element_of(rodinpos(s1_mch3_trains,act1,'_Rx5GYS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],identifier(none,'PLATFORM'))],[]),event(rodinpos(s1_mch3_trains,'TURN_OUT_SWITCH','_Rx5GYi68Ed-0PKStM0XZhg'),'TURN_OUT_SWITCH',anticipated(none),['TURN_OUT_SWITCH'],[],[equal(rodinpos(s1_mch3_trains,grd1,'_XmtVAzB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,forbidden))],[],[becomes_element_of(rodinpos(s1_mch3_trains,act1,'_Rx5GYy68Ed-0PKStM0XZhg'),[identifier(none,'OUT_SWITCH')],identifier(none,'PLATFORM'))],[]),event(rodinpos(s1_mch3_trains,'ALLOW_ENTRANCE','_XmtVBDB6Ed-6kJpHxFX5oA'),'ALLOW_ENTRANCE',anticipated(none),['ALLOW_ENTRANCE'],[],[not_member(rodinpos(s1_mch3_trains,grd1,'_Xmt8EDB6Ed-6kJpHxFX5oA'),identifier(none,'IN_SWITCH'),identifier(none,'OCC'))],[],[assign(rodinpos(s1_mch3_trains,act1,'_Xmt8ETB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,allowed)])],[]),event(rodinpos(s1_mch3_trains,'ALLOW_DEPARTURE','_Xmt8EjB6Ed-6kJpHxFX5oA'),'ALLOW_DEPARTURE',anticipated(none),['ALLOW_DEPARTURE'],[],[not_member(rodinpos(s1_mch3_trains,grd1,'_Xmt8EzB6Ed-6kJpHxFX5oA'),identifier(none,ext_pnt),identifier(none,'OCC'))],[],[assign(rodinpos(s1_mch3_trains,act1,'_Xmt8FDB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,allowed)])],[])])]),event_b_model(none,s1_mch2_signals,[sees(none,[s1_ctx0_blocks,s1_ctx1_blocks,s1_ctx2_signal]),refines(none,s1_mch1_switches),variables(none,[identifier(none,'ENTRY_SIGNAL'),identifier(none,'EXIT_SIGNAL'),identifier(none,'IN_SWITCH'),identifier(none,'OCC'),identifier(none,'OUT_SWITCH')]),invariant(none,[subset(rodinpos(s1_mch2_signals,inv1,'_oK_Fwy6wEd-XL95EVwlwxw'),identifier(none,'OCC'),identifier(none,'BLOCK')),member(rodinpos(s1_mch2_signals,inv1,'_XmqRsjB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,'ACCESS')),member(rodinpos(s1_mch2_signals,inv2,'_XmqRszB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,'ACCESS')),disjunct(rodinpos(s1_mch2_signals,inv3,'_Xmq4wDB6Ed-6kJpHxFX5oA'),not_equal(none,identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed)),not_member(none,identifier(none,'IN_SWITCH'),identifier(none,'OCC'))),disjunct(rodinpos(s1_mch2_signals,inv4,'_Xmq4wTB6Ed-6kJpHxFX5oA'),not_equal(none,identifier(none,'EXIT_SIGNAL'),identifier(none,allowed)),not_member(none,identifier(none,ext_pnt),identifier(none,'OCC')))]),theorems(none,[]),events(none,[event(rodinpos(s1_mch2_signals,'INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(s1_mch2_signals,act1,'_oLAT4C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[empty_set(none)]),becomes_element_of(rodinpos(s1_mch2_signals,act2,'_Rx34QS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],identifier(none,'PLATFORM')),becomes_element_of(rodinpos(s1_mch2_signals,act3,'_Rx34Qi68Ed-0PKStM0XZhg'),[identifier(none,'OUT_SWITCH')],identifier(none,'PLATFORM')),assign(rodinpos(s1_mch2_signals,act4,'_Xmrf0DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)]),assign(rodinpos(s1_mch2_signals,act5,'_Xmrf0TB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)])],[]),event(rodinpos(s1_mch2_signals,'ARRIVE','_oLAT4i6wEd-XL95EVwlwxw'),'ARRIVE',anticipated(none),['ARRIVE'],[],[not_member(rodinpos(s1_mch2_signals,grd1,'_oLAT4y6wEd-XL95EVwlwxw'),identifier(none,ent_pnt),identifier(none,'OCC'))],[],[assign(rodinpos(s1_mch2_signals,act1,'_oLA68C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ent_pnt)]))])],[]),event(rodinpos(s1_mch2_signals,'LEAVE','_oLA68i6wEd-XL95EVwlwxw'),'LEAVE',anticipated(none),['LEAVE'],[],[member(rodinpos(s1_mch2_signals,grd1,'_oLA68y6wEd-XL95EVwlwxw'),identifier(none,ext_pnt),identifier(none,'OCC'))],[],[assign(rodinpos(s1_mch2_signals,act1,'_oLA69C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)]))])],[]),event(rodinpos(s1_mch2_signals,'MOVE_IN_PLATFORM','_oLBiAC6wEd-XL95EVwlwxw'),'MOVE_IN_PLATFORM',anticipated(none),['MOVE_IN_PLATFORM'],[],[member(rodinpos(s1_mch2_signals,grd1,'_XmsG4TB6Ed-6kJpHxFX5oA'),identifier(none,ent_pnt),identifier(none,'OCC')),equal(rodinpos(s1_mch2_signals,grd2,'_XmsG4jB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,allowed))],[],[assign(rodinpos(s1_mch2_signals,act1,'_XmsG4zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,'IN_SWITCH')])),set_extension(none,[identifier(none,ent_pnt)]))]),assign(rodinpos(s1_mch2_signals,act2,'_XmsG5DB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,forbidden)])],[]),event(rodinpos(s1_mch2_signals,'MOVE_OUT_PLATFORM','_oLBiBC6wEd-XL95EVwlwxw'),'MOVE_OUT_PLATFORM',anticipated(none),['MOVE_OUT_PLATFORM'],[],[member(rodinpos(s1_mch2_signals,grd1,'_Xmst8TB6Ed-6kJpHxFX5oA'),identifier(none,'OUT_SWITCH'),identifier(none,'OCC')),equal(rodinpos(s1_mch2_signals,grd2,'_Xmst8jB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,allowed))],[],[assign(rodinpos(s1_mch2_signals,act1,'_Xmst8zB6Ed-6kJpHxFX5oA'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)])),set_extension(none,[identifier(none,'OUT_SWITCH')]))]),assign(rodinpos(s1_mch2_signals,act2,'_Xmst9DB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,forbidden)])],[]),event(rodinpos(s1_mch2_signals,'TURN_IN_SWITCH','_Rx5GYC68Ed-0PKStM0XZhg'),'TURN_IN_SWITCH',anticipated(none),['TURN_IN_SWITCH'],[],[equal(rodinpos(s1_mch2_signals,grd1,'_XmtVATB6Ed-6kJpHxFX5oA'),identifier(none,'ENTRY_SIGNAL'),identifier(none,forbidden))],[],[becomes_element_of(rodinpos(s1_mch2_signals,act1,'_Rx5GYS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],identifier(none,'PLATFORM'))],[]),event(rodinpos(s1_mch2_signals,'TURN_OUT_SWITCH','_Rx5GYi68Ed-0PKStM0XZhg'),'TURN_OUT_SWITCH',anticipated(none),['TURN_OUT_SWITCH'],[],[equal(rodinpos(s1_mch2_signals,grd1,'_XmtVAzB6Ed-6kJpHxFX5oA'),identifier(none,'EXIT_SIGNAL'),identifier(none,forbidden))],[],[becomes_element_of(rodinpos(s1_mch2_signals,act1,'_Rx5GYy68Ed-0PKStM0XZhg'),[identifier(none,'OUT_SWITCH')],identifier(none,'PLATFORM'))],[]),event(rodinpos(s1_mch2_signals,'ALLOW_ENTRANCE','_XmtVBDB6Ed-6kJpHxFX5oA'),'ALLOW_ENTRANCE',anticipated(none),[],[],[not_member(rodinpos(s1_mch2_signals,grd1,'_Xmt8EDB6Ed-6kJpHxFX5oA'),identifier(none,'IN_SWITCH'),identifier(none,'OCC'))],[],[assign(rodinpos(s1_mch2_signals,act1,'_Xmt8ETB6Ed-6kJpHxFX5oA'),[identifier(none,'ENTRY_SIGNAL')],[identifier(none,allowed)])],[]),event(rodinpos(s1_mch2_signals,'ALLOW_DEPARTURE','_Xmt8EjB6Ed-6kJpHxFX5oA'),'ALLOW_DEPARTURE',anticipated(none),[],[],[not_member(rodinpos(s1_mch2_signals,grd1,'_Xmt8EzB6Ed-6kJpHxFX5oA'),identifier(none,ext_pnt),identifier(none,'OCC'))],[],[assign(rodinpos(s1_mch2_signals,act1,'_Xmt8FDB6Ed-6kJpHxFX5oA'),[identifier(none,'EXIT_SIGNAL')],[identifier(none,allowed)])],[])])]),event_b_model(none,s1_mch1_switches,[sees(none,[s1_ctx0_blocks,s1_ctx1_blocks]),refines(none,s1_mch0_blocks),variables(none,[identifier(none,'IN_SWITCH'),identifier(none,'OCC'),identifier(none,'OUT_SWITCH')]),invariant(none,[member(rodinpos(s1_mch1_switches,inv1,'_Rx3RMC68Ed-0PKStM0XZhg'),identifier(none,'IN_SWITCH'),identifier(none,'PLATFORM')),member(rodinpos(s1_mch1_switches,inv2,'_Rx34QC68Ed-0PKStM0XZhg'),identifier(none,'OUT_SWITCH'),identifier(none,'PLATFORM'))]),theorems(none,[]),events(none,[event(rodinpos(s1_mch1_switches,'INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(s1_mch1_switches,act1,'_oLAT4C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[empty_set(none)]),becomes_element_of(rodinpos(s1_mch1_switches,act2,'_Rx34QS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],identifier(none,'PLATFORM')),becomes_element_of(rodinpos(s1_mch1_switches,act3,'_Rx34Qi68Ed-0PKStM0XZhg'),[identifier(none,'OUT_SWITCH')],identifier(none,'PLATFORM'))],[]),event(rodinpos(s1_mch1_switches,'ARRIVE','_oLAT4i6wEd-XL95EVwlwxw'),'ARRIVE',anticipated(none),['ARRIVE'],[],[not_member(rodinpos(s1_mch1_switches,grd1,'_oLAT4y6wEd-XL95EVwlwxw'),identifier(none,ent_pnt),identifier(none,'OCC'))],[],[assign(rodinpos(s1_mch1_switches,act1,'_oLA68C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ent_pnt)]))])],[]),event(rodinpos(s1_mch1_switches,'LEAVE','_oLA68i6wEd-XL95EVwlwxw'),'LEAVE',anticipated(none),['LEAVE'],[],[member(rodinpos(s1_mch1_switches,grd1,'_oLA68y6wEd-XL95EVwlwxw'),identifier(none,ext_pnt),identifier(none,'OCC'))],[],[assign(rodinpos(s1_mch1_switches,act1,'_oLA69C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)]))])],[]),event(rodinpos(s1_mch1_switches,'MOVE_IN_PLATFORM','_oLBiAC6wEd-XL95EVwlwxw'),'MOVE_IN_PLATFORM',anticipated(none),['MOVE_IN_PLATFORM'],[],[member(rodinpos(s1_mch1_switches,grd1,'_Ept98C62Ed-0PKStM0XZhg'),identifier(none,ent_pnt),identifier(none,'OCC')),not_member(rodinpos(s1_mch1_switches,grd2,'_ftXP0S7JEd-ybNjevNaONQ'),identifier(none,'IN_SWITCH'),identifier(none,'OCC'))],[],[assign(rodinpos(s1_mch1_switches,act1,'_oLBiAy6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,'IN_SWITCH')])),set_extension(none,[identifier(none,ent_pnt)]))])],[witness(none,identifier(none,p),equal(rodinpos(s1_mch1_switches,p,'_Rx4fUi68Ed-0PKStM0XZhg'),identifier(none,p),identifier(none,'IN_SWITCH')))]),event(rodinpos(s1_mch1_switches,'MOVE_OUT_PLATFORM','_oLBiBC6wEd-XL95EVwlwxw'),'MOVE_OUT_PLATFORM',anticipated(none),['MOVE_OUT_PLATFORM'],[],[member(rodinpos(s1_mch1_switches,grd1,'_EpulAS62Ed-0PKStM0XZhg'),identifier(none,'OUT_SWITCH'),identifier(none,'OCC')),not_member(rodinpos(s1_mch1_switches,grd2,'_ftX24S7JEd-ybNjevNaONQ'),identifier(none,ext_pnt),identifier(none,'OCC'))],[],[assign(rodinpos(s1_mch1_switches,act1,'_oLCJEC6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)])),set_extension(none,[identifier(none,'OUT_SWITCH')]))])],[witness(none,identifier(none,p),equal(rodinpos(s1_mch1_switches,p,'_Rx4fVC68Ed-0PKStM0XZhg'),identifier(none,p),identifier(none,'OUT_SWITCH')))]),event(rodinpos(s1_mch1_switches,'TURN_IN_SWITCH','_Rx5GYC68Ed-0PKStM0XZhg'),'TURN_IN_SWITCH',anticipated(none),[],[],[],[],[becomes_element_of(rodinpos(s1_mch1_switches,act1,'_Rx5GYS68Ed-0PKStM0XZhg'),[identifier(none,'IN_SWITCH')],identifier(none,'PLATFORM'))],[]),event(rodinpos(s1_mch1_switches,'TURN_OUT_SWITCH','_Rx5GYi68Ed-0PKStM0XZhg'),'TURN_OUT_SWITCH',anticipated(none),[],[],[],[],[becomes_element_of(rodinpos(s1_mch1_switches,act1,'_Rx5GYy68Ed-0PKStM0XZhg'),[identifier(none,'OUT_SWITCH')],identifier(none,'PLATFORM'))],[])])]),event_b_model(none,s1_mch0_blocks,[sees(none,[s1_ctx0_blocks]),variables(none,[identifier(none,'OCC')]),invariant(none,[subset(rodinpos(s1_mch0_blocks,inv1,'_oK_Fwy6wEd-XL95EVwlwxw'),identifier(none,'OCC'),identifier(none,'BLOCK'))]),theorems(none,[]),events(none,[event(rodinpos(s1_mch0_blocks,'INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(s1_mch0_blocks,act1,'_oLAT4C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[empty_set(none)])],[]),event(rodinpos(s1_mch0_blocks,'ARRIVE','_oLAT4i6wEd-XL95EVwlwxw'),'ARRIVE',anticipated(none),[],[],[not_member(rodinpos(s1_mch0_blocks,grd1,'_oLAT4y6wEd-XL95EVwlwxw'),identifier(none,ent_pnt),identifier(none,'OCC'))],[],[assign(rodinpos(s1_mch0_blocks,act1,'_oLA68C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ent_pnt)]))])],[]),event(rodinpos(s1_mch0_blocks,'LEAVE','_oLA68i6wEd-XL95EVwlwxw'),'LEAVE',anticipated(none),[],[],[member(rodinpos(s1_mch0_blocks,grd1,'_oLA68y6wEd-XL95EVwlwxw'),identifier(none,ext_pnt),identifier(none,'OCC'))],[],[assign(rodinpos(s1_mch0_blocks,act1,'_oLA69C6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)]))])],[]),event(rodinpos(s1_mch0_blocks,'MOVE_IN_PLATFORM','_oLBiAC6wEd-XL95EVwlwxw'),'MOVE_IN_PLATFORM',anticipated(none),[],[identifier(rodinpos(s1_mch0_blocks,[],'_oLBiAS6wEd-XL95EVwlwxw'),p)],[member(rodinpos(s1_mch0_blocks,grd1,'_Ept98C62Ed-0PKStM0XZhg'),identifier(none,ent_pnt),identifier(none,'OCC')),member(rodinpos(s1_mch0_blocks,grd2,'_Ept98S62Ed-0PKStM0XZhg'),identifier(none,p),set_subtraction(none,identifier(none,'PLATFORM'),identifier(none,'OCC')))],[],[assign(rodinpos(s1_mch0_blocks,act1,'_oLBiAy6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,p)])),set_extension(none,[identifier(none,ent_pnt)]))])],[]),event(rodinpos(s1_mch0_blocks,'MOVE_OUT_PLATFORM','_oLBiBC6wEd-XL95EVwlwxw'),'MOVE_OUT_PLATFORM',anticipated(none),[],[identifier(rodinpos(s1_mch0_blocks,[],'_oLBiBS6wEd-XL95EVwlwxw'),p)],[member(rodinpos(s1_mch0_blocks,grd1,'_EpulAC62Ed-0PKStM0XZhg'),identifier(none,p),identifier(none,'OCC')),not_member(rodinpos(s1_mch0_blocks,grd2,'_EpulAS62Ed-0PKStM0XZhg'),identifier(none,ext_pnt),identifier(none,'OCC'))],[],[assign(rodinpos(s1_mch0_blocks,act1,'_oLCJEC6wEd-XL95EVwlwxw'),[identifier(none,'OCC')],[set_subtraction(none,union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,ext_pnt)])),set_extension(none,[identifier(none,p)]))])],[])])])],[event_b_context(none,s1_ctx0_blocks,[extends(none,[]),constants(none,[identifier(none,'PLATFORM'),identifier(none,ent_pnt),identifier(none,ext_pnt)]),axioms(none,[partition(rodinpos(s1_ctx0_blocks,axm1,'+'),identifier(none,'BLOCK'),[set_extension(none,[identifier(none,ent_pnt)]),set_extension(none,[identifier(none,ext_pnt)]),identifier(none,'PLATFORM')])]),theorems(none,[]),sets(none,[deferred_set(none,'BLOCK')])]),event_b_context(none,s1_ctx1_blocks,[extends(none,[s1_ctx0_blocks]),constants(none,[]),axioms(none,[not_equal(rodinpos(s1_ctx1_blocks,axm1,'('),identifier(none,'PLATFORM'),empty_set(none))]),theorems(none,[]),sets(none,[])]),event_b_context(none,s1_ctx2_signal,[extends(none,[]),constants(none,[identifier(none,allowed),identifier(none,forbidden)]),axioms(none,[partition(rodinpos(s1_ctx2_signal,axm1,'*'),identifier(none,'ACCESS'),[set_extension(none,[identifier(none,allowed)]),set_extension(none,[identifier(none,forbidden)])])]),theorems(none,[]),sets(none,[deferred_set(none,'ACCESS')])]),event_b_context(none,s1_ctx3_trains,[extends(none,[]),constants(none,[]),axioms(none,[]),theorems(none,[]),sets(none,[deferred_set(none,'TRAIN')])])],[discharged(s3_mch8_switch,'INITIALISATION',inv3),discharged(s3_mch8_switch,'INITIALISATION',inv4),discharged(s3_mch8_switch,'TURN_IN_SWITCH',inv1),discharged(s3_mch8_switch,'TURN_IN_SWITCH',inv3),discharged(s3_mch8_switch,'TURN_OUT_SWITCH',inv2),discharged(s3_mch8_switch,'TURN_OUT_SWITCH',inv4),discharged(s3_mch8_switch,trigger_in_switch,inv1),discharged(s3_mch8_switch,trigger_in_switch,inv3),discharged(s3_mch8_switch,trigger_out_switch,inv2),discharged(s3_mch8_switch,trigger_out_switch,inv4),discharged(s3_mch7_track_sensor,'INITIALISATION',inv1),discharged(s3_mch6_signal_sensor,'INITIALISATION',inv1),discharged(s3_mch6_signal_sensor,'INITIALISATION',inv2),discharged(s3_mch6_signal_sensor,'MOVE_IN_PLATFORM',inv1),discharged(s3_mch6_signal_sensor,'MOVE_OUT_PLATFORM',inv2),discharged(s3_mch6_signal_sensor,'ALLOW_ENTRANCE',inv1),discharged(s3_mch6_signal_sensor,'ALLOW_DEPARTURE',inv2),discharged(s2_mch5_signal_actuator,'INITIALISATION',inv5),discharged(s2_mch5_signal_actuator,'INITIALISATION',inv6),discharged(s2_mch5_signal_actuator,'INITIALISATION',inv7),discharged(s2_mch5_signal_actuator,'INITIALISATION',inv8),discharged(s2_mch5_signal_actuator,'TURN_IN_SWITCH',inv7),discharged(s2_mch5_signal_actuator,'TURN_OUT_SWITCH',inv8),discharged(s2_mch5_signal_actuator,'ALLOW_ENTRANCE',inv5),discharged(s2_mch5_signal_actuator,'ALLOW_ENTRANCE',inv7),discharged(s2_mch5_signal_actuator,'ALLOW_DEPARTURE',inv6),discharged(s2_mch5_signal_actuator,'ALLOW_DEPARTURE',inv8),discharged(s2_mch5_signal_actuator,trigger_in_switch,inv7),discharged(s2_mch5_signal_actuator,trigger_out_switch,inv8),discharged(s2_mch5_signal_actuator,allow_entrance,inv7),discharged(s2_mch5_signal_actuator,allow_departure,inv8),discharged(s2_mch4_switch_actuator,'INITIALISATION',inv1),discharged(s2_mch4_switch_actuator,'INITIALISATION',inv2),discharged(s2_mch4_switch_actuator,'INITIALISATION',inv3),discharged(s2_mch4_switch_actuator,'INITIALISATION',inv4),discharged(s2_mch4_switch_actuator,'MOVE_IN_PLATFORM',inv3),discharged(s2_mch4_switch_actuator,'MOVE_OUT_PLATFORM',inv4),discharged(s2_mch4_switch_actuator,'TURN_IN_SWITCH',inv3),discharged(s2_mch4_switch_actuator,'TURN_OUT_SWITCH',inv4),discharged(s2_mch4_switch_actuator,trigger_in_switch,inv1),discharged(s2_mch4_switch_actuator,trigger_in_switch,inv3),discharged(s2_mch4_switch_actuator,trigger_out_switch,inv2),discharged(s2_mch4_switch_actuator,trigger_out_switch,inv4),discharged(s1_mch3_trains,'INITIALISATION',inv2),discharged(s1_mch3_trains,'INITIALISATION',inv3),discharged(s1_mch2_signals,'INITIALISATION',inv3),discharged(s1_mch2_signals,'INITIALISATION',inv4),discharged(s1_mch2_signals,'ALLOW_ENTRANCE',inv3),discharged(s1_mch2_signals,'ALLOW_DEPARTURE',inv4),discharged(s1_mch1_switches,'INITIALISATION',inv1),discharged(s1_mch1_switches,'INITIALISATION',inv2),discharged(s1_mch1_switches,'TURN_IN_SWITCH',inv1),discharged(s1_mch1_switches,'TURN_OUT_SWITCH',inv2)],_Error)).
2