LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 17 0: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0
2 24 2: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0
4 31 4: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0
6 38 6: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0
9 45 9: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 8, 13, 15, 16 using the following ranking functions, which are bounded by −23.

12: 0
11: 0
0: 0
1: 0
2: 0
3: 0
4: 0
5: 0
6: 0
7: 0
8: 0
9: 0
10: 0
12: −6
11: −7
0: −8
1: −8
2: −8
3: −8
0_var_snapshot: −8
0*: −8
2_var_snapshot: −8
2*: −8
4: −11
5: −11
6: −11
7: −11
8: −11
9: −11
4_var_snapshot: −11
4*: −11
6_var_snapshot: −11
6*: −11
9_var_snapshot: −11
9*: −11
10: −16

3 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

0* 20 0: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0

4 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

0 18 0_var_snapshot: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0

5 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

2* 27 2: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0

6 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

2 25 2_var_snapshot: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0

7 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

4* 34 4: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0

8 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

4 32 4_var_snapshot: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0

9 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

6* 41 6: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0

10 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

6 39 6_var_snapshot: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0

11 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

9* 48 9: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0

12 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

9 46 9_var_snapshot: − k6_post + k6_post ≤ 0 ∧ k6_post − k6_post ≤ 0 ∧ − k6_0 + k6_0 ≤ 0 ∧ k6_0 − k6_0 ≤ 0 ∧ − j5_post + j5_post ≤ 0 ∧ j5_post − j5_post ≤ 0 ∧ − j5_0 + j5_0 ≤ 0 ∧ j5_0 − j5_0 ≤ 0 ∧ − i4_post + i4_post ≤ 0 ∧ i4_post − i4_post ≤ 0 ∧ − i4_0 + i4_0 ≤ 0 ∧ i4_0 − i4_0 ≤ 0 ∧ − ___const_5_0 + ___const_5_0 ≤ 0 ∧ ___const_5_0 − ___const_5_0 ≤ 0

13 SCC Decomposition

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

13.1 SCC Subproblem 1/2

Here we consider the SCC { 4, 5, 6, 7, 8, 9, 4_var_snapshot, 4*, 6_var_snapshot, 6*, 9_var_snapshot, 9* }.

13.1.1 Transition Removal

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

4: 10 + 12⋅___const_5_0 − 12⋅i4_0
5: 8 + 12⋅___const_5_0 − 12⋅i4_0
6: 12⋅___const_5_0 − 12⋅i4_0
7: 12⋅___const_5_0 − 12⋅i4_0
8: 12⋅___const_5_0 − 12⋅i4_0
9: 12⋅___const_5_0 − 12⋅i4_0
4_var_snapshot: 9 + 12⋅___const_5_0 − 12⋅i4_0
4*: 11 + 12⋅___const_5_0 − 12⋅i4_0
6_var_snapshot: 12⋅___const_5_0 − 12⋅i4_0
6*: 12⋅___const_5_0 − 12⋅i4_0
9_var_snapshot: 12⋅___const_5_0 − 12⋅i4_0
9*: 12⋅___const_5_0 − 12⋅i4_0

13.1.2 Transition Removal

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

4: −1 + 12⋅___const_5_0 − 12⋅j5_0
5: −3 + 12⋅___const_5_0 − 12⋅j5_0
6: 3 + 12⋅___const_5_0 − 12⋅j5_0
7: 1 + 12⋅___const_5_0 − 12⋅j5_0
8: 12⋅___const_5_0 − 12⋅j5_0
9: 12⋅___const_5_0 − 12⋅j5_0
4_var_snapshot: −2 + 12⋅___const_5_0 − 12⋅j5_0
4*: 12⋅___const_5_0 − 12⋅j5_0
6_var_snapshot: 2 + 12⋅___const_5_0 − 12⋅j5_0
6*: 4 + 12⋅___const_5_0 − 12⋅j5_0
9_var_snapshot: 12⋅___const_5_0 − 12⋅j5_0
9*: 12⋅___const_5_0 − 12⋅j5_0

13.1.3 Transition Removal

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

