NO Initial ITS Start location: [1] Program variables: i j 0: [1] -> [2] : j'=100, T, cost: 1 1: [2] -> [3] : i'=0, T, cost: 1 2: [3] -> [4] : i-j < 0, cost: 1 6: [3] -> [7] : i-j >= 0, cost: 1 3: [4] -> [5] : j'=1+j, T, cost: 1 4: [5] -> [6] : i'=1+i, T, cost: 1 5: [6] -> [3] : T, cost: 1 Chained Linear Paths Start location: [1] Program variables: i j 7: [1] -> [3] : i'=0, j'=100, T, cost: 1 6: [3] -> [7] : i-j >= 0, cost: 1 10: [3] -> [3] : i'=1+i, j'=1+j, i-j < 0, cost: 1 Eliminating location [2] by chaining: Applied chaining First rule: [1] -> [2] : j'=100, T, cost: 1 Second rule: [2] -> [3] : i'=0, T, cost: 1 New rule: [1] -> [3] : i'=0, j'=100, T, cost: 1 Applied deletion Removed the following rules: 0 1 Eliminating location [4] by chaining: Applied chaining First rule: [3] -> [4] : i-j < 0, cost: 1 Second rule: [4] -> [5] : j'=1+j, T, cost: 1 New rule: [3] -> [5] : j'=1+j, i-j < 0, cost: 1 Applied deletion Removed the following rules: 2 3 Eliminating location [5] by chaining: Applied chaining First rule: [3] -> [5] : j'=1+j, i-j < 0, cost: 1 Second rule: [5] -> [6] : i'=1+i, T, cost: 1 New rule: [3] -> [6] : i'=1+i, j'=1+j, i-j < 0, cost: 1 Applied deletion Removed the following rules: 4 8 Eliminating location [6] by chaining: Applied chaining First rule: [3] -> [6] : i'=1+i, j'=1+j, i-j < 0, cost: 1 Second rule: [6] -> [3] : T, cost: 1 New rule: [3] -> [3] : i'=1+i, j'=1+j, i-j < 0, cost: 1 Applied deletion Removed the following rules: 5 9 Step with 7 Trace 7[T] Blocked [{}, {}] Step with 10 Trace 7[T], 10[(i-j < 0)] Blocked [{}, {6[T]}, {}] Nonterm Start location: [1] Program variables: i j 7: [1] -> [3] : i'=0, j'=100, T, cost: 1 6: [3] -> [7] : i-j >= 0, cost: 1 10: [3] -> [3] : i'=1+i, j'=1+j, i-j < 0, cost: 1 11: [3] -> LoAT_sink : (-i+j > 0 /\ -1+n >= 0), cost: NONTERM 12: [3] -> [3] : i'=i+n, j'=j+n, (-i+j > 0 /\ -1+n >= 0), cost: 1 Certificate of Non-Termination Original rule: [3] -> [3] : i'=1+i, j'=1+j, (i-j < 0), cost: 1 New rule: [3] -> LoAT_sink : (-i+j > 0 /\ -1+n >= 0), cost: NONTERM -i+j > 0 [0]: monotonic increase yields -i+j > 0 Replacement map: {-i+j > 0 -> -i+j > 0} Loop Acceleration Original rule: [3] -> [3] : i'=1+i, j'=1+j, (i-j < 0), cost: 1 New rule: [3] -> [3] : i'=i+n, j'=j+n, (-i+j > 0 /\ -1+n >= 0), cost: 1 -i+j > 0 [0]: monotonic increase yields -i+j > 0 Replacement map: {-i+j > 0 -> -i+j > 0} Step with 11 Trace 7[T], 11[(-i+j > 0 /\ -1+n >= 0)] Blocked [{}, {6[T]}, {11[T]}] Refute Counterexample [ i=0 j=100 ] 7 [ i=i j=j ] 11 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b