1		package(load_event_b_project([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')])])],[exporter_version(3),po('Ref4_ControllerHandle','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(handle3)],true),po('Ref4_ControllerHandle','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(r31simple)],true),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stimulate_open_door_valve),event(con_stimulate_open_door_valve),invariant(handle3)],true),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stimulate_open_door_valve),event(con_stimulate_open_door_valve),invariant(r31simple)],true),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stop_stimulate_open_door_valve),event(con_stop_stimulate_open_door_valve),invariant(handle3)],true),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stop_stimulate_open_door_valve),event(con_stop_stimulate_open_door_valve),invariant(r31simple)],true),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stimulate_close_door_valve),event(con_stimulate_close_door_valve),invariant(handle3)],true),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stop_stimulate_close_door_valve),event(con_stop_stimulate_close_door_valve),invariant(handle3)],true),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stimulate_retract_gear_valve),event(con_stimulate_retract_gear_valve),invariant(r31simple)],true),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stop_stimulate_retract_gear_valve),event(con_stop_stimulate_retract_gear_valve),invariant(r31simple)],true),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stimulate_extend_gear_valve),event(con_stimulate_extend_gear_valve),invariant(r31simple)],true),po('Ref4_ControllerHandle','Invariant preservation',[event(con_stop_stimulate_extend_gear_valve),event(con_stop_stimulate_extend_gear_valve),invariant(r31simple)],true),po('Ref4_ControllerHandle','Feasibility of action',[action(act)],true),po('Ref4_ControllerHandle','Feasibility of action',[action(act)],true),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)],true),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)],true),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_open_door_valve),event(con_stimulate_open_door_valve),invariant(last_door_action)],true),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_open_door_valve),event(con_stimulate_open_door_valve),invariant(last_door_action2)],true),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_close_door_valve),event(con_stimulate_close_door_valve),invariant(last_door_action)],true),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_close_door_valve),event(con_stimulate_close_door_valve),invariant(last_door_action2)],true),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_retract_gear_valve),event(con_stimulate_retract_gear_valve),invariant(last_gear_action)],true),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_retract_gear_valve),event(con_stimulate_retract_gear_valve),invariant(last_gear_action2)],true),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_extend_gear_valve),event(con_stimulate_extend_gear_valve),invariant(last_gear_action)],true),po('Ref3_ControllerSensors','Invariant preservation',[event(con_stimulate_extend_gear_valve),event(con_stimulate_extend_gear_valve),invariant(last_gear_action2)],true),po('Ref2_ControllerOutputs','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant('R41')],true),po('Ref2_ControllerOutputs','Invariant preservation',[event(con_stimulate_open_door_valve),invariant('R41')],true),po('Ref2_ControllerOutputs','Invariant preservation',[event(con_stop_stimulate_open_door_valve),invariant('R41')],true),po('Ref2_ControllerOutputs','Invariant preservation',[event(con_stimulate_close_door_valve),invariant('R41')],true),po('Ref2_ControllerOutputs','Invariant preservation',[event(con_stop_stimulate_close_door_valve),invariant('R41')],true)],_Error)).
2