LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: copied_post ≤ 0copied_0 ≤ 0
1: copied_post ≤ 01 − copied_0 ≤ 0
2: −1 + copied_post ≤ 01 − copied_post ≤ 0−1 + copied_0 ≤ 01 − copied_0 ≤ 0
3: −1 + copied_post ≤ 01 − copied_post ≤ 0−1 + copied_0 ≤ 01 − copied_0 ≤ 0
4: copied_post ≤ 0copied_0 ≤ 0
5: copied_post ≤ 0copied_0 ≤ 0
6: TRUE
7: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 11 0: oldn_post + oldn_post ≤ 0oldn_postoldn_post ≤ 0oldn_0 + oldn_0 ≤ 0oldn_0oldn_0 ≤ 0olde_post + olde_post ≤ 0olde_postolde_post ≤ 0olde_0 + olde_0 ≤ 0olde_0olde_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0e_post + e_post ≤ 0e_poste_post ≤ 0e_0 + e_0 ≤ 0e_0e_0 ≤ 0copied_post + copied_post ≤ 0copied_postcopied_post ≤ 0copied_0 + copied_0 ≤ 0copied_0copied_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 9, 10 using the following ranking functions, which are bounded by −13.

7: 0
6: 0
0: 0
2: 0
3: 0
4: 0
5: 0
1: 0
7: −5
6: −6
0: −7
2: −7
3: −7
4: −7
5: −7
0_var_snapshot: −7
0*: −7
1: −11
Hints:
12 lexWeak[ [0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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] ]
3 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, 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, 0, 0] ]
5 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, 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] ]
7 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, 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 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, 0, 0] ]
9 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] ]
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] ]

4 Location Addition

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

0* 14 0: oldn_post + oldn_post ≤ 0oldn_postoldn_post ≤ 0oldn_0 + oldn_0 ≤ 0oldn_0oldn_0 ≤ 0olde_post + olde_post ≤ 0olde_postolde_post ≤ 0olde_0 + olde_0 ≤ 0olde_0olde_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0e_post + e_post ≤ 0e_poste_post ≤ 0e_0 + e_0 ≤ 0e_0e_0 ≤ 0copied_post + copied_post ≤ 0copied_postcopied_post ≤ 0copied_0 + copied_0 ≤ 0copied_0copied_0 ≤ 0

5 Location Addition

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

0 12 0_var_snapshot: oldn_post + oldn_post ≤ 0oldn_postoldn_post ≤ 0oldn_0 + oldn_0 ≤ 0oldn_0oldn_0 ≤ 0olde_post + olde_post ≤ 0olde_postolde_post ≤ 0olde_0 + olde_0 ≤ 0olde_0olde_0 ≤ 0n_post + n_post ≤ 0n_postn_post ≤ 0n_0 + n_0 ≤ 0n_0n_0 ≤ 0e_post + e_post ≤ 0e_poste_post ≤ 0e_0 + e_0 ≤ 0e_0e_0 ≤ 0copied_post + copied_post ≤ 0copied_postcopied_post ≤ 0copied_0 + copied_0 ≤ 0copied_0copied_0 ≤ 0

6 SCC Decomposition

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

6.1 SCC Subproblem 1/1

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

6.1.1 Transition Removal

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

0: −1 + 84⋅e_0 − 8⋅n_0
2: copied_post + 84⋅e_0 − 8⋅n_0
3: 1 + 84⋅e_0 − 8⋅n_0
4: 1 + 84⋅e_0 − 8⋅n_0
5: 1 + 84⋅e_0 − 8⋅n_0
0_var_snapshot: −2 + 84⋅e_0 − 8⋅n_0
0*: 84⋅e_0 − 8⋅n_0
Hints:
12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 84, 0, 0, 0, 0, 0] ]
14 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 84, 0, 0, 0, 0, 0] ]
1 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 8, 84, 0, 0, 0, 84, 0, 0, 8, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 84, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
2 lexWeak[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 84, 0, 0, 0, 0, 0] ]
3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 84, 0, 0, 0, 84, 0, 0, 8, 0, 0, 0, 0] ]
4 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 84, 0, 0, 0, 0, 0] ]
5 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 84, 0, 84, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 84, 8, 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, 8, 0, 0, 84, 0, 0, 0, 0, 0] ]
7 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 84, 0, 84, 0, 0, 8, 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, 8, 0, 0, 84, 0, 0, 0, 0, 0] ]

6.1.2 Transition Removal

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

0: 30⋅e_0
2: 1 + 30⋅e_0
3: copied_post + 30⋅e_0
4: 1 + 30⋅e_0
5: 10 + 30⋅e_0
0_var_snapshot: −10 + 30⋅e_0
0*: 30⋅e_0
Hints:
12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 30, 0, 0, 0, 0, 0] ]
14 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 30, 0, 0, 0, 0, 0] ]
2 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 30, 0, 0, 0, 0, 0] ]
3 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 30, 0, 0, 0, 30, 0, 0, 0, 0, 0, 0, 0] ]
4 lexWeak[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 30, 0, 0, 0, 0, 0] ]
6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 30, 0, 0, 0, 0, 0] ]
7 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 30, 0, 30, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 30, 0, 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, 30, 0, 0, 0, 0, 0] ]

6.1.3 Transition Removal

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

0: −1 − 4⋅copied_0
2: 1 − 4⋅copied_0
3: −3⋅copied_0
4: 1 − 4⋅copied_0
5: 1
0_var_snapshot: −2 − 4⋅copied_0
0*: −4⋅copied_0
Hints:
12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4] ]
14 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4] ]
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, 4] , [0, 0, 4, 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, 4, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4] , [0, 0, 3, 0, 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, 4] ]
8 lexStrict[ [0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

6.1.4 Transition Removal

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

0: 0
2: 0
3: 0
4: 2
5: 0
0_var_snapshot: −1
0*: 1
Hints:
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] ]
14 lexWeak[ [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] ]

6.1.5 Transition Removal

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

0: 0
2: 0
3: 0
4: 0
5: 0
0_var_snapshot: 0
0*: 1
Hints:
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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

6.1.6 Splitting Cut-Point Transitions

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

6.1.6.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 11.

6.1.6.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert