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
