unknown Initial ITS Start location: l6 Program variables: j^0 0: l0 -> l1 : j^0'=j^post1, -j^post1+j^0 == 0, cost: 1 1: l0 -> l1 : j^0'=j^post2, j^0-j^post2 == 0, cost: 1 5: l1 -> l4 : j^0'=j^post6, -j^post6+j^0 == 0, cost: 1 2: l2 -> l0 : j^0'=j^post3, (2-j^0 <= 0 /\ -j^post3+j^0 == 0), cost: 1 3: l2 -> l3 : j^0'=j^post4, (-1+j^0 <= 0 /\ -1+j^post4-j^0 == 0), cost: 1 4: l3 -> l2 : j^0'=j^post5, j^0-j^post5 == 0, cost: 1 6: l5 -> l3 : j^0'=j^post7, j^post7 == 0, cost: 1 7: l6 -> l5 : j^0'=j^post8, j^0-j^post8 == 0, cost: 1 Chained Linear Paths Start location: l6 Program variables: j^0 0: l0 -> l1 : j^0'=j^post1, -j^post1+j^0 == 0, cost: 1 1: l0 -> l1 : j^0'=j^post2, j^0-j^post2 == 0, cost: 1 5: l1 -> l4 : j^0'=j^post6, -j^post6+j^0 == 0, cost: 1 2: l2 -> l0 : j^0'=j^post3, (2-j^0 <= 0 /\ -j^post3+j^0 == 0), cost: 1 3: l2 -> l3 : j^0'=j^post4, (-1+j^0 <= 0 /\ -1+j^post4-j^0 == 0), cost: 1 4: l3 -> l2 : j^0'=j^post5, j^0-j^post5 == 0, cost: 1 8: l6 -> l3 : j^0'=j^post7, (j^0-j^post8 == 0 /\ j^post7 == 0), cost: 1 Eliminating location l5 by chaining: Applied chaining First rule: l6 -> l5 : j^0'=j^post8, j^0-j^post8 == 0, cost: 1 Second rule: l5 -> l3 : j^0'=j^post7, j^post7 == 0, cost: 1 New rule: l6 -> l3 : j^0'=j^post7, (j^0-j^post8 == 0 /\ j^post7 == 0), cost: 1 Applied deletion Removed the following rules: 6 7 Simplified Transitions Start location: l6 Program variables: j^0 9: l0 -> l1 : T, cost: 1 10: l0 -> l1 : T, cost: 1 14: l1 -> l4 : T, cost: 1 11: l2 -> l0 : 2-j^0 <= 0, cost: 1 12: l2 -> l3 : j^0'=1+j^0, -1+j^0 <= 0, cost: 1 13: l3 -> l2 : T, cost: 1 15: l6 -> l3 : j^0'=0, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : j^0'=j^post1, -j^post1+j^0 == 0, cost: 1 New rule: l0 -> l1 : j^0'=j^0, 0 == 0, cost: 1 propagated equality j^post1 = j^0 Simplified Guard Original rule: l0 -> l1 : j^0'=j^0, 0 == 0, cost: 1 New rule: l0 -> l1 : j^0'=j^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : j^0'=j^0, T, cost: 1 New rule: l0 -> l1 : T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : j^0'=j^post2, j^0-j^post2 == 0, cost: 1 New rule: l0 -> l1 : j^0'=j^0, 0 == 0, cost: 1 propagated equality j^post2 = j^0 Simplified Guard Original rule: l0 -> l1 : j^0'=j^0, 0 == 0, cost: 1 New rule: l0 -> l1 : j^0'=j^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : j^0'=j^0, T, cost: 1 New rule: l0 -> l1 : T, cost: 1 Propagated Equalities Original rule: l2 -> l0 : j^0'=j^post3, (2-j^0 <= 0 /\ -j^post3+j^0 == 0), cost: 1 New rule: l2 -> l0 : j^0'=j^0, (0 == 0 /\ 2-j^0 <= 0), cost: 1 propagated equality j^post3 = j^0 Simplified Guard Original rule: l2 -> l0 : j^0'=j^0, (0 == 0 /\ 2-j^0 <= 0), cost: 1 New rule: l2 -> l0 : j^0'=j^0, 2-j^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l0 : j^0'=j^0, 2-j^0 <= 0, cost: 1 New rule: l2 -> l0 : 2-j^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l3 : j^0'=j^post4, (-1+j^0 <= 0 /\ -1+j^post4-j^0 == 0), cost: 1 New rule: l2 -> l3 : j^0'=1+j^0, (0 == 0 /\ -1+j^0 <= 0), cost: 1 propagated equality j^post4 = 1+j^0 Simplified Guard Original rule: l2 -> l3 : j^0'=1+j^0, (0 == 0 /\ -1+j^0 <= 0), cost: 1 New rule: l2 -> l3 : j^0'=1+j^0, -1+j^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l2 : j^0'=j^post5, j^0-j^post5 == 0, cost: 1 New rule: l3 -> l2 : j^0'=j^0, 0 == 0, cost: 1 propagated equality j^post5 = j^0 Simplified Guard Original rule: l3 -> l2 : j^0'=j^0, 0 == 0, cost: 1 New rule: l3 -> l2 : j^0'=j^0, T, cost: 1 Removed Trivial Updates Original rule: l3 -> l2 : j^0'=j^0, T, cost: 1 New rule: l3 -> l2 : T, cost: 1 Propagated Equalities Original rule: l1 -> l4 : j^0'=j^post6, -j^post6+j^0 == 0, cost: 1 New rule: l1 -> l4 : j^0'=j^0, 0 == 0, cost: 1 propagated equality j^post6 = j^0 Simplified Guard Original rule: l1 -> l4 : j^0'=j^0, 0 == 0, cost: 1 New rule: l1 -> l4 : j^0'=j^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l4 : j^0'=j^0, T, cost: 1 New rule: l1 -> l4 : T, cost: 1 Propagated Equalities Original rule: l6 -> l3 : j^0'=j^post7, (j^0-j^post8 == 0 /\ j^post7 == 0), cost: 1 New rule: l6 -> l3 : j^0'=0, (0 == 0 /\ j^0-j^post8 == 0), cost: 1 propagated equality j^post7 = 0 Propagated Equalities Original rule: l6 -> l3 : j^0'=0, (0 == 0 /\ j^0-j^post8 == 0), cost: 1 New rule: l6 -> l3 : j^0'=0, 0 == 0, cost: 1 propagated equality j^post8 = j^0 Simplified Guard Original rule: l6 -> l3 : j^0'=0, 0 == 0, cost: 1 New rule: l6 -> l3 : j^0'=0, T, cost: 1 Step with 15 Trace 15[T] Blocked [{}, {}] Step with 13 Trace 15[T], 13[T] Blocked [{}, {}, {}] Step with 12 Trace 15[T], 13[T], 12[(-1+j^0 <= 0)] Blocked [{}, {}, {11[T]}, {}] Accelerate Start location: l6 Program variables: j^0 9: l0 -> l1 : T, cost: 1 10: l0 -> l1 : T, cost: 1 14: l1 -> l4 : T, cost: 1 11: l2 -> l0 : 2-j^0 <= 0, cost: 1 12: l2 -> l3 : j^0'=1+j^0, -1+j^0 <= 0, cost: 1 13: l3 -> l2 : T, cost: 1 16: l3 -> l3 : j^0'=n+j^0, (-1+n >= 0 /\ 2-n-j^0 >= 0), cost: 1 15: l6 -> l3 : j^0'=0, T, cost: 1 Loop Acceleration Original rule: l3 -> l3 : j^0'=1+j^0, -1+j^0 <= 0, cost: 1 New rule: l3 -> l3 : j^0'=n+j^0, (-1+n >= 0 /\ 2-n-j^0 >= 0), cost: 1 1-j^0 >= 0 [0]: montonic decrease yields 2-n-j^0 >= 0 1-j^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 1-j^0 >= 0) Replacement map: {1-j^0 >= 0 -> 2-n-j^0 >= 0} Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)] Blocked [{}, {}, {16[T]}] Step with 13 Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)], 13[T] Blocked [{}, {}, {16[T]}, {}] Step with 12 Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)], 13[T], 12[(-1+j^0 <= 0)] Blocked [{}, {}, {16[T]}, {}, {}] Covered Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)], 13[T] Blocked [{}, {}, {16[T]}, {12[T]}] Step with 11 Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)], 13[T], 11[(2-j^0 <= 0)] Blocked [{}, {}, {16[T]}, {12[T]}, {}] Step with 9 Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)], 13[T], 11[(2-j^0 <= 0)], 9[T] Blocked [{}, {}, {16[T]}, {12[T]}, {}, {}] Step with 14 Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)], 13[T], 11[(2-j^0 <= 0)], 9[T], 14[T] Blocked [{}, {}, {16[T]}, {12[T]}, {}, {}, {}] Backtrack Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)], 13[T], 11[(2-j^0 <= 0)], 9[T] Blocked [{}, {}, {16[T]}, {12[T]}, {}, {14[T]}] Backtrack Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)], 13[T], 11[(2-j^0 <= 0)] Blocked [{}, {}, {16[T]}, {12[T]}, {9[T]}] Step with 10 Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)], 13[T], 11[(2-j^0 <= 0)], 10[T] Blocked [{}, {}, {16[T]}, {12[T]}, {9[T]}, {}] Step with 14 Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)], 13[T], 11[(2-j^0 <= 0)], 10[T], 14[T] Blocked [{}, {}, {16[T]}, {12[T]}, {9[T]}, {}, {}] Backtrack Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)], 13[T], 11[(2-j^0 <= 0)], 10[T] Blocked [{}, {}, {16[T]}, {12[T]}, {9[T]}, {14[T]}] Backtrack Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)], 13[T], 11[(2-j^0 <= 0)] Blocked [{}, {}, {16[T]}, {12[T]}, {9[T], 10[T]}] Backtrack Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)], 13[T] Blocked [{}, {}, {16[T]}, {11[T], 12[T]}] Backtrack Trace 15[T], 16[(-1+n >= 0 /\ 2-n-j^0 >= 0)] Blocked [{}, {}, {13[T], 16[T]}] Backtrack Trace 15[T] Blocked [{}, {16[T]}] Step with 13 Trace 15[T], 13[T] Blocked [{}, {16[T]}, {}] Step with 12 Trace 15[T], 13[T], 12[(-1+j^0 <= 0)] Blocked [{}, {16[T]}, {11[T]}, {}] Covered Trace 15[T], 13[T] Blocked [{}, {16[T]}, {11[T], 12[T]}] Backtrack Trace 15[T] Blocked [{}, {13[T], 16[T]}] Backtrack Trace Blocked [{15[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b