variable[x1 v1 x2 v2 x3 v3 t]

propsteps(2)

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

invariant l0:
	v2 +5 >=0
	v2 <= 5

#Model the elapse of time

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