variable [ X1 X2 X3 X4 X5 X6 ]

location l0
X1>=1 
 X2=0 
 X3=0 
X4=1 
X5=0 
X6=0

invariant l0:
X1 >= 0
X2 >= 0
X3 >= 0
X4 >= 0
X5 >= 0
X6 >= 0

transition t1:l0,
	X1 >= 1
	X4 >= 1
	'X1=X1-1
	'X4=X4-1
	'X2=X2+1
	'X5=X5+1
	preserve[X3, X6]

transition t2:l0,
	X2 >=1
	X6 >= 1
	'X2=X2 -1
	'X3=X3 +1
	preserve[X1, X4,X5,X6]

transition t3:l0,
	X4 >= 1
	X3 >= 1
	'X3=X3-1
	 'X2=X2+1
	preserve[X1,X4,X5,X6]

transition t4:l0,
	X3>=1
	'X3=X3-1
	'X1=X1+1
	'X6=X6+X5
	'X5=0
	preserve[X2,X4]

transition t5:l0,
	X2 >= 1
	'X2 = X2 -1
	'X1 = X1 +1
	'X4 = X4 + X6
	'X6=0
	preserve[X3,X5]

end	
