LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
f2260_0_jaro_GE f2260_0_jaro_GE f2260_0_jaro_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f8074_0_append_GE f8074_0_append_GE f8074_0_append_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f2059_0_hamming_Return f2059_0_hamming_Return f2059_0_hamming_Return: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f8972_0_main_GT f8972_0_main_GT f8972_0_main_GT: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f1_0_main_ConstantStackPush f1_0_main_ConstantStackPush f1_0_main_ConstantStackPush: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f2057_0_hamming_Return f2057_0_hamming_Return f2057_0_hamming_Return: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f4039_0_hamming_GE f4039_0_hamming_GE f4039_0_hamming_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
__init __init __init: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f6098_0_levenshtein_ArrayAccess f6098_0_levenshtein_ArrayAccess f6098_0_levenshtein_ArrayAccess: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f1034_0_levenshtein_GT f1034_0_levenshtein_GT f1034_0_levenshtein_GT: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f833_0__init__GE' f833_0__init__GE' f833_0__init__GE': x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f5323_0_levenshtein_ArrayAccess f5323_0_levenshtein_ArrayAccess f5323_0_levenshtein_ArrayAccess: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f4567_0_levenshtein_GE f4567_0_levenshtein_GE f4567_0_levenshtein_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f8879_0_jaro_GE f8879_0_jaro_GE f8879_0_jaro_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f5542_0_levenshtein_ArrayAccess f5542_0_levenshtein_ArrayAccess f5542_0_levenshtein_ArrayAccess: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f537_0_main_InvokeMethod f537_0_main_InvokeMethod f537_0_main_InvokeMethod: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f2058_0_hamming_Return f2058_0_hamming_Return f2058_0_hamming_Return: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f1232_0_levenshtein_GT f1232_0_levenshtein_GT f1232_0_levenshtein_GT: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f6023_0_min_LE f6023_0_min_LE f6023_0_min_LE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f5888_0_min_LE f5888_0_min_LE f5888_0_min_LE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f7279_0_jaro_Return f7279_0_jaro_Return f7279_0_jaro_Return: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f2549_0_levenshtein_GE f2549_0_levenshtein_GE f2549_0_levenshtein_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f6656_0_jaro_GT f6656_0_jaro_GT f6656_0_jaro_GT: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f5195_0_levenshtein_ArrayAccess f5195_0_levenshtein_ArrayAccess f5195_0_levenshtein_ArrayAccess: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f833_0__init__GE f833_0__init__GE f833_0__init__GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f894_0_main_GE f894_0_main_GE f894_0_main_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f2260_0_jaro_GE' f2260_0_jaro_GE' f2260_0_jaro_GE': x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f7552_0_jaro_InvokeMethod f7552_0_jaro_InvokeMethod f7552_0_jaro_InvokeMethod: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f1960_0_jaro_GE f1960_0_jaro_GE f1960_0_jaro_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f6831_0_findMatch_Return f6831_0_findMatch_Return f6831_0_findMatch_Return: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f7277_0_jaro_Return f7277_0_jaro_Return f7277_0_jaro_Return: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f7489_0_findMatch_GE f7489_0_findMatch_GE f7489_0_findMatch_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f537_0_main_InvokeMethod' f537_0_main_InvokeMethod' f537_0_main_InvokeMethod': x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f6456_0_jaro_GE f6456_0_jaro_GE f6456_0_jaro_GE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f7275_0_jaro_Return f7275_0_jaro_Return f7275_0_jaro_Return: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
f6616_0_min_LE f6616_0_min_LE f6616_0_min_LE: x1 = x1x2 = x2x3 = x3x4 = x4x5 = x5x6 = x6x7 = x7x8 = x8x9 = x9x10 = x10x11 = x11
and for every transition t, a duplicate t is considered.

2 SCC Decomposition

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

2.1 SCC Subproblem 1/12

