#
#Inductive invariants from swim-pool.in added
# back to the transition system
#

variable [x1 x2 x3 x4 x5 x6 x7 p q]

Location l0
x1=0
x2=0
x3=0
x4=0
x5=0
x6-p=0
x7-q=0
p >=1
q >=1



Transition t1: l0,

1*x2 +1*x3 +1*x4 +1*x7 -1*q   = 0 
1*x1 +1*x2 +1*x4 +1*x5 +1*x6 -1*p   = 0 
1*x7  >= 0
1*x6  >= 0
1*x5  >= 0
1*x4  >= 0
1*x3  >= 0
1*x2  >= 0
1*x2 +1*x3 +1*x4 +1*x7 -1 >= 0
1*x1  >= 0
1*x1 +1*x2 +1*x4 +1*x5 +1*x6 -1 >= 0

x6 >=1
'x1-x1-1=0
'x2-x2=0
'x3-x3=0
'x4-x4=0
'x5-x5=0
'x6-x6+1=0
'x7-x7=0
'p-p=0
'q-q=0

Transition t2: l0,

1*x2 +1*x3 +1*x4 +1*x7 -1*q   = 0 
1*x1 +1*x2 +1*x4 +1*x5 +1*x6 -1*p   = 0 
1*x7  >= 0
1*x6  >= 0
1*x5  >= 0
1*x4  >= 0
1*x3  >= 0
1*x2  >= 0
1*x2 +1*x3 +1*x4 +1*x7 -1 >= 0
1*x1  >= 0
1*x1 +1*x2 +1*x4 +1*x5 +1*x6 -1 >= 0


x1 >=1
x7 >=1

'x1-x1+1=0
'x2-x2-1=0
'x3-x3=0
'x4-x4=0
'x5-x5=0
'x6-x6=0
'x7-x7+1=0
'p-p=0
'q-q=0

Transition t3: l0,

1*x2 +1*x3 +1*x4 +1*x7 -1*q   = 0 
1*x1 +1*x2 +1*x4 +1*x5 +1*x6 -1*p   = 0 
1*x7  >= 0
1*x6  >= 0
1*x5  >= 0
1*x4  >= 0
1*x3  >= 0
1*x2  >= 0
1*x2 +1*x3 +1*x4 +1*x7 -1 >= 0
1*x1  >= 0
1*x1 +1*x2 +1*x4 +1*x5 +1*x6 -1 >= 0


x2 >=1

'x1-x1=0
'x2-x2+1=0
'x3-x3-1=0
'x4-x4=0
'x5-x5=0
'x6-x6-1=0
'x7-x7=0
'p-p=0
'q-q=0

Transition t4: l0,

1*x2 +1*x3 +1*x4 +1*x7 -1*q   = 0 
1*x1 +1*x2 +1*x4 +1*x5 +1*x6 -1*p   = 0 
1*x7  >= 0
1*x6  >= 0
1*x5  >= 0
1*x4  >= 0
1*x3  >= 0
1*x2  >= 0
1*x2 +1*x3 +1*x4 +1*x7 -1 >= 0
1*x1  >= 0
1*x1 +1*x2 +1*x4 +1*x5 +1*x6 -1 >= 0


x3>=1
x6>=1

'x1-x1=0
'x2-x2=0
'x3-x3+1=0
'x4-x4-1=0
'x5-x5=0
'x6-x6+1=0
'x7-x7=0
'p-p=0
'q-q=0

Transition t5: l0,


1*x2 +1*x3 +1*x4 +1*x7 -1*q   = 0 
1*x1 +1*x2 +1*x4 +1*x5 +1*x6 -1*p   = 0 
1*x7  >= 0
1*x6  >= 0
1*x5  >= 0
1*x4  >= 0
1*x3  >= 0
1*x2  >= 0
1*x2 +1*x3 +1*x4 +1*x7 -1 >= 0
1*x1  >= 0
1*x1 +1*x2 +1*x4 +1*x5 +1*x6 -1 >= 0


x4>=1
'x1-x1=0
'x2-x2=0
'x3-x3=0
'x4-x4+1=0
'x5-x5-1=0
'x6-x6=0
'x7-x7-1=0
'p-p=0
'q-q=0

Transition t6: l0,


1*x2 +1*x3 +1*x4 +1*x7 -1*q   = 0 
1*x1 +1*x2 +1*x4 +1*x5 +1*x6 -1*p   = 0 
1*x7  >= 0
1*x6  >= 0
1*x5  >= 0
1*x4  >= 0
1*x3  >= 0
1*x2  >= 0
1*x2 +1*x3 +1*x4 +1*x7 -1 >= 0
1*x1  >= 0
1*x1 +1*x2 +1*x4 +1*x5 +1*x6 -1 >= 0


x5>=1

'x1-x1=0
'x2-x2=0
'x3-x3=0
'x4-x4=0
'x5-x5+1=0
'x6-x6-1=0
'x7-x7=0
'p-p=0
'q-q=0




end