unknown Initial ITS Start location: [1] Program variables: x y z 0: [1] -> [2] : x'=12, T, cost: 1 1: [2] -> [3] : y'=0, T, cost: 1 2: [3] -> [4] : z'=nondet, T, cost: 1 3: [4] -> [5] : z > 0, cost: 1 8: [4] -> [9] : z <= 0, cost: 1 4: [5] -> [6] : x'=1+x, T, cost: 1 5: [6] -> [7] : y'=-1+y, T, cost: 1 6: [7] -> [8] : z'=-1+z, T, cost: 1 7: [8] -> [4] : T, cost: 1 Chained Linear Paths Start location: [1] Program variables: x y z 10: [1] -> [4] : x'=12, y'=0, z'=nondet, T, cost: 1 8: [4] -> [9] : z <= 0, cost: 1 14: [4] -> [4] : x'=1+x, y'=-1+y, z'=-1+z, z > 0, cost: 1 Eliminating location [2] by chaining: Applied chaining First rule: [1] -> [2] : x'=12, T, cost: 1 Second rule: [2] -> [3] : y'=0, T, cost: 1 New rule: [1] -> [3] : x'=12, y'=0, T, cost: 1 Applied deletion Removed the following rules: 0 1 Eliminating location [3] by chaining: Applied chaining First rule: [1] -> [3] : x'=12, y'=0, T, cost: 1 Second rule: [3] -> [4] : z'=nondet, T, cost: 1 New rule: [1] -> [4] : x'=12, y'=0, z'=nondet, T, cost: 1 Applied deletion Removed the following rules: 2 9 Eliminating location [5] by chaining: Applied chaining First rule: [4] -> [5] : z > 0, cost: 1 Second rule: [5] -> [6] : x'=1+x, T, cost: 1 New rule: [4] -> [6] : x'=1+x, z > 0, cost: 1 Applied deletion Removed the following rules: 3 4 Eliminating location [6] by chaining: Applied chaining First rule: [4] -> [6] : x'=1+x, z > 0, cost: 1 Second rule: [6] -> [7] : y'=-1+y, T, cost: 1 New rule: [4] -> [7] : x'=1+x, y'=-1+y, z > 0, cost: 1 Applied deletion Removed the following rules: 5 11 Eliminating location [7] by chaining: Applied chaining First rule: [4] -> [7] : x'=1+x, y'=-1+y, z > 0, cost: 1 Second rule: [7] -> [8] : z'=-1+z, T, cost: 1 New rule: [4] -> [8] : x'=1+x, y'=-1+y, z'=-1+z, z > 0, cost: 1 Applied deletion Removed the following rules: 6 12 Eliminating location [8] by chaining: Applied chaining First rule: [4] -> [8] : x'=1+x, y'=-1+y, z'=-1+z, z > 0, cost: 1 Second rule: [8] -> [4] : T, cost: 1 New rule: [4] -> [4] : x'=1+x, y'=-1+y, z'=-1+z, z > 0, cost: 1 Applied deletion Removed the following rules: 7 13 Step with 10 Trace 10[T] Blocked [{}, {}] Step with 8 Trace 10[T], 8[(z <= 0)] Blocked [{}, {}, {}] Backtrack Trace 10[T] Blocked [{}, {8[T]}] Step with 14 Trace 10[T], 14[(z > 0)] Blocked [{}, {8[T]}, {}] Accelerate Start location: [1] Program variables: x y z 10: [1] -> [4] : x'=12, y'=0, z'=nondet, T, cost: 1 8: [4] -> [9] : z <= 0, cost: 1 14: [4] -> [4] : x'=1+x, y'=-1+y, z'=-1+z, z > 0, cost: 1 15: [4] -> [4] : x'=n+x, y'=-n+y, z'=-n+z, (-1+n >= 0 /\ 1-n+z > 0), cost: 1 Loop Acceleration Original rule: [4] -> [4] : x'=1+x, y'=-1+y, z'=-1+z, (z > 0), cost: 1 New rule: [4] -> [4] : x'=n+x, y'=-n+y, z'=-n+z, (-1+n >= 0 /\ 1-n+z > 0), cost: 1 z > 0 [0]: montonic decrease yields 1-n+z > 0 z > 0 [1]: eventual increase yields (1 <= 0 /\ z > 0) Replacement map: {z > 0 -> 1-n+z > 0} Trace 10[T], 15[(-1+n >= 0 /\ 1-n+z > 0)] Blocked [{}, {8[T]}, {14[T], 15[T]}] Step with 8 Trace 10[T], 15[(-1+n >= 0 /\ 1-n+z > 0)], 8[(z <= 0)] Blocked [{}, {8[T]}, {14[T], 15[T]}, {}] Backtrack Trace 10[T], 15[(-1+n >= 0 /\ 1-n+z > 0)] Blocked [{}, {8[T]}, {8[T], 14[T], 15[T]}] Backtrack Trace 10[T] Blocked [{}, {8[T], 15[T]}] Step with 14 Trace 10[T], 14[(z > 0)] Blocked [{}, {8[T], 15[T]}, {}] Covered Trace 10[T] Blocked [{}, {8[T], 14[T], 15[T]}] Backtrack Trace Blocked [{10[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b