0 JBC
↳1 JBCToGraph (⇒, 940 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 11 ms)
↳4 JBCTerminationSCC
↳5 SCCToIntTRSProof (⇒, 99 ms)
↳6 intTRS
↳7 TerminationGraphProcessor (⇒, 0 ms)
↳8 AND
↳9 intTRS
↳10 PolynomialOrderProcessor (⇔, 0 ms)
↳11 YES
↳12 intTRS
↳13 PolynomialOrderProcessor (⇔, 0 ms)
↳14 YES
/**
* 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 PastaC11 {
public static void main(String[] args) {
Random.args = args;
int x = Random.random();
int y = Random.random();
while (true) {
if (x >= 0) {
x--;
y = Random.random();
} else if (y >= 0) {
y--;
} else {
break;
}
}
}
}
public class Random {
static String[] args;
static int index = 0;
public static int random() {
String string = args[index];
index++;
return string.length();
}
}
Generated rules. Obtained 33 IRules
P rules:
f2155_0_main_LT(EOS, matching1, i779, matching2) → f2156_0_main_LT(EOS, -1, i779, -1) | &&(=(matching1, -1), =(matching2, -1))
f2155_0_main_LT(EOS, i789, i779, i789) → f2157_0_main_LT(EOS, i789, i779, i789)
f2156_0_main_LT(EOS, matching1, i779, matching2) → f2159_0_main_Load(EOS, -1, i779) | &&(&&(<(-1, 0), =(matching1, -1)), =(matching2, -1))
f2159_0_main_Load(EOS, matching1, i779) → f2163_0_main_LT(EOS, -1, i779, i779) | =(matching1, -1)
f2163_0_main_LT(EOS, matching1, i795, i795) → f2169_0_main_LT(EOS, -1, i795, i795) | =(matching1, -1)
f2169_0_main_LT(EOS, matching1, i795, i795) → f2174_0_main_Inc(EOS, -1, i795) | &&(>=(i795, 0), =(matching1, -1))
f2174_0_main_Inc(EOS, matching1, i795) → f2179_0_main_JMP(EOS, -1, +(i795, -1)) | &&(>=(i795, 0), =(matching1, -1))
f2179_0_main_JMP(EOS, matching1, i797) → f2193_0_main_Load(EOS, -1, i797) | =(matching1, -1)
f2193_0_main_Load(EOS, matching1, i797) → f2147_0_main_Load(EOS, -1, i797) | =(matching1, -1)
f2147_0_main_Load(EOS, i778, i779) → f2155_0_main_LT(EOS, i778, i779, i778)
f2157_0_main_LT(EOS, i789, i779, i789) → f2161_0_main_Inc(EOS, i789) | >=(i789, 0)
f2161_0_main_Inc(EOS, i789) → f2165_0_main_InvokeMethod(EOS, +(i789, -1)) | >=(i789, 0)
f2165_0_main_InvokeMethod(EOS, i793) → f2170_0_random_FieldAccess(EOS, i793)
f2170_0_random_FieldAccess(EOS, i793) → f2183_0_random_FieldAccess(EOS, i793)
f2183_0_random_FieldAccess(EOS, i793) → f2200_0_random_ArrayAccess(EOS, i793)
f2200_0_random_ArrayAccess(EOS, i793) → f2712_0_random_ArrayAccess(EOS, i793)
f2712_0_random_ArrayAccess(EOS, i793) → f2718_0_random_Store(EOS, i793, o754)
f2718_0_random_Store(EOS, i793, o754) → f2724_0_random_FieldAccess(EOS, i793, o754)
f2724_0_random_FieldAccess(EOS, i793, o754) → f2728_0_random_ConstantStackPush(EOS, i793, o754)
f2728_0_random_ConstantStackPush(EOS, i793, o754) → f2736_0_random_IntArithmetic(EOS, i793, o754)
f2736_0_random_IntArithmetic(EOS, i793, o754) → f2741_0_random_FieldAccess(EOS, i793, o754)
f2741_0_random_FieldAccess(EOS, i793, o754) → f2745_0_random_Load(EOS, i793, o754)
f2745_0_random_Load(EOS, i793, o754) → f2760_0_random_InvokeMethod(EOS, i793, o754)
f2760_0_random_InvokeMethod(EOS, i793, java.lang.Object(o782sub)) → f2765_0_random_InvokeMethod(EOS, i793, java.lang.Object(o782sub))
f2765_0_random_InvokeMethod(EOS, i793, java.lang.Object(o782sub)) → f2770_0_length_Load(EOS, i793, java.lang.Object(o782sub), java.lang.Object(o782sub))
f2770_0_length_Load(EOS, i793, java.lang.Object(o782sub), java.lang.Object(o782sub)) → f2789_0_length_FieldAccess(EOS, i793, java.lang.Object(o782sub), java.lang.Object(o782sub))
f2789_0_length_FieldAccess(EOS, i793, java.lang.Object(java.lang.String(o795sub, i1032)), java.lang.Object(java.lang.String(o795sub, i1032))) → f2791_0_length_FieldAccess(EOS, i793, java.lang.Object(java.lang.String(o795sub, i1032)), java.lang.Object(java.lang.String(o795sub, i1032))) | >=(i1032, 0)
f2791_0_length_FieldAccess(EOS, i793, java.lang.Object(java.lang.String(o795sub, i1032)), java.lang.Object(java.lang.String(o795sub, i1032))) → f2805_0_length_Return(EOS, i793, java.lang.Object(java.lang.String(o795sub, i1032)), i1032)
f2805_0_length_Return(EOS, i793, java.lang.Object(java.lang.String(o795sub, i1032)), i1032) → f2813_0_random_Return(EOS, i793, i1032)
f2813_0_random_Return(EOS, i793, i1032) → f2816_0_main_Store(EOS, i793, i1032)
f2816_0_main_Store(EOS, i793, i1032) → f2831_0_main_JMP(EOS, i793, i1032)
f2831_0_main_JMP(EOS, i793, i1032) → f2847_0_main_Load(EOS, i793, i1032)
f2847_0_main_Load(EOS, i793, i1032) → f2147_0_main_Load(EOS, i793, i1032)
Combined rules. Obtained 2 IRules
P rules:
f2155_0_main_LT(EOS, -1, x1, -1) → f2155_0_main_LT(EOS, -1, -(x1, 1), -1) | >(+(x1, 1), 0)
f2155_0_main_LT(EOS, x0, x1, x0) → f2155_0_main_LT(EOS, -(x0, 1), x2, -(x0, 1)) | &&(>(+(x2, 1), 0), >(+(x0, 1), 0))
Filtered ground terms:
f2155_0_main_LT(x1, x2, x3, x4) → f2155_0_main_LT(x2, x3, x4)
Cond_f2155_0_main_LT(x1, x2, x3, x4, x5) → Cond_f2155_0_main_LT(x1, x4)
Cond_f2155_0_main_LT1(x1, x2, x3, x4, x5, x6) → Cond_f2155_0_main_LT1(x1, x3, x4, x5, x6)
Filtered duplicate terms:
f2155_0_main_LT(x1, x2, x3) → f2155_0_main_LT(x2, x3)
Cond_f2155_0_main_LT1(x1, x2, x3, x4, x5) → Cond_f2155_0_main_LT1(x1, x3, x4, x5)
Filtered unneeded terms:
Cond_f2155_0_main_LT1(x1, x2, x3, x4) → Cond_f2155_0_main_LT1(x1, x3, x4)
Prepared 2 rules for path length conversion:
P rules:
f2155_0_main_LT(x1, -1) → f2155_0_main_LT(-(x1, 1), -1) | >(+(x1, 1), 0)
f2155_0_main_LT(x1, x0) → f2155_0_main_LT(x2, -(x0, 1)) | &&(>(+(x2, 1), 0), >(+(x0, 1), 0))
Finished conversion. Obtained 2 rules.
P rules:
f2155_0_main_LT(x0, cm1) → f2155_0_main_LT(-(x0, 1), -1) | &&(>(x0, -1), =(-1, cm1))
f2155_0_main_LT(x1, x2) → f2155_0_main_LT(x3, -(x2, 1)) | &&(>(x2, -1), >(x3, -1))
Constructed the termination graph and obtained 2 non-trivial SCCs.
Found the following polynomial interpretation:
Therefore the following rule(s) have been dropped:
Found the following polynomial interpretation:
Therefore the following rule(s) have been dropped: