LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
f826_0_binarySearch_LE' f826_0_binarySearch_LE' f826_0_binarySearch_LE': x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
f1076_0_binarySearch_EQ f1076_0_binarySearch_EQ f1076_0_binarySearch_EQ: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
f242_0_createArray_Return f242_0_createArray_Return f242_0_createArray_Return: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
f826_0_binarySearch_LE f826_0_binarySearch_LE f826_0_binarySearch_LE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
f1078_0_binarySearch_EQ f1078_0_binarySearch_EQ f1078_0_binarySearch_EQ: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
f382_0_random_ArrayAccess f382_0_random_ArrayAccess f382_0_random_ArrayAccess: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
f1_0_main_Load f1_0_main_Load f1_0_main_Load: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
f464_0_createArray_GE f464_0_createArray_GE f464_0_createArray_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
__init __init __init: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
and for every transition t, a duplicate t is considered.

2 SCC Decomposition

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

2.1 SCC Subproblem 1/2

Here we consider the SCC { f464_0_createArray_GE }.

2.1.1 Transition Removal

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

f464_0_createArray_GE: x4 + x3

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

Here we consider the SCC { f826_0_binarySearch_LE', f1076_0_binarySearch_EQ, f826_0_binarySearch_LE, f1078_0_binarySearch_EQ }.

2.2.1 Transition Removal

We remove transitions 6, 8, 7, 9, 10, 25, 24, 19, 18, 15, 14, 23, 22, 17, 16, 12 using the following ranking functions, which are bounded by 0.

f826_0_binarySearch_LE: −3⋅x4 + 2⋅x5 + 2⋅x6 + 2
f826_0_binarySearch_LE': −3⋅x4 + 2⋅x5 + 2⋅x6 + 1
f1078_0_binarySearch_EQ: −3⋅x4 + 2⋅x3 + 2⋅x7
f1076_0_binarySearch_EQ: −3⋅x4 + 2⋅x3 + 2⋅x7

2.2.2 Transition Removal

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

f1078_0_binarySearch_EQ: 0⋅x5
f826_0_binarySearch_LE: −1
f826_0_binarySearch_LE': −1
f1076_0_binarySearch_EQ: −1 + 0⋅x5

2.2.3 Transition Removal

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

f826_0_binarySearch_LE: −3⋅x4 + 3⋅x6
f826_0_binarySearch_LE': −3⋅x4 + 3⋅x6 − 1
f1076_0_binarySearch_EQ: −3⋅x4 + 3⋅x7 − 2

2.2.4 Transition Removal

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

f1076_0_binarySearch_EQ: 0⋅x5
f826_0_binarySearch_LE: −1

2.2.5 Trivial Cooperation Program

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

Tool configuration

AProVE