4: −5 + 4⋅___const_5_0 − 4⋅k6_0
5: −7 + 4⋅___const_5_0 − 4⋅k6_0
6: −2 + 4⋅___const_5_0 − 4⋅k6_0
7: −4 + 4⋅___const_5_0 − 4⋅k6_0
8: −1 + 4⋅___const_5_0 − 4⋅k6_0
9: 1 + 4⋅___const_5_0 − 4⋅k6_0
4_var_snapshot: −6 + 4⋅___const_5_0 − 4⋅k6_0
4*: −4 + 4⋅___const_5_0 − 4⋅k6_0
6_var_snapshot: −3 + 4⋅___const_5_0 − 4⋅k6_0
6*: −1 + 4⋅___const_5_0 − 4⋅k6_0
9_var_snapshot: 4⋅___const_5_0 − 4⋅k6_0
9*: 2 + 4⋅___const_5_0 − 4⋅k6_0

13.1.4 Transition Removal

We remove transitions 32, 34, 39, 41, 46, 48, 2, 3, 4, 6, 10 using the following ranking functions, which are bounded by −9.

4: −7
5: −9
6: −3
7: −5
8: −1
9: 1
4_var_snapshot: −8
4*: −6
6_var_snapshot: −4
6*: −2
9_var_snapshot: 0
9*: 2

13.1.5 Splitting Cut-Point Transitions

We consider 3 subproblems corresponding to sets of cut-point transitions as follows.

13.1.5.1 Cut-Point Subproblem 1/3

Here we consider cut-point transition 31.

13.1.5.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

13.1.5.2 Cut-Point Subproblem 2/3

Here we consider cut-point transition 38.

13.1.5.2.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

13.1.5.3 Cut-Point Subproblem 3/3

Here we consider cut-point transition 45.

13.1.5.3.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

13.2 SCC Subproblem 2/2

Here we consider the SCC { 0, 1, 2, 3, 0_var_snapshot, 0*, 2_var_snapshot, 2* }.

13.2.1 Transition Removal

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

0: 2 + 9⋅___const_5_0 − 9⋅i4_0
1: 9⋅___const_5_0 − 9⋅i4_0
2: −6 + 9⋅___const_5_0 − 9⋅i4_0
3: −6 + 9⋅___const_5_0 − 9⋅i4_0
0_var_snapshot: 1 + 9⋅___const_5_0 − 9⋅i4_0
0*: 2 + 9⋅___const_5_0 − 9⋅i4_0
2_var_snapshot: −6 + 9⋅___const_5_0 − 9⋅i4_0
2*: −6 + 9⋅___const_5_0 − 9⋅i4_0

13.2.2 Transition Removal

We remove transition 12 using the following ranking functions, which are bounded by −1.

0: −2 + 3⋅___const_5_0 − 3⋅j5_0
1: −4 + 3⋅___const_5_0 − 3⋅j5_0
2: 1 + 3⋅___const_5_0 − 3⋅j5_0
3: 3⋅___const_5_0 − 3⋅j5_0
0_var_snapshot: −3 + 3⋅___const_5_0 − 3⋅j5_0
0*: −1 + 3⋅___const_5_0 − 3⋅j5_0
2_var_snapshot: 3⋅___const_5_0 − 3⋅j5_0
2*: 2 + 3⋅___const_5_0 − 3⋅j5_0

13.2.3 Transition Removal

We remove transitions 18, 20, 25, 27, 0, 11 using the following ranking functions, which are bounded by −4.

0: −2
1: −4
2: 2
3: 0
0_var_snapshot: −3
0*: −1
2_var_snapshot: 1
2*: 3

13.2.4 Transition Removal

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

0: 0
1: 0
2: 0
3: −1
0_var_snapshot: 0
0*: 0
2_var_snapshot: 0
2*: 0

13.2.5 Splitting Cut-Point Transitions

We consider 2 subproblems corresponding to sets of cut-point transitions as follows.

13.2.5.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 17.

13.2.5.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

13.2.5.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 24.

13.2.5.2.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

Tool configuration

T2Cert