LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
f456_0_createList_Return f456_0_createList_Return f456_0_createList_Return: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f11135_0_indexOf_EQ f11135_0_indexOf_EQ f11135_0_indexOf_EQ: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f4420_0_createList_LE f4420_0_createList_LE f4420_0_createList_LE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f9903_0_hasNext_EQ f9903_0_hasNext_EQ f9903_0_hasNext_EQ: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f10686_0_indexOf_EQ f10686_0_indexOf_EQ f10686_0_indexOf_EQ: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f1844_0_createList_LE f1844_0_createList_LE f1844_0_createList_LE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f817_0_createList_Load f817_0_createList_Load f817_0_createList_Load: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f11144_0_indexOf_EQ f11144_0_indexOf_EQ f11144_0_indexOf_EQ: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
__init __init __init: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f11013_0_indexOf_EQ f11013_0_indexOf_EQ f11013_0_indexOf_EQ: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f11014_0_indexOf_EQ f11014_0_indexOf_EQ f11014_0_indexOf_EQ: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f2543_0_createList_Return f2543_0_createList_Return f2543_0_createList_Return: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f2892_0_createList_Load f2892_0_createList_Load f2892_0_createList_Load: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f431_0_createList_Load f431_0_createList_Load f431_0_createList_Load: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f3144_0__init__GE f3144_0__init__GE f3144_0__init__GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f11138_0_indexOf_EQ f11138_0_indexOf_EQ f11138_0_indexOf_EQ: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f3426_0__init__LE f3426_0__init__LE f3426_0__init__LE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f10687_0_indexOf_EQ f10687_0_indexOf_EQ f10687_0_indexOf_EQ: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f11141_0_indexOf_EQ f11141_0_indexOf_EQ f11141_0_indexOf_EQ: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f1901_0_random_ArrayAccess f1901_0_random_ArrayAccess f1901_0_random_ArrayAccess: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f2525_0_createList_Load f2525_0_createList_Load f2525_0_createList_Load: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
f1_0_main_Load f1_0_main_Load f1_0_main_Load: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13x14 = x14x15 = x15x16 = x16x17 = x17x18 = x18x19 = x19x20 = x20x21 = x21x22 = x22x23 = x23x24 = x24x25 = x25x26 = x26x27 = x27x28 = x28
and for every transition t, a duplicate t is considered.

2 SCC Decomposition

We consider subproblems for each of the 4 SCC(s) of the program graph.

2.1 SCC Subproblem 1/4

Here we consider the SCC { f3426_0__init__LE }.

2.1.1 Transition Removal

We remove transitions 8, 9, 10, 11, 12 using the following ranking functions, which are bounded by 0.

f3426_0__init__LE: x25

2.1.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.2 SCC Subproblem 2/4

Here we consider the SCC { f11135_0_indexOf_EQ, f11013_0_indexOf_EQ, f11014_0_indexOf_EQ, f11138_0_indexOf_EQ, f9903_0_hasNext_EQ, f10687_0_indexOf_EQ, f11141_0_indexOf_EQ, f10686_0_indexOf_EQ, f11144_0_indexOf_EQ }.

2.2.1 Transition Removal

We remove transitions 26, 52, 54, 39, 35, 24 using the following ranking functions, which are bounded by 0.

f9903_0_hasNext_EQ: −2
f10686_0_indexOf_EQ: −2 + x7
f10687_0_indexOf_EQ: −2 + x7
f11135_0_indexOf_EQ: −2 − x5 + 3⋅x7
f11013_0_indexOf_EQ: −2 + 3⋅x8
f11141_0_indexOf_EQ: −2 − x5 + 3⋅x7
f11014_0_indexOf_EQ: −2 + 3⋅x8
f11144_0_indexOf_EQ: −2
f11138_0_indexOf_EQ: −2

2.2.2 Transition Removal

We remove transitions 18, 19, 28, 29, 41, 37 using the following ranking functions, which are bounded by 0.

