variable [ x1 x2 x3 x4 x5 v1 v2 v3 v4 v5 a1 a2 a3 a4 a5 t br ac r2 r3 r4 r5]

propsteps(1)

location l0
	x1=100
	x2=50
	x3=0
	x4+50=0
	x5+100=0

	v1=15
	v2 = 5
	v3=10
	v4=15
	v5=10

	br +1 =0
	ac -1=0

	a1=0
	a2=0	
	a3=0
	a4=0
	a5=0

	r2=0
	r3=0
	r4=0
	r5=0
	t=0

invariant l0:
	r2 >=0
	r2 -5 <=0
	r3 >=0
	r3 - 5 <=0
	r4 >=0
	r4 - 5<=0
	r5 >=0
	r5 -5 <=0


#time step is 1 seconds
# let us assume that things are 
# normalized to this time step


#time step is 1 seconds
# let us assume that things are 
# normalized to this time step

transition telapse111: l0,

        br+1=0
	ac -1=0

	x1 -x2 >=30
	x2 - x3 >=30

        r2=0
	r3=0

	x3 -x4 >= 30
	r4=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
	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0
	
	
	r5=0
	x4-x5 >= 30

	't-t-1=0

	preserve[a1,a2,a3,br,ac,r2,r3,r4,r5]


transition telapse121: l0,


        br+1=0
	ac -1=0

	x1 -x2 >=30

	x2 - x3 >=0
	x2-x3 <= 30        
	
	x3 -x4 >= 30
	r4=0

	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
		
	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0


	't-t-1=0

	'r3-r3-1=0

		r5=0
	x4-x5 >= 30

	preserve[a1,a2,a3,br,ac,r2,r4,r5]

transition telapse131: l0,


        br+1=0
	ac -1=0

	x2 - x3 >= 30

	x1 - x2 >= 0
	x1 - x2 <= 30        
	r3 = 0

	x3 -x4 >= 30
	r4=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
	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0

	
		r5=0
	x4-x5 >= 30
		
	't-t-1=0
	'r2-r2-1=0

	preserve[a1,a2,a3,br,ac,r3,r4,r5]

transition telapse141: l0,

        br+1=0
	ac -1=0
	
	x2 - x3 >= 0
	x2 - x3 <= 30
	x1 - x2 >= 0
	x1 - x2 <= 30        
	
	x3 -x4 >= 30
	r4=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
	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0

		
	't-t-1=0

	'r2-r2-1=0
	'r3-r3-1=0

	r5=0
	x4-x5 >= 30

	preserve[a1,a2,a3,br,ac,r4,r5]



transition telapse211: l0,

        br+1=0
	ac -1=0

	x1 -x2 >=30
	x2 - x3 >=30

	x3 -x4 >= 0
	x3-x4 <=30
	'r4-r4-1=0

	r4=0
        r2=0
	r3=0

	v1 >=0
	v2 >=0
	v3 >=0
	
	'x1-  x1 - v1  =0
	'x2-  x2 -  v2  =0
	'x3-  x3 -  v3 =0
	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0

	
	'v1-v1-a1=0
	'v2-v2-a2=0
	'v3-v3-a3=0
		
	't-t-1=0

	r5=0
	x4-x5 >= 30


	preserve[a1,a2,a3,br,ac,r2,r3,r5]


transition telapse221: 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

	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0
		
	
	x3 -x4 >= 0
	x3-x4 <=30
	'r4-r4-1=0

	't-t-1=0

	'r3-r3-1=0

	r5=0
	x4-x5 >= 30


	preserve[a1,a2,a3,br,ac,r2,r5]

transition telapse231: 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
	
	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0

	
	x3 -x4 >= 0
	x3-x4 <=30
	'r4-r4-1=0
	
	
	't-t-1=0
	'r2-r2-1=0

	r5=0
	x4-x5 >= 30

	preserve[a1,a2,a3,br,ac,r3,r5]

transition telapse241: 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
		
	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0
	

	x3 -x4 >= 0
	x3-x4 <=30
	'r4-r4-1=0

	't-t-1=0

	'r2-r2-1=0
	'r3-r3-1=0

	r5=0
	x4-x5 >= 30

	preserve[a1,a2,a3,br,ac,r5]



transition telapse112: l0,

        br+1=0
	ac -1=0

	x1 -x2 >=30
	x2 - x3 >=30

        r2=0
	r3=0

	x3 -x4 >= 30
	r4=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
		
	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0

	't-t-1=0

	x4 -x5 >=0
	x4 -x5 <=30
	'r5-r5-1=0

	preserve[a1,a2,a3,br,ac,r2,r3,r4]


transition telapse122: l0,


        br+1=0
	ac -1=0

	x1 -x2 >=30

	x2 - x3 >=0
	x2-x3 <= 30        
	
	x3 -x4 >= 30
	r4=0

	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

	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0

	'r3-r3-1=0
	x4 -x5 >=0
	x4 -x5 <=30
	'r5-r5-1=0

	preserve[a1,a2,a3,br,ac,r2,r4]

transition telapse132: l0,


        br+1=0
	ac -1=0

	x2 - x3 >= 30

	x1 - x2 >= 0
	x1 - x2 <= 30        
	r3 = 0

	x3 -x4 >= 30
	r4=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
	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0
		

	't-t-1=0
	'r2-r2-1=0
	
		x4 -x5 >=0
	x4 -x5 <=30
	'r5-r5-1=0


	preserve[a1,a2,a3,br,ac,r3,r4]

transition telapse142: l0,

        br+1=0
	ac -1=0
	
	x2 - x3 >= 0
	x2 - x3 <= 30
	x1 - x2 >= 0
	x1 - x2 <= 30        
	
	x3 -x4 >= 30
	r4=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
		
	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0


	't-t-1=0

	'r2-r2-1=0
	'r3-r3-1=0

		x4 -x5 >=0
	x4 -x5 <=30
	'r5-r5-1=0

	preserve[a1,a2,a3,br,ac,r4]



transition telapse212: l0,

        br+1=0
	ac -1=0

	x1 -x2 >=30
	x2 - x3 >=30

	x3 -x4 >= 0
	x3-x4 <=30
	'r4-r4-1=0

	r4=0
        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
	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0
		

	't-t-1=0

		x4 -x5 >=0
	x4 -x5 <=30
	'r5-r5-1=0


	preserve[a1,a2,a3,br,ac,r2,r3]


transition telapse222: 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
		
	
	x3 -x4 >= 0
	x3-x4 <=30
	'r4-r4-1=0
	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0


	't-t-1=0

	'r3-r3-1=0
	
		x4 -x5 >=0
	x4 -x5 <=30
	'r5-r5-1=0


	preserve[a1,a2,a3,br,ac,r2]

transition telapse232: 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
	
	
	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=0


	x3 -x4 >= 0
	x3-x4 <=30
	'r4-r4-1=0
	
		x4 -x5 >=0
	x4 -x5 <=30
	'r5-r5-1=0
	

	't-t-1=0
	'r2-r2-1=0

	preserve[a1,a2,a3,br,ac,r3]

transition telapse242: 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
		
		x4 -x5 >=0
	x4 -x5 <=30
	'r5-r5-1=0
	

	x3 -x4 >= 0
	x3-x4 <=30
	'r4-r4-1=0
	
	'x4-x4-v4=0
	'v4-v4-a4=0
	'a4-a4=0
	
	'x5-x5-v5=0
	'v5-v5-a5=0
	'a5-a5=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
	x3 - x4 >= 0 

	v1 >=0
	v2 >=0
	v3 >=0
	v4 >=0

	
	x4 -x5 >=0
	v5 >=0


	'a1 - ac <=0
	'a1 - br >=0


	preserve[x1,x2,x3,x4,v1,v2,v3,v4,a2,a3,a4,t,br,ac,x5,v5,a5,r2,r3,r4,r5]


#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
	x3 - x4 >=0
	

	x4 -x5 >=0
	v5 >=0


	v1 >=0
	v2 >=0
	v3 >=0
	v4 >=0
	
	x1 -x2 <= 30
	
	'a2 <=0
	'a2 -a1 <=0
	'a2 -br >= 0
	
	'r2=0

	preserve[x1,x2,x3,x4,v1,v2,v3,v4,a1,a3,a4,t,br,ac,x5,v5,a5,r3,r4,r5]

#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
	   x3-x4>=0
	   
	   
	   x4 -x5 >=0
	   v5 >=0
	   

	   v1 >=0
	   v2 >=0
	   v3 >=0
	   
	   x1 -x2 >= 50
	   
	   'a2 >=0
	   'a2-a1 >=0
	   'a2 -ac <=0

	   


	preserve[x1,x2,x3,x4,v1,v2,v3,v4,a1,a3,a4,t,br,ac,x5,v5,a5,r2,r3,r4,r5]

#If in optimal range, car 2 will just coast

transition t5: l0,
	   br +1 =0
       	   ac -1=0
	   
	   x1 -x2 >=0
	   x2 - x3 >=0
	   x3-x4>=0

	   
	  x4 -x5 >=0
	  v5 >=0


	   v1 >=0
	   v2 >=0
	   v3 >=0
	   v4 >=0

	   x1 -x2 >= 30
	   x1 -x2 <= 50
	   
	   'a2 =0

	   
	preserve[x1,x2,x3,x4,v1,v2,v3,v4,a1,a3,a4,t,br,ac,x5,v5,a5,r2,r3,r4,r5]

#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
	x3-x4>=0
	
	x4-x5>=0	
	v5 >=0

	v1 >= 0
	v2 >= 0
	v3 >= 0
	v4 >= 0
	

	x2 - x3 <= 30
	
	'a3 <=0
	'a3-a2 <=0
	'a3 -br >= 0
	
	'r3 =0

	
	
	preserve[x1,x2,x3,x4,v1,v2,v3,v4,a1,a2,a4,t,br,ac,x5,v5,a5,r2,r4,r5]



