LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: TRUE
1: TRUE
2: TRUE
3: TRUE
4: TRUE
5: TRUE
6: TRUE
7: TRUE
8: TRUE
9: TRUE
10: 6 − i4_0 ≤ 0
11: TRUE
12: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 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
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
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
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
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
and for every transition t, a duplicate t is considered.

3 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

4 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

5 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

6 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

7 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

8 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

9 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

10 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

11 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

12 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

13 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

14 SCC Decomposition

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

14.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* }.

14.1.1 Transition Removal

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

4: 13 − 14⋅i4_0
5: 11 − 14⋅i4_0
6: −14⋅i4_0
7: −14⋅i4_0
8: −14⋅i4_0
9: −14⋅i4_0
4_var_snapshot: 12 − 14⋅i4_0
4*: 13 − 14⋅i4_0
6_var_snapshot: −14⋅i4_0
6*: −14⋅i4_0
9_var_snapshot: −14⋅i4_0
9*: −14⋅i4_0

14.1.2 Transition Removal

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

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

14.1.3 Transition Removal

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

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

14.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

14.1.5 Splitting Cut-Point Transitions

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

14.1.5.1 Cut-Point Subproblem 1/3

Here we consider cut-point transition 31.

14.1.5.1.1 Splitting Cut-Point Transitions

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

14.1.5.2 Cut-Point Subproblem 2/3

Here we consider cut-point transition 38.

14.1.5.2.1 Splitting Cut-Point Transitions

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

14.1.5.3 Cut-Point Subproblem 3/3

Here we consider cut-point transition 45.

14.1.5.3.1 Splitting Cut-Point Transitions

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

14.2 SCC Subproblem 2/2

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

14.2.1 Transition Removal

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

0: 9 − 10⋅i4_0
1: 9 − 10⋅i4_0
2: −10⋅i4_0
3: −10⋅i4_0
0_var_snapshot: 9 − 10⋅i4_0
0*: 10 − 10⋅i4_0
2_var_snapshot: −10⋅i4_0
2*: −10⋅i4_0

14.2.2 Transition Removal

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

0: −5⋅j5_0
1: −2 − 5⋅j5_0
2: 1 − 3⋅j5_0
3: −3⋅j5_0
0_var_snapshot: −1 − 5⋅j5_0
0*: 12 − 5⋅j5_0
2_var_snapshot: −3⋅j5_0
2*: 2 − 3⋅j5_0

14.2.3 Transition Removal

We remove transitions 18, 25, 27, 0, 1, 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

14.2.4 Transition Removal

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

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

14.2.5 Splitting Cut-Point Transitions

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

14.2.5.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 17.

14.2.5.1.1 Splitting Cut-Point Transitions

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

14.2.5.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 24.

14.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