f9903_0_hasNext_EQ: −1 + 2⋅x12 − 2⋅x13
f10686_0_indexOf_EQ: −1 + 2⋅x13 − 2⋅x14
f10687_0_indexOf_EQ: −1 + 2⋅x13 − 2⋅x14
f11013_0_indexOf_EQ: 2⋅x14 − 2⋅x15
f11135_0_indexOf_EQ: 0⋅x5 + 2⋅x13 − 2⋅x14
f11014_0_indexOf_EQ: 2⋅x14 − 2⋅x15
f11141_0_indexOf_EQ: 0⋅x5 + 2⋅x13 − 2⋅x14
f11144_0_indexOf_EQ: x5 + 2⋅x10 − 2⋅x11
f11138_0_indexOf_EQ: x5 + 2⋅x10 − 2⋅x11

2.2.3 Transition Removal

We remove transitions 55, 53, 27, 22, 23, 25, 20, 21 using the following ranking functions, which are bounded by 0.

f11013_0_indexOf_EQ: −1
f11135_0_indexOf_EQ: −1 + 0⋅x5
f11014_0_indexOf_EQ: −1
f11141_0_indexOf_EQ: −1 + 0⋅x5
f11144_0_indexOf_EQ: −1 + 2⋅x5
f9903_0_hasNext_EQ: −1 + x4
f11138_0_indexOf_EQ: −1 + 2⋅x5
f10687_0_indexOf_EQ: x8
f10686_0_indexOf_EQ: −1 + x8

2.2.4 Transition Removal

We remove transitions 38, 40, 45, 46, 47 using the following ranking functions, which are bounded by 0.

f11013_0_indexOf_EQ: 2 − x5 + x9 + x14 + x15 + x16 − 6⋅x17 + x18 + x19 + x20 − 3⋅x21 + x22
f11135_0_indexOf_EQ: 1 − x4 + 0⋅x5 + x9 + x13 + x14 + x15 − 6⋅x16 + x17 + x18 + x21 − 3⋅x22 + x23
f11014_0_indexOf_EQ: 4 + x9 + x14x15
f11141_0_indexOf_EQ: 4 + 0⋅x5 + x9 + x13x14
f11144_0_indexOf_EQ: 4 + 0⋅x5 + x6 + x10x11
f11138_0_indexOf_EQ: 1 − x4 + 0⋅x5 + x6 + x10 + x11 + x12 − 6⋅x13 + x14 + x15 + x20 − 3⋅x21 + x22

2.2.5 Transition Removal

We remove transitions 50, 51 using the following ranking functions, which are bounded by 0.

f11013_0_indexOf_EQ: −20 + x5 + x9 + x14 + x15 + x16 + x17 + x18 + x19 + x20 + x21 − 3⋅x22
f11135_0_indexOf_EQ: −19 + x4 + 0⋅x5 + x9 + x13 + x14 + x15 + x16 + x17 + x18 + x21 + x22 − 3⋅x23
f11141_0_indexOf_EQ: 0⋅x5
f11014_0_indexOf_EQ: −1
f11144_0_indexOf_EQ: 0⋅x5
f11138_0_indexOf_EQ: −19 + x4 + 0⋅x5 + x6 + x10 + x11 + x12 + x13 + x14 + x15 + x20 + x21 − 3⋅x22

2.2.6 Transition Removal

We remove transitions 34, 36, 42, 43, 44 using the following ranking functions, which are bounded by 0.

f11013_0_indexOf_EQ: x9 + x14x15
f11135_0_indexOf_EQ: 0⋅x5 + x9 + x13x14
f11138_0_indexOf_EQ: 0⋅x5 + x6 + x10x11

2.2.7 Transition Removal

We remove transitions 48, 49 using the following ranking functions, which are bounded by 0.

f11135_0_indexOf_EQ: 0⋅x5
f11013_0_indexOf_EQ: −1
f11138_0_indexOf_EQ: 0⋅x5

2.2.8 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.3 SCC Subproblem 3/4

Here we consider the SCC { f4420_0_createList_LE }.

2.3.1 Transition Removal

We remove transitions 62, 63 using the following ranking functions, which are bounded by 0.

f4420_0_createList_LE: x2

2.3.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.4 SCC Subproblem 4/4

Here we consider the SCC { f1844_0_createList_LE }.

2.4.1 Transition Removal

We remove transitions 58, 59 using the following ranking functions, which are bounded by 0.

f1844_0_createList_LE: x2

2.4.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

Tool configuration

AProVE