transition t4: l0,
	
	br +1 =0
	ac -1=0
	
	x1 - x2 >=0
	x2 - x3 >=0
	x3 - x4 >=0
	
	x4-x5>=0
	v5 >=0

	v1 >=0
	v2 >=0
	v3 >=0
	v4 >=0

	x2 - x3 >= 50
	
	'a3 >=0
	'a3 -ac <= 0
	'a3 -a2 >=0


	
	preserve[x1,x2,x3,x4,v1,v2,v3,v4,a1,a2,a4,t,br,ac,x5,v5,a5,r2,r3,r4,r5]


transition t6: l0,
	
	br +1 =0
	ac -1=0
	
	x1 -x2 >=0
	x2 - x3 >=0
	x3 - x4 >=0

	v1 >=0
	v2 >=0
	v3 >=0
	v4 >=0
	
	
	x4 -x5 >=0
	v5 >=0


	x2 -x3 >= 30
	x2 - x3 <= 50
	
	'a3 =0
	

	preserve[x1,x2,x3,x4,v1,v2,v3,v4,a1,a2,a4,t,br,ac,x5,v5,a5,r2,r3,r4,r5]

#For the car 4 in the platoon, 
#needs to look at car 3 and adjust

transition t7: l0,
	br +1 =0
	ac -1=0
	
	x1 -x2 >=0
	x2 - x3 >=0
	x3-x4>=0
	
	v1 >= 0
	v2 >= 0
	v3 >= 0
	v4 >= 0
	
	
	x4 -x5 >=0
	v5 >=0


	x3 - x4 <= 30
	
	'a4 <=0
	'a4-a3 <=0
	'a4 -br >= 0
	
	'r4=0



	preserve[x1,x2,x3,x4,v1,v2,v3,v4,a1,a2,a3,t,br,ac,x5,v5,a5,r2,r3,r5]



transition t8: l0,
	
	br +1 =0
	ac -1=0
	
	x1 - x2 >=0
	x2 - x3 >=0
	x3 - x4 >=0
	
	v1 >=0
	v2 >=0
	v3 >=0
	v4 >=0

	
	x4 -x5 >=0
	v5 >=0


	x3 - x4 >= 50
	
	'a4 >=0
	'a4 -a3 >=0
	'a4 -ac <= 0
	


	preserve[x1,x2,x3,x4,v1,v2,v3,v4,a1,a2,a3,t,br,ac,x5,v5,a5,r2,r3,r4,r5]


transition t9: l0,
	
	br +1 =0
	ac -1=0
	
	x1 -x2 >=0
	x2 - x3 >=0
	x3 - x4 >=0

	v1 >=0
	v2 >=0
	v3 >=0
	v4 >=0

	
	x4 -x5 >=0
	v5 >=0

	x3 -x4 >= 30
	x3 - x4 <= 50
	
	'a4 =0
	
	preserve[x1,x2,x3,x4,v1,v2,v3,v4,a1,a2,a3,t,br,ac,x5,v5,a5,r2,r3,r4,r5]

#Now car 5 needs to sense and upgrade its position


transition t10: l0,
	br +1 =0
	ac -1=0
	
	x1 -x2 >=0
	x2 - x3 >=0
	x3-x4>=0
	
	v1 >= 0
	v2 >= 0
	v3 >= 0
	v4 >= 0
	
	
	x4 -x5 >=0
	v5 >=0


	x4 - x5 <= 30
	
	'a5 <=0
	'a5-a4 <=0
	'a5 -br >= 0
	
	'r5=0
	
	preserve[x1,x2,x3,x4,v1,v2,v3,v4,a1,a2,a3,a4,t,br,ac,x5,v5,r2,r3,r4]



transition t11: l0,
	
	br +1 =0
	ac -1=0
	
	x1 - x2 >=0
	x2 - x3 >=0
	x3 - x4 >=0
	
	v1 >=0
	v2 >=0
	v3 >=0
	v4 >=0

	
	x4 -x5 >=0
	v5 >=0


	x4 - x5 >= 50
	
	'a5 >=0
	'a5-a4>=0
	'a5 -ac <= 0
	
	preserve[x1,x2,x3,x4,v1,v2,v3,v4,a1,a2,a3,a4,t,br,ac,x5,v5,r2,r3,r4,r5]


transition t12: l0,
	
	br +1 =0
	ac -1=0
	
	x1 -x2 >=0
	x2 - x3 >=0
	x3 - x4 >=0

	v1 >=0
	v2 >=0
	v3 >=0
	v4 >=0

	
	x4 -x5 >=0
	v5 >=0

	x4 -x5 >= 3
	x4 - x5 <= 5
	
	'a5 =0
	
	preserve[x1,x2,x3,x4,v1,v2,v3,v4,a1,a2,a3,a4,t,br,ac,x5,v5,r2,r3,r4,r5]
	   
	  

end
