add second refinement of bridge example

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

Bridge/m2_lights_convergent_mch.eventb

+package(load_event_b_project([event_b_model(none,m2_lights_convergent,[sees(none,[context0]),refines(none,m1_bridge),variables(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,ml_pass),identifier(none,il_tl),identifier(none,ml_tl),identifier(none,il_pass)]),invariant(none,[member(rodinpos(m2_lights_convergent,inv1,'_EAPNgJE_EeWRGJ9JkSwucQ'),identifier(none,ml_tl),identifier(none,'LIGHT')),member(rodinpos(m2_lights_convergent,inv2,'_EAPNgZE_EeWRGJ9JkSwucQ'),identifier(none,il_tl),identifier(none,'LIGHT')),member(rodinpos(m2_lights_convergent,inv3,'_EAPNgpE_EeWRGJ9JkSwucQ'),identifier(none,ml_pass),bool_set(none)),member(rodinpos(m2_lights_convergent,inv4,'_EAPNg5E_EeWRGJ9JkSwucQ'),identifier(none,il_pass),bool_set(none)),implication(rodinpos(m2_lights_convergent,inv5,'_EAPNhJE_EeWRGJ9JkSwucQ'),equal(none,identifier(none,ml_tl),identifier(none,green)),conjunct(none,less(none,add(none,identifier(none,a),add(none,identifier(none,b),identifier(none,c))),identifier(none,d)),equal(none,identifier(none,c),integer(none,0)))),implication(rodinpos(m2_lights_convergent,inv6,'_EAPNhpE_EeWRGJ9JkSwucQ'),equal(none,identifier(none,il_tl),identifier(none,green)),conjunct(none,greater(none,identifier(none,b),integer(none,0)),equal(none,identifier(none,a),integer(none,0)))),disjunct(rodinpos(m2_lights_convergent,inv7,'_EAPNh5E_EeWRGJ9JkSwucQ'),equal(none,identifier(none,ml_tl),identifier(none,red)),equal(none,identifier(none,il_tl),identifier(none,red))),disjunct(rodinpos(m2_lights_convergent,inv8,'_EAPNiJE_EeWRGJ9JkSwucQ'),equal(none,identifier(none,ml_tl),identifier(none,green)),equal(none,identifier(none,ml_pass),boolean_true(none))),disjunct(rodinpos(m2_lights_convergent,inv9,'_EAPNiZE_EeWRGJ9JkSwucQ'),equal(none,identifier(none,il_tl),identifier(none,green)),equal(none,identifier(none,il_pass),boolean_true(none)))]),theorems(none,[implication(rodinpos(m2_lights_convergent,thm5,'_EAPNhZE_EeWRGJ9JkSwucQ'),disjunct(none,greater(none,identifier(none,c),integer(none,0)),equal(none,add(none,identifier(none,a),add(none,identifier(none,b),identifier(none,c))),identifier(none,d))),equal(none,identifier(none,ml_tl),identifier(none,red))),implication(rodinpos(m2_lights_convergent,inv10,'_EAP0kJE_EeWRGJ9JkSwucQ'),equal(none,identifier(none,b),integer(none,0)),equal(none,identifier(none,il_tl),identifier(none,red)))]),variant(none,card(none,range_restriction(none,set_extension(none,[couple(none,[integer(none,1),identifier(none,il_pass)]),couple(none,[integer(none,2),identifier(none,ml_pass)])]),set_extension(none,[boolean_true(none)])))),events(none,[event(rodinpos(m2_lights_convergent,'INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(m2_lights_convergent,act1,'_EAOmcJE_EeWRGJ9JkSwucQ'),[identifier(none,a),identifier(none,b),identifier(none,c)],[integer(none,0),integer(none,0),integer(none,0)]),assign(rodinpos(m2_lights_convergent,act2,'_EAOmcZE_EeWRGJ9JkSwucQ'),[identifier(none,ml_tl)],[identifier(none,red)]),assign(rodinpos(m2_lights_convergent,act3,'_EAOmcpE_EeWRGJ9JkSwucQ'),[identifier(none,il_tl)],[identifier(none,red)]),assign(rodinpos(m2_lights_convergent,act4,'_EAOmc5E_EeWRGJ9JkSwucQ'),[identifier(none,ml_pass)],[boolean_true(none)]),assign(rodinpos(m2_lights_convergent,act5,'_EAOmdJE_EeWRGJ9JkSwucQ'),[identifier(none,il_pass)],[boolean_true(none)])],[]),event(rodinpos(m2_lights_convergent,'ML_out','_EAP0kZE_EeWRGJ9JkSwucQ'),'ML_out',ordinary(none),['ML_out'],[],[equal(rodinpos(m2_lights_convergent,grd1,'_EAP0k5E_EeWRGJ9JkSwucQ'),identifier(none,ml_tl),identifier(none,green)),not_equal(rodinpos(m2_lights_convergent,grd2,'_EAP0lJE_EeWRGJ9JkSwucQ'),add(none,identifier(none,a),add(none,identifier(none,b),integer(none,1))),identifier(none,d))],[],[assign(rodinpos(m2_lights_convergent,act1,'_EAP0lZE_EeWRGJ9JkSwucQ'),[identifier(none,a)],[add(none,identifier(none,a),integer(none,1))]),assign(rodinpos(m2_lights_convergent,act2,'_EAP0lpE_EeWRGJ9JkSwucQ'),[identifier(none,ml_pass)],[boolean_true(none)])],[]),event(rodinpos(m2_lights_convergent,'ML_out_last','_EAP0l5E_EeWRGJ9JkSwucQ'),'ML_out_last',ordinary(none),['ML_out'],[],[equal(rodinpos(m2_lights_convergent,grd1,'_EAQboZE_EeWRGJ9JkSwucQ'),identifier(none,ml_tl),identifier(none,green)),equal(rodinpos(m2_lights_convergent,grd2,'_EAQbopE_EeWRGJ9JkSwucQ'),add(none,identifier(none,a),add(none,identifier(none,b),integer(none,1))),identifier(none,d))],[],[assign(rodinpos(m2_lights_convergent,act1,'_EAQbo5E_EeWRGJ9JkSwucQ'),[identifier(none,a)],[add(none,identifier(none,a),integer(none,1))]),assign(rodinpos(m2_lights_convergent,act2,'_EAQbpJE_EeWRGJ9JkSwucQ'),[identifier(none,ml_pass)],[boolean_true(none)]),assign(rodinpos(m2_lights_convergent,act3,'_EAQbpZE_EeWRGJ9JkSwucQ'),[identifier(none,ml_tl)],[identifier(none,red)])],[]),event(rodinpos(m2_lights_convergent,'ML_in','_EAQbppE_EeWRGJ9JkSwucQ'),'ML_in',ordinary(none),['ML_in'],[],[greater(rodinpos(m2_lights_convergent,grd1,internal_grd1),identifier(none,c),integer(none,0))],[],[assign(rodinpos(m2_lights_convergent,act1,internal_act1),[identifier(none,c)],[minus(none,identifier(none,c),integer(none,1))])],[]),event(rodinpos(m2_lights_convergent,'IL_in','_EAQbqJE_EeWRGJ9JkSwucQ'),'IL_in',ordinary(none),['IL_in'],[],[greater(rodinpos(m2_lights_convergent,grd1,internal_grd1),identifier(none,a),integer(none,0))],[],[assign(rodinpos(m2_lights_convergent,act1,internal_act1),[identifier(none,a)],[minus(none,identifier(none,a),integer(none,1))]),assign(rodinpos(m2_lights_convergent,act2,'_QsLTsFBaEeOH8cnegPmrEg'),[identifier(none,b)],[add(none,identifier(none,b),integer(none,1))])],[]),event(rodinpos(m2_lights_convergent,'IL_out','_EAQbqpE_EeWRGJ9JkSwucQ'),'IL_out',ordinary(none),['IL_out'],[],[equal(rodinpos(m2_lights_convergent,grd1,'_EARCsZE_EeWRGJ9JkSwucQ'),identifier(none,il_tl),identifier(none,green)),not_equal(rodinpos(m2_lights_convergent,grd2,'_EARCspE_EeWRGJ9JkSwucQ'),identifier(none,b),integer(none,1))],[],[assign(rodinpos(m2_lights_convergent,act1,'_EARCs5E_EeWRGJ9JkSwucQ'),[identifier(none,b)],[minus(none,identifier(none,b),integer(none,1))]),assign(rodinpos(m2_lights_convergent,act2,'_EARCtJE_EeWRGJ9JkSwucQ'),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))]),assign(rodinpos(m2_lights_convergent,act3,'_EARCtZE_EeWRGJ9JkSwucQ'),[identifier(none,il_pass)],[boolean_true(none)])],[]),event(rodinpos(m2_lights_convergent,'IL_out_last','_EARCtpE_EeWRGJ9JkSwucQ'),'IL_out_last',ordinary(none),['IL_out'],[],[equal(rodinpos(m2_lights_convergent,grd1,'_EARCuJE_EeWRGJ9JkSwucQ'),identifier(none,il_tl),identifier(none,green)),equal(rodinpos(m2_lights_convergent,grd2,'_EARCuZE_EeWRGJ9JkSwucQ'),identifier(none,b),integer(none,1))],[],[assign(rodinpos(m2_lights_convergent,act1,'_EARCupE_EeWRGJ9JkSwucQ'),[identifier(none,b)],[minus(none,identifier(none,b),integer(none,1))]),assign(rodinpos(m2_lights_convergent,act2,'_EARpwJE_EeWRGJ9JkSwucQ'),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))]),assign(rodinpos(m2_lights_convergent,act3,'_EARpwZE_EeWRGJ9JkSwucQ'),[identifier(none,il_pass)],[boolean_true(none)]),assign(rodinpos(m2_lights_convergent,act4,'_EARpwpE_EeWRGJ9JkSwucQ'),[identifier(none,il_tl)],[identifier(none,red)])],[]),event(rodinpos(m2_lights_convergent,'ML_tl_green','_EARpw5E_EeWRGJ9JkSwucQ'),'ML_tl_green',convergent(none),[],[],[equal(rodinpos(m2_lights_convergent,grd1,'_EARpxJE_EeWRGJ9JkSwucQ'),identifier(none,ml_tl),identifier(none,red)),less(rodinpos(m2_lights_convergent,grd2,'_EARpxZE_EeWRGJ9JkSwucQ'),add(none,identifier(none,a),identifier(none,b)),identifier(none,d)),equal(rodinpos(m2_lights_convergent,grd3,'_EARpxpE_EeWRGJ9JkSwucQ'),identifier(none,c),integer(none,0)),equal(rodinpos(m2_lights_convergent,grd4,'_EARpx5E_EeWRGJ9JkSwucQ'),identifier(none,il_pass),boolean_true(none))],[],[assign(rodinpos(m2_lights_convergent,act1,'_EARpyJE_EeWRGJ9JkSwucQ'),[identifier(none,ml_tl)],[identifier(none,green)]),assign(rodinpos(m2_lights_convergent,act2,'_EARpyZE_EeWRGJ9JkSwucQ'),[identifier(none,il_tl)],[identifier(none,red)]),assign(rodinpos(m2_lights_convergent,act3,'_EARpypE_EeWRGJ9JkSwucQ'),[identifier(none,ml_pass)],[boolean_false(none)])],[]),event(rodinpos(m2_lights_convergent,'IL_tl_green','_EASQ0JE_EeWRGJ9JkSwucQ'),'IL_tl_green',convergent(none),[],[],[equal(rodinpos(m2_lights_convergent,grd1,'_EASQ0ZE_EeWRGJ9JkSwucQ'),identifier(none,il_tl),identifier(none,red)),equal(rodinpos(m2_lights_convergent,grd2,'_EASQ0pE_EeWRGJ9JkSwucQ'),identifier(none,a),integer(none,0)),equal(rodinpos(m2_lights_convergent,grd3,'_EASQ05E_EeWRGJ9JkSwucQ'),identifier(none,ml_pass),boolean_true(none)),greater(rodinpos(m2_lights_convergent,grd4,'_EASQ1JE_EeWRGJ9JkSwucQ'),identifier(none,b),integer(none,0))],[],[assign(rodinpos(m2_lights_convergent,act1,'_EASQ1ZE_EeWRGJ9JkSwucQ'),[identifier(none,il_tl)],[identifier(none,green)]),assign(rodinpos(m2_lights_convergent,act2,'_EASQ1pE_EeWRGJ9JkSwucQ'),[identifier(none,ml_tl)],[identifier(none,red)]),assign(rodinpos(m2_lights_convergent,act3,'_EASQ15E_EeWRGJ9JkSwucQ'),[identifier(none,il_pass)],[boolean_false(none)])],[])])]),event_b_model(none,m1_bridge,[sees(none,[context0]),refines(none,m0_island_bridge),variables(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),invariant(none,[member(rodinpos(m1_bridge,inv1,internal_inv1I),identifier(none,a),natural_set(none)),member(rodinpos(m1_bridge,inv2,internal_inv2I),identifier(none,b),natural_set(none)),member(rodinpos(m1_bridge,inv3,internal_inv3I),identifier(none,c),natural_set(none)),equal(rodinpos(m1_bridge,inv4,internal_inv4I),add(none,identifier(none,a),add(none,identifier(none,b),identifier(none,c))),identifier(none,n)),disjunct(rodinpos(m1_bridge,inv5,internal_inv5I),equal(none,identifier(none,a),integer(none,0)),equal(none,identifier(none,c),integer(none,0)))]),theorems(none,[]),variant(none,add(none,multiplication(none,integer(none,3),identifier(none,a)),identifier(none,b))),events(none,[event(rodinpos(m1_bridge,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,a),identifier(none,b),identifier(none,c)],[integer(none,0),integer(none,0),integer(none,0)])],[]),event(rodinpos(m1_bridge,'ML_out',internal_evt2),'ML_out',ordinary(none),['ML_out'],[],[less(rodinpos(m1_bridge,grd1,internal_grd1),add(none,identifier(none,a),add(none,identifier(none,b),identifier(none,c))),identifier(none,d)),equal(rodinpos(m1_bridge,grd2,internal_grd2),identifier(none,c),integer(none,0))],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,a)],[add(none,identifier(none,a),integer(none,1))])],[]),event(rodinpos(m1_bridge,'ML_in',internal_evt3),'ML_in',ordinary(none),['ML_in'],[],[greater(rodinpos(m1_bridge,grd1,internal_grd1),identifier(none,c),integer(none,0))],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,c)],[minus(none,identifier(none,c),integer(none,1))])],[]),event(rodinpos(m1_bridge,'IL_in',internal_evt4),'IL_in',convergent(none),[],[],[greater(rodinpos(m1_bridge,grd1,internal_grd1),identifier(none,a),integer(none,0))],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,a)],[minus(none,identifier(none,a),integer(none,1))]),assign(rodinpos(m1_bridge,act2,'_QsLTsFBaEeOH8cnegPmrEg'),[identifier(none,b)],[add(none,identifier(none,b),integer(none,1))])],[]),event(rodinpos(m1_bridge,'IL_out',internal_evt5),'IL_out',convergent(none),[],[],[greater(rodinpos(m1_bridge,grd1,internal_grd1),identifier(none,b),integer(none,0)),equal(rodinpos(m1_bridge,grd2,'_gSBLsLV0EeaoRIOcax8gTQ'),identifier(none,a),integer(none,0))],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,b)],[minus(none,identifier(none,b),integer(none,1))]),assign(rodinpos(m1_bridge,act2,internal_act3),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))])],[])])]),event_b_model(none,m0_island_bridge,[sees(none,[context0]),variables(none,[identifier(none,n)]),invariant(none,[member(rodinpos(m0_island_bridge,inv1,internal_inv1I),identifier(none,n),natural_set(none)),less_equal(rodinpos(m0_island_bridge,inv2,internal_inv3I),identifier(none,n),identifier(none,d)),disjunct(rodinpos(m0_island_bridge,'DLF','_MLohYJHeEeWRGJ9JkSwucQ'),less(none,identifier(none,n),identifier(none,d)),greater(none,identifier(none,n),integer(none,0)))]),theorems(none,[]),events(none,[event(rodinpos(m0_island_bridge,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[integer(none,0)])],[]),event(rodinpos(m0_island_bridge,'ML_out',internal_evt2),'ML_out',ordinary(none),[],[],[less(rodinpos(m0_island_bridge,grd1,internal_grd1),identifier(none,n),identifier(none,d))],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[add(none,identifier(none,n),integer(none,1))])],[]),event(rodinpos(m0_island_bridge,'ML_in',internal_evt3),'ML_in',ordinary(none),[],[],[greater(rodinpos(m0_island_bridge,grd1,internal_grd1),identifier(none,n),integer(none,0))],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[minus(none,identifier(none,n),integer(none,1))])],[])])])],[event_b_context(none,context0,[extends(none,[]),constants(none,[identifier(none,d),identifier(none,red),identifier(none,green)]),abstract_constants(none,[]),axioms(none,[member(rodinpos(context0,axm1,internal_axm1A),identifier(none,d),natural_set(none)),equal(rodinpos(context0,axm2,internal_axm2A),identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(rodinpos(context0,axm3,internal_axm3A),identifier(none,green),identifier(none,red)),greater(rodinpos(context0,axm4,'_5LvooLr2EeaoOKVlIjG7fA'),identifier(none,d),integer(none,0))]),theorems(none,[]),sets(none,[deferred_set(none,'LIGHT')])])],[exporter_version(3),po(m2_lights_convergent,'Theorem',[invariant(thm5)],true),po(m2_lights_convergent,'Theorem',[invariant(inv10)],true),po(m2_lights_convergent,'Well-definedness of variant',[variant(vrn)],true),po(m2_lights_convergent,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],true),po(m2_lights_convergent,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv6)],true),po(m2_lights_convergent,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv7)],true),po(m2_lights_convergent,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv8)],true),po(m2_lights_convergent,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv9)],true),po(m2_lights_convergent,'Invariant  preservation',[event('ML_out'),event('ML_out'),invariant(inv5)],true),po(m2_lights_convergent,'Invariant  preservation',[event('ML_out'),event('ML_out'),invariant(inv6)],true),po(m2_lights_convergent,'Invariant  preservation',[event('ML_out'),event('ML_out'),invariant(inv8)],true),po(m2_lights_convergent,'Guard strengthening (split)',[event('ML_out'),guard(grd1),event('ML_out'),event('ML_out')],true),po(m2_lights_convergent,'Guard strengthening (split)',[event('ML_out'),guard(grd2),event('ML_out'),event('ML_out')],true),po(m2_lights_convergent,'Invariant  preservation',[event('ML_out'),event('ML_out_last'),invariant(inv5)],true),po(m2_lights_convergent,'Invariant  preservation',[event('ML_out'),event('ML_out_last'),invariant(inv6)],true),po(m2_lights_convergent,'Invariant  preservation',[event('ML_out'),event('ML_out_last'),invariant(inv7)],true),po(m2_lights_convergent,'Invariant  preservation',[event('ML_out'),event('ML_out_last'),invariant(inv8)],true),po(m2_lights_convergent,'Guard strengthening (split)',[event('ML_out'),guard(grd1),event('ML_out'),event('ML_out_last')],true),po(m2_lights_convergent,'Guard strengthening (split)',[event('ML_out'),guard(grd2),event('ML_out'),event('ML_out_last')],true),po(m2_lights_convergent,'Invariant  preservation',[event('ML_in'),event('ML_in'),invariant(inv5)],true),po(m2_lights_convergent,'Invariant  preservation',[event('IL_in'),event('IL_in'),invariant(inv5)],true),po(m2_lights_convergent,'Invariant  preservation',[event('IL_in'),event('IL_in'),invariant(inv6)],true),po(m2_lights_convergent,'Invariant  preservation',[event('IL_out'),event('IL_out'),invariant(inv5)],true),po(m2_lights_convergent,'Invariant  preservation',[event('IL_out'),event('IL_out'),invariant(inv6)],true),po(m2_lights_convergent,'Invariant  preservation',[event('IL_out'),event('IL_out'),invariant(inv9)],true),po(m2_lights_convergent,'Guard strengthening (split)',[event('IL_out'),guard(grd1),event('IL_out'),event('IL_out')],true),po(m2_lights_convergent,'Guard strengthening (split)',[event('IL_out'),guard(grd2),event('IL_out'),event('IL_out')],true),po(m2_lights_convergent,'Invariant  preservation',[event('IL_out'),event('IL_out_last'),invariant(inv5)],true),po(m2_lights_convergent,'Invariant  preservation',[event('IL_out'),event('IL_out_last'),invariant(inv6)],true),po(m2_lights_convergent,'Invariant  preservation',[event('IL_out'),event('IL_out_last'),invariant(inv7)],true),po(m2_lights_convergent,'Invariant  preservation',[event('IL_out'),event('IL_out_last'),invariant(inv9)],true),po(m2_lights_convergent,'Guard strengthening (split)',[event('IL_out'),guard(grd1),event('IL_out'),event('IL_out_last')],true),po(m2_lights_convergent,'Guard strengthening (split)',[event('IL_out'),guard(grd2),event('IL_out'),event('IL_out_last')],true),po(m2_lights_convergent,'Invariant  preservation',[event('ML_tl_green'),invariant(inv5)],true),po(m2_lights_convergent,'Invariant  preservation',[event('ML_tl_green'),invariant(inv6)],true),po(m2_lights_convergent,'Invariant  preservation',[event('ML_tl_green'),invariant(inv7)],true),po(m2_lights_convergent,'Invariant  preservation',[event('ML_tl_green'),invariant(inv8)],true),po(m2_lights_convergent,'Invariant  preservation',[event('ML_tl_green'),invariant(inv9)],true),po(m2_lights_convergent,'Natural number variant of event',[event('ML_tl_green'),variant(vrn)],true),po(m2_lights_convergent,'Variant of event',[event('ML_tl_green'),variant(vrn)],true),po(m2_lights_convergent,'Invariant  preservation',[event('IL_tl_green'),invariant(inv5)],true),po(m2_lights_convergent,'Invariant  preservation',[event('IL_tl_green'),invariant(inv6)],true),po(m2_lights_convergent,'Invariant  preservation',[event('IL_tl_green'),invariant(inv7)],true),po(m2_lights_convergent,'Invariant  preservation',[event('IL_tl_green'),invariant(inv8)],true),po(m2_lights_convergent,'Invariant  preservation',[event('IL_tl_green'),invariant(inv9)],true),po(m2_lights_convergent,'Natural number variant of event',[event('IL_tl_green'),variant(vrn)],true),po(m2_lights_convergent,'Variant of event',[event('IL_tl_green'),variant(vrn)],true),po(m1_bridge,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po(m1_bridge,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po(m1_bridge,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po(m1_bridge,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4)],true),po(m1_bridge,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],true),po(m1_bridge,'Invariant  preservation',[event('ML_out'),event('ML_out'),invariant(inv1)],true),po(m1_bridge,'Invariant  preservation',[event('ML_out'),event('ML_out'),invariant(inv4)],true),po(m1_bridge,'Invariant  preservation',[event('ML_out'),event('ML_out'),invariant(inv5)],true),po(m1_bridge,'Guard strengthening (split)',[event('ML_out'),guard(grd1),event('ML_out'),event('ML_out')],true),po(m1_bridge,'Invariant  preservation',[event('ML_in'),event('ML_in'),invariant(inv3)],true),po(m1_bridge,'Invariant  preservation',[event('ML_in'),event('ML_in'),invariant(inv4)],true),po(m1_bridge,'Invariant  preservation',[event('ML_in'),event('ML_in'),invariant(inv5)],true),po(m1_bridge,'Guard strengthening (split)',[event('ML_in'),guard(grd1),event('ML_in'),event('ML_in')],true),po(m1_bridge,'Invariant  preservation',[event('IL_in'),invariant(inv1)],true),po(m1_bridge,'Invariant  preservation',[event('IL_in'),invariant(inv2)],true),po(m1_bridge,'Invariant  preservation',[event('IL_in'),invariant(inv4)],true),po(m1_bridge,'Invariant  preservation',[event('IL_in'),invariant(inv5)],true),po(m1_bridge,'Natural number variant of event',[event('IL_in'),variant(vrn)],true),po(m1_bridge,'Variant of event',[event('IL_in'),variant(vrn)],true),po(m1_bridge,'Invariant  preservation',[event('IL_out'),invariant(inv2)],true),po(m1_bridge,'Invariant  preservation',[event('IL_out'),invariant(inv3)],true),po(m1_bridge,'Invariant  preservation',[event('IL_out'),invariant(inv4)],true),po(m1_bridge,'Invariant  preservation',[event('IL_out'),invariant(inv5)],true),po(m1_bridge,'Natural number variant of event',[event('IL_out'),variant(vrn)],true),po(m1_bridge,'Variant of event',[event('IL_out'),variant(vrn)],true),po(m0_island_bridge,'Invariant  establishment',[event('INITIALISATION'),invariant(inv1)],true),po(m0_island_bridge,'Invariant  establishment',[event('INITIALISATION'),invariant(inv2)],true),po(m0_island_bridge,'Invariant  establishment',[event('INITIALISATION'),invariant('DLF')],true),po(m0_island_bridge,'Invariant  preservation',[event('ML_out'),invariant(inv1)],true),po(m0_island_bridge,'Invariant  preservation',[event('ML_out'),invariant(inv2)],true),po(m0_island_bridge,'Invariant  preservation',[event('ML_out'),invariant('DLF')],true),po(m0_island_bridge,'Invariant  preservation',[event('ML_in'),invariant(inv1)],true),po(m0_island_bridge,'Invariant  preservation',[event('ML_in'),invariant(inv2)],true),po(m0_island_bridge,'Invariant  preservation',[event('ML_in'),invariant('DLF')],true)],_Error)).
+

Bridge/m2_lights_wrong_v2_mch.eventb

+package(load_event_b_project([event_b_model(none,m2_lights_wrong_v2,[sees(none,[context0]),refines(none,m1_bridge),variables(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,il_tl),identifier(none,ml_tl)]),invariant(none,[member(rodinpos(m2_lights_wrong_v2,inv1,'_flq6hFA5EeOH8cnegPmrEg'),identifier(none,ml_tl),identifier(none,'LIGHT')),member(rodinpos(m2_lights_wrong_v2,inv2,'_flq6hVA5EeOH8cnegPmrEg'),identifier(none,il_tl),identifier(none,'LIGHT')),disjunct(rodinpos(m2_lights_wrong_v2,inv2_5,'_flrhkFA5EeOH8cnegPmrEg'),equal(none,identifier(none,ml_tl),identifier(none,red)),equal(none,identifier(none,il_tl),identifier(none,red))),implication(rodinpos(m2_lights_wrong_v2,inv5,'_flrhklA5EeOH8cnegPmrEg'),equal(none,identifier(none,ml_tl),identifier(none,green)),conjunct(none,less(none,add(none,identifier(none,a),add(none,identifier(none,b),identifier(none,c))),identifier(none,d)),equal(none,identifier(none,c),integer(none,0)))),implication(rodinpos(m2_lights_wrong_v2,inv6,'_XzT68IxTEeWlXPUxOQKV8A'),equal(none,identifier(none,il_tl),identifier(none,green)),conjunct(none,greater(none,identifier(none,b),integer(none,0)),equal(none,identifier(none,a),integer(none,0))))]),theorems(none,[implication(rodinpos(m2_lights_wrong_v2,thm1,'_flrhkVA5EeOH8cnegPmrEg'),equal(none,identifier(none,il_tl),identifier(none,green)),equal(none,identifier(none,ml_tl),identifier(none,red)))]),events(none,[event(rodinpos(m2_lights_wrong_v2,'INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(m2_lights_wrong_v2,act1,'_flqTcVA5EeOH8cnegPmrEg'),[identifier(none,a),identifier(none,b),identifier(none,c)],[integer(none,0),integer(none,0),integer(none,0)]),assign(rodinpos(m2_lights_wrong_v2,act2,'_flqTclA5EeOH8cnegPmrEg'),[identifier(none,ml_tl)],[identifier(none,red)]),assign(rodinpos(m2_lights_wrong_v2,act3,'_flqTc1A5EeOH8cnegPmrEg'),[identifier(none,il_tl)],[identifier(none,red)])],[]),event(rodinpos(m2_lights_wrong_v2,'ML_out','_flrhk1A5EeOH8cnegPmrEg'),'ML_out',ordinary(none),['ML_out'],[],[equal(rodinpos(m2_lights_wrong_v2,grd1,'_flrhlVA5EeOH8cnegPmrEg'),identifier(none,ml_tl),identifier(none,green))],[],[assign(rodinpos(m2_lights_wrong_v2,act1,'_flsIoFA5EeOH8cnegPmrEg'),[identifier(none,a)],[add(none,identifier(none,a),integer(none,1))])],[]),event(rodinpos(m2_lights_wrong_v2,'ML_in','_flsIoVA5EeOH8cnegPmrEg'),'ML_in',ordinary(none),['ML_in'],[],[greater(rodinpos(m2_lights_wrong_v2,grd1,internal_grd1),identifier(none,c),integer(none,0))],[],[assign(rodinpos(m2_lights_wrong_v2,act1,internal_act1),[identifier(none,c)],[minus(none,identifier(none,c),integer(none,1))])],[]),event(rodinpos(m2_lights_wrong_v2,'IL_in','_flsIpVA5EeOH8cnegPmrEg'),'IL_in',ordinary(none),['IL_in'],[],[greater(rodinpos(m2_lights_wrong_v2,grd1,internal_grd1),identifier(none,a),integer(none,0))],[],[assign(rodinpos(m2_lights_wrong_v2,act1,internal_act1),[identifier(none,a)],[minus(none,identifier(none,a),integer(none,1))]),assign(rodinpos(m2_lights_wrong_v2,act2,'_QsLTsFBaEeOH8cnegPmrEg'),[identifier(none,b)],[add(none,identifier(none,b),integer(none,1))])],[]),event(rodinpos(m2_lights_wrong_v2,'IL_out','_flsvtFA5EeOH8cnegPmrEg'),'IL_out',ordinary(none),['IL_out'],[],[equal(rodinpos(m2_lights_wrong_v2,grd1,'_flsIo1A5EeOH8cnegPmrEg'),identifier(none,il_tl),identifier(none,green))],[],[assign(rodinpos(m2_lights_wrong_v2,act1,'_flsIpFA5EeOH8cnegPmrEg'),[identifier(none,b)],[minus(none,identifier(none,b),integer(none,1))]),assign(rodinpos(m2_lights_wrong_v2,act2,'_flsvs1A5EeOH8cnegPmrEg'),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))])],[]),event(rodinpos(m2_lights_wrong_v2,'ML_tl_green','_fltWwlA5EeOH8cnegPmrEg'),'ML_tl_green',ordinary(none),[],[],[equal(rodinpos(m2_lights_wrong_v2,grd1,'_flsvsVA5EeOH8cnegPmrEg'),identifier(none,ml_tl),identifier(none,red)),less(rodinpos(m2_lights_wrong_v2,grd2,'_fltWxFA5EeOH8cnegPmrEg'),add(none,identifier(none,a),identifier(none,b)),identifier(none,d)),equal(rodinpos(m2_lights_wrong_v2,grd3,'_fltWxVA5EeOH8cnegPmrEg'),identifier(none,c),integer(none,0))],[],[assign(rodinpos(m2_lights_wrong_v2,act1,'_flsvslA5EeOH8cnegPmrEg'),[identifier(none,ml_tl)],[identifier(none,green)]),assign(rodinpos(m2_lights_wrong_v2,act2,'_fltWwVA5EeOH8cnegPmrEg'),[identifier(none,il_tl)],[identifier(none,red)])],[]),event(rodinpos(m2_lights_wrong_v2,'IL_tl_green','_flt90lA5EeOH8cnegPmrEg'),'IL_tl_green',ordinary(none),[],[],[equal(rodinpos(m2_lights_wrong_v2,grd1,'_flsvtlA5EeOH8cnegPmrEg'),identifier(none,il_tl),identifier(none,red)),equal(rodinpos(m2_lights_wrong_v2,grd2,'_flt91FA5EeOH8cnegPmrEg'),identifier(none,a),integer(none,0)),greater(rodinpos(m2_lights_wrong_v2,grd4,'_flt91VA5EeOH8cnegPmrEg'),identifier(none,b),integer(none,0))],[],[assign(rodinpos(m2_lights_wrong_v2,act1,'_fltWwFA5EeOH8cnegPmrEg'),[identifier(none,il_tl)],[identifier(none,green)]),assign(rodinpos(m2_lights_wrong_v2,act2,'_flt90VA5EeOH8cnegPmrEg'),[identifier(none,ml_tl)],[identifier(none,red)])],[])])]),event_b_model(none,m1_bridge,[sees(none,[context0]),refines(none,m0_island_bridge),variables(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),invariant(none,[member(rodinpos(m1_bridge,inv1,internal_inv1I),identifier(none,a),natural_set(none)),member(rodinpos(m1_bridge,inv2,internal_inv2I),identifier(none,b),natural_set(none)),member(rodinpos(m1_bridge,inv3,internal_inv3I),identifier(none,c),natural_set(none)),equal(rodinpos(m1_bridge,inv4,internal_inv4I),add(none,identifier(none,a),add(none,identifier(none,b),identifier(none,c))),identifier(none,n)),disjunct(rodinpos(m1_bridge,inv5,internal_inv5I),equal(none,identifier(none,a),integer(none,0)),equal(none,identifier(none,c),integer(none,0)))]),theorems(none,[]),variant(none,add(none,multiplication(none,integer(none,3),identifier(none,a)),identifier(none,b))),events(none,[event(rodinpos(m1_bridge,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,a),identifier(none,b),identifier(none,c)],[integer(none,0),integer(none,0),integer(none,0)])],[]),event(rodinpos(m1_bridge,'ML_out',internal_evt2),'ML_out',ordinary(none),['ML_out'],[],[less(rodinpos(m1_bridge,grd1,internal_grd1),add(none,identifier(none,a),add(none,identifier(none,b),identifier(none,c))),identifier(none,d)),equal(rodinpos(m1_bridge,grd2,internal_grd2),identifier(none,c),integer(none,0))],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,a)],[add(none,identifier(none,a),integer(none,1))])],[]),event(rodinpos(m1_bridge,'ML_in',internal_evt3),'ML_in',ordinary(none),['ML_in'],[],[greater(rodinpos(m1_bridge,grd1,internal_grd1),identifier(none,c),integer(none,0))],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,c)],[minus(none,identifier(none,c),integer(none,1))])],[]),event(rodinpos(m1_bridge,'IL_in',internal_evt4),'IL_in',convergent(none),[],[],[greater(rodinpos(m1_bridge,grd1,internal_grd1),identifier(none,a),integer(none,0))],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,a)],[minus(none,identifier(none,a),integer(none,1))]),assign(rodinpos(m1_bridge,act2,'_QsLTsFBaEeOH8cnegPmrEg'),[identifier(none,b)],[add(none,identifier(none,b),integer(none,1))])],[]),event(rodinpos(m1_bridge,'IL_out',internal_evt5),'IL_out',convergent(none),[],[],[greater(rodinpos(m1_bridge,grd1,internal_grd1),identifier(none,b),integer(none,0)),equal(rodinpos(m1_bridge,grd2,'_gSBLsLV0EeaoRIOcax8gTQ'),identifier(none,a),integer(none,0))],[],[assign(rodinpos(m1_bridge,act1,internal_act1),[identifier(none,b)],[minus(none,identifier(none,b),integer(none,1))]),assign(rodinpos(m1_bridge,act2,internal_act3),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))])],[])])]),event_b_model(none,m0_island_bridge,[sees(none,[context0]),variables(none,[identifier(none,n)]),invariant(none,[member(rodinpos(m0_island_bridge,inv1,internal_inv1I),identifier(none,n),natural_set(none)),less_equal(rodinpos(m0_island_bridge,inv2,internal_inv3I),identifier(none,n),identifier(none,d)),disjunct(rodinpos(m0_island_bridge,'DLF','_MLohYJHeEeWRGJ9JkSwucQ'),less(none,identifier(none,n),identifier(none,d)),greater(none,identifier(none,n),integer(none,0)))]),theorems(none,[]),events(none,[event(rodinpos(m0_island_bridge,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[integer(none,0)])],[]),event(rodinpos(m0_island_bridge,'ML_out',internal_evt2),'ML_out',ordinary(none),[],[],[less(rodinpos(m0_island_bridge,grd1,internal_grd1),identifier(none,n),identifier(none,d))],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[add(none,identifier(none,n),integer(none,1))])],[]),event(rodinpos(m0_island_bridge,'ML_in',internal_evt3),'ML_in',ordinary(none),[],[],[greater(rodinpos(m0_island_bridge,grd1,internal_grd1),identifier(none,n),integer(none,0))],[],[assign(rodinpos(m0_island_bridge,act1,internal_act1),[identifier(none,n)],[minus(none,identifier(none,n),integer(none,1))])],[])])])],[event_b_context(none,context0,[extends(none,[]),constants(none,[identifier(none,d),identifier(none,red),identifier(none,green)]),abstract_constants(none,[]),axioms(none,[member(rodinpos(context0,axm1,internal_axm1A),identifier(none,d),natural_set(none)),equal(rodinpos(context0,axm2,internal_axm2A),identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(rodinpos(context0,axm3,internal_axm3A),identifier(none,green),identifier(none,red)),greater(rodinpos(context0,axm4,'_5LvooLr2EeaoOKVlIjG7fA'),identifier(none,d),integer(none,0))]),theorems(none,[]),sets(none,[deferred_set(none,'LIGHT')])])],[exporter_version(3),po(m2_lights_wrong_v2,'Theorem',[invariant(thm1)],true),po(m2_lights_wrong_v2,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2_5)],true),po(m2_lights_wrong_v2,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],true),po(m2_lights_wrong_v2,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv6)],true),po(m2_lights_wrong_v2,'Invariant  preservation',[event('ML_out'),event('ML_out'),invariant(inv5)],false),po(m2_lights_wrong_v2,'Invariant  preservation',[event('ML_out'),event('ML_out'),invariant(inv6)],true),po(m2_lights_wrong_v2,'Guard strengthening (split)',[event('ML_out'),guard(grd1),event('ML_out'),event('ML_out')],true),po(m2_lights_wrong_v2,'Guard strengthening (split)',[event('ML_out'),guard(grd2),event('ML_out'),event('ML_out')],true),po(m2_lights_wrong_v2,'Invariant  preservation',[event('ML_in'),event('ML_in'),invariant(inv5)],true),po(m2_lights_wrong_v2,'Invariant  preservation',[event('IL_in'),event('IL_in'),invariant(inv5)],true),po(m2_lights_wrong_v2,'Invariant  preservation',[event('IL_in'),event('IL_in'),invariant(inv6)],true),po(m2_lights_wrong_v2,'Invariant  preservation',[event('IL_out'),event('IL_out'),invariant(inv5)],true),po(m2_lights_wrong_v2,'Invariant  preservation',[event('IL_out'),event('IL_out'),invariant(inv6)],false),po(m2_lights_wrong_v2,'Guard strengthening (split)',[event('IL_out'),guard(grd1),event('IL_out'),event('IL_out')],true),po(m2_lights_wrong_v2,'Guard strengthening (split)',[event('IL_out'),guard(grd2),event('IL_out'),event('IL_out')],true),po(m2_lights_wrong_v2,'Invariant  preservation',[event('ML_tl_green'),invariant(inv2_5)],true),po(m2_lights_wrong_v2,'Invariant  preservation',[event('ML_tl_green'),invariant(inv5)],true),po(m2_lights_wrong_v2,'Invariant  preservation',[event('ML_tl_green'),invariant(inv6)],true),po(m2_lights_wrong_v2,'Invariant  preservation',[event('IL_tl_green'),invariant(inv2_5)],true),po(m2_lights_wrong_v2,'Invariant  preservation',[event('IL_tl_green'),invariant(inv5)],true),po(m2_lights_wrong_v2,'Invariant  preservation',[event('IL_tl_green'),invariant(inv6)],true),po(m1_bridge,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po(m1_bridge,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po(m1_bridge,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po(m1_bridge,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4)],true),po(m1_bridge,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],true),po(m1_bridge,'Invariant  preservation',[event('ML_out'),event('ML_out'),invariant(inv1)],true),po(m1_bridge,'Invariant  preservation',[event('ML_out'),event('ML_out'),invariant(inv4)],true),po(m1_bridge,'Invariant  preservation',[event('ML_out'),event('ML_out'),invariant(inv5)],true),po(m1_bridge,'Guard strengthening (split)',[event('ML_out'),guard(grd1),event('ML_out'),event('ML_out')],true),po(m1_bridge,'Invariant  preservation',[event('ML_in'),event('ML_in'),invariant(inv3)],true),po(m1_bridge,'Invariant  preservation',[event('ML_in'),event('ML_in'),invariant(inv4)],true),po(m1_bridge,'Invariant  preservation',[event('ML_in'),event('ML_in'),invariant(inv5)],true),po(m1_bridge,'Guard strengthening (split)',[event('ML_in'),guard(grd1),event('ML_in'),event('ML_in')],true),po(m1_bridge,'Invariant  preservation',[event('IL_in'),invariant(inv1)],true),po(m1_bridge,'Invariant  preservation',[event('IL_in'),invariant(inv2)],true),po(m1_bridge,'Invariant  preservation',[event('IL_in'),invariant(inv4)],true),po(m1_bridge,'Invariant  preservation',[event('IL_in'),invariant(inv5)],true),po(m1_bridge,'Natural number variant of event',[event('IL_in'),variant(vrn)],true),po(m1_bridge,'Variant of event',[event('IL_in'),variant(vrn)],true),po(m1_bridge,'Invariant  preservation',[event('IL_out'),invariant(inv2)],true),po(m1_bridge,'Invariant  preservation',[event('IL_out'),invariant(inv3)],true),po(m1_bridge,'Invariant  preservation',[event('IL_out'),invariant(inv4)],true),po(m1_bridge,'Invariant  preservation',[event('IL_out'),invariant(inv5)],true),po(m1_bridge,'Natural number variant of event',[event('IL_out'),variant(vrn)],true),po(m1_bridge,'Variant of event',[event('IL_out'),variant(vrn)],true),po(m0_island_bridge,'Invariant  establishment',[event('INITIALISATION'),invariant(inv1)],true),po(m0_island_bridge,'Invariant  establishment',[event('INITIALISATION'),invariant(inv2)],true),po(m0_island_bridge,'Invariant  establishment',[event('INITIALISATION'),invariant('DLF')],true),po(m0_island_bridge,'Invariant  preservation',[event('ML_out'),invariant(inv1)],true),po(m0_island_bridge,'Invariant  preservation',[event('ML_out'),invariant(inv2)],true),po(m0_island_bridge,'Invariant  preservation',[event('ML_out'),invariant('DLF')],true),po(m0_island_bridge,'Invariant  preservation',[event('ML_in'),invariant(inv1)],true),po(m0_island_bridge,'Invariant  preservation',[event('ML_in'),invariant(inv2)],true),po(m0_island_bridge,'Invariant  preservation',[event('ML_in'),invariant('DLF')],true)],_Error)).
+

Bridge/visb_m2.json

+{
+  "svg": "bridge_island_visualization.svg",
+  "include": "visb_m1.json",
+  "items": [
+    {
+      "id": "ml_tl",
+      "attr": "fill",
+      "override": "true",
+      "value": "IF ml_tl=green THEN \"green\" ELSE \"red\" END"
+    },
+    {
+      "id": "il_tl",
+      "attr": "fill",
+      "override": "true",
+      "value": "IF il_tl=green THEN \"green\" ELSE \"red\" END"
+    }
+  ],
+  "events": [
+    {
+      "id": "ml_tl",
+      "event": "ML_tl_green",
+      "hovers": [{ "id": "il_tl", "attr":"opacity", "enter":"0.75", "leave":"1.0"},
+                 { "id": "ml_tl", "attr":"opacity", "enter":"0.75", "leave":"1.0"}]
+    },
+    {
+      "id": "il_tl",
+      "event": "IL_tl_green",
+      "hovers": [{ "id": "il_tl", "attr":"opacity", "enter":"0.75", "leave":"1.0"},
+                 { "id": "ml_tl", "attr":"opacity", "enter":"0.75", "leave":"1.0"}]
+    }
+  ]
+}