LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
f5710_0_hasNext_NULL f5710_0_hasNext_NULL f5710_0_hasNext_NULL: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f5883_0_nextEntry_GE f5883_0_nextEntry_GE f5883_0_nextEntry_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f4901_0__init__GE f4901_0__init__GE f4901_0__init__GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f4226_0_createMap_LE f4226_0_createMap_LE f4226_0_createMap_LE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f535_0_createMap_Return f535_0_createMap_Return f535_0_createMap_Return: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f5848_0_transfer_ArrayAccess f5848_0_transfer_ArrayAccess f5848_0_transfer_ArrayAccess: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f4680_0__init__LE f4680_0__init__LE f4680_0__init__LE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
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 = x13
f5714_0_transfer_GE f5714_0_transfer_GE f5714_0_transfer_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f4961_0_put_EQ f4961_0_put_EQ f4961_0_put_EQ: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
__init __init __init: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f4846_0_put_NULL f4846_0_put_NULL f4846_0_put_NULL: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
and for every transition t, a duplicate t is considered.

2 SCC Decomposition

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

2.1 SCC Subproblem 1/5

Here we consider the SCC { f4226_0_createMap_LE }.

2.1.1 Transition Removal

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

f4226_0_createMap_LE: x2

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

Here we consider the SCC { f4961_0_put_EQ, f4846_0_put_NULL }.

2.2.1 Transition Removal

We remove transitions 15, 17, 18, 19, 20, 21, 16 using the following ranking functions, which are bounded by 0.

f4846_0_put_NULL: 1 + x4
f4961_0_put_EQ: x3

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

Here we consider the SCC { f5848_0_transfer_ArrayAccess, f5714_0_transfer_GE }.

2.3.1 Transition Removal

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

f5714_0_transfer_GE: −2⋅x4 + 2⋅x8 + 1
f5848_0_transfer_ArrayAccess: −2⋅x3 + 2⋅x10

2.3.2 Transition Removal

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

f5714_0_transfer_GE: −1 − x4 + x7 + x8
f5848_0_transfer_ArrayAccess: −2 − x3 + x10 + x13

2.3.3 Transition Removal

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

f5848_0_transfer_ArrayAccess: x4
f5714_0_transfer_GE: −1

2.3.4 Trivial Cooperation Program

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

2.4 SCC Subproblem 4/5

Here we consider the SCC { f4901_0__init__GE }.

2.4.1 Transition Removal

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

f4901_0__init__GE: x3 + x6

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

Here we consider the SCC { f5710_0_hasNext_NULL, f5883_0_nextEntry_GE }.

2.5.1 Transition Removal

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

f5710_0_hasNext_NULL: x3 + x5
f5883_0_nextEntry_GE: x3 + x6

2.5.2 Transition Removal

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

f5710_0_hasNext_NULL: x2
f5883_0_nextEntry_GE: x2

2.5.3 Trivial Cooperation Program

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

Tool configuration

AProVE