# #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