LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: −1 + i2_post ≤ 01 − i2_post ≤ 01 − i2_0 ≤ 0i2_0 ≤ 0
1: −1 + i2_post ≤ 01 − i2_post ≤ 0−1 + i2_0 ≤ 01 − i2_0 ≤ 0
2: −1 + i2_post ≤ 01 − i2_post ≤ 01 − i2_0 ≤ 0i2_0 ≤ 0
3: −1 + i2_post ≤ 01 − i2_post ≤ 0−1 + i2_0 ≤ 01 − i2_0 ≤ 0
4: −1 + i2_post ≤ 01 − i2_post ≤ 0−1 + i2_0 ≤ 01 − i2_0 ≤ 0
5: −1 + i2_post ≤ 01 − i2_post ≤ 0−1 + i2_0 ≤ 01 − i2_0 ≤ 0
6: −1 + i2_post ≤ 01 − i2_post ≤ 0−1 + i2_0 ≤ 01 − i2_0 ≤ 01 + i6_0 ≤ 0
7: −1 + i2_post ≤ 01 − i2_post ≤ 0−1 + i2_0 ≤ 01 − i2_0 ≤ 01 + i6_0 ≤ 01 + i8_0 ≤ 0
8: −1 + i2_post ≤ 01 − i2_post ≤ 0−1 + i2_0 ≤ 01 − i2_0 ≤ 01 + i6_0 ≤ 0
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:
2 15 2: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0i6_post + i6_post ≤ 0i6_posti6_post ≤ 0i6_0 + i6_0 ≤ 0i6_0i6_0 ≤ 0i34_post + i34_post ≤ 0i34_posti34_post ≤ 0i34_0 + i34_0 ≤ 0i34_0i34_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0
4 22 4: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0i6_post + i6_post ≤ 0i6_posti6_post ≤ 0i6_0 + i6_0 ≤ 0i6_0i6_0 ≤ 0i34_post + i34_post ≤ 0i34_posti34_post ≤ 0i34_0 + i34_0 ≤ 0i34_0i34_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0
8 29 8: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0i6_post + i6_post ≤ 0i6_posti6_post ≤ 0i6_0 + i6_0 ≤ 0i6_0i6_0 ≤ 0i34_post + i34_post ≤ 0i34_posti34_post ≤ 0i34_0 + i34_0 ≤ 0i34_0i34_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 2, 3, 4, 7, 10, 12, 13, 14 using the following ranking functions, which are bounded by −25.

10: 0
9: 0
3: 0
0: 0
2: 0
1: 0
4: 0
5: 0
6: 0
8: 0
7: 0
10: −9
9: −10
3: −11
0: −12
2: −12
2_var_snapshot: −12
2*: −12
1: −13
4: −14
5: −14
4_var_snapshot: −14
4*: −14
6: −15
8: −15
8_var_snapshot: −15
8*: −15
7: −16
Hints:
16 lexWeak[ [0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
23 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
30 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
1 lexWeak[ [0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
5 lexWeak[ [0, 0, 1, 1, 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] ]
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, 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, 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, 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] ]
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, 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, 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, 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] ]
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] ]
14 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] ]

4 Location Addition

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

2* 18 2: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0i6_post + i6_post ≤ 0i6_posti6_post ≤ 0i6_0 + i6_0 ≤ 0i6_0i6_0 ≤ 0i34_post + i34_post ≤ 0i34_posti34_post ≤ 0i34_0 + i34_0 ≤ 0i34_0i34_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0

5 Location Addition

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

2 16 2_var_snapshot: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0i6_post + i6_post ≤ 0i6_posti6_post ≤ 0i6_0 + i6_0 ≤ 0i6_0i6_0 ≤ 0i34_post + i34_post ≤ 0i34_posti34_post ≤ 0i34_0 + i34_0 ≤ 0i34_0i34_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0

6 Location Addition

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

4* 25 4: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0i6_post + i6_post ≤ 0i6_posti6_post ≤ 0i6_0 + i6_0 ≤ 0i6_0i6_0 ≤ 0i34_post + i34_post ≤ 0i34_posti34_post ≤ 0i34_0 + i34_0 ≤ 0i34_0i34_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0

