LTS Termination Proof

by AProVE

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
l5 l5 l5: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l22 l22 l22: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l1 l1 l1: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l13 l13 l13: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l18 l18 l18: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l17 l17 l17: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l21 l21 l21: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l9 l9 l9: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l14 l14 l14: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l25 l25 l25: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l8 l8 l8: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l27 l27 l27: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l0 l0 l0: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l12 l12 l12: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l19 l19 l19: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l26 l26 l26: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l7 l7 l7: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l24 l24 l24: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l11 l11 l11: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l3 l3 l3: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l20 l20 l20: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l28 l28 l28: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l2 l2 l2: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l23 l23 l23: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l4 l4 l4: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l10 l10 l10: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l29 l29 l29: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l15 l15 l15: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
l16 l16 l16: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10 ∧ x11 = x11 ∧ x12 = x12 ∧ x13 = x13 ∧ x14 = x14 ∧ x15 = x15
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 { l23, l22, l25, l24, l27, l26 }.

2.1.1 Transition Removal

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

l22: −1 − x5 + x10
l23: −1 − x5 + x10
l24: −1 − x5 + x10
l25: −1 − x5 + x10
l27: − x5 + x10
l26: − x5 + x10

2.1.2 Transition Removal

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

l22: 2
l23: 2
l24: 2
l25: 2
l26: 0
l27: −1

2.1.3 Transition Removal

We remove transitions 34, 32 using the following ranking functions, which are bounded by 0.

l22: −1 + x5 − x7
l23: x5 − x7
l24: x5 − x7
l25: x5 − x7

2.1.4 Transition Removal

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

l22: −1 − x7 + x10
l23: − x7 + x10
l24: −1 − x7 + x10
l25: − x7 + x10

2.1.5 Transition Removal

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

l22: 1
l23: 0
l24: 2
l25: −1

2.1.6 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 { l7, l1, l13, l20, l18, l17, l21, l8, l16, l15, l0, l12, l19 }.

2.2.1 Transition Removal

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

l0: −2 − x4 + x9
l1: −2 − x4 + x9
l21: −1 − x4 + x9
l17: −1 − x4 + x9
l13: −2 − x4 + x9
l12: −2 − x4 + x9
l16: −2 − x4 + x9
l15: −2 − x4 + x9
l18: −2 − x4 + x9
l20: −2 − x4 + x9
l8: −2 − x4 + x9
l7: −2 − x4 + x9
l19: −2 − x4 + x9

2.2.2 Transition Removal

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

l0: 2
l1: 2
l17: 0
l21: −1
l13: 1
l12: 1
l16: 1
l15: 1
l18: 2
l20: 2
l8: 2
l7: 2
l19: 2

2.2.3 Transition Removal

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

l0: −1 + 2⋅x1 + 3⋅x2 + 4⋅x3 + x4 + 5⋅x5 − x6 + 6⋅x7 − x9 + 7⋅x10 + 8⋅x11 + 9⋅x12 + 10⋅x13 + 11⋅x15
l1: −2 + 2⋅x1 + 3⋅x2 + 4⋅x3 + x4 + 5⋅x5 − x6 + 6⋅x7 − x9 + 7⋅x10 + 8⋅x11 + 9⋅x12 + 10⋅x13 + 11⋅x15
l12: − x6 + x9
l13: − x6 + x9
l16: −1 − x6 + x9
l15: −1 − x6 + x9
l18: −2 + 2⋅x1 + 3⋅x2 + 4⋅x3 + x4 + 5⋅x5 − x6 + 6⋅x7 − x9 + 7⋅x10 + 8⋅x11 + 9⋅x12 + 10⋅x13 + 11⋅x15
l20: −2 + 2⋅x1 + 3⋅x2 + 4⋅x3 + x4 + 5⋅x5 − x6 + 6⋅x7 − x9 + 7⋅x10 + 8⋅x11 + 9⋅x12 + 10⋅x13 + 11⋅x15
l8: −2 + 2⋅x1 + 3⋅x2 + 4⋅x3 + x4 + 5⋅x5 − x6 + 6⋅x7 − x9 + 7⋅x10 + 8⋅x11 + 9⋅x12 + 10⋅x13 + 11⋅x15
l7: −2 + 2⋅x1 + 3⋅x2 + 4⋅x3 + x4 + 5⋅x5 − x6 + 6⋅x7 − x9 + 7⋅x10 + 8⋅x11 + 9⋅x12 + 10⋅x13 + 11⋅x15
l19: −2 + 2⋅x1 + 3⋅x2 + 4⋅x3 + x4 + 5⋅x5 − x6 + 6⋅x7 − x9 + 7⋅x10 + 8⋅x11 + 9⋅x12 + 10⋅x13 + 11⋅x15

2.2.4 Transition Removal

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

