LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
f532_0_createMap_Return f532_0_createMap_Return f532_0_createMap_Return: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f5950_0_nextEntry_GE f5950_0_nextEntry_GE f5950_0_nextEntry_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f5790_0_hasNext_NULL f5790_0_hasNext_NULL f5790_0_hasNext_NULL: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f4279_0_createMap_LE f4279_0_createMap_LE f4279_0_createMap_LE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f5935_0_transfer_ArrayAccess f5935_0_transfer_ArrayAccess f5935_0_transfer_ArrayAccess: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f4729_0__init__LE f4729_0__init__LE f4729_0__init__LE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f5797_0_transfer_GE f5797_0_transfer_GE f5797_0_transfer_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11x12 = x12x13 = x13
f4900_0_put_NULL f4900_0_put_NULL f4900_0_put_NULL: 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
f4935_0__init__GE f4935_0__init__GE f4935_0__init__GE: 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
f5022_0_put_EQ f5022_0_put_EQ f5022_0_put_EQ: 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 { f4279_0_createMap_LE }.

2.1.1 Transition Removal

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

f4279_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 { f4900_0_put_NULL, f5022_0_put_EQ }.

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.

f4900_0_put_NULL: 1 + x4
f5022_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 { f5935_0_transfer_ArrayAccess, f5797_0_transfer_GE }.

2.3.1 Transition Removal

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

f5797_0_transfer_GE: −2⋅x4 + 2⋅x8 + 1
f5935_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.

f5797_0_transfer_GE: −2⋅x4 + 2⋅x8 + 2
f5935_0_transfer_ArrayAccess: −2⋅x3 + 2⋅x10 + 1

2.3.3 Transition Removal

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

f5935_0_transfer_ArrayAccess: x4
f5797_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 { f4935_0__init__GE }.

2.4.1 Transition Removal

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

f4935_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 { f5950_0_nextEntry_GE, f5790_0_hasNext_NULL }.

2.5.1 Transition Removal

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

f5790_0_hasNext_NULL: x3 + x5
f5950_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.

f5790_0_hasNext_NULL: x2
f5950_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