1		package(load_event_b_project([event_b_model(none,'M2',[sees(none,['C1','C2']),refines(none,'M1'),variables(none,[identifier(none,authorised),identifier(none,location),identifier(none,valid)]),invariant(none,[subset(rodinpos('M2',inv4,'_8uZH4N1HEeGJ88a0BTYTjQ'),identifier(none,valid),identifier(none,'TOKEN')),forall(rodinpos('M2',inv5,'_gPGhUB0EEeKJjdIh10j4Wg'),[identifier(none,t)],implication(none,member(none,identifier(none,t),identifier(none,valid)),subset(none,image(none,identifier(none,takeplace),set_extension(none,[function(none,identifier(none,room),[identifier(none,t)])])),image(none,identifier(none,authorised),set_extension(none,[function(none,identifier(none,holder),[identifier(none,t)])])))))]),theorems(none,[]),events(none,[event(rodinpos('M2','INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('M2',act1,internal_act1),[identifier(none,authorised)],[empty_set(none)]),assign(rodinpos('M2',act2,'_d0lXkN1GEeGJ88a0BTYTjQ'),[identifier(none,location)],[empty_set(none)]),assign(rodinpos('M2',act3,internal_act4),[identifier(none,valid)],[empty_set(none)])],[]),event(rodinpos('M2','AddAuth',internal_evt2),'AddAuth',ordinary(none),['AddAuth'],[identifier(rodinpos('M2',[],internal_var2),a),identifier(rodinpos('M2',[],internal_var1),u)],[member(rodinpos('M2',grd1,internal_grd1),identifier(none,u),identifier(none,'USER')),member(rodinpos('M2',grd2,internal_grd2),identifier(none,a),identifier(none,'ACTIVITY'))],[],[assign(rodinpos('M2',act1,internal_act1),[identifier(none,authorised)],[union(none,identifier(none,authorised),set_extension(none,[couple(none,[identifier(none,u),identifier(none,a)])]))])],[]),event(rodinpos('M2','GetValidToken','_84oYcR0CEeKJjdIh10j4Wg'),'GetValidToken',ordinary(none),[],[identifier(rodinpos('M2',[],'_84o_gR0CEeKJjdIh10j4Wg'),r),identifier(rodinpos('M2',[],'_84o_gh0CEeKJjdIh10j4Wg'),t),identifier(rodinpos('M2',[],'_84o_gB0CEeKJjdIh10j4Wg'),u)],[member(rodinpos('M2',grd1,'_84o_gx0CEeKJjdIh10j4Wg'),identifier(none,u),identifier(none,'USER')),member(rodinpos('M2',grd2,'_84pmkB0CEeKJjdIh10j4Wg'),identifier(none,r),identifier(none,'ROOM')),subset(rodinpos('M2',grd4,'_84pmkR0CEeKJjdIh10j4Wg'),image(none,identifier(none,takeplace),set_extension(none,[identifier(none,r)])),image(none,identifier(none,authorised),set_extension(none,[identifier(none,u)]))),member(rodinpos('M2',grd3,'_84pmkh0CEeKJjdIh10j4Wg'),identifier(none,t),set_subtraction(none,identifier(none,'TOKEN'),identifier(none,valid))),equal(rodinpos('M2',grd5,'_84pmkx0CEeKJjdIh10j4Wg'),function(none,identifier(none,room),[identifier(none,t)]),identifier(none,r)),equal(rodinpos('M2',grd6,'_84qNoB0CEeKJjdIh10j4Wg'),function(none,identifier(none,holder),[identifier(none,t)]),identifier(none,u))],[],[assign(rodinpos('M2',act1,'_84qNoR0CEeKJjdIh10j4Wg'),[identifier(none,valid)],[union(none,identifier(none,valid),set_extension(none,[identifier(none,t)]))])],[]),event(rodinpos('M2','Enter',internal_evt3),'Enter',ordinary(none),['Enter'],[identifier(rodinpos('M2',[],internal_var2),r),identifier(rodinpos('M2',[],internal_var3),t),identifier(rodinpos('M2',[],internal_var1),u)],[member(rodinpos('M2',grd1,internal_grd1),identifier(none,u),set_subtraction(none,identifier(none,'USER'),domain(none,identifier(none,location)))),member(rodinpos('M2',grd2,internal_element1),identifier(none,t),identifier(none,valid)),equal(rodinpos('M2',grd3,internal_grd3),identifier(none,r),function(none,identifier(none,room),[identifier(none,t)])),equal(rodinpos('M2',grd4,internal_grd4),identifier(none,u),function(none,identifier(none,holder),[identifier(none,t)]))],[],[assign(rodinpos('M2',act1,internal_act1),[identifier(none,location)],[union(none,identifier(none,location),set_extension(none,[couple(none,[identifier(none,u),identifier(none,r)])]))]),assign(rodinpos('M2',act4,internal_element3),[identifier(none,valid)],[set_subtraction(none,identifier(none,valid),set_extension(none,[identifier(none,t)]))])],[]),event(rodinpos('M2','Leave',evt1),'Leave',ordinary(none),['Leave'],[identifier(rodinpos('M2',[],internal_var2),r),identifier(rodinpos('M2',[],internal_var1),u)],[member(rodinpos('M2',grd1,internal_grd1),couple(none,[identifier(none,u),identifier(none,r)]),identifier(none,location))],[],[assign(rodinpos('M2',act1,internal_act1),[identifier(none,location)],[set_subtraction(none,identifier(none,location),set_extension(none,[couple(none,[identifier(none,u),identifier(none,r)])]))])],[]),event(rodinpos('M2','RescindToken',internal_evt5),'RescindToken',ordinary(none),[],[identifier(rodinpos('M2',[],internal_var1),t)],[member(rodinpos('M2',grd1,internal_grd1),identifier(none,t),identifier(none,valid))],[],[assign(rodinpos('M2',act1,internal_act1),[identifier(none,valid)],[set_subtraction(none,identifier(none,valid),set_extension(none,[identifier(none,t)]))])],[]),event(rodinpos('M2','RemAuth',evt0),'RemAuth',ordinary(none),['RemAuth'],[identifier(rodinpos('M2',[],internal_var2),a),identifier(rodinpos('M2',[],internal_var1),u)],[member(rodinpos('M2',grd1,'_d0nz0N1GEeGJ88a0BTYTjQ'),couple(none,[identifier(none,u),identifier(none,a)]),identifier(none,authorised)),implication(rodinpos('M2',grd2,'_GjNj4Dk9EeKnRYTKu_Ha7A'),member(none,identifier(none,u),domain(none,identifier(none,location))),not_member(none,couple(none,[function(none,identifier(none,location),[identifier(none,u)]),identifier(none,a)]),identifier(none,takeplace))),equal(rodinpos('M2',grd3,internal_element1),integer(none,1),integer(none,1))],[],[assign(rodinpos('M2',act1,internal_act1),[identifier(none,authorised)],[set_subtraction(none,identifier(none,authorised),set_extension(none,[couple(none,[identifier(none,u),identifier(none,a)])]))])],[])])]),event_b_model(none,'M1',[sees(none,['C1']),variables(none,[identifier(none,authorised),identifier(none,location)]),invariant(none,[member(rodinpos('M1',inv1,internal_inv1I),identifier(none,authorised),relations(none,identifier(none,'USER'),identifier(none,'ACTIVITY'))),member(rodinpos('M1',inv2,'_6VHFIDtEEeCV0aVqCvY8-w'),identifier(none,location),partial_function(none,identifier(none,'USER'),identifier(none,'ROOM'))),forall(rodinpos('M1',inv3,internal_inv3I),[identifier(none,u),identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,u),domain(none,identifier(none,location))),equal(none,function(none,identifier(none,location),[identifier(none,u)]),identifier(none,r))),subset(none,image(none,identifier(none,takeplace),set_extension(none,[identifier(none,r)])),image(none,identifier(none,authorised),set_extension(none,[identifier(none,u)])))))]),theorems(none,[]),events(none,[event(rodinpos('M1','INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('M1',act1,internal_act1),[identifier(none,authorised)],[empty_set(none)]),assign(rodinpos('M1',act2,'_d0lXkN1GEeGJ88a0BTYTjQ'),[identifier(none,location)],[empty_set(none)])],[]),event(rodinpos('M1','AddAuth',internal_evt2),'AddAuth',ordinary(none),[],[identifier(rodinpos('M1',[],internal_var2),a),identifier(rodinpos('M1',[],internal_var1),u)],[member(rodinpos('M1',grd1,internal_grd1),identifier(none,u),identifier(none,'USER')),member(rodinpos('M1',grd2,internal_grd2),identifier(none,a),identifier(none,'ACTIVITY'))],[],[assign(rodinpos('M1',act1,internal_act1),[identifier(none,authorised)],[union(none,identifier(none,authorised),set_extension(none,[couple(none,[identifier(none,u),identifier(none,a)])]))])],[]),event(rodinpos('M1','Enter',internal_evt3),'Enter',ordinary(none),[],[identifier(rodinpos('M1',[],internal_var2),r),identifier(rodinpos('M1',[],internal_var1),u)],[member(rodinpos('M1',grd1,internal_grd1),identifier(none,u),set_subtraction(none,identifier(none,'USER'),domain(none,identifier(none,location)))),member(rodinpos('M1',grd2,internal_grd2),identifier(none,r),identifier(none,'ROOM')),subset(rodinpos('M1',grd3,internal_grd3),image(none,identifier(none,takeplace),set_extension(none,[identifier(none,r)])),image(none,identifier(none,authorised),set_extension(none,[identifier(none,u)])))],[],[assign(rodinpos('M1',act1,internal_act1),[identifier(none,location)],[union(none,identifier(none,location),set_extension(none,[couple(none,[identifier(none,u),identifier(none,r)])]))])],[]),event(rodinpos('M1','Leave',evt1),'Leave',ordinary(none),[],[identifier(rodinpos('M1',[],internal_var2),r),identifier(rodinpos('M1',[],internal_var1),u)],[member(rodinpos('M1',grd1,internal_grd1),couple(none,[identifier(none,u),identifier(none,r)]),identifier(none,location))],[],[assign(rodinpos('M1',act1,internal_act1),[identifier(none,location)],[set_subtraction(none,identifier(none,location),set_extension(none,[couple(none,[identifier(none,u),identifier(none,r)])]))])],[]),event(rodinpos('M1','RemAuth',evt0),'RemAuth',ordinary(none),[],[identifier(rodinpos('M1',[],internal_var2),a),identifier(rodinpos('M1',[],internal_var1),u)],[member(rodinpos('M1',grd1,'_d0nz0N1GEeGJ88a0BTYTjQ'),couple(none,[identifier(none,u),identifier(none,a)]),identifier(none,authorised)),implication(rodinpos('M1',grd2,'_GjNj4Dk9EeKnRYTKu_Ha7A'),member(none,identifier(none,u),domain(none,identifier(none,location))),not_member(none,couple(none,[function(none,identifier(none,location),[identifier(none,u)]),identifier(none,a)]),identifier(none,takeplace)))],[],[assign(rodinpos('M1',act1,internal_act1),[identifier(none,authorised)],[set_subtraction(none,identifier(none,authorised),set_extension(none,[couple(none,[identifier(none,u),identifier(none,a)])]))])],[])])])],[event_b_context(none,'C1',[extends(none,[]),constants(none,[identifier(none,'ACTIVITY1'),identifier(none,'ACTIVITY2'),identifier(none,'ROOM1'),identifier(none,'ROOM2'),identifier(none,'USER1'),identifier(none,'USER2'),identifier(none,takeplace)]),axioms(none,[partition(rodinpos('C1',axmA,'_Lrh-sB1IEeKslfjbU8A_KA'),identifier(none,'ROOM'),[set_extension(none,[identifier(none,'ROOM1')]),set_extension(none,[identifier(none,'ROOM2')])]),partition(rodinpos('C1',axmB,'_Lrh-sR1IEeKslfjbU8A_KA'),identifier(none,'USER'),[set_extension(none,[identifier(none,'USER1')]),set_extension(none,[identifier(none,'USER2')])]),partition(rodinpos('C1',axmC,'_LrilwB1IEeKslfjbU8A_KA'),identifier(none,'ACTIVITY'),[set_extension(none,[identifier(none,'ACTIVITY1')]),set_extension(none,[identifier(none,'ACTIVITY2')])]),member(rodinpos('C1',axm1,'_pEob0jtEEeCV0aVqCvY8-w'),identifier(none,takeplace),relations(none,identifier(none,'ROOM'),identifier(none,'ACTIVITY'))),equal(rodinpos('C1',axm2,'_mYL8YNk0EeCS7biZYz2djg'),identifier(none,takeplace),cartesian_product(none,identifier(none,'ROOM'),identifier(none,'ACTIVITY')))]),theorems(none,[]),sets(none,[deferred_set(none,'ACTIVITY'),deferred_set(none,'ROOM'),deferred_set(none,'USER')])]),event_b_context(none,'C2',[extends(none,['C1']),constants(none,[identifier(none,holder),identifier(none,room)]),axioms(none,[member(rodinpos('C2',axm1,internal_axm1A),identifier(none,room),total_function(none,identifier(none,'TOKEN'),identifier(none,'ROOM'))),member(rodinpos('C2',axm2,internal_element1A),identifier(none,holder),total_function(none,identifier(none,'TOKEN'),identifier(none,'USER')))]),theorems(none,[]),sets(none,[deferred_set(none,'TOKEN')])])],[discharged('M2','INITIALISATION',inv5),discharged('M2','AddAuth',inv5),discharged('M2','GetValidToken',inv5),discharged('M2','Enter',inv5),discharged('M2','RescindToken',inv5),discharged('M1','INITIALISATION',inv2),discharged('M1','INITIALISATION',inv3),discharged('M1','AddAuth',inv3),discharged('M1','Enter',inv2),discharged('M1','Enter',inv3),discharged('M1','Leave',inv2),discharged('M1','Leave',inv3),discharged('M1','RemAuth',inv3)],_Error)).
2