1

package(load_event_b_project([event_b_model(none,m3,[sees(none,[cd,'COLOR','SENSOR']),refines(none,m2),variables(none,[identifier(none,'A'),identifier(none,'B'),identifier(none,'C'),identifier(none,'IL_IN_SR'),identifier(none,'IL_OUT_SR'),identifier(none,'ML_IN_SR'),identifier(none,'ML_OUT_SR'),identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,il_in_10),identifier(none,il_out_10),identifier(none,il_pass),identifier(none,il_tl),identifier(none,ml_in_10),identifier(none,ml_out_10),identifier(none,ml_pass),identifier(none,ml_tl)]),invariant(none,[implication(rodinpos(inv1,internal_inv1I),equal(none,identifier(none,'IL_IN_SR'),identifier(none,on)),greater(none,identifier(none,'A'),integer(none,0))),implication(rodinpos(inv2,internal_inv2I),equal(none,identifier(none,'IL_OUT_SR'),identifier(none,on)),greater(none,identifier(none,'B'),integer(none,0))),implication(rodinpos(inv3,internal_inv3I),equal(none,identifier(none,'ML_IN_SR'),identifier(none,on)),greater(none,identifier(none,'C'),integer(none,0))),implication(rodinpos(inv4,internal_inv4I),equal(none,identifier(none,ml_out_10),boolean_true(none)),equal(none,identifier(none,ml_tl),identifier(none,green))),implication(rodinpos(inv5,internal_inv5I),equal(none,identifier(none,il_out_10),boolean_true(none)),equal(none,identifier(none,il_tl),identifier(none,green))),implication(rodinpos(inv6,internal_inv6I),equal(none,identifier(none,'IL_IN_SR'),identifier(none,on)),equal(none,identifier(none,il_in_10),boolean_false(none))),implication(rodinpos(inv7,internal_inv7I),equal(none,identifier(none,'IL_OUT_SR'),identifier(none,on)),equal(none,identifier(none,il_out_10),boolean_false(none))),implication(rodinpos(inv8,internal_inv8I),equal(none,identifier(none,'ML_IN_SR'),identifier(none,on)),equal(none,identifier(none,ml_in_10),boolean_false(none))),implication(rodinpos(inv9,internal_inv9I),equal(none,identifier(none,'ML_OUT_SR'),identifier(none,on)),equal(none,identifier(none,ml_out_10),boolean_false(none))),implication(rodinpos(inv10,internal_inv10I),conjunct(none,equal(none,identifier(none,il_in_10),boolean_true(none)),equal(none,identifier(none,ml_out_10),boolean_true(none))),equal(none,identifier(none,'A'),identifier(none,a))),implication(rodinpos(inv11,internal_inv11I),conjunct(none,equal(none,identifier(none,il_in_10),boolean_false(none)),equal(none,identifier(none,ml_out_10),boolean_true(none))),equal(none,identifier(none,'A'),add(none,identifier(none,a),integer(none,1)))),implication(rodinpos(inv12,internal_inv12I),conjunct(none,equal(none,identifier(none,il_in_10),boolean_true(none)),equal(none,identifier(none,ml_out_10),boolean_false(none))),equal(none,identifier(none,'A'),minus(none,identifier(none,a),integer(none,1)))),implication(rodinpos(inv13,internal_inv13I),conjunct(none,equal(none,identifier(none,il_in_10),boolean_false(none)),equal(none,identifier(none,ml_out_10),boolean_false(none))),equal(none,identifier(none,'A'),identifier(none,a))),implication(rodinpos(inv14,internal_inv14I),conjunct(none,equal(none,identifier(none,il_in_10),boolean_true(none)),equal(none,identifier(none,il_out_10),boolean_true(none))),equal(none,identifier(none,'B'),identifier(none,b))),implication(rodinpos(inv15,internal_inv15I),conjunct(none,equal(none,identifier(none,il_in_10),boolean_true(none)),equal(none,identifier(none,il_out_10),boolean_false(none))),equal(none,identifier(none,'B'),add(none,identifier(none,b),integer(none,1)))),implication(rodinpos(inv16,internal_inv16I),conjunct(none,equal(none,identifier(none,il_in_10),boolean_false(none)),equal(none,identifier(none,il_out_10),boolean_true(none))),equal(none,identifier(none,'B'),minus(none,identifier(none,b),integer(none,1)))),implication(rodinpos(inv17,internal_inv17I),conjunct(none,equal(none,identifier(none,il_in_10),boolean_false(none)),equal(none,identifier(none,il_out_10),boolean_false(none))),equal(none,identifier(none,'B'),identifier(none,b))),implication(rodinpos(inv18,internal_inv18I),conjunct(none,equal(none,identifier(none,il_out_10),boolean_true(none)),equal(none,identifier(none,ml_in_10),boolean_true(none))),equal(none,identifier(none,'C'),identifier(none,c))),implication(rodinpos(inv19,internal_inv19I),conjunct(none,equal(none,identifier(none,il_out_10),boolean_true(none)),equal(none,identifier(none,ml_in_10),boolean_false(none))),equal(none,identifier(none,'C'),add(none,identifier(none,c),integer(none,1)))),implication(rodinpos(inv20,internal_inv20I),conjunct(none,equal(none,identifier(none,il_out_10),boolean_false(none)),equal(none,identifier(none,ml_in_10),boolean_true(none))),equal(none,identifier(none,'C'),minus(none,identifier(none,c),integer(none,1)))),implication(rodinpos(inv21,internal_inv21I),conjunct(none,equal(none,identifier(none,il_out_10),boolean_false(none)),equal(none,identifier(none,ml_in_10),boolean_false(none))),equal(none,identifier(none,'C'),identifier(none,c))),disjunct(rodinpos(inv22,internal_inv22I),equal(none,identifier(none,'A'),integer(none,0)),equal(none,identifier(none,'C'),integer(none,0))),less_equal(rodinpos(inv23,internal_inv23I),add(none,identifier(none,'A'),add(none,identifier(none,'B'),identifier(none,'C'))),identifier(none,d)),member(rodinpos(inv24,internal_inv24I),identifier(none,'A'),natural_set(none)),member(rodinpos(inv25,internal_inv25I),identifier(none,'B'),natural_set(none)),member(rodinpos(inv26,internal_inv26I),identifier(none,'C'),natural_set(none))]),theorems(none,[]),events(none,[event(rodinpos('INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[assign(rodinpos(act2,internal_act2),[identifier(none,a)],[integer(none,0)]),assign(rodinpos(act3,internal_act3),[identifier(none,b)],[integer(none,0)]),assign(rodinpos(act4,internal_act4),[identifier(none,c)],[integer(none,0)]),assign(rodinpos(act1,internal_act1),[identifier(none,ml_tl)],[identifier(none,red)]),assign(rodinpos(act5,internal_act5),[identifier(none,il_tl)],[identifier(none,red)]),assign(rodinpos(act6,internal_act6),[identifier(none,ml_pass)],[integer(none,1)]),assign(rodinpos(act7,internal_act7),[identifier(none,il_pass)],[integer(none,1)]),assign(rodinpos(act15,internal_act8),[identifier(none,ml_out_10)],[boolean_false(none)]),assign(rodinpos(qct16,internal_act9),[identifier(none,il_out_10)],[boolean_false(none)]),assign(rodinpos(act17,internal_act10),[identifier(none,ml_in_10)],[boolean_false(none)]),assign(rodinpos(act18,internal_act11),[identifier(none,il_in_10)],[boolean_false(none)]),assign(rodinpos(act8,internal_act12),[identifier(none,'A')],[integer(none,0)]),assign(rodinpos(act9,internal_act13),[identifier(none,'B')],[integer(none,0)]),assign(rodinpos(act10,internal_act14),[identifier(none,'C')],[integer(none,0)]),assign(rodinpos(act11,internal_act15),[identifier(none,'ML_IN_SR')],[identifier(none,off)]),assign(rodinpos(act12,internal_act16),[identifier(none,'ML_OUT_SR')],[identifier(none,off)]),assign(rodinpos(act13,internal_act17),[identifier(none,'IL_OUT_SR')],[identifier(none,off)]),assign(rodinpos(act14,internal_act18),[identifier(none,'IL_IN_SR')],[identifier(none,off)])],[]),event(rodinpos('ML_out1',internal_evt2),'ML_out1',ordinary(none),['ML_out1'],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,ml_out_10),boolean_true(none)),less(rodinpos(grd2,internal_grd2),add(none,identifier(none,a),add(none,identifier(none,b),integer(none,1))),identifier(none,d))],[assign(rodinpos(act1,internal_act1),[identifier(none,a)],[add(none,identifier(none,a),integer(none,1))]),assign(rodinpos(act2,internal_act2),[identifier(none,ml_pass)],[integer(none,1)]),assign(rodinpos(act3,internal_act3),[identifier(none,ml_out_10)],[boolean_false(none)])],[]),event(rodinpos('ML_out2',internal_evt3),'ML_out2',ordinary(none),['ML_out2'],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,ml_out_10),boolean_true(none)),equal(rodinpos(grd2,internal_grd2),add(none,identifier(none,a),add(none,identifier(none,b),integer(none,1))),identifier(none,d))],[assign(rodinpos(act1,internal_act1),[identifier(none,a)],[add(none,identifier(none,a),integer(none,1))]),assign(rodinpos(act2,internal_act2),[identifier(none,ml_tl)],[identifier(none,red)]),assign(rodinpos(act3,internal_act3),[identifier(none,ml_pass)],[integer(none,1)]),assign(rodinpos(act4,internal_act4),[identifier(none,ml_out_10)],[boolean_false(none)])],[]),event(rodinpos('IL_out1',internal_evt4),'IL_out1',ordinary(none),['IL_out1'],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,il_out_10),boolean_true(none)),greater(rodinpos(grd2,internal_grd2),identifier(none,b),integer(none,1))],[assign(rodinpos(act1,internal_act1),[identifier(none,b)],[minus(none,identifier(none,b),integer(none,1))]),assign(rodinpos(act2,internal_act2),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))]),assign(rodinpos(act3,internal_act3),[identifier(none,il_pass)],[integer(none,1)]),assign(rodinpos(act4,internal_act4),[identifier(none,il_out_10)],[boolean_false(none)])],[]),event(rodinpos('IL_out2',internal_evt5),'IL_out2',ordinary(none),['IL_out2'],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,il_out_10),boolean_true(none)),equal(rodinpos(grd2,internal_grd2),identifier(none,b),integer(none,1))],[assign(rodinpos(act1,internal_act1),[identifier(none,b)],[minus(none,identifier(none,b),integer(none,1))]),assign(rodinpos(act2,internal_act2),[identifier(none,il_tl)],[identifier(none,red)]),assign(rodinpos(act3,internal_act3),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))]),assign(rodinpos(act4,internal_act4),[identifier(none,il_pass)],[integer(none,1)]),assign(rodinpos(act5,internal_act5),[identifier(none,il_out_10)],[boolean_false(none)])],[]),event(rodinpos('ML_tl_green',internal_evt6),'ML_tl_green',convergent(none),['ML_tl_green'],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,ml_tl),identifier(none,red)),less(rodinpos(grd2,internal_grd2),add(none,identifier(none,a),identifier(none,b)),identifier(none,d)),equal(rodinpos(grd3,internal_grd3),identifier(none,c),integer(none,0)),equal(rodinpos(grd4,internal_grd4),identifier(none,il_pass),integer(none,1)),equal(rodinpos(grd5,internal_grd5),identifier(none,il_out_10),boolean_false(none)),equal(rodinpos(grd6,internal_grd6),identifier(none,'ML_OUT_SR'),identifier(none,on))],[assign(rodinpos(act1,internal_act1),[identifier(none,ml_tl)],[identifier(none,green)]),assign(rodinpos(act2,internal_act2),[identifier(none,il_tl)],[identifier(none,red)]),assign(rodinpos(act3,internal_act3),[identifier(none,ml_pass)],[integer(none,0)])],[]),event(rodinpos('IL_tl_green',internal_evt7),'IL_tl_green',convergent(none),['IL_tl_green'],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,il_tl),identifier(none,red)),less(rodinpos(grd2,internal_grd2),integer(none,0),identifier(none,b)),equal(rodinpos(grd3,internal_grd3),identifier(none,a),integer(none,0)),equal(rodinpos(grd4,internal_grd4),identifier(none,ml_pass),integer(none,1)),equal(rodinpos(grd5,internal_grd5),identifier(none,ml_out_10),boolean_false(none)),equal(rodinpos(grd6,internal_grd6),identifier(none,'IL_OUT_SR'),identifier(none,on))],[assign(rodinpos(act1,internal_act1),[identifier(none,il_tl)],[identifier(none,green)]),assign(rodinpos(act2,internal_act2),[identifier(none,ml_tl)],[identifier(none,red)]),assign(rodinpos(act3,internal_act3),[identifier(none,il_pass)],[integer(none,0)])],[]),event(rodinpos('ML_in',internal_evt8),'ML_in',ordinary(none),['ML_in'],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,ml_in_10),boolean_true(none)),greater(rodinpos(grd2,internal_grd2),identifier(none,c),integer(none,0))],[assign(rodinpos(act1,internal_act1),[identifier(none,c)],[minus(none,identifier(none,c),integer(none,1))]),assign(rodinpos(act2,internal_act2),[identifier(none,ml_in_10)],[boolean_false(none)])],[]),event(rodinpos('IL_in',internal_evt9),'IL_in',ordinary(none),['IL_in'],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,il_in_10),boolean_true(none)),less(rodinpos(grd2,internal_grd2),integer(none,0),identifier(none,a))],[assign(rodinpos(act1,internal_act1),[identifier(none,a)],[minus(none,identifier(none,a),integer(none,1))]),assign(rodinpos(act2,internal_act2),[identifier(none,b)],[add(none,identifier(none,b),integer(none,1))]),assign(rodinpos(act3,internal_act3),[identifier(none,il_in_10)],[boolean_false(none)])],[]),event(rodinpos('ML_OUT_ARR',internal_evt10),'ML_OUT_ARR',ordinary(none),[],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,'ML_OUT_SR'),identifier(none,off)),equal(rodinpos(grd2,internal_grd2),identifier(none,ml_out_10),boolean_false(none))],[assign(rodinpos(act1,internal_act1),[identifier(none,'ML_OUT_SR')],[identifier(none,on)])],[]),event(rodinpos('ML_IN_ARR',internal_evt11),'ML_IN_ARR',ordinary(none),[],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,'ML_IN_SR'),identifier(none,off)),equal(rodinpos(grd2,internal_grd2),identifier(none,ml_in_10),boolean_false(none)),greater(rodinpos(grd3,internal_grd3),identifier(none,'C'),integer(none,0))],[assign(rodinpos(act1,internal_act1),[identifier(none,'ML_IN_SR')],[identifier(none,on)])],[]),event(rodinpos('IL_IN_ARR',internal_evt12),'IL_IN_ARR',ordinary(none),[],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,'IL_IN_SR'),identifier(none,off)),equal(rodinpos(grd2,internal_grd2),identifier(none,il_in_10),boolean_false(none)),greater(rodinpos(grd3,internal_grd3),identifier(none,'A'),integer(none,0))],[assign(rodinpos(act1,internal_act1),[identifier(none,'IL_IN_SR')],[identifier(none,on)])],[]),event(rodinpos('IL_OUT_AR',internal_evt13),'IL_OUT_AR',ordinary(none),[],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,'IL_OUT_SR'),identifier(none,off)),equal(rodinpos(grd2,internal_grd2),identifier(none,il_out_10),boolean_false(none)),greater(rodinpos(grd3,internal_grd3),identifier(none,'B'),integer(none,0))],[assign(rodinpos(act1,internal_act1),[identifier(none,'IL_OUT_SR')],[identifier(none,on)])],[]),event(rodinpos('ML_OUT_DEP',internal_evt14),'ML_OUT_DEP',ordinary(none),[],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,'ML_OUT_SR'),identifier(none,on)),equal(rodinpos(grd2,internal_grd2),identifier(none,ml_tl),identifier(none,green))],[assign(rodinpos(act1,internal_act1),[identifier(none,'ML_OUT_SR')],[identifier(none,off)]),assign(rodinpos(act2,internal_act2),[identifier(none,ml_out_10)],[boolean_true(none)]),assign(rodinpos(act3,internal_act3),[identifier(none,'A')],[add(none,identifier(none,'A'),integer(none,1))])],[]),event(rodinpos('ML_IN_DEP',internal_evt15),'ML_IN_DEP',ordinary(none),[],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,'ML_IN_SR'),identifier(none,on))],[assign(rodinpos(act1,internal_act1),[identifier(none,'ML_IN_SR')],[identifier(none,off)]),assign(rodinpos(act2,internal_act2),[identifier(none,ml_in_10)],[boolean_true(none)]),assign(rodinpos(act3,internal_act3),[identifier(none,'C')],[minus(none,identifier(none,'C'),integer(none,1))])],[]),event(rodinpos('IL_IN_DEP',internal_evt16),'IL_IN_DEP',ordinary(none),[],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,'IL_IN_SR'),identifier(none,on))],[assign(rodinpos(act1,internal_act1),[identifier(none,'IL_IN_SR')],[identifier(none,off)]),assign(rodinpos(act2,internal_act2),[identifier(none,il_in_10)],[boolean_true(none)]),assign(rodinpos(act3,internal_act3),[identifier(none,'A')],[minus(none,identifier(none,'A'),integer(none,1))]),assign(rodinpos(act4,internal_act4),[identifier(none,'B')],[add(none,identifier(none,'B'),integer(none,1))])],[]),event(rodinpos('IL_OUT_DEP',internal_evt17),'IL_OUT_DEP',ordinary(none),[],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,'IL_OUT_SR'),identifier(none,on)),equal(rodinpos(grd2,internal_grd2),identifier(none,il_tl),identifier(none,green))],[assign(rodinpos(act1,internal_act1),[identifier(none,'IL_OUT_SR')],[identifier(none,off)]),assign(rodinpos(act2,internal_act2),[identifier(none,il_out_10)],[boolean_true(none)]),assign(rodinpos(act3,internal_act3),[identifier(none,'B')],[minus(none,identifier(none,'B'),integer(none,1))]),assign(rodinpos(act4,internal_act4),[identifier(none,'C')],[add(none,identifier(none,'C'),integer(none,1))])],[])])]),event_b_model(none,m2,[sees(none,[cd,'COLOR']),refines(none,m1),variables(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,il_pass),identifier(none,il_tl),identifier(none,ml_pass),identifier(none,ml_tl)]),invariant(none,[member(rodinpos(inv1,internal_inv1I),identifier(none,ml_tl),identifier(none,'Color')),member(rodinpos(inv2,internal_inv2I),identifier(none,il_tl),identifier(none,'Color')),implication(rodinpos(inv3,internal_inv3I),equal(none,identifier(none,ml_tl),identifier(none,green)),equal(none,identifier(none,c),integer(none,0))),implication(rodinpos(inv12,internal_inv12I),equal(none,identifier(none,ml_tl),identifier(none,green)),less(none,add(none,identifier(none,a),add(none,identifier(none,b),identifier(none,c))),identifier(none,d))),implication(rodinpos(inv4,internal_inv4I),equal(none,identifier(none,il_tl),identifier(none,green)),equal(none,identifier(none,a),integer(none,0))),implication(rodinpos(inv11,internal_inv11I),equal(none,identifier(none,il_tl),identifier(none,green)),greater(none,identifier(none,b),integer(none,0))),member(rodinpos(inv6,internal_inv6I),identifier(none,il_pass),interval(none,integer(none,0),integer(none,1))),member(rodinpos(inv7,internal_inv7I),identifier(none,ml_pass),interval(none,integer(none,0),integer(none,1))),implication(rodinpos(inv8,internal_inv8I),equal(none,identifier(none,ml_tl),identifier(none,red)),equal(none,identifier(none,ml_pass),integer(none,1))),implication(rodinpos(inv9,internal_inv9I),equal(none,identifier(none,il_tl),identifier(none,red)),equal(none,identifier(none,il_pass),integer(none,1))),disjunct(rodinpos(inv5,internal_element1I),equal(none,identifier(none,il_tl),identifier(none,red)),equal(none,identifier(none,ml_tl),identifier(none,red)))]),theorems(none,[]),variant(none,add(none,identifier(none,ml_pass),identifier(none,il_pass))),events(none,[event(rodinpos('INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[assign(rodinpos(act2,internal_act2),[identifier(none,a)],[integer(none,0)]),assign(rodinpos(act3,internal_act3),[identifier(none,b)],[integer(none,0)]),assign(rodinpos(act4,internal_act4),[identifier(none,c)],[integer(none,0)]),assign(rodinpos(act1,internal_act1),[identifier(none,ml_tl)],[identifier(none,red)]),assign(rodinpos(act5,internal_act5),[identifier(none,il_tl)],[identifier(none,red)]),assign(rodinpos(act6,internal_act6),[identifier(none,ml_pass)],[integer(none,1)]),assign(rodinpos(act7,internal_act7),[identifier(none,il_pass)],[integer(none,1)])],[]),event(rodinpos('ML_out1',internal_evt2),'ML_out1',ordinary(none),['ML_out'],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,ml_tl),identifier(none,green)),less(rodinpos(grd2,internal_grd2),add(none,identifier(none,a),add(none,identifier(none,b),integer(none,1))),identifier(none,d))],[assign(rodinpos(act1,internal_act1),[identifier(none,a)],[add(none,identifier(none,a),integer(none,1))]),assign(rodinpos(act2,internal_act2),[identifier(none,ml_pass)],[integer(none,1)])],[]),event(rodinpos('ML_out2',internal_evt3),'ML_out2',ordinary(none),['ML_out'],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,ml_tl),identifier(none,green)),equal(rodinpos(grd2,internal_grd2),add(none,identifier(none,a),add(none,identifier(none,b),integer(none,1))),identifier(none,d))],[assign(rodinpos(act1,internal_act1),[identifier(none,a)],[add(none,identifier(none,a),integer(none,1))]),assign(rodinpos(act2,internal_act2),[identifier(none,ml_tl)],[identifier(none,red)]),assign(rodinpos(act3,internal_act3),[identifier(none,ml_pass)],[integer(none,1)])],[]),event(rodinpos('IL_out1',internal_evt4),'IL_out1',ordinary(none),['IL_out'],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,il_tl),identifier(none,green)),greater(rodinpos(grd2,internal_grd2),identifier(none,b),integer(none,1))],[assign(rodinpos(act1,internal_act1),[identifier(none,b)],[minus(none,identifier(none,b),integer(none,1))]),assign(rodinpos(act2,internal_act2),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))]),assign(rodinpos(act3,internal_act3),[identifier(none,il_pass)],[integer(none,1)])],[]),event(rodinpos('IL_out2',internal_evt5),'IL_out2',ordinary(none),['IL_out'],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,il_tl),identifier(none,green)),equal(rodinpos(grd2,internal_grd2),identifier(none,b),integer(none,1))],[assign(rodinpos(act1,internal_act1),[identifier(none,b)],[minus(none,identifier(none,b),integer(none,1))]),assign(rodinpos(act2,internal_act2),[identifier(none,il_tl)],[identifier(none,red)]),assign(rodinpos(act3,internal_act3),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))]),assign(rodinpos(act4,internal_act4),[identifier(none,il_pass)],[integer(none,1)])],[]),event(rodinpos('ML_tl_green',internal_evt6),'ML_tl_green',convergent(none),[],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,ml_tl),identifier(none,red)),less(rodinpos(grd2,internal_grd2),add(none,identifier(none,a),identifier(none,b)),identifier(none,d)),equal(rodinpos(grd3,internal_grd3),identifier(none,c),integer(none,0)),equal(rodinpos(grd4,internal_grd4),identifier(none,il_pass),integer(none,1))],[assign(rodinpos(act1,internal_act1),[identifier(none,ml_tl)],[identifier(none,green)]),assign(rodinpos(act2,internal_act2),[identifier(none,il_tl)],[identifier(none,red)]),assign(rodinpos(act3,internal_act3),[identifier(none,ml_pass)],[integer(none,0)])],[]),event(rodinpos('IL_tl_green',internal_evt7),'IL_tl_green',convergent(none),[],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,il_tl),identifier(none,red)),less(rodinpos(grd2,internal_grd2),integer(none,0),identifier(none,b)),equal(rodinpos(grd3,internal_grd3),identifier(none,a),integer(none,0)),equal(rodinpos(grd4,internal_grd4),identifier(none,ml_pass),integer(none,1))],[assign(rodinpos(act1,internal_act1),[identifier(none,il_tl)],[identifier(none,green)]),assign(rodinpos(act2,internal_act2),[identifier(none,ml_tl)],[identifier(none,red)]),assign(rodinpos(act3,internal_act3),[identifier(none,il_pass)],[integer(none,0)])],[]),event(rodinpos('IL_in',internal_evt8),'IL_in',ordinary(none),['IL_in'],[],[less(rodinpos(grd11,internal_grd1),integer(none,0),identifier(none,a))],[assign(rodinpos(act11,internal_act1),[identifier(none,a)],[minus(none,identifier(none,a),integer(none,1))]),assign(rodinpos(act12,internal_act2),[identifier(none,b)],[add(none,identifier(none,b),integer(none,1))])],[]),event(rodinpos('ML_in',internal_evt9),'ML_in',ordinary(none),['ML_in'],[],[less(rodinpos(grd1,internal_grd1),integer(none,0),identifier(none,c))],[assign(rodinpos(act1,internal_act1),[identifier(none,c)],[minus(none,identifier(none,c),integer(none,1))])],[])])]),event_b_model(none,m1,[sees(none,[cd]),refines(none,m0),variables(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),invariant(none,[member(rodinpos(inv1,internal_inv1I),identifier(none,a),natural_set(none)),member(rodinpos(inv2,internal_inv2I),identifier(none,b),natural_set(none)),member(rodinpos(inv3,internal_inv3I),identifier(none,c),natural_set(none)),equal(rodinpos(inv4,internal_inv4I),identifier(none,n),add(none,identifier(none,a),add(none,identifier(none,b),identifier(none,c)))),disjunct(rodinpos(inv5,internal_inv5I),equal(none,identifier(none,a),integer(none,0)),equal(none,identifier(none,c),integer(none,0)))]),theorems(none,[member(rodinpos(thm1,internal_thm1T),add(none,identifier(none,a),add(none,identifier(none,b),identifier(none,c))),natural_set(none))]),variant(none,add(none,multiplication(none,integer(none,2),identifier(none,a)),identifier(none,b))),events(none,[event(rodinpos('INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[assign(rodinpos(act2,internal_act2),[identifier(none,a)],[integer(none,0)]),assign(rodinpos(act3,internal_act3),[identifier(none,b)],[integer(none,0)]),assign(rodinpos(act4,internal_act4),[identifier(none,c)],[integer(none,0)])],[]),event(rodinpos('ML_out',internal_evt3),'ML_out',ordinary(none),['ML_out'],[],[less(rodinpos(grd1,internal_grd1),add(none,identifier(none,a),identifier(none,b)),identifier(none,d)),equal(rodinpos(grd2,internal_grd2),identifier(none,c),integer(none,0))],[assign(rodinpos(act1,internal_act1),[identifier(none,a)],[add(none,identifier(none,a),integer(none,1))])],[]),event(rodinpos('IL_in',internal_evt2),'IL_in',convergent(none),[],[],[greater(rodinpos(grd1,internal_grd1),identifier(none,a),integer(none,0))],[assign(rodinpos(act1,internal_act1),[identifier(none,a)],[minus(none,identifier(none,a),integer(none,1))]),assign(rodinpos(act2,internal_act2),[identifier(none,b)],[add(none,identifier(none,b),integer(none,1))])],[]),event(rodinpos('IL_out',internal_evt5),'IL_out',convergent(none),[],[],[less(rodinpos(grd1,internal_grd1),integer(none,0),identifier(none,b)),equal(rodinpos(grd2,internal_grd2),identifier(none,a),integer(none,0))],[assign(rodinpos(act1,internal_act1),[identifier(none,b)],[minus(none,identifier(none,b),integer(none,1))]),assign(rodinpos(act2,internal_act2),[identifier(none,c)],[add(none,identifier(none,c),integer(none,1))])],[]),event(rodinpos('ML_in',internal_evt4),'ML_in',ordinary(none),['ML_in'],[],[greater(rodinpos(grd1,internal_grd1),identifier(none,c),integer(none,0))],[assign(rodinpos(act2,internal_act2),[identifier(none,c)],[minus(none,identifier(none,c),integer(none,1))])],[])])]),event_b_model(none,m0,[sees(none,[cd]),variables(none,[identifier(none,n)]),invariant(none,[member(rodinpos(inv1,internal_inv1I),identifier(none,n),natural_set(none)),less_equal(rodinpos(inv2,internal_inv2I),identifier(none,n),identifier(none,d))]),theorems(none,[disjunct(rodinpos(thm1,internal_thm1T),greater(none,identifier(none,n),integer(none,0)),less(none,identifier(none,n),identifier(none,d)))]),events(none,[event(rodinpos('INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[assign(rodinpos(act1,internal_act1),[identifier(none,n)],[integer(none,0)])],[]),event(rodinpos('ML_out',internal_evt3),'ML_out',ordinary(none),[],[],[less(rodinpos(grd1,internal_grd1),identifier(none,n),identifier(none,d))],[assign(rodinpos(act1,internal_act1),[identifier(none,n)],[add(none,identifier(none,n),integer(none,1))])],[]),event(rodinpos('ML_in',internal_evt4),'ML_in',ordinary(none),[],[],[greater(rodinpos(grd1,internal_grd1),identifier(none,n),integer(none,0))],[assign(rodinpos(act1,internal_act1),[identifier(none,n)],[minus(none,identifier(none,n),integer(none,1))])],[])])])],[event_b_context(none,cd,[extends(none,[]),constants(none,[identifier(none,d)]),axioms(none,[member(rodinpos(axm1,internal_axm1A),identifier(none,d),natural_set(none)),greater(rodinpos(axm2,internal_axm2A),identifier(none,d),integer(none,0))]),theorems(none,[]),sets(none,[])]),event_b_context(none,'COLOR',[extends(none,[]),constants(none,[identifier(none,green),identifier(none,red)]),axioms(none,[equal(rodinpos(axm4,internal_axm4A),identifier(none,'Color'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(rodinpos(axm3,internal_axm3A),identifier(none,green),identifier(none,red))]),theorems(none,[]),sets(none,[deferred_set(none,'Color')])]),event_b_context(none,'SENSOR',[extends(none,[]),constants(none,[identifier(none,off),identifier(none,on)]),axioms(none,[equal(rodinpos(axm1,internal_axm1A),identifier(none,'Sensor'),set_extension(none,[identifier(none,on),identifier(none,off)])),negation(rodinpos(axm2,internal_axm2A),equal(none,identifier(none,on),identifier(none,off)))]),theorems(none,[]),sets(none,[deferred_set(none,'Sensor')])])],[discharged(m3,'INITIALISATION',inv6),discharged(m3,'INITIALISATION',inv7),discharged(m3,'INITIALISATION',inv8),discharged(m3,'INITIALISATION',inv9),discharged(m3,'INITIALISATION',inv10),discharged(m3,'INITIALISATION',inv13),discharged(m3,'INITIALISATION',inv14),discharged(m3,'INITIALISATION',inv17),discharged(m3,'INITIALISATION',inv18),discharged(m3,'INITIALISATION',inv21),discharged(m3,'ML_out1',inv9),discharged(m3,'ML_out2',inv9),discharged(m3,'IL_out1',inv7),discharged(m3,'IL_out2',inv7),discharged(m3,'ML_tl_green',inv4),discharged(m3,'IL_tl_green',inv5),discharged(m3,'ML_in',inv8),discharged(m3,'IL_in',inv6),discharged(m3,'ML_OUT_ARR',inv9),discharged(m3,'ML_IN_ARR',inv3),discharged(m3,'ML_IN_ARR',inv8),discharged(m3,'IL_IN_ARR',inv1),discharged(m3,'IL_IN_ARR',inv6),discharged(m3,'IL_OUT_AR',inv2),discharged(m3,'IL_OUT_AR',inv7),discharged(m3,'ML_OUT_DEP',inv4),discharged(m3,'ML_IN_DEP',inv22),discharged(m3,'IL_OUT_DEP',inv5),discharged(m2,'INITIALISATION',inv3),discharged(m2,'INITIALISATION',inv4),discharged(m2,'INITIALISATION',inv8),discharged(m2,'INITIALISATION',inv9),discharged(m2,'ML_out1',inv8),discharged(m2,'ML_out2',inv8),discharged(m2,'IL_out1',inv9),discharged(m2,'IL_out2',inv9),discharged(m2,'ML_tl_green',inv3),discharged(m2,'ML_tl_green',inv9),discharged(m2,'IL_tl_green',inv4),discharged(m2,'IL_tl_green',inv8),discharged(m2,'ML_in',inv12),discharged(m1,'INITIALISATION',inv1),discharged(m1,'INITIALISATION',inv2),discharged(m1,'INITIALISATION',inv3),discharged(m1,'INITIALISATION',inv4),discharged(m1,'INITIALISATION',inv5),discharged(m1,'ML_out',inv1),discharged(m1,'ML_out',inv4),discharged(m1,'ML_out',inv5),discharged(m1,'IL_in',inv1),discharged(m1,'IL_in',inv2),discharged(m1,'IL_in',inv5),discharged(m1,'IL_out',inv2),discharged(m1,'IL_out',inv3),discharged(m1,'IL_out',inv4),discharged(m1,'IL_out',inv5),discharged(m1,'ML_in',inv3),discharged(m1,'ML_in',inv4),discharged(m1,'ML_in',inv5),discharged(m0,'INITIALISATION',inv1),discharged(m0,'INITIALISATION',inv2),discharged(m0,'ML_out',inv1),discharged(m0,'ML_out',inv2),discharged(m0,'ML_in',inv1),discharged(m0,'ML_in',inv2),wp('IL_IN_ARR','IL_IN_ARR',[equal(none,identifier(none,on),identifier(none,off)),equal(none,identifier(none,il_in_10),boolean_false(none)),greater(none,identifier(none,'A'),integer(none,0))]),wp('IL_IN_ARR','IL_IN_DEP',[equal(none,identifier(none,on),identifier(none,on))]),wp('IL_IN_DEP','IL_IN_ARR',[equal(none,identifier(none,off),identifier(none,off)),equal(none,boolean_true(none),boolean_false(none)),greater(none,minus(none,identifier(none,'A'),integer(none,1)),integer(none,0))]),wp('IL_IN_DEP','IL_IN_DEP',[equal(none,identifier(none,off),identifier(none,on))]),wp('IL_IN_DEP','IL_OUT_AR',[equal(none,identifier(none,'IL_OUT_SR'),identifier(none,off)),equal(none,identifier(none,il_out_10),boolean_false(none)),greater(none,add(none,identifier(none,'B'),integer(none,1)),integer(none,0))]),wp('IL_IN_DEP','IL_in',[equal(none,boolean_true(none),boolean_true(none)),less(none,integer(none,0),identifier(none,a))]),wp('IL_OUT_AR','IL_OUT_AR',[equal(none,identifier(none,on),identifier(none,off)),equal(none,identifier(none,il_out_10),boolean_false(none)),greater(none,identifier(none,'B'),integer(none,0))]),wp('IL_OUT_AR','IL_OUT_DEP',[equal(none,identifier(none,on),identifier(none,on)),equal(none,identifier(none,il_tl),identifier(none,green))]),wp('IL_OUT_AR','IL_tl_green',[equal(none,identifier(none,il_tl),identifier(none,red)),less(none,integer(none,0),identifier(none,b)),equal(none,identifier(none,a),integer(none,0)),equal(none,identifier(none,ml_pass),integer(none,1)),equal(none,identifier(none,ml_out_10),boolean_false(none)),equal(none,identifier(none,on),identifier(none,on))]),wp('IL_OUT_DEP','IL_OUT_AR',[equal(none,identifier(none,off),identifier(none,off)),equal(none,boolean_true(none),boolean_false(none)),greater(none,minus(none,identifier(none,'B'),integer(none,1)),integer(none,0))]),wp('IL_OUT_DEP','IL_OUT_DEP',[equal(none,identifier(none,off),identifier(none,on)),equal(none,identifier(none,il_tl),identifier(none,green))]),wp('IL_OUT_DEP','IL_out1',[equal(none,boolean_true(none),boolean_true(none)),greater(none,identifier(none,b),integer(none,1))]),wp('IL_OUT_DEP','IL_out2',[equal(none,boolean_true(none),boolean_true(none)),equal(none,identifier(none,b),integer(none,1))]),wp('IL_OUT_DEP','IL_tl_green',[equal(none,identifier(none,il_tl),identifier(none,red)),less(none,integer(none,0),identifier(none,b)),equal(none,identifier(none,a),integer(none,0)),equal(none,identifier(none,ml_pass),integer(none,1)),equal(none,identifier(none,ml_out_10),boolean_false(none)),equal(none,identifier(none,off),identifier(none,on))]),wp('IL_OUT_DEP','ML_IN_ARR',[equal(none,identifier(none,'ML_IN_SR'),identifier(none,off)),equal(none,identifier(none,ml_in_10),boolean_false(none)),greater(none,add(none,identifier(none,'C'),integer(none,1)),integer(none,0))]),wp('IL_OUT_DEP','ML_tl_green',[equal(none,identifier(none,ml_tl),identifier(none,red)),less(none,add(none,identifier(none,a),identifier(none,b)),identifier(none,d)),equal(none,identifier(none,c),integer(none,0)),equal(none,identifier(none,il_pass),integer(none,1)),equal(none,boolean_true(none),boolean_false(none)),equal(none,identifier(none,'ML_OUT_SR'),identifier(none,on))]),wp('IL_in','IL_IN_ARR',[equal(none,identifier(none,'IL_IN_SR'),identifier(none,off)),equal(none,boolean_false(none),boolean_false(none)),greater(none,identifier(none,'A'),integer(none,0))]),wp('IL_in','IL_in',[equal(none,boolean_false(none),boolean_true(none)),less(none,integer(none,0),minus(none,identifier(none,a),integer(none,1)))]),wp('IL_in','IL_out1',[equal(none,identifier(none,il_out_10),boolean_true(none)),greater(none,add(none,identifier(none,b),integer(none,1)),integer(none,1))]),wp('IL_in','IL_out2',[equal(none,identifier(none,il_out_10),boolean_true(none)),equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,1))]),wp('IL_in','IL_tl_green',[equal(none,identifier(none,il_tl),identifier(none,red)),less(none,integer(none,0),add(none,identifier(none,b),integer(none,1))),equal(none,minus(none,identifier(none,a),integer(none,1)),integer(none,0)),equal(none,identifier(none,ml_pass),integer(none,1)),equal(none,identifier(none,ml_out_10),boolean_false(none)),equal(none,identifier(none,'IL_OUT_SR'),identifier(none,on))]),wp('IL_in','ML_out1',[equal(none,identifier(none,ml_out_10),boolean_true(none)),less(none,add(none,minus(none,identifier(none,a),integer(none,1)),add(none,add(none,identifier(none,b),integer(none,1)),integer(none,1))),identifier(none,d))]),wp('IL_in','ML_out2',[equal(none,identifier(none,ml_out_10),boolean_true(none)),equal(none,add(none,minus(none,identifier(none,a),integer(none,1)),add(none,add(none,identifier(none,b),integer(none,1)),integer(none,1))),identifier(none,d))]),wp('IL_in','ML_tl_green',[equal(none,identifier(none,ml_tl),identifier(none,red)),less(none,add(none,minus(none,identifier(none,a),integer(none,1)),add(none,identifier(none,b),integer(none,1))),identifier(none,d)),equal(none,identifier(none,c),integer(none,0)),equal(none,identifier(none,il_pass),integer(none,1)),equal(none,identifier(none,il_out_10),boolean_false(none)),equal(none,identifier(none,'ML_OUT_SR'),identifier(none,on))]),wp('IL_out1','IL_OUT_AR',[equal(none,identifier(none,'IL_OUT_SR'),identifier(none,off)),equal(none,boolean_false(none),boolean_false(none)),greater(none,identifier(none,'B'),integer(none,0))]),wp('IL_out1','IL_out1',[equal(none,boolean_false(none),boolean_true(none)),greater(none,minus(none,identifier(none,b),integer(none,1)),integer(none,1))]),wp('IL_out1','IL_out2',[equal(none,boolean_false(none),boolean_true(none)),equal(none,minus(none,identifier(none,b),integer(none,1)),integer(none,1))]),wp('IL_out1','IL_tl_green',[equal(none,identifier(none,il_tl),identifier(none,red)),less(none,integer(none,0),minus(none,identifier(none,b),integer(none,1))),equal(none,identifier(none,a),integer(none,0)),equal(none,identifier(none,ml_pass),integer(none,1)),equal(none,identifier(none,ml_out_10),boolean_false(none)),equal(none,identifier(none,'IL_OUT_SR'),identifier(none,on))]),wp('IL_out1','ML_in',[equal(none,identifier(none,ml_in_10),boolean_true(none)),greater(none,add(none,identifier(none,c),integer(none,1)),integer(none,0))]),wp('IL_out1','ML_out1',[equal(none,identifier(none,ml_out_10),boolean_true(none)),less(none,add(none,identifier(none,a),add(none,minus(none,identifier(none,b),integer(none,1)),integer(none,1))),identifier(none,d))]),wp('IL_out1','ML_out2',[equal(none,identifier(none,ml_out_10),boolean_true(none)),equal(none,add(none,identifier(none,a),add(none,minus(none,identifier(none,b),integer(none,1)),integer(none,1))),identifier(none,d))]),wp('IL_out1','ML_tl_green',[equal(none,identifier(none,ml_tl),identifier(none,red)),less(none,add(none,identifier(none,a),minus(none,identifier(none,b),integer(none,1))),identifier(none,d)),equal(none,add(none,identifier(none,c),integer(none,1)),integer(none,0)),equal(none,integer(none,1),integer(none,1)),equal(none,boolean_false(none),boolean_false(none)),equal(none,identifier(none,'ML_OUT_SR'),identifier(none,on))]),wp('IL_out2','IL_OUT_AR',[equal(none,identifier(none,'IL_OUT_SR'),identifier(none,off)),equal(none,boolean_false(none),boolean_false(none)),greater(none,identifier(none,'B'),integer(none,0))]),wp('IL_out2','IL_OUT_DEP',[equal(none,identifier(none,'IL_OUT_SR'),identifier(none,on)),equal(none,identifier(none,red),identifier(none,green))]),wp('IL_out2','IL_out1',[equal(none,boolean_false(none),boolean_true(none)),greater(none,minus(none,identifier(none,b),integer(none,1)),integer(none,1))]),wp('IL_out2','IL_out2',[equal(none,boolean_false(none),boolean_true(none)),equal(none,minus(none,identifier(none,b),integer(none,1)),integer(none,1))]),wp('IL_out2','IL_tl_green',[equal(none,identifier(none,red),identifier(none,red)),less(none,integer(none,0),minus(none,identifier(none,b),integer(none,1))),equal(none,identifier(none,a),integer(none,0)),equal(none,identifier(none,ml_pass),integer(none,1)),equal(none,identifier(none,ml_out_10),boolean_false(none)),equal(none,identifier(none,'IL_OUT_SR'),identifier(none,on))]),wp('IL_out2','ML_in',[equal(none,identifier(none,ml_in_10),boolean_true(none)),greater(none,add(none,identifier(none,c),integer(none,1)),integer(none,0))]),wp('IL_out2','ML_out1',[equal(none,identifier(none,ml_out_10),boolean_true(none)),less(none,add(none,identifier(none,a),add(none,minus(none,identifier(none,b),integer(none,1)),integer(none,1))),identifier(none,d))]),wp('IL_out2','ML_out2',[equal(none,identifier(none,ml_out_10),boolean_true(none)),equal(none,add(none,identifier(none,a),add(none,minus(none,identifier(none,b),integer(none,1)),integer(none,1))),identifier(none,d))]),wp('IL_out2','ML_tl_green',[equal(none,identifier(none,ml_tl),identifier(none,red)),less(none,add(none,identifier(none,a),minus(none,identifier(none,b),integer(none,1))),identifier(none,d)),equal(none,add(none,identifier(none,c),integer(none,1)),integer(none,0)),equal(none,integer(none,1),integer(none,1)),equal(none,boolean_false(none),boolean_false(none)),equal(none,identifier(none,'ML_OUT_SR'),identifier(none,on))]),wp('IL_tl_green','IL_OUT_DEP',[equal(none,identifier(none,'IL_OUT_SR'),identifier(none,on)),equal(none,identifier(none,green),identifier(none,green))]),wp('IL_tl_green','IL_tl_green',[equal(none,identifier(none,green),identifier(none,red)),less(none,integer(none,0),identifier(none,b)),equal(none,identifier(none,a),integer(none,0)),equal(none,identifier(none,ml_pass),integer(none,1)),equal(none,identifier(none,ml_out_10),boolean_false(none)),equal(none,identifier(none,'IL_OUT_SR'),identifier(none,on))]),wp('IL_tl_green','ML_OUT_DEP',[equal(none,identifier(none,'ML_OUT_SR'),identifier(none,on)),equal(none,identifier(none,red),identifier(none,green))]),wp('IL_tl_green','ML_tl_green',[equal(none,identifier(none,red),identifier(none,red)),less(none,add(none,identifier(none,a),identifier(none,b)),identifier(none,d)),equal(none,identifier(none,c),integer(none,0)),equal(none,integer(none,0),integer(none,1)),equal(none,identifier(none,il_out_10),boolean_false(none)),equal(none,identifier(none,'ML_OUT_SR'),identifier(none,on))]),wp('INITIALISATION','IL_IN_ARR',[equal(none,identifier(none,off),identifier(none,off)),equal(none,boolean_false(none),boolean_false(none)),greater(none,integer(none,0),integer(none,0))]),wp('INITIALISATION','IL_IN_DEP',[equal(none,identifier(none,off),identifier(none,on))]),wp('INITIALISATION','IL_OUT_AR',[equal(none,identifier(none,off),identifier(none,off)),equal(none,boolean_false(none),boolean_false(none)),greater(none,integer(none,0),integer(none,0))]),wp('INITIALISATION','IL_OUT_DEP',[equal(none,identifier(none,off),identifier(none,on)),equal(none,identifier(none,red),identifier(none,green))]),wp('INITIALISATION','IL_in',[equal(none,boolean_false(none),boolean_true(none)),less(none,integer(none,0),integer(none,0))]),wp('INITIALISATION','IL_out1',[equal(none,boolean_false(none),boolean_true(none)),greater(none,integer(none,0),integer(none,1))]),wp('INITIALISATION','IL_out2',[equal(none,boolean_false(none),boolean_true(none)),equal(none,integer(none,0),integer(none,1))]),wp('INITIALISATION','IL_tl_green',[equal(none,identifier(none,red),identifier(none,red)),less(none,integer(none,0),integer(none,0)),equal(none,integer(none,0),integer(none,0)),equal(none,integer(none,1),integer(none,1)),equal(none,boolean_false(none),boolean_false(none)),equal(none,identifier(none,off),identifier(none,on))]),wp('INITIALISATION','ML_IN_ARR',[equal(none,identifier(none,off),identifier(none,off)),equal(none,boolean_false(none),boolean_false(none)),greater(none,integer(none,0),integer(none,0))]),wp('INITIALISATION','ML_IN_DEP',[equal(none,identifier(none,off),identifier(none,on))]),wp('INITIALISATION','ML_OUT_ARR',[equal(none,identifier(none,off),identifier(none,off)),equal(none,boolean_false(none),boolean_false(none))]),wp('INITIALISATION','ML_OUT_DEP',[equal(none,identifier(none,off),identifier(none,on)),equal(none,identifier(none,red),identifier(none,green))]),wp('INITIALISATION','ML_in',[equal(none,boolean_false(none),boolean_true(none)),greater(none,integer(none,0),integer(none,0))]),wp('INITIALISATION','ML_out1',[equal(none,boolean_false(none),boolean_true(none)),less(none,add(none,integer(none,0),add(none,integer(none,0),integer(none,1))),identifier(none,d))]),wp('INITIALISATION','ML_out2',[equal(none,boolean_false(none),boolean_true(none)),equal(none,add(none,integer(none,0),add(none,integer(none,0),integer(none,1))),identifier(none,d))]),wp('INITIALISATION','ML_tl_green',[equal(none,identifier(none,red),identifier(none,red)),less(none,add(none,integer(none,0),integer(none,0)),identifier(none,d)),equal(none,integer(none,0),integer(none,0)),equal(none,integer(none,1),integer(none,1)),equal(none,boolean_false(none),boolean_false(none)),equal(none,identifier(none,off),identifier(none,on))]),wp('ML_IN_ARR','ML_IN_ARR',[equal(none,identifier(none,on),identifier(none,off)),equal(none,identifier(none,ml_in_10),boolean_false(none)),greater(none,identifier(none,'C'),integer(none,0))]),wp('ML_IN_ARR','ML_IN_DEP',[equal(none,identifier(none,on),identifier(none,on))]),wp('ML_IN_DEP','ML_IN_ARR',[equal(none,identifier(none,off),identifier(none,off)),equal(none,boolean_true(none),boolean_false(none)),greater(none,minus(none,identifier(none,'C'),integer(none,1)),integer(none,0))]),wp('ML_IN_DEP','ML_IN_DEP',[equal(none,identifier(none,off),identifier(none,on))]),wp('ML_IN_DEP','ML_in',[equal(none,boolean_true(none),boolean_true(none)),greater(none,identifier(none,c),integer(none,0))]),wp('ML_OUT_ARR','ML_OUT_ARR',[equal(none,identifier(none,on),identifier(none,off)),equal(none,identifier(none,ml_out_10),boolean_false(none))]),wp('ML_OUT_ARR','ML_OUT_DEP',[equal(none,identifier(none,on),identifier(none,on)),equal(none,identifier(none,ml_tl),identifier(none,green))]),wp('ML_OUT_ARR','ML_tl_green',[equal(none,identifier(none,ml_tl),identifier(none,red)),less(none,add(none,identifier(none,a),identifier(none,b)),identifier(none,d)),equal(none,identifier(none,c),integer(none,0)),equal(none,identifier(none,il_pass),integer(none,1)),equal(none,identifier(none,il_out_10),boolean_false(none)),equal(none,identifier(none,on),identifier(none,on))]),wp('ML_OUT_DEP','IL_IN_ARR',[equal(none,identifier(none,'IL_IN_SR'),identifier(none,off)),equal(none,identifier(none,il_in_10),boolean_false(none)),greater(none,add(none,identifier(none,'A'),integer(none,1)),integer(none,0))]),wp('ML_OUT_DEP','IL_tl_green',[equal(none,identifier(none,il_tl),identifier(none,red)),less(none,integer(none,0),identifier(none,b)),equal(none,identifier(none,a),integer(none,0)),equal(none,identifier(none,ml_pass),integer(none,1)),equal(none,boolean_true(none),boolean_false(none)),equal(none,identifier(none,'IL_OUT_SR'),identifier(none,on))]),wp('ML_OUT_DEP','ML_OUT_ARR',[equal(none,identifier(none,off),identifier(none,off)),equal(none,boolean_true(none),boolean_false(none))]),wp('ML_OUT_DEP','ML_OUT_DEP',[equal(none,identifier(none,off),identifier(none,on)),equal(none,identifier(none,ml_tl),identifier(none,green))]),wp('ML_OUT_DEP','ML_out1',[equal(none,boolean_true(none),boolean_true(none)),less(none,add(none,identifier(none,a),add(none,identifier(none,b),integer(none,1))),identifier(none,d))]),wp('ML_OUT_DEP','ML_out2',[equal(none,boolean_true(none),boolean_true(none)),equal(none,add(none,identifier(none,a),add(none,identifier(none,b),integer(none,1))),identifier(none,d))]),wp('ML_OUT_DEP','ML_tl_green',[equal(none,identifier(none,ml_tl),identifier(none,red)),less(none,add(none,identifier(none,a),identifier(none,b)),identifier(none,d)),equal(none,identifier(none,c),integer(none,0)),equal(none,identifier(none,il_pass),integer(none,1)),equal(none,identifier(none,il_out_10),boolean_false(none)),equal(none,identifier(none,off),identifier(none,on))]),wp('ML_in','ML_IN_ARR',[equal(none,identifier(none,'ML_IN_SR'),identifier(none,off)),equal(none,boolean_false(none),boolean_false(none)),greater(none,identifier(none,'C'),integer(none,0))]),wp('ML_in','ML_in',[equal(none,boolean_false(none),boolean_true(none)),greater(none,minus(none,identifier(none,c),integer(none,1)),integer(none,0))]),wp('ML_in','ML_tl_green',[equal(none,identifier(none,ml_tl),identifier(none,red)),less(none,add(none,identifier(none,a),identifier(none,b)),identifier(none,d)),equal(none,minus(none,identifier(none,c),integer(none,1)),integer(none,0)),equal(none,identifier(none,il_pass),integer(none,1)),equal(none,identifier(none,il_out_10),boolean_false(none)),equal(none,identifier(none,'ML_OUT_SR'),identifier(none,on))]),wp('ML_out1','IL_in',[equal(none,identifier(none,il_in_10),boolean_true(none)),less(none,integer(none,0),add(none,identifier(none,a),integer(none,1)))]),wp('ML_out1','IL_tl_green',[equal(none,identifier(none,il_tl),identifier(none,red)),less(none,integer(none,0),identifier(none,b)),equal(none,add(none,identifier(none,a),integer(none,1)),integer(none,0)),equal(none,integer(none,1),integer(none,1)),equal(none,boolean_false(none),boolean_false(none)),equal(none,identifier(none,'IL_OUT_SR'),identifier(none,on))]),wp('ML_out1','ML_OUT_ARR',[equal(none,identifier(none,'ML_OUT_SR'),identifier(none,off)),equal(none,boolean_false(none),boolean_false(none))]),wp('ML_out1','ML_out1',[equal(none,boolean_false(none),boolean_true(none)),less(none,add(none,add(none,identifier(none,a),integer(none,1)),add(none,identifier(none,b),integer(none,1))),identifier(none,d))]),wp('ML_out1','ML_out2',[equal(none,boolean_false(none),boolean_true(none)),equal(none,add(none,add(none,identifier(none,a),integer(none,1)),add(none,identifier(none,b),integer(none,1))),identifier(none,d))]),wp('ML_out1','ML_tl_green',[equal(none,identifier(none,ml_tl),identifier(none,red)),less(none,add(none,add(none,identifier(none,a),integer(none,1)),identifier(none,b)),identifier(none,d)),equal(none,identifier(none,c),integer(none,0)),equal(none,identifier(none,il_pass),integer(none,1)),equal(none,identifier(none,il_out_10),boolean_false(none)),equal(none,identifier(none,'ML_OUT_SR'),identifier(none,on))]),wp('ML_out2','IL_in',[equal(none,identifier(none,il_in_10),boolean_true(none)),less(none,integer(none,0),add(none,identifier(none,a),integer(none,1)))]),wp('ML_out2','IL_tl_green',[equal(none,identifier(none,il_tl),identifier(none,red)),less(none,integer(none,0),identifier(none,b)),equal(none,add(none,identifier(none,a),integer(none,1)),integer(none,0)),equal(none,integer(none,1),integer(none,1)),equal(none,boolean_false(none),boolean_false(none)),equal(none,identifier(none,'IL_OUT_SR'),identifier(none,on))]),wp('ML_out2','ML_OUT_ARR',[equal(none,identifier(none,'ML_OUT_SR'),identifier(none,off)),equal(none,boolean_false(none),boolean_false(none))]),wp('ML_out2','ML_OUT_DEP',[equal(none,identifier(none,'ML_OUT_SR'),identifier(none,on)),equal(none,identifier(none,red),identifier(none,green))]),wp('ML_out2','ML_out1',[equal(none,boolean_false(none),boolean_true(none)),less(none,add(none,add(none,identifier(none,a),integer(none,1)),add(none,identifier(none,b),integer(none,1))),identifier(none,d))]),wp('ML_out2','ML_out2',[equal(none,boolean_false(none),boolean_true(none)),equal(none,add(none,add(none,identifier(none,a),integer(none,1)),add(none,identifier(none,b),integer(none,1))),identifier(none,d))]),wp('ML_out2','ML_tl_green',[equal(none,identifier(none,red),identifier(none,red)),less(none,add(none,add(none,identifier(none,a),integer(none,1)),identifier(none,b)),identifier(none,d)),equal(none,identifier(none,c),integer(none,0)),equal(none,identifier(none,il_pass),integer(none,1)),equal(none,identifier(none,il_out_10),boolean_false(none)),equal(none,identifier(none,'ML_OUT_SR'),identifier(none,on))]),wp('ML_tl_green','IL_OUT_DEP',[equal(none,identifier(none,'IL_OUT_SR'),identifier(none,on)),equal(none,identifier(none,red),identifier(none,green))]),wp('ML_tl_green','IL_tl_green',[equal(none,identifier(none,red),identifier(none,red)),less(none,integer(none,0),identifier(none,b)),equal(none,identifier(none,a),integer(none,0)),equal(none,integer(none,0),integer(none,1)),equal(none,identifier(none,ml_out_10),boolean_false(none)),equal(none,identifier(none,'IL_OUT_SR'),identifier(none,on))]),wp('ML_tl_green','ML_OUT_DEP',[equal(none,identifier(none,'ML_OUT_SR'),identifier(none,on)),equal(none,identifier(none,green),identifier(none,green))]),wp('ML_tl_green','ML_tl_green',[equal(none,identifier(none,green),identifier(none,red)),less(none,add(none,identifier(none,a),identifier(none,b)),identifier(none,d)),equal(none,identifier(none,c),integer(none,0)),equal(none,identifier(none,il_pass),integer(none,1)),equal(none,identifier(none,il_out_10),boolean_false(none)),equal(none,identifier(none,'ML_OUT_SR'),identifier(none,on))]),nonchanging_guard('INITIALISATION',[]),nonchanging_guard('ML_out1',[]),nonchanging_guard('ML_out2',[]),nonchanging_guard('IL_out1',[]),nonchanging_guard('IL_out2',[]),nonchanging_guard('ML_tl_green',[less(none,add(none,identifier(none,a),identifier(none,b)),identifier(none,d)),equal(none,identifier(none,c),integer(none,0)),equal(none,identifier(none,il_pass),integer(none,1)),equal(none,identifier(none,il_out_10),boolean_false(none)),equal(none,identifier(none,'ML_OUT_SR'),identifier(none,on))]),nonchanging_guard('IL_tl_green',[less(none,integer(none,0),identifier(none,b)),equal(none,identifier(none,a),integer(none,0)),equal(none,identifier(none,ml_pass),integer(none,1)),equal(none,identifier(none,ml_out_10),boolean_false(none)),equal(none,identifier(none,'IL_OUT_SR'),identifier(none,on))]),nonchanging_guard('ML_in',[]),nonchanging_guard('IL_in',[]),nonchanging_guard('ML_OUT_ARR',[equal(none,identifier(none,ml_out_10),boolean_false(none))]),nonchanging_guard('ML_IN_ARR',[equal(none,identifier(none,ml_in_10),boolean_false(none)),greater(none,identifier(none,'C'),integer(none,0))]),nonchanging_guard('IL_IN_ARR',[equal(none,identifier(none,il_in_10),boolean_false(none)),greater(none,identifier(none,'A'),integer(none,0))]),nonchanging_guard('IL_OUT_AR',[equal(none,identifier(none,il_out_10),boolean_false(none)),greater(none,identifier(none,'B'),integer(none,0))]),nonchanging_guard('ML_OUT_DEP',[equal(none,identifier(none,ml_tl),identifier(none,green))]),nonchanging_guard('ML_IN_DEP',[]),nonchanging_guard('IL_IN_DEP',[]),nonchanging_guard('IL_OUT_DEP',[equal(none,identifier(none,il_tl),identifier(none,green))])],_Error)).