1		package(load_event_b_project([event_b_model(none,'FiveWay_new',[sees(none,['Traffic_Context2']),variables(none,[identifier(none,light_dir)]),invariant(none,[member(rodinpos('FiveWay_new',inv1,'0'),identifier(none,light_dir),total_function(none,identifier(none,'DIRECTION'),identifier(none,'LIGHTS'))),forall(rodinpos('FiveWay_new',inv11,'*'),[identifier(none,d)],implication(none,conjunct(none,member(none,identifier(none,d),identifier(none,'DIRECTION')),conjunct(none,member(none,identifier(none,d),identifier(none,'DIRECTION')),member(none,function(none,identifier(none,light_dir),[identifier(none,d)]),set_extension(none,[identifier(none,'Green'),identifier(none,'Amber')])))),equal(none,image(none,identifier(none,light_dir),image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,d)]))),set_extension(none,[identifier(none,'Red')]))))]),theorems(none,[]),events(none,[event(rodinpos('FiveWay_new','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('FiveWay_new',act1,'\''),[identifier(none,light_dir)],[cartesian_product(none,identifier(none,'DIRECTION'),set_extension(none,[identifier(none,'Red')]))])],[]),event(rodinpos('FiveWay_new','ToRed','3'),'ToRed',ordinary(none),[],[identifier(rodinpos('FiveWay_new',[],'\''),dir)],[member(rodinpos('FiveWay_new',grd1,'('),identifier(none,dir),identifier(none,'DIRECTION')),equal(rodinpos('FiveWay_new',grd2,')'),function(none,identifier(none,light_dir),[identifier(none,dir)]),identifier(none,'Amber'))],[],[assign(rodinpos('FiveWay_new',act1,'*'),[identifier(none,light_dir)],[overwrite(none,identifier(none,light_dir),set_extension(none,[couple(none,[identifier(none,dir),identifier(none,'Red')])]))])],[]),event(rodinpos('FiveWay_new','ToGreen','4'),'ToGreen',ordinary(none),[],[identifier(rodinpos('FiveWay_new',[],'\''),dir)],[member(rodinpos('FiveWay_new',grd1,'('),identifier(none,dir),identifier(none,'DIRECTION')),equal(rodinpos('FiveWay_new',grd2,')'),function(none,identifier(none,light_dir),[identifier(none,dir)]),identifier(none,'Red')),equal(rodinpos('FiveWay_new',grd7,'/'),image(none,identifier(none,light_dir),image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,dir)]))),set_extension(none,[identifier(none,'Red')]))],[],[assign(rodinpos('FiveWay_new',act1,'*'),[identifier(none,light_dir)],[overwrite(none,identifier(none,light_dir),set_extension(none,[couple(none,[identifier(none,dir),identifier(none,'Green')])]))])],[]),event(rodinpos('FiveWay_new','ToAmber','5'),'ToAmber',ordinary(none),[],[identifier(rodinpos('FiveWay_new',[],'\''),dir)],[member(rodinpos('FiveWay_new',grd1,'('),identifier(none,dir),identifier(none,'DIRECTION')),equal(rodinpos('FiveWay_new',grd2,')'),image(none,identifier(none,light_dir),set_extension(none,[identifier(none,dir)])),set_extension(none,[identifier(none,'Green')]))],[],[assign(rodinpos('FiveWay_new',act1,'+'),[identifier(none,light_dir)],[overwrite(none,identifier(none,light_dir),set_extension(none,[couple(none,[identifier(none,dir),identifier(none,'Amber')])]))])],[])])])],[event_b_context(none,'Traffic_Context2',[extends(none,[]),constants(none,[identifier(none,'Amber'),identifier(none,'CONFLICT'),identifier(none,'EastWest'),identifier(none,'Green'),identifier(none,'North'),identifier(none,'NorthRight'),identifier(none,'Red'),identifier(none,'South'),identifier(none,'SouthRight')]),abstract_constants(none,[]),axioms(none,[partition(rodinpos('Traffic_Context2',axm1,'2'),identifier(none,'LIGHTS'),[set_extension(none,[identifier(none,'Red')]),set_extension(none,[identifier(none,'Green')]),set_extension(none,[identifier(none,'Amber')])]),finite(rodinpos('Traffic_Context2',axm2,'3'),identifier(none,'LIGHTS')),partition(rodinpos('Traffic_Context2',axm3,'4'),identifier(none,'DIRECTION'),[set_extension(none,[identifier(none,'North')]),set_extension(none,[identifier(none,'SouthRight')]),set_extension(none,[identifier(none,'NorthRight')]),set_extension(none,[identifier(none,'EastWest')]),set_extension(none,[identifier(none,'South')])]),finite(rodinpos('Traffic_Context2',axm4,'5'),identifier(none,'DIRECTION')),member(rodinpos('Traffic_Context2',axm5,'6'),identifier(none,'CONFLICT'),relations(none,identifier(none,'DIRECTION'),identifier(none,'DIRECTION'))),equal(rodinpos('Traffic_Context2',axm6,'8'),image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'EastWest')])),set_extension(none,[identifier(none,'North'),identifier(none,'South'),identifier(none,'SouthRight'),identifier(none,'NorthRight')])),equal(rodinpos('Traffic_Context2',axm7,'9'),image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'North')])),set_extension(none,[identifier(none,'EastWest'),identifier(none,'SouthRight')])),equal(rodinpos('Traffic_Context2',axm8,':'),image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'South')])),set_extension(none,[identifier(none,'EastWest'),identifier(none,'NorthRight')])),equal(rodinpos('Traffic_Context2',axm9,';'),image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'SouthRight')])),set_extension(none,[identifier(none,'EastWest'),identifier(none,'North')])),equal(rodinpos('Traffic_Context2',axm10,'='),image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,'NorthRight')])),set_extension(none,[identifier(none,'EastWest'),identifier(none,'South')])),forall(rodinpos('Traffic_Context2',axm11,'>'),[identifier(none,d1)],implication(none,conjunct(none,member(none,identifier(none,d1),identifier(none,'DIRECTION')),member(none,identifier(none,d1),identifier(none,'DIRECTION'))),not_subset(none,set_extension(none,[identifier(none,d1)]),image(none,identifier(none,'CONFLICT'),set_extension(none,[identifier(none,d1)])))))]),theorems(none,[]),sets(none,[deferred_set(none,'DIRECTION'),deferred_set(none,'LIGHTS')])])],[exporter_version(3),po('FiveWay_new','Well-definedness of Invariant',[invariant(inv11)],true),po('FiveWay_new','Invariant establishment',[event('INITIALISATION'),invariant(inv1)],true),po('FiveWay_new','Invariant establishment',[event('INITIALISATION'),invariant(inv11)],true),po('FiveWay_new','Well-definedness of Guard',[guard(grd2),event('ToRed')],true),po('FiveWay_new','Invariant preservation',[event('ToRed'),invariant(inv1)],true),po('FiveWay_new','Invariant preservation',[event('ToRed'),invariant(inv11)],true),po('FiveWay_new','Well-definedness of Guard',[guard(grd2),event('ToGreen')],true),po('FiveWay_new','Invariant preservation',[event('ToGreen'),invariant(inv1)],true),po('FiveWay_new','Invariant preservation',[event('ToGreen'),invariant(inv11)],false),po('FiveWay_new','Invariant preservation',[event('ToAmber'),invariant(inv1)],true),po('FiveWay_new','Invariant preservation',[event('ToAmber'),invariant(inv11)],true)],_Error)).
2