LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: TRUE
1: TRUE
2: 1 + i_0 ≤ 0
3: 1 + i_0 ≤ 0
4: 1 + i_0 ≤ 0
5: TRUE
6: TRUE
7: TRUE
8: TRUE
9: TRUE
10: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 14 0: y4_post + y4_post ≤ 0y4_posty4_post ≤ 0y4_0 + y4_0 ≤ 0y4_0y4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0tmp5_post + tmp5_post ≤ 0tmp5_posttmp5_post ≤ 0tmp5_0 + tmp5_0 ≤ 0tmp5_0tmp5_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0
6 21 6: y4_post + y4_post ≤ 0y4_posty4_post ≤ 0y4_0 + y4_0 ≤ 0y4_0y4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0tmp5_post + tmp5_post ≤ 0tmp5_posttmp5_post ≤ 0tmp5_0 + tmp5_0 ≤ 0tmp5_0tmp5_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 1, 2, 3, 10, 12, 13 using the following ranking functions, which are bounded by −19.

10: 0
9: 0
0: 0
1: 0
5: 0
6: 0
7: 0
8: 0
4: 0
2: 0
3: 0
10: −7
9: −8
0: −9
1: −9
5: −9
6: −9
7: −9
8: −9
0_var_snapshot: −9
0*: −9
6_var_snapshot: −9
6*: −9
4: −12
2: −13
3: −14
Hints:
15 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
22 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
0 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
4 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
7 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
8 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
9 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
11 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
1 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
2 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
3 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
10 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
12 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
13 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

4 Location Addition

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

0* 17 0: y4_post + y4_post ≤ 0y4_posty4_post ≤ 0y4_0 + y4_0 ≤ 0y4_0y4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0tmp5_post + tmp5_post ≤ 0tmp5_posttmp5_post ≤ 0tmp5_0 + tmp5_0 ≤ 0tmp5_0tmp5_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0

5 Location Addition

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

0 15 0_var_snapshot: y4_post + y4_post ≤ 0y4_posty4_post ≤ 0y4_0 + y4_0 ≤ 0y4_0y4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0tmp5_post + tmp5_post ≤ 0tmp5_posttmp5_post ≤ 0tmp5_0 + tmp5_0 ≤ 0tmp5_0tmp5_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0

6 Location Addition

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

6* 24 6: y4_post + y4_post ≤ 0y4_posty4_post ≤ 0y4_0 + y4_0 ≤ 0y4_0y4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0tmp5_post + tmp5_post ≤ 0tmp5_posttmp5_post ≤ 0tmp5_0 + tmp5_0 ≤ 0tmp5_0tmp5_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0

7 Location Addition

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

6 22 6_var_snapshot: y4_post + y4_post ≤ 0y4_posty4_post ≤ 0y4_0 + y4_0 ≤ 0y4_0y4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0tmp5_post + tmp5_post ≤ 0tmp5_posttmp5_post ≤ 0tmp5_0 + tmp5_0 ≤ 0tmp5_0tmp5_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0

8 SCC Decomposition

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

8.1 SCC Subproblem 1/1

Here we consider the SCC { 0, 1, 5, 6, 7, 8, 0_var_snapshot, 0*, 6_var_snapshot, 6* }.

8.1.1 Transition Removal

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

0: 2 + 5⋅i_0
1: 5⋅i_0
5: −1 + 5⋅i_0
6: −1 + 5⋅i_0
7: −1 + 5⋅i_0
8: −1 + 5⋅i_0
0_var_snapshot: 1 + 5⋅i_0
0*: 3 + 5⋅i_0
6_var_snapshot: −1 + 5⋅i_0
6*: −1 + 5⋅i_0
Hints:
15 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0] ]
17 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0] ]
22 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0] ]
24 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0] ]
0 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0] ]
4 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0] ]
5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0] ]
6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0] ]
7 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0] ]
8 lexWeak[ [0, 0, 0, 5, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
9 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0] ]
11 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0] , [5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

8.1.2 Transition Removal

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

0: 9 + i_0 + 10⋅i_post − 11⋅j_0
1: 8 + i_0 + 10⋅i_post − 11⋅j_0
5: −8 + 11⋅i_0 − 11⋅j_0
6: 1 + 11⋅i_0 − 11⋅j_0
7: 11⋅i_0 − 11⋅j_0
8: −1 + 11⋅i_0 − 11⋅j_0
0_var_snapshot: 8 + i_0 + 10⋅i_post − 11⋅j_0
0*: 10 + i_0 + 10⋅i_post − 11⋅j_0
6_var_snapshot: 11⋅i_0 − 11⋅j_0
6*: 2 + 11⋅i_0 − 11⋅j_0
Hints:
15 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 10, 0, 1, 0] ]
17 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 10, 0, 1, 0] ]
22 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 11, 0] ]
24 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 11, 0] ]
0 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 10, 0, 1, 0] ]
4 lexWeak[ [0, 0, 0, 11, 0, 11, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0] ]
5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 11, 0] ]
6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 11, 0] ]
7 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 11, 0] ]
8 lexWeak[ [0, 0, 0, 11, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11] ]
9 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 11, 0] , [11, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

8.1.3 Transition Removal

We remove transitions 15, 17, 22, 24, 0, 4, 5, 6, 7, 8 using the following ranking functions, which are bounded by −4.

0: −2
1: −4
5: 4
6: 2
7: 0
8: 5
0_var_snapshot: −3
0*: −1
6_var_snapshot: 1
6*: 3
Hints:
15 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
17 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
22 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
24 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
0 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
4 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
5 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
6 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
7 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
8 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

8.1.4 Splitting Cut-Point Transitions

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

8.1.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 14.

8.1.4.1.1 Splitting Cut-Point Transitions

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

8.1.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 21.

8.1.4.2.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert