1

package(load_event_b_project([event_b_model(none,platoon_3_0,[sees(none,[context,context_1,context_2,context_3]),refines(none,platoon_2),variables(none,[identifier(none,accel),identifier(none,d_vehicle),identifier(none,speed),identifier(none,vehicle),identifier(none,xpos),identifier(none,xpos0)]),invariant(none,[member(rodinpos(inv1,element0I),identifier(none,d_vehicle),interval(none,integer(none,1),add(none,identifier(none,'VEHICLES'),integer(none,1)))),member(rodinpos(inv2,element1I),identifier(none,accel),total_function(none,interval(none,integer(none,1),identifier(none,'VEHICLES')),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL')))),disjunct(rodinpos(inv7,element2I),equal(none,identifier(none,d_vehicle),add(none,identifier(none,'VEHICLES'),integer(none,1))),forall(none,[identifier(none,v)],implication(none,member(none,identifier(none,v),interval(none,integer(none,2),minus(none,identifier(none,d_vehicle),integer(none,1)))),exists(none,[identifier(none,f1),identifier(none,f2)],conjunct(none,member(none,identifier(none,f1),set_extension(none,[identifier(none,new_xpos),identifier(none,new_xpos_max),identifier(none,new_xpos_min)])),conjunct(none,member(none,identifier(none,f2),set_extension(none,[identifier(none,new_xpos),identifier(none,new_xpos_max),identifier(none,new_xpos_min)])),greater(none,minus(none,function(none,identifier(none,f1),[couple(none,[couple(none,[function(none,identifier(none,xpos),[minus(none,identifier(none,v),integer(none,1))]),function(none,identifier(none,speed),[minus(none,identifier(none,v),integer(none,1))])]),function(none,identifier(none,accel),[minus(none,identifier(none,v),integer(none,1))])])]),function(none,identifier(none,f2),[couple(none,[couple(none,[function(none,identifier(none,xpos),[identifier(none,v)]),function(none,identifier(none,speed),[identifier(none,v)])]),function(none,identifier(none,accel),[identifier(none,v)])])])),identifier(none,'CRITICAL_DISTANCE'))))))))]),theorems(none,[]),variant(none,minus(none,add(none,identifier(none,'VEHICLES'),integer(none,1)),identifier(none,d_vehicle))),events(none,[event(rodinpos('INITIALISATION',internal_evt1),'INITIALISATION',['INITIALISATION'],[],[],[assign(rodinpos(act1,internal_act1),[identifier(none,xpos0)],[identifier(none,initial_xpos)]),assign(rodinpos(act3,internal_act3),[identifier(none,xpos)],[identifier(none,initial_xpos)]),assign(rodinpos(act4,internal_act4),[identifier(none,vehicle)],[integer(none,1)]),assign(rodinpos(act2,internal_element1),[identifier(none,speed)],[identifier(none,initial_speed)]),assign(rodinpos(act5,element0),[identifier(none,d_vehicle)],[integer(none,1)]),assign(rodinpos(act6,element1),[identifier(none,accel)],[identifier(none,initial_accel)])],[]),event(rodinpos(decide1,element0),decide1,[],[identifier(rodinpos([],internal_element1),magic_accel)],[equal(rodinpos(grd2,internal_element1),identifier(none,vehicle),integer(none,1)),equal(rodinpos(grd1,internal_element2),identifier(none,d_vehicle),integer(none,1)),member(rodinpos(grd3,internal_element3),identifier(none,magic_accel),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL')))],[assign(rodinpos(act1,internal_element1),[identifier(none,d_vehicle)],[add(none,identifier(none,d_vehicle),integer(none,1))]),assign(rodinpos(act2,internal_element2),[identifier(none,accel)],[overwrite(none,identifier(none,accel),set_extension(none,[couple(none,[identifier(none,d_vehicle),identifier(none,magic_accel)])]))])],[]),event(rodinpos(decide,element1),decide,[],[identifier(rodinpos([],internal_element1),magic_accel)],[equal(rodinpos(grd1,internal_element1),identifier(none,vehicle),integer(none,1)),member(rodinpos(grd2,internal_element2),identifier(none,d_vehicle),interval(none,integer(none,2),identifier(none,'VEHICLES'))),member(rodinpos(grd3,internal_element3),identifier(none,magic_accel),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))),exists(rodinpos(grd4,internal_element4),[identifier(none,g1),identifier(none,g2)],conjunct(none,member(none,identifier(none,g1),set_extension(none,[identifier(none,new_xpos),identifier(none,new_xpos_max),identifier(none,new_xpos_min)])),conjunct(none,member(none,identifier(none,g2),set_extension(none,[identifier(none,new_xpos),identifier(none,new_xpos_max),identifier(none,new_xpos_min)])),greater(none,minus(none,function(none,identifier(none,g1),[couple(none,[couple(none,[function(none,identifier(none,xpos),[minus(none,identifier(none,d_vehicle),integer(none,1))]),function(none,identifier(none,speed),[minus(none,identifier(none,d_vehicle),integer(none,1))])]),function(none,identifier(none,accel),[minus(none,identifier(none,d_vehicle),integer(none,1))])])]),function(none,identifier(none,g2),[couple(none,[couple(none,[function(none,identifier(none,xpos),[identifier(none,d_vehicle)]),function(none,identifier(none,speed),[identifier(none,d_vehicle)])]),identifier(none,magic_accel)])])),identifier(none,'CRITICAL_DISTANCE')))))],[assign(rodinpos(act1,internal_element1),[identifier(none,d_vehicle)],[add(none,identifier(none,d_vehicle),integer(none,1))]),assign(rodinpos(act2,internal_element2),[identifier(none,accel)],[overwrite(none,identifier(none,accel),set_extension(none,[couple(none,[identifier(none,d_vehicle),identifier(none,magic_accel)])]))])],[]),event(rodinpos('move1_normal\11\',internal_evt2),move1_normal,[move1_normal],[identifier(rodinpos([],internal_element1),nspeed),identifier(rodinpos([],internal_element2),nxpos)],[equal(rodinpos(grd1,internal_grd1),identifier(none,vehicle),integer(none,1)),equal(rodinpos(grd2,internal_element3),identifier(none,d_vehicle),add(none,identifier(none,'VEHICLES'),integer(none,1))),equal(rodinpos(grd5,internal_element1),identifier(none,nspeed),function(none,identifier(none,new_speed),[couple(none,[function(none,identifier(none,speed),[identifier(none,vehicle)]),function(none,identifier(none,accel),[identifier(none,vehicle)])])])),member(rodinpos(grd4,internal_grd4),identifier(none,nspeed),interval(none,integer(none,0),identifier(none,'MAX_SPEED'))),equal(rodinpos(grd6,internal_element2),identifier(none,nxpos),function(none,identifier(none,new_xpos),[couple(none,[couple(none,[function(none,identifier(none,xpos),[identifier(none,vehicle)]),function(none,identifier(none,speed),[identifier(none,vehicle)])]),function(none,identifier(none,accel),[identifier(none,vehicle)])])]))],[assign(rodinpos(act3,internal_act3),[identifier(none,vehicle)],[add(none,identifier(none,vehicle),integer(none,1))]),assign(rodinpos(act1,internal_act1),[identifier(none,xpos)],[overwrite(none,identifier(none,xpos),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nxpos)])]))]),assign(rodinpos(act2,internal_act2),[identifier(none,speed)],[overwrite(none,identifier(none,speed),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nspeed)])]))])],[witness(none,identifier(none,magic_accel),equal(rodinpos(magic_accel,internal_element1),identifier(none,magic_accel),function(none,identifier(none,accel),[identifier(none,vehicle)])))]),event(rodinpos(move1_max,evt1),move1_max,[move1_max],[identifier(rodinpos([],internal_element2),nspeed),identifier(rodinpos([],internal_element1),nxpos)],[equal(rodinpos(grd1,internal_grd1),identifier(none,vehicle),integer(none,1)),equal(rodinpos(grd2,element0),identifier(none,d_vehicle),add(none,identifier(none,'VEHICLES'),integer(none,1))),equal(rodinpos(grd5,internal_element2),identifier(none,nspeed),function(none,identifier(none,new_speed),[couple(none,[function(none,identifier(none,speed),[identifier(none,vehicle)]),function(none,identifier(none,accel),[identifier(none,vehicle)])])])),greater(rodinpos(grd4,internal_grd4),identifier(none,nspeed),identifier(none,'MAX_SPEED')),equal(rodinpos(grd3,internal_element1),identifier(none,nxpos),function(none,identifier(none,new_xpos_max),[couple(none,[couple(none,[function(none,identifier(none,xpos),[identifier(none,vehicle)]),function(none,identifier(none,speed),[identifier(none,vehicle)])]),function(none,identifier(none,accel),[identifier(none,vehicle)])])]))],[assign(rodinpos(act3,internal_act3),[identifier(none,vehicle)],[add(none,identifier(none,vehicle),integer(none,1))]),assign(rodinpos(act1,internal_act1),[identifier(none,xpos)],[overwrite(none,identifier(none,xpos),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nxpos)])]))]),assign(rodinpos(act2,internal_act2),[identifier(none,speed)],[overwrite(none,identifier(none,speed),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,'MAX_SPEED')])]))])],[witness(none,identifier(none,magic_accel),equal(rodinpos(magic_accel,internal_element1),identifier(none,magic_accel),function(none,identifier(none,accel),[identifier(none,vehicle)])))]),event(rodinpos(move1_reduce,evt2),move1_reduce,[move1_reduce],[identifier(rodinpos([],internal_element2),nspeed),identifier(rodinpos([],internal_element1),nxpos)],[equal(rodinpos(grd1,internal_grd1),identifier(none,vehicle),integer(none,1)),equal(rodinpos(grd2,element0),identifier(none,d_vehicle),add(none,identifier(none,'VEHICLES'),integer(none,1))),equal(rodinpos(grd5,internal_element2),identifier(none,nspeed),function(none,identifier(none,new_speed),[couple(none,[function(none,identifier(none,speed),[identifier(none,vehicle)]),function(none,identifier(none,accel),[identifier(none,vehicle)])])])),less(rodinpos(grd3,internal_grd3),identifier(none,nspeed),integer(none,0)),equal(rodinpos(grd4,internal_element1),identifier(none,nxpos),function(none,identifier(none,new_xpos_min),[couple(none,[couple(none,[function(none,identifier(none,xpos),[identifier(none,vehicle)]),function(none,identifier(none,speed),[identifier(none,vehicle)])]),function(none,identifier(none,accel),[identifier(none,vehicle)])])]))],[assign(rodinpos(act3,internal_act3),[identifier(none,vehicle)],[add(none,identifier(none,vehicle),integer(none,1))]),assign(rodinpos(act1,internal_act1),[identifier(none,xpos)],[overwrite(none,identifier(none,xpos),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nxpos)])]))]),assign(rodinpos(act2,internal_act2),[identifier(none,speed)],[overwrite(none,identifier(none,speed),set_extension(none,[couple(none,[identifier(none,vehicle),integer(none,0)])]))])],[witness(none,identifier(none,magic_accel),equal(rodinpos(magic_accel,internal_element1),identifier(none,magic_accel),function(none,identifier(none,accel),[identifier(none,vehicle)])))]),event(rodinpos(move_normal,evt0),move_normal,[move_normal],[identifier(rodinpos([],internal_element1),nspeed),identifier(rodinpos([],internal_element2),nxpos)],[member(rodinpos(grd1,internal_grd1),identifier(none,vehicle),interval(none,integer(none,2),identifier(none,'VEHICLES'))),equal(rodinpos(grd2,element0),identifier(none,d_vehicle),add(none,identifier(none,'VEHICLES'),integer(none,1))),equal(rodinpos(grd3,internal_element1),identifier(none,nspeed),function(none,identifier(none,new_speed),[couple(none,[function(none,identifier(none,speed),[identifier(none,vehicle)]),function(none,identifier(none,accel),[identifier(none,vehicle)])])])),member(rodinpos(grd4,internal_grd4),identifier(none,nspeed),interval(none,integer(none,0),identifier(none,'MAX_SPEED'))),equal(rodinpos(grd7,internal_element2),identifier(none,nxpos),function(none,identifier(none,new_xpos),[couple(none,[couple(none,[function(none,identifier(none,xpos),[identifier(none,vehicle)]),function(none,identifier(none,speed),[identifier(none,vehicle)])]),function(none,identifier(none,accel),[identifier(none,vehicle)])])])),greater(rodinpos(grd6,internal_grd6),minus(none,function(none,identifier(none,xpos),[minus(none,identifier(none,vehicle),integer(none,1))]),identifier(none,nxpos)),identifier(none,'CRITICAL_DISTANCE'))],[assign(rodinpos(act2,internal_act2),[identifier(none,vehicle)],[add(none,identifier(none,vehicle),integer(none,1))]),assign(rodinpos(act1,internal_act1),[identifier(none,xpos)],[overwrite(none,identifier(none,xpos),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nxpos)])]))]),assign(rodinpos(act3,internal_element1),[identifier(none,speed)],[overwrite(none,identifier(none,speed),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nspeed)])]))])],[witness(none,identifier(none,magic_accel),equal(rodinpos(magic_accel,internal_element1),identifier(none,magic_accel),function(none,identifier(none,accel),[identifier(none,vehicle)])))]),event(rodinpos(move_max,evt3),move_max,[move_max],[identifier(rodinpos([],internal_element2),nspeed),identifier(rodinpos([],internal_element1),nxpos)],[member(rodinpos(grd1,internal_grd1),identifier(none,vehicle),interval(none,integer(none,2),identifier(none,'VEHICLES'))),equal(rodinpos(grd2,element0),identifier(none,d_vehicle),add(none,identifier(none,'VEHICLES'),integer(none,1))),equal(rodinpos(grd5,internal_element2),identifier(none,nspeed),function(none,identifier(none,new_speed),[couple(none,[function(none,identifier(none,speed),[identifier(none,vehicle)]),function(none,identifier(none,accel),[identifier(none,vehicle)])])])),greater(rodinpos(grd4,internal_grd4),identifier(none,nspeed),identifier(none,'MAX_SPEED')),equal(rodinpos(grd3,internal_element1),identifier(none,nxpos),function(none,identifier(none,new_xpos_max),[couple(none,[couple(none,[function(none,identifier(none,xpos),[identifier(none,vehicle)]),function(none,identifier(none,speed),[identifier(none,vehicle)])]),function(none,identifier(none,accel),[identifier(none,vehicle)])])])),greater(rodinpos(grd6,internal_grd6),minus(none,function(none,identifier(none,xpos),[minus(none,identifier(none,vehicle),integer(none,1))]),identifier(none,nxpos)),identifier(none,'CRITICAL_DISTANCE'))],[assign(rodinpos(act2,internal_act2),[identifier(none,vehicle)],[add(none,identifier(none,vehicle),integer(none,1))]),assign(rodinpos(act1,internal_act1),[identifier(none,xpos)],[overwrite(none,identifier(none,xpos),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nxpos)])]))]),assign(rodinpos(act3,internal_element1),[identifier(none,speed)],[overwrite(none,identifier(none,speed),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,'MAX_SPEED')])]))])],[witness(none,identifier(none,magic_accel),equal(rodinpos(magic_accel,internal_element1),identifier(none,magic_accel),function(none,identifier(none,accel),[identifier(none,vehicle)])))]),event(rodinpos(move_reduce,evt4),move_reduce,[move_reduce],[identifier(rodinpos([],internal_element2),nspeed),identifier(rodinpos([],internal_element1),nxpos)],[member(rodinpos(grd1,internal_grd1),identifier(none,vehicle),interval(none,integer(none,2),identifier(none,'VEHICLES'))),equal(rodinpos(grd2,element0),identifier(none,d_vehicle),add(none,identifier(none,'VEHICLES'),integer(none,1))),equal(rodinpos(grd5,internal_grd5),identifier(none,nspeed),function(none,identifier(none,new_speed),[couple(none,[function(none,identifier(none,speed),[identifier(none,vehicle)]),function(none,identifier(none,accel),[identifier(none,vehicle)])])])),less(rodinpos(grd4,internal_element2),identifier(none,nspeed),integer(none,0)),equal(rodinpos(grd3,internal_element1),identifier(none,nxpos),function(none,identifier(none,new_xpos_min),[couple(none,[couple(none,[function(none,identifier(none,xpos),[identifier(none,vehicle)]),function(none,identifier(none,speed),[identifier(none,vehicle)])]),function(none,identifier(none,accel),[identifier(none,vehicle)])])])),greater(rodinpos(grd6,internal_grd6),minus(none,function(none,identifier(none,xpos),[minus(none,identifier(none,vehicle),integer(none,1))]),identifier(none,nxpos)),identifier(none,'CRITICAL_DISTANCE'))],[assign(rodinpos(act2,internal_act2),[identifier(none,vehicle)],[add(none,identifier(none,vehicle),integer(none,1))]),assign(rodinpos(act1,internal_act1),[identifier(none,xpos)],[overwrite(none,identifier(none,xpos),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nxpos)])]))]),assign(rodinpos(act3,internal_element1),[identifier(none,speed)],[overwrite(none,identifier(none,speed),set_extension(none,[couple(none,[identifier(none,vehicle),integer(none,0)])]))])],[witness(none,identifier(none,magic_accel),equal(rodinpos(magic_accel,internal_element1),identifier(none,magic_accel),function(none,identifier(none,accel),[identifier(none,vehicle)])))]),event(rodinpos(all_moves,internal_evt3),all_moves,[all_moves],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,vehicle),add(none,identifier(none,'VEHICLES'),integer(none,1))),equal(rodinpos(grd2,element0),identifier(none,d_vehicle),add(none,identifier(none,'VEHICLES'),integer(none,1)))],[assign(rodinpos(act2,internal_act2),[identifier(none,xpos0)],[identifier(none,xpos)]),assign(rodinpos(act1,internal_act1),[identifier(none,vehicle)],[integer(none,1)]),assign(rodinpos(act3,element0),[identifier(none,d_vehicle)],[integer(none,1)])],[])])]),event_b_model(none,platoon_2,[sees(none,[context,context_1,context_2]),refines(none,platoon_1),variables(none,[identifier(none,speed),identifier(none,vehicle),identifier(none,xpos),identifier(none,xpos0)]),invariant(none,[member(rodinpos(inv1,internal_element1I),identifier(none,speed),total_function(none,interval(none,integer(none,1),identifier(none,'VEHICLES')),interval(none,integer(none,0),identifier(none,'MAX_SPEED'))))]),theorems(none,[]),events(none,[event(rodinpos('INITIALISATION',internal_evt1),'INITIALISATION',['INITIALISATION'],[],[],[assign(rodinpos(act1,internal_act1),[identifier(none,xpos0)],[identifier(none,initial_xpos)]),assign(rodinpos(act3,internal_act3),[identifier(none,xpos)],[identifier(none,initial_xpos)]),assign(rodinpos(act4,internal_act4),[identifier(none,vehicle)],[integer(none,1)]),assign(rodinpos(act2,internal_element1),[identifier(none,speed)],[identifier(none,initial_speed)])],[]),event(rodinpos('move1_normal\11\',internal_evt2),move1_normal,[move1],[identifier(rodinpos([],internal_var2),magic_accel),identifier(rodinpos([],internal_element1),nspeed),identifier(rodinpos([],internal_element2),nxpos)],[equal(rodinpos(grd1,internal_grd1),identifier(none,vehicle),integer(none,1)),member(rodinpos(grd2,internal_grd2),identifier(none,magic_accel),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))),equal(rodinpos(grd5,internal_element1),identifier(none,nspeed),function(none,identifier(none,new_speed),[couple(none,[function(none,identifier(none,speed),[identifier(none,vehicle)]),identifier(none,magic_accel)])])),member(rodinpos(grd4,internal_grd4),identifier(none,nspeed),interval(none,integer(none,0),identifier(none,'MAX_SPEED'))),equal(rodinpos(grd6,internal_element2),identifier(none,nxpos),function(none,identifier(none,new_xpos),[couple(none,[couple(none,[function(none,identifier(none,xpos),[identifier(none,vehicle)]),function(none,identifier(none,speed),[identifier(none,vehicle)])]),identifier(none,magic_accel)])]))],[assign(rodinpos(act3,internal_act3),[identifier(none,vehicle)],[add(none,identifier(none,vehicle),integer(none,1))]),assign(rodinpos(act1,internal_act1),[identifier(none,xpos)],[overwrite(none,identifier(none,xpos),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nxpos)])]))]),assign(rodinpos(act2,internal_act2),[identifier(none,speed)],[overwrite(none,identifier(none,speed),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nspeed)])]))])],[witness(none,identifier(none,magic_xpos_vehicle),equal(rodinpos(magic_xpos_vehicle,internal_wit1),identifier(none,magic_xpos_vehicle),identifier(none,nxpos)))]),event(rodinpos(move1_max,evt1),move1_max,[move1],[identifier(rodinpos([],internal_var2),magic_accel),identifier(rodinpos([],internal_element2),nspeed),identifier(rodinpos([],internal_element1),nxpos)],[equal(rodinpos(grd1,internal_grd1),identifier(none,vehicle),integer(none,1)),member(rodinpos(grd2,internal_grd2),identifier(none,magic_accel),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))),equal(rodinpos(grd5,internal_element2),identifier(none,nspeed),function(none,identifier(none,new_speed),[couple(none,[function(none,identifier(none,speed),[identifier(none,vehicle)]),identifier(none,magic_accel)])])),greater(rodinpos(grd4,internal_grd4),identifier(none,nspeed),identifier(none,'MAX_SPEED')),equal(rodinpos(grd3,internal_element1),identifier(none,nxpos),function(none,identifier(none,new_xpos_max),[couple(none,[couple(none,[function(none,identifier(none,xpos),[identifier(none,vehicle)]),function(none,identifier(none,speed),[identifier(none,vehicle)])]),identifier(none,magic_accel)])]))],[assign(rodinpos(act3,internal_act3),[identifier(none,vehicle)],[add(none,identifier(none,vehicle),integer(none,1))]),assign(rodinpos(act1,internal_act1),[identifier(none,xpos)],[overwrite(none,identifier(none,xpos),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nxpos)])]))]),assign(rodinpos(act2,internal_act2),[identifier(none,speed)],[overwrite(none,identifier(none,speed),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,'MAX_SPEED')])]))])],[witness(none,identifier(none,magic_xpos_vehicle),equal(rodinpos(magic_xpos_vehicle,internal_wit1),identifier(none,magic_xpos_vehicle),identifier(none,nxpos)))]),event(rodinpos(move1_reduce,evt2),move1_reduce,[move1],[identifier(rodinpos([],internal_var2),magic_accel),identifier(rodinpos([],internal_element2),nspeed),identifier(rodinpos([],internal_element1),nxpos)],[equal(rodinpos(grd1,internal_grd1),identifier(none,vehicle),integer(none,1)),member(rodinpos(grd2,internal_grd2),identifier(none,magic_accel),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))),equal(rodinpos(grd5,internal_element2),identifier(none,nspeed),function(none,identifier(none,new_speed),[couple(none,[function(none,identifier(none,speed),[identifier(none,vehicle)]),identifier(none,magic_accel)])])),less(rodinpos(grd3,internal_grd3),identifier(none,nspeed),integer(none,0)),equal(rodinpos(grd4,internal_element1),identifier(none,nxpos),function(none,identifier(none,new_xpos_min),[couple(none,[couple(none,[function(none,identifier(none,xpos),[identifier(none,vehicle)]),function(none,identifier(none,speed),[identifier(none,vehicle)])]),identifier(none,magic_accel)])]))],[assign(rodinpos(act3,internal_act3),[identifier(none,vehicle)],[add(none,identifier(none,vehicle),integer(none,1))]),assign(rodinpos(act1,internal_act1),[identifier(none,xpos)],[overwrite(none,identifier(none,xpos),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nxpos)])]))]),assign(rodinpos(act2,internal_act2),[identifier(none,speed)],[overwrite(none,identifier(none,speed),set_extension(none,[couple(none,[identifier(none,vehicle),integer(none,0)])]))])],[witness(none,identifier(none,magic_xpos_vehicle),equal(rodinpos(magic_xpos_vehicle,internal_wit1),identifier(none,magic_xpos_vehicle),identifier(none,nxpos)))]),event(rodinpos(move_normal,evt0),move_normal,[move],[identifier(rodinpos([],internal_var2),magic_accel),identifier(rodinpos([],internal_element1),nspeed),identifier(rodinpos([],internal_element2),nxpos)],[member(rodinpos(grd1,internal_grd1),identifier(none,vehicle),interval(none,integer(none,2),identifier(none,'VEHICLES'))),member(rodinpos(grd2,internal_grd2),identifier(none,magic_accel),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))),equal(rodinpos(grd3,internal_element1),identifier(none,nspeed),function(none,identifier(none,new_speed),[couple(none,[function(none,identifier(none,speed),[identifier(none,vehicle)]),identifier(none,magic_accel)])])),member(rodinpos(grd4,internal_grd4),identifier(none,nspeed),interval(none,integer(none,0),identifier(none,'MAX_SPEED'))),equal(rodinpos(grd7,internal_element2),identifier(none,nxpos),function(none,identifier(none,new_xpos),[couple(none,[couple(none,[function(none,identifier(none,xpos),[identifier(none,vehicle)]),function(none,identifier(none,speed),[identifier(none,vehicle)])]),identifier(none,magic_accel)])])),greater(rodinpos(grd6,internal_grd6),minus(none,function(none,identifier(none,xpos),[minus(none,identifier(none,vehicle),integer(none,1))]),identifier(none,nxpos)),identifier(none,'CRITICAL_DISTANCE'))],[assign(rodinpos(act2,internal_act2),[identifier(none,vehicle)],[add(none,identifier(none,vehicle),integer(none,1))]),assign(rodinpos(act1,internal_act1),[identifier(none,xpos)],[overwrite(none,identifier(none,xpos),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nxpos)])]))]),assign(rodinpos(act3,internal_element1),[identifier(none,speed)],[overwrite(none,identifier(none,speed),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nspeed)])]))])],[witness(none,identifier(none,magic_xpos_vehicle),equal(rodinpos(magic_xpos_vehicle,internal_wit1),identifier(none,magic_xpos_vehicle),identifier(none,nxpos)))]),event(rodinpos(move_max,evt3),move_max,[move],[identifier(rodinpos([],internal_var2),magic_accel),identifier(rodinpos([],internal_element2),nspeed),identifier(rodinpos([],internal_element1),nxpos)],[member(rodinpos(grd1,internal_grd1),identifier(none,vehicle),interval(none,integer(none,2),identifier(none,'VEHICLES'))),member(rodinpos(grd2,internal_grd2),identifier(none,magic_accel),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))),equal(rodinpos(grd5,internal_element2),identifier(none,nspeed),function(none,identifier(none,new_speed),[couple(none,[function(none,identifier(none,speed),[identifier(none,vehicle)]),identifier(none,magic_accel)])])),greater(rodinpos(grd4,internal_grd4),identifier(none,nspeed),identifier(none,'MAX_SPEED')),equal(rodinpos(grd3,internal_element1),identifier(none,nxpos),function(none,identifier(none,new_xpos_max),[couple(none,[couple(none,[function(none,identifier(none,xpos),[identifier(none,vehicle)]),function(none,identifier(none,speed),[identifier(none,vehicle)])]),identifier(none,magic_accel)])])),greater(rodinpos(grd6,internal_grd6),minus(none,function(none,identifier(none,xpos),[minus(none,identifier(none,vehicle),integer(none,1))]),identifier(none,nxpos)),identifier(none,'CRITICAL_DISTANCE'))],[assign(rodinpos(act2,internal_act2),[identifier(none,vehicle)],[add(none,identifier(none,vehicle),integer(none,1))]),assign(rodinpos(act1,internal_act1),[identifier(none,xpos)],[overwrite(none,identifier(none,xpos),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nxpos)])]))]),assign(rodinpos(act3,internal_element1),[identifier(none,speed)],[overwrite(none,identifier(none,speed),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,'MAX_SPEED')])]))])],[witness(none,identifier(none,magic_xpos_vehicle),equal(rodinpos(magic_xpos_vehicle,internal_wit1),identifier(none,magic_xpos_vehicle),identifier(none,nxpos)))]),event(rodinpos(move_reduce,evt4),move_reduce,[move],[identifier(rodinpos([],internal_var2),magic_accel),identifier(rodinpos([],internal_element2),nspeed),identifier(rodinpos([],internal_element1),nxpos)],[member(rodinpos(grd1,internal_grd1),identifier(none,vehicle),interval(none,integer(none,2),identifier(none,'VEHICLES'))),member(rodinpos(grd2,internal_grd2),identifier(none,magic_accel),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))),equal(rodinpos(grd5,internal_grd5),identifier(none,nspeed),function(none,identifier(none,new_speed),[couple(none,[function(none,identifier(none,speed),[identifier(none,vehicle)]),identifier(none,magic_accel)])])),less(rodinpos(grd4,internal_element2),identifier(none,nspeed),integer(none,0)),equal(rodinpos(grd3,internal_element1),identifier(none,nxpos),function(none,identifier(none,new_xpos_min),[couple(none,[couple(none,[function(none,identifier(none,xpos),[identifier(none,vehicle)]),function(none,identifier(none,speed),[identifier(none,vehicle)])]),identifier(none,magic_accel)])])),greater(rodinpos(grd6,internal_grd6),minus(none,function(none,identifier(none,xpos),[minus(none,identifier(none,vehicle),integer(none,1))]),identifier(none,nxpos)),identifier(none,'CRITICAL_DISTANCE'))],[assign(rodinpos(act2,internal_act2),[identifier(none,vehicle)],[add(none,identifier(none,vehicle),integer(none,1))]),assign(rodinpos(act1,internal_act1),[identifier(none,xpos)],[overwrite(none,identifier(none,xpos),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,nxpos)])]))]),assign(rodinpos(act3,internal_element1),[identifier(none,speed)],[overwrite(none,identifier(none,speed),set_extension(none,[couple(none,[identifier(none,vehicle),integer(none,0)])]))])],[witness(none,identifier(none,magic_xpos_vehicle),equal(rodinpos(magic_xpos_vehicle,internal_wit1),identifier(none,magic_xpos_vehicle),identifier(none,nxpos)))]),event(rodinpos(all_moves,internal_evt3),all_moves,[all_moves],[],[equal(rodinpos(grd1,internal_grd1),identifier(none,vehicle),add(none,identifier(none,'VEHICLES'),integer(none,1)))],[assign(rodinpos(act2,internal_act2),[identifier(none,xpos0)],[identifier(none,xpos)]),assign(rodinpos(act1,internal_act1),[identifier(none,vehicle)],[integer(none,1)])],[])])]),event_b_model(none,platoon_1,[sees(none,[context]),refines(none,platoon),variables(none,[identifier(none,vehicle),identifier(none,xpos),identifier(none,xpos0)]),invariant(none,[member(rodinpos(inv2,internal_inv2I),identifier(none,xpos),total_function(none,interval(none,integer(none,1),identifier(none,'VEHICLES')),natural_set(none))),member(rodinpos(inv3,internal_inv3I),identifier(none,vehicle),interval(none,integer(none,1),add(none,identifier(none,'VEHICLES'),integer(none,1)))),forall(rodinpos(inv1,internal_inv1I),[identifier(none,v)],implication(none,member(none,identifier(none,v),interval(none,integer(none,2),minus(none,identifier(none,vehicle),integer(none,1)))),greater(none,minus(none,function(none,identifier(none,xpos),[minus(none,identifier(none,v),integer(none,1))]),function(none,identifier(none,xpos),[identifier(none,v)])),identifier(none,'CRITICAL_DISTANCE'))))]),theorems(none,[]),variant(none,minus(none,add(none,identifier(none,'VEHICLES'),integer(none,1)),identifier(none,vehicle))),events(none,[event(rodinpos('INITIALISATION',internal_evt1),'INITIALISATION',['INITIALISATION'],[],[],[assign(rodinpos(act1,internal_act1),[identifier(none,xpos0)],[identifier(none,initial_xpos)]),assign(rodinpos(act4,internal_act4),[identifier(none,vehicle)],[integer(none,1)]),assign(rodinpos(act2,internal_element1),[identifier(none,xpos)],[identifier(none,initial_xpos)])],[]),event(rodinpos(move1,internal_evt2),move1,[],[identifier(rodinpos([],internal_var2),magic_xpos_vehicle)],[equal(rodinpos(grd1,internal_grd1),identifier(none,vehicle),integer(none,1)),member(rodinpos(grd2,internal_grd2),identifier(none,magic_xpos_vehicle),natural_set(none)),greater_equal(rodinpos(grd4,internal_grd4),identifier(none,magic_xpos_vehicle),function(none,identifier(none,xpos),[identifier(none,vehicle)]))],[assign(rodinpos(act1,internal_act1),[identifier(none,xpos)],[overwrite(none,identifier(none,xpos),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,magic_xpos_vehicle)])]))]),assign(rodinpos(act3,internal_act3),[identifier(none,vehicle)],[add(none,identifier(none,vehicle),integer(none,1))])],[]),event(rodinpos(move,evt0),move,[],[identifier(rodinpos([],internal_var2),magic_xpos_vehicle)],[member(rodinpos(grd1,internal_grd1),identifier(none,vehicle),interval(none,integer(none,2),identifier(none,'VEHICLES'))),member(rodinpos(grd2,internal_grd2),identifier(none,magic_xpos_vehicle),natural_set(none)),greater_equal(rodinpos(grd4,internal_grd4),identifier(none,magic_xpos_vehicle),function(none,identifier(none,xpos),[identifier(none,vehicle)])),greater(rodinpos(grd5,internal_grd5),minus(none,function(none,identifier(none,xpos),[minus(none,identifier(none,vehicle),integer(none,1))]),identifier(none,magic_xpos_vehicle)),identifier(none,'CRITICAL_DISTANCE'))],[assign(rodinpos(act1,internal_act1),[identifier(none,xpos)],[overwrite(none,identifier(none,xpos),set_extension(none,[couple(none,[identifier(none,vehicle),identifier(none,magic_xpos_vehicle)])]))]),assign(rodinpos(act2,internal_act2),[identifier(none,vehicle)],[add(none,identifier(none,vehicle),integer(none,1))])],[]),event(rodinpos(all_moves,internal_evt3),all_moves,[all_moves],[],[equal(rodinpos(grd1,internal_element2),identifier(none,vehicle),add(none,identifier(none,'VEHICLES'),integer(none,1)))],[assign(rodinpos(act2,internal_element1),[identifier(none,xpos0)],[identifier(none,xpos)]),assign(rodinpos(act1,internal_act1),[identifier(none,vehicle)],[integer(none,1)])],[witness(none,identifier(none,magic_xpos),equal(rodinpos(magic_xpos,internal_element1),identifier(none,magic_xpos),identifier(none,xpos)))])])]),event_b_model(none,platoon,[sees(none,[context]),variables(none,[identifier(none,xpos0)]),invariant(none,[member(rodinpos(inv1,internal_inv1I),identifier(none,xpos0),total_function(none,interval(none,integer(none,1),identifier(none,'VEHICLES')),natural_set(none))),forall(rodinpos(inv3,internal_inv3I),[identifier(none,v)],implication(none,member(none,identifier(none,v),interval(none,integer(none,2),identifier(none,'VEHICLES'))),greater(none,minus(none,function(none,identifier(none,xpos0),[minus(none,identifier(none,v),integer(none,1))]),function(none,identifier(none,xpos0),[identifier(none,v)])),identifier(none,'CRITICAL_DISTANCE'))))]),theorems(none,[]),events(none,[event(rodinpos('INITIALISATION',internal_evt1),'INITIALISATION',[],[],[],[assign(rodinpos(act1,internal_act1),[identifier(none,xpos0)],[identifier(none,initial_xpos)])],[]),event(rodinpos(all_moves,internal_evt3),all_moves,[],[identifier(rodinpos([],internal_element1),magic_xpos)],[member(rodinpos(grd1,internal_element1),identifier(none,magic_xpos),total_function(none,interval(none,integer(none,1),identifier(none,'VEHICLES')),natural_set(none))),forall(rodinpos(grd2,internal_element2),[identifier(none,v)],implication(none,member(none,identifier(none,v),interval(none,integer(none,2),identifier(none,'VEHICLES'))),greater(none,minus(none,function(none,identifier(none,magic_xpos),[minus(none,identifier(none,v),integer(none,1))]),function(none,identifier(none,magic_xpos),[identifier(none,v)])),identifier(none,'CRITICAL_DISTANCE'))))],[assign(rodinpos(act1,internal_element1),[identifier(none,xpos0)],[identifier(none,magic_xpos)])],[])])])],[event_b_context(none,context,[extends(none,[]),constants(none,[identifier(none,'CRITICAL_DISTANCE'),identifier(none,'VEHICLES'),identifier(none,initial_xpos)]),axioms(none,[member(rodinpos(axm1,internal_axm1A),identifier(none,'VEHICLES'),natural1_set(none)),greater_equal(rodinpos(axm2,internal_axm2A),identifier(none,'VEHICLES'),integer(none,2)),member(rodinpos(axm7,internal_axm6A),identifier(none,'CRITICAL_DISTANCE'),natural1_set(none)),member(rodinpos(axm3,internal_axm3A),identifier(none,initial_xpos),total_function(none,interval(none,integer(none,1),identifier(none,'VEHICLES')),natural_set(none))),forall(rodinpos(axm4,internal_element1A),[identifier(none,v)],implication(none,member(none,identifier(none,v),interval(none,integer(none,1),identifier(none,'VEHICLES'))),equal(none,function(none,identifier(none,initial_xpos),[identifier(none,v)]),multiplication(none,minus(none,identifier(none,'VEHICLES'),identifier(none,v)),add(none,identifier(none,'CRITICAL_DISTANCE'),integer(none,1))))))]),theorems(none,[]),sets(none,[])]),event_b_context(none,context_1,[extends(none,[context]),constants(none,[]),axioms(none,[]),theorems(none,[]),sets(none,[])]),event_b_context(none,context_2,[extends(none,[context_1]),constants(none,[identifier(none,'MAX_ACCEL'),identifier(none,'MAX_SPEED'),identifier(none,'MIN_ACCEL'),identifier(none,initial_speed),identifier(none,new_speed),identifier(none,new_xpos),identifier(none,new_xpos_max),identifier(none,new_xpos_min)]),axioms(none,[member(rodinpos(axm1,internal_element1A),identifier(none,'MAX_SPEED'),natural1_set(none)),member(rodinpos(axm3,internal_element3A),identifier(none,'MAX_ACCEL'),natural1_set(none)),member(rodinpos(axm4,internal_element4A),identifier(none,'MIN_ACCEL'),integer_set(none)),less(rodinpos(axm5,internal_element5A),identifier(none,'MIN_ACCEL'),integer(none,0)),member(rodinpos(axm61,internal_element6A),identifier(none,initial_speed),total_function(none,interval(none,integer(none,1),identifier(none,'VEHICLES')),interval(none,integer(none,0),identifier(none,'MAX_SPEED')))),forall(rodinpos(axm62,internal_element10A),[identifier(none,vehi0)],implication(none,member(none,identifier(none,vehi0),interval(none,integer(none,1),identifier(none,'VEHICLES'))),exists(none,[identifier(none,speed0)],conjunct(none,member(none,identifier(none,speed0),interval(none,integer(none,0),identifier(none,'MAX_SPEED'))),equal(none,function(none,identifier(none,initial_speed),[identifier(none,vehi0)]),identifier(none,speed0)))))),member(rodinpos(axm2,internal_element2A),identifier(none,new_speed),total_function(none,cartesian_product(none,interval(none,integer(none,0),identifier(none,'MAX_SPEED')),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))),integer_set(none))),forall(rodinpos(axm22,element1A),[identifier(none,speed1),identifier(none,accel1)],implication(none,conjunct(none,member(none,identifier(none,speed1),interval(none,integer(none,0),identifier(none,'MAX_SPEED'))),member(none,identifier(none,accel1),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL')))),equal(none,function(none,identifier(none,new_speed),[couple(none,[identifier(none,speed1),identifier(none,accel1)])]),add(none,identifier(none,speed1),identifier(none,accel1))))),member(rodinpos(axm71,element0A),identifier(none,new_xpos),total_function(none,cartesian_product(none,cartesian_product(none,natural_set(none),interval(none,integer(none,0),identifier(none,'MAX_SPEED'))),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))),natural_set(none))),forall(rodinpos(axm72,internal_element7A),[identifier(none,xpos0),identifier(none,speed0),identifier(none,accel0)],implication(none,conjunct(none,member(none,identifier(none,xpos0),natural_set(none)),conjunct(none,member(none,identifier(none,speed0),interval(none,integer(none,0),identifier(none,'MAX_SPEED'))),member(none,identifier(none,accel0),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))))),equal(none,function(none,identifier(none,new_xpos),[couple(none,[couple(none,[identifier(none,xpos0),identifier(none,speed0)]),identifier(none,accel0)])]),add(none,identifier(none,xpos0),add(none,identifier(none,speed0),div(none,identifier(none,accel0),integer(none,2))))))),member(rodinpos(axm81,element3A),identifier(none,new_xpos_max),total_function(none,cartesian_product(none,cartesian_product(none,natural_set(none),interval(none,integer(none,0),identifier(none,'MAX_SPEED'))),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))),natural_set(none))),forall(rodinpos(axm82,internal_element8A),[identifier(none,xpos0),identifier(none,speed0),identifier(none,accel0)],implication(none,conjunct(none,member(none,identifier(none,xpos0),natural_set(none)),conjunct(none,member(none,identifier(none,speed0),interval(none,integer(none,0),identifier(none,'MAX_SPEED'))),member(none,identifier(none,accel0),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))))),conjunct(none,implication(none,equal(none,identifier(none,accel0),integer(none,0)),equal(none,function(none,identifier(none,new_xpos_max),[couple(none,[couple(none,[identifier(none,xpos0),identifier(none,speed0)]),identifier(none,accel0)])]),add(none,identifier(none,xpos0),identifier(none,'MAX_SPEED')))),implication(none,not_equal(none,identifier(none,accel0),integer(none,0)),equal(none,function(none,identifier(none,new_xpos_max),[couple(none,[couple(none,[identifier(none,xpos0),identifier(none,speed0)]),identifier(none,accel0)])]),minus(none,add(none,identifier(none,xpos0),identifier(none,'MAX_SPEED')),div(none,multiplication(none,minus(none,identifier(none,'MAX_SPEED'),identifier(none,speed0)),minus(none,identifier(none,'MAX_SPEED'),identifier(none,speed0))),multiplication(none,integer(none,2),identifier(none,accel0))))))))),member(rodinpos(axm91,element4A),identifier(none,new_xpos_min),total_function(none,cartesian_product(none,cartesian_product(none,natural_set(none),interval(none,integer(none,0),identifier(none,'MAX_SPEED'))),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))),natural_set(none))),forall(rodinpos(axm92,internal_element9A),[identifier(none,xpos0),identifier(none,speed0),identifier(none,accel0)],implication(none,conjunct(none,member(none,identifier(none,xpos0),natural_set(none)),conjunct(none,member(none,identifier(none,speed0),interval(none,integer(none,0),identifier(none,'MAX_SPEED'))),member(none,identifier(none,accel0),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))))),conjunct(none,implication(none,equal(none,identifier(none,accel0),integer(none,0)),equal(none,function(none,identifier(none,new_xpos_min),[couple(none,[couple(none,[identifier(none,xpos0),identifier(none,speed0)]),identifier(none,accel0)])]),identifier(none,xpos0))),implication(none,not_equal(none,identifier(none,accel0),integer(none,0)),equal(none,function(none,identifier(none,new_xpos_min),[couple(none,[couple(none,[identifier(none,xpos0),identifier(none,speed0)]),identifier(none,accel0)])]),minus(none,identifier(none,xpos0),div(none,multiplication(none,identifier(none,speed0),identifier(none,speed0)),multiplication(none,integer(none,2),identifier(none,accel0)))))))))]),theorems(none,[]),sets(none,[])]),event_b_context(none,context_3,[extends(none,[context_2]),constants(none,[identifier(none,initial_accel)]),axioms(none,[member(rodinpos(axm61,element1A),identifier(none,initial_accel),total_function(none,interval(none,integer(none,1),identifier(none,'VEHICLES')),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL')))),forall(rodinpos(axm62,element0A),[identifier(none,vehi0)],implication(none,member(none,identifier(none,vehi0),interval(none,integer(none,1),identifier(none,'VEHICLES'))),exists(none,[identifier(none,accel0)],conjunct(none,member(none,identifier(none,accel0),interval(none,identifier(none,'MIN_ACCEL'),identifier(none,'MAX_ACCEL'))),equal(none,function(none,identifier(none,initial_accel),[identifier(none,vehi0)]),identifier(none,accel0))))))]),theorems(none,[]),sets(none,[])])],[discharged(platoon_3_0,'INITIALISATION',inv1),discharged(platoon_3_0,'INITIALISATION',inv2),discharged(platoon_3_0,'INITIALISATION',inv7),discharged(platoon_3_0,decide1,inv1),discharged(platoon_3_0,decide1,inv2),discharged(platoon_3_0,decide1,inv7),discharged(platoon_3_0,decide,inv1),discharged(platoon_3_0,decide,inv2),discharged(platoon_3_0,'move1_normal\11\',inv7),discharged(platoon_3_0,move1_max,inv7),discharged(platoon_3_0,move1_reduce,inv7),discharged(platoon_3_0,move_normal,inv7),discharged(platoon_3_0,move_max,inv7),discharged(platoon_3_0,move_reduce,inv7),discharged(platoon_3_0,all_moves,inv1),discharged(platoon_3_0,all_moves,inv7),discharged(platoon_2,'INITIALISATION',inv1),discharged(platoon_2,'move1_normal\11\',inv1),discharged(platoon_2,move1_max,inv1),discharged(platoon_2,move1_reduce,inv1),discharged(platoon_2,move_normal,inv1),discharged(platoon_2,move_max,inv1),discharged(platoon_2,move_reduce,inv1),discharged(platoon_1,'INITIALISATION',inv2),discharged(platoon_1,'INITIALISATION',inv3),discharged(platoon_1,'INITIALISATION',inv1),discharged(platoon_1,move1,inv2),discharged(platoon_1,move1,inv3),discharged(platoon_1,move1,inv1),discharged(platoon_1,move,inv2),discharged(platoon_1,move,inv3),discharged(platoon_1,move,inv1),discharged(platoon_1,all_moves,inv3),discharged(platoon_1,all_moves,inv1),discharged(platoon,'INITIALISATION',inv1),discharged(platoon,'INITIALISATION',inv3),discharged(platoon,all_moves,inv1),discharged(platoon,all_moves,inv3)],Error)).