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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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 − x3 + x8
l23: −1 − x3 + x8
l24: −1 − x3 + x8
l25: −1 − x3 + x8
l27: − x3 + x8
l26: − x3 + x8

2.1.2 Transition Removal

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

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

2.1.3 Transition Removal

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

l22: −4⋅x5 + 4⋅x8
l23: −4⋅x5 + 4⋅x8 + 3
l24: −4⋅x5 + 4⋅x8 + 1
l25: −4⋅x5 + 4⋅x8 + 2

2.1.4 Transition Removal

We remove transitions 31, 34, 33, 32, 41 using the following ranking functions, which are bounded by −2.

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

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/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 − x2 + x7
l1: −2 − x2 + x7
l21: −1 − x2 + x7
l17: −1 − x2 + x7
l13: −2 − x2 + x7
l12: −2 − x2 + x7
l16: −2 − x2 + x7
l15: −2 − x2 + x7
l18: −2 − x2 + x7
l20: −2 − x2 + x7
l8: −2 − x2 + x7
l7: −2 − x2 + x7
l19: −2 − x2 + x7

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 + x2 + 3⋅x3 − x4 + 4⋅x5 − x7 + 5⋅x8 + 6⋅x9 + 7⋅x10 + 8⋅x11 + 9⋅x13
l1: −2 + 2⋅x1 + x2 + 3⋅x3 − x4 + 4⋅x5 − x7 + 5⋅x8 + 6⋅x9 + 7⋅x10 + 8⋅x11 + 9⋅x13
l12: − x4 + x7
l13: − x4 + x7
l16: −1 − x4 + x7
l15: −1 − x4 + x7
l18: −2 + 2⋅x1 + x2 + 3⋅x3 − x4 + 4⋅x5 − x7 + 5⋅x8 + 6⋅x9 + 7⋅x10 + 8⋅x11 + 9⋅x13
l20: −2 + 2⋅x1 + x2 + 3⋅x3 − x4 + 4⋅x5 − x7 + 5⋅x8 + 6⋅x9 + 7⋅x10 + 8⋅x11 + 9⋅x13
l8: −2 + 2⋅x1 + x2 + 3⋅x3 − x4 + 4⋅x5 − x7 + 5⋅x8 + 6⋅x9 + 7⋅x10 + 8⋅x11 + 9⋅x13
l7: −2 + 2⋅x1 + x2 + 3⋅x3 − x4 + 4⋅x5 − x7 + 5⋅x8 + 6⋅x9 + 7⋅x10 + 8⋅x11 + 9⋅x13
l19: −2 + 2⋅x1 + x2 + 3⋅x3 − x4 + 4⋅x5 − x7 + 5⋅x8 + 6⋅x9 + 7⋅x10 + 8⋅x11 + 9⋅x13

2.2.4 Transition Removal

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

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

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 − x2 + 4⋅x3 − x4 + 5⋅x5 − x7 + 6⋅x8 + 7⋅x9 + 8⋅x10 + 9⋅x11 + 10⋅x13
l1: −2 + 3⋅x1 − x2 + 4⋅x3 − x4 + 5⋅x5 − x7 + 6⋅x8 + 7⋅x9 + 8⋅x10 + 9⋅x11 + 10⋅x13
l12: 0
l13: −1
l16: 1
l15: 2
l18: −2 + 3⋅x1 − x2 + 4⋅x3 − x4 + 5⋅x5 − x7 + 6⋅x8 + 7⋅x9 + 8⋅x10 + 9⋅x11 + 10⋅x13
l20: −2 + 3⋅x1 − x2 + 4⋅x3 − x4 + 5⋅x5 − x7 + 6⋅x8 + 7⋅x9 + 8⋅x10 + 9⋅x11 + 10⋅x13
l8: −2 + 3⋅x1 − x2 + 4⋅x3 − x4 + 5⋅x5 − x7 + 6⋅x8 + 7⋅x9 + 8⋅x10 + 9⋅x11 + 10⋅x13
l7: −2 + 3⋅x1 − x2 + 4⋅x3 − x4 + 5⋅x5 − x7 + 6⋅x8 + 7⋅x9 + 8⋅x10 + 9⋅x11 + 10⋅x13
l19: −2 + 3⋅x1 − x2 + 4⋅x3 − x4 + 5⋅x5 − x7 + 6⋅x8 + 7⋅x9 + 8⋅x10 + 9⋅x11 + 10⋅x13

2.2.6 Transition Removal

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

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

2.2.7 Transition Removal

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

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

2.2.8 Transition Removal

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

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

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: − x2 + x7
l14: − x2 + x7
l9: −1 − x2 + x7
l11: −1 − x2 + x7

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⋅x2 − 2⋅x4 + 1
l9: 2⋅x2 − 2⋅x4

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: 3⋅x2 + 2
l5: 3⋅x2 + 1
l2: 3⋅x2
l4: 3⋅x2

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: − x4 + x7
l2: − x4 + x7

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