variable[x1 v1 x2 v2 x3 v3 t]

propsteps(1)

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
5 -1*v1>= 0
2* t-1*v1 +2*v2 -1*v3   >= 0
75 -1*x2 +5*t   >= 0
1*v3  >= 0
1*x2 +5*t -75 >= 0
1*v1 -2*v2 +1*v3 +2*t  >= 0
1*v1 -1*v3  >= 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