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
l7 l7 l7: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
l11 l11 l11: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
l1 l1 l1: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
l13 l13 l13: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
l3 l3 l3: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
l2 l2 l2: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
l9 l9 l9: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
l14 l14 l14: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
l4 l4 l4: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
l6 l6 l6: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
l10 l10 l10: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
l8 l8 l8: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
l15 l15 l15: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
l16 l16 l16: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
l0 l0 l0: x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 ∧ x10 = x10
and for every transition t, a duplicate t is considered.

2 SCC Decomposition

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

2.1 SCC Subproblem 1/3

Here we consider the SCC { l1, l3, l0, l2 }.

2.1.1 Transition Removal

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

l0: 19 − x6
l1: 19 − x6
l3: 18 − x6
l2: 18 − x6

2.1.2 Transition Removal

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

l0: 0
l1: −1
l3: 1
l2: 1

2.1.3 Transition Removal

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

l2: 19 − x3
l3: 19 − x3

2.1.4 Transition Removal

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

l2: 0
l3: −1

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

Here we consider the SCC { l5, l4, l13, l14 }.

2.2.1 Transition Removal

We remove transition 15 using the following ranking functions, which are bounded by −57.

l4: −3⋅x7 + 1
l5: −3⋅x7
l14: −3⋅x7 − 1
l13: −3⋅x7 − 1

2.2.2 Transition Removal

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

l4: 0
l5: −1
l14: 1
l13: 1

2.2.3 Transition Removal

We remove transition 13 using the following ranking functions, which are bounded by −38.

l13: −2⋅x4 + 1
l14: −2⋅x4

2.2.4 Transition Removal

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

l13: 0
l14: −1

2.2.5 Trivial Cooperation Program

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

2.3 SCC Subproblem 3/3

Here we consider the SCC { l7, l10, l6, l11, l8, l9 }.

2.3.1 Transition Removal

We remove transition 9 using the following ranking functions, which are bounded by −55.

l10: −3⋅x5 + 3
l11: −3⋅x5 + 2
l9: −3⋅x5 + 1
l7: −3⋅x5 + 1
l6: −3⋅x5 + 1
l8: −3⋅x5 + 1

2.3.2 Transition Removal

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

l10: 0
l11: −1
l9: 1
l7: 1
l6: 1
l8: 1

2.3.3 Transition Removal

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

l7: −3⋅x2 + 1
l9: −3⋅x2
l6: −3⋅x2 − 1
l8: −3⋅x2 − 1

2.3.4 Transition Removal

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

l7: 19 − x1
l9: 19 − x1
l6: 19 − x1
l8: 19 − x1

2.3.5 Transition Removal

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

l7: 0
l9: −1
l6: 1
l8: 2

2.3.6 Trivial Cooperation Program

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

Tool configuration

AProVE