LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
f2753_0_insert_NONNULL f2753_0_insert_NONNULL f2753_0_insert_NONNULL: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
f1598_0_main_InvokeMethod f1598_0_main_InvokeMethod f1598_0_main_InvokeMethod: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
f2353_0_createCollection_GE f2353_0_createCollection_GE f2353_0_createCollection_GE: 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
f2751_0_insert_NONNULL f2751_0_insert_NONNULL f2751_0_insert_NONNULL: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
f202_0_createCollection_Return f202_0_createCollection_Return f202_0_createCollection_Return: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
f2789_0_createCollection_InvokeMethod f2789_0_createCollection_InvokeMethod f2789_0_createCollection_InvokeMethod: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
__init __init __init: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
f89_0_createCollection_LE f89_0_createCollection_LE f89_0_createCollection_LE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7
f1863_0_minimum_NONNULL f1863_0_minimum_NONNULL f1863_0_minimum_NONNULL: 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 4 SCC(s) of the program graph.

2.1 SCC Subproblem 1/4

Here we consider the SCC { f2353_0_createCollection_GE, f2789_0_createCollection_InvokeMethod }.

2.1.1 Transition Removal

We remove transitions 16, 22, 23, 17, 24, 26, 28, 30, 32, 34, 36, 37, 35, 33, 31, 29, 27, 25 using the following ranking functions, which are bounded by 0.

f2353_0_createCollection_GE: 1 − 2⋅x2 + 2⋅x3
f2789_0_createCollection_InvokeMethod: 2⋅x1 − 2⋅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/4

Here we consider the SCC { f2753_0_insert_NONNULL }.

2.2.1 Transition Removal

We remove transitions 40, 41, 42 using the following ranking functions, which are bounded by 0.

f2753_0_insert_NONNULL: x2

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

Here we consider the SCC { f2751_0_insert_NONNULL }.

2.3.1 Transition Removal

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

f2751_0_insert_NONNULL: 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 { f1863_0_minimum_NONNULL }.

2.4.1 Transition Removal

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

f1863_0_minimum_NONNULL: x1 + 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