variable [ x1 x2 x3 v1 v2 v3 a1 a2 a3 t br ac r2 r3] propsteps(2) location l0 x1=100 x2=50 x3=0 v1=15 v2 = 5 v3=10 br +1 =0 ac -1=0 a1=0 a2=0 a3=0 t=0 r2=0 r3=0 invariant l0: r2 >=0 r3 >=0 r2 <= 5 r3 <= 5 #time step is 1 seconds # let us assume that things are # normalized to this time step transition telapse1: l0, br+1=0 ac -1=0 x1 -x2 >=30 x2 - x3 >=30 r2=0 r3=0 v1 >=0 v2 >=0 v3 >=0 'x1- x1 - v1 =0 'x2- x2 - v2 =0 'x3- x3 - v3 =0 'v1-v1-a1=0 'v2-v2-a2=0 'v3-v3-a3=0 't-t-1=0 preserve[a1,a2,a3,br,ac,r2,r3] transition telapse2: l0, br+1=0 ac -1=0 x1 -x2 >=30 x2 - x3 >=0 x2-x3 <= 30 r2 =0 v1 >=0 v2 >=0 v3 >=0 'x1- x1 - v1 =0 'x2- x2 - v2 =0 'x3- x3 - v3 =0 'v1-v1-a1=0 'v2-v2-a2=0 'v3-v3-a3=0 't-t-1=0 'r3-r3-1=0 preserve[a1,a2,a3,br,ac,r2] transition telapse3: l0, br+1=0 ac -1=0 x2 - x3 >= 30 x1 - x2 >= 0 x1 - x2 <= 30 r3 = 0 v1 >=0 v2 >=0 v3 >=0 'x1 - x1 - v1 = 0 'x2 - x2 - v2 = 0 'x3 - x3 - v3 = 0 'v1-v1-a1=0 'v2-v2-a2=0 'v3-v3-a3=0 't-t-1=0 'r2-r2-1=0 preserve[a1,a2,a3,br,ac,r3] transition telapse4: l0, br+1=0 ac -1=0 x2 - x3 >= 0 x2 - x3 <= 30 x1 - x2 >= 0 x1 - x2 <= 30 v1 >=0 v2 >=0 v3 >=0 'x1 - x1 - v1 =0 'x2 - x2 - v2 =0 'x3 - x3 - v3 =0 'v1-v1-a1=0 'v2-v2-a2=0 'v3-v3-a3=0 't-t-1=0 'r2-r2-1=0 'r3-r3-1=0 preserve[a1,a2,a3,br,ac] #lead car transitions # it can decide to do anything quirky # like set its acceleration to anywhere between # br and ac transition tlead: l0, br +1 =0 ac -1=0 x1 -x2 >=0 x2 - x3 >=0 v1 >=0 v2 >=0 v3 >=0 ac -br >=0 'a1 - ac <=0 'a1 - br >=0 preserve[x1,x2,x3,v1,v2,v3,a2,a3,t,br,ac,r2,r3] #car 2 senses the position of x1 and breaks if it is too close transition t1: l0, br +1 =0 ac -1=0 x1 - x2 >=0 x2 - x3 >=0 v1 >=0 v2 >=0 v3 >=0 x1 -x2 <= 30 'a2 <=0 'a2 -br >= 0 'a2 -a1 <=0 'r2=0 preserve[x1,x2,x3,v1,v2,v3,a1,a3,t,br,ac,r3] #car 2 senses the position of x1 and accelerates if it is too far transition t2: l0, br +1 =0 ac -1=0 x1 -x2 >=0 x2 - x3 >=0 v1 >=0 v2 >=0 v3 >=0 x1 -x2 >= 50 'a2 >=0 'a2 -ac <=0 'a2 - a1 >=0 preserve[x1,x2,x3,v1,v2,v3,a1,a3,t,br,ac,r2,r3] #If in optimal range, car 2 will just coast transition t5: l0, br +1 =0 ac -1=0 x1 -x2 >=0 x2 - x3 >=0 v1 >=0 v2 >=0 v3 >=0 x1 -x2 >= 30 x1 -x2 <= 50 'a2 =0 preserve[x1,x2,x3,v1,v2,v3,a1,a3,t,br,ac,r2,r3] #car 3 senses the position of car 2 and does some adjustments to its # position transition t3: l0, br +1 =0 ac -1=0 x1 -x2 >=0 x2 - x3 >=0 v1 >=0 v2 >=0 v3 >=0 x2 - x3 <= 30 'a3 <=0 'a3 -br >= 0 'a3 - a2 <=0 'r3=0 preserve[x1,x2,x3,v1,v2,v3,a1,a2,t,br,ac,r2] transition t4: l0, br +1 =0 ac -1=0 x1 -x2 >=0 x2 - x3 >=0 v1 >=0 v2 >=0 v3 >=0 x2 - x3 >= 50 'a3 >=0 'a3 -ac <= 0 'a3 -a2 >=0 preserve[x1,x2,x3,v1,v2,v3,a1,a2,t,br,ac,r2,r3] transition t6: l0, br +1 =0 ac -1=0 x1 -x2 >=0 x2 - x3 >=0 v1 >=0 v2 >=0 v3 >=0 x2 -x3 >= 30 x2 - x3 <= 50 'a3 =0 preserve[x1,x2,x3,v1,v2,v3,a1,a2,t,br,ac,r2,r3] end