1		package(load_event_b_project([event_b_model(none,m4,[sees(none,[m0_implicitContext,m1_implicitContext,m2_implicitContext,m3_implicitContext,m4_implicitContext]),refines(none,m3),variables(none,[identifier(none,'CS_2_HD_StartsCFTesting'),identifier(none,'CS_LL_CF_NOT_TESTED'),identifier(none,'CS_LL_CF_TESTED_KO'),identifier(none,'CS_LL_CF_TESTED_OK'),identifier(none,'CS_LL_CF_TESTING'),identifier(none,'CS_TopLevel'),identifier(none,'ENDING_sm'),identifier(none,'HDMachine_CFTestedOK'),identifier(none,'HD_2_CS_CFTestingFinished'),identifier(none,'INITIATION_sm'),identifier(none,'PREPARATION_sm')]),invariant(none,[implication(rodinpos(m4,'CS_LowLevel_CFTesting_invariants2','_d72-oL95EeWuMPCp23wdnQ'),equal(none,identifier(none,'CS_LL_CF_NOT_TESTED'),boolean_true(none)),equal(none,identifier(none,'HD_2_CS_CFTestingFinished'),boolean_false(none))),implication(rodinpos(m4,'CS_LowLevel_CFTesting_invariants1','_d73lsL95EeWuMPCp23wdnQ'),equal(none,identifier(none,'CS_LL_CF_TESTED_OK'),boolean_true(none)),equal(none,identifier(none,'HD_2_CS_CFTestingFinished'),boolean_false(none))),implication(rodinpos(m4,'CS_LowLevel_CFTesting_invariants3','_d73lsb95EeWuMPCp23wdnQ'),equal(none,identifier(none,'CS_LL_CF_TESTED_KO'),boolean_true(none)),equal(none,identifier(none,'HD_2_CS_CFTestingFinished'),boolean_false(none))),implication(rodinpos(m4,inv1,'_buRZULSPEeW1p-Q_lMMcSX'),equal(none,identifier(none,'CS_2_HD_StartsCFTesting'),boolean_true(none)),equal(none,identifier(none,'CS_LL_CF_TESTING'),boolean_true(none))),implication(rodinpos(m4,inv2,'_buRZULSPEeW1p-Q_lMMcSZ'),equal(none,identifier(none,'HD_2_CS_CFTestingFinished'),boolean_true(none)),equal(none,identifier(none,'CS_2_HD_StartsCFTesting'),boolean_false(none)))]),theorems(none,[]),events(none,[event(rodinpos(m4,'INITIALISATION','_buRZULSPEeW1p-Q_lMMcSC'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(m4,init_CS_TopLevel,'_JjCZ8LR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'STANDBY')]),assign(rodinpos(m4,init_PREPARATION_sm,'_ttVsILR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'PREPARATION_sm_NULL')]),assign(rodinpos(m4,init_INITIATION_sm,'_ttVsIbR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'INITIATION_sm_NULL')]),assign(rodinpos(m4,init_ENDING_sm,'_ttVsIrR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'ENDING_sm_NULL')]),assign(rodinpos(m4,init_CS_LL_CF_NOT_TESTED,'_0fj3gLUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_NOT_TESTED')],[boolean_true(none)]),assign(rodinpos(m4,init_CS_LL_CF_TESTING,'_0fj3gbUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTING')],[boolean_false(none)]),assign(rodinpos(m4,init_CS_LL_CF_TESTED_OK,'_0fj3grUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_OK')],[boolean_false(none)]),assign(rodinpos(m4,init_CS_LL_CF_TESTED_KO,'_0fj3g7UlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_KO')],[boolean_false(none)]),becomes_element_of(rodinpos(m4,init_HDMachine_CFTestedOK,'\''),[identifier(none,'HDMachine_CFTestedOK')],bool_set(none)),assign(rodinpos(m4,act1,'\''),[identifier(none,'CS_2_HD_StartsCFTesting')],[boolean_false(none)]),assign(rodinpos(m4,act2,'('),[identifier(none,'HD_2_CS_CFTestingFinished')],[boolean_false(none)])],[]),event(rodinpos(m4,'User_PressesOn','_buRZULSPEeW1p-Q_lMMcSD'),'User_PressesOn',ordinary(none),['User_PressesOn'],[],[equal(rodinpos(m4,isin_STANDBY,'_JjCZ8bR5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'STANDBY')),equal(rodinpos(m4,'CS_TopLevel_guards1','_0cjm0LUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_NOT_TESTED'),boolean_true(none))],[],[assign(rodinpos(m4,enter_PREPARATION,'_JjCZ8rR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'PREPARATION')]),assign(rodinpos(m4,enter_CF_TESTING,'_ttVsI7R9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'CF_TESTING')])],[]),event(rodinpos(m4,'HDSystem_StartsConnectingPatient','_buRZULSPEeW1p-Q_lMMcSE'),'HDSystem_StartsConnectingPatient',ordinary(none),['HDSystem_StartsConnectingPatient'],[],[equal(rodinpos(m4,isin_PREPARATION,'_JjCZ87R5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'PREPARATION')),equal(rodinpos(m4,isin_DIALYZER_RINSING,'_ttVsJLR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'DIALYZER_RINSING'))],[],[assign(rodinpos(m4,enter_INITIATION,'_JjDBALR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'INITIATION')]),assign(rodinpos(m4,leave_PREPARATION_sm,'_ttVsJbR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'PREPARATION_sm_NULL')]),assign(rodinpos(m4,enter_PATIENT_CONNECTING,'_ttVsJrR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'PATIENT_CONNECTING')])],[]),event(rodinpos(m4,'HDSystem_StartsReinfusion','_buRZULSPEeW1p-Q_lMMcSF'),'HDSystem_StartsReinfusion',ordinary(none),['HDSystem_StartsReinfusion'],[],[equal(rodinpos(m4,isin_INITIATION,'_JjDBAbR5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'INITIATION')),equal(rodinpos(m4,isin_THERAPY,'_ttWTMLR9EeW1p-Q_lMMcSA'),identifier(none,'INITIATION_sm'),identifier(none,'THERAPY'))],[],[assign(rodinpos(m4,enter_ENDING,'_JjDBArR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'ENDING')]),assign(rodinpos(m4,leave_INITIATION_sm,'_ttWTMbR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'INITIATION_sm_NULL')]),assign(rodinpos(m4,enter_REINFUSION,'_ttWTMrR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'REINFUSION')])],[]),event(rodinpos(m4,'User_PressesOff','_buRZULSPEeW1p-Q_lMMcSG'),'User_PressesOff',ordinary(none),['User_PressesOff'],[],[equal(rodinpos(m4,isin_ENDING,'_JjDBA7R5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'ENDING')),equal(rodinpos(m4,isin_THERAPY_OVERVIEWING,'_ttWTM7R9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'THERAPY_OVERVIEWING'))],[],[assign(rodinpos(m4,enter_STANDBY,'_JjDoELR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'STANDBY')]),assign(rodinpos(m4,leave_ENDING_sm,'_ttWTNLR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'ENDING_sm_NULL')])],[]),event(rodinpos(m4,'CS_TopLevel_StartsConnectingConcentrate','_buRZULSPEeW1p-Q_lMMcSH'),'CS_TopLevel_StartsConnectingConcentrate',ordinary(none),['CS_TopLevel_StartsConnectingConcentrate'],[],[equal(rodinpos(m4,isin_CF_TESTING,'_ttW6QLR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'CF_TESTING')),equal(rodinpos(m4,'PREPARATION_sm_guards1','_0cjm0bUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTED_OK'),boolean_true(none))],[],[assign(rodinpos(m4,enter_CONCENTRATE_CONNECTING,'_ttXhULR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'CONCENTRATE_CONNECTING')])],[]),event(rodinpos(m4,'HDSystem_StartsSettingRP','_buRZULSPEeW1p-Q_lMMcSI'),'HDSystem_StartsSettingRP',ordinary(none),['HDSystem_StartsSettingRP'],[],[equal(rodinpos(m4,isin_CONCENTRATE_CONNECTING,'_ttXhUbR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'CONCENTRATE_CONNECTING'))],[],[assign(rodinpos(m4,enter_RP_SETTING,'_ttXhUrR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'RP_SETTING')])],[]),event(rodinpos(m4,'HDSystem_StartsPreparingTS','_buRZULSPEeW1p-Q_lMMcSJ'),'HDSystem_StartsPreparingTS',ordinary(none),['HDSystem_StartsPreparingTS'],[],[equal(rodinpos(m4,isin_RP_SETTING,'_ttXhU7R9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'RP_SETTING'))],[],[assign(rodinpos(m4,enter_TS_PREPARING,'_ttXhVLR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'TS_PREPARING')])],[]),event(rodinpos(m4,'HDSystem_StartsPreparingHP','_buRZULSPEeW1p-Q_lMMcSK'),'HDSystem_StartsPreparingHP',ordinary(none),['HDSystem_StartsPreparingHP'],[],[equal(rodinpos(m4,isin_TS_PREPARING,'_ttXhVbR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'TS_PREPARING'))],[],[assign(rodinpos(m4,enter_HP_PREPARING,'_ttYIYLR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'HP_PREPARING')])],[]),event(rodinpos(m4,'HDSystem_StartsSettingTP','_buRZULSPEeW1p-Q_lMMcSL'),'HDSystem_StartsSettingTP',ordinary(none),['HDSystem_StartsSettingTP'],[],[equal(rodinpos(m4,isin_HP_PREPARING,'_ttYIYbR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'HP_PREPARING'))],[],[assign(rodinpos(m4,enter_TP_SETTING,'_ttYIYrR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'TP_SETTING')])],[]),event(rodinpos(m4,'HDSystem_StartsRinsingDialyzer','_buRZULSPEeW1p-Q_lMMcSM'),'HDSystem_StartsRinsingDialyzer',ordinary(none),['HDSystem_StartsRinsingDialyzer'],[],[equal(rodinpos(m4,isin_TP_SETTING,'_ttYIY7R9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'TP_SETTING'))],[],[assign(rodinpos(m4,enter_DIALYZER_RINSING,'_ttYIZLR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'DIALYZER_RINSING')])],[]),event(rodinpos(m4,'HDSystem_StartsTherapy','_buRZULSPEeW1p-Q_lMMcSN'),'HDSystem_StartsTherapy',ordinary(none),['HDSystem_StartsTherapy'],[],[equal(rodinpos(m4,isin_PATIENT_CONNECTING,'_ttYIZbR9EeW1p-Q_lMMcSA'),identifier(none,'INITIATION_sm'),identifier(none,'PATIENT_CONNECTING'))],[],[assign(rodinpos(m4,enter_THERAPY,'_ttYIZrR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'THERAPY')])],[]),event(rodinpos(m4,'HDSystem_StartsEmptyingDialyzer','_buRZULSPEeW1p-Q_lMMcSO'),'HDSystem_StartsEmptyingDialyzer',ordinary(none),['HDSystem_StartsEmptyingDialyzer'],[],[equal(rodinpos(m4,isin_REINFUSION,'_ttYvcLR9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'REINFUSION'))],[],[assign(rodinpos(m4,enter_DIALYZER_EMPTYING,'_ttYvcbR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'DIALYZER_EMPTYING')])],[]),event(rodinpos(m4,'HDSystem_StartsEmptyingCartridge','_buRZULSPEeW1p-Q_lMMcSP'),'HDSystem_StartsEmptyingCartridge',ordinary(none),['HDSystem_StartsEmptyingCartridge'],[],[equal(rodinpos(m4,isin_DIALYZER_EMPTYING,'_ttYvcrR9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'DIALYZER_EMPTYING'))],[],[assign(rodinpos(m4,enter_CARTRIDGE_EMPTYING,'_ttYvc7R9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'CARTRIDGE_EMPTYING')])],[]),event(rodinpos(m4,'HDSystem_StartsOverviewingTherapy','_buRZULSPEeW1p-Q_lMMcSQ'),'HDSystem_StartsOverviewingTherapy',ordinary(none),['HDSystem_StartsOverviewingTherapy'],[],[equal(rodinpos(m4,isin_CARTRIDGE_EMPTYING,'_ttYvdLR9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'CARTRIDGE_EMPTYING'))],[],[assign(rodinpos(m4,enter_THERAPY_OVERVIEWING,'_ttZWgLR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'THERAPY_OVERVIEWING')])],[]),event(rodinpos(m4,'CS_LowLevel_StartsTestingCF','_buRZULSPEeW1p-Q_lMMcSR'),'CS_LowLevel_StartsTestingCF',ordinary(none),['CS_LowLevel_StartsTestingCF'],[],[equal(rodinpos(m4,'CS_LowLevel_CFTesting_guards1','_0fmTwLUlEeWNr7Z28XyZAQ'),identifier(none,'PREPARATION_sm'),identifier(none,'CF_TESTING')),equal(rodinpos(m4,isin_CS_LL_CF_NOT_TESTED,'_0fmTwbUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_NOT_TESTED'),boolean_true(none))],[],[assign(rodinpos(m4,leave_CS_LL_CF_NOT_TESTED,'_0fm60LUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_NOT_TESTED')],[boolean_false(none)]),assign(rodinpos(m4,enter_CS_LL_CF_TESTING,'_0fm60bUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTING')],[boolean_true(none)]),assign(rodinpos(m4,act1,'('),[identifier(none,'CS_2_HD_StartsCFTesting')],[boolean_true(none)])],[]),event(rodinpos(m4,'CS_LowLevel_StandsBy','_buRZULSPEeW1p-Q_lMMcSS'),'CS_LowLevel_StandsBy',ordinary(none),['CS_LowLevel_StandsBy'],[],[equal(rodinpos(m4,'CS_LowLevel_CFTesting_guards2','_0fm60rUlEeWNr7Z28XyZAQ'),identifier(none,'CS_TopLevel'),identifier(none,'STANDBY')),equal(rodinpos(m4,isin_CS_LL_CF_TESTED_OK,'_0fm607UlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTED_OK'),boolean_true(none))],[],[assign(rodinpos(m4,leave_CS_LL_CF_TESTED_OK,'_0fm61LUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_OK')],[boolean_false(none)]),assign(rodinpos(m4,enter_CS_LL_CF_NOT_TESTED,'_0fm61bUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_NOT_TESTED')],[boolean_true(none)])],[]),event(rodinpos(m4,'CS_LowLevel_CFTestsOK','_buRZULSPEeW1p-Q_lMMcST'),'CS_LowLevel_CFTestsOK',ordinary(none),['CS_LowLevel_CFTestsOK'],[],[equal(rodinpos(m4,isin_CS_LL_CF_TESTING,'_0fnh4LUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTING'),boolean_true(none)),equal(rodinpos(m4,'CS_LowLevel_CFTesting_guards3','_P7bT8LVsEeWZYZ7CLrnHEQ'),identifier(none,'HDMachine_CFTestedOK'),boolean_true(none)),equal(rodinpos(m4,'CS_LowLevel_CFTesting_guards5','_d71JcL95EeWuMPCp23wdnQ'),identifier(none,'HD_2_CS_CFTestingFinished'),boolean_true(none))],[],[assign(rodinpos(m4,leave_CS_LL_CF_TESTING,'_0fnh4bUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTING')],[boolean_false(none)]),assign(rodinpos(m4,enter_CS_LL_CF_TESTED_OK,'_0fnh4rUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_OK')],[boolean_true(none)]),assign(rodinpos(m4,'CS_LowLevel_CFTesting_actions2','_d71wgL95EeWuMPCp23wdnQ'),[identifier(none,'HD_2_CS_CFTestingFinished')],[boolean_false(none)])],[]),event(rodinpos(m4,'CS_LowLevel_CFTestsKO','_buRZULSPEeW1p-Q_lMMcSU'),'CS_LowLevel_CFTestsKO',ordinary(none),['CS_LowLevel_CFTestsKO'],[],[equal(rodinpos(m4,isin_CS_LL_CF_TESTING,'_0fnh47UlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTING'),boolean_true(none)),equal(rodinpos(m4,'CS_LowLevel_CFTesting_guards4','_P7bT8bVsEeWZYZ7CLrnHEQ'),identifier(none,'HDMachine_CFTestedOK'),boolean_false(none)),equal(rodinpos(m4,'CS_LowLevel_CFTesting_guards6','_d71wgb95EeWuMPCp23wdnQ'),identifier(none,'HD_2_CS_CFTestingFinished'),boolean_true(none))],[],[assign(rodinpos(m4,leave_CS_LL_CF_TESTING,'_0fnh5LUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTING')],[boolean_false(none)]),assign(rodinpos(m4,enter_CS_LL_CF_TESTED_KO,'_0fnh5bUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_KO')],[boolean_true(none)]),assign(rodinpos(m4,'CS_LowLevel_CFTesting_actions1','_d71wgr95EeWuMPCp23wdnQ'),[identifier(none,'HD_2_CS_CFTestingFinished')],[boolean_false(none)])],[]),event(rodinpos(m4,'HDMachine_CFTests','_buRZULSPEeW1p-Q_lMMcSV'),'HDMachine_CFTests',ordinary(none),['HDMachine_CFTests'],[],[equal(rodinpos(m4,grd1,'('),identifier(none,'CS_2_HD_StartsCFTesting'),boolean_true(none))],[],[becomes_element_of(rodinpos(m4,act1,'\''),[identifier(none,'HDMachine_CFTestedOK')],bool_set(none)),assign(rodinpos(m4,act2,')'),[identifier(none,'CS_2_HD_StartsCFTesting')],[boolean_false(none)]),assign(rodinpos(m4,act3,'*'),[identifier(none,'HD_2_CS_CFTestingFinished')],[boolean_true(none)])],[])])]),event_b_model(none,m3,[sees(none,[m0_implicitContext,m1_implicitContext,m2_implicitContext,m3_implicitContext]),refines(none,m2),variables(none,[identifier(none,'CS_LL_CF_NOT_TESTED'),identifier(none,'CS_LL_CF_TESTED_KO'),identifier(none,'CS_LL_CF_TESTED_OK'),identifier(none,'CS_LL_CF_TESTING'),identifier(none,'CS_TopLevel'),identifier(none,'ENDING_sm'),identifier(none,'HDMachine_CFTestedOK'),identifier(none,'INITIATION_sm'),identifier(none,'PREPARATION_sm')]),invariant(none,[]),theorems(none,[member(rodinpos(m3,'HDMachine_CFTestedOK_TYPE','_buRZULSPEeW1p-Q_lMMcSC'),identifier(none,'HDMachine_CFTestedOK'),bool_set(none))]),events(none,[event(rodinpos(m3,'INITIALISATION','_bPvj4LSHEeW1p-Q_lMMcSB'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(m3,init_CS_TopLevel,'_JjCZ8LR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'STANDBY')]),assign(rodinpos(m3,init_PREPARATION_sm,'_ttVsILR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'PREPARATION_sm_NULL')]),assign(rodinpos(m3,init_INITIATION_sm,'_ttVsIbR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'INITIATION_sm_NULL')]),assign(rodinpos(m3,init_ENDING_sm,'_ttVsIrR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'ENDING_sm_NULL')]),assign(rodinpos(m3,init_CS_LL_CF_NOT_TESTED,'_0fj3gLUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_NOT_TESTED')],[boolean_true(none)]),assign(rodinpos(m3,init_CS_LL_CF_TESTING,'_0fj3gbUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTING')],[boolean_false(none)]),assign(rodinpos(m3,init_CS_LL_CF_TESTED_OK,'_0fj3grUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_OK')],[boolean_false(none)]),assign(rodinpos(m3,init_CS_LL_CF_TESTED_KO,'_0fj3g7UlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_KO')],[boolean_false(none)]),becomes_element_of(rodinpos(m3,init_HDMachine_CFTestedOK,'\''),[identifier(none,'HDMachine_CFTestedOK')],bool_set(none))],[]),event(rodinpos(m3,'User_PressesOn','_bPvj4LSHEeW1p-Q_lMMcSC'),'User_PressesOn',ordinary(none),['User_PressesOn'],[],[equal(rodinpos(m3,isin_STANDBY,'_JjCZ8bR5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'STANDBY')),equal(rodinpos(m3,'CS_TopLevel_guards1','_0cjm0LUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_NOT_TESTED'),boolean_true(none))],[],[assign(rodinpos(m3,enter_PREPARATION,'_JjCZ8rR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'PREPARATION')]),assign(rodinpos(m3,enter_CF_TESTING,'_ttVsI7R9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'CF_TESTING')])],[]),event(rodinpos(m3,'HDSystem_StartsConnectingPatient','_bPvj4LSHEeW1p-Q_lMMcSD'),'HDSystem_StartsConnectingPatient',ordinary(none),['HDSystem_StartsConnectingPatient'],[],[equal(rodinpos(m3,isin_PREPARATION,'_JjCZ87R5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'PREPARATION')),equal(rodinpos(m3,isin_DIALYZER_RINSING,'_ttVsJLR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'DIALYZER_RINSING'))],[],[assign(rodinpos(m3,enter_INITIATION,'_JjDBALR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'INITIATION')]),assign(rodinpos(m3,leave_PREPARATION_sm,'_ttVsJbR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'PREPARATION_sm_NULL')]),assign(rodinpos(m3,enter_PATIENT_CONNECTING,'_ttVsJrR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'PATIENT_CONNECTING')])],[]),event(rodinpos(m3,'HDSystem_StartsReinfusion','_bPvj4LSHEeW1p-Q_lMMcSE'),'HDSystem_StartsReinfusion',ordinary(none),['HDSystem_StartsReinfusion'],[],[equal(rodinpos(m3,isin_INITIATION,'_JjDBAbR5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'INITIATION')),equal(rodinpos(m3,isin_THERAPY,'_ttWTMLR9EeW1p-Q_lMMcSA'),identifier(none,'INITIATION_sm'),identifier(none,'THERAPY'))],[],[assign(rodinpos(m3,enter_ENDING,'_JjDBArR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'ENDING')]),assign(rodinpos(m3,leave_INITIATION_sm,'_ttWTMbR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'INITIATION_sm_NULL')]),assign(rodinpos(m3,enter_REINFUSION,'_ttWTMrR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'REINFUSION')])],[]),event(rodinpos(m3,'User_PressesOff','_bPvj4LSHEeW1p-Q_lMMcSF'),'User_PressesOff',ordinary(none),['User_PressesOff'],[],[equal(rodinpos(m3,isin_ENDING,'_JjDBA7R5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'ENDING')),equal(rodinpos(m3,isin_THERAPY_OVERVIEWING,'_ttWTM7R9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'THERAPY_OVERVIEWING'))],[],[assign(rodinpos(m3,enter_STANDBY,'_JjDoELR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'STANDBY')]),assign(rodinpos(m3,leave_ENDING_sm,'_ttWTNLR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'ENDING_sm_NULL')])],[]),event(rodinpos(m3,'CS_TopLevel_StartsConnectingConcentrate','_bPvj4LSHEeW1p-Q_lMMcSG'),'CS_TopLevel_StartsConnectingConcentrate',ordinary(none),['HDSystem_StartsConnectingConcentrate'],[],[equal(rodinpos(m3,isin_CF_TESTING,'_ttW6QLR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'CF_TESTING')),equal(rodinpos(m3,'PREPARATION_sm_guards1','_0cjm0bUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTED_OK'),boolean_true(none))],[],[assign(rodinpos(m3,enter_CONCENTRATE_CONNECTING,'_ttXhULR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'CONCENTRATE_CONNECTING')])],[]),event(rodinpos(m3,'HDSystem_StartsSettingRP','_bPvj4LSHEeW1p-Q_lMMcSH'),'HDSystem_StartsSettingRP',ordinary(none),['HDSystem_StartsSettingRP'],[],[equal(rodinpos(m3,isin_CONCENTRATE_CONNECTING,'_ttXhUbR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'CONCENTRATE_CONNECTING'))],[],[assign(rodinpos(m3,enter_RP_SETTING,'_ttXhUrR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'RP_SETTING')])],[]),event(rodinpos(m3,'HDSystem_StartsPreparingTS','_bPvj4LSHEeW1p-Q_lMMcSI'),'HDSystem_StartsPreparingTS',ordinary(none),['HDSystem_StartsPreparingTS'],[],[equal(rodinpos(m3,isin_RP_SETTING,'_ttXhU7R9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'RP_SETTING'))],[],[assign(rodinpos(m3,enter_TS_PREPARING,'_ttXhVLR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'TS_PREPARING')])],[]),event(rodinpos(m3,'HDSystem_StartsPreparingHP','_bPvj4LSHEeW1p-Q_lMMcSJ'),'HDSystem_StartsPreparingHP',ordinary(none),['HDSystem_StartsPreparingHP'],[],[equal(rodinpos(m3,isin_TS_PREPARING,'_ttXhVbR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'TS_PREPARING'))],[],[assign(rodinpos(m3,enter_HP_PREPARING,'_ttYIYLR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'HP_PREPARING')])],[]),event(rodinpos(m3,'HDSystem_StartsSettingTP','_bPvj4LSHEeW1p-Q_lMMcSK'),'HDSystem_StartsSettingTP',ordinary(none),['HDSystem_StartsSettingTP'],[],[equal(rodinpos(m3,isin_HP_PREPARING,'_ttYIYbR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'HP_PREPARING'))],[],[assign(rodinpos(m3,enter_TP_SETTING,'_ttYIYrR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'TP_SETTING')])],[]),event(rodinpos(m3,'HDSystem_StartsRinsingDialyzer','_bPvj4LSHEeW1p-Q_lMMcSL'),'HDSystem_StartsRinsingDialyzer',ordinary(none),['HDSystem_StartsRinsingDialyzer'],[],[equal(rodinpos(m3,isin_TP_SETTING,'_ttYIY7R9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'TP_SETTING'))],[],[assign(rodinpos(m3,enter_DIALYZER_RINSING,'_ttYIZLR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'DIALYZER_RINSING')])],[]),event(rodinpos(m3,'HDSystem_StartsTherapy','_bPvj4LSHEeW1p-Q_lMMcSM'),'HDSystem_StartsTherapy',ordinary(none),['HDSystem_StartsTherapy'],[],[equal(rodinpos(m3,isin_PATIENT_CONNECTING,'_ttYIZbR9EeW1p-Q_lMMcSA'),identifier(none,'INITIATION_sm'),identifier(none,'PATIENT_CONNECTING'))],[],[assign(rodinpos(m3,enter_THERAPY,'_ttYIZrR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'THERAPY')])],[]),event(rodinpos(m3,'HDSystem_StartsEmptyingDialyzer','_bPvj4LSHEeW1p-Q_lMMcSN'),'HDSystem_StartsEmptyingDialyzer',ordinary(none),['HDSystem_StartsEmptyingDialyzer'],[],[equal(rodinpos(m3,isin_REINFUSION,'_ttYvcLR9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'REINFUSION'))],[],[assign(rodinpos(m3,enter_DIALYZER_EMPTYING,'_ttYvcbR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'DIALYZER_EMPTYING')])],[]),event(rodinpos(m3,'HDSystem_StartsEmptyingCartridge','_bPvj4LSHEeW1p-Q_lMMcSO'),'HDSystem_StartsEmptyingCartridge',ordinary(none),['HDSystem_StartsEmptyingCartridge'],[],[equal(rodinpos(m3,isin_DIALYZER_EMPTYING,'_ttYvcrR9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'DIALYZER_EMPTYING'))],[],[assign(rodinpos(m3,enter_CARTRIDGE_EMPTYING,'_ttYvc7R9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'CARTRIDGE_EMPTYING')])],[]),event(rodinpos(m3,'HDSystem_StartsOverviewingTherapy','_bPvj4LSHEeW1p-Q_lMMcSP'),'HDSystem_StartsOverviewingTherapy',ordinary(none),['HDSystem_StartsOverviewingTherapy'],[],[equal(rodinpos(m3,isin_CARTRIDGE_EMPTYING,'_ttYvdLR9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'CARTRIDGE_EMPTYING'))],[],[assign(rodinpos(m3,enter_THERAPY_OVERVIEWING,'_ttZWgLR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'THERAPY_OVERVIEWING')])],[]),event(rodinpos(m3,'CS_LowLevel_StartsTestingCF','_bPvj4LSHEeW1p-Q_lMMcSQ'),'CS_LowLevel_StartsTestingCF',ordinary(none),['CS_LowLevel_StartsTestingCF'],[],[equal(rodinpos(m3,'CS_LowLevel_CFTesting_guards1','_0fmTwLUlEeWNr7Z28XyZAQ'),identifier(none,'PREPARATION_sm'),identifier(none,'CF_TESTING')),equal(rodinpos(m3,isin_CS_LL_CF_NOT_TESTED,'_0fmTwbUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_NOT_TESTED'),boolean_true(none))],[],[assign(rodinpos(m3,leave_CS_LL_CF_NOT_TESTED,'_0fm60LUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_NOT_TESTED')],[boolean_false(none)]),assign(rodinpos(m3,enter_CS_LL_CF_TESTING,'_0fm60bUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTING')],[boolean_true(none)])],[]),event(rodinpos(m3,'CS_LowLevel_StandsBy','_bPvj4LSHEeW1p-Q_lMMcSR'),'CS_LowLevel_StandsBy',ordinary(none),['CS_LowLevel_StandsBy'],[],[equal(rodinpos(m3,'CS_LowLevel_CFTesting_guards2','_0fm60rUlEeWNr7Z28XyZAQ'),identifier(none,'CS_TopLevel'),identifier(none,'STANDBY')),equal(rodinpos(m3,isin_CS_LL_CF_TESTED_OK,'_0fm607UlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTED_OK'),boolean_true(none))],[],[assign(rodinpos(m3,leave_CS_LL_CF_TESTED_OK,'_0fm61LUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_OK')],[boolean_false(none)]),assign(rodinpos(m3,enter_CS_LL_CF_NOT_TESTED,'_0fm61bUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_NOT_TESTED')],[boolean_true(none)])],[]),event(rodinpos(m3,'CS_LowLevel_CFTestsOK','_bPvj4LSHEeW1p-Q_lMMcSS'),'CS_LowLevel_CFTestsOK',ordinary(none),['CS_LowLevel_CFTestsOK'],[],[equal(rodinpos(m3,isin_CS_LL_CF_TESTING,'_0fnh4LUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTING'),boolean_true(none)),equal(rodinpos(m3,'CS_LowLevel_CFTesting_guards3','_P7bT8LVsEeWZYZ7CLrnHEQ'),identifier(none,'HDMachine_CFTestedOK'),boolean_true(none))],[],[assign(rodinpos(m3,leave_CS_LL_CF_TESTING,'_0fnh4bUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTING')],[boolean_false(none)]),assign(rodinpos(m3,enter_CS_LL_CF_TESTED_OK,'_0fnh4rUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_OK')],[boolean_true(none)])],[]),event(rodinpos(m3,'CS_LowLevel_CFTestsKO','_bPvj4LSHEeW1p-Q_lMMcST'),'CS_LowLevel_CFTestsKO',ordinary(none),['CS_LowLevel_CFTestsKO'],[],[equal(rodinpos(m3,isin_CS_LL_CF_TESTING,'_0fnh47UlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTING'),boolean_true(none)),equal(rodinpos(m3,'CS_LowLevel_CFTesting_guards4','_P7bT8bVsEeWZYZ7CLrnHEQ'),identifier(none,'HDMachine_CFTestedOK'),boolean_false(none))],[],[assign(rodinpos(m3,leave_CS_LL_CF_TESTING,'_0fnh5LUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTING')],[boolean_false(none)]),assign(rodinpos(m3,enter_CS_LL_CF_TESTED_KO,'_0fnh5bUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_KO')],[boolean_true(none)])],[]),event(rodinpos(m3,'HDMachine_CFTests','_buRZULSPEeW1p-Q_lMMcSD'),'HDMachine_CFTests',ordinary(none),[],[],[equal(rodinpos(m3,grd1,'('),identifier(none,'CS_LL_CF_TESTING'),boolean_true(none))],[],[becomes_element_of(rodinpos(m3,act1,'\''),[identifier(none,'HDMachine_CFTestedOK')],bool_set(none))],[])])]),event_b_model(none,m2,[sees(none,[m0_implicitContext,m1_implicitContext,m2_implicitContext]),refines(none,m1),variables(none,[identifier(none,'CS_LL_CF_NOT_TESTED'),identifier(none,'CS_LL_CF_TESTED_KO'),identifier(none,'CS_LL_CF_TESTED_OK'),identifier(none,'CS_LL_CF_TESTING'),identifier(none,'CS_TopLevel'),identifier(none,'ENDING_sm'),identifier(none,'INITIATION_sm'),identifier(none,'PREPARATION_sm')]),invariant(none,[member(rodinpos(m2,typeof_CS_LL_CF_NOT_TESTED,'_0foI8LUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_NOT_TESTED'),bool_set(none)),member(rodinpos(m2,typeof_CS_LL_CF_TESTING,'_0foI8bUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTING'),bool_set(none)),member(rodinpos(m2,typeof_CS_LL_CF_TESTED_OK,'_0foI8rUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTED_OK'),bool_set(none)),member(rodinpos(m2,typeof_CS_LL_CF_TESTED_KO,'_0foI87UlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTED_KO'),bool_set(none)),partition(rodinpos(m2,distinct_states_in_CS_LowLevel_CFTesting,'_0foI9LUlEeWNr7Z28XyZAQ'),set_extension(none,[boolean_true(none)]),[intersection(none,set_extension(none,[identifier(none,'CS_LL_CF_NOT_TESTED')]),set_extension(none,[boolean_true(none)])),intersection(none,set_extension(none,[identifier(none,'CS_LL_CF_TESTING')]),set_extension(none,[boolean_true(none)])),intersection(none,set_extension(none,[identifier(none,'CS_LL_CF_TESTED_OK')]),set_extension(none,[boolean_true(none)])),intersection(none,set_extension(none,[identifier(none,'CS_LL_CF_TESTED_KO')]),set_extension(none,[boolean_true(none)]))]),implication(rodinpos(m2,'CS_TopLevel_invariants1','_0cn4QbUlEeWNr7Z28XyZAQ'),equal(none,identifier(none,'CS_TopLevel'),identifier(none,'PREPARATION')),implication(none,not_equal(none,identifier(none,'PREPARATION_sm'),identifier(none,'CF_TESTING')),equal(none,identifier(none,'CS_LL_CF_TESTED_OK'),boolean_true(none)))),implication(rodinpos(m2,'CS_TopLevel_invariants2','_0cn4QrUlEeWNr7Z28XyZAQ'),equal(none,identifier(none,'CS_TopLevel'),identifier(none,'INITIATION')),equal(none,identifier(none,'CS_LL_CF_TESTED_OK'),boolean_true(none))),implication(rodinpos(m2,'CS_TopLevel_invariants3','_0cn4Q7UlEeWNr7Z28XyZAQ'),equal(none,identifier(none,'CS_TopLevel'),identifier(none,'ENDING')),equal(none,identifier(none,'CS_LL_CF_TESTED_OK'),boolean_true(none)))]),theorems(none,[]),events(none,[event(rodinpos(m2,'INITIALISATION','_ttZWhLR9EeW1p-Q_lMMcSB'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(m2,init_CS_TopLevel,'_JjCZ8LR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'STANDBY')]),assign(rodinpos(m2,init_PREPARATION_sm,'_ttVsILR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'PREPARATION_sm_NULL')]),assign(rodinpos(m2,init_INITIATION_sm,'_ttVsIbR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'INITIATION_sm_NULL')]),assign(rodinpos(m2,init_ENDING_sm,'_ttVsIrR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'ENDING_sm_NULL')]),assign(rodinpos(m2,init_CS_LL_CF_NOT_TESTED,'_0fj3gLUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_NOT_TESTED')],[boolean_true(none)]),assign(rodinpos(m2,init_CS_LL_CF_TESTING,'_0fj3gbUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTING')],[boolean_false(none)]),assign(rodinpos(m2,init_CS_LL_CF_TESTED_OK,'_0fj3grUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_OK')],[boolean_false(none)]),assign(rodinpos(m2,init_CS_LL_CF_TESTED_KO,'_0fj3g7UlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_KO')],[boolean_false(none)])],[]),event(rodinpos(m2,'User_PressesOn','_ttZWhLR9EeW1p-Q_lMMcSC'),'User_PressesOn',ordinary(none),['HDSystem_StartsTestingCF'],[],[equal(rodinpos(m2,isin_STANDBY,'_JjCZ8bR5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'STANDBY')),equal(rodinpos(m2,'CS_TopLevel_guards1','_0cjm0LUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_NOT_TESTED'),boolean_true(none))],[],[assign(rodinpos(m2,enter_PREPARATION,'_JjCZ8rR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'PREPARATION')]),assign(rodinpos(m2,enter_CF_TESTING,'_ttVsI7R9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'CF_TESTING')])],[]),event(rodinpos(m2,'HDSystem_StartsConnectingPatient','_ttZWhLR9EeW1p-Q_lMMcSD'),'HDSystem_StartsConnectingPatient',ordinary(none),['HDSystem_StartsConnectingPatient'],[],[equal(rodinpos(m2,isin_PREPARATION,'_JjCZ87R5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'PREPARATION')),equal(rodinpos(m2,isin_DIALYZER_RINSING,'_ttVsJLR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'DIALYZER_RINSING'))],[],[assign(rodinpos(m2,enter_INITIATION,'_JjDBALR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'INITIATION')]),assign(rodinpos(m2,leave_PREPARATION_sm,'_ttVsJbR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'PREPARATION_sm_NULL')]),assign(rodinpos(m2,enter_PATIENT_CONNECTING,'_ttVsJrR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'PATIENT_CONNECTING')])],[]),event(rodinpos(m2,'HDSystem_StartsReinfusion','_ttZWhLR9EeW1p-Q_lMMcSE'),'HDSystem_StartsReinfusion',ordinary(none),['HDSystem_StartsReinfusion'],[],[equal(rodinpos(m2,isin_INITIATION,'_JjDBAbR5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'INITIATION')),equal(rodinpos(m2,isin_THERAPY,'_ttWTMLR9EeW1p-Q_lMMcSA'),identifier(none,'INITIATION_sm'),identifier(none,'THERAPY'))],[],[assign(rodinpos(m2,enter_ENDING,'_JjDBArR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'ENDING')]),assign(rodinpos(m2,leave_INITIATION_sm,'_ttWTMbR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'INITIATION_sm_NULL')]),assign(rodinpos(m2,enter_REINFUSION,'_ttWTMrR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'REINFUSION')])],[]),event(rodinpos(m2,'User_PressesOff','_ttZWhLR9EeW1p-Q_lMMcSF'),'User_PressesOff',ordinary(none),['HDSystem_StartsStandingBy'],[],[equal(rodinpos(m2,isin_ENDING,'_JjDBA7R5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'ENDING')),equal(rodinpos(m2,isin_THERAPY_OVERVIEWING,'_ttWTM7R9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'THERAPY_OVERVIEWING'))],[],[assign(rodinpos(m2,enter_STANDBY,'_JjDoELR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'STANDBY')]),assign(rodinpos(m2,leave_ENDING_sm,'_ttWTNLR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'ENDING_sm_NULL')])],[]),event(rodinpos(m2,'HDSystem_StartsConnectingConcentrate','_ttZWhLR9EeW1p-Q_lMMcSG'),'HDSystem_StartsConnectingConcentrate',ordinary(none),['HDSystem_StartsConnectingConcentrate'],[],[equal(rodinpos(m2,isin_CF_TESTING,'_ttW6QLR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'CF_TESTING')),equal(rodinpos(m2,'PREPARATION_sm_guards1','_0cjm0bUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTED_OK'),boolean_true(none))],[],[assign(rodinpos(m2,enter_CONCENTRATE_CONNECTING,'_ttXhULR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'CONCENTRATE_CONNECTING')])],[]),event(rodinpos(m2,'HDSystem_StartsSettingRP','_ttZWhLR9EeW1p-Q_lMMcSH'),'HDSystem_StartsSettingRP',ordinary(none),['HDSystem_StartsSettingRP'],[],[equal(rodinpos(m2,isin_CONCENTRATE_CONNECTING,'_ttXhUbR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'CONCENTRATE_CONNECTING'))],[],[assign(rodinpos(m2,enter_RP_SETTING,'_ttXhUrR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'RP_SETTING')])],[]),event(rodinpos(m2,'HDSystem_StartsPreparingTS','_ttZWhLR9EeW1p-Q_lMMcSI'),'HDSystem_StartsPreparingTS',ordinary(none),['HDSystem_StartsPreparingTS'],[],[equal(rodinpos(m2,isin_RP_SETTING,'_ttXhU7R9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'RP_SETTING'))],[],[assign(rodinpos(m2,enter_TS_PREPARING,'_ttXhVLR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'TS_PREPARING')])],[]),event(rodinpos(m2,'HDSystem_StartsPreparingHP','_ttZWhLR9EeW1p-Q_lMMcSJ'),'HDSystem_StartsPreparingHP',ordinary(none),['HDSystem_StartsPreparingHP'],[],[equal(rodinpos(m2,isin_TS_PREPARING,'_ttXhVbR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'TS_PREPARING'))],[],[assign(rodinpos(m2,enter_HP_PREPARING,'_ttYIYLR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'HP_PREPARING')])],[]),event(rodinpos(m2,'HDSystem_StartsSettingTP','_ttZWhLR9EeW1p-Q_lMMcSK'),'HDSystem_StartsSettingTP',ordinary(none),['HDSystem_StartsSettingTP'],[],[equal(rodinpos(m2,isin_HP_PREPARING,'_ttYIYbR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'HP_PREPARING'))],[],[assign(rodinpos(m2,enter_TP_SETTING,'_ttYIYrR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'TP_SETTING')])],[]),event(rodinpos(m2,'HDSystem_StartsRinsingDialyzer','_ttZWhLR9EeW1p-Q_lMMcSL'),'HDSystem_StartsRinsingDialyzer',ordinary(none),['HDSystem_StartsRinsingDialyzer'],[],[equal(rodinpos(m2,isin_TP_SETTING,'_ttYIY7R9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'TP_SETTING'))],[],[assign(rodinpos(m2,enter_DIALYZER_RINSING,'_ttYIZLR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'DIALYZER_RINSING')])],[]),event(rodinpos(m2,'HDSystem_StartsTherapy','_ttZWhLR9EeW1p-Q_lMMcSM'),'HDSystem_StartsTherapy',ordinary(none),['HDSystem_StartsTherapy'],[],[equal(rodinpos(m2,isin_PATIENT_CONNECTING,'_ttYIZbR9EeW1p-Q_lMMcSA'),identifier(none,'INITIATION_sm'),identifier(none,'PATIENT_CONNECTING'))],[],[assign(rodinpos(m2,enter_THERAPY,'_ttYIZrR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'THERAPY')])],[]),event(rodinpos(m2,'HDSystem_StartsEmptyingDialyzer','_ttZWhLR9EeW1p-Q_lMMcSN'),'HDSystem_StartsEmptyingDialyzer',ordinary(none),['HDSystem_StartsEmptyingDialyzer'],[],[equal(rodinpos(m2,isin_REINFUSION,'_ttYvcLR9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'REINFUSION'))],[],[assign(rodinpos(m2,enter_DIALYZER_EMPTYING,'_ttYvcbR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'DIALYZER_EMPTYING')])],[]),event(rodinpos(m2,'HDSystem_StartsEmptyingCartridge','_ttZWhLR9EeW1p-Q_lMMcSO'),'HDSystem_StartsEmptyingCartridge',ordinary(none),['HDSystem_StartsEmptyingCartridge'],[],[equal(rodinpos(m2,isin_DIALYZER_EMPTYING,'_ttYvcrR9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'DIALYZER_EMPTYING'))],[],[assign(rodinpos(m2,enter_CARTRIDGE_EMPTYING,'_ttYvc7R9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'CARTRIDGE_EMPTYING')])],[]),event(rodinpos(m2,'HDSystem_StartsOverviewingTherapy','_ttZWhLR9EeW1p-Q_lMMcSP'),'HDSystem_StartsOverviewingTherapy',ordinary(none),['HDSystem_StartsOverviewingTherapy'],[],[equal(rodinpos(m2,isin_CARTRIDGE_EMPTYING,'_ttYvdLR9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'CARTRIDGE_EMPTYING'))],[],[assign(rodinpos(m2,enter_THERAPY_OVERVIEWING,'_ttZWgLR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'THERAPY_OVERVIEWING')])],[]),event(rodinpos(m2,'CS_LowLevel_StartsTestingCF','_91cCALSGEeW1p-Q_lMMcSA'),'CS_LowLevel_StartsTestingCF',ordinary(none),[],[],[equal(rodinpos(m2,'CS_LowLevel_CFTesting_guards1','_0fmTwLUlEeWNr7Z28XyZAQ'),identifier(none,'PREPARATION_sm'),identifier(none,'CF_TESTING')),equal(rodinpos(m2,isin_CS_LL_CF_NOT_TESTED,'_0fmTwbUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_NOT_TESTED'),boolean_true(none))],[],[assign(rodinpos(m2,leave_CS_LL_CF_NOT_TESTED,'_0fm60LUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_NOT_TESTED')],[boolean_false(none)]),assign(rodinpos(m2,enter_CS_LL_CF_TESTING,'_0fm60bUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTING')],[boolean_true(none)])],[]),event(rodinpos(m2,'CS_LowLevel_StandsBy','_91cCAbSGEeW1p-Q_lMMcSA'),'CS_LowLevel_StandsBy',ordinary(none),[],[],[equal(rodinpos(m2,'CS_LowLevel_CFTesting_guards2','_0fm60rUlEeWNr7Z28XyZAQ'),identifier(none,'CS_TopLevel'),identifier(none,'STANDBY')),equal(rodinpos(m2,isin_CS_LL_CF_TESTED_OK,'_0fm607UlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTED_OK'),boolean_true(none))],[],[assign(rodinpos(m2,leave_CS_LL_CF_TESTED_OK,'_0fm61LUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_OK')],[boolean_false(none)]),assign(rodinpos(m2,enter_CS_LL_CF_NOT_TESTED,'_0fm61bUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_NOT_TESTED')],[boolean_true(none)])],[]),event(rodinpos(m2,'CS_LowLevel_CFTestsOK','_91cCArSGEeW1p-Q_lMMcSA'),'CS_LowLevel_CFTestsOK',ordinary(none),[],[],[equal(rodinpos(m2,isin_CS_LL_CF_TESTING,'_0fnh4LUlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTING'),boolean_true(none))],[],[assign(rodinpos(m2,leave_CS_LL_CF_TESTING,'_0fnh4bUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTING')],[boolean_false(none)]),assign(rodinpos(m2,enter_CS_LL_CF_TESTED_OK,'_0fnh4rUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_OK')],[boolean_true(none)])],[]),event(rodinpos(m2,'CS_LowLevel_CFTestsKO','_91cCA7SGEeW1p-Q_lMMcSA'),'CS_LowLevel_CFTestsKO',ordinary(none),[],[],[equal(rodinpos(m2,isin_CS_LL_CF_TESTING,'_0fnh47UlEeWNr7Z28XyZAQ'),identifier(none,'CS_LL_CF_TESTING'),boolean_true(none))],[],[assign(rodinpos(m2,leave_CS_LL_CF_TESTING,'_0fnh5LUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTING')],[boolean_false(none)]),assign(rodinpos(m2,enter_CS_LL_CF_TESTED_KO,'_0fnh5bUlEeWNr7Z28XyZAQ'),[identifier(none,'CS_LL_CF_TESTED_KO')],[boolean_true(none)])],[])])]),event_b_model(none,m1,[sees(none,[m0_implicitContext,m1_implicitContext]),refines(none,m0),variables(none,[identifier(none,'CS_TopLevel'),identifier(none,'ENDING_sm'),identifier(none,'INITIATION_sm'),identifier(none,'PREPARATION_sm')]),invariant(none,[member(rodinpos(m1,typeof_PREPARATION_sm,'_ttZWhbR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'PREPARATION_sm_STATES')),member(rodinpos(m1,typeof_INITIATION_sm,'_ttZWhrR9EeW1p-Q_lMMcSA'),identifier(none,'INITIATION_sm'),identifier(none,'INITIATION_sm_STATES')),member(rodinpos(m1,typeof_ENDING_sm,'_ttZWh7R9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'ENDING_sm_STATES')),equivalence(rodinpos(m1,superstateof_PREPARATION_sm,'_ttZWiLR9EeW1p-Q_lMMcSA'),not_equal(none,identifier(none,'PREPARATION_sm'),identifier(none,'PREPARATION_sm_NULL')),equal(none,identifier(none,'CS_TopLevel'),identifier(none,'PREPARATION'))),equivalence(rodinpos(m1,superstateof_INITIATION_sm,'_ttZ9kLR9EeW1p-Q_lMMcSA'),not_equal(none,identifier(none,'INITIATION_sm'),identifier(none,'INITIATION_sm_NULL')),equal(none,identifier(none,'CS_TopLevel'),identifier(none,'INITIATION'))),equivalence(rodinpos(m1,superstateof_ENDING_sm,'_ttZ9kbR9EeW1p-Q_lMMcSA'),not_equal(none,identifier(none,'ENDING_sm'),identifier(none,'ENDING_sm_NULL')),equal(none,identifier(none,'CS_TopLevel'),identifier(none,'ENDING')))]),theorems(none,[]),events(none,[event(rodinpos(m1,'INITIALISATION','_egXkoKJTEeWzIMhBFfqG3R'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(m1,init_CS_TopLevel,'_JjCZ8LR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'STANDBY')]),assign(rodinpos(m1,init_PREPARATION_sm,'_ttVsILR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'PREPARATION_sm_NULL')]),assign(rodinpos(m1,init_INITIATION_sm,'_ttVsIbR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'INITIATION_sm_NULL')]),assign(rodinpos(m1,init_ENDING_sm,'_ttVsIrR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'ENDING_sm_NULL')])],[]),event(rodinpos(m1,'HDSystem_StartsTestingCF','_egXkoKJTEeWzIMhBFfqG3S'),'HDSystem_StartsTestingCF',ordinary(none),['HDSystem_Prepares'],[],[equal(rodinpos(m1,isin_STANDBY,'_JjCZ8bR5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'STANDBY'))],[],[assign(rodinpos(m1,enter_PREPARATION,'_JjCZ8rR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'PREPARATION')]),assign(rodinpos(m1,enter_CF_TESTING,'_ttVsI7R9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'CF_TESTING')])],[]),event(rodinpos(m1,'HDSystem_StartsConnectingPatient','_egXkoKJTEeWzIMhBFfqG3T'),'HDSystem_StartsConnectingPatient',ordinary(none),['HDSystem_Initiates'],[],[equal(rodinpos(m1,isin_PREPARATION,'_JjCZ87R5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'PREPARATION')),equal(rodinpos(m1,isin_DIALYZER_RINSING,'_ttVsJLR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'DIALYZER_RINSING'))],[],[assign(rodinpos(m1,enter_INITIATION,'_JjDBALR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'INITIATION')]),assign(rodinpos(m1,leave_PREPARATION_sm,'_ttVsJbR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'PREPARATION_sm_NULL')]),assign(rodinpos(m1,enter_PATIENT_CONNECTING,'_ttVsJrR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'PATIENT_CONNECTING')])],[]),event(rodinpos(m1,'HDSystem_StartsReinfusion','_egXkoKJTEeWzIMhBFfqG3U'),'HDSystem_StartsReinfusion',ordinary(none),['HDSystem_Ends'],[],[equal(rodinpos(m1,isin_INITIATION,'_JjDBAbR5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'INITIATION')),equal(rodinpos(m1,isin_THERAPY,'_ttWTMLR9EeW1p-Q_lMMcSA'),identifier(none,'INITIATION_sm'),identifier(none,'THERAPY'))],[],[assign(rodinpos(m1,enter_ENDING,'_JjDBArR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'ENDING')]),assign(rodinpos(m1,leave_INITIATION_sm,'_ttWTMbR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'INITIATION_sm_NULL')]),assign(rodinpos(m1,enter_REINFUSION,'_ttWTMrR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'REINFUSION')])],[]),event(rodinpos(m1,'HDSystem_StartsStandingBy','_egXkoKJTEeWzIMhBFfqG3V'),'HDSystem_StartsStandingBy',ordinary(none),['HDSystem_StandsBy'],[],[equal(rodinpos(m1,isin_ENDING,'_JjDBA7R5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'ENDING')),equal(rodinpos(m1,isin_THERAPY_OVERVIEWING,'_ttWTM7R9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'THERAPY_OVERVIEWING'))],[],[assign(rodinpos(m1,enter_STANDBY,'_JjDoELR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'STANDBY')]),assign(rodinpos(m1,leave_ENDING_sm,'_ttWTNLR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'ENDING_sm_NULL')])],[]),event(rodinpos(m1,'HDSystem_StartsConnectingConcentrate','_JHqEILQ6EeW1p-Q_lMMcSA'),'HDSystem_StartsConnectingConcentrate',ordinary(none),[],[],[equal(rodinpos(m1,isin_CF_TESTING,'_ttW6QLR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'CF_TESTING'))],[],[assign(rodinpos(m1,enter_CONCENTRATE_CONNECTING,'_ttXhULR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'CONCENTRATE_CONNECTING')])],[]),event(rodinpos(m1,'HDSystem_StartsSettingRP','_XmAkELQ6EeW1p-Q_lMMcSA'),'HDSystem_StartsSettingRP',ordinary(none),[],[],[equal(rodinpos(m1,isin_CONCENTRATE_CONNECTING,'_ttXhUbR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'CONCENTRATE_CONNECTING'))],[],[assign(rodinpos(m1,enter_RP_SETTING,'_ttXhUrR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'RP_SETTING')])],[]),event(rodinpos(m1,'HDSystem_StartsPreparingTS','_hfJzcLQ6EeW1p-Q_lMMcSA'),'HDSystem_StartsPreparingTS',ordinary(none),[],[],[equal(rodinpos(m1,isin_RP_SETTING,'_ttXhU7R9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'RP_SETTING'))],[],[assign(rodinpos(m1,enter_TS_PREPARING,'_ttXhVLR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'TS_PREPARING')])],[]),event(rodinpos(m1,'HDSystem_StartsPreparingHP','_oYozwLQ6EeW1p-Q_lMMcSA'),'HDSystem_StartsPreparingHP',ordinary(none),[],[],[equal(rodinpos(m1,isin_TS_PREPARING,'_ttXhVbR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'TS_PREPARING'))],[],[assign(rodinpos(m1,enter_HP_PREPARING,'_ttYIYLR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'HP_PREPARING')])],[]),event(rodinpos(m1,'HDSystem_StartsSettingTP','_xp4T0LR1EeW1p-Q_lMMcSA'),'HDSystem_StartsSettingTP',ordinary(none),[],[],[equal(rodinpos(m1,isin_HP_PREPARING,'_ttYIYbR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'HP_PREPARING'))],[],[assign(rodinpos(m1,enter_TP_SETTING,'_ttYIYrR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'TP_SETTING')])],[]),event(rodinpos(m1,'HDSystem_StartsRinsingDialyzer','_BRMm8LR2EeW1p-Q_lMMcSA'),'HDSystem_StartsRinsingDialyzer',ordinary(none),[],[],[equal(rodinpos(m1,isin_TP_SETTING,'_ttYIY7R9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm'),identifier(none,'TP_SETTING'))],[],[assign(rodinpos(m1,enter_DIALYZER_RINSING,'_ttYIZLR9EeW1p-Q_lMMcSA'),[identifier(none,'PREPARATION_sm')],[identifier(none,'DIALYZER_RINSING')])],[]),event(rodinpos(m1,'HDSystem_StartsTherapy','_GW8G0LR4EeW1p-Q_lMMcSA'),'HDSystem_StartsTherapy',ordinary(none),[],[],[equal(rodinpos(m1,isin_PATIENT_CONNECTING,'_ttYIZbR9EeW1p-Q_lMMcSA'),identifier(none,'INITIATION_sm'),identifier(none,'PATIENT_CONNECTING'))],[],[assign(rodinpos(m1,enter_THERAPY,'_ttYIZrR9EeW1p-Q_lMMcSA'),[identifier(none,'INITIATION_sm')],[identifier(none,'THERAPY')])],[]),event(rodinpos(m1,'HDSystem_StartsEmptyingDialyzer','_i1CfILR4EeW1p-Q_lMMcSA'),'HDSystem_StartsEmptyingDialyzer',ordinary(none),[],[],[equal(rodinpos(m1,isin_REINFUSION,'_ttYvcLR9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'REINFUSION'))],[],[assign(rodinpos(m1,enter_DIALYZER_EMPTYING,'_ttYvcbR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'DIALYZER_EMPTYING')])],[]),event(rodinpos(m1,'HDSystem_StartsEmptyingCartridge','_qVG-ULR4EeW1p-Q_lMMcSA'),'HDSystem_StartsEmptyingCartridge',ordinary(none),[],[],[equal(rodinpos(m1,isin_DIALYZER_EMPTYING,'_ttYvcrR9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'DIALYZER_EMPTYING'))],[],[assign(rodinpos(m1,enter_CARTRIDGE_EMPTYING,'_ttYvc7R9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'CARTRIDGE_EMPTYING')])],[]),event(rodinpos(m1,'HDSystem_StartsOverviewingTherapy','_0fo4oLR4EeW1p-Q_lMMcSA'),'HDSystem_StartsOverviewingTherapy',ordinary(none),[],[],[equal(rodinpos(m1,isin_CARTRIDGE_EMPTYING,'_ttYvdLR9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm'),identifier(none,'CARTRIDGE_EMPTYING'))],[],[assign(rodinpos(m1,enter_THERAPY_OVERVIEWING,'_ttZWgLR9EeW1p-Q_lMMcSA'),[identifier(none,'ENDING_sm')],[identifier(none,'THERAPY_OVERVIEWING')])],[])])]),event_b_model(none,m0,[sees(none,[m0_implicitContext]),variables(none,[identifier(none,'CS_TopLevel')]),invariant(none,[member(rodinpos(m0,typeof_CS_TopLevel,'_JjEPILR5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'CS_TopLevel_STATES'))]),theorems(none,[]),events(none,[event(rodinpos(m0,'INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(m0,init_CS_TopLevel,'_JjCZ8LR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'STANDBY')])],[]),event(rodinpos(m0,'HDSystem_Prepares','_M2qGgKJUEeWzIMhBFfqG3Q'),'HDSystem_Prepares',ordinary(none),[],[],[equal(rodinpos(m0,isin_STANDBY,'_JjCZ8bR5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'STANDBY'))],[],[assign(rodinpos(m0,enter_PREPARATION,'_JjCZ8rR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'PREPARATION')])],[]),event(rodinpos(m0,'HDSystem_Initiates','_M2qtkKJUEeWzIMhBFfqG3Q'),'HDSystem_Initiates',ordinary(none),[],[],[equal(rodinpos(m0,isin_PREPARATION,'_JjCZ87R5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'PREPARATION'))],[],[assign(rodinpos(m0,enter_INITIATION,'_JjDBALR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'INITIATION')])],[]),event(rodinpos(m0,'HDSystem_Ends','_M2qtkaJUEeWzIMhBFfqG3Q'),'HDSystem_Ends',ordinary(none),[],[],[equal(rodinpos(m0,isin_INITIATION,'_JjDBAbR5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'INITIATION'))],[],[assign(rodinpos(m0,enter_ENDING,'_JjDBArR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'ENDING')])],[]),event(rodinpos(m0,'HDSystem_StandsBy','_OIxOoKJUEeWzIMhBFfqG3Q'),'HDSystem_StandsBy',ordinary(none),[],[],[equal(rodinpos(m0,isin_ENDING,'_JjDBA7R5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel'),identifier(none,'ENDING'))],[],[assign(rodinpos(m0,enter_STANDBY,'_JjDoELR5EeW1p-Q_lMMcSA'),[identifier(none,'CS_TopLevel')],[identifier(none,'STANDBY')])],[])])])],[event_b_context(none,m0_implicitContext,[extends(none,[]),constants(none,[identifier(none,'ENDING'),identifier(none,'HDSystem_END'),identifier(none,'HDSystem_INIT'),identifier(none,'HDSystem_PREP'),identifier(none,'HDSystem_STANDBY'),identifier(none,'INITIATION'),identifier(none,'PREPARATION'),identifier(none,'STANDBY')]),abstract_constants(none,[]),axioms(none,[member(rodinpos(m0_implicitContext,typeof_STANDBY,'_JjNZELR5EeW1p-Q_lMMcSA'),identifier(none,'STANDBY'),identifier(none,'CS_TopLevel_STATES')),member(rodinpos(m0_implicitContext,typeof_PREPARATION,'_JjNZEbR5EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION'),identifier(none,'CS_TopLevel_STATES')),member(rodinpos(m0_implicitContext,typeof_INITIATION,'_JjNZErR5EeW1p-Q_lMMcSA'),identifier(none,'INITIATION'),identifier(none,'CS_TopLevel_STATES')),member(rodinpos(m0_implicitContext,typeof_ENDING,'_JjOAILR5EeW1p-Q_lMMcSA'),identifier(none,'ENDING'),identifier(none,'CS_TopLevel_STATES')),partition(rodinpos(m0_implicitContext,distinct_states_in_CS_TopLevel_STATES,'_JjOAIbR5EeW1p-Q_lMMcSA'),identifier(none,'CS_TopLevel_STATES'),[set_extension(none,[identifier(none,'STANDBY')]),set_extension(none,[identifier(none,'PREPARATION')]),set_extension(none,[identifier(none,'INITIATION')]),set_extension(none,[identifier(none,'ENDING')])]),member(rodinpos(m0_implicitContext,typeof_HDSystem_STANDBY,'_637ds6PgEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_STANDBY'),identifier(none,'HDSystem_STATES')),member(rodinpos(m0_implicitContext,typeof_HDSystem_PREP,'_637dtKPgEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_PREP'),identifier(none,'HDSystem_STATES')),member(rodinpos(m0_implicitContext,typeof_HDSystem_INIT,'_638EwKPgEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_INIT'),identifier(none,'HDSystem_STATES')),member(rodinpos(m0_implicitContext,typeof_HDSystem_END,'_638EwaPgEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_END'),identifier(none,'HDSystem_STATES')),partition(rodinpos(m0_implicitContext,distinct_states_in_HDSystem_STATES,'_638EwqPgEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_STATES'),[set_extension(none,[identifier(none,'HDSystem_STANDBY')]),set_extension(none,[identifier(none,'HDSystem_PREP')]),set_extension(none,[identifier(none,'HDSystem_INIT')]),set_extension(none,[identifier(none,'HDSystem_END')])])]),theorems(none,[]),sets(none,[deferred_set(none,'CS_TopLevel_STATES'),deferred_set(none,'HDSystem_STATES')])]),event_b_context(none,m1_implicitContext,[extends(none,[m0_implicitContext]),constants(none,[identifier(none,'CARTRIDGE_EMPTYING'),identifier(none,'CF_TESTING'),identifier(none,'CONCENTRATE_CONNECTING'),identifier(none,'DIALYZER_EMPTYING'),identifier(none,'DIALYZER_RINSING'),identifier(none,'ENDING_sm_NULL'),identifier(none,'HDSystem_ConnectingConcentrate'),identifier(none,'HDSystem_ConnectingPatient'),identifier(none,'HDSystem_DisplayingOverview'),identifier(none,'HDSystem_END_sm_NULL'),identifier(none,'HDSystem_EmptyingCartridge'),identifier(none,'HDSystem_EmptyingDialyzer'),identifier(none,'HDSystem_INIT_sm_NULL'),identifier(none,'HDSystem_PREP_sm_NULL'),identifier(none,'HDSystem_PreparingHP'),identifier(none,'HDSystem_PreparingTubingSystem'),identifier(none,'HDSystem_Reinfusion'),identifier(none,'HDSystem_RinsingDialyzer'),identifier(none,'HDSystem_SettingRinsingParameters'),identifier(none,'HDSystem_SettingTreatmentParameters'),identifier(none,'HDSystem_Testing'),identifier(none,'HDSystem_Therapy'),identifier(none,'HP_PREPARING'),identifier(none,'INITIATION_sm_NULL'),identifier(none,'PATIENT_CONNECTING'),identifier(none,'PREPARATION_sm_NULL'),identifier(none,'REINFUSION'),identifier(none,'RP_SETTING'),identifier(none,'THERAPY'),identifier(none,'THERAPY_OVERVIEWING'),identifier(none,'TP_SETTING'),identifier(none,'TS_PREPARING')]),abstract_constants(none,[]),axioms(none,[member(rodinpos(m1_implicitContext,typeof_PREPARATION_sm_NULL,'_tth5YLR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm_NULL'),identifier(none,'PREPARATION_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_INITIATION_sm_NULL,'_ttigcLR9EeW1p-Q_lMMcSA'),identifier(none,'INITIATION_sm_NULL'),identifier(none,'INITIATION_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_ENDING_sm_NULL,'_ttigcbR9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm_NULL'),identifier(none,'ENDING_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_CF_TESTING,'_ttigcrR9EeW1p-Q_lMMcSA'),identifier(none,'CF_TESTING'),identifier(none,'PREPARATION_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_CONCENTRATE_CONNECTING,'_ttigc7R9EeW1p-Q_lMMcSA'),identifier(none,'CONCENTRATE_CONNECTING'),identifier(none,'PREPARATION_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_RP_SETTING,'_ttigdLR9EeW1p-Q_lMMcSA'),identifier(none,'RP_SETTING'),identifier(none,'PREPARATION_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_TS_PREPARING,'_ttigdbR9EeW1p-Q_lMMcSA'),identifier(none,'TS_PREPARING'),identifier(none,'PREPARATION_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HP_PREPARING,'_ttigdrR9EeW1p-Q_lMMcSA'),identifier(none,'HP_PREPARING'),identifier(none,'PREPARATION_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_TP_SETTING,'_ttigd7R9EeW1p-Q_lMMcSA'),identifier(none,'TP_SETTING'),identifier(none,'PREPARATION_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_DIALYZER_RINSING,'_ttjHgLR9EeW1p-Q_lMMcSA'),identifier(none,'DIALYZER_RINSING'),identifier(none,'PREPARATION_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_PATIENT_CONNECTING,'_ttjHgbR9EeW1p-Q_lMMcSA'),identifier(none,'PATIENT_CONNECTING'),identifier(none,'INITIATION_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_THERAPY,'_ttjHgrR9EeW1p-Q_lMMcSA'),identifier(none,'THERAPY'),identifier(none,'INITIATION_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_REINFUSION,'_ttjHg7R9EeW1p-Q_lMMcSA'),identifier(none,'REINFUSION'),identifier(none,'ENDING_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_DIALYZER_EMPTYING,'_ttjHhLR9EeW1p-Q_lMMcSA'),identifier(none,'DIALYZER_EMPTYING'),identifier(none,'ENDING_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_CARTRIDGE_EMPTYING,'_ttjHhbR9EeW1p-Q_lMMcSA'),identifier(none,'CARTRIDGE_EMPTYING'),identifier(none,'ENDING_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_THERAPY_OVERVIEWING,'_ttjukLR9EeW1p-Q_lMMcSA'),identifier(none,'THERAPY_OVERVIEWING'),identifier(none,'ENDING_sm_STATES')),partition(rodinpos(m1_implicitContext,distinct_states_in_PREPARATION_sm_STATES,'_ttjukbR9EeW1p-Q_lMMcSA'),identifier(none,'PREPARATION_sm_STATES'),[set_extension(none,[identifier(none,'CF_TESTING')]),set_extension(none,[identifier(none,'CONCENTRATE_CONNECTING')]),set_extension(none,[identifier(none,'RP_SETTING')]),set_extension(none,[identifier(none,'TS_PREPARING')]),set_extension(none,[identifier(none,'HP_PREPARING')]),set_extension(none,[identifier(none,'TP_SETTING')]),set_extension(none,[identifier(none,'DIALYZER_RINSING')]),set_extension(none,[identifier(none,'PREPARATION_sm_NULL')])]),partition(rodinpos(m1_implicitContext,distinct_states_in_INITIATION_sm_STATES,'_ttjukrR9EeW1p-Q_lMMcSA'),identifier(none,'INITIATION_sm_STATES'),[set_extension(none,[identifier(none,'PATIENT_CONNECTING')]),set_extension(none,[identifier(none,'THERAPY')]),set_extension(none,[identifier(none,'INITIATION_sm_NULL')])]),partition(rodinpos(m1_implicitContext,distinct_states_in_ENDING_sm_STATES,'_ttjuk7R9EeW1p-Q_lMMcSA'),identifier(none,'ENDING_sm_STATES'),[set_extension(none,[identifier(none,'REINFUSION')]),set_extension(none,[identifier(none,'DIALYZER_EMPTYING')]),set_extension(none,[identifier(none,'CARTRIDGE_EMPTYING')]),set_extension(none,[identifier(none,'THERAPY_OVERVIEWING')]),set_extension(none,[identifier(none,'ENDING_sm_NULL')])]),member(rodinpos(m1_implicitContext,typeof_HDSystem_PREP_sm_NULL,'_IYzzUqPiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_PREP_sm_NULL'),identifier(none,'HDSystem_PREP_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_INIT_sm_NULL,'_IYzzU6PiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_INIT_sm_NULL'),identifier(none,'HDSystem_INIT_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_END_sm_NULL,'_IYzzVKPiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_END_sm_NULL'),identifier(none,'HDSystem_END_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_Testing,'_IYzzVaPiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_Testing'),identifier(none,'HDSystem_PREP_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_ConnectingConcentrate,'_IYzzVqPiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_ConnectingConcentrate'),identifier(none,'HDSystem_PREP_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_SettingRinsingParameters,'_IYzzV6PiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_SettingRinsingParameters'),identifier(none,'HDSystem_PREP_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_PreparingTubingSystem,'_IYzzWKPiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_PreparingTubingSystem'),identifier(none,'HDSystem_PREP_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_PreparingHP,'_IY0aYKPiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_PreparingHP'),identifier(none,'HDSystem_PREP_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_SettingTreatmentParameters,'_IY0aYaPiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_SettingTreatmentParameters'),identifier(none,'HDSystem_PREP_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_RinsingDialyzer,'_IY0aYqPiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_RinsingDialyzer'),identifier(none,'HDSystem_PREP_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_ConnectingPatient,'_IY0aY6PiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_ConnectingPatient'),identifier(none,'HDSystem_INIT_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_Therapy,'_IY0aZKPiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_Therapy'),identifier(none,'HDSystem_INIT_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_Reinfusion,'_IY0aZaPiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_Reinfusion'),identifier(none,'HDSystem_END_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_EmptyingDialyzer,'_IY0aZqPiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_EmptyingDialyzer'),identifier(none,'HDSystem_END_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_EmptyingCartridge,'_IY0aZ6PiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_EmptyingCartridge'),identifier(none,'HDSystem_END_sm_STATES')),member(rodinpos(m1_implicitContext,typeof_HDSystem_DisplayingOverview,'_IY1BcKPiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_DisplayingOverview'),identifier(none,'HDSystem_END_sm_STATES')),partition(rodinpos(m1_implicitContext,distinct_states_in_HDSystem_PREP_sm_STATES,'_IY1BcaPiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_PREP_sm_STATES'),[set_extension(none,[identifier(none,'HDSystem_Testing')]),set_extension(none,[identifier(none,'HDSystem_ConnectingConcentrate')]),set_extension(none,[identifier(none,'HDSystem_SettingRinsingParameters')]),set_extension(none,[identifier(none,'HDSystem_PreparingTubingSystem')]),set_extension(none,[identifier(none,'HDSystem_PreparingHP')]),set_extension(none,[identifier(none,'HDSystem_SettingTreatmentParameters')]),set_extension(none,[identifier(none,'HDSystem_RinsingDialyzer')]),set_extension(none,[identifier(none,'HDSystem_PREP_sm_NULL')])]),partition(rodinpos(m1_implicitContext,distinct_states_in_HDSystem_INIT_sm_STATES,'_IY1BcqPiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_INIT_sm_STATES'),[set_extension(none,[identifier(none,'HDSystem_ConnectingPatient')]),set_extension(none,[identifier(none,'HDSystem_Therapy')]),set_extension(none,[identifier(none,'HDSystem_INIT_sm_NULL')])]),partition(rodinpos(m1_implicitContext,distinct_states_in_HDSystem_END_sm_STATES,'_IY1Bc6PiEeWaQrtEc5Lq6g'),identifier(none,'HDSystem_END_sm_STATES'),[set_extension(none,[identifier(none,'HDSystem_Reinfusion')]),set_extension(none,[identifier(none,'HDSystem_EmptyingDialyzer')]),set_extension(none,[identifier(none,'HDSystem_EmptyingCartridge')]),set_extension(none,[identifier(none,'HDSystem_DisplayingOverview')]),set_extension(none,[identifier(none,'HDSystem_END_sm_NULL')])])]),theorems(none,[]),sets(none,[deferred_set(none,'ENDING_sm_STATES'),deferred_set(none,'HDSystem_END_sm_STATES'),deferred_set(none,'HDSystem_INIT_sm_STATES'),deferred_set(none,'HDSystem_PREP_sm_STATES'),deferred_set(none,'INITIATION_sm_STATES'),deferred_set(none,'PREPARATION_sm_STATES')])]),event_b_context(none,m2_implicitContext,[extends(none,[m1_implicitContext]),constants(none,[]),abstract_constants(none,[]),axioms(none,[]),theorems(none,[]),sets(none,[])]),event_b_context(none,m3_implicitContext,[extends(none,[m2_implicitContext]),constants(none,[]),abstract_constants(none,[]),axioms(none,[]),theorems(none,[]),sets(none,[])]),event_b_context(none,m4_implicitContext,[extends(none,[m3_implicitContext]),constants(none,[]),abstract_constants(none,[]),axioms(none,[]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po(m4,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant('CS_LowLevel_CFTesting_invariants2')],true),po(m4,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant('CS_LowLevel_CFTesting_invariants1')],true),po(m4,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant('CS_LowLevel_CFTesting_invariants3')],true),po(m4,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po(m4,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po(m4,'Invariant preservation',[event('CS_LowLevel_StartsTestingCF'),event('CS_LowLevel_StartsTestingCF'),invariant('CS_LowLevel_CFTesting_invariants2')],true),po(m4,'Invariant preservation',[event('CS_LowLevel_StartsTestingCF'),event('CS_LowLevel_StartsTestingCF'),invariant(inv1)],true),po(m4,'Invariant preservation',[event('CS_LowLevel_StartsTestingCF'),event('CS_LowLevel_StartsTestingCF'),invariant(inv2)],true),po(m4,'Invariant preservation',[event('CS_LowLevel_StandsBy'),event('CS_LowLevel_StandsBy'),invariant('CS_LowLevel_CFTesting_invariants2')],true),po(m4,'Invariant preservation',[event('CS_LowLevel_StandsBy'),event('CS_LowLevel_StandsBy'),invariant('CS_LowLevel_CFTesting_invariants1')],true),po(m4,'Invariant preservation',[event('CS_LowLevel_CFTestsOK'),event('CS_LowLevel_CFTestsOK'),invariant('CS_LowLevel_CFTesting_invariants2')],true),po(m4,'Invariant preservation',[event('CS_LowLevel_CFTestsOK'),event('CS_LowLevel_CFTestsOK'),invariant('CS_LowLevel_CFTesting_invariants1')],true),po(m4,'Invariant preservation',[event('CS_LowLevel_CFTestsOK'),event('CS_LowLevel_CFTestsOK'),invariant('CS_LowLevel_CFTesting_invariants3')],true),po(m4,'Invariant preservation',[event('CS_LowLevel_CFTestsOK'),event('CS_LowLevel_CFTestsOK'),invariant(inv1)],true),po(m4,'Invariant preservation',[event('CS_LowLevel_CFTestsOK'),event('CS_LowLevel_CFTestsOK'),invariant(inv2)],true),po(m4,'Invariant preservation',[event('CS_LowLevel_CFTestsKO'),event('CS_LowLevel_CFTestsKO'),invariant('CS_LowLevel_CFTesting_invariants2')],true),po(m4,'Invariant preservation',[event('CS_LowLevel_CFTestsKO'),event('CS_LowLevel_CFTestsKO'),invariant('CS_LowLevel_CFTesting_invariants1')],true),po(m4,'Invariant preservation',[event('CS_LowLevel_CFTestsKO'),event('CS_LowLevel_CFTestsKO'),invariant('CS_LowLevel_CFTesting_invariants3')],true),po(m4,'Invariant preservation',[event('CS_LowLevel_CFTestsKO'),event('CS_LowLevel_CFTestsKO'),invariant(inv1)],true),po(m4,'Invariant preservation',[event('CS_LowLevel_CFTestsKO'),event('CS_LowLevel_CFTestsKO'),invariant(inv2)],true),po(m4,'Invariant preservation',[event('HDMachine_CFTests'),event('HDMachine_CFTests'),invariant('CS_LowLevel_CFTesting_invariants2')],true),po(m4,'Invariant preservation',[event('HDMachine_CFTests'),event('HDMachine_CFTests'),invariant('CS_LowLevel_CFTesting_invariants1')],true),po(m4,'Invariant preservation',[event('HDMachine_CFTests'),event('HDMachine_CFTests'),invariant('CS_LowLevel_CFTesting_invariants3')],true),po(m4,'Invariant preservation',[event('HDMachine_CFTests'),event('HDMachine_CFTests'),invariant(inv1)],true),po(m4,'Invariant preservation',[event('HDMachine_CFTests'),event('HDMachine_CFTests'),invariant(inv2)],true),po(m4,'Guard strengthening (split)',[event('HDMachine_CFTests'),guard(grd1),event('HDMachine_CFTests'),event('HDMachine_CFTests')],true),po(m3,'Feasibility of action',[action(init_HDMachine_CFTestedOK)],true),po(m3,'Feasibility of action',[action(act1)],true),po(m2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(distinct_states_in_CS_LowLevel_CFTesting)],true),po(m2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant('CS_TopLevel_invariants1')],true),po(m2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant('CS_TopLevel_invariants2')],true),po(m2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant('CS_TopLevel_invariants3')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsTestingCF'),event('User_PressesOn'),invariant('CS_TopLevel_invariants1')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsTestingCF'),event('User_PressesOn'),invariant('CS_TopLevel_invariants2')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsTestingCF'),event('User_PressesOn'),invariant('CS_TopLevel_invariants3')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsConnectingPatient'),event('HDSystem_StartsConnectingPatient'),invariant('CS_TopLevel_invariants1')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsConnectingPatient'),event('HDSystem_StartsConnectingPatient'),invariant('CS_TopLevel_invariants2')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsConnectingPatient'),event('HDSystem_StartsConnectingPatient'),invariant('CS_TopLevel_invariants3')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsReinfusion'),event('HDSystem_StartsReinfusion'),invariant('CS_TopLevel_invariants1')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsReinfusion'),event('HDSystem_StartsReinfusion'),invariant('CS_TopLevel_invariants2')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsReinfusion'),event('HDSystem_StartsReinfusion'),invariant('CS_TopLevel_invariants3')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsStandingBy'),event('User_PressesOff'),invariant('CS_TopLevel_invariants1')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsStandingBy'),event('User_PressesOff'),invariant('CS_TopLevel_invariants2')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsStandingBy'),event('User_PressesOff'),invariant('CS_TopLevel_invariants3')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsConnectingConcentrate'),event('HDSystem_StartsConnectingConcentrate'),invariant('CS_TopLevel_invariants1')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsSettingRP'),event('HDSystem_StartsSettingRP'),invariant('CS_TopLevel_invariants1')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsPreparingTS'),event('HDSystem_StartsPreparingTS'),invariant('CS_TopLevel_invariants1')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsPreparingHP'),event('HDSystem_StartsPreparingHP'),invariant('CS_TopLevel_invariants1')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsSettingTP'),event('HDSystem_StartsSettingTP'),invariant('CS_TopLevel_invariants1')],true),po(m2,'Invariant preservation',[event('HDSystem_StartsRinsingDialyzer'),event('HDSystem_StartsRinsingDialyzer'),invariant('CS_TopLevel_invariants1')],true),po(m2,'Invariant preservation',[event('CS_LowLevel_StartsTestingCF'),invariant(distinct_states_in_CS_LowLevel_CFTesting)],true),po(m2,'Invariant preservation',[event('CS_LowLevel_StandsBy'),invariant(distinct_states_in_CS_LowLevel_CFTesting)],true),po(m2,'Invariant preservation',[event('CS_LowLevel_StandsBy'),invariant('CS_TopLevel_invariants1')],true),po(m2,'Invariant preservation',[event('CS_LowLevel_StandsBy'),invariant('CS_TopLevel_invariants2')],true),po(m2,'Invariant preservation',[event('CS_LowLevel_StandsBy'),invariant('CS_TopLevel_invariants3')],true),po(m2,'Invariant preservation',[event('CS_LowLevel_CFTestsOK'),invariant(distinct_states_in_CS_LowLevel_CFTesting)],true),po(m2,'Invariant preservation',[event('CS_LowLevel_CFTestsOK'),invariant('CS_TopLevel_invariants1')],true),po(m2,'Invariant preservation',[event('CS_LowLevel_CFTestsOK'),invariant('CS_TopLevel_invariants2')],true),po(m2,'Invariant preservation',[event('CS_LowLevel_CFTestsOK'),invariant('CS_TopLevel_invariants3')],true),po(m2,'Invariant preservation',[event('CS_LowLevel_CFTestsKO'),invariant(distinct_states_in_CS_LowLevel_CFTesting)],true),po(m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(superstateof_PREPARATION_sm)],true),po(m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(superstateof_INITIATION_sm)],true),po(m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(superstateof_ENDING_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_Prepares'),event('HDSystem_StartsTestingCF'),invariant(superstateof_PREPARATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_Prepares'),event('HDSystem_StartsTestingCF'),invariant(superstateof_INITIATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_Prepares'),event('HDSystem_StartsTestingCF'),invariant(superstateof_ENDING_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_Initiates'),event('HDSystem_StartsConnectingPatient'),invariant(superstateof_PREPARATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_Initiates'),event('HDSystem_StartsConnectingPatient'),invariant(superstateof_INITIATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_Initiates'),event('HDSystem_StartsConnectingPatient'),invariant(superstateof_ENDING_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_Ends'),event('HDSystem_StartsReinfusion'),invariant(superstateof_PREPARATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_Ends'),event('HDSystem_StartsReinfusion'),invariant(superstateof_INITIATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_Ends'),event('HDSystem_StartsReinfusion'),invariant(superstateof_ENDING_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_StandsBy'),event('HDSystem_StartsStandingBy'),invariant(superstateof_PREPARATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_StandsBy'),event('HDSystem_StartsStandingBy'),invariant(superstateof_INITIATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_StandsBy'),event('HDSystem_StartsStandingBy'),invariant(superstateof_ENDING_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_StartsConnectingConcentrate'),invariant(superstateof_PREPARATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_StartsSettingRP'),invariant(superstateof_PREPARATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_StartsPreparingTS'),invariant(superstateof_PREPARATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_StartsPreparingHP'),invariant(superstateof_PREPARATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_StartsSettingTP'),invariant(superstateof_PREPARATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_StartsRinsingDialyzer'),invariant(superstateof_PREPARATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_StartsTherapy'),invariant(superstateof_INITIATION_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_StartsEmptyingDialyzer'),invariant(superstateof_ENDING_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_StartsEmptyingCartridge'),invariant(superstateof_ENDING_sm)],true),po(m1,'Invariant preservation',[event('HDSystem_StartsOverviewingTherapy'),invariant(superstateof_ENDING_sm)],true)],_Error)).
2