(0) Obligation:
Need to prove time_complexity of the following program:
/**
* Example taken from "A Term Rewriting Approach to the Automated Termination
* Analysis of Imperative Programs" (http://www.cs.unm.edu/~spf/papers/2009-02.pdf)
* and converted to Java.
*/
public class PastaA6 {
public static void main(int x, int y, int z) {
while (x > y + z) {
y++;
z++;
}
}
}
(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Constructed TerminationGraph.
(2) Obligation:
Termination Graph based on JBC Program:
PastaA6.main(III)V: Graph of 48 nodes with 1 SCC.
(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)) transformation)
Extracted set of 44 edges for the analysis of TIME complexity. Kept leaves.
(4) Obligation:
Set of 44 edges based on JBC Program.
Performed SCC analyses:
- Used field analysis yielded the following read fields:
Considered paths: nonterm paths and paths from start to sinks
(5) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 44 jbc graph edges to a weighted ITS with 44 rules.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.
(6) Obligation:
IntTrs with 44 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, i6, env, static) -{0,0}> main_Load_3(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_3(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_23(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_23(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, i4, i6, env, static) -{1,1}> main_Load_41(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_41(i1, i4, i6, env, static) -{0,0}> main_Load_42(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_42(i1, i4, i6, env, static) -{0,0}> main_Load_43(i1, i4, i6, env, static) :|: 0 <= static
main_Load_43(i1, i4, i6, env, static) -{0,0}> main_Load_48(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_48(i1, i4, i6, env, static) -{0,0}> main_Load_49(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i1, i4, i6, env, static) -{1,1}> main_Load_51(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_51(i1, i4, i6, env, static) -{1,1}> main_Load_53(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_53(i1, i4, i6, env, static) -{1,1}> main_IntArithmetic_54(i1, i4, i6, env, static) :|: 0 >= 0
main_IntArithmetic_54(i1, i4, i6, env, static) -{1,1}> main_LE_59(i1, i4, i6, i8, env, static) :|: i4 + i6 = i8
main_LE_59(i1, i4, i6, i8, env, static) -{0,0}> main_LE_60(i1, i4, i6, i8, env, static) :|: i1 <= i8
main_LE_59(i1, i4, i6, i8, env, static) -{0,0}> main_LE_61(i1, i4, i6, i8, env, static) :|: i8 < i1
main_LE_61(i1, i4, i6, i8, env, static) -{1,1}> main_Inc_72(i1, i4, i6, env, static) :|: i8 < i1
main_Inc_72(i1, i4, i6, env, static) -{1,1}> main_Inc_74(i1, i4, i6, i12, env, static) :|: i4 + 1 = i12
main_Inc_74(i1, i4, i6, i12, env, static) -{1,1}> main_JMP_75(i1, i4, i6, i12, i13, env, static) :|: i6 + 1 = i13
main_JMP_75(i1, i4, i6, i12, i13, env, static) -{0,0}> main_JMP_135(i1, i4, i6, i12, i13, env, static) :|: 0 >= 0
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_139(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_139(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_142(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_142(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_149(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_149(i1, i4, i6, i43, i48, env, static) -{1,1}> main_IntArithmetic_151(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_IntArithmetic_151(i1, i4, i6, i43, i48, env, static) -{1,1}> main_LE_166(i1, i4, i6, i63, i43, i48, env, static) :|: i43 + i48 = i63
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{0,0}> main_LE_171(i1, i4, i6, i63, i43, i48, env, static) :|: i1 <= i63
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{0,0}> main_LE_172(i1, i4, i6, i63, i43, i48, env, static) :|: i63 < i1
main_LE_172(i1, i4, i6, i63, i43, i48, env, static) -{1,1}> main_Inc_182(i1, i4, i6, i43, i48, env, static) :|: i63 < i1
main_Inc_182(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Inc_189(i1, i4, i6, i81, i48, env, static) :|: i43 + 1 = i81
main_Inc_189(i1, i4, i6, i81, i48, env, static) -{1,1}> main_JMP_195(i1, i4, i6, i81, i86, env, static) :|: i48 + 1 = i86
main_JMP_195(i1, i4, i6, i81, i86, env, static) -{0,0}> main_JMP_135(i1, i4, i6, i81, i86, env, static) :|: 0 >= 0
(7) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_Load_2(
i1,
i4,
i6,
env,
static) -{19,19}>
main_LE_59(
i1,
i4,
i6,
i8',
env,
static'1) :|:
i4 +
i6 =
i8' &&
0 <
2 &&
0 <=
static'1 &&
0 <=
static &&
0 <=
1 &&
0 <
1 &&
static''' <=
static +
2 &&
0 <=
static''' &&
0 <=
2 && 0 >= 0 &&
static'1 <=
static''' +
1by chaining
main_Load_2(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_3(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_3(
i1,
i4,
i6,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_6(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i1,
i4,
i6,
env,
static) :|:
iconst_0 =
0langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_13(
a2,
i1,
i4,
i6,
iconst_0,
env,
static) :|:
a2 =
2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_13(
a2,
i1,
i4,
i6,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_14(
i1,
i4,
i6,
env,
static') :|:
0 <=
a2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_14(
i1,
i4,
i6,
env,
static) -{0,0}>
langle_clinit_rangle_New_16(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
langle_clinit_rangle_New_16(
i1,
i4,
i6,
env,
static) -{0,0}>
langle_clinit_rangle_New_17(
i1,
i4,
i6,
env,
static) :|:
0 <=
staticlangle_clinit_rangle_New_17(
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_19(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2 &&
o2 =
1langle_clinit_rangle_Duplicate_19(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_21(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_clinit_rangle_ConstantStackPush_21(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_22(
o2,
NULL,
i1,
i4,
i6,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_clinit_rangle_InvokeMethod_22(
o2,
NULL,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_Load_23(
o2,
i1,
i4,
i6,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_init_rangle_Load_23(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_26(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_26(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_Load_27(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_Load_27(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_30(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_30(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_Return_32(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_Return_32(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_Return_34(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_Return_34(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_36(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_clinit_rangle_FieldAccess_36(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_Return_38(
i1,
i4,
i6,
env,
static') :|:
0 <
o2 &&
0 <=
o2 &&
0 <=
static &&
static' <=
static +
o2langle_clinit_rangle_Return_38(
i1,
i4,
i6,
env,
static) -{1,1}>
main_Load_41(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_41(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_42(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_42(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_43(
i1,
i4,
i6,
env,
static) :|:
0 <=
staticmain_Load_43(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_48(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_48(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_49(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_49(
i1,
i4,
i6,
env,
static) -{1,1}>
main_Load_51(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_51(
i1,
i4,
i6,
env,
static) -{1,1}>
main_Load_53(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_53(
i1,
i4,
i6,
env,
static) -{1,1}>
main_IntArithmetic_54(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_IntArithmetic_54(
i1,
i4,
i6,
env,
static) -{1,1}>
main_LE_59(
i1,
i4,
i6,
i8,
env,
static) :|:
i4 +
i6 =
i8obtained
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i12', i13', env, static) :|: 0 >= 0 && i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
by chaining
main_LE_59(i1, i4, i6, i8, env, static) -{0,0}> main_LE_61(i1, i4, i6, i8, env, static) :|: i8 < i1
main_LE_61(i1, i4, i6, i8, env, static) -{1,1}> main_Inc_72(i1, i4, i6, env, static) :|: i8 < i1
main_Inc_72(i1, i4, i6, env, static) -{1,1}> main_Inc_74(i1, i4, i6, i12, env, static) :|: i4 + 1 = i12
main_Inc_74(i1, i4, i6, i12, env, static) -{1,1}> main_JMP_75(i1, i4, i6, i12, i13, env, static) :|: i6 + 1 = i13
main_JMP_75(i1, i4, i6, i12, i13, env, static) -{0,0}> main_JMP_135(i1, i4, i6, i12, i13, env, static) :|: 0 >= 0
obtained
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i63', i43, i48, env, static) :|: 0 >= 0 && i43 + i48 = i63'
by chaining
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_139(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_139(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_142(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_142(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_149(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_149(i1, i4, i6, i43, i48, env, static) -{1,1}> main_IntArithmetic_151(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_IntArithmetic_151(i1, i4, i6, i43, i48, env, static) -{1,1}> main_LE_166(i1, i4, i6, i63, i43, i48, env, static) :|: i43 + i48 = i63
obtained
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i81', i86', env, static) :|: 0 >= 0 && i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
by chaining
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{0,0}> main_LE_172(i1, i4, i6, i63, i43, i48, env, static) :|: i63 < i1
main_LE_172(i1, i4, i6, i63, i43, i48, env, static) -{1,1}> main_Inc_182(i1, i4, i6, i43, i48, env, static) :|: i63 < i1
main_Inc_182(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Inc_189(i1, i4, i6, i81, i48, env, static) :|: i43 + 1 = i81
main_Inc_189(i1, i4, i6, i81, i48, env, static) -{1,1}> main_JMP_195(i1, i4, i6, i81, i86, env, static) :|: i48 + 1 = i86
main_JMP_195(i1, i4, i6, i81, i86, env, static) -{0,0}> main_JMP_135(i1, i4, i6, i81, i86, env, static) :|: 0 >= 0
(8) Obligation:
IntTrs with 6 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, i6, env, static) -{19,19}> main_LE_59(i1, i4, i6, i8', env, static'1) :|: i4 + i6 = i8' && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
main_LE_59(i1, i4, i6, i8, env, static) -{0,0}> main_LE_60(i1, i4, i6, i8, env, static) :|: i1 <= i8
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i12', i13', env, static) :|: 0 >= 0 && i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i63', i43, i48, env, static) :|: 0 >= 0 && i43 + i48 = i63'
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{0,0}> main_LE_171(i1, i4, i6, i63, i43, i48, env, static) :|: i1 <= i63
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i81', i86', env, static) :|: 0 >= 0 && i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
(9) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i12', i13', env, static) :|: 0 >= 0 && i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
was transformed to
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1, env, static) :|: 0 >= 0 && i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i63', i43, i48, env, static) :|: 0 >= 0 && i43 + i48 = i63'
was transformed to
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i43 + i48, i43, i48, env, static) :|: 0 >= 0 && i43 + i48 = i63'
main_Load_2(i1, i4, i6, env, static) -{19,19}> main_LE_59(i1, i4, i6, i8', env, static'1) :|: i4 + i6 = i8' && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
was transformed to
main_Load_2(i1, i4, i6, env, static) -{19,19}> main_LE_59(i1, i4, i6, i4 + i6, env, static'1) :|: i4 + i6 = i8' && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i81', i86', env, static) :|: 0 >= 0 && i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
was transformed to
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1, env, static) :|: 0 >= 0 && i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
(10) Obligation:
IntTrs with 6 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1, env, static) :|: 0 >= 0 && i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i43 + i48, i43, i48, env, static) :|: 0 >= 0 && i43 + i48 = i63'
main_LE_59(i1, i4, i6, i8, env, static) -{0,0}> main_LE_60(i1, i4, i6, i8, env, static) :|: i1 <= i8
main_Load_2(i1, i4, i6, env, static) -{19,19}> main_LE_59(i1, i4, i6, i4 + i6, env, static'1) :|: i4 + i6 = i8' && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1, env, static) :|: 0 >= 0 && i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{0,0}> main_LE_171(i1, i4, i6, i63, i43, i48, env, static) :|: i1 <= i63
(11) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
main_Load_2(i1, i4, i6, env, static) -{19,19}> main_LE_59(i1, i4, i6, i4 + i6, env, static'1) :|: i4 + i6 = i8' && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
was transformed to
main_Load_2(i1, i4, i6, env, static) -{19,19}> main_LE_59(i1, i4, i6, i4 + i6, env, static'1) :|: i4 + i6 = i8' && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1, env, static) :|: 0 >= 0 && i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
was transformed to
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1, env, static) :|: i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i43 + i48, i43, i48, env, static) :|: 0 >= 0 && i43 + i48 = i63'
was transformed to
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i43 + i48, i43, i48, env, static) :|: i43 + i48 = i63'
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1, env, static) :|: 0 >= 0 && i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
was transformed to
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1, env, static) :|: i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
(12) Obligation:
IntTrs with 6 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i43 + i48, i43, i48, env, static) :|: i43 + i48 = i63'
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1, env, static) :|: i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
main_LE_59(i1, i4, i6, i8, env, static) -{0,0}> main_LE_60(i1, i4, i6, i8, env, static) :|: i1 <= i8
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1, env, static) :|: i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{0,0}> main_LE_171(i1, i4, i6, i63, i43, i48, env, static) :|: i1 <= i63
main_Load_2(i1, i4, i6, env, static) -{19,19}> main_LE_59(i1, i4, i6, i4 + i6, env, static'1) :|: i4 + i6 = i8' && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
(13) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 44 jbc graph edges to a weighted ITS with 44 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.
(14) Obligation:
IntTrs with 44 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, i6, env, static) -{0,0}> main_Load_3(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_3(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_23(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_23(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, i4, i6, env, static) -{1,1}> main_Load_41(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_41(i1, i4, i6, env, static) -{0,0}> main_Load_42(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_42(i1, i4, i6, env, static) -{0,0}> main_Load_43(i1, i4, i6, env, static) :|: 0 <= static
main_Load_43(i1, i4, i6, env, static) -{0,0}> main_Load_48(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_48(i1, i4, i6, env, static) -{0,0}> main_Load_49(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i1, i4, i6, env, static) -{1,1}> main_Load_51(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_51(i1, i4, i6, env, static) -{1,1}> main_Load_53(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_53(i1, i4, i6, env, static) -{1,1}> main_IntArithmetic_54(i1, i4, i6, env, static) :|: 0 >= 0
main_IntArithmetic_54(i1, i4, i6, env, static) -{1,1}> main_LE_59(i1, i4, i6, i8, env, static) :|: i4 + i6 = i8
main_LE_59(i1, i4, i6, i8, env, static) -{0,0}> main_LE_60(i1, i4, i6, i8, env, static) :|: i1 <= i8
main_LE_59(i1, i4, i6, i8, env, static) -{0,0}> main_LE_61(i1, i4, i6, i8, env, static) :|: i8 < i1
main_LE_61(i1, i4, i6, i8, env, static) -{1,1}> main_Inc_72(i1, i4, i6, env, static) :|: i8 < i1
main_Inc_72(i1, i4, i6, env, static) -{1,1}> main_Inc_74(i1, i4, i6, i12, env, static) :|: i4 + 1 = i12
main_Inc_74(i1, i4, i6, i12, env, static) -{1,1}> main_JMP_75(i1, i4, i6, i12, i13, env, static) :|: i6 + 1 = i13
main_JMP_75(i1, i4, i6, i12, i13, env, static) -{0,0}> main_JMP_135(i1, i4, i6, i12, i13, env, static) :|: 0 >= 0
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_139(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_139(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_142(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_142(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_149(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_149(i1, i4, i6, i43, i48, env, static) -{1,1}> main_IntArithmetic_151(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_IntArithmetic_151(i1, i4, i6, i43, i48, env, static) -{1,1}> main_LE_166(i1, i4, i6, i63, i43, i48, env, static) :|: i43 + i48 = i63
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{0,0}> main_LE_171(i1, i4, i6, i63, i43, i48, env, static) :|: i1 <= i63
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{0,0}> main_LE_172(i1, i4, i6, i63, i43, i48, env, static) :|: i63 < i1
main_LE_172(i1, i4, i6, i63, i43, i48, env, static) -{1,1}> main_Inc_182(i1, i4, i6, i43, i48, env, static) :|: i63 < i1
main_Inc_182(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Inc_189(i1, i4, i6, i81, i48, env, static) :|: i43 + 1 = i81
main_Inc_189(i1, i4, i6, i81, i48, env, static) -{1,1}> main_JMP_195(i1, i4, i6, i81, i86, env, static) :|: i48 + 1 = i86
main_JMP_195(i1, i4, i6, i81, i86, env, static) -{0,0}> main_JMP_135(i1, i4, i6, i81, i86, env, static) :|: 0 >= 0
(15) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_Load_2(
i1,
i4,
i6,
env,
static) -{19,19}>
main_LE_59(
i1,
i4,
i6,
i8',
env,
static'1) :|:
i4 +
i6 =
i8' &&
0 <
2 &&
0 <=
static'1 &&
0 <=
static &&
0 <=
1 &&
0 <
1 &&
static''' <=
static +
2 &&
0 <=
static''' &&
0 <=
2 && 0 >= 0 &&
static'1 <=
static''' +
1by chaining
main_Load_2(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_3(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_3(
i1,
i4,
i6,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_6(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i1,
i4,
i6,
env,
static) :|:
iconst_0 =
0langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_13(
a2,
i1,
i4,
i6,
iconst_0,
env,
static) :|:
a2 =
2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_13(
a2,
i1,
i4,
i6,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_14(
i1,
i4,
i6,
env,
static') :|:
0 <=
a2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_14(
i1,
i4,
i6,
env,
static) -{0,0}>
langle_clinit_rangle_New_16(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
langle_clinit_rangle_New_16(
i1,
i4,
i6,
env,
static) -{0,0}>
langle_clinit_rangle_New_17(
i1,
i4,
i6,
env,
static) :|:
0 <=
staticlangle_clinit_rangle_New_17(
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_19(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2 &&
o2 =
1langle_clinit_rangle_Duplicate_19(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_21(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_clinit_rangle_ConstantStackPush_21(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_22(
o2,
NULL,
i1,
i4,
i6,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_clinit_rangle_InvokeMethod_22(
o2,
NULL,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_Load_23(
o2,
i1,
i4,
i6,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_init_rangle_Load_23(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_26(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_26(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_Load_27(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_Load_27(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_30(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_30(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_Return_32(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_Return_32(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_Return_34(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_Return_34(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_36(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_clinit_rangle_FieldAccess_36(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_Return_38(
i1,
i4,
i6,
env,
static') :|:
0 <
o2 &&
0 <=
o2 &&
0 <=
static &&
static' <=
static +
o2langle_clinit_rangle_Return_38(
i1,
i4,
i6,
env,
static) -{1,1}>
main_Load_41(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_41(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_42(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_42(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_43(
i1,
i4,
i6,
env,
static) :|:
0 <=
staticmain_Load_43(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_48(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_48(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_49(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_49(
i1,
i4,
i6,
env,
static) -{1,1}>
main_Load_51(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_51(
i1,
i4,
i6,
env,
static) -{1,1}>
main_Load_53(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_53(
i1,
i4,
i6,
env,
static) -{1,1}>
main_IntArithmetic_54(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_IntArithmetic_54(
i1,
i4,
i6,
env,
static) -{1,1}>
main_LE_59(
i1,
i4,
i6,
i8,
env,
static) :|:
i4 +
i6 =
i8obtained
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i12', i13', env, static) :|: 0 >= 0 && i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
by chaining
main_LE_59(i1, i4, i6, i8, env, static) -{0,0}> main_LE_61(i1, i4, i6, i8, env, static) :|: i8 < i1
main_LE_61(i1, i4, i6, i8, env, static) -{1,1}> main_Inc_72(i1, i4, i6, env, static) :|: i8 < i1
main_Inc_72(i1, i4, i6, env, static) -{1,1}> main_Inc_74(i1, i4, i6, i12, env, static) :|: i4 + 1 = i12
main_Inc_74(i1, i4, i6, i12, env, static) -{1,1}> main_JMP_75(i1, i4, i6, i12, i13, env, static) :|: i6 + 1 = i13
main_JMP_75(i1, i4, i6, i12, i13, env, static) -{0,0}> main_JMP_135(i1, i4, i6, i12, i13, env, static) :|: 0 >= 0
obtained
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i63', i43, i48, env, static) :|: 0 >= 0 && i43 + i48 = i63'
by chaining
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_139(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_139(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_142(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_142(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_149(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_149(i1, i4, i6, i43, i48, env, static) -{1,1}> main_IntArithmetic_151(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_IntArithmetic_151(i1, i4, i6, i43, i48, env, static) -{1,1}> main_LE_166(i1, i4, i6, i63, i43, i48, env, static) :|: i43 + i48 = i63
obtained
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i81', i86', env, static) :|: 0 >= 0 && i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
by chaining
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{0,0}> main_LE_172(i1, i4, i6, i63, i43, i48, env, static) :|: i63 < i1
main_LE_172(i1, i4, i6, i63, i43, i48, env, static) -{1,1}> main_Inc_182(i1, i4, i6, i43, i48, env, static) :|: i63 < i1
main_Inc_182(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Inc_189(i1, i4, i6, i81, i48, env, static) :|: i43 + 1 = i81
main_Inc_189(i1, i4, i6, i81, i48, env, static) -{1,1}> main_JMP_195(i1, i4, i6, i81, i86, env, static) :|: i48 + 1 = i86
main_JMP_195(i1, i4, i6, i81, i86, env, static) -{0,0}> main_JMP_135(i1, i4, i6, i81, i86, env, static) :|: 0 >= 0
(16) Obligation:
IntTrs with 6 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, i6, env, static) -{19,19}> main_LE_59(i1, i4, i6, i8', env, static'1) :|: i4 + i6 = i8' && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
main_LE_59(i1, i4, i6, i8, env, static) -{0,0}> main_LE_60(i1, i4, i6, i8, env, static) :|: i1 <= i8
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i12', i13', env, static) :|: 0 >= 0 && i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i63', i43, i48, env, static) :|: 0 >= 0 && i43 + i48 = i63'
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{0,0}> main_LE_171(i1, i4, i6, i63, i43, i48, env, static) :|: i1 <= i63
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i81', i86', env, static) :|: 0 >= 0 && i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
(17) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i12', i13', env, static) :|: 0 >= 0 && i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
was transformed to
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1, env, static) :|: 0 >= 0 && i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i63', i43, i48, env, static) :|: 0 >= 0 && i43 + i48 = i63'
was transformed to
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i43 + i48, i43, i48, env, static) :|: 0 >= 0 && i43 + i48 = i63'
main_Load_2(i1, i4, i6, env, static) -{19,19}> main_LE_59(i1, i4, i6, i8', env, static'1) :|: i4 + i6 = i8' && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
was transformed to
main_Load_2(i1, i4, i6, env, static) -{19,19}> main_LE_59(i1, i4, i6, i4 + i6, env, static'1) :|: i4 + i6 = i8' && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i81', i86', env, static) :|: 0 >= 0 && i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
was transformed to
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1, env, static) :|: 0 >= 0 && i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
(18) Obligation:
IntTrs with 6 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1, env, static) :|: 0 >= 0 && i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i43 + i48, i43, i48, env, static) :|: 0 >= 0 && i43 + i48 = i63'
main_LE_59(i1, i4, i6, i8, env, static) -{0,0}> main_LE_60(i1, i4, i6, i8, env, static) :|: i1 <= i8
main_Load_2(i1, i4, i6, env, static) -{19,19}> main_LE_59(i1, i4, i6, i4 + i6, env, static'1) :|: i4 + i6 = i8' && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1, env, static) :|: 0 >= 0 && i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{0,0}> main_LE_171(i1, i4, i6, i63, i43, i48, env, static) :|: i1 <= i63
(19) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
main_Load_2(i1, i4, i6, env, static) -{19,19}> main_LE_59(i1, i4, i6, i4 + i6, env, static'1) :|: i4 + i6 = i8' && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && 0 >= 0 && static'1 <= static''' + 1
was transformed to
main_Load_2(i1, i4, i6, env, static) -{19,19}> main_LE_59(i1, i4, i6, i4 + i6, env, static'1) :|: i4 + i6 = i8' && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1, env, static) :|: 0 >= 0 && i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
was transformed to
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1, env, static) :|: i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i43 + i48, i43, i48, env, static) :|: 0 >= 0 && i43 + i48 = i63'
was transformed to
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i43 + i48, i43, i48, env, static) :|: i43 + i48 = i63'
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1, env, static) :|: 0 >= 0 && i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
was transformed to
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1, env, static) :|: i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
(20) Obligation:
IntTrs with 6 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{5,5}> main_LE_166(i1, i4, i6, i43 + i48, i43, i48, env, static) :|: i43 + i48 = i63'
main_LE_59(i1, i4, i6, i8, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1, env, static) :|: i4 + 1 = i12' && i6 + 1 = i13' && i8 < i1
main_LE_59(i1, i4, i6, i8, env, static) -{0,0}> main_LE_60(i1, i4, i6, i8, env, static) :|: i1 <= i8
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{3,3}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1, env, static) :|: i43 + 1 = i81' && i48 + 1 = i86' && i63 < i1
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{0,0}> main_LE_171(i1, i4, i6, i63, i43, i48, env, static) :|: i1 <= i63
main_Load_2(i1, i4, i6, env, static) -{19,19}> main_LE_59(i1, i4, i6, i4 + i6, env, static'1) :|: i4 + i6 = i8' && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
(21) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(3)) transformation)
Extracted set of 42 edges for the analysis of TIME complexity. Dropped leaves.
(22) Obligation:
Set of 42 edges based on JBC Program.
Performed SCC analyses:
- Used field analysis yielded the following read fields:
Considered paths: all paths from start
(23) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)
Transformed 42 jbc graph edges to a weighted ITS with 42 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Filtered fields of type java.lang.Object.
Did no encode lower bounds for putfield and astore.
(24) Obligation:
IntTrs with 42 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, i6, env, static) -{0,0}> main_Load_3(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_3(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, i6, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, i6, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i1, i4, i6, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, i6, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, i6, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, i6, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, i6, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_23(o2, i1, i4, i6, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_23(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, i6, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, i4, i6, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, i4, i6, env, static) -{1,1}> langle_clinit_rangle_Return_38(i1, i4, i6, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i1, i4, i6, env, static) -{1,1}> main_Load_41(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_41(i1, i4, i6, env, static) -{0,0}> main_Load_42(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_42(i1, i4, i6, env, static) -{0,0}> main_Load_43(i1, i4, i6, env, static) :|: 0 <= static
main_Load_43(i1, i4, i6, env, static) -{0,0}> main_Load_48(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_48(i1, i4, i6, env, static) -{0,0}> main_Load_49(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_49(i1, i4, i6, env, static) -{1,1}> main_Load_51(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_51(i1, i4, i6, env, static) -{1,1}> main_Load_53(i1, i4, i6, env, static) :|: 0 >= 0
main_Load_53(i1, i4, i6, env, static) -{1,1}> main_IntArithmetic_54(i1, i4, i6, env, static) :|: 0 >= 0
main_IntArithmetic_54(i1, i4, i6, env, static) -{1,1}> main_LE_59(i1, i4, i6, i8, env, static) :|: i4 + i6 = i8
main_LE_59(i1, i4, i6, i8, env, static) -{0,0}> main_LE_61(i1, i4, i6, i8, env, static) :|: i8 < i1
main_LE_61(i1, i4, i6, i8, env, static) -{1,1}> main_Inc_72(i1, i4, i6, env, static) :|: i8 < i1
main_Inc_72(i1, i4, i6, env, static) -{1,1}> main_Inc_74(i1, i4, i6, i12, env, static) :|: i4 + 1 = i12
main_Inc_74(i1, i4, i6, i12, env, static) -{1,1}> main_JMP_75(i1, i4, i6, i12, i13, env, static) :|: i6 + 1 = i13
main_JMP_75(i1, i4, i6, i12, i13, env, static) -{0,0}> main_JMP_135(i1, i4, i6, i12, i13, env, static) :|: 0 >= 0
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_139(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_139(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_142(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_142(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_149(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_149(i1, i4, i6, i43, i48, env, static) -{1,1}> main_IntArithmetic_151(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_IntArithmetic_151(i1, i4, i6, i43, i48, env, static) -{1,1}> main_LE_166(i1, i4, i6, i63, i43, i48, env, static) :|: i43 + i48 = i63
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{0,0}> main_LE_172(i1, i4, i6, i63, i43, i48, env, static) :|: i63 < i1
main_LE_172(i1, i4, i6, i63, i43, i48, env, static) -{1,1}> main_Inc_182(i1, i4, i6, i43, i48, env, static) :|: i63 < i1
main_Inc_182(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Inc_189(i1, i4, i6, i81, i48, env, static) :|: i43 + 1 = i81
main_Inc_189(i1, i4, i6, i81, i48, env, static) -{1,1}> main_JMP_195(i1, i4, i6, i81, i86, env, static) :|: i48 + 1 = i86
main_JMP_195(i1, i4, i6, i81, i86, env, static) -{0,0}> main_JMP_135(i1, i4, i6, i81, i86, env, static) :|: 0 >= 0
(25) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
obtained
main_Load_2(
i1,
i4,
i6,
env,
static) -{22,22}>
main_JMP_135(
i1,
i4,
i6,
i12',
i13',
env,
static'1) :|: 0 >= 0 &&
static'1 <=
static''' +
1 &&
i4 +
1 =
i12' &&
0 <=
2 &&
0 <=
static''' &&
static''' <=
static +
2 &&
0 <
1 &&
0 <=
1 &&
0 <=
static &&
0 <=
static'1 &&
i4 +
i6 =
i8' &&
i8' <
i1 &&
i6 +
1 =
i13' &&
0 <
2by chaining
main_Load_2(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_3(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_3(
i1,
i4,
i6,
env,
static) -{0,0}>
langle_clinit_rangle_ConstantStackPush_6(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i1,
i4,
i6,
env,
static) :|:
iconst_0 =
0langle_clinit_rangle_ArrayCreate_12(
iconst_0,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_13(
a2,
i1,
i4,
i6,
iconst_0,
env,
static) :|:
a2 =
2 &&
iconst_0 =
0 &&
0 <
a2langle_clinit_rangle_FieldAccess_13(
a2,
i1,
i4,
i6,
iconst_0,
env,
static) -{1,1}>
langle_clinit_rangle_New_14(
i1,
i4,
i6,
env,
static') :|:
0 <=
a2 &&
iconst_0 =
0 &&
static' <=
static +
a2 &&
0 <=
static &&
0 <
a2langle_clinit_rangle_New_14(
i1,
i4,
i6,
env,
static) -{0,0}>
langle_clinit_rangle_New_16(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
langle_clinit_rangle_New_16(
i1,
i4,
i6,
env,
static) -{0,0}>
langle_clinit_rangle_New_17(
i1,
i4,
i6,
env,
static) :|:
0 <=
staticlangle_clinit_rangle_New_17(
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_Duplicate_19(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2 &&
o2 =
1langle_clinit_rangle_Duplicate_19(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_ConstantStackPush_21(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_clinit_rangle_ConstantStackPush_21(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_InvokeMethod_22(
o2,
NULL,
i1,
i4,
i6,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_clinit_rangle_InvokeMethod_22(
o2,
NULL,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_Load_23(
o2,
i1,
i4,
i6,
env,
static) :|:
NULL =
0 &&
0 <
o2langle_init_rangle_Load_23(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_26(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_26(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_Load_27(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_Load_27(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_InvokeMethod_30(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_InvokeMethod_30(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_Return_32(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_Return_32(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_init_rangle_Return_34(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_init_rangle_Return_34(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_FieldAccess_36(
o2,
i1,
i4,
i6,
env,
static) :|:
0 <
o2langle_clinit_rangle_FieldAccess_36(
o2,
i1,
i4,
i6,
env,
static) -{1,1}>
langle_clinit_rangle_Return_38(
i1,
i4,
i6,
env,
static') :|:
0 <
o2 &&
0 <=
o2 &&
0 <=
static &&
static' <=
static +
o2langle_clinit_rangle_Return_38(
i1,
i4,
i6,
env,
static) -{1,1}>
main_Load_41(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_41(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_42(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_42(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_43(
i1,
i4,
i6,
env,
static) :|:
0 <=
staticmain_Load_43(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_48(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_48(
i1,
i4,
i6,
env,
static) -{0,0}>
main_Load_49(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_49(
i1,
i4,
i6,
env,
static) -{1,1}>
main_Load_51(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_51(
i1,
i4,
i6,
env,
static) -{1,1}>
main_Load_53(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_Load_53(
i1,
i4,
i6,
env,
static) -{1,1}>
main_IntArithmetic_54(
i1,
i4,
i6,
env,
static) :|: 0 >= 0
main_IntArithmetic_54(
i1,
i4,
i6,
env,
static) -{1,1}>
main_LE_59(
i1,
i4,
i6,
i8,
env,
static) :|:
i4 +
i6 =
i8main_LE_59(
i1,
i4,
i6,
i8,
env,
static) -{0,0}>
main_LE_61(
i1,
i4,
i6,
i8,
env,
static) :|:
i8 <
i1main_LE_61(
i1,
i4,
i6,
i8,
env,
static) -{1,1}>
main_Inc_72(
i1,
i4,
i6,
env,
static) :|:
i8 <
i1main_Inc_72(
i1,
i4,
i6,
env,
static) -{1,1}>
main_Inc_74(
i1,
i4,
i6,
i12,
env,
static) :|:
i4 +
1 =
i12main_Inc_74(
i1,
i4,
i6,
i12,
env,
static) -{1,1}>
main_JMP_75(
i1,
i4,
i6,
i12,
i13,
env,
static) :|:
i6 +
1 =
i13main_JMP_75(
i1,
i4,
i6,
i12,
i13,
env,
static) -{0,0}>
main_JMP_135(
i1,
i4,
i6,
i12,
i13,
env,
static) :|: 0 >= 0
obtained
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{8,8}> main_JMP_135(i1, i4, i6, i81', i86', env, static) :|: 0 >= 0 && i43 + 1 = i81' && i63' < i1 && i48 + 1 = i86' && i43 + i48 = i63'
by chaining
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_139(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_139(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_142(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_142(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Load_149(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_Load_149(i1, i4, i6, i43, i48, env, static) -{1,1}> main_IntArithmetic_151(i1, i4, i6, i43, i48, env, static) :|: 0 >= 0
main_IntArithmetic_151(i1, i4, i6, i43, i48, env, static) -{1,1}> main_LE_166(i1, i4, i6, i63, i43, i48, env, static) :|: i43 + i48 = i63
main_LE_166(i1, i4, i6, i63, i43, i48, env, static) -{0,0}> main_LE_172(i1, i4, i6, i63, i43, i48, env, static) :|: i63 < i1
main_LE_172(i1, i4, i6, i63, i43, i48, env, static) -{1,1}> main_Inc_182(i1, i4, i6, i43, i48, env, static) :|: i63 < i1
main_Inc_182(i1, i4, i6, i43, i48, env, static) -{1,1}> main_Inc_189(i1, i4, i6, i81, i48, env, static) :|: i43 + 1 = i81
main_Inc_189(i1, i4, i6, i81, i48, env, static) -{1,1}> main_JMP_195(i1, i4, i6, i81, i86, env, static) :|: i48 + 1 = i86
main_JMP_195(i1, i4, i6, i81, i86, env, static) -{0,0}> main_JMP_135(i1, i4, i6, i81, i86, env, static) :|: 0 >= 0
(26) Obligation:
IntTrs with 2 rules
Start term: main_Load_2(#0, #1, #2, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, i6, env, static) -{22,22}> main_JMP_135(i1, i4, i6, i12', i13', env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && i4 + 1 = i12' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i4 + i6 = i8' && i8' < i1 && i6 + 1 = i13' && 0 < 2
main_JMP_135(i1, i4, i6, i43, i48, env, static) -{8,8}> main_JMP_135(i1, i4, i6, i81', i86', env, static) :|: 0 >= 0 && i43 + 1 = i81' && i63' < i1 && i48 + 1 = i86' && i43 + i48 = i63'
(27) WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID) transformation)
Some arguments are removed because they cannot influence termination. We removed arguments according to the following replacements:
main_Load_2(x1, x2, x3, x4, x5) → main_Load_2(x1, x2, x3, x5)
main_JMP_135(x1, x2, x3, x4, x5, x6, x7) → main_JMP_135(x1, x2, x3, x4, x5)
(28) Obligation:
IntTrs with 2 rules
Start term: main_Load_2(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, i6, static) -{22,22}> main_JMP_135(i1, i4, i6, i12', i13') :|: 0 >= 0 && static'1 <= static''' + 1 && i4 + 1 = i12' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i4 + i6 = i8' && i8' < i1 && i6 + 1 = i13' && 0 < 2
main_JMP_135(i1, i4, i6, i43, i48) -{8,8}> main_JMP_135(i1, i4, i6, i81', i86') :|: 0 >= 0 && i43 + 1 = i81' && i63' < i1 && i48 + 1 = i86' && i43 + i48 = i63'
(29) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Moved arithmethic from constraints to rhss.
main_Load_2(i1, i4, i6, static) -{22,22}> main_JMP_135(i1, i4, i6, i12', i13') :|: 0 >= 0 && static'1 <= static''' + 1 && i4 + 1 = i12' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i4 + i6 = i8' && i8' < i1 && i6 + 1 = i13' && 0 < 2
was transformed to
main_Load_2(i1, i4, i6, static) -{22,22}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1) :|: 0 >= 0 && static'1 <= static''' + 1 && i4 + 1 = i12' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i4 + i6 = i8' && i8' < i1 && i6 + 1 = i13' && 0 < 2
main_JMP_135(i1, i4, i6, i43, i48) -{8,8}> main_JMP_135(i1, i4, i6, i81', i86') :|: 0 >= 0 && i43 + 1 = i81' && i63' < i1 && i48 + 1 = i86' && i43 + i48 = i63'
was transformed to
main_JMP_135(i1, i4, i6, i43, i48) -{8,8}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1) :|: 0 >= 0 && i43 + 1 = i81' && i63' < i1 && i48 + 1 = i86' && i43 + i48 = i63'
(30) Obligation:
IntTrs with 2 rules
Start term: main_Load_2(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, i6, static) -{22,22}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1) :|: 0 >= 0 && static'1 <= static''' + 1 && i4 + 1 = i12' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i4 + i6 = i8' && i8' < i1 && i6 + 1 = i13' && 0 < 2
main_JMP_135(i1, i4, i6, i43, i48) -{8,8}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1) :|: 0 >= 0 && i43 + 1 = i81' && i63' < i1 && i48 + 1 = i86' && i43 + i48 = i63'
(31) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)
Simplified expressions.
main_Load_2(i1, i4, i6, static) -{22,22}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1) :|: 0 >= 0 && static'1 <= static''' + 1 && i4 + 1 = i12' && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && i4 + i6 = i8' && i8' < i1 && i6 + 1 = i13' && 0 < 2
was transformed to
main_Load_2(i1, i4, i6, static) -{22,22}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1) :|: static'1 <= static''' + 1 && i4 + 1 = i12' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i4 + i6 = i8' && i8' < i1 && i6 + 1 = i13'
main_JMP_135(i1, i4, i6, i43, i48) -{8,8}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1) :|: 0 >= 0 && i43 + 1 = i81' && i63' < i1 && i48 + 1 = i86' && i43 + i48 = i63'
was transformed to
main_JMP_135(i1, i4, i6, i43, i48) -{8,8}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1) :|: i43 + 1 = i81' && i63' < i1 && i48 + 1 = i86' && i43 + i48 = i63'
(32) Obligation:
IntTrs with 2 rules
Start term: main_Load_2(#0, #1, #2, static)
Considered paths: all paths from start
Rules:
main_JMP_135(i1, i4, i6, i43, i48) -{8,8}> main_JMP_135(i1, i4, i6, i43 + 1, i48 + 1) :|: i43 + 1 = i81' && i63' < i1 && i48 + 1 = i86' && i43 + i48 = i63'
main_Load_2(i1, i4, i6, static) -{22,22}> main_JMP_135(i1, i4, i6, i4 + 1, i6 + 1) :|: static'1 <= static''' + 1 && i4 + 1 = i12' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i4 + i6 = i8' && i8' < i1 && i6 + 1 = i13'
(33) koat Proof (EQUIVALENT transformation)
YES(?, 8*ar_0 + 8*ar_1 + 8*ar_2 + 22)
Initial complexity problem:
1: T:
(Comp: ?, Cost: 8) main_JMP_135(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_JMP_135(ar_0, ar_1, ar_2, ar_3 + 1, ar_4 + 1)) [ ar_3 + 1 = i81' /\ i63' < ar_0 /\ ar_4 + 1 = i86' /\ ar_3 + ar_4 = i63' ]
(Comp: ?, Cost: 22) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_JMP_135(ar_0, ar_1, ar_2, ar_1 + 1, ar_2 + 1)) [ static'1 <= static''' + 1 /\ ar_1 + 1 = i12' /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_1 + ar_2 = i8' /\ i8' < ar_0 /\ ar_2 + 1 = i13' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 8) main_JMP_135(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_JMP_135(ar_0, ar_1, ar_2, ar_3 + 1, ar_4 + 1)) [ ar_3 + 1 = i81' /\ i63' < ar_0 /\ ar_4 + 1 = i86' /\ ar_3 + ar_4 = i63' ]
(Comp: 1, Cost: 22) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_JMP_135(ar_0, ar_1, ar_2, ar_1 + 1, ar_2 + 1)) [ static'1 <= static''' + 1 /\ ar_1 + 1 = i12' /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_1 + ar_2 = i8' /\ i8' < ar_0 /\ ar_2 + 1 = i13' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
A polynomial rank function with
Pol(main_JMP_135) = V_1 - V_4 - V_5
Pol(main_Load_2) = V_1 - V_2 - V_3
Pol(koat_start) = V_1 - V_2 - V_3
orients all transitions weakly and the transition
main_JMP_135(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_JMP_135(ar_0, ar_1, ar_2, ar_3 + 1, ar_4 + 1)) [ ar_3 + 1 = i81' /\ i63' < ar_0 /\ ar_4 + 1 = i86' /\ ar_3 + ar_4 = i63' ]
strictly and produces the following problem:
3: T:
(Comp: ar_0 + ar_1 + ar_2, Cost: 8) main_JMP_135(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_JMP_135(ar_0, ar_1, ar_2, ar_3 + 1, ar_4 + 1)) [ ar_3 + 1 = i81' /\ i63' < ar_0 /\ ar_4 + 1 = i86' /\ ar_3 + ar_4 = i63' ]
(Comp: 1, Cost: 22) main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_JMP_135(ar_0, ar_1, ar_2, ar_1 + 1, ar_2 + 1)) [ static'1 <= static''' + 1 /\ ar_1 + 1 = i12' /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 /\ ar_1 + ar_2 = i8' /\ i8' < ar_0 /\ ar_2 + 1 = i13' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0
Complexity upper bound 8*ar_0 + 8*ar_1 + 8*ar_2 + 22
Time: 0.225 sec (SMT: 0.189 sec)
(34) BOUNDS(CONSTANT, 22 + 8 * |#0| + 8 * |#1| + 8 * |#2|)