l0: −1 + 2⋅x1 + 3⋅x2 + 4⋅x3 + x4 + 5⋅x5 − 2⋅x6 + 6⋅x7 + x9 + 7⋅x10 + 8⋅x11 + 9⋅x12 + 10⋅x13 + 11⋅x15
l1: −3 + 2⋅x1 + 3⋅x2 + 4⋅x3 + x4 + 5⋅x5 − 2⋅x6 + 6⋅x7 + x9 + 7⋅x10 + 8⋅x11 + 9⋅x12 + 10⋅x13 + 11⋅x15
l12: x4 − x8
l13: x4 − x8
l16: x4 − x8
l15: x4 − x8
l18: −3 + 2⋅x1 + 3⋅x2 + 4⋅x3 + x4 + 5⋅x5 − 2⋅x6 + 6⋅x7 + x9 + 7⋅x10 + 8⋅x11 + 9⋅x12 + 10⋅x13 + 11⋅x15
l20: −3 + 2⋅x1 + 3⋅x2 + 4⋅x3 + x4 + 5⋅x5 − 2⋅x6 + 6⋅x7 + x9 + 7⋅x10 + 8⋅x11 + 9⋅x12 + 10⋅x13 + 11⋅x15
l8: −3 + 2⋅x1 + 3⋅x2 + 4⋅x3 + x4 + 5⋅x5 − 2⋅x6 + 6⋅x7 + x9 + 7⋅x10 + 8⋅x11 + 9⋅x12 + 10⋅x13 + 11⋅x15
l7: −3 + 2⋅x1 + 3⋅x2 + 4⋅x3 + x4 + 5⋅x5 − 2⋅x6 + 6⋅x7 + x9 + 7⋅x10 + 8⋅x11 + 9⋅x12 + 10⋅x13 + 11⋅x15
l19: −3 + 2⋅x1 + 3⋅x2 + 4⋅x3 + x4 + 5⋅x5 − 2⋅x6 + 6⋅x7 + x9 + 7⋅x10 + 8⋅x11 + 9⋅x12 + 10⋅x13 + 11⋅x15

2.2.5 Transition Removal

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

l0: −1 + 3⋅x1 + 4⋅x2 + 5⋅x3 − x4 + 6⋅x5 − x6 + 7⋅x7 − x9 + 8⋅x10 + 9⋅x11 + 10⋅x12 + 11⋅x13 + 12⋅x15
l1: −2 + 3⋅x1 + 4⋅x2 + 5⋅x3 − x4 + 6⋅x5 − x6 + 7⋅x7 − x9 + 8⋅x10 + 9⋅x11 + 10⋅x12 + 11⋅x13 + 12⋅x15
l12: 0
l13: −1
l16: 1
l15: 2
l18: −2 + 3⋅x1 + 4⋅x2 + 5⋅x3 − x4 + 6⋅x5 − x6 + 7⋅x7 − x9 + 8⋅x10 + 9⋅x11 + 10⋅x12 + 11⋅x13 + 12⋅x15
l20: −2 + 3⋅x1 + 4⋅x2 + 5⋅x3 − x4 + 6⋅x5 − x6 + 7⋅x7 − x9 + 8⋅x10 + 9⋅x11 + 10⋅x12 + 11⋅x13 + 12⋅x15
l8: −2 + 3⋅x1 + 4⋅x2 + 5⋅x3 − x4 + 6⋅x5 − x6 + 7⋅x7 − x9 + 8⋅x10 + 9⋅x11 + 10⋅x12 + 11⋅x13 + 12⋅x15
l7: −2 + 3⋅x1 + 4⋅x2 + 5⋅x3 − x4 + 6⋅x5 − x6 + 7⋅x7 − x9 + 8⋅x10 + 9⋅x11 + 10⋅x12 + 11⋅x13 + 12⋅x15
l19: −2 + 3⋅x1 + 4⋅x2 + 5⋅x3 − x4 + 6⋅x5 − x6 + 7⋅x7 − x9 + 8⋅x10 + 9⋅x11 + 10⋅x12 + 11⋅x13 + 12⋅x15

2.2.6 Transition Removal

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

l0: − x6 + x9
l1: − x6 + x9
l18: −1 − x6 + x9
l20: −1 − x6 + x9
l8: −1 − x6 + x9
l7: −1 − x6 + x9
l19: −1 − x6 + x9

2.2.7 Transition Removal

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

l0: −1 + x4
l1: −1 + x4
l18: −1 + x4
l20: x4
l8: −1 + x4
l7: −1 + x4
l19: −1 + x4

2.2.8 Transition Removal

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

l0: −1 + x4 − x8
l1: −1 + x4 − x8
l18: −1 + x4 − x8
l8: −1 + x4 − x8
l7: −1 + x4 − x8
l19: −1 + x4
l20: −1 + x4

2.2.9 Transition Removal

We remove transitions 1, 18, 19, 6, 21, 25 using the following ranking functions, which are bounded by 0.

l0: 0
l1: −1
l18: 1
l8: 2
l7: 3
l19: 4
l20: 5

2.2.10 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 { l10, l11, l9, l14 }.

2.3.1 Transition Removal

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

l10: − x4 + x9
l14: − x4 + x9
l9: −1 − x4 + x9
l11: −1 − x4 + x9

2.3.2 Transition Removal

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

l10: −1
l14: −1
l9: 0
l11: 0

2.3.3 Transition Removal

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

l10: 0
l14: −1
l11: 2⋅x4 − 2⋅x6 + 1
l9: 2⋅x4 − 2⋅x6

2.3.4 Transition Removal

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

l11: 0
l9: −1

2.3.5 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 { l5, l4, l3, l2 }.

2.4.1 Transition Removal

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

l3: x4
l5: x4
l2: −1 + x4
l4: −1 + x4

2.4.2 Transition Removal

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

l3: 0
l5: −1
l2: 1
l4: 1

2.4.3 Transition Removal

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

l4: − x6 + x9
l2: − x6 + x9

2.4.4 Transition Removal

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

l4: 0
l2: −1

2.4.5 Trivial Cooperation Program

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

Tool configuration

AProVE