Here we consider the SCC { f537_0_main_InvokeMethod, f894_0_main_GE, f8972_0_main_GT, f537_0_main_InvokeMethod' }.

2.1.1 Transition Removal

We remove transitions 24, 22, 19, 17, 14, 3, 10, 6, 82, 80, 78, 59, 57, 55, 33, 31, 29, 21, 18, 16, 13, 9, 5 using the following ranking functions, which are bounded by 0.

f537_0_main_InvokeMethod: 1 − 3⋅x2 + 3⋅x3
f537_0_main_InvokeMethod': −3⋅x2 + 3⋅x3
f8972_0_main_GT: 2 − 3⋅x2 + 3⋅x3
f894_0_main_GE: −1 − 3⋅x2 + 3⋅x4

2.1.2 Transition Removal

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

f537_0_main_InvokeMethod: 1
f537_0_main_InvokeMethod': 0
f894_0_main_GE: −1 + x2 + x4
f8972_0_main_GT: −2 + x2 + x3

2.1.3 Transition Removal

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

f894_0_main_GE: x4
f8972_0_main_GT: −1 + x3

2.1.4 Transition Removal

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

f894_0_main_GE: x3

2.1.5 Trivial Cooperation Program

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

2.2 SCC Subproblem 2/12

Here we consider the SCC { f833_0__init__GE', f833_0__init__GE }.

2.2.1 Transition Removal

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

f833_0__init__GE: −2⋅x3 + 2⋅x4 + 1
f833_0__init__GE': −2⋅x3 + 2⋅x4

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

Here we consider the SCC { f4039_0_hamming_GE }.

2.3.1 Transition Removal

We remove transitions 84, 85 using the following ranking functions, which are bounded by 0.

f4039_0_hamming_GE: x2 + x3

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

Here we consider the SCC { f1960_0_jaro_GE }.

2.4.1 Transition Removal

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

f1960_0_jaro_GE: x2 + x3

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

Here we consider the SCC { f2260_0_jaro_GE }.

2.5.1 Transition Removal

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

f2260_0_jaro_GE: x2 + x3

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

Here we consider the SCC { f6656_0_jaro_GT, f6456_0_jaro_GE, f6616_0_min_LE }.

2.6.1 Transition Removal

We remove transitions 66, 67, 72 using the following ranking functions, which are bounded by 0.

f6456_0_jaro_GE: −1 − 2⋅x4 + 2⋅x6
f6616_0_min_LE: −2 − 2⋅x4 + 2⋅x8
f6656_0_jaro_GT: −2 − 2⋅x4 + 2⋅x7

2.6.2 Transition Removal

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

f6656_0_jaro_GT: 0
f6456_0_jaro_GE: −1
f6616_0_min_LE: 0

2.6.3 Transition Removal

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

f6616_0_min_LE: −1 − x4x5 + 2⋅x8
f6656_0_jaro_GT: −1 − x4x5 + 2⋅x7

2.6.4 Transition Removal

We remove transitions 68, 69 using the following ranking functions, which are bounded by 0.

f6616_0_min_LE: 1
f6656_0_jaro_GT: 0

2.6.5 Trivial Cooperation Program

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

2.7 SCC Subproblem 7/12

Here we consider the SCC { f7489_0_findMatch_GE }.

2.7.1 Transition Removal

We remove transitions 88, 89, 90 using the following ranking functions, which are bounded by 0.

f7489_0_findMatch_GE: x4 + x5

2.7.2 Trivial Cooperation Program

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

2.8 SCC Subproblem 8/12

Here we consider the SCC { f8074_0_append_GE }.

2.8.1 Transition Removal

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

f8074_0_append_GE: x3 + x5

2.8.2 Trivial Cooperation Program

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

2.9 SCC Subproblem 9/12

Here we consider the SCC { f8879_0_jaro_GE }.

2.9.1 Transition Removal

We remove transitions 76, 77 using the following ranking functions, which are bounded by 0.

f8879_0_jaro_GE: x3 + x4 + x5

2.9.2 Trivial Cooperation Program

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

2.10 SCC Subproblem 10/12

Here we consider the SCC { f1034_0_levenshtein_GT }.

2.10.1 Transition Removal

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

f1034_0_levenshtein_GT: x3 + x4

2.10.2 Trivial Cooperation Program

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

2.11 SCC Subproblem 11/12

Here we consider the SCC { f1232_0_levenshtein_GT }.

2.11.1 Transition Removal

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

f1232_0_levenshtein_GT: x3 + x4

2.11.2 Trivial Cooperation Program

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

2.12 SCC Subproblem 12/12

Here we consider the SCC { f6023_0_min_LE, f5888_0_min_LE, f5323_0_levenshtein_ArrayAccess, f4567_0_levenshtein_GE, f2549_0_levenshtein_GE, f5195_0_levenshtein_ArrayAccess, f5542_0_levenshtein_ArrayAccess, f6098_0_levenshtein_ArrayAccess }.

2.12.1 Transition Removal

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

f2549_0_levenshtein_GE: −3⋅x3 + 3⋅x4
f4567_0_levenshtein_GE: −3⋅x3 + 3⋅x5 − 1
f5195_0_levenshtein_ArrayAccess: −3⋅x3 + 3⋅x7 − 1
f6098_0_levenshtein_ArrayAccess: −3⋅x3 + 3⋅x7 − 1
f6023_0_min_LE: −3⋅x3 + 3⋅x9 − 1
f5888_0_min_LE: −3⋅x3 + 3⋅x10 − 1
f5542_0_levenshtein_ArrayAccess: −3⋅x2 + 3⋅x9 − 1
f5323_0_levenshtein_ArrayAccess: −3⋅x2 + 3⋅x9 − 1

2.12.2 Transition Removal

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

f4567_0_levenshtein_GE: 0
f2549_0_levenshtein_GE: −1
f5195_0_levenshtein_ArrayAccess: 0
f6098_0_levenshtein_ArrayAccess: 0
f6023_0_min_LE: 0
f5888_0_min_LE: 0
f5542_0_levenshtein_ArrayAccess: 0
f5323_0_levenshtein_ArrayAccess: 0

2.12.3 Transition Removal

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

f5195_0_levenshtein_ArrayAccess: −2 − x3x4 + x7 + 2⋅x8
f4567_0_levenshtein_GE: −1 − x3x4 + x5 + 2⋅x6
f6098_0_levenshtein_ArrayAccess: −2 − x3x4 + x7 + 2⋅x8
f6023_0_min_LE: −2 − x3x4 + x9 + 2⋅x10
f5888_0_min_LE: −2 − x3x4 + x10 + 2⋅x11
f5542_0_levenshtein_ArrayAccess: −2 − x2x8 + x9 + 2⋅x10
f5323_0_levenshtein_ArrayAccess: −2 − x2x3 + x9 + 2⋅x10

2.12.4 Transition Removal

We remove transitions 53, 54, 52, 51, 50, 49, 48, 47, 46, 45 using the following ranking functions, which are bounded by 0.

f5195_0_levenshtein_ArrayAccess: 0
f4567_0_levenshtein_GE: −1
f6098_0_levenshtein_ArrayAccess: −1 + x5
f6023_0_min_LE: x5
f5888_0_min_LE: 1 + x5
f5542_0_levenshtein_ArrayAccess: 1 + x3 + x7
f5323_0_levenshtein_ArrayAccess: 1 + x4 + 2⋅x7

2.12.5 Trivial Cooperation Program

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

Tool configuration

AProVE