variable[x1 v1 x2 v2 x3 v3 t]

propsteps(3)

location l0
	
	x1=100
	x2=75
	x3+50=0
	v3 >= 0
	v1 <= 5
	v1 -v3 >= 0
	2* v2 - v1 - v3=0
	t=0


#Model the elapse of time

invariant l0:

v2+5 >=0
v2 -5<=0
0-34*x1 -251*v1 +460*x2 +110*v2 -34*x3 -55*v3 +2530*t -31820 >= 0
0-12*x1 -5*v1 +220*x2 +10*v2 -12*x3 -5*v3 +1210*t -15900 >= 0
0-11*x1 -74*v1 +120*x2 +50*v2 -11*x3 -74*v3 +660*t -7960 >= 0
0-2*x1 -9*v1 +4*x2 +18*v2 -2*x3 -9*v3 +22*t -4 >= 0
0-1*x1 +5*t  + 100 >= 0
0-1*x1 +1*v1 +2*x2 +20*v2 -1*x3 +1*v3  + 130 >= 0
0-10*v1 -17*x2 +20*v2 +85*t  + 1275 >= 0
0-5*v1 -10*x2 +10*v2 -3*v3 +50*t  + 750 >= 0
0-1*v1  + 5 >= 0
0-1*v1 +2*v2 -1*v3 +2*t  >= 0
0-3*x2 +5*v2 +15*t  + 225 >= 0
0-1*x2 +5*t  + 75 >= 0
0-1*v2  + 6 >= 0
1*v3  >= 0
1*x3  + 50 >= 0
1*v2  + 6 >= 0
1*x2 -10*v2 +5*t -25 >= 0
1*x2 +5*t -75 >= 0
7*x2 -20*v2 +10*v3 +35*t -475 >= 0
1*v1 -2*v2 +1*v3 +2*t  >= 0
1*v1 -1*v3  >= 0
5*v1 +6*x2 -10*v2 +5*v3 +30*t -450 >= 0
1*x1 -1*x3 -150 >= 0



Transition t0:l0,
	2* x2 - x1 - x3>=0
	'x1-x1-v1=0
	'x3-x3- v3=0
	'x2-x2-v2=0
	 'v2-v2+1=0
	't-t-1=0
preserve[v1,v3]

Transition t1: l0,
	2*x2 -x1-x3 <=0
	'x1-x1- v1=0
	'x3-x3- v3=0
	'x2-x2- v2=0
	 'v2-v2-1=0
	't-t-1=0
preserve[v1,v3]

end