1		package(load_event_b_project([event_b_model(none,'Ref6_CockpitLights',[sees(none,['Context0','Context1','Context2','Lights6']),refines(none,'Ref5_Switch'),variables(none,[identifier(none,analogical_switch),identifier(none,anomaly),identifier(none,close_EV),identifier(none,close_door_valve),identifier(none,door),identifier(none,door_closed),identifier(none,door_open),identifier(none,extend_EV),identifier(none,extend_gear_valve),identifier(none,gear),identifier(none,gear_extended),identifier(none,gear_retracted),identifier(none,gears_locked_down),identifier(none,gears_maneuvering),identifier(none,general_EV),identifier(none,general_valve),identifier(none,green_light),identifier(none,handle),identifier(none,handle_move),identifier(none,last_door_action),identifier(none,last_gear_action),identifier(none,last_handle_state),identifier(none,lock_door_opening),identifier(none,open_EV),identifier(none,open_door_valve),identifier(none,orange_light),identifier(none,red_light),identifier(none,retract_EV),identifier(none,retract_gear_valve),identifier(none,shock_absorber)]),invariant(none,[member(rodinpos('Ref6_CockpitLights',anomaly,'_U-oL8nkNEeOBXrBZ8EbeCQ'),identifier(none,anomaly),bool_set(none)),member(rodinpos('Ref6_CockpitLights',gears_locked_down,'_U-ozAHkNEeOBXrBZ8EbeCQ'),identifier(none,gears_locked_down),bool_set(none)),member(rodinpos('Ref6_CockpitLights',gears_maneuvering,'_U-ozAXkNEeOBXrBZ8EbeCQ'),identifier(none,gears_maneuvering),bool_set(none)),member(rodinpos('Ref6_CockpitLights',green_light,'_cGTHUHkPEeOBXrBZ8EbeCQ'),identifier(none,green_light),identifier(none,'LIGHT_STATE')),member(rodinpos('Ref6_CockpitLights',orange_light,'_cGTHUXkPEeOBXrBZ8EbeCQ'),identifier(none,orange_light),identifier(none,'LIGHT_STATE')),member(rodinpos('Ref6_CockpitLights',red_light,'_cGTHUnkPEeOBXrBZ8EbeCQ'),identifier(none,red_light),identifier(none,'LIGHT_STATE')),implication(rodinpos('Ref6_CockpitLights','R41','_lIxBwH6_EeOk5IscBNq0oQ'),equal(none,identifier(none,anomaly),boolean_false(none)),negation(none,conjunct(none,equal(none,identifier(none,open_EV),boolean_true(none)),equal(none,identifier(none,close_EV),boolean_true(none))))),implication(rodinpos('Ref6_CockpitLights','R42','_lIxBwX6_EeOk5IscBNq0oQ'),equal(none,identifier(none,anomaly),boolean_false(none)),negation(none,conjunct(none,equal(none,identifier(none,retract_EV),boolean_true(none)),equal(none,identifier(none,extend_EV),boolean_true(none))))),implication(rodinpos('Ref6_CockpitLights','R51','_gsqNYH7AEeOk5IscBNq0oQ'),equal(none,identifier(none,anomaly),boolean_false(none)),implication(none,disjunct(none,equal(none,identifier(none,open_EV),boolean_true(none)),disjunct(none,equal(none,identifier(none,close_EV),boolean_true(none)),disjunct(none,equal(none,identifier(none,extend_EV),boolean_true(none)),equal(none,identifier(none,retract_EV),boolean_true(none))))),equal(none,identifier(none,general_EV),boolean_true(none)))),implication(rodinpos('Ref6_CockpitLights',safe,'_thlRYH7AEeOk5IscBNq0oQ'),equal(none,identifier(none,anomaly),boolean_false(none)),implication(none,disjunct(none,equal(none,identifier(none,extend_EV),boolean_true(none)),equal(none,identifier(none,retract_EV),boolean_true(none))),equal(none,identifier(none,open_EV),boolean_true(none))))]),theorems(none,[]),events(none,[event(rodinpos('Ref6_CockpitLights','INITIALISATION','_zmqekGctEeOU3Z0T65yXqB'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_Y7EY0GY0EeO7UsfGCD69ng'),[identifier(none,gear)],[identifier(none,extended)]),assign(rodinpos('Ref6_CockpitLights',act2,'_KkdfoGY0EeO7UsfGCD69ng'),[identifier(none,door)],[identifier(none,closed)]),assign(rodinpos('Ref6_CockpitLights',close_door_valve,'_yQPxAGY3EeO7UsfGCD69ng'),[identifier(none,close_door_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref6_CockpitLights',open_door_valve,'_yQPxAWY3EeO7UsfGCD69ng'),[identifier(none,open_door_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref6_CockpitLights',retract_gear_valve,'_yQQYEGY3EeO7UsfGCD69ng'),[identifier(none,retract_gear_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref6_CockpitLights',extend_gear_valve,'_yQQYEWY3EeO7UsfGCD69ng'),[identifier(none,extend_gear_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref6_CockpitLights',open_EV,'_xEJigGcBEeO7UsfGCD69ng'),[identifier(none,open_EV)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',close_EV,'_xEKJkGcBEeO7UsfGCD69ng'),[identifier(none,close_EV)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',retract_EV,'_PLAoYGcCEeO7UsfGCD69ng'),[identifier(none,retract_EV)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',extend_EV,'_PLAoYWcCEeO7UsfGCD69ng'),[identifier(none,extend_EV)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',door_closed,'_soNwcGcGEeO7UsfGCD69ng'),[identifier(none,door_closed)],[boolean_true(none)]),assign(rodinpos('Ref6_CockpitLights',door_open,'_soNwcWcGEeO7UsfGCD69ng'),[identifier(none,door_open)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',gear_extended,'_soNwcmcGEeO7UsfGCD69ng'),[identifier(none,gear_extended)],[boolean_true(none)]),assign(rodinpos('Ref6_CockpitLights',gear_retracted,'_soNwc2cGEeO7UsfGCD69ng'),[identifier(none,gear_retracted)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',last_door_action,'_pmSioWcpEeOIZYXp1CRUOw'),[identifier(none,last_door_action)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'STIMULI')))]),assign(rodinpos('Ref6_CockpitLights',last_gear_action,'_cRkAYGctEeOU3Z0T65yXqA'),[identifier(none,last_gear_action)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'STIMULI')))]),assign(rodinpos('Ref6_CockpitLights',handle,'_68JSoGcSEeO7UsfGCD69ng'),[identifier(none,handle)],[identifier(none,down)]),assign(rodinpos('Ref6_CockpitLights',handle2,'_RCQvAGcwEeOU3Z0T65yXqA'),[identifier(none,last_handle_state)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'HANDLE_STATE')))]),assign(rodinpos('Ref6_CockpitLights',ground,'_d1sSAGigEeOT_9tDelWe4g'),[identifier(none,shock_absorber)],[identifier(none,flight)]),assign(rodinpos('Ref6_CockpitLights',groundlock,'_dpP8AGihEeOT_9tDelWe4g'),[identifier(none,lock_door_opening)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',general_EV,'_TD_sYXd6EeOBXrBZ8EbeCQ'),[identifier(none,general_EV)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',handle_move,'_UjZNIHd7EeOBXrBZ8EbeCQ'),[identifier(none,handle_move)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',general_valve,'__IzIQHeEEeOBXrBZ8EbeCQ'),[identifier(none,general_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref6_CockpitLights',analogical_switch,'_JqjfsHeZEeOBXrBZ8EbeCQ'),[identifier(none,analogical_switch)],[identifier(none,switch_open)]),assign(rodinpos('Ref6_CockpitLights',anomaly,'_U-iFUHkNEeOBXrBZ8EbeCQ'),[identifier(none,anomaly)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',gears_locked_down,'_U-iFUXkNEeOBXrBZ8EbeCQ'),[identifier(none,gears_locked_down)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',gears_maneuvering,'_U-iFUnkNEeOBXrBZ8EbeCQ'),[identifier(none,gears_maneuvering)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',green_light,'_g5cGMHkPEeOBXrBZ8EbeCQ'),[identifier(none,green_light)],[identifier(none,off)]),assign(rodinpos('Ref6_CockpitLights',orange_light,'_g5cGMXkPEeOBXrBZ8EbeCQ'),[identifier(none,orange_light)],[identifier(none,off)]),assign(rodinpos('Ref6_CockpitLights',red_light,'_g5cGMnkPEeOBXrBZ8EbeCQ'),[identifier(none,red_light)],[identifier(none,off)])],[]),event(rodinpos('Ref6_CockpitLights',env_start_extending,'_zmqekGctEeOU3Z0T65yXqC'),env_start_extending,ordinary(none),[env_start_extending],[],[equal(rodinpos('Ref6_CockpitLights',grd2,'_XbFLomfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,retracted)),equal(rodinpos('Ref6_CockpitLights',grd3,'_fVIREmfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref6_CockpitLights',grd4,'_WLnKIX64EeOk5IscBNq0oQ'),identifier(none,retract_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref6_CockpitLights',general_valve,'_1cR6cHeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_XbFysGfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,gear_moving)]),assign(rodinpos('Ref6_CockpitLights',act3,'_hBLRQmfJEeO3ssiFDTK-qw'),[identifier(none,gear_retracted)],[boolean_false(none)])],[]),event(rodinpos('Ref6_CockpitLights',env_extend_gear,'_zmqekGctEeOU3Z0T65yXqD'),env_extend_gear,ordinary(none),[env_extend_gear],[],[equal(rodinpos('Ref6_CockpitLights',grd2,'_XbGZwGfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,gear_moving)),equal(rodinpos('Ref6_CockpitLights',grd3,'_fVI4IWfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref6_CockpitLights',grd4,'_WLnKI364EeOk5IscBNq0oQ'),identifier(none,retract_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref6_CockpitLights',general_valve,'_1cR6cXeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_XbGZwWfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,extended)]),assign(rodinpos('Ref6_CockpitLights',act3,'_hBLRRWfJEeO3ssiFDTK-qw'),[identifier(none,gear_extended)],[boolean_true(none)])],[]),event(rodinpos('Ref6_CockpitLights',env_retract_gear,'_zmqekGctEeOU3Z0T65yXqE'),env_retract_gear,ordinary(none),[env_retract_gear],[],[equal(rodinpos('Ref6_CockpitLights',grd2,'_XbHA0WfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,gear_moving)),equal(rodinpos('Ref6_CockpitLights',grd3,'_fVJfMGfHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref6_CockpitLights',grd4,'_WLnxMX64EeOk5IscBNq0oQ'),identifier(none,extend_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref6_CockpitLights',general_valve,'_1cShgHeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_XbHA0mfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,retracted)]),assign(rodinpos('Ref6_CockpitLights',act3,'_hBL4UmfJEeO3ssiFDTK-qw'),[identifier(none,gear_retracted)],[boolean_true(none)]),assign(rodinpos('Ref6_CockpitLights',shockabs,'_5RGikWmCEeOLrLY1DXbL2w'),[identifier(none,shock_absorber)],[identifier(none,flight)])],[]),event(rodinpos('Ref6_CockpitLights',env_start_retracting,'_zmqekGctEeOU3Z0T65yXqF'),env_start_retracting,ordinary(none),[env_start_retracting],[],[equal(rodinpos('Ref6_CockpitLights',grd2,'_XbHn4WfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,extended)),equal(rodinpos('Ref6_CockpitLights',grd3,'_fVJfM2fHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref6_CockpitLights',grd4,'_WLnxM364EeOk5IscBNq0oQ'),identifier(none,extend_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref6_CockpitLights',general_valve,'_1cShgXeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_XbIO8GfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,gear_moving)]),assign(rodinpos('Ref6_CockpitLights',act3,'_hBMfYGfJEeO3ssiFDTK-qw'),[identifier(none,gear_extended)],[boolean_false(none)])],[]),event(rodinpos('Ref6_CockpitLights',env_start_open_door,'_zmqekGctEeOU3Z0T65yXqG'),env_start_open_door,ordinary(none),[env_start_open_door],[],[equal(rodinpos('Ref6_CockpitLights',grd2,'_XbI2AGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,closed)),equal(rodinpos('Ref6_CockpitLights',grd3,'_fVKGQmfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref6_CockpitLights',grd4,'_WLnxNX64EeOk5IscBNq0oQ'),identifier(none,close_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref6_CockpitLights',general_valve,'_1cTIkHeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_XbI2AWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,door_moving)]),assign(rodinpos('Ref6_CockpitLights',act3,'_hBNGcGfJEeO3ssiFDTK-qw'),[identifier(none,door_closed)],[boolean_false(none)])],[]),event(rodinpos('Ref6_CockpitLights',env_open_door,'_zmqekGctEeOU3Z0T65yXqH'),env_open_door,ordinary(none),[env_open_door],[],[equal(rodinpos('Ref6_CockpitLights',grd2,'_XbJdEGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,door_moving)),equal(rodinpos('Ref6_CockpitLights',grd3,'_fVKtUWfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref6_CockpitLights',grd4,'_WLoYQH64EeOk5IscBNq0oQ'),identifier(none,close_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref6_CockpitLights',general_valve,'_1cTIkXeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_XbJdEWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,open)]),assign(rodinpos('Ref6_CockpitLights',act3,'_hBNtgWfJEeO3ssiFDTK-qw'),[identifier(none,door_open)],[boolean_true(none)])],[]),event(rodinpos('Ref6_CockpitLights',env_close_door,'_zmqekGctEeOU3Z0T65yXqI'),env_close_door,ordinary(none),[env_close_door],[],[equal(rodinpos('Ref6_CockpitLights',grd2,'_XbKEIWfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,door_moving)),equal(rodinpos('Ref6_CockpitLights',grd3,'_fVKtVGfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref6_CockpitLights',grd4,'_WLoYQn64EeOk5IscBNq0oQ'),identifier(none,open_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref6_CockpitLights',general_valve,'_1cTvoHeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_XbKrMGfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,closed)]),assign(rodinpos('Ref6_CockpitLights',act3,'_hBOUkWfJEeO3ssiFDTK-qw'),[identifier(none,door_closed)],[boolean_true(none)])],[]),event(rodinpos('Ref6_CockpitLights',env_start_close_door,'_zmqekGctEeOU3Z0T65yXqJ'),env_start_close_door,ordinary(none),[env_start_close_door],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_XbLSQGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,open)),equal(rodinpos('Ref6_CockpitLights',grd3,'_fVLUYmfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref6_CockpitLights',grd4,'_WLoYRH64EeOk5IscBNq0oQ'),identifier(none,open_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref6_CockpitLights',general_valve,'_1cTvoXeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_XbLSQWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,door_moving)]),assign(rodinpos('Ref6_CockpitLights',act3,'_hBO7oWfJEeO3ssiFDTK-qw'),[identifier(none,door_open)],[boolean_false(none)])],[]),event(rodinpos('Ref6_CockpitLights',env_open_valve_open_door,'_zmqekGctEeOU3Z0T65yXqK'),env_open_valve_open_door,ordinary(none),[env_open_valve_open_door],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_CreNUWY4EeO7UsfGCD69ng'),identifier(none,open_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref6_CockpitLights',grd3,'_3bBYgn68EeOk5IscBNq0oQ'),identifier(none,open_EV),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_Cre0YGY4EeO7UsfGCD69ng'),[identifier(none,open_door_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref6_CockpitLights',env_close_valve_open_door,'_zmqekGctEeOU3Z0T65yXqL'),env_close_valve_open_door,ordinary(none),[env_close_valve_open_door],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_0L1aMWfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref6_CockpitLights',grd3,'_3bBYhH68EeOk5IscBNq0oQ'),identifier(none,open_EV),boolean_false(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_0L2BQGfHEeO3ssiFDTK-qw'),[identifier(none,open_door_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref6_CockpitLights',env_open_valve_close_door,'_zmqekGctEeOU3Z0T65yXqM'),env_open_valve_close_door,ordinary(none),[env_open_valve_close_door],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_0L2BQmfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref6_CockpitLights',grd3,'_3bBYhn68EeOk5IscBNq0oQ'),identifier(none,close_EV),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_0L2BQ2fHEeO3ssiFDTK-qw'),[identifier(none,close_door_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref6_CockpitLights',env_close_valve_close_door,'_zmqekGctEeOU3Z0T65yXqN'),env_close_valve_close_door,ordinary(none),[env_close_valve_close_door],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_0L2oUWfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref6_CockpitLights',grd2,'_3bBYiH68EeOk5IscBNq0oQ'),identifier(none,close_EV),boolean_false(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_0L2oUmfHEeO3ssiFDTK-qw'),[identifier(none,close_door_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref6_CockpitLights',env_open_valve_retract_gear,'_zmqekGctEeOU3Z0T65yXqO'),env_open_valve_retract_gear,ordinary(none),[env_open_valve_retract_gear],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_0L3PYGfHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref6_CockpitLights',grd3,'_3bB_kX68EeOk5IscBNq0oQ'),identifier(none,retract_EV),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_0L3PYWfHEeO3ssiFDTK-qw'),[identifier(none,retract_gear_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref6_CockpitLights',env_close_valve_retract_gear,'_zmqekGctEeOU3Z0T65yXqP'),env_close_valve_retract_gear,ordinary(none),[env_close_valve_retract_gear],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_0L3PY2fHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref6_CockpitLights',grd3,'_3bB_k368EeOk5IscBNq0oQ'),identifier(none,retract_EV),boolean_false(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_0L32cGfHEeO3ssiFDTK-qw'),[identifier(none,retract_gear_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref6_CockpitLights',env_open_valve_extend_gear,'_zmqekGctEeOU3Z0T65yXqQ'),env_open_valve_extend_gear,ordinary(none),[env_open_valve_extend_gear],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_0L32cmfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref6_CockpitLights',grd3,'_3bB_lX68EeOk5IscBNq0oQ'),identifier(none,extend_EV),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_0L32c2fHEeO3ssiFDTK-qw'),[identifier(none,extend_gear_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref6_CockpitLights',env_close_valve_extend_gear,'_zmqekGctEeOU3Z0T65yXqR'),env_close_valve_extend_gear,ordinary(none),[env_close_valve_extend_gear],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_0L4dgWfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref6_CockpitLights',grd3,'_3bB_l368EeOk5IscBNq0oQ'),identifier(none,extend_EV),boolean_false(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_0L4dgmfHEeO3ssiFDTK-qw'),[identifier(none,extend_gear_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref6_CockpitLights',con_stimulate_open_door_valve,'_zmqekGctEeOU3Z0T65yXqS'),con_stimulate_open_door_valve,ordinary(none),[con_stimulate_open_door_valve],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_reokEGfIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_false(none)),equal(rodinpos('Ref6_CockpitLights',grd2,'_reokEWfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_false(none)),disjunct(rodinpos('Ref6_CockpitLights',gear_not_moving,'_Ie4-wGc7EeOU3Z0T65yXqA'),equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,gear_retracted),boolean_true(none))),disjunct(rodinpos('Ref6_CockpitLights',handle,'_FGeEcmfKEeO3ssiFDTK-qw'),conjunct(none,equal(none,identifier(none,gear),identifier(none,extended)),equal(none,identifier(none,handle),identifier(none,up))),conjunct(none,equal(none,identifier(none,gear),identifier(none,retracted)),equal(none,identifier(none,handle),identifier(none,down)))),equal(rodinpos('Ref6_CockpitLights',dooropeningnotlocked,'_dpRxM2ihEeOT_9tDelWe4g'),identifier(none,lock_door_opening),boolean_false(none)),equal(rodinpos('Ref6_CockpitLights',general_ev,'_hcowcHd7EeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_reokEmfIEeO3ssiFDTK-qw'),[identifier(none,open_EV)],[boolean_true(none)]),assign(rodinpos('Ref6_CockpitLights',act,'_Yg1BEGcqEeOIZYXp1CRUOw'),[identifier(none,last_door_action)],[set_extension(none,[identifier(none,open_door_stimulus)])]),assign(rodinpos('Ref6_CockpitLights',act3,'_FGergGfKEeO3ssiFDTK-qw'),[identifier(none,last_handle_state)],[set_extension(none,[identifier(none,handle)])])],[]),event(rodinpos('Ref6_CockpitLights',con_stop_stimulate_open_door_valve,'_zmqekGctEeOU3Z0T65yXqT'),con_stop_stimulate_open_door_valve,ordinary(none),[con_stop_stimulate_open_door_valve],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_reokFGfIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_true(none)),disjunct(rodinpos('Ref6_CockpitLights',handle,'_FGerg2fKEeO3ssiFDTK-qw'),conjunct(none,equal(none,identifier(none,gear),identifier(none,extended)),equal(none,identifier(none,handle),identifier(none,down))),disjunct(none,conjunct(none,equal(none,identifier(none,gear),identifier(none,retracted)),equal(none,identifier(none,handle),identifier(none,up))),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,handle),identifier(none,up)),conjunct(none,equal(none,identifier(none,door_open),boolean_true(none)),equal(none,identifier(none,shock_absorber),identifier(none,ground))))))),conjunct(rodinpos('Ref6_CockpitLights',grd6,'_FGerhGfKEeO3ssiFDTK-qw'),equal(none,identifier(none,retract_EV),boolean_false(none)),equal(none,identifier(none,extend_EV),boolean_false(none))),equal(rodinpos('Ref6_CockpitLights',general_ev,'_cnpCcHhiEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_repLIGfIEeO3ssiFDTK-qw'),[identifier(none,open_EV)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',act3,'_FGfSkGfKEeO3ssiFDTK-qw'),[identifier(none,last_handle_state)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'HANDLE_STATE')))]),assign(rodinpos('Ref6_CockpitLights',lockdooropening,'_BlYzMGiiEeOT_9tDelWe4g'),[identifier(none,lock_door_opening)],[boolean_true(none)])],[]),event(rodinpos('Ref6_CockpitLights',con_stimulate_close_door_valve,'_zmqekGctEeOU3Z0T65yXqU'),con_stimulate_close_door_valve,ordinary(none),[con_stimulate_close_door_valve],[],[equal(rodinpos('Ref6_CockpitLights',grd2,'_repLImfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_false(none)),equal(rodinpos('Ref6_CockpitLights',grd1,'_repLI2fIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_false(none)),disjunct(rodinpos('Ref6_CockpitLights',grd,'_oZAasGcqEeOIZYXp1CRUOw'),equal(none,identifier(none,door_closed),boolean_false(none)),equal(none,identifier(none,last_door_action),set_extension(none,[identifier(none,open_door_stimulus)]))),disjunct(rodinpos('Ref6_CockpitLights',gear_not_moving,'_Ie4-wWc7EeOU3Z0T65yXqA'),equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,gear_retracted),boolean_true(none))),disjunct(rodinpos('Ref6_CockpitLights',gear_not_waitingformoving,'_2FwWI2f8EeOan70hsodGWg'),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,handle),identifier(none,down))),disjunct(none,conjunct(none,equal(none,identifier(none,gear_retracted),boolean_true(none)),equal(none,identifier(none,handle),identifier(none,up))),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,handle),identifier(none,up)),equal(none,identifier(none,shock_absorber),identifier(none,ground)))))),equal(rodinpos('Ref6_CockpitLights',general_ev,'_cnpCcXhiEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_repLJGfIEeO3ssiFDTK-qw'),[identifier(none,close_EV)],[boolean_true(none)]),assign(rodinpos('Ref6_CockpitLights',act,'_Yg1oIGcqEeOIZYXp1CRUOw'),[identifier(none,last_door_action)],[set_extension(none,[identifier(none,close_door_stimulus)])]),assign(rodinpos('Ref6_CockpitLights',act3,'_8I6FEGcwEeOU3Z0T65yXqA'),[identifier(none,last_handle_state)],[set_extension(none,[identifier(none,handle)])]),assign(rodinpos('Ref6_CockpitLights',lockdooropening,'_dpSYQWihEeOT_9tDelWe4g'),[identifier(none,lock_door_opening)],[boolean_true(none)])],[]),event(rodinpos('Ref6_CockpitLights',con_stop_stimulate_close_door_valve,'_zmqekGctEeOU3Z0T65yXqV'),con_stop_stimulate_close_door_valve,ordinary(none),[con_stop_stimulate_close_door_valve],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_repyMWfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_true(none)),disjunct(rodinpos('Ref6_CockpitLights',grd5,'_FGfSk2fKEeO3ssiFDTK-qw'),equal(none,identifier(none,door_closed),boolean_true(none)),conjunct(none,equal(none,identifier(none,door_closed),boolean_false(none)),not_equal(none,identifier(none,last_handle_state),set_extension(none,[identifier(none,handle)])))),equal(rodinpos('Ref6_CockpitLights',general_ev,'_cnppgHhiEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_repyMmfIEeO3ssiFDTK-qw'),[identifier(none,close_EV)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',act3,'_FGfSlGfKEeO3ssiFDTK-qw'),[identifier(none,last_handle_state)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'HANDLE_STATE')))])],[]),event(rodinpos('Ref6_CockpitLights',con_stimulate_retract_gear_valve,'_zmqekGctEeOU3Z0T65yXqW'),con_stimulate_retract_gear_valve,ordinary(none),[con_stimulate_retract_gear_valve],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_repyNGfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_false(none)),equal(rodinpos('Ref6_CockpitLights',grd2,'_reqZQGfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_false(none)),equal(rodinpos('Ref6_CockpitLights',grd3,'_ssC38GgAEeOan70hsodGWg'),identifier(none,open_EV),boolean_true(none)),equal(rodinpos('Ref6_CockpitLights',door,'_hBR-8GfJEeO3ssiFDTK-qw'),identifier(none,door_open),boolean_true(none)),disjunct(rodinpos('Ref6_CockpitLights',grd4,'_hBR-8WfJEeO3ssiFDTK-qw'),equal(none,identifier(none,gear_retracted),boolean_false(none)),conjunct(none,equal(none,identifier(none,gear_retracted),boolean_true(none)),equal(none,identifier(none,last_gear_action),set_extension(none,[identifier(none,extend_gear_stimulus)])))),equal(rodinpos('Ref6_CockpitLights',grd7,'_FGf5omfKEeO3ssiFDTK-qw'),identifier(none,handle),identifier(none,up)),disjunct(rodinpos('Ref6_CockpitLights',grd8,'_h3dFgImVEeOQc6S3EYezPA'),equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,gear_extended),boolean_false(none)),not_equal(none,identifier(none,last_handle_state),set_extension(none,[identifier(none,handle)])))),equal(rodinpos('Ref6_CockpitLights',groundguard,'_dpSYRGihEeOT_9tDelWe4g'),identifier(none,shock_absorber),identifier(none,flight)),equal(rodinpos('Ref6_CockpitLights',general_ev,'_cnppgXhiEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_reqZQmfIEeO3ssiFDTK-qw'),[identifier(none,retract_EV)],[boolean_true(none)]),assign(rodinpos('Ref6_CockpitLights',act,'_hBR-8mfJEeO3ssiFDTK-qw'),[identifier(none,last_gear_action)],[set_extension(none,[identifier(none,retract_gear_stimulus)])])],[]),event(rodinpos('Ref6_CockpitLights',con_stop_stimulate_retract_gear_valve,'_zmqekGctEeOU3Z0T65yXqX'),con_stop_stimulate_retract_gear_valve,ordinary(none),[con_stop_stimulate_retract_gear_valve],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_reqZRGfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_true(none)),disjunct(rodinpos('Ref6_CockpitLights',grd,'_FGggsGfKEeO3ssiFDTK-qw'),equal(none,identifier(none,gear_retracted),boolean_true(none)),conjunct(none,equal(none,identifier(none,gear_retracted),boolean_false(none)),equal(none,identifier(none,handle),identifier(none,down)))),equal(rodinpos('Ref6_CockpitLights',general_ev,'_cnppgnhiEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_reqZRWfIEeO3ssiFDTK-qw'),[identifier(none,retract_EV)],[boolean_false(none)])],[]),event(rodinpos('Ref6_CockpitLights',con_stimulate_extend_gear_valve,'_zmqekGctEeOU3Z0T65yXqY'),con_stimulate_extend_gear_valve,ordinary(none),[con_stimulate_extend_gear_valve],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_rerAUWfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_false(none)),equal(rodinpos('Ref6_CockpitLights',grd2,'_rerAUmfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_false(none)),equal(rodinpos('Ref6_CockpitLights',grd3,'_ssDfAGgAEeOan70hsodGWg'),identifier(none,open_EV),boolean_true(none)),equal(rodinpos('Ref6_CockpitLights',door,'_hBSmAWfJEeO3ssiFDTK-qw'),identifier(none,door_open),boolean_true(none)),disjunct(rodinpos('Ref6_CockpitLights',grd,'_hBSmAmfJEeO3ssiFDTK-qw'),equal(none,identifier(none,gear_extended),boolean_false(none)),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,last_gear_action),set_extension(none,[identifier(none,retract_gear_stimulus)])))),equal(rodinpos('Ref6_CockpitLights',grd7,'_FGggs2fKEeO3ssiFDTK-qw'),identifier(none,handle),identifier(none,down)),disjunct(rodinpos('Ref6_CockpitLights',grd8,'_akrbcImVEeOQc6S3EYezPA'),equal(none,identifier(none,gear_retracted),boolean_true(none)),conjunct(none,equal(none,identifier(none,gear_retracted),boolean_false(none)),not_equal(none,identifier(none,last_handle_state),set_extension(none,[identifier(none,handle)])))),equal(rodinpos('Ref6_CockpitLights',general_ev,'_cnqQkHhiEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_rerAVGfIEeO3ssiFDTK-qw'),[identifier(none,extend_EV)],[boolean_true(none)]),assign(rodinpos('Ref6_CockpitLights',act,'_hBSmA2fJEeO3ssiFDTK-qw'),[identifier(none,last_gear_action)],[set_extension(none,[identifier(none,extend_gear_stimulus)])])],[]),event(rodinpos('Ref6_CockpitLights',con_stop_stimulate_extend_gear_valve,'_zmqekGctEeOU3Z0T65yXqZ'),con_stop_stimulate_extend_gear_valve,ordinary(none),[con_stop_stimulate_extend_gear_valve],[],[equal(rodinpos('Ref6_CockpitLights',grd2,'_rernYWfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_true(none)),disjunct(rodinpos('Ref6_CockpitLights',grd,'_FGhHwWfKEeO3ssiFDTK-qw'),equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,gear_extended),boolean_false(none)),equal(none,identifier(none,handle),identifier(none,up)))),equal(rodinpos('Ref6_CockpitLights',general_ev,'_cnqQkXhiEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_rernYmfIEeO3ssiFDTK-qw'),[identifier(none,extend_EV)],[boolean_false(none)])],[]),event(rodinpos('Ref6_CockpitLights',env_toggle_handle,'_zmqekGctEeOU3Z0T65yXq['),env_toggle_handle,ordinary(none),[env_toggle_handle],[],[],[],[becomes_element_of(rodinpos('Ref6_CockpitLights',act,'_FGhHw2fKEeO3ssiFDTK-qw'),[identifier(none,handle)],set_subtraction(none,identifier(none,'HANDLE_STATE'),set_extension(none,[identifier(none,handle)]))),assign(rodinpos('Ref6_CockpitLights',removegroundlocking,'_dpS_U2ihEeOT_9tDelWe4g'),[identifier(none,lock_door_opening)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',handle_move,'_XRGwkHd7EeOBXrBZ8EbeCQ'),[identifier(none,handle_move)],[boolean_true(none)])],[]),event(rodinpos('Ref6_CockpitLights',env_changeShockAbsorber,'_zmqekGctEeOU3Z0T65yXq\\'),env_changeShockAbsorber,ordinary(none),[env_changeShockAbsorber],[],[equal(rodinpos('Ref6_CockpitLights',grd,'_5RdH4GmCEeOLrLY1DXbL2w'),identifier(none,gear_retracted),boolean_false(none))],[],[becomes_element_of(rodinpos('Ref6_CockpitLights',act,'_5RdH4WmCEeOLrLY1DXbL2w'),[identifier(none,shock_absorber)],set_subtraction(none,identifier(none,'PLANE_STATE'),set_extension(none,[identifier(none,shock_absorber)])))],[]),event(rodinpos('Ref6_CockpitLights',con_stimulate_general_valve,'_zmqekGctEeOU3Z0T65yXq]'),con_stimulate_general_valve,ordinary(none),[con_stimulate_general_valve],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_lqz2gHd6EeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_false(none)),equal(rodinpos('Ref6_CockpitLights',grd2,'_ZxSOUHd7EeOBXrBZ8EbeCQ'),identifier(none,handle_move),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act,'_lqz2gXd6EeOBXrBZ8EbeCQ'),[identifier(none,general_EV)],[boolean_true(none)])],[]),event(rodinpos('Ref6_CockpitLights',con_stop_stimulate_general_valve,'_zmqekGctEeOU3Z0T65yXq^'),con_stop_stimulate_general_valve,ordinary(none),[con_stop_stimulate_general_valve],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_1tvf4neAEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none)),disjunct(rodinpos('Ref6_CockpitLights',grd2,'_1tvf43eAEeOBXrBZ8EbeCQ'),conjunct(none,equal(none,identifier(none,handle),identifier(none,up)),conjunct(none,equal(none,identifier(none,gear_retracted),boolean_true(none)),conjunct(none,equal(none,identifier(none,door_closed),boolean_true(none)),conjunct(none,equal(none,identifier(none,close_EV),boolean_false(none)),equal(none,identifier(none,open_EV),boolean_false(none)))))),disjunct(none,conjunct(none,equal(none,identifier(none,handle),identifier(none,down)),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,door_closed),boolean_true(none)),conjunct(none,equal(none,identifier(none,close_EV),boolean_false(none)),conjunct(none,equal(none,identifier(none,open_EV),boolean_false(none)),conjunct(none,equal(none,identifier(none,last_handle_state),typeof(none,empty_set(none),pow_subset(none,identifier(none,'HANDLE_STATE')))),conjunct(none,equal(none,identifier(none,lock_door_opening),boolean_false(none)),equal(none,identifier(none,last_door_action),set_extension(none,[identifier(none,close_door_stimulus)]))))))))),conjunct(none,equal(none,identifier(none,handle),identifier(none,up)),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,door_closed),boolean_true(none)),conjunct(none,equal(none,identifier(none,close_EV),boolean_false(none)),conjunct(none,equal(none,identifier(none,open_EV),boolean_false(none)),equal(none,identifier(none,lock_door_opening),boolean_true(none)))))))))],[],[assign(rodinpos('Ref6_CockpitLights',act,'_1twG8HeAEeOBXrBZ8EbeCQ'),[identifier(none,general_EV)],[boolean_false(none)]),assign(rodinpos('Ref6_CockpitLights',act2,'_vW6-YHeZEeOBXrBZ8EbeCQ'),[identifier(none,handle_move)],[boolean_false(none)])],[]),event(rodinpos('Ref6_CockpitLights',evn_open_general_valve,'_zmqekGctEeOU3Z0T65yXq_'),evn_open_general_valve,ordinary(none),[evn_open_general_valve],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_7tSDoHeEEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none)),equal(rodinpos('Ref6_CockpitLights',grd2,'_7tSDoXeEEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_closed)),equal(rodinpos('Ref6_CockpitLights',grd3,'_LY1xAHeaEeOBXrBZ8EbeCQ'),identifier(none,analogical_switch),identifier(none,switch_closed))],[],[assign(rodinpos('Ref6_CockpitLights',act,'_JzFgsHeFEeOBXrBZ8EbeCQ'),[identifier(none,general_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref6_CockpitLights',evn_close_general_valve,'_zmqekGctEeOU3Z0T65yXq\140\'),evn_close_general_valve,ordinary(none),[evn_close_general_valve],[],[disjunct(rodinpos('Ref6_CockpitLights',grd1,'_ONp-0XeWEeOBXrBZ8EbeCQ'),equal(none,identifier(none,general_EV),boolean_false(none)),equal(none,identifier(none,analogical_switch),identifier(none,switch_open))),equal(rodinpos('Ref6_CockpitLights',grd2,'_ONql4HeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref6_CockpitLights',act,'_ONql4XeWEeOBXrBZ8EbeCQ'),[identifier(none,general_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref6_CockpitLights',env_close_switch,'_zmqekGctEeOU3Z0T65yXqa'),env_close_switch,ordinary(none),[env_close_switch],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_vW8MgXeZEeOBXrBZ8EbeCQ'),identifier(none,analogical_switch),identifier(none,switch_open)),equal(rodinpos('Ref6_CockpitLights',grd2,'_vW8zkHeZEeOBXrBZ8EbeCQ'),identifier(none,handle_move),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act,'_vW8zkXeZEeOBXrBZ8EbeCQ'),[identifier(none,analogical_switch)],[identifier(none,switch_closed)])],[]),event(rodinpos('Ref6_CockpitLights',env_open_switch,'_zmqekGctEeOU3Z0T65yXqb'),env_open_switch,ordinary(none),[env_open_switch],[],[equal(rodinpos('Ref6_CockpitLights',grd1,'_4awWYXeZEeOBXrBZ8EbeCQ'),identifier(none,analogical_switch),identifier(none,switch_closed))],[],[assign(rodinpos('Ref6_CockpitLights',act,'_4aw9cHeZEeOBXrBZ8EbeCQ'),[identifier(none,analogical_switch)],[identifier(none,switch_open)])],[]),event(rodinpos('Ref6_CockpitLights',con_set_anomaly_output,'_4K0vwH32EeOaotIwUX9rtQ'),con_set_anomaly_output,ordinary(none),[],[],[],[],[assign(rodinpos('Ref6_CockpitLights',act,'_4K0vwX32EeOaotIwUX9rtQ'),[identifier(none,anomaly)],[boolean_true(none)])],[]),event(rodinpos('Ref6_CockpitLights',con_set_cockpit_outputs,'_ANk3gHkQEeOBXrBZ8EbeCQ'),con_set_cockpit_outputs,ordinary(none),[],[],[disjunct(rodinpos('Ref6_CockpitLights',grd1,'_Gt1isH32EeOaotIwUX9rtQ'),not_equal(none,identifier(none,gears_locked_down),identifier(none,gear_extended)),not_equal(none,identifier(none,gears_maneuvering),convert_bool(none,conjunct(none,equal(none,identifier(none,gear_retracted),boolean_false(none)),equal(none,identifier(none,gear_extended),boolean_false(none))))))],[],[assign(rodinpos('Ref6_CockpitLights',act1,'_ANk3gXkQEeOBXrBZ8EbeCQ'),[identifier(none,gears_locked_down)],[identifier(none,gear_extended)]),assign(rodinpos('Ref6_CockpitLights',act2,'_ANk3gnkQEeOBXrBZ8EbeCQ'),[identifier(none,gears_maneuvering)],[convert_bool(none,conjunct(none,equal(none,identifier(none,gear_retracted),boolean_false(none)),equal(none,identifier(none,gear_extended),boolean_false(none))))])],[]),event(rodinpos('Ref6_CockpitLights',env_turn_on_red_light,'_wyLOkHkREeOBXrBZ8EbeCQ'),env_turn_on_red_light,ordinary(none),[],[],[equal(rodinpos('Ref6_CockpitLights',grd,'_wyLOkXkREeOBXrBZ8EbeCQ'),identifier(none,red_light),identifier(none,off)),equal(rodinpos('Ref6_CockpitLights',grd2,'_wyL1oHkREeOBXrBZ8EbeCQ'),identifier(none,anomaly),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act,'_wyL1oXkREeOBXrBZ8EbeCQ'),[identifier(none,red_light)],[identifier(none,on)])],[]),event(rodinpos('Ref6_CockpitLights',env_turn_on_orange_light,'_wyL1onkREeOBXrBZ8EbeCQ'),env_turn_on_orange_light,ordinary(none),[],[],[equal(rodinpos('Ref6_CockpitLights',grd,'_wyL1o3kREeOBXrBZ8EbeCQ'),identifier(none,orange_light),identifier(none,off)),equal(rodinpos('Ref6_CockpitLights',grd2,'_8_HFgHkREeOBXrBZ8EbeCQ'),identifier(none,gears_maneuvering),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act,'_wyL1pHkREeOBXrBZ8EbeCQ'),[identifier(none,orange_light)],[identifier(none,on)])],[]),event(rodinpos('Ref6_CockpitLights',env_turn_off_orange_light,'_f-puYHkOEeOBXrBZ8EbeCQ'),env_turn_off_orange_light,ordinary(none),[],[],[equal(rodinpos('Ref6_CockpitLights',grd,'_NF3GoHkSEeOBXrBZ8EbeCQ'),identifier(none,orange_light),identifier(none,on)),equal(rodinpos('Ref6_CockpitLights',grd2,'_NF3GoXkSEeOBXrBZ8EbeCQ'),identifier(none,gears_maneuvering),boolean_false(none))],[],[assign(rodinpos('Ref6_CockpitLights',act,'_G4xuwHkREeOBXrBZ8EbeCQ'),[identifier(none,orange_light)],[identifier(none,off)])],[]),event(rodinpos('Ref6_CockpitLights',env_turn_on_green_light,'_NF4UwHkSEeOBXrBZ8EbeCQ'),env_turn_on_green_light,ordinary(none),[],[],[equal(rodinpos('Ref6_CockpitLights',grd,'_NF4UwXkSEeOBXrBZ8EbeCQ'),identifier(none,green_light),identifier(none,off)),equal(rodinpos('Ref6_CockpitLights',grd2,'_NF4UwnkSEeOBXrBZ8EbeCQ'),identifier(none,gears_locked_down),boolean_true(none))],[],[assign(rodinpos('Ref6_CockpitLights',act,'_NF470HkSEeOBXrBZ8EbeCQ'),[identifier(none,green_light)],[identifier(none,on)])],[]),event(rodinpos('Ref6_CockpitLights',env_turn_off_green_light,'_NF470XkSEeOBXrBZ8EbeCQ'),env_turn_off_green_light,ordinary(none),[],[],[equal(rodinpos('Ref6_CockpitLights',grd,'_NF470nkSEeOBXrBZ8EbeCQ'),identifier(none,green_light),identifier(none,on)),equal(rodinpos('Ref6_CockpitLights',grd2,'_NF4703kSEeOBXrBZ8EbeCQ'),identifier(none,gears_locked_down),boolean_false(none))],[],[assign(rodinpos('Ref6_CockpitLights',act,'_NF471HkSEeOBXrBZ8EbeCQ'),[identifier(none,green_light)],[identifier(none,off)])],[])])]),event_b_model(none,'Ref5_Switch',[sees(none,['Context0','Context1','Context2']),refines(none,'Ref4_ControllerHandle'),variables(none,[identifier(none,analogical_switch),identifier(none,close_EV),identifier(none,close_door_valve),identifier(none,door),identifier(none,door_closed),identifier(none,door_open),identifier(none,extend_EV),identifier(none,extend_gear_valve),identifier(none,gear),identifier(none,gear_extended),identifier(none,gear_retracted),identifier(none,general_EV),identifier(none,general_valve),identifier(none,handle),identifier(none,handle_move),identifier(none,last_door_action),identifier(none,last_gear_action),identifier(none,last_handle_state),identifier(none,lock_door_opening),identifier(none,open_EV),identifier(none,open_door_valve),identifier(none,retract_EV),identifier(none,retract_gear_valve),identifier(none,shock_absorber)]),invariant(none,[member(rodinpos('Ref5_Switch',general_EV,'_TESAQHd6EeOBXrBZ8EbeCQ'),identifier(none,general_EV),bool_set(none)),member(rodinpos('Ref5_Switch',handle_move,'_UjiXEXd7EeOBXrBZ8EbeCQ'),identifier(none,handle_move),bool_set(none)),member(rodinpos('Ref5_Switch',general_valve,'_7tRckXeEEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,'VALVE_STATE')),member(rodinpos('Ref5_Switch',analogical_switch,'_8S0pkXeYEeOBXrBZ8EbeCQ'),identifier(none,analogical_switch),identifier(none,'SWITCH_STATE')),implication(rodinpos('Ref5_Switch',r51,'_LxHk8IjvEeOQc6S3EYezPA'),disjunct(none,equal(none,identifier(none,open_EV),boolean_true(none)),disjunct(none,equal(none,identifier(none,close_EV),boolean_true(none)),disjunct(none,equal(none,identifier(none,retract_EV),boolean_true(none)),equal(none,identifier(none,extend_EV),boolean_true(none))))),equal(none,identifier(none,general_EV),boolean_true(none)))]),theorems(none,[]),events(none,[event(rodinpos('Ref5_Switch','INITIALISATION','_zmqekGctEeOU3Z0T65yXqB'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('Ref5_Switch',act1,'_Y7EY0GY0EeO7UsfGCD69ng'),[identifier(none,gear)],[identifier(none,extended)]),assign(rodinpos('Ref5_Switch',act2,'_KkdfoGY0EeO7UsfGCD69ng'),[identifier(none,door)],[identifier(none,closed)]),assign(rodinpos('Ref5_Switch',close_door_valve,'_yQPxAGY3EeO7UsfGCD69ng'),[identifier(none,close_door_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref5_Switch',open_door_valve,'_yQPxAWY3EeO7UsfGCD69ng'),[identifier(none,open_door_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref5_Switch',retract_gear_valve,'_yQQYEGY3EeO7UsfGCD69ng'),[identifier(none,retract_gear_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref5_Switch',extend_gear_valve,'_yQQYEWY3EeO7UsfGCD69ng'),[identifier(none,extend_gear_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref5_Switch',open_EV,'_xEJigGcBEeO7UsfGCD69ng'),[identifier(none,open_EV)],[boolean_false(none)]),assign(rodinpos('Ref5_Switch',close_EV,'_xEKJkGcBEeO7UsfGCD69ng'),[identifier(none,close_EV)],[boolean_false(none)]),assign(rodinpos('Ref5_Switch',retract_EV,'_PLAoYGcCEeO7UsfGCD69ng'),[identifier(none,retract_EV)],[boolean_false(none)]),assign(rodinpos('Ref5_Switch',extend_EV,'_PLAoYWcCEeO7UsfGCD69ng'),[identifier(none,extend_EV)],[boolean_false(none)]),assign(rodinpos('Ref5_Switch',door_closed,'_soNwcGcGEeO7UsfGCD69ng'),[identifier(none,door_closed)],[boolean_true(none)]),assign(rodinpos('Ref5_Switch',door_open,'_soNwcWcGEeO7UsfGCD69ng'),[identifier(none,door_open)],[boolean_false(none)]),assign(rodinpos('Ref5_Switch',gear_extended,'_soNwcmcGEeO7UsfGCD69ng'),[identifier(none,gear_extended)],[boolean_true(none)]),assign(rodinpos('Ref5_Switch',gear_retracted,'_soNwc2cGEeO7UsfGCD69ng'),[identifier(none,gear_retracted)],[boolean_false(none)]),assign(rodinpos('Ref5_Switch',last_door_action,'_pmSioWcpEeOIZYXp1CRUOw'),[identifier(none,last_door_action)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'STIMULI')))]),assign(rodinpos('Ref5_Switch',last_gear_action,'_cRkAYGctEeOU3Z0T65yXqA'),[identifier(none,last_gear_action)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'STIMULI')))]),assign(rodinpos('Ref5_Switch',handle,'_68JSoGcSEeO7UsfGCD69ng'),[identifier(none,handle)],[identifier(none,down)]),assign(rodinpos('Ref5_Switch',handle2,'_RCQvAGcwEeOU3Z0T65yXqA'),[identifier(none,last_handle_state)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'HANDLE_STATE')))]),assign(rodinpos('Ref5_Switch',ground,'_d1sSAGigEeOT_9tDelWe4g'),[identifier(none,shock_absorber)],[identifier(none,flight)]),assign(rodinpos('Ref5_Switch',groundlock,'_dpP8AGihEeOT_9tDelWe4g'),[identifier(none,lock_door_opening)],[boolean_false(none)]),assign(rodinpos('Ref5_Switch',general_EV,'_TD_sYXd6EeOBXrBZ8EbeCQ'),[identifier(none,general_EV)],[boolean_false(none)]),assign(rodinpos('Ref5_Switch',handle_move,'_UjZNIHd7EeOBXrBZ8EbeCQ'),[identifier(none,handle_move)],[boolean_false(none)]),assign(rodinpos('Ref5_Switch',general_valve,'__IzIQHeEEeOBXrBZ8EbeCQ'),[identifier(none,general_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref5_Switch',analogical_switch,'_JqjfsHeZEeOBXrBZ8EbeCQ'),[identifier(none,analogical_switch)],[identifier(none,switch_open)])],[]),event(rodinpos('Ref5_Switch',env_start_extending,'_zmqekGctEeOU3Z0T65yXqC'),env_start_extending,ordinary(none),[env_start_extending],[],[equal(rodinpos('Ref5_Switch',grd2,'_XbFLomfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,retracted)),equal(rodinpos('Ref5_Switch',grd3,'_fVIREmfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref5_Switch',grd4,'_WLnKIX64EeOk5IscBNq0oQ'),identifier(none,retract_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref5_Switch',general_valve,'_1cR6cHeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref5_Switch',act1,'_XbFysGfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,gear_moving)]),assign(rodinpos('Ref5_Switch',act3,'_hBLRQmfJEeO3ssiFDTK-qw'),[identifier(none,gear_retracted)],[boolean_false(none)])],[]),event(rodinpos('Ref5_Switch',env_extend_gear,'_zmqekGctEeOU3Z0T65yXqD'),env_extend_gear,ordinary(none),[env_extend_gear],[],[equal(rodinpos('Ref5_Switch',grd2,'_XbGZwGfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,gear_moving)),equal(rodinpos('Ref5_Switch',grd3,'_fVI4IWfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref5_Switch',grd4,'_WLnKI364EeOk5IscBNq0oQ'),identifier(none,retract_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref5_Switch',general_valve,'_1cR6cXeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref5_Switch',act1,'_XbGZwWfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,extended)]),assign(rodinpos('Ref5_Switch',act3,'_hBLRRWfJEeO3ssiFDTK-qw'),[identifier(none,gear_extended)],[boolean_true(none)])],[]),event(rodinpos('Ref5_Switch',env_retract_gear,'_zmqekGctEeOU3Z0T65yXqE'),env_retract_gear,ordinary(none),[env_retract_gear],[],[equal(rodinpos('Ref5_Switch',grd2,'_XbHA0WfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,gear_moving)),equal(rodinpos('Ref5_Switch',grd3,'_fVJfMGfHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref5_Switch',grd4,'_WLnxMX64EeOk5IscBNq0oQ'),identifier(none,extend_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref5_Switch',general_valve,'_1cShgHeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref5_Switch',act1,'_XbHA0mfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,retracted)]),assign(rodinpos('Ref5_Switch',act3,'_hBL4UmfJEeO3ssiFDTK-qw'),[identifier(none,gear_retracted)],[boolean_true(none)]),assign(rodinpos('Ref5_Switch',shockabs,'_5RGikWmCEeOLrLY1DXbL2w'),[identifier(none,shock_absorber)],[identifier(none,flight)])],[]),event(rodinpos('Ref5_Switch',env_start_retracting,'_zmqekGctEeOU3Z0T65yXqF'),env_start_retracting,ordinary(none),[env_start_retracting],[],[equal(rodinpos('Ref5_Switch',grd2,'_XbHn4WfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,extended)),equal(rodinpos('Ref5_Switch',grd3,'_fVJfM2fHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref5_Switch',grd4,'_WLnxM364EeOk5IscBNq0oQ'),identifier(none,extend_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref5_Switch',general_valve,'_1cShgXeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref5_Switch',act1,'_XbIO8GfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,gear_moving)]),assign(rodinpos('Ref5_Switch',act3,'_hBMfYGfJEeO3ssiFDTK-qw'),[identifier(none,gear_extended)],[boolean_false(none)])],[]),event(rodinpos('Ref5_Switch',env_start_open_door,'_zmqekGctEeOU3Z0T65yXqG'),env_start_open_door,ordinary(none),[env_start_open_door],[],[equal(rodinpos('Ref5_Switch',grd2,'_XbI2AGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,closed)),equal(rodinpos('Ref5_Switch',grd3,'_fVKGQmfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref5_Switch',grd4,'_WLnxNX64EeOk5IscBNq0oQ'),identifier(none,close_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref5_Switch',general_valve,'_1cTIkHeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref5_Switch',act1,'_XbI2AWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,door_moving)]),assign(rodinpos('Ref5_Switch',act3,'_hBNGcGfJEeO3ssiFDTK-qw'),[identifier(none,door_closed)],[boolean_false(none)])],[]),event(rodinpos('Ref5_Switch',env_open_door,'_zmqekGctEeOU3Z0T65yXqH'),env_open_door,ordinary(none),[env_open_door],[],[equal(rodinpos('Ref5_Switch',grd2,'_XbJdEGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,door_moving)),equal(rodinpos('Ref5_Switch',grd3,'_fVKtUWfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref5_Switch',grd4,'_WLoYQH64EeOk5IscBNq0oQ'),identifier(none,close_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref5_Switch',general_valve,'_1cTIkXeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref5_Switch',act1,'_XbJdEWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,open)]),assign(rodinpos('Ref5_Switch',act3,'_hBNtgWfJEeO3ssiFDTK-qw'),[identifier(none,door_open)],[boolean_true(none)])],[]),event(rodinpos('Ref5_Switch',env_close_door,'_zmqekGctEeOU3Z0T65yXqI'),env_close_door,ordinary(none),[env_close_door],[],[equal(rodinpos('Ref5_Switch',grd2,'_XbKEIWfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,door_moving)),equal(rodinpos('Ref5_Switch',grd3,'_fVKtVGfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref5_Switch',grd4,'_WLoYQn64EeOk5IscBNq0oQ'),identifier(none,open_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref5_Switch',general_valve,'_1cTvoHeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref5_Switch',act1,'_XbKrMGfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,closed)]),assign(rodinpos('Ref5_Switch',act3,'_hBOUkWfJEeO3ssiFDTK-qw'),[identifier(none,door_closed)],[boolean_true(none)])],[]),event(rodinpos('Ref5_Switch',env_start_close_door,'_zmqekGctEeOU3Z0T65yXqJ'),env_start_close_door,ordinary(none),[env_start_close_door],[],[equal(rodinpos('Ref5_Switch',grd1,'_XbLSQGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,open)),equal(rodinpos('Ref5_Switch',grd3,'_fVLUYmfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref5_Switch',grd4,'_WLoYRH64EeOk5IscBNq0oQ'),identifier(none,open_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref5_Switch',general_valve,'_1cTvoXeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref5_Switch',act1,'_XbLSQWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,door_moving)]),assign(rodinpos('Ref5_Switch',act3,'_hBO7oWfJEeO3ssiFDTK-qw'),[identifier(none,door_open)],[boolean_false(none)])],[]),event(rodinpos('Ref5_Switch',env_open_valve_open_door,'_zmqekGctEeOU3Z0T65yXqK'),env_open_valve_open_door,ordinary(none),[env_open_valve_open_door],[],[equal(rodinpos('Ref5_Switch',grd1,'_CreNUWY4EeO7UsfGCD69ng'),identifier(none,open_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref5_Switch',grd3,'_3bBYgn68EeOk5IscBNq0oQ'),identifier(none,open_EV),boolean_true(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_Cre0YGY4EeO7UsfGCD69ng'),[identifier(none,open_door_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref5_Switch',env_close_valve_open_door,'_zmqekGctEeOU3Z0T65yXqL'),env_close_valve_open_door,ordinary(none),[env_close_valve_open_door],[],[equal(rodinpos('Ref5_Switch',grd1,'_0L1aMWfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref5_Switch',grd3,'_3bBYhH68EeOk5IscBNq0oQ'),identifier(none,open_EV),boolean_false(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_0L2BQGfHEeO3ssiFDTK-qw'),[identifier(none,open_door_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref5_Switch',env_open_valve_close_door,'_zmqekGctEeOU3Z0T65yXqM'),env_open_valve_close_door,ordinary(none),[env_open_valve_close_door],[],[equal(rodinpos('Ref5_Switch',grd1,'_0L2BQmfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref5_Switch',grd3,'_3bBYhn68EeOk5IscBNq0oQ'),identifier(none,close_EV),boolean_true(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_0L2BQ2fHEeO3ssiFDTK-qw'),[identifier(none,close_door_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref5_Switch',env_close_valve_close_door,'_zmqekGctEeOU3Z0T65yXqN'),env_close_valve_close_door,ordinary(none),[env_close_valve_close_door],[],[equal(rodinpos('Ref5_Switch',grd1,'_0L2oUWfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref5_Switch',grd2,'_3bBYiH68EeOk5IscBNq0oQ'),identifier(none,close_EV),boolean_false(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_0L2oUmfHEeO3ssiFDTK-qw'),[identifier(none,close_door_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref5_Switch',env_open_valve_retract_gear,'_zmqekGctEeOU3Z0T65yXqO'),env_open_valve_retract_gear,ordinary(none),[env_open_valve_retract_gear],[],[equal(rodinpos('Ref5_Switch',grd1,'_0L3PYGfHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref5_Switch',grd3,'_3bB_kX68EeOk5IscBNq0oQ'),identifier(none,retract_EV),boolean_true(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_0L3PYWfHEeO3ssiFDTK-qw'),[identifier(none,retract_gear_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref5_Switch',env_close_valve_retract_gear,'_zmqekGctEeOU3Z0T65yXqP'),env_close_valve_retract_gear,ordinary(none),[env_close_valve_retract_gear],[],[equal(rodinpos('Ref5_Switch',grd1,'_0L3PY2fHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref5_Switch',grd3,'_3bB_k368EeOk5IscBNq0oQ'),identifier(none,retract_EV),boolean_false(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_0L32cGfHEeO3ssiFDTK-qw'),[identifier(none,retract_gear_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref5_Switch',env_open_valve_extend_gear,'_zmqekGctEeOU3Z0T65yXqQ'),env_open_valve_extend_gear,ordinary(none),[env_open_valve_extend_gear],[],[equal(rodinpos('Ref5_Switch',grd1,'_0L32cmfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref5_Switch',grd3,'_3bB_lX68EeOk5IscBNq0oQ'),identifier(none,extend_EV),boolean_true(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_0L32c2fHEeO3ssiFDTK-qw'),[identifier(none,extend_gear_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref5_Switch',env_close_valve_extend_gear,'_zmqekGctEeOU3Z0T65yXqR'),env_close_valve_extend_gear,ordinary(none),[env_close_valve_extend_gear],[],[equal(rodinpos('Ref5_Switch',grd1,'_0L4dgWfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref5_Switch',grd3,'_3bB_l368EeOk5IscBNq0oQ'),identifier(none,extend_EV),boolean_false(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_0L4dgmfHEeO3ssiFDTK-qw'),[identifier(none,extend_gear_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref5_Switch',con_stimulate_open_door_valve,'_zmqekGctEeOU3Z0T65yXqS'),con_stimulate_open_door_valve,ordinary(none),[con_stimulate_open_door_valve],[],[equal(rodinpos('Ref5_Switch',grd1,'_reokEGfIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_false(none)),equal(rodinpos('Ref5_Switch',grd2,'_reokEWfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_false(none)),disjunct(rodinpos('Ref5_Switch',gear_not_moving,'_Ie4-wGc7EeOU3Z0T65yXqA'),equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,gear_retracted),boolean_true(none))),disjunct(rodinpos('Ref5_Switch',handle,'_FGeEcmfKEeO3ssiFDTK-qw'),conjunct(none,equal(none,identifier(none,gear),identifier(none,extended)),equal(none,identifier(none,handle),identifier(none,up))),conjunct(none,equal(none,identifier(none,gear),identifier(none,retracted)),equal(none,identifier(none,handle),identifier(none,down)))),equal(rodinpos('Ref5_Switch',dooropeningnotlocked,'_dpRxM2ihEeOT_9tDelWe4g'),identifier(none,lock_door_opening),boolean_false(none)),equal(rodinpos('Ref5_Switch',general_ev,'_hcowcHd7EeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_reokEmfIEeO3ssiFDTK-qw'),[identifier(none,open_EV)],[boolean_true(none)]),assign(rodinpos('Ref5_Switch',act,'_Yg1BEGcqEeOIZYXp1CRUOw'),[identifier(none,last_door_action)],[set_extension(none,[identifier(none,open_door_stimulus)])]),assign(rodinpos('Ref5_Switch',act3,'_FGergGfKEeO3ssiFDTK-qw'),[identifier(none,last_handle_state)],[set_extension(none,[identifier(none,handle)])])],[]),event(rodinpos('Ref5_Switch',con_stop_stimulate_open_door_valve,'_zmqekGctEeOU3Z0T65yXqT'),con_stop_stimulate_open_door_valve,ordinary(none),[con_stop_stimulate_open_door_valve],[],[equal(rodinpos('Ref5_Switch',grd1,'_reokFGfIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_true(none)),disjunct(rodinpos('Ref5_Switch',handle,'_FGerg2fKEeO3ssiFDTK-qw'),conjunct(none,equal(none,identifier(none,gear),identifier(none,extended)),equal(none,identifier(none,handle),identifier(none,down))),disjunct(none,conjunct(none,equal(none,identifier(none,gear),identifier(none,retracted)),equal(none,identifier(none,handle),identifier(none,up))),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,handle),identifier(none,up)),conjunct(none,equal(none,identifier(none,door_open),boolean_true(none)),equal(none,identifier(none,shock_absorber),identifier(none,ground))))))),conjunct(rodinpos('Ref5_Switch',grd6,'_FGerhGfKEeO3ssiFDTK-qw'),equal(none,identifier(none,retract_EV),boolean_false(none)),equal(none,identifier(none,extend_EV),boolean_false(none))),equal(rodinpos('Ref5_Switch',general_ev,'_cnpCcHhiEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_repLIGfIEeO3ssiFDTK-qw'),[identifier(none,open_EV)],[boolean_false(none)]),assign(rodinpos('Ref5_Switch',act3,'_FGfSkGfKEeO3ssiFDTK-qw'),[identifier(none,last_handle_state)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'HANDLE_STATE')))]),assign(rodinpos('Ref5_Switch',lockdooropening,'_BlYzMGiiEeOT_9tDelWe4g'),[identifier(none,lock_door_opening)],[boolean_true(none)])],[]),event(rodinpos('Ref5_Switch',con_stimulate_close_door_valve,'_zmqekGctEeOU3Z0T65yXqU'),con_stimulate_close_door_valve,ordinary(none),[con_stimulate_close_door_valve],[],[equal(rodinpos('Ref5_Switch',grd2,'_repLImfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_false(none)),equal(rodinpos('Ref5_Switch',grd1,'_repLI2fIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_false(none)),disjunct(rodinpos('Ref5_Switch',grd,'_oZAasGcqEeOIZYXp1CRUOw'),equal(none,identifier(none,door_closed),boolean_false(none)),equal(none,identifier(none,last_door_action),set_extension(none,[identifier(none,open_door_stimulus)]))),disjunct(rodinpos('Ref5_Switch',gear_not_moving,'_Ie4-wWc7EeOU3Z0T65yXqA'),equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,gear_retracted),boolean_true(none))),disjunct(rodinpos('Ref5_Switch',gear_not_waitingformoving,'_2FwWI2f8EeOan70hsodGWg'),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,handle),identifier(none,down))),disjunct(none,conjunct(none,equal(none,identifier(none,gear_retracted),boolean_true(none)),equal(none,identifier(none,handle),identifier(none,up))),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,handle),identifier(none,up)),equal(none,identifier(none,shock_absorber),identifier(none,ground)))))),equal(rodinpos('Ref5_Switch',general_ev,'_cnpCcXhiEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_repLJGfIEeO3ssiFDTK-qw'),[identifier(none,close_EV)],[boolean_true(none)]),assign(rodinpos('Ref5_Switch',act,'_Yg1oIGcqEeOIZYXp1CRUOw'),[identifier(none,last_door_action)],[set_extension(none,[identifier(none,close_door_stimulus)])]),assign(rodinpos('Ref5_Switch',act3,'_8I6FEGcwEeOU3Z0T65yXqA'),[identifier(none,last_handle_state)],[set_extension(none,[identifier(none,handle)])]),assign(rodinpos('Ref5_Switch',lockdooropening,'_dpSYQWihEeOT_9tDelWe4g'),[identifier(none,lock_door_opening)],[boolean_true(none)])],[]),event(rodinpos('Ref5_Switch',con_stop_stimulate_close_door_valve,'_zmqekGctEeOU3Z0T65yXqV'),con_stop_stimulate_close_door_valve,ordinary(none),[con_stop_stimulate_close_door_valve],[],[equal(rodinpos('Ref5_Switch',grd1,'_repyMWfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_true(none)),disjunct(rodinpos('Ref5_Switch',grd5,'_FGfSk2fKEeO3ssiFDTK-qw'),equal(none,identifier(none,door_closed),boolean_true(none)),conjunct(none,equal(none,identifier(none,door_closed),boolean_false(none)),not_equal(none,identifier(none,last_handle_state),set_extension(none,[identifier(none,handle)])))),equal(rodinpos('Ref5_Switch',general_ev,'_cnppgHhiEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_repyMmfIEeO3ssiFDTK-qw'),[identifier(none,close_EV)],[boolean_false(none)]),assign(rodinpos('Ref5_Switch',act3,'_FGfSlGfKEeO3ssiFDTK-qw'),[identifier(none,last_handle_state)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'HANDLE_STATE')))])],[]),event(rodinpos('Ref5_Switch',con_stimulate_retract_gear_valve,'_zmqekGctEeOU3Z0T65yXqW'),con_stimulate_retract_gear_valve,ordinary(none),[con_stimulate_retract_gear_valve],[],[equal(rodinpos('Ref5_Switch',grd1,'_repyNGfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_false(none)),equal(rodinpos('Ref5_Switch',grd2,'_reqZQGfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_false(none)),equal(rodinpos('Ref5_Switch',grd3,'_ssC38GgAEeOan70hsodGWg'),identifier(none,open_EV),boolean_true(none)),equal(rodinpos('Ref5_Switch',door,'_hBR-8GfJEeO3ssiFDTK-qw'),identifier(none,door_open),boolean_true(none)),disjunct(rodinpos('Ref5_Switch',grd4,'_hBR-8WfJEeO3ssiFDTK-qw'),equal(none,identifier(none,gear_retracted),boolean_false(none)),conjunct(none,equal(none,identifier(none,gear_retracted),boolean_true(none)),equal(none,identifier(none,last_gear_action),set_extension(none,[identifier(none,extend_gear_stimulus)])))),equal(rodinpos('Ref5_Switch',grd7,'_FGf5omfKEeO3ssiFDTK-qw'),identifier(none,handle),identifier(none,up)),disjunct(rodinpos('Ref5_Switch',grd8,'_h3dFgImVEeOQc6S3EYezPA'),equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,gear_extended),boolean_false(none)),not_equal(none,identifier(none,last_handle_state),set_extension(none,[identifier(none,handle)])))),equal(rodinpos('Ref5_Switch',groundguard,'_dpSYRGihEeOT_9tDelWe4g'),identifier(none,shock_absorber),identifier(none,flight)),equal(rodinpos('Ref5_Switch',general_ev,'_cnppgXhiEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_reqZQmfIEeO3ssiFDTK-qw'),[identifier(none,retract_EV)],[boolean_true(none)]),assign(rodinpos('Ref5_Switch',act,'_hBR-8mfJEeO3ssiFDTK-qw'),[identifier(none,last_gear_action)],[set_extension(none,[identifier(none,retract_gear_stimulus)])])],[]),event(rodinpos('Ref5_Switch',con_stop_stimulate_retract_gear_valve,'_zmqekGctEeOU3Z0T65yXqX'),con_stop_stimulate_retract_gear_valve,ordinary(none),[con_stop_stimulate_retract_gear_valve],[],[equal(rodinpos('Ref5_Switch',grd1,'_reqZRGfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_true(none)),disjunct(rodinpos('Ref5_Switch',grd,'_FGggsGfKEeO3ssiFDTK-qw'),equal(none,identifier(none,gear_retracted),boolean_true(none)),conjunct(none,equal(none,identifier(none,gear_retracted),boolean_false(none)),equal(none,identifier(none,handle),identifier(none,down)))),equal(rodinpos('Ref5_Switch',general_ev,'_cnppgnhiEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_reqZRWfIEeO3ssiFDTK-qw'),[identifier(none,retract_EV)],[boolean_false(none)])],[]),event(rodinpos('Ref5_Switch',con_stimulate_extend_gear_valve,'_zmqekGctEeOU3Z0T65yXqY'),con_stimulate_extend_gear_valve,ordinary(none),[con_stimulate_extend_gear_valve],[],[equal(rodinpos('Ref5_Switch',grd1,'_rerAUWfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_false(none)),equal(rodinpos('Ref5_Switch',grd2,'_rerAUmfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_false(none)),equal(rodinpos('Ref5_Switch',grd3,'_ssDfAGgAEeOan70hsodGWg'),identifier(none,open_EV),boolean_true(none)),equal(rodinpos('Ref5_Switch',door,'_hBSmAWfJEeO3ssiFDTK-qw'),identifier(none,door_open),boolean_true(none)),disjunct(rodinpos('Ref5_Switch',grd,'_hBSmAmfJEeO3ssiFDTK-qw'),equal(none,identifier(none,gear_extended),boolean_false(none)),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,last_gear_action),set_extension(none,[identifier(none,retract_gear_stimulus)])))),equal(rodinpos('Ref5_Switch',grd7,'_FGggs2fKEeO3ssiFDTK-qw'),identifier(none,handle),identifier(none,down)),disjunct(rodinpos('Ref5_Switch',grd8,'_akrbcImVEeOQc6S3EYezPA'),equal(none,identifier(none,gear_retracted),boolean_true(none)),conjunct(none,equal(none,identifier(none,gear_retracted),boolean_false(none)),not_equal(none,identifier(none,last_handle_state),set_extension(none,[identifier(none,handle)])))),equal(rodinpos('Ref5_Switch',general_ev,'_cnqQkHhiEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_rerAVGfIEeO3ssiFDTK-qw'),[identifier(none,extend_EV)],[boolean_true(none)]),assign(rodinpos('Ref5_Switch',act,'_hBSmA2fJEeO3ssiFDTK-qw'),[identifier(none,last_gear_action)],[set_extension(none,[identifier(none,extend_gear_stimulus)])])],[]),event(rodinpos('Ref5_Switch',con_stop_stimulate_extend_gear_valve,'_zmqekGctEeOU3Z0T65yXqZ'),con_stop_stimulate_extend_gear_valve,ordinary(none),[con_stop_stimulate_extend_gear_valve],[],[equal(rodinpos('Ref5_Switch',grd2,'_rernYWfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_true(none)),disjunct(rodinpos('Ref5_Switch',grd,'_FGhHwWfKEeO3ssiFDTK-qw'),equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,gear_extended),boolean_false(none)),equal(none,identifier(none,handle),identifier(none,up)))),equal(rodinpos('Ref5_Switch',general_ev,'_cnqQkXhiEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none))],[],[assign(rodinpos('Ref5_Switch',act1,'_rernYmfIEeO3ssiFDTK-qw'),[identifier(none,extend_EV)],[boolean_false(none)])],[]),event(rodinpos('Ref5_Switch',env_toggle_handle,'_zmqekGctEeOU3Z0T65yXq['),env_toggle_handle,ordinary(none),[env_toggle_handle],[],[],[],[becomes_element_of(rodinpos('Ref5_Switch',act,'_FGhHw2fKEeO3ssiFDTK-qw'),[identifier(none,handle)],set_subtraction(none,identifier(none,'HANDLE_STATE'),set_extension(none,[identifier(none,handle)]))),assign(rodinpos('Ref5_Switch',removegroundlocking,'_dpS_U2ihEeOT_9tDelWe4g'),[identifier(none,lock_door_opening)],[boolean_false(none)]),assign(rodinpos('Ref5_Switch',handle_move,'_XRGwkHd7EeOBXrBZ8EbeCQ'),[identifier(none,handle_move)],[boolean_true(none)])],[]),event(rodinpos('Ref5_Switch',env_changeShockAbsorber,'_zmqekGctEeOU3Z0T65yXq\\'),env_changeShockAbsorber,ordinary(none),[env_changeShockAbsorber],[],[equal(rodinpos('Ref5_Switch',grd,'_5RdH4GmCEeOLrLY1DXbL2w'),identifier(none,gear_retracted),boolean_false(none))],[],[becomes_element_of(rodinpos('Ref5_Switch',act,'_5RdH4WmCEeOLrLY1DXbL2w'),[identifier(none,shock_absorber)],set_subtraction(none,identifier(none,'PLANE_STATE'),set_extension(none,[identifier(none,shock_absorber)])))],[]),event(rodinpos('Ref5_Switch',con_stimulate_general_valve,'_lqzPcHd6EeOBXrBZ8EbeCQ'),con_stimulate_general_valve,ordinary(none),[],[],[equal(rodinpos('Ref5_Switch',grd1,'_lqz2gHd6EeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_false(none)),equal(rodinpos('Ref5_Switch',grd2,'_ZxSOUHd7EeOBXrBZ8EbeCQ'),identifier(none,handle_move),boolean_true(none))],[],[assign(rodinpos('Ref5_Switch',act,'_lqz2gXd6EeOBXrBZ8EbeCQ'),[identifier(none,general_EV)],[boolean_true(none)])],[]),event(rodinpos('Ref5_Switch',con_stop_stimulate_general_valve,'_1tvf4XeAEeOBXrBZ8EbeCQ'),con_stop_stimulate_general_valve,ordinary(none),[],[],[equal(rodinpos('Ref5_Switch',grd1,'_1tvf4neAEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none)),disjunct(rodinpos('Ref5_Switch',grd2,'_1tvf43eAEeOBXrBZ8EbeCQ'),conjunct(none,equal(none,identifier(none,handle),identifier(none,up)),conjunct(none,equal(none,identifier(none,gear_retracted),boolean_true(none)),conjunct(none,equal(none,identifier(none,door_closed),boolean_true(none)),conjunct(none,equal(none,identifier(none,close_EV),boolean_false(none)),equal(none,identifier(none,open_EV),boolean_false(none)))))),disjunct(none,conjunct(none,equal(none,identifier(none,handle),identifier(none,down)),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,door_closed),boolean_true(none)),conjunct(none,equal(none,identifier(none,close_EV),boolean_false(none)),conjunct(none,equal(none,identifier(none,open_EV),boolean_false(none)),conjunct(none,equal(none,identifier(none,last_handle_state),typeof(none,empty_set(none),pow_subset(none,identifier(none,'HANDLE_STATE')))),conjunct(none,equal(none,identifier(none,lock_door_opening),boolean_false(none)),equal(none,identifier(none,last_door_action),set_extension(none,[identifier(none,close_door_stimulus)]))))))))),conjunct(none,equal(none,identifier(none,handle),identifier(none,up)),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,door_closed),boolean_true(none)),conjunct(none,equal(none,identifier(none,close_EV),boolean_false(none)),conjunct(none,equal(none,identifier(none,open_EV),boolean_false(none)),equal(none,identifier(none,lock_door_opening),boolean_true(none)))))))))],[],[assign(rodinpos('Ref5_Switch',act,'_1twG8HeAEeOBXrBZ8EbeCQ'),[identifier(none,general_EV)],[boolean_false(none)]),assign(rodinpos('Ref5_Switch',act2,'_vW6-YHeZEeOBXrBZ8EbeCQ'),[identifier(none,handle_move)],[boolean_false(none)])],[]),event(rodinpos('Ref5_Switch',evn_open_general_valve,'_7tRckneEEeOBXrBZ8EbeCQ'),evn_open_general_valve,ordinary(none),[],[],[equal(rodinpos('Ref5_Switch',grd1,'_7tSDoHeEEeOBXrBZ8EbeCQ'),identifier(none,general_EV),boolean_true(none)),equal(rodinpos('Ref5_Switch',grd2,'_7tSDoXeEEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_closed)),equal(rodinpos('Ref5_Switch',grd3,'_LY1xAHeaEeOBXrBZ8EbeCQ'),identifier(none,analogical_switch),identifier(none,switch_closed))],[],[assign(rodinpos('Ref5_Switch',act,'_JzFgsHeFEeOBXrBZ8EbeCQ'),[identifier(none,general_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref5_Switch',evn_close_general_valve,'_ONp-0HeWEeOBXrBZ8EbeCQ'),evn_close_general_valve,ordinary(none),[],[],[disjunct(rodinpos('Ref5_Switch',grd1,'_ONp-0XeWEeOBXrBZ8EbeCQ'),equal(none,identifier(none,general_EV),boolean_false(none)),equal(none,identifier(none,analogical_switch),identifier(none,switch_open))),equal(rodinpos('Ref5_Switch',grd2,'_ONql4HeWEeOBXrBZ8EbeCQ'),identifier(none,general_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref5_Switch',act,'_ONql4XeWEeOBXrBZ8EbeCQ'),[identifier(none,general_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref5_Switch',env_close_switch,'_vW8MgHeZEeOBXrBZ8EbeCQ'),env_close_switch,ordinary(none),[],[],[equal(rodinpos('Ref5_Switch',grd1,'_vW8MgXeZEeOBXrBZ8EbeCQ'),identifier(none,analogical_switch),identifier(none,switch_open)),equal(rodinpos('Ref5_Switch',grd2,'_vW8zkHeZEeOBXrBZ8EbeCQ'),identifier(none,handle_move),boolean_true(none))],[],[assign(rodinpos('Ref5_Switch',act,'_vW8zkXeZEeOBXrBZ8EbeCQ'),[identifier(none,analogical_switch)],[identifier(none,switch_closed)])],[]),event(rodinpos('Ref5_Switch',env_open_switch,'_4awWYHeZEeOBXrBZ8EbeCQ'),env_open_switch,ordinary(none),[],[],[equal(rodinpos('Ref5_Switch',grd1,'_4awWYXeZEeOBXrBZ8EbeCQ'),identifier(none,analogical_switch),identifier(none,switch_closed))],[],[assign(rodinpos('Ref5_Switch',act,'_4aw9cHeZEeOBXrBZ8EbeCQ'),[identifier(none,analogical_switch)],[identifier(none,switch_open)])],[])])]),event_b_model(none,'Ref4_ControllerHandle',[sees(none,['Context0','Context1','Context2']),refines(none,'Ref3_ControllerSensors'),variables(none,[identifier(none,close_EV),identifier(none,close_door_valve),identifier(none,door),identifier(none,door_closed),identifier(none,door_open),identifier(none,extend_EV),identifier(none,extend_gear_valve),identifier(none,gear),identifier(none,gear_extended),identifier(none,gear_retracted),identifier(none,handle),identifier(none,last_door_action),identifier(none,last_gear_action),identifier(none,last_handle_state),identifier(none,lock_door_opening),identifier(none,open_EV),identifier(none,open_door_valve),identifier(none,retract_EV),identifier(none,retract_gear_valve),identifier(none,shock_absorber)]),invariant(none,[member(rodinpos('Ref4_ControllerHandle',handle,'_zcRnwGcSEeO7UsfGCD69ng'),identifier(none,handle),identifier(none,'HANDLE_STATE')),member(rodinpos('Ref4_ControllerHandle',handle2,'_Lsb50WcwEeOU3Z0T65yXqA'),identifier(none,last_handle_state),pow_subset(none,identifier(none,'HANDLE_STATE'))),conjunct(rodinpos('Ref4_ControllerHandle',handle3,'_RCXcsGcwEeOU3Z0T65yXqA'),finite(none,identifier(none,last_handle_state)),less(none,card(none,identifier(none,last_handle_state)),integer(none,2))),member(rodinpos('Ref4_ControllerHandle',ground,'_d1pOsGigEeOT_9tDelWe4g'),identifier(none,shock_absorber),identifier(none,'PLANE_STATE')),member(rodinpos('Ref4_ControllerHandle',groundlock,'_dpPU8GihEeOT_9tDelWe4g'),identifier(none,lock_door_opening),bool_set(none)),implication(rodinpos('Ref4_ControllerHandle',r31simple,'_ZEclwIj7EeOQc6S3EYezPA'),disjunct(none,equal(none,identifier(none,extend_EV),boolean_true(none)),equal(none,identifier(none,retract_EV),boolean_true(none))),equal(none,identifier(none,open_EV),boolean_true(none)))]),theorems(none,[]),events(none,[event(rodinpos('Ref4_ControllerHandle','INITIALISATION','_xET6kWcBEeO7UsfGCD69nh'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_Y7EY0GY0EeO7UsfGCD69ng'),[identifier(none,gear)],[identifier(none,extended)]),assign(rodinpos('Ref4_ControllerHandle',act2,'_KkdfoGY0EeO7UsfGCD69ng'),[identifier(none,door)],[identifier(none,closed)]),assign(rodinpos('Ref4_ControllerHandle',close_door_valve,'_yQPxAGY3EeO7UsfGCD69ng'),[identifier(none,close_door_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref4_ControllerHandle',open_door_valve,'_yQPxAWY3EeO7UsfGCD69ng'),[identifier(none,open_door_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref4_ControllerHandle',retract_gear_valve,'_yQQYEGY3EeO7UsfGCD69ng'),[identifier(none,retract_gear_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref4_ControllerHandle',extend_gear_valve,'_yQQYEWY3EeO7UsfGCD69ng'),[identifier(none,extend_gear_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref4_ControllerHandle',open_EV,'_xEJigGcBEeO7UsfGCD69ng'),[identifier(none,open_EV)],[boolean_false(none)]),assign(rodinpos('Ref4_ControllerHandle',close_EV,'_xEKJkGcBEeO7UsfGCD69ng'),[identifier(none,close_EV)],[boolean_false(none)]),assign(rodinpos('Ref4_ControllerHandle',retract_EV,'_PLAoYGcCEeO7UsfGCD69ng'),[identifier(none,retract_EV)],[boolean_false(none)]),assign(rodinpos('Ref4_ControllerHandle',extend_EV,'_PLAoYWcCEeO7UsfGCD69ng'),[identifier(none,extend_EV)],[boolean_false(none)]),assign(rodinpos('Ref4_ControllerHandle',door_closed,'_soNwcGcGEeO7UsfGCD69ng'),[identifier(none,door_closed)],[boolean_true(none)]),assign(rodinpos('Ref4_ControllerHandle',door_open,'_soNwcWcGEeO7UsfGCD69ng'),[identifier(none,door_open)],[boolean_false(none)]),assign(rodinpos('Ref4_ControllerHandle',gear_extended,'_soNwcmcGEeO7UsfGCD69ng'),[identifier(none,gear_extended)],[boolean_true(none)]),assign(rodinpos('Ref4_ControllerHandle',gear_retracted,'_soNwc2cGEeO7UsfGCD69ng'),[identifier(none,gear_retracted)],[boolean_false(none)]),assign(rodinpos('Ref4_ControllerHandle',last_door_action,'_pmSioWcpEeOIZYXp1CRUOw'),[identifier(none,last_door_action)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'STIMULI')))]),assign(rodinpos('Ref4_ControllerHandle',last_gear_action,'_cRkAYGctEeOU3Z0T65yXqA'),[identifier(none,last_gear_action)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'STIMULI')))]),assign(rodinpos('Ref4_ControllerHandle',handle,'_68JSoGcSEeO7UsfGCD69ng'),[identifier(none,handle)],[identifier(none,down)]),assign(rodinpos('Ref4_ControllerHandle',handle2,'_RCQvAGcwEeOU3Z0T65yXqA'),[identifier(none,last_handle_state)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'HANDLE_STATE')))]),assign(rodinpos('Ref4_ControllerHandle',ground,'_d1sSAGigEeOT_9tDelWe4g'),[identifier(none,shock_absorber)],[identifier(none,flight)]),assign(rodinpos('Ref4_ControllerHandle',groundlock,'_dpP8AGihEeOT_9tDelWe4g'),[identifier(none,lock_door_opening)],[boolean_false(none)])],[]),event(rodinpos('Ref4_ControllerHandle',env_start_extending,'_93_EgGfJEeO3ssiFDTK-qw'),env_start_extending,ordinary(none),[env_start_extending],[],[equal(rodinpos('Ref4_ControllerHandle',grd2,'_XbFLomfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,retracted)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_fVIREmfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref4_ControllerHandle',grd4,'_WLnKIX64EeOk5IscBNq0oQ'),identifier(none,retract_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_XbFysGfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,gear_moving)]),assign(rodinpos('Ref4_ControllerHandle',act3,'_hBLRQmfJEeO3ssiFDTK-qw'),[identifier(none,gear_retracted)],[boolean_false(none)])],[]),event(rodinpos('Ref4_ControllerHandle',env_extend_gear,'_93_EgmfJEeO3ssiFDTK-qw'),env_extend_gear,ordinary(none),[env_extend_gear],[],[equal(rodinpos('Ref4_ControllerHandle',grd2,'_XbGZwGfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,gear_moving)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_fVI4IWfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref4_ControllerHandle',grd4,'_WLnKI364EeOk5IscBNq0oQ'),identifier(none,retract_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_XbGZwWfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,extended)]),assign(rodinpos('Ref4_ControllerHandle',act3,'_hBLRRWfJEeO3ssiFDTK-qw'),[identifier(none,gear_extended)],[boolean_true(none)])],[]),event(rodinpos('Ref4_ControllerHandle',env_retract_gear,'_93_rkWfJEeO3ssiFDTK-qw'),env_retract_gear,ordinary(none),[env_retract_gear],[],[equal(rodinpos('Ref4_ControllerHandle',grd2,'_XbHA0WfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,gear_moving)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_fVJfMGfHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref4_ControllerHandle',grd4,'_WLnxMX64EeOk5IscBNq0oQ'),identifier(none,extend_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_XbHA0mfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,retracted)]),assign(rodinpos('Ref4_ControllerHandle',act3,'_hBL4UmfJEeO3ssiFDTK-qw'),[identifier(none,gear_retracted)],[boolean_true(none)]),assign(rodinpos('Ref4_ControllerHandle',shockabs,'_5RGikWmCEeOLrLY1DXbL2w'),[identifier(none,shock_absorber)],[identifier(none,flight)])],[]),event(rodinpos('Ref4_ControllerHandle',env_start_retracting,'_93_rk2fJEeO3ssiFDTK-qw'),env_start_retracting,ordinary(none),[env_start_retracting],[],[equal(rodinpos('Ref4_ControllerHandle',grd2,'_XbHn4WfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,extended)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_fVJfM2fHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref4_ControllerHandle',grd4,'_WLnxM364EeOk5IscBNq0oQ'),identifier(none,extend_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_XbIO8GfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,gear_moving)]),assign(rodinpos('Ref4_ControllerHandle',act3,'_hBMfYGfJEeO3ssiFDTK-qw'),[identifier(none,gear_extended)],[boolean_false(none)])],[]),event(rodinpos('Ref4_ControllerHandle',env_start_open_door,'_94ASoWfJEeO3ssiFDTK-qw'),env_start_open_door,ordinary(none),[env_start_open_door],[],[equal(rodinpos('Ref4_ControllerHandle',grd2,'_XbI2AGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,closed)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_fVKGQmfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref4_ControllerHandle',grd4,'_WLnxNX64EeOk5IscBNq0oQ'),identifier(none,close_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_XbI2AWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,door_moving)]),assign(rodinpos('Ref4_ControllerHandle',act3,'_hBNGcGfJEeO3ssiFDTK-qw'),[identifier(none,door_closed)],[boolean_false(none)])],[]),event(rodinpos('Ref4_ControllerHandle',env_open_door,'_94ASo2fJEeO3ssiFDTK-qw'),env_open_door,ordinary(none),[env_open_door],[],[equal(rodinpos('Ref4_ControllerHandle',grd2,'_XbJdEGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,door_moving)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_fVKtUWfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref4_ControllerHandle',grd4,'_WLoYQH64EeOk5IscBNq0oQ'),identifier(none,close_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_XbJdEWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,open)]),assign(rodinpos('Ref4_ControllerHandle',act3,'_hBNtgWfJEeO3ssiFDTK-qw'),[identifier(none,door_open)],[boolean_true(none)])],[]),event(rodinpos('Ref4_ControllerHandle',env_close_door,'_94ASpWfJEeO3ssiFDTK-qw'),env_close_door,ordinary(none),[env_close_door],[],[equal(rodinpos('Ref4_ControllerHandle',grd2,'_XbKEIWfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,door_moving)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_fVKtVGfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref4_ControllerHandle',grd4,'_WLoYQn64EeOk5IscBNq0oQ'),identifier(none,open_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_XbKrMGfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,closed)]),assign(rodinpos('Ref4_ControllerHandle',act3,'_hBOUkWfJEeO3ssiFDTK-qw'),[identifier(none,door_closed)],[boolean_true(none)])],[]),event(rodinpos('Ref4_ControllerHandle',env_start_close_door,'_94A5sWfJEeO3ssiFDTK-qw'),env_start_close_door,ordinary(none),[env_start_close_door],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_XbLSQGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,open)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_fVLUYmfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref4_ControllerHandle',grd4,'_WLoYRH64EeOk5IscBNq0oQ'),identifier(none,open_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_XbLSQWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,door_moving)]),assign(rodinpos('Ref4_ControllerHandle',act3,'_hBO7oWfJEeO3ssiFDTK-qw'),[identifier(none,door_open)],[boolean_false(none)])],[]),event(rodinpos('Ref4_ControllerHandle',env_open_valve_open_door,'_94A5s2fJEeO3ssiFDTK-qw'),env_open_valve_open_door,ordinary(none),[env_open_valve_open_door],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_CreNUWY4EeO7UsfGCD69ng'),identifier(none,open_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_3bBYgn68EeOk5IscBNq0oQ'),identifier(none,open_EV),boolean_true(none))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_Cre0YGY4EeO7UsfGCD69ng'),[identifier(none,open_door_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref4_ControllerHandle',env_close_valve_open_door,'_94BgwWfJEeO3ssiFDTK-qw'),env_close_valve_open_door,ordinary(none),[env_close_valve_open_door],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_0L1aMWfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_3bBYhH68EeOk5IscBNq0oQ'),identifier(none,open_EV),boolean_false(none))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_0L2BQGfHEeO3ssiFDTK-qw'),[identifier(none,open_door_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref4_ControllerHandle',env_open_valve_close_door,'_94Bgw2fJEeO3ssiFDTK-qw'),env_open_valve_close_door,ordinary(none),[env_open_valve_close_door],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_0L2BQmfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_3bBYhn68EeOk5IscBNq0oQ'),identifier(none,close_EV),boolean_true(none))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_0L2BQ2fHEeO3ssiFDTK-qw'),[identifier(none,close_door_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref4_ControllerHandle',env_close_valve_close_door,'_94BgxWfJEeO3ssiFDTK-qw'),env_close_valve_close_door,ordinary(none),[env_close_valve_close_door],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_0L2oUWfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref4_ControllerHandle',grd2,'_3bBYiH68EeOk5IscBNq0oQ'),identifier(none,close_EV),boolean_false(none))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_0L2oUmfHEeO3ssiFDTK-qw'),[identifier(none,close_door_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref4_ControllerHandle',env_open_valve_retract_gear,'_94CH0WfJEeO3ssiFDTK-qw'),env_open_valve_retract_gear,ordinary(none),[env_open_valve_retract_gear],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_0L3PYGfHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_3bB_kX68EeOk5IscBNq0oQ'),identifier(none,retract_EV),boolean_true(none))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_0L3PYWfHEeO3ssiFDTK-qw'),[identifier(none,retract_gear_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref4_ControllerHandle',env_close_valve_retract_gear,'_94CH02fJEeO3ssiFDTK-qw'),env_close_valve_retract_gear,ordinary(none),[env_close_valve_retract_gear],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_0L3PY2fHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_3bB_k368EeOk5IscBNq0oQ'),identifier(none,retract_EV),boolean_false(none))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_0L32cGfHEeO3ssiFDTK-qw'),[identifier(none,retract_gear_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref4_ControllerHandle',env_open_valve_extend_gear,'_94Cu4WfJEeO3ssiFDTK-qw'),env_open_valve_extend_gear,ordinary(none),[env_open_valve_extend_gear],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_0L32cmfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_3bB_lX68EeOk5IscBNq0oQ'),identifier(none,extend_EV),boolean_true(none))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_0L32c2fHEeO3ssiFDTK-qw'),[identifier(none,extend_gear_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref4_ControllerHandle',env_close_valve_extend_gear,'_94Cu42fJEeO3ssiFDTK-qw'),env_close_valve_extend_gear,ordinary(none),[env_close_valve_extend_gear],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_0L4dgWfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_3bB_l368EeOk5IscBNq0oQ'),identifier(none,extend_EV),boolean_false(none))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_0L4dgmfHEeO3ssiFDTK-qw'),[identifier(none,extend_gear_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref4_ControllerHandle',con_stimulate_open_door_valve,'_FGeEcGfKEeO3ssiFDTK-qw'),con_stimulate_open_door_valve,ordinary(none),[con_stimulate_open_door_valve],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_reokEGfIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_false(none)),equal(rodinpos('Ref4_ControllerHandle',grd2,'_reokEWfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_false(none)),disjunct(rodinpos('Ref4_ControllerHandle',gear_not_moving,'_Ie4-wGc7EeOU3Z0T65yXqA'),equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,gear_retracted),boolean_true(none))),disjunct(rodinpos('Ref4_ControllerHandle',handle,'_FGeEcmfKEeO3ssiFDTK-qw'),conjunct(none,equal(none,identifier(none,gear),identifier(none,extended)),equal(none,identifier(none,handle),identifier(none,up))),conjunct(none,equal(none,identifier(none,gear),identifier(none,retracted)),equal(none,identifier(none,handle),identifier(none,down)))),equal(rodinpos('Ref4_ControllerHandle',dooropeningnotlocked,'_dpRxM2ihEeOT_9tDelWe4g'),identifier(none,lock_door_opening),boolean_false(none))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_reokEmfIEeO3ssiFDTK-qw'),[identifier(none,open_EV)],[boolean_true(none)]),assign(rodinpos('Ref4_ControllerHandle',act,'_Yg1BEGcqEeOIZYXp1CRUOw'),[identifier(none,last_door_action)],[set_extension(none,[identifier(none,open_door_stimulus)])]),assign(rodinpos('Ref4_ControllerHandle',act3,'_FGergGfKEeO3ssiFDTK-qw'),[identifier(none,last_handle_state)],[set_extension(none,[identifier(none,handle)])])],[]),event(rodinpos('Ref4_ControllerHandle',con_stop_stimulate_open_door_valve,'_FGergWfKEeO3ssiFDTK-qw'),con_stop_stimulate_open_door_valve,ordinary(none),[con_stop_stimulate_open_door_valve],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_reokFGfIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_true(none)),disjunct(rodinpos('Ref4_ControllerHandle',handle,'_FGerg2fKEeO3ssiFDTK-qw'),conjunct(none,equal(none,identifier(none,gear),identifier(none,extended)),equal(none,identifier(none,handle),identifier(none,down))),disjunct(none,conjunct(none,equal(none,identifier(none,gear),identifier(none,retracted)),equal(none,identifier(none,handle),identifier(none,up))),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,handle),identifier(none,up)),conjunct(none,equal(none,identifier(none,door_open),boolean_true(none)),equal(none,identifier(none,shock_absorber),identifier(none,ground))))))),conjunct(rodinpos('Ref4_ControllerHandle',grd6,'_FGerhGfKEeO3ssiFDTK-qw'),equal(none,identifier(none,retract_EV),boolean_false(none)),equal(none,identifier(none,extend_EV),boolean_false(none)))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_repLIGfIEeO3ssiFDTK-qw'),[identifier(none,open_EV)],[boolean_false(none)]),assign(rodinpos('Ref4_ControllerHandle',act3,'_FGfSkGfKEeO3ssiFDTK-qw'),[identifier(none,last_handle_state)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'HANDLE_STATE')))]),assign(rodinpos('Ref4_ControllerHandle',lockdooropening,'_BlYzMGiiEeOT_9tDelWe4g'),[identifier(none,lock_door_opening)],[boolean_true(none)])],[]),event(rodinpos('Ref4_ControllerHandle',con_stimulate_close_door_valve,'_xET6kWcBEeO7UsfGCD69n{'),con_stimulate_close_door_valve,ordinary(none),[con_stimulate_close_door_valve],[],[equal(rodinpos('Ref4_ControllerHandle',grd2,'_repLImfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_false(none)),equal(rodinpos('Ref4_ControllerHandle',grd1,'_repLI2fIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_false(none)),disjunct(rodinpos('Ref4_ControllerHandle',grd,'_oZAasGcqEeOIZYXp1CRUOw'),equal(none,identifier(none,door_closed),boolean_false(none)),equal(none,identifier(none,last_door_action),set_extension(none,[identifier(none,open_door_stimulus)]))),disjunct(rodinpos('Ref4_ControllerHandle',gear_not_moving,'_Ie4-wWc7EeOU3Z0T65yXqA'),equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,gear_retracted),boolean_true(none))),disjunct(rodinpos('Ref4_ControllerHandle',gear_not_waitingformoving,'_2FwWI2f8EeOan70hsodGWg'),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,handle),identifier(none,down))),disjunct(none,conjunct(none,equal(none,identifier(none,gear_retracted),boolean_true(none)),equal(none,identifier(none,handle),identifier(none,up))),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,handle),identifier(none,up)),equal(none,identifier(none,shock_absorber),identifier(none,ground))))))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_repLJGfIEeO3ssiFDTK-qw'),[identifier(none,close_EV)],[boolean_true(none)]),assign(rodinpos('Ref4_ControllerHandle',act,'_Yg1oIGcqEeOIZYXp1CRUOw'),[identifier(none,last_door_action)],[set_extension(none,[identifier(none,close_door_stimulus)])]),assign(rodinpos('Ref4_ControllerHandle',act3,'_8I6FEGcwEeOU3Z0T65yXqA'),[identifier(none,last_handle_state)],[set_extension(none,[identifier(none,handle)])]),assign(rodinpos('Ref4_ControllerHandle',lockdooropening,'_dpSYQWihEeOT_9tDelWe4g'),[identifier(none,lock_door_opening)],[boolean_true(none)])],[]),event(rodinpos('Ref4_ControllerHandle',con_stop_stimulate_close_door_valve,'_FGfSkWfKEeO3ssiFDTK-qw'),con_stop_stimulate_close_door_valve,ordinary(none),[con_stop_stimulate_close_door_valve],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_repyMWfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_true(none)),disjunct(rodinpos('Ref4_ControllerHandle',grd5,'_FGfSk2fKEeO3ssiFDTK-qw'),equal(none,identifier(none,door_closed),boolean_true(none)),conjunct(none,equal(none,identifier(none,door_closed),boolean_false(none)),not_equal(none,identifier(none,last_handle_state),set_extension(none,[identifier(none,handle)]))))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_repyMmfIEeO3ssiFDTK-qw'),[identifier(none,close_EV)],[boolean_false(none)]),assign(rodinpos('Ref4_ControllerHandle',act3,'_FGfSlGfKEeO3ssiFDTK-qw'),[identifier(none,last_handle_state)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'HANDLE_STATE')))])],[]),event(rodinpos('Ref4_ControllerHandle',con_stimulate_retract_gear_valve,'_FGf5oGfKEeO3ssiFDTK-qw'),con_stimulate_retract_gear_valve,ordinary(none),[con_stimulate_retract_gear_valve],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_repyNGfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_false(none)),equal(rodinpos('Ref4_ControllerHandle',grd2,'_reqZQGfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_false(none)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_ssC38GgAEeOan70hsodGWg'),identifier(none,open_EV),boolean_true(none)),equal(rodinpos('Ref4_ControllerHandle',door,'_hBR-8GfJEeO3ssiFDTK-qw'),identifier(none,door_open),boolean_true(none)),disjunct(rodinpos('Ref4_ControllerHandle',grd4,'_hBR-8WfJEeO3ssiFDTK-qw'),equal(none,identifier(none,gear_retracted),boolean_false(none)),conjunct(none,equal(none,identifier(none,gear_retracted),boolean_true(none)),equal(none,identifier(none,last_gear_action),set_extension(none,[identifier(none,extend_gear_stimulus)])))),equal(rodinpos('Ref4_ControllerHandle',grd7,'_FGf5omfKEeO3ssiFDTK-qw'),identifier(none,handle),identifier(none,up)),disjunct(rodinpos('Ref4_ControllerHandle',grd8,'_h3dFgImVEeOQc6S3EYezPA'),equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,gear_extended),boolean_false(none)),not_equal(none,identifier(none,last_handle_state),set_extension(none,[identifier(none,handle)])))),equal(rodinpos('Ref4_ControllerHandle',groundguard,'_dpSYRGihEeOT_9tDelWe4g'),identifier(none,shock_absorber),identifier(none,flight))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_reqZQmfIEeO3ssiFDTK-qw'),[identifier(none,retract_EV)],[boolean_true(none)]),assign(rodinpos('Ref4_ControllerHandle',act,'_hBR-8mfJEeO3ssiFDTK-qw'),[identifier(none,last_gear_action)],[set_extension(none,[identifier(none,retract_gear_stimulus)])])],[]),event(rodinpos('Ref4_ControllerHandle',con_stop_stimulate_retract_gear_valve,'_FGf5o2fKEeO3ssiFDTK-qw'),con_stop_stimulate_retract_gear_valve,ordinary(none),[con_stop_stimulate_retract_gear_valve],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_reqZRGfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_true(none)),disjunct(rodinpos('Ref4_ControllerHandle',grd,'_FGggsGfKEeO3ssiFDTK-qw'),equal(none,identifier(none,gear_retracted),boolean_true(none)),conjunct(none,equal(none,identifier(none,gear_retracted),boolean_false(none)),equal(none,identifier(none,handle),identifier(none,down))))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_reqZRWfIEeO3ssiFDTK-qw'),[identifier(none,retract_EV)],[boolean_false(none)])],[]),event(rodinpos('Ref4_ControllerHandle',con_stimulate_extend_gear_valve,'_FGggsWfKEeO3ssiFDTK-qw'),con_stimulate_extend_gear_valve,ordinary(none),[con_stimulate_extend_gear_valve],[],[equal(rodinpos('Ref4_ControllerHandle',grd1,'_rerAUWfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_false(none)),equal(rodinpos('Ref4_ControllerHandle',grd2,'_rerAUmfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_false(none)),equal(rodinpos('Ref4_ControllerHandle',grd3,'_ssDfAGgAEeOan70hsodGWg'),identifier(none,open_EV),boolean_true(none)),equal(rodinpos('Ref4_ControllerHandle',door,'_hBSmAWfJEeO3ssiFDTK-qw'),identifier(none,door_open),boolean_true(none)),disjunct(rodinpos('Ref4_ControllerHandle',grd,'_hBSmAmfJEeO3ssiFDTK-qw'),equal(none,identifier(none,gear_extended),boolean_false(none)),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,last_gear_action),set_extension(none,[identifier(none,retract_gear_stimulus)])))),equal(rodinpos('Ref4_ControllerHandle',grd7,'_FGggs2fKEeO3ssiFDTK-qw'),identifier(none,handle),identifier(none,down)),disjunct(rodinpos('Ref4_ControllerHandle',grd8,'_akrbcImVEeOQc6S3EYezPA'),equal(none,identifier(none,gear_retracted),boolean_true(none)),conjunct(none,equal(none,identifier(none,gear_retracted),boolean_false(none)),not_equal(none,identifier(none,last_handle_state),set_extension(none,[identifier(none,handle)]))))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_rerAVGfIEeO3ssiFDTK-qw'),[identifier(none,extend_EV)],[boolean_true(none)]),assign(rodinpos('Ref4_ControllerHandle',act,'_hBSmA2fJEeO3ssiFDTK-qw'),[identifier(none,last_gear_action)],[set_extension(none,[identifier(none,extend_gear_stimulus)])])],[]),event(rodinpos('Ref4_ControllerHandle',con_stop_stimulate_extend_gear_valve,'_FGggtGfKEeO3ssiFDTK-qw'),con_stop_stimulate_extend_gear_valve,ordinary(none),[con_stop_stimulate_extend_gear_valve],[],[equal(rodinpos('Ref4_ControllerHandle',grd2,'_rernYWfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_true(none)),disjunct(rodinpos('Ref4_ControllerHandle',grd,'_FGhHwWfKEeO3ssiFDTK-qw'),equal(none,identifier(none,gear_extended),boolean_true(none)),conjunct(none,equal(none,identifier(none,gear_extended),boolean_false(none)),equal(none,identifier(none,handle),identifier(none,up))))],[],[assign(rodinpos('Ref4_ControllerHandle',act1,'_rernYmfIEeO3ssiFDTK-qw'),[identifier(none,extend_EV)],[boolean_false(none)])],[]),event(rodinpos('Ref4_ControllerHandle',env_toggle_handle,'_FGhHwmfKEeO3ssiFDTK-qw'),env_toggle_handle,ordinary(none),[],[],[],[],[becomes_element_of(rodinpos('Ref4_ControllerHandle',act,'_FGhHw2fKEeO3ssiFDTK-qw'),[identifier(none,handle)],set_subtraction(none,identifier(none,'HANDLE_STATE'),set_extension(none,[identifier(none,handle)]))),assign(rodinpos('Ref4_ControllerHandle',removegroundlocking,'_dpS_U2ihEeOT_9tDelWe4g'),[identifier(none,lock_door_opening)],[boolean_false(none)])],[]),event(rodinpos('Ref4_ControllerHandle',env_changeShockAbsorber,'_5Rcg0GmCEeOLrLY1DXbL2w'),env_changeShockAbsorber,ordinary(none),[],[],[equal(rodinpos('Ref4_ControllerHandle',grd,'_5RdH4GmCEeOLrLY1DXbL2w'),identifier(none,gear_retracted),boolean_false(none))],[],[becomes_element_of(rodinpos('Ref4_ControllerHandle',act,'_5RdH4WmCEeOLrLY1DXbL2w'),[identifier(none,shock_absorber)],set_subtraction(none,identifier(none,'PLANE_STATE'),set_extension(none,[identifier(none,shock_absorber)])))],[])])]),event_b_model(none,'Ref3_ControllerSensors',[sees(none,['Context0','Context1','Context2']),refines(none,'Ref2_ControllerOutputs'),variables(none,[identifier(none,close_EV),identifier(none,close_door_valve),identifier(none,door),identifier(none,door_closed),identifier(none,door_open),identifier(none,extend_EV),identifier(none,extend_gear_valve),identifier(none,gear),identifier(none,gear_extended),identifier(none,gear_retracted),identifier(none,last_door_action),identifier(none,last_gear_action),identifier(none,open_EV),identifier(none,open_door_valve),identifier(none,retract_EV),identifier(none,retract_gear_valve)]),invariant(none,[member(rodinpos('Ref3_ControllerSensors',door_closed,'_soSB4GcGEeO7UsfGCD69ng'),identifier(none,door_closed),bool_set(none)),member(rodinpos('Ref3_ControllerSensors',door_open,'_soSB4WcGEeO7UsfGCD69ng'),identifier(none,door_open),bool_set(none)),member(rodinpos('Ref3_ControllerSensors',gear_extended,'_soSB4mcGEeO7UsfGCD69ng'),identifier(none,gear_extended),bool_set(none)),member(rodinpos('Ref3_ControllerSensors',gear_retracted,'_soSo8GcGEeO7UsfGCD69ng'),identifier(none,gear_retracted),bool_set(none)),member(rodinpos('Ref3_ControllerSensors',last_door_action,'_pmkPcGcpEeOIZYXp1CRUOw'),identifier(none,last_door_action),pow_subset(none,set_extension(none,[identifier(none,open_door_stimulus),identifier(none,close_door_stimulus)]))),conjunct(rodinpos('Ref3_ControllerSensors',last_door_action2,'_pmk2gGcpEeOIZYXp1CRUOw'),finite(none,identifier(none,last_door_action)),less(none,card(none,identifier(none,last_door_action)),integer(none,2))),member(rodinpos('Ref3_ControllerSensors',last_gear_action,'_cRqHAWctEeOU3Z0T65yXqA'),identifier(none,last_gear_action),pow_subset(none,set_extension(none,[identifier(none,extend_gear_stimulus),identifier(none,retract_gear_stimulus)]))),conjunct(rodinpos('Ref3_ControllerSensors',last_gear_action2,'_cRqHAmctEeOU3Z0T65yXqA'),finite(none,identifier(none,last_gear_action)),less(none,card(none,identifier(none,last_gear_action)),integer(none,2)))]),theorems(none,[]),events(none,[event(rodinpos('Ref3_ControllerSensors','INITIALISATION','_xET6kWcBEeO7UsfGCD69nh'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_Y7EY0GY0EeO7UsfGCD69ng'),[identifier(none,gear)],[identifier(none,extended)]),assign(rodinpos('Ref3_ControllerSensors',act2,'_KkdfoGY0EeO7UsfGCD69ng'),[identifier(none,door)],[identifier(none,closed)]),assign(rodinpos('Ref3_ControllerSensors',close_door_valve,'_yQPxAGY3EeO7UsfGCD69ng'),[identifier(none,close_door_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref3_ControllerSensors',open_door_valve,'_yQPxAWY3EeO7UsfGCD69ng'),[identifier(none,open_door_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref3_ControllerSensors',retract_gear_valve,'_yQQYEGY3EeO7UsfGCD69ng'),[identifier(none,retract_gear_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref3_ControllerSensors',extend_gear_valve,'_yQQYEWY3EeO7UsfGCD69ng'),[identifier(none,extend_gear_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref3_ControllerSensors',open_EV,'_xEJigGcBEeO7UsfGCD69ng'),[identifier(none,open_EV)],[boolean_false(none)]),assign(rodinpos('Ref3_ControllerSensors',close_EV,'_xEKJkGcBEeO7UsfGCD69ng'),[identifier(none,close_EV)],[boolean_false(none)]),assign(rodinpos('Ref3_ControllerSensors',retract_EV,'_PLAoYGcCEeO7UsfGCD69ng'),[identifier(none,retract_EV)],[boolean_false(none)]),assign(rodinpos('Ref3_ControllerSensors',extend_EV,'_PLAoYWcCEeO7UsfGCD69ng'),[identifier(none,extend_EV)],[boolean_false(none)]),assign(rodinpos('Ref3_ControllerSensors',door_closed,'_soNwcGcGEeO7UsfGCD69ng'),[identifier(none,door_closed)],[boolean_true(none)]),assign(rodinpos('Ref3_ControllerSensors',door_open,'_soNwcWcGEeO7UsfGCD69ng'),[identifier(none,door_open)],[boolean_false(none)]),assign(rodinpos('Ref3_ControllerSensors',gear_extended,'_soNwcmcGEeO7UsfGCD69ng'),[identifier(none,gear_extended)],[boolean_true(none)]),assign(rodinpos('Ref3_ControllerSensors',gear_retracted,'_soNwc2cGEeO7UsfGCD69ng'),[identifier(none,gear_retracted)],[boolean_false(none)]),assign(rodinpos('Ref3_ControllerSensors',last_door_action,'_pmSioWcpEeOIZYXp1CRUOw'),[identifier(none,last_door_action)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'STIMULI')))]),assign(rodinpos('Ref3_ControllerSensors',last_gear_action,'_cRkAYGctEeOU3Z0T65yXqA'),[identifier(none,last_gear_action)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'STIMULI')))])],[]),event(rodinpos('Ref3_ControllerSensors',env_start_extending,'_hBLRQGfJEeO3ssiFDTK-qw'),env_start_extending,ordinary(none),[env_start_extending],[],[equal(rodinpos('Ref3_ControllerSensors',grd2,'_XbFLomfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,retracted)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_fVIREmfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref3_ControllerSensors',grd4,'_WLnKIX64EeOk5IscBNq0oQ'),identifier(none,retract_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_XbFysGfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,gear_moving)]),assign(rodinpos('Ref3_ControllerSensors',act3,'_hBLRQmfJEeO3ssiFDTK-qw'),[identifier(none,gear_retracted)],[boolean_false(none)])],[]),event(rodinpos('Ref3_ControllerSensors',env_extend_gear,'_hBLRQ2fJEeO3ssiFDTK-qw'),env_extend_gear,ordinary(none),[env_extend_gear],[],[equal(rodinpos('Ref3_ControllerSensors',grd2,'_XbGZwGfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,gear_moving)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_fVI4IWfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref3_ControllerSensors',grd4,'_WLnKI364EeOk5IscBNq0oQ'),identifier(none,retract_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_XbGZwWfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,extended)]),assign(rodinpos('Ref3_ControllerSensors',act3,'_hBLRRWfJEeO3ssiFDTK-qw'),[identifier(none,gear_extended)],[boolean_true(none)])],[]),event(rodinpos('Ref3_ControllerSensors',env_retract_gear,'_hBL4UGfJEeO3ssiFDTK-qw'),env_retract_gear,ordinary(none),[env_retract_gear],[],[equal(rodinpos('Ref3_ControllerSensors',grd2,'_XbHA0WfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,gear_moving)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_fVJfMGfHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref3_ControllerSensors',grd4,'_WLnxMX64EeOk5IscBNq0oQ'),identifier(none,extend_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_XbHA0mfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,retracted)]),assign(rodinpos('Ref3_ControllerSensors',act3,'_hBL4UmfJEeO3ssiFDTK-qw'),[identifier(none,gear_retracted)],[boolean_true(none)])],[]),event(rodinpos('Ref3_ControllerSensors',env_start_retracting,'_hBL4U2fJEeO3ssiFDTK-qw'),env_start_retracting,ordinary(none),[env_start_retracting],[],[equal(rodinpos('Ref3_ControllerSensors',grd2,'_XbHn4WfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,extended)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_fVJfM2fHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref3_ControllerSensors',grd4,'_WLnxM364EeOk5IscBNq0oQ'),identifier(none,extend_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_XbIO8GfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,gear_moving)]),assign(rodinpos('Ref3_ControllerSensors',act3,'_hBMfYGfJEeO3ssiFDTK-qw'),[identifier(none,gear_extended)],[boolean_false(none)])],[]),event(rodinpos('Ref3_ControllerSensors',env_start_open_door,'_hBMfYWfJEeO3ssiFDTK-qw'),env_start_open_door,ordinary(none),[env_start_open_door],[],[equal(rodinpos('Ref3_ControllerSensors',grd2,'_XbI2AGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,closed)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_fVKGQmfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref3_ControllerSensors',grd4,'_WLnxNX64EeOk5IscBNq0oQ'),identifier(none,close_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_XbI2AWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,door_moving)]),assign(rodinpos('Ref3_ControllerSensors',act3,'_hBNGcGfJEeO3ssiFDTK-qw'),[identifier(none,door_closed)],[boolean_false(none)])],[]),event(rodinpos('Ref3_ControllerSensors',env_open_door,'_hBNGcWfJEeO3ssiFDTK-qw'),env_open_door,ordinary(none),[env_open_door],[],[equal(rodinpos('Ref3_ControllerSensors',grd2,'_XbJdEGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,door_moving)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_fVKtUWfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref3_ControllerSensors',grd4,'_WLoYQH64EeOk5IscBNq0oQ'),identifier(none,close_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_XbJdEWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,open)]),assign(rodinpos('Ref3_ControllerSensors',act3,'_hBNtgWfJEeO3ssiFDTK-qw'),[identifier(none,door_open)],[boolean_true(none)])],[]),event(rodinpos('Ref3_ControllerSensors',env_close_door,'_hBNtgmfJEeO3ssiFDTK-qw'),env_close_door,ordinary(none),[env_close_door],[],[equal(rodinpos('Ref3_ControllerSensors',grd2,'_XbKEIWfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,door_moving)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_fVKtVGfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref3_ControllerSensors',grd4,'_WLoYQn64EeOk5IscBNq0oQ'),identifier(none,open_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_XbKrMGfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,closed)]),assign(rodinpos('Ref3_ControllerSensors',act3,'_hBOUkWfJEeO3ssiFDTK-qw'),[identifier(none,door_closed)],[boolean_true(none)])],[]),event(rodinpos('Ref3_ControllerSensors',env_start_close_door,'_hBOUkmfJEeO3ssiFDTK-qw'),env_start_close_door,ordinary(none),[env_start_close_door],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_XbLSQGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,open)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_fVLUYmfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref3_ControllerSensors',grd4,'_WLoYRH64EeOk5IscBNq0oQ'),identifier(none,open_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_XbLSQWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,door_moving)]),assign(rodinpos('Ref3_ControllerSensors',act3,'_hBO7oWfJEeO3ssiFDTK-qw'),[identifier(none,door_open)],[boolean_false(none)])],[]),event(rodinpos('Ref3_ControllerSensors',env_open_valve_open_door,'_hBO7omfJEeO3ssiFDTK-qw'),env_open_valve_open_door,ordinary(none),[env_open_valve_open_door],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_CreNUWY4EeO7UsfGCD69ng'),identifier(none,open_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_3bBYgn68EeOk5IscBNq0oQ'),identifier(none,open_EV),boolean_true(none))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_Cre0YGY4EeO7UsfGCD69ng'),[identifier(none,open_door_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref3_ControllerSensors',env_close_valve_open_door,'_hBPisWfJEeO3ssiFDTK-qw'),env_close_valve_open_door,ordinary(none),[env_close_valve_open_door],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_0L1aMWfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_3bBYhH68EeOk5IscBNq0oQ'),identifier(none,open_EV),boolean_false(none))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_0L2BQGfHEeO3ssiFDTK-qw'),[identifier(none,open_door_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref3_ControllerSensors',env_open_valve_close_door,'_hBPis2fJEeO3ssiFDTK-qw'),env_open_valve_close_door,ordinary(none),[env_open_valve_close_door],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_0L2BQmfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_3bBYhn68EeOk5IscBNq0oQ'),identifier(none,close_EV),boolean_true(none))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_0L2BQ2fHEeO3ssiFDTK-qw'),[identifier(none,close_door_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref3_ControllerSensors',env_close_valve_close_door,'_hBPitWfJEeO3ssiFDTK-qw'),env_close_valve_close_door,ordinary(none),[env_close_valve_close_door],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_0L2oUWfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref3_ControllerSensors',grd2,'_3bBYiH68EeOk5IscBNq0oQ'),identifier(none,close_EV),boolean_false(none))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_0L2oUmfHEeO3ssiFDTK-qw'),[identifier(none,close_door_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref3_ControllerSensors',env_open_valve_retract_gear,'_hBQJwWfJEeO3ssiFDTK-qw'),env_open_valve_retract_gear,ordinary(none),[env_open_valve_retract_gear],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_0L3PYGfHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_3bB_kX68EeOk5IscBNq0oQ'),identifier(none,retract_EV),boolean_true(none))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_0L3PYWfHEeO3ssiFDTK-qw'),[identifier(none,retract_gear_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref3_ControllerSensors',env_close_valve_retract_gear,'_hBQJw2fJEeO3ssiFDTK-qw'),env_close_valve_retract_gear,ordinary(none),[env_close_valve_retract_gear],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_0L3PY2fHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_3bB_k368EeOk5IscBNq0oQ'),identifier(none,retract_EV),boolean_false(none))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_0L32cGfHEeO3ssiFDTK-qw'),[identifier(none,retract_gear_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref3_ControllerSensors',env_open_valve_extend_gear,'_hBQw0GfJEeO3ssiFDTK-qw'),env_open_valve_extend_gear,ordinary(none),[env_open_valve_extend_gear],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_0L32cmfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_3bB_lX68EeOk5IscBNq0oQ'),identifier(none,extend_EV),boolean_true(none))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_0L32c2fHEeO3ssiFDTK-qw'),[identifier(none,extend_gear_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref3_ControllerSensors',env_close_valve_extend_gear,'_hBQw0mfJEeO3ssiFDTK-qw'),env_close_valve_extend_gear,ordinary(none),[env_close_valve_extend_gear],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_0L4dgWfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_3bB_l368EeOk5IscBNq0oQ'),identifier(none,extend_EV),boolean_false(none))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_0L4dgmfHEeO3ssiFDTK-qw'),[identifier(none,extend_gear_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref3_ControllerSensors',con_stimulate_open_door_valve,'_xET6kWcBEeO7UsfGCD69ny'),con_stimulate_open_door_valve,ordinary(none),[con_stimulate_open_door_valve],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_reokEGfIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_false(none)),equal(rodinpos('Ref3_ControllerSensors',grd2,'_reokEWfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_false(none)),disjunct(rodinpos('Ref3_ControllerSensors',gear_not_moving,'_Ie4-wGc7EeOU3Z0T65yXqA'),equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,gear_retracted),boolean_true(none)))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_reokEmfIEeO3ssiFDTK-qw'),[identifier(none,open_EV)],[boolean_true(none)]),assign(rodinpos('Ref3_ControllerSensors',act,'_Yg1BEGcqEeOIZYXp1CRUOw'),[identifier(none,last_door_action)],[set_extension(none,[identifier(none,open_door_stimulus)])])],[]),event(rodinpos('Ref3_ControllerSensors',con_stop_stimulate_open_door_valve,'_hBQw1GfJEeO3ssiFDTK-qw'),con_stop_stimulate_open_door_valve,ordinary(none),[con_stop_stimulate_open_door_valve],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_reokFGfIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_true(none))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_repLIGfIEeO3ssiFDTK-qw'),[identifier(none,open_EV)],[boolean_false(none)])],[]),event(rodinpos('Ref3_ControllerSensors',con_stimulate_close_door_valve,'_xET6kWcBEeO7UsfGCD69n{'),con_stimulate_close_door_valve,ordinary(none),[con_stimulate_close_door_valve],[],[equal(rodinpos('Ref3_ControllerSensors',grd2,'_repLImfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_false(none)),equal(rodinpos('Ref3_ControllerSensors',grd1,'_repLI2fIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_false(none)),disjunct(rodinpos('Ref3_ControllerSensors',grd,'_oZAasGcqEeOIZYXp1CRUOw'),equal(none,identifier(none,door_closed),boolean_false(none)),equal(none,identifier(none,last_door_action),set_extension(none,[identifier(none,open_door_stimulus)]))),disjunct(rodinpos('Ref3_ControllerSensors',gear_not_moving,'_Ie4-wWc7EeOU3Z0T65yXqA'),equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,gear_retracted),boolean_true(none)))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_repLJGfIEeO3ssiFDTK-qw'),[identifier(none,close_EV)],[boolean_true(none)]),assign(rodinpos('Ref3_ControllerSensors',act,'_Yg1oIGcqEeOIZYXp1CRUOw'),[identifier(none,last_door_action)],[set_extension(none,[identifier(none,close_door_stimulus)])])],[]),event(rodinpos('Ref3_ControllerSensors',con_stop_stimulate_close_door_valve,'_hBRX4WfJEeO3ssiFDTK-qw'),con_stop_stimulate_close_door_valve,ordinary(none),[con_stop_stimulate_close_door_valve],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_repyMWfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_true(none))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_repyMmfIEeO3ssiFDTK-qw'),[identifier(none,close_EV)],[boolean_false(none)])],[]),event(rodinpos('Ref3_ControllerSensors',con_stimulate_retract_gear_valve,'_hBRX42fJEeO3ssiFDTK-qw'),con_stimulate_retract_gear_valve,ordinary(none),[con_stimulate_retract_gear_valve],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_repyNGfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_false(none)),equal(rodinpos('Ref3_ControllerSensors',grd2,'_reqZQGfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_false(none)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_ssC38GgAEeOan70hsodGWg'),identifier(none,open_EV),boolean_true(none)),equal(rodinpos('Ref3_ControllerSensors',door,'_hBR-8GfJEeO3ssiFDTK-qw'),identifier(none,door_open),boolean_true(none)),disjunct(rodinpos('Ref3_ControllerSensors',grd4,'_hBR-8WfJEeO3ssiFDTK-qw'),equal(none,identifier(none,gear_retracted),boolean_false(none)),conjunct(none,equal(none,identifier(none,gear_retracted),boolean_true(none)),equal(none,identifier(none,last_gear_action),set_extension(none,[identifier(none,extend_gear_stimulus)]))))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_reqZQmfIEeO3ssiFDTK-qw'),[identifier(none,retract_EV)],[boolean_true(none)]),assign(rodinpos('Ref3_ControllerSensors',act,'_hBR-8mfJEeO3ssiFDTK-qw'),[identifier(none,last_gear_action)],[set_extension(none,[identifier(none,retract_gear_stimulus)])])],[]),event(rodinpos('Ref3_ControllerSensors',con_stop_stimulate_retract_gear_valve,'_hBR-82fJEeO3ssiFDTK-qw'),con_stop_stimulate_retract_gear_valve,ordinary(none),[con_stop_stimulate_retract_gear_valve],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_reqZRGfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_true(none))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_reqZRWfIEeO3ssiFDTK-qw'),[identifier(none,retract_EV)],[boolean_false(none)])],[]),event(rodinpos('Ref3_ControllerSensors',con_stimulate_extend_gear_valve,'_hBR-9WfJEeO3ssiFDTK-qw'),con_stimulate_extend_gear_valve,ordinary(none),[con_stimulate_extend_gear_valve],[],[equal(rodinpos('Ref3_ControllerSensors',grd1,'_rerAUWfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_false(none)),equal(rodinpos('Ref3_ControllerSensors',grd2,'_rerAUmfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_false(none)),equal(rodinpos('Ref3_ControllerSensors',grd3,'_ssDfAGgAEeOan70hsodGWg'),identifier(none,open_EV),boolean_true(none)),equal(rodinpos('Ref3_ControllerSensors',door,'_hBSmAWfJEeO3ssiFDTK-qw'),identifier(none,door_open),boolean_true(none)),disjunct(rodinpos('Ref3_ControllerSensors',grd,'_hBSmAmfJEeO3ssiFDTK-qw'),equal(none,identifier(none,gear_extended),boolean_false(none)),conjunct(none,equal(none,identifier(none,gear_extended),boolean_true(none)),equal(none,identifier(none,last_gear_action),set_extension(none,[identifier(none,retract_gear_stimulus)]))))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_rerAVGfIEeO3ssiFDTK-qw'),[identifier(none,extend_EV)],[boolean_true(none)]),assign(rodinpos('Ref3_ControllerSensors',act,'_hBSmA2fJEeO3ssiFDTK-qw'),[identifier(none,last_gear_action)],[set_extension(none,[identifier(none,extend_gear_stimulus)])])],[]),event(rodinpos('Ref3_ControllerSensors',con_stop_stimulate_extend_gear_valve,'_hBSmBGfJEeO3ssiFDTK-qw'),con_stop_stimulate_extend_gear_valve,ordinary(none),[con_stop_stimulate_extend_gear_valve],[],[equal(rodinpos('Ref3_ControllerSensors',grd2,'_rernYWfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_true(none))],[],[assign(rodinpos('Ref3_ControllerSensors',act1,'_rernYmfIEeO3ssiFDTK-qw'),[identifier(none,extend_EV)],[boolean_false(none)])],[])])]),event_b_model(none,'Ref2_ControllerOutputs',[sees(none,['Context0','Context1','Context2']),refines(none,'Ref1_Valve'),variables(none,[identifier(none,close_EV),identifier(none,close_door_valve),identifier(none,door),identifier(none,extend_EV),identifier(none,extend_gear_valve),identifier(none,gear),identifier(none,open_EV),identifier(none,open_door_valve),identifier(none,retract_EV),identifier(none,retract_gear_valve)]),invariant(none,[member(rodinpos('Ref2_ControllerOutputs',open_EV,'_xET6kmcBEeO7UsfGCD69ng'),identifier(none,open_EV),bool_set(none)),member(rodinpos('Ref2_ControllerOutputs',close_EV,'_xEUhoGcBEeO7UsfGCD69ng'),identifier(none,close_EV),bool_set(none)),member(rodinpos('Ref2_ControllerOutputs',retract_EV,'_L0O50WcCEeO7UsfGCD69ng'),identifier(none,retract_EV),bool_set(none)),member(rodinpos('Ref2_ControllerOutputs',extend_EV,'_L0O50mcCEeO7UsfGCD69ng'),identifier(none,extend_EV),bool_set(none)),negation(rodinpos('Ref2_ControllerOutputs','R41','_VXU3sImTEeOQc6S3EYezPA'),conjunct(none,equal(none,identifier(none,open_EV),boolean_true(none)),equal(none,identifier(none,close_EV),boolean_true(none))))]),theorems(none,[]),events(none,[event(rodinpos('Ref2_ControllerOutputs','INITIALISATION','_snVnwGY3EeO7UsfGCD69nh'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_Y7EY0GY0EeO7UsfGCD69ng'),[identifier(none,gear)],[identifier(none,extended)]),assign(rodinpos('Ref2_ControllerOutputs',act2,'_KkdfoGY0EeO7UsfGCD69ng'),[identifier(none,door)],[identifier(none,closed)]),assign(rodinpos('Ref2_ControllerOutputs',close_door_valve,'_yQPxAGY3EeO7UsfGCD69ng'),[identifier(none,close_door_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref2_ControllerOutputs',open_door_valve,'_yQPxAWY3EeO7UsfGCD69ng'),[identifier(none,open_door_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref2_ControllerOutputs',retract_gear_valve,'_yQQYEGY3EeO7UsfGCD69ng'),[identifier(none,retract_gear_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref2_ControllerOutputs',extend_gear_valve,'_yQQYEWY3EeO7UsfGCD69ng'),[identifier(none,extend_gear_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref2_ControllerOutputs',open_EV,'_xEJigGcBEeO7UsfGCD69ng'),[identifier(none,open_EV)],[boolean_false(none)]),assign(rodinpos('Ref2_ControllerOutputs',close_EV,'_xEKJkGcBEeO7UsfGCD69ng'),[identifier(none,close_EV)],[boolean_false(none)]),assign(rodinpos('Ref2_ControllerOutputs',retract_EV,'_PLAoYGcCEeO7UsfGCD69ng'),[identifier(none,retract_EV)],[boolean_false(none)]),assign(rodinpos('Ref2_ControllerOutputs',extend_EV,'_PLAoYWcCEeO7UsfGCD69ng'),[identifier(none,extend_EV)],[boolean_false(none)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_start_extending,'_6I09EGfHEeO3ssiFDTK-qw'),env_start_extending,ordinary(none),[env_start_extending],[],[equal(rodinpos('Ref2_ControllerOutputs',grd2,'_XbFLomfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,retracted)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_fVIREmfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref2_ControllerOutputs',grd4,'_WLnKIX64EeOk5IscBNq0oQ'),identifier(none,retract_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_XbFysGfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,gear_moving)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_extend_gear,'_6I1kIWfHEeO3ssiFDTK-qw'),env_extend_gear,ordinary(none),[env_extend_gear],[],[equal(rodinpos('Ref2_ControllerOutputs',grd2,'_XbGZwGfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,gear_moving)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_fVI4IWfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref2_ControllerOutputs',grd4,'_WLnKI364EeOk5IscBNq0oQ'),identifier(none,retract_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_XbGZwWfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,extended)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_retract_gear,'_6I2LMGfHEeO3ssiFDTK-qw'),env_retract_gear,ordinary(none),[env_retract_gear],[],[equal(rodinpos('Ref2_ControllerOutputs',grd2,'_XbHA0WfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,gear_moving)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_fVJfMGfHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref2_ControllerOutputs',grd4,'_WLnxMX64EeOk5IscBNq0oQ'),identifier(none,extend_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_XbHA0mfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,retracted)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_start_retracting,'_6I2LMmfHEeO3ssiFDTK-qw'),env_start_retracting,ordinary(none),[env_start_retracting],[],[equal(rodinpos('Ref2_ControllerOutputs',grd2,'_XbHn4WfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,extended)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_fVJfM2fHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref2_ControllerOutputs',grd4,'_WLnxM364EeOk5IscBNq0oQ'),identifier(none,extend_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_XbIO8GfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,gear_moving)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_start_open_door,'_6I2yQWfHEeO3ssiFDTK-qw'),env_start_open_door,ordinary(none),[env_start_open_door],[],[equal(rodinpos('Ref2_ControllerOutputs',grd2,'_XbI2AGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,closed)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_fVKGQmfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref2_ControllerOutputs',grd4,'_WLnxNX64EeOk5IscBNq0oQ'),identifier(none,close_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_XbI2AWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,door_moving)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_open_door,'_rek5sGfIEeO3ssiFDTK-qw'),env_open_door,ordinary(none),[env_open_door],[],[equal(rodinpos('Ref2_ControllerOutputs',grd2,'_XbJdEGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,door_moving)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_fVKtUWfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref2_ControllerOutputs',grd4,'_WLoYQH64EeOk5IscBNq0oQ'),identifier(none,close_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_XbJdEWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,open)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_close_door,'_rek5smfIEeO3ssiFDTK-qw'),env_close_door,ordinary(none),[env_close_door],[],[equal(rodinpos('Ref2_ControllerOutputs',grd2,'_XbKEIWfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,door_moving)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_fVKtVGfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref2_ControllerOutputs',grd4,'_WLoYQn64EeOk5IscBNq0oQ'),identifier(none,open_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_XbKrMGfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,closed)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_start_close_door,'_relgwWfIEeO3ssiFDTK-qw'),env_start_close_door,ordinary(none),[env_start_close_door],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_XbLSQGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,open)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_fVLUYmfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref2_ControllerOutputs',grd4,'_WLoYRH64EeOk5IscBNq0oQ'),identifier(none,open_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_XbLSQWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,door_moving)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_open_valve_open_door,'_relgw2fIEeO3ssiFDTK-qw'),env_open_valve_open_door,ordinary(none),[env_open_valve_open_door],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_CreNUWY4EeO7UsfGCD69ng'),identifier(none,open_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_3bBYgn68EeOk5IscBNq0oQ'),identifier(none,open_EV),boolean_true(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_Cre0YGY4EeO7UsfGCD69ng'),[identifier(none,open_door_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_close_valve_open_door,'_remH0GfIEeO3ssiFDTK-qw'),env_close_valve_open_door,ordinary(none),[env_close_valve_open_door],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_0L1aMWfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_3bBYhH68EeOk5IscBNq0oQ'),identifier(none,open_EV),boolean_false(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_0L2BQGfHEeO3ssiFDTK-qw'),[identifier(none,open_door_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_open_valve_close_door,'_remH02fIEeO3ssiFDTK-qw'),env_open_valve_close_door,ordinary(none),[env_open_valve_close_door],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_0L2BQmfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_closed)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_3bBYhn68EeOk5IscBNq0oQ'),identifier(none,close_EV),boolean_true(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_0L2BQ2fHEeO3ssiFDTK-qw'),[identifier(none,close_door_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_close_valve_close_door,'_remu4WfIEeO3ssiFDTK-qw'),env_close_valve_close_door,ordinary(none),[env_close_valve_close_door],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_0L2oUWfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref2_ControllerOutputs',grd2,'_3bBYiH68EeOk5IscBNq0oQ'),identifier(none,close_EV),boolean_false(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_0L2oUmfHEeO3ssiFDTK-qw'),[identifier(none,close_door_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_open_valve_retract_gear,'_remu5GfIEeO3ssiFDTK-qw'),env_open_valve_retract_gear,ordinary(none),[env_open_valve_retract_gear],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_0L3PYGfHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_3bB_kX68EeOk5IscBNq0oQ'),identifier(none,retract_EV),boolean_true(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_0L3PYWfHEeO3ssiFDTK-qw'),[identifier(none,retract_gear_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_close_valve_retract_gear,'_renV8mfIEeO3ssiFDTK-qw'),env_close_valve_retract_gear,ordinary(none),[env_close_valve_retract_gear],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_0L3PY2fHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_3bB_k368EeOk5IscBNq0oQ'),identifier(none,retract_EV),boolean_false(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_0L32cGfHEeO3ssiFDTK-qw'),[identifier(none,retract_gear_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_open_valve_extend_gear,'_renV9WfIEeO3ssiFDTK-qw'),env_open_valve_extend_gear,ordinary(none),[env_open_valve_extend_gear],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_0L32cmfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_closed)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_3bB_lX68EeOk5IscBNq0oQ'),identifier(none,extend_EV),boolean_true(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_0L32c2fHEeO3ssiFDTK-qw'),[identifier(none,extend_gear_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref2_ControllerOutputs',env_close_valve_extend_gear,'_ren9AmfIEeO3ssiFDTK-qw'),env_close_valve_extend_gear,ordinary(none),[env_close_valve_extend_gear],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_0L4dgWfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_3bB_l368EeOk5IscBNq0oQ'),identifier(none,extend_EV),boolean_false(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_0L4dgmfHEeO3ssiFDTK-qw'),[identifier(none,extend_gear_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref2_ControllerOutputs',con_stimulate_open_door_valve,'_ren9BWfIEeO3ssiFDTK-qw'),con_stimulate_open_door_valve,ordinary(none),[],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_reokEGfIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_false(none)),equal(rodinpos('Ref2_ControllerOutputs',grd2,'_reokEWfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_false(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_reokEmfIEeO3ssiFDTK-qw'),[identifier(none,open_EV)],[boolean_true(none)])],[]),event(rodinpos('Ref2_ControllerOutputs',con_stop_stimulate_open_door_valve,'_reokE2fIEeO3ssiFDTK-qw'),con_stop_stimulate_open_door_valve,ordinary(none),[],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_reokFGfIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_true(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_repLIGfIEeO3ssiFDTK-qw'),[identifier(none,open_EV)],[boolean_false(none)])],[]),event(rodinpos('Ref2_ControllerOutputs',con_stimulate_close_door_valve,'_repLIWfIEeO3ssiFDTK-qw'),con_stimulate_close_door_valve,ordinary(none),[],[],[equal(rodinpos('Ref2_ControllerOutputs',grd2,'_repLImfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_false(none)),equal(rodinpos('Ref2_ControllerOutputs',grd1,'_repLI2fIEeO3ssiFDTK-qw'),identifier(none,open_EV),boolean_false(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_repLJGfIEeO3ssiFDTK-qw'),[identifier(none,close_EV)],[boolean_true(none)])],[]),event(rodinpos('Ref2_ControllerOutputs',con_stop_stimulate_close_door_valve,'_repyMGfIEeO3ssiFDTK-qw'),con_stop_stimulate_close_door_valve,ordinary(none),[],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_repyMWfIEeO3ssiFDTK-qw'),identifier(none,close_EV),boolean_true(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_repyMmfIEeO3ssiFDTK-qw'),[identifier(none,close_EV)],[boolean_false(none)])],[]),event(rodinpos('Ref2_ControllerOutputs',con_stimulate_retract_gear_valve,'_repyM2fIEeO3ssiFDTK-qw'),con_stimulate_retract_gear_valve,ordinary(none),[],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_repyNGfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_false(none)),equal(rodinpos('Ref2_ControllerOutputs',grd2,'_reqZQGfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_false(none)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_ssC38GgAEeOan70hsodGWg'),identifier(none,open_EV),boolean_true(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_reqZQmfIEeO3ssiFDTK-qw'),[identifier(none,retract_EV)],[boolean_true(none)])],[]),event(rodinpos('Ref2_ControllerOutputs',con_stop_stimulate_retract_gear_valve,'_reqZQ2fIEeO3ssiFDTK-qw'),con_stop_stimulate_retract_gear_valve,ordinary(none),[],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_reqZRGfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_true(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_reqZRWfIEeO3ssiFDTK-qw'),[identifier(none,retract_EV)],[boolean_false(none)])],[]),event(rodinpos('Ref2_ControllerOutputs',con_stimulate_extend_gear_valve,'_rerAUGfIEeO3ssiFDTK-qw'),con_stimulate_extend_gear_valve,ordinary(none),[],[],[equal(rodinpos('Ref2_ControllerOutputs',grd1,'_rerAUWfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_false(none)),equal(rodinpos('Ref2_ControllerOutputs',grd2,'_rerAUmfIEeO3ssiFDTK-qw'),identifier(none,retract_EV),boolean_false(none)),equal(rodinpos('Ref2_ControllerOutputs',grd3,'_ssDfAGgAEeOan70hsodGWg'),identifier(none,open_EV),boolean_true(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_rerAVGfIEeO3ssiFDTK-qw'),[identifier(none,extend_EV)],[boolean_true(none)])],[]),event(rodinpos('Ref2_ControllerOutputs',con_stop_stimulate_extend_gear_valve,'_rernYGfIEeO3ssiFDTK-qw'),con_stop_stimulate_extend_gear_valve,ordinary(none),[],[],[equal(rodinpos('Ref2_ControllerOutputs',grd2,'_rernYWfIEeO3ssiFDTK-qw'),identifier(none,extend_EV),boolean_true(none))],[],[assign(rodinpos('Ref2_ControllerOutputs',act1,'_rernYmfIEeO3ssiFDTK-qw'),[identifier(none,extend_EV)],[boolean_false(none)])],[])])]),event_b_model(none,'Ref1_Valve',[sees(none,['Context0','Context1']),refines(none,'Mch0_GearDoor'),variables(none,[identifier(none,close_door_valve),identifier(none,door),identifier(none,extend_gear_valve),identifier(none,gear),identifier(none,open_door_valve),identifier(none,retract_gear_valve)]),invariant(none,[member(rodinpos('Ref1_Valve',close_door_valve,'_qplho2Y3EeO7UsfGCD69ng'),identifier(none,close_door_valve),identifier(none,'VALVE_STATE')),member(rodinpos('Ref1_Valve',open_door_valve,'_qpmIsGY3EeO7UsfGCD69ng'),identifier(none,open_door_valve),identifier(none,'VALVE_STATE')),member(rodinpos('Ref1_Valve',retract_gear_valve,'_qpmIsWY3EeO7UsfGCD69ng'),identifier(none,retract_gear_valve),identifier(none,'VALVE_STATE')),member(rodinpos('Ref1_Valve',extend_gear_valve,'_qpmIsmY3EeO7UsfGCD69ng'),identifier(none,extend_gear_valve),identifier(none,'VALVE_STATE'))]),theorems(none,[]),events(none,[event(rodinpos('Ref1_Valve','INITIALISATION','_Y7IDMGY0EeO7UsfGCD69nh'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('Ref1_Valve',act1,'_Y7EY0GY0EeO7UsfGCD69ng'),[identifier(none,gear)],[identifier(none,extended)]),assign(rodinpos('Ref1_Valve',act2,'_KkdfoGY0EeO7UsfGCD69ng'),[identifier(none,door)],[identifier(none,closed)]),assign(rodinpos('Ref1_Valve',close_door_valve,'_yQPxAGY3EeO7UsfGCD69ng'),[identifier(none,close_door_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref1_Valve',open_door_valve,'_yQPxAWY3EeO7UsfGCD69ng'),[identifier(none,open_door_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref1_Valve',retract_gear_valve,'_yQQYEGY3EeO7UsfGCD69ng'),[identifier(none,retract_gear_valve)],[identifier(none,valve_closed)]),assign(rodinpos('Ref1_Valve',extend_gear_valve,'_yQQYEWY3EeO7UsfGCD69ng'),[identifier(none,extend_gear_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref1_Valve',env_start_extending,'_fVIREGfHEeO3ssiFDTK-qw'),env_start_extending,ordinary(none),[env_start_extending],[],[equal(rodinpos('Ref1_Valve',grd2,'_XbFLomfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,retracted)),equal(rodinpos('Ref1_Valve',grd3,'_fVIREmfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref1_Valve',grd4,'_WLnKIX64EeOk5IscBNq0oQ'),identifier(none,retract_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref1_Valve',act1,'_XbFysGfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,gear_moving)])],[]),event(rodinpos('Ref1_Valve',env_extend_gear,'_fVIRE2fHEeO3ssiFDTK-qw'),env_extend_gear,ordinary(none),[env_extend_gear],[],[equal(rodinpos('Ref1_Valve',grd2,'_XbGZwGfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,gear_moving)),equal(rodinpos('Ref1_Valve',grd3,'_fVI4IWfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref1_Valve',grd4,'_WLnKI364EeOk5IscBNq0oQ'),identifier(none,retract_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref1_Valve',act1,'_XbGZwWfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,extended)])],[]),event(rodinpos('Ref1_Valve',env_retract_gear,'_fVI4ImfHEeO3ssiFDTK-qw'),env_retract_gear,ordinary(none),[env_retract_gear],[],[equal(rodinpos('Ref1_Valve',grd2,'_XbHA0WfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,gear_moving)),equal(rodinpos('Ref1_Valve',grd3,'_fVJfMGfHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref1_Valve',grd4,'_WLnxMX64EeOk5IscBNq0oQ'),identifier(none,extend_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref1_Valve',act1,'_XbHA0mfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,retracted)])],[]),event(rodinpos('Ref1_Valve',env_start_retracting,'_fVJfMWfHEeO3ssiFDTK-qw'),env_start_retracting,ordinary(none),[env_start_retracting],[],[equal(rodinpos('Ref1_Valve',grd2,'_XbHn4WfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,extended)),equal(rodinpos('Ref1_Valve',grd3,'_fVJfM2fHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open)),equal(rodinpos('Ref1_Valve',grd4,'_WLnxM364EeOk5IscBNq0oQ'),identifier(none,extend_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref1_Valve',act1,'_XbIO8GfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,gear_moving)])],[]),event(rodinpos('Ref1_Valve',env_start_open_door,'_fVKGQGfHEeO3ssiFDTK-qw'),env_start_open_door,ordinary(none),[env_start_open_door],[],[equal(rodinpos('Ref1_Valve',grd2,'_XbI2AGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,closed)),equal(rodinpos('Ref1_Valve',grd3,'_fVKGQmfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref1_Valve',grd4,'_WLnxNX64EeOk5IscBNq0oQ'),identifier(none,close_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref1_Valve',act1,'_XbI2AWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,door_moving)])],[]),event(rodinpos('Ref1_Valve',env_open_door,'_fVKGQ2fHEeO3ssiFDTK-qw'),env_open_door,ordinary(none),[env_open_door],[],[equal(rodinpos('Ref1_Valve',grd2,'_XbJdEGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,door_moving)),equal(rodinpos('Ref1_Valve',grd3,'_fVKtUWfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref1_Valve',grd4,'_WLoYQH64EeOk5IscBNq0oQ'),identifier(none,close_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref1_Valve',act1,'_XbJdEWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,open)])],[]),event(rodinpos('Ref1_Valve',env_close_door,'_fVKtUmfHEeO3ssiFDTK-qw'),env_close_door,ordinary(none),[env_close_door],[],[equal(rodinpos('Ref1_Valve',grd2,'_XbKEIWfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,door_moving)),equal(rodinpos('Ref1_Valve',grd3,'_fVKtVGfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref1_Valve',grd4,'_WLoYQn64EeOk5IscBNq0oQ'),identifier(none,open_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref1_Valve',act1,'_XbKrMGfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,closed)])],[]),event(rodinpos('Ref1_Valve',env_start_close_door,'_fVLUYGfHEeO3ssiFDTK-qw'),env_start_close_door,ordinary(none),[env_start_close_door],[],[equal(rodinpos('Ref1_Valve',grd1,'_XbLSQGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,open)),equal(rodinpos('Ref1_Valve',grd3,'_fVLUYmfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open)),equal(rodinpos('Ref1_Valve',grd4,'_WLoYRH64EeOk5IscBNq0oQ'),identifier(none,open_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref1_Valve',act1,'_XbLSQWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,door_moving)])],[]),event(rodinpos('Ref1_Valve',env_open_valve_open_door,'_CreNUGY4EeO7UsfGCD69ng'),env_open_valve_open_door,ordinary(none),[],[],[equal(rodinpos('Ref1_Valve',grd1,'_CreNUWY4EeO7UsfGCD69ng'),identifier(none,open_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref1_Valve',act1,'_Cre0YGY4EeO7UsfGCD69ng'),[identifier(none,open_door_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref1_Valve',env_close_valve_open_door,'_0L1aMGfHEeO3ssiFDTK-qw'),env_close_valve_open_door,ordinary(none),[],[],[equal(rodinpos('Ref1_Valve',grd1,'_0L1aMWfHEeO3ssiFDTK-qw'),identifier(none,open_door_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref1_Valve',act1,'_0L2BQGfHEeO3ssiFDTK-qw'),[identifier(none,open_door_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref1_Valve',env_open_valve_close_door,'_0L2BQWfHEeO3ssiFDTK-qw'),env_open_valve_close_door,ordinary(none),[],[],[equal(rodinpos('Ref1_Valve',grd1,'_0L2BQmfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref1_Valve',act1,'_0L2BQ2fHEeO3ssiFDTK-qw'),[identifier(none,close_door_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref1_Valve',env_close_valve_close_door,'_0L2oUGfHEeO3ssiFDTK-qw'),env_close_valve_close_door,ordinary(none),[],[],[equal(rodinpos('Ref1_Valve',grd1,'_0L2oUWfHEeO3ssiFDTK-qw'),identifier(none,close_door_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref1_Valve',act1,'_0L2oUmfHEeO3ssiFDTK-qw'),[identifier(none,close_door_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref1_Valve',env_open_valve_retract_gear,'_0L2oU2fHEeO3ssiFDTK-qw'),env_open_valve_retract_gear,ordinary(none),[],[],[equal(rodinpos('Ref1_Valve',grd1,'_0L3PYGfHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref1_Valve',act1,'_0L3PYWfHEeO3ssiFDTK-qw'),[identifier(none,retract_gear_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref1_Valve',env_close_valve_retract_gear,'_0L3PYmfHEeO3ssiFDTK-qw'),env_close_valve_retract_gear,ordinary(none),[],[],[equal(rodinpos('Ref1_Valve',grd1,'_0L3PY2fHEeO3ssiFDTK-qw'),identifier(none,retract_gear_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref1_Valve',act1,'_0L32cGfHEeO3ssiFDTK-qw'),[identifier(none,retract_gear_valve)],[identifier(none,valve_closed)])],[]),event(rodinpos('Ref1_Valve',env_open_valve_extend_gear,'_0L32cWfHEeO3ssiFDTK-qw'),env_open_valve_extend_gear,ordinary(none),[],[],[equal(rodinpos('Ref1_Valve',grd1,'_0L32cmfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_closed))],[],[assign(rodinpos('Ref1_Valve',act1,'_0L32c2fHEeO3ssiFDTK-qw'),[identifier(none,extend_gear_valve)],[identifier(none,valve_open)])],[]),event(rodinpos('Ref1_Valve',env_close_valve_extend_gear,'_0L4dgGfHEeO3ssiFDTK-qw'),env_close_valve_extend_gear,ordinary(none),[],[],[equal(rodinpos('Ref1_Valve',grd1,'_0L4dgWfHEeO3ssiFDTK-qw'),identifier(none,extend_gear_valve),identifier(none,valve_open))],[],[assign(rodinpos('Ref1_Valve',act1,'_0L4dgmfHEeO3ssiFDTK-qw'),[identifier(none,extend_gear_valve)],[identifier(none,valve_closed)])],[])])]),event_b_model(none,'Mch0_GearDoor',[sees(none,['Context0']),variables(none,[identifier(none,door),identifier(none,gear)]),invariant(none,[member(rodinpos('Mch0_GearDoor',inv1,'_Y7E_4GY0EeO7UsfGCD69ng'),identifier(none,gear),identifier(none,'GEAR_STATE')),member(rodinpos('Mch0_GearDoor',inv2,'_KkeGsGY0EeO7UsfGCD69ng'),identifier(none,door),identifier(none,'DOOR_STATE'))]),theorems(none,[]),events(none,[event(rodinpos('Mch0_GearDoor','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('Mch0_GearDoor',act1,'_Y7EY0GY0EeO7UsfGCD69ng'),[identifier(none,gear)],[identifier(none,extended)]),assign(rodinpos('Mch0_GearDoor',act2,'_KkdfoGY0EeO7UsfGCD69ng'),[identifier(none,door)],[identifier(none,closed)])],[]),event(rodinpos('Mch0_GearDoor',env_start_extending,'_XbFLoWfHEeO3ssiFDTK-qw'),env_start_extending,ordinary(none),[],[],[equal(rodinpos('Mch0_GearDoor',grd2,'_XbFLomfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,retracted))],[],[assign(rodinpos('Mch0_GearDoor',act1,'_XbFysGfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,gear_moving)])],[]),event(rodinpos('Mch0_GearDoor',env_extend_gear,'_XbFysWfHEeO3ssiFDTK-qw'),env_extend_gear,ordinary(none),[],[],[equal(rodinpos('Mch0_GearDoor',grd2,'_XbGZwGfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,gear_moving))],[],[assign(rodinpos('Mch0_GearDoor',act1,'_XbGZwWfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,extended)])],[]),event(rodinpos('Mch0_GearDoor',env_retract_gear,'_XbHA0GfHEeO3ssiFDTK-qw'),env_retract_gear,ordinary(none),[],[],[equal(rodinpos('Mch0_GearDoor',grd2,'_XbHA0WfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,gear_moving))],[],[assign(rodinpos('Mch0_GearDoor',act1,'_XbHA0mfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,retracted)])],[]),event(rodinpos('Mch0_GearDoor',env_start_retracting,'_XbHn4GfHEeO3ssiFDTK-qw'),env_start_retracting,ordinary(none),[],[],[equal(rodinpos('Mch0_GearDoor',grd2,'_XbHn4WfHEeO3ssiFDTK-qw'),identifier(none,gear),identifier(none,extended))],[],[assign(rodinpos('Mch0_GearDoor',act1,'_XbIO8GfHEeO3ssiFDTK-qw'),[identifier(none,gear)],[identifier(none,gear_moving)])],[]),event(rodinpos('Mch0_GearDoor',env_start_open_door,'_XbIO8WfHEeO3ssiFDTK-qw'),env_start_open_door,ordinary(none),[],[],[equal(rodinpos('Mch0_GearDoor',grd2,'_XbI2AGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,closed))],[],[assign(rodinpos('Mch0_GearDoor',act1,'_XbI2AWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,door_moving)])],[]),event(rodinpos('Mch0_GearDoor',env_open_door,'_XbI2AmfHEeO3ssiFDTK-qw'),env_open_door,ordinary(none),[],[],[equal(rodinpos('Mch0_GearDoor',grd2,'_XbJdEGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,door_moving))],[],[assign(rodinpos('Mch0_GearDoor',act1,'_XbJdEWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,open)])],[]),event(rodinpos('Mch0_GearDoor',env_close_door,'_XbKEIGfHEeO3ssiFDTK-qw'),env_close_door,ordinary(none),[],[],[equal(rodinpos('Mch0_GearDoor',grd2,'_XbKEIWfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,door_moving))],[],[assign(rodinpos('Mch0_GearDoor',act1,'_XbKrMGfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,closed)])],[]),event(rodinpos('Mch0_GearDoor',env_start_close_door,'_XbKrMWfHEeO3ssiFDTK-qw'),env_start_close_door,ordinary(none),[],[],[equal(rodinpos('Mch0_GearDoor',grd1,'_XbLSQGfHEeO3ssiFDTK-qw'),identifier(none,door),identifier(none,open))],[],[assign(rodinpos('Mch0_GearDoor',act1,'_XbLSQWfHEeO3ssiFDTK-qw'),[identifier(none,door)],[identifier(none,door_moving)])],[])])])],[event_b_context(none,'Context0',[extends(none,[]),constants(none,[identifier(none,closed),identifier(none,door_moving),identifier(none,down),identifier(none,extended),identifier(none,flight),identifier(none,gear_moving),identifier(none,ground),identifier(none,open),identifier(none,retracted),identifier(none,up)]),abstract_constants(none,[]),axioms(none,[partition(rodinpos('Context0',axm1,'_r0i1smYzEeO7UsfGCD69ng'),identifier(none,'DOOR_STATE'),[set_extension(none,[identifier(none,open)]),set_extension(none,[identifier(none,closed)]),set_extension(none,[identifier(none,door_moving)])]),partition(rodinpos('Context0',axm2,'_r0kD0GYzEeO7UsfGCD69ng'),identifier(none,'GEAR_STATE'),[set_extension(none,[identifier(none,retracted)]),set_extension(none,[identifier(none,extended)]),set_extension(none,[identifier(none,gear_moving)])]),partition(rodinpos('Context0',axm3,'_r0kD0WYzEeO7UsfGCD69ng'),identifier(none,'HANDLE_STATE'),[set_extension(none,[identifier(none,up)]),set_extension(none,[identifier(none,down)])]),partition(rodinpos('Context0',axm4,'_r0kq4GYzEeO7UsfGCD69ng'),identifier(none,'PLANE_STATE'),[set_extension(none,[identifier(none,ground)]),set_extension(none,[identifier(none,flight)])])]),theorems(none,[]),sets(none,[deferred_set(none,'DOOR_STATE'),deferred_set(none,'GEAR_STATE'),deferred_set(none,'HANDLE_STATE'),deferred_set(none,'PLANE_STATE')])]),event_b_context(none,'Context1',[extends(none,[]),constants(none,[identifier(none,switch_closed),identifier(none,switch_open),identifier(none,valve_closed),identifier(none,valve_open)]),abstract_constants(none,[]),axioms(none,[partition(rodinpos('Context1',axm1,'_CLwdYGY2EeO7UsfGCD69ng'),identifier(none,'VALVE_STATE'),[set_extension(none,[identifier(none,valve_open)]),set_extension(none,[identifier(none,valve_closed)])]),partition(rodinpos('Context1',axm2,'_CLwdYWY2EeO7UsfGCD69ng'),identifier(none,'SWITCH_STATE'),[set_extension(none,[identifier(none,switch_open)]),set_extension(none,[identifier(none,switch_closed)])])]),theorems(none,[]),sets(none,[deferred_set(none,'SWITCH_STATE'),deferred_set(none,'VALVE_STATE')])]),event_b_context(none,'Context2',[extends(none,[]),constants(none,[identifier(none,close_door_stimulus),identifier(none,extend_gear_stimulus),identifier(none,open_door_stimulus),identifier(none,retract_gear_stimulus),identifier(none,stop_close_door_stimulus),identifier(none,stop_extend_gear_stimulus),identifier(none,stop_open_door_stimulus),identifier(none,stop_retract_gear_stimulus)]),abstract_constants(none,[]),axioms(none,[partition(rodinpos('Context2',axm1,','),identifier(none,'STIMULI'),[set_extension(none,[identifier(none,open_door_stimulus)]),set_extension(none,[identifier(none,close_door_stimulus)]),set_extension(none,[identifier(none,retract_gear_stimulus)]),set_extension(none,[identifier(none,extend_gear_stimulus)]),set_extension(none,[identifier(none,stop_open_door_stimulus)]),set_extension(none,[identifier(none,stop_close_door_stimulus)]),set_extension(none,[identifier(none,stop_retract_gear_stimulus)]),set_extension(none,[identifier(none,stop_extend_gear_stimulus)])])]),theorems(none,[]),sets(none,[deferred_set(none,'STIMULI')])]),event_b_context(none,'Lights6',[extends(none,[]),constants(none,[identifier(none,bool_to_light),identifier(none,off),identifier(none,on)]),abstract_constants(none,[]),axioms(none,[partition(rodinpos('Lights6',axm1,'*'),identifier(none,'LIGHT_STATE'),[set_extension(none,[identifier(none,on)]),set_extension(none,[identifier(none,off)])]),equal(rodinpos('Lights6',axm2,'_1jDZEXkQEeOBXrBZ8EbeCQ'),identifier(none,bool_to_light),set_extension(none,[couple(none,[boolean_true(none),identifier(none,on)]),couple(none,[boolean_false(none),identifier(none,off)])]))]),theorems(none,[]),sets(none,[deferred_set(none,'LIGHT_STATE')])])],[exporter_version(3),po('Ref6_CockpitLights','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant('R41')],false),po('Ref6_CockpitLights','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant('R42')],false),po('Ref6_CockpitLights','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant('R51')],false),po('Ref6_CockpitLights','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(safe)],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stimulate_open_door_valve),event(con_stimulate_open_door_valve),invariant('R41')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stimulate_open_door_valve),event(con_stimulate_open_door_valve),invariant('R51')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stimulate_open_door_valve),event(con_stimulate_open_door_valve),invariant(safe)],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stop_stimulate_open_door_valve),event(con_stop_stimulate_open_door_valve),invariant('R41')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stop_stimulate_open_door_valve),event(con_stop_stimulate_open_door_valve),invariant('R51')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stop_stimulate_open_door_valve),event(con_stop_stimulate_open_door_valve),invariant(safe)],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stimulate_close_door_valve),event(con_stimulate_close_door_valve),invariant('R41')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stimulate_close_door_valve),event(con_stimulate_close_door_valve),invariant('R51')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stop_stimulate_close_door_valve),event(con_stop_stimulate_close_door_valve),invariant('R41')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stop_stimulate_close_door_valve),event(con_stop_stimulate_close_door_valve),invariant('R51')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stimulate_retract_gear_valve),event(con_stimulate_retract_gear_valve),invariant('R42')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stimulate_retract_gear_valve),event(con_stimulate_retract_gear_valve),invariant('R51')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stimulate_retract_gear_valve),event(con_stimulate_retract_gear_valve),invariant(safe)],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stop_stimulate_retract_gear_valve),event(con_stop_stimulate_retract_gear_valve),invariant('R42')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stop_stimulate_retract_gear_valve),event(con_stop_stimulate_retract_gear_valve),invariant('R51')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stop_stimulate_retract_gear_valve),event(con_stop_stimulate_retract_gear_valve),invariant(safe)],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stimulate_extend_gear_valve),event(con_stimulate_extend_gear_valve),invariant('R42')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stimulate_extend_gear_valve),event(con_stimulate_extend_gear_valve),invariant('R51')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stimulate_extend_gear_valve),event(con_stimulate_extend_gear_valve),invariant(safe)],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stop_stimulate_extend_gear_valve),event(con_stop_stimulate_extend_gear_valve),invariant('R42')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stop_stimulate_extend_gear_valve),event(con_stop_stimulate_extend_gear_valve),invariant('R51')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stop_stimulate_extend_gear_valve),event(con_stop_stimulate_extend_gear_valve),invariant(safe)],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stimulate_general_valve),event(con_stimulate_general_valve),invariant('R51')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_stop_stimulate_general_valve),event(con_stop_stimulate_general_valve),invariant('R51')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_set_anomaly_output),invariant('R41')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_set_anomaly_output),invariant('R42')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_set_anomaly_output),invariant('R51')],false),po('Ref6_CockpitLights','Invariant preservation',[event(con_set_anomaly_output),invariant(safe)],false),po('Ref5_Switch','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(r51)],false),po('Ref5_Switch','Invariant preservation',[event(con_stimulate_open_door_valve),event(con_stimulate_open_door_valve),invariant(r51)],false),po('Ref5_Switch','Invariant preservation',[event(con_stop_stimulate_open_door_valve),event(con_stop_stimulate_open_door_valve),invariant(r51)],false),po('Ref5_Switch','Invariant preservation',[event(con_stimulate_close_door_valve),event(con_stimulate_close_door_valve),invariant(r51)],false),po('Ref5_Switch','Invariant preservation',[event(con_stop_stimulate_close_door_valve),event(con_stop_stimulate_close_door_valve),invariant(r51)],false),po('Ref5_Switch','Invariant preservation',[event(con_stimulate_retract_gear_valve),event(con_stimulate_retract_gear_valve),invariant(r51)],false),po('Ref5_Switch','Invariant preservation',[event(con_stop_stimulate_retract_gear_valve),event(con_stop_stimulate_retract_gear_valve),invariant(r51)],false),po('Ref5_Switch','Invariant preservation',[event(con_stimulate_extend_gear_valve),event(con_stimulate_extend_gear_valve),invariant(r51)],false),po('Ref5_Switch','Invariant preservation',[event(con_stop_stimulate_extend_gear_valve),event(con_stop_stimulate_extend_gear_valve),invariant(r51)],false),po('Ref5_Switch','Invariant preservation',[event(con_stimulate_general_valve),invariant(r51)],false),po('Ref5_Switch','Invariant preservation',[event(con_stop_stimulate_general_valve),invariant(r51)],false),po('Ref4_ControllerHandle','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(handle3)],false),po('Ref4_ControllerHandle','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(r31simple)],false),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stimulate_open_door_valve),event(con_stimulate_open_door_valve),invariant(handle3)],false),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stimulate_open_door_valve),event(con_stimulate_open_door_valve),invariant(r31simple)],false),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stop_stimulate_open_door_valve),event(con_stop_stimulate_open_door_valve),invariant(handle3)],false),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stop_stimulate_open_door_valve),event(con_stop_stimulate_open_door_valve),invariant(r31simple)],false),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stimulate_close_door_valve),event(con_stimulate_close_door_valve),invariant(handle3)],false),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stop_stimulate_close_door_valve),event(con_stop_stimulate_close_door_valve),invariant(handle3)],false),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stimulate_retract_gear_valve),event(con_stimulate_retract_gear_valve),invariant(r31simple)],false),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stop_stimulate_retract_gear_valve),event(con_stop_stimulate_retract_gear_valve),invariant(r31simple)],false),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stimulate_extend_gear_valve),event(con_stimulate_extend_gear_valve),invariant(r31simple)],false),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stop_stimulate_extend_gear_valve),event(con_stop_stimulate_extend_gear_valve),invariant(r31simple)],false),po('Ref4_ControllerHandle','Feasibility of action',[action(act)],false),po('Ref4_ControllerHandle','Feasibility of action',[action(act)],false),po('Ref3_ControllerSensors','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(last_door_action)],true),po('Ref3_ControllerSensors','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(last_door_action2)],false),po('Ref3_ControllerSensors','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(last_gear_action)],true),po('Ref3_ControllerSensors','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(last_gear_action2)],false),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_open_door_valve),event(con_stimulate_open_door_valve),invariant(last_door_action)],false),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_open_door_valve),event(con_stimulate_open_door_valve),invariant(last_door_action2)],false),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_close_door_valve),event(con_stimulate_close_door_valve),invariant(last_door_action)],false),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_close_door_valve),event(con_stimulate_close_door_valve),invariant(last_door_action2)],false),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_retract_gear_valve),event(con_stimulate_retract_gear_valve),invariant(last_gear_action)],false),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_retract_gear_valve),event(con_stimulate_retract_gear_valve),invariant(last_gear_action2)],false),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_extend_gear_valve),event(con_stimulate_extend_gear_valve),invariant(last_gear_action)],false),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_extend_gear_valve),event(con_stimulate_extend_gear_valve),invariant(last_gear_action2)],false),po('Ref2_ControllerOutputs','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant('R41')],false),po('Ref2_ControllerOutputs','Invariant preservation',[event(con_stimulate_open_door_valve),invariant('R41')],false),po('Ref2_ControllerOutputs','Invariant preservation',[event(con_stop_stimulate_open_door_valve),invariant('R41')],false),po('Ref2_ControllerOutputs','Invariant preservation',[event(con_stimulate_close_door_valve),invariant('R41')],false),po('Ref2_ControllerOutputs','Invariant preservation',[event(con_stop_stimulate_close_door_valve),invariant('R41')],false)],_Error)).
2