LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
f3437_0__init__GE f3437_0__init__GE f3437_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
f3438_0__init__GE f3438_0__init__GE f3438_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
f6761_0_removeRange_GE f6761_0_removeRange_GE f6761_0_removeRange_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
f3396_0__init__GE f3396_0__init__GE f3396_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
f3043_0__init__LE f3043_0__init__LE f3043_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
f850_0_createList_Load f850_0_createList_Load f850_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
__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
f500_0_createList_Return f500_0_createList_Return f500_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
f6942_0_remove_FieldAccess f6942_0_remove_FieldAccess f6942_0_remove_FieldAccess: 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
f477_0_createList_Load f477_0_createList_Load f477_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
f6944_0_remove_FieldAccess f6944_0_remove_FieldAccess f6944_0_remove_FieldAccess: 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
f6947_0_remove_FieldAccess f6947_0_remove_FieldAccess f6947_0_remove_FieldAccess: 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
f2250_0_createList_LE f2250_0_createList_LE f2250_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
f2336_0_random_ArrayAccess f2336_0_random_ArrayAccess f2336_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
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
f3395_0__init__GE f3395_0__init__GE f3395_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
f6913_0_remove_FieldAccess f6913_0_remove_FieldAccess f6913_0_remove_FieldAccess: 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 7 SCC(s) of the program graph.

2.1 SCC Subproblem 1/7

Here we consider the SCC { f3438_0__init__GE }.

2.1.1 Transition Removal

We remove transitions 19, 20 using the following ranking functions, which are bounded by 0.

f3438_0__init__GE: x3x10

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/7

Here we consider the SCC { f3437_0__init__GE }.

2.2.1 Transition Removal

We remove transitions 17, 18 using the following ranking functions, which are bounded by 0.

f3437_0__init__GE: x3x11

2.2.2 Trivial Cooperation Program

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

2.3 SCC Subproblem 3/7

Here we consider the SCC { f3396_0__init__GE }.

2.3.1 Transition Removal

We remove transition 16 using the following ranking functions, which are bounded by 0.

f3396_0__init__GE: x3x5

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/7

Here we consider the SCC { f3395_0__init__GE }.

2.4.1 Transition Removal

We remove transition 15 using the following ranking functions, which are bounded by 0.

f3395_0__init__GE: x3x6

2.4.2 Trivial Cooperation Program

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

2.5 SCC Subproblem 5/7

Here we consider the SCC { f3043_0__init__LE }.

2.5.1 Transition Removal

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

f3043_0__init__LE: x4 + x13

2.5.2 Trivial Cooperation Program

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

2.6 SCC Subproblem 6/7

Here we consider the SCC { f2250_0_createList_LE }.

2.6.1 Transition Removal

We remove transitions 37, 38 using the following ranking functions, which are bounded by 0.

f2250_0_createList_LE: x2

2.6.2 Trivial Cooperation Program

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

2.7 SCC Subproblem 7/7

Here we consider the SCC { f6942_0_remove_FieldAccess, f6944_0_remove_FieldAccess, f6761_0_removeRange_GE, f6947_0_remove_FieldAccess, f6913_0_remove_FieldAccess }.

2.7.1 Transition Removal

We remove transitions 26, 27 using the following ranking functions, which are bounded by 0.

f6942_0_remove_FieldAccess: −1 − x1 + x2
f6947_0_remove_FieldAccess: −1 − x1 + x2
f6913_0_remove_FieldAccess: −1 − x1 + x2
f6761_0_removeRange_GE: x2 + x3
f6944_0_remove_FieldAccess: −1 − x1 + x2

2.7.2 Transition Removal

We remove transitions 1, 28, 31, 29, 34, 33, 32, 30 using the following ranking functions, which are bounded by −1.

f6942_0_remove_FieldAccess: 0
f6947_0_remove_FieldAccess: −1
f6913_0_remove_FieldAccess: x17 + x6 − 1
f6944_0_remove_FieldAccess: −1
f6761_0_removeRange_GE: −2

2.7.3 Trivial Cooperation Program

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

Tool configuration

AProVE