7 Location Addition

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

4 23 4_var_snapshot: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0i6_post + i6_post ≤ 0i6_posti6_post ≤ 0i6_0 + i6_0 ≤ 0i6_0i6_0 ≤ 0i34_post + i34_post ≤ 0i34_posti34_post ≤ 0i34_0 + i34_0 ≤ 0i34_0i34_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0

8 Location Addition

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

8* 32 8: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0i6_post + i6_post ≤ 0i6_posti6_post ≤ 0i6_0 + i6_0 ≤ 0i6_0i6_0 ≤ 0i34_post + i34_post ≤ 0i34_posti34_post ≤ 0i34_0 + i34_0 ≤ 0i34_0i34_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0

9 Location Addition

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

8 30 8_var_snapshot: i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0i6_post + i6_post ≤ 0i6_posti6_post ≤ 0i6_0 + i6_0 ≤ 0i6_0i6_0 ≤ 0i34_post + i34_post ≤ 0i34_posti34_post ≤ 0i34_0 + i34_0 ≤ 0i34_0i34_0 ≤ 0i2_post + i2_post ≤ 0i2_posti2_post ≤ 0i2_0 + i2_0 ≤ 0i2_0i2_0 ≤ 0

10 SCC Decomposition

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

10.1 SCC Subproblem 1/3

Here we consider the SCC { 6, 8, 8_var_snapshot, 8* }.

10.1.1 Transition Removal

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

6: i2_0 − 2⋅i2_post + 4⋅i8_0
8: −1 + 4⋅i8_0
8_var_snapshot: −2⋅i2_post + 4⋅i8_0
8*: 4⋅i8_0
Hints:
30 lexWeak[ [0, 2, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 0] ]
32 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
8 lexStrict[ [2, 0, 1, 0, 0, 0, 0, 0, 4, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [2, 0, 1, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
9 lexWeak[ [0, 0, 0, 1, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 1] ]

10.1.2 Transition Removal

We remove transitions 30, 32, 9 using the following ranking functions, which are bounded by −2.

6: i2_0i2_post
8: 0
8_var_snapshot: i2_post
8*: i2_0
Hints:
30 lexStrict[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
32 lexStrict[ [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
9 lexStrict[ [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1] , [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

10.1.3 Splitting Cut-Point Transitions

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

10.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 29.

10.1.3.1.1 Splitting Cut-Point Transitions

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

10.2 SCC Subproblem 2/3

Here we consider the SCC { 4, 5, 4_var_snapshot, 4* }.

10.2.1 Transition Removal

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

4: 2⋅i2_0 + 3⋅i6_0
5: 3⋅i6_0
4_var_snapshot: 1 + 3⋅i6_0
4*: 2⋅i2_0 + 3⋅i6_0
Hints:
23 lexWeak[ [0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
25 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 2, 0] ]
6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
11 lexStrict[ [0, 0, 2, 0, 0, 0, 0, 3, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0] , [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

10.2.2 Transition Removal

We remove transitions 23, 25, 6 using the following ranking functions, which are bounded by −2.

4: 0
5: −1 − i2_post
4_var_snapshot: i2_post
4*: i2_0
Hints:
23 lexStrict[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
25 lexStrict[ [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 1, 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, 1, 0, 0] , [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

10.2.3 Splitting Cut-Point Transitions

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

10.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 22.

10.2.3.1.1 Splitting Cut-Point Transitions

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

10.3 SCC Subproblem 3/3

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

10.3.1 Transition Removal

We remove transitions 16, 18, 1, 5 using the following ranking functions, which are bounded by −2.

0: 1
2: i2_post
2_var_snapshot: 0
2*: 0
Hints:
16 lexStrict[ [1, 0, 2, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
18 lexStrict[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 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, 0, 0, 0, 0] ]
5 lexStrict[ [0, 0, 2, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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.3.2 Splitting Cut-Point Transitions

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

10.3.2.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 15.

10.3.2.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert