1		package(load_event_b_project([event_b_model(none,'M0',[sees(none,['C0']),variables(none,[identifier(none,'ReceiveTC'),identifier(none,'TCValid_GenerateData'),identifier(none,'TCValid_ReplyDataTM'),identifier(none,'TC_Validation_Fail'),identifier(none,'TC_Validation_Ok')]),invariant(none,[subset(rodinpos(inv1,'+'),identifier(none,'ReceiveTC'),identifier(none,'TC')),subset(rodinpos(inv2,'.'),identifier(none,'TC_Validation_Ok'),identifier(none,'ReceiveTC')),subset(rodinpos(inv3,'_QQ_SEEfbEd-N39pVhh5UbU'),identifier(none,'TCValid_GenerateData'),identifier(none,'TC_Validation_Ok')),subset(rodinpos(inv4,'/'),identifier(none,'TCValid_ReplyDataTM'),identifier(none,'TCValid_GenerateData')),subset(rodinpos(inv5,'7'),identifier(none,'TC_Validation_Fail'),identifier(none,'ReceiveTC')),equal(rodinpos(inv6,'_QQ_SEEfbEd-N39pVhh5UbR'),intersection(none,identifier(none,'TC_Validation_Ok'),identifier(none,'TC_Validation_Fail')),empty_set(none))]),theorems(none,[]),events(none,[event(rodinpos('INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(act1,'\''),[identifier(none,'ReceiveTC')],[empty_set(none)]),assign(rodinpos(act2,'('),[identifier(none,'TC_Validation_Ok')],[empty_set(none)]),assign(rodinpos(act3,'+'),[identifier(none,'TCValid_GenerateData')],[empty_set(none)]),assign(rodinpos(act4,')'),[identifier(none,'TCValid_ReplyDataTM')],[empty_set(none)]),assign(rodinpos(act5,'*'),[identifier(none,'TC_Validation_Fail')],[empty_set(none)])],[]),event(rodinpos('ReceiveTC','1'),'ReceiveTC',ordinary(none),[],[identifier(rodinpos([],'\''),tc)],[member(rodinpos(grd1,')'),identifier(none,tc),set_subtraction(none,identifier(none,'TC'),identifier(none,'ReceiveTC')))],[],[assign(rodinpos(act1,'('),[identifier(none,'ReceiveTC')],[union(none,identifier(none,'ReceiveTC'),set_extension(none,[identifier(none,tc)]))])],[]),event(rodinpos('TC_Validation_Ok','2'),'TC_Validation_Ok',ordinary(none),[],[identifier(rodinpos([],'\''),tc)],[member(rodinpos(grd1,'('),identifier(none,tc),set_subtraction(none,identifier(none,'ReceiveTC'),union(none,identifier(none,'TC_Validation_Ok'),identifier(none,'TC_Validation_Fail'))))],[],[assign(rodinpos(act1,')'),[identifier(none,'TC_Validation_Ok')],[union(none,identifier(none,'TC_Validation_Ok'),set_extension(none,[identifier(none,tc)]))])],[]),event(rodinpos('TCValid_GenerateData','_QQ_SEEfbEd-N39pVhh5UbS'),'TCValid_GenerateData',ordinary(none),[],[identifier(rodinpos([],'\''),tc)],[member(rodinpos(grd1,'('),identifier(none,tc),set_subtraction(none,identifier(none,'TC_Validation_Ok'),identifier(none,'TCValid_GenerateData'))),member(rodinpos(grd2,'*'),function(none,identifier(none,'TC_Type'),[identifier(none,tc)]),set_extension(none,[identifier(none,'HK_on_TC'),identifier(none,'SCI_on_TC')]))],[],[assign(rodinpos(act1,')'),[identifier(none,'TCValid_GenerateData')],[union(none,identifier(none,'TCValid_GenerateData'),set_extension(none,[identifier(none,tc)]))])],[]),event(rodinpos('TCValid_ReplyDataTM','3'),'TCValid_ReplyDataTM',ordinary(none),[],[identifier(rodinpos([],'\''),tc)],[member(rodinpos(grd1,'('),identifier(none,tc),set_subtraction(none,identifier(none,'TCValid_GenerateData'),identifier(none,'TCValid_ReplyDataTM')))],[],[assign(rodinpos(act1,')'),[identifier(none,'TCValid_ReplyDataTM')],[union(none,identifier(none,'TCValid_ReplyDataTM'),set_extension(none,[identifier(none,tc)]))])],[]),event(rodinpos('TC_Validation_Fail','4'),'TC_Validation_Fail',ordinary(none),[],[identifier(rodinpos([],'\''),tc)],[member(rodinpos(grd1,'('),identifier(none,tc),set_subtraction(none,identifier(none,'ReceiveTC'),union(none,identifier(none,'TC_Validation_Ok'),identifier(none,'TC_Validation_Fail'))))],[],[assign(rodinpos(act1,')'),[identifier(none,'TC_Validation_Fail')],[union(none,identifier(none,'TC_Validation_Fail'),set_extension(none,[identifier(none,tc)]))])],[])])])],[event_b_context(none,'C0',[extends(none,[]),constants(none,[identifier(none,'HK_off_TC'),identifier(none,'HK_on_TC'),identifier(none,'SCI_off_TC'),identifier(none,'SCI_on_TC'),identifier(none,'TC'),identifier(none,'TC_Type')]),axioms(none,[equal(rodinpos(axm3,'_TMj5IdnxEeClWIu11FY0Kg'),identifier(none,'TC'),integer_set(none)),equal(rodinpos(axm1,'_MFCk0E4XEd-Ig5BBg6jk3g'),identifier(none,'TC_Types_Set'),set_extension(none,[identifier(none,'HK_on_TC'),identifier(none,'HK_off_TC'),identifier(none,'SCI_on_TC'),identifier(none,'SCI_off_TC')])),member(rodinpos(axm2,'_u2LIYCxgEd-7_7XdqfeyKh'),identifier(none,'TC_Type'),total_function(none,identifier(none,'TC'),identifier(none,'TC_Types_Set')))]),theorems(none,[]),sets(none,[deferred_set(none,'TC_Types_Set')])])],[discharged('M0','INITIALISATION',inv1),discharged('M0','INITIALISATION',inv2),discharged('M0','INITIALISATION',inv3),discharged('M0','INITIALISATION',inv4),discharged('M0','INITIALISATION',inv5),discharged('M0','INITIALISATION',inv6),discharged('M0','ReceiveTC',inv1),discharged('M0','ReceiveTC',inv2),discharged('M0','ReceiveTC',inv5),discharged('M0','TC_Validation_Ok',inv2),discharged('M0','TC_Validation_Ok',inv3),discharged('M0','TC_Validation_Ok',inv6),discharged('M0','TCValid_GenerateData',inv3),discharged('M0','TCValid_GenerateData',inv4),discharged('M0','TCValid_ReplyDataTM',inv4),discharged('M0','TC_Validation_Fail',inv5),discharged('M0','TC_Validation_Fail',inv6)],_Error)).
2