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: −1 + tmp_post ≤ 0−1 + tmp_0 ≤ 0
7: TRUE
8: −1 + tmp_post ≤ 0−1 + tmp_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:
4 16 4: x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0N_0 + N_0 ≤ 0N_0N_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 2, 5, 6, 7, 8, 9, 10, 11, 12, 14, 15 using the following ranking functions, which are bounded by −21.

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

4 Location Addition

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

4* 19 4: x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0N_0 + N_0 ≤ 0N_0N_0 ≤ 0

5 Location Addition

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

4 17 4_var_snapshot: x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0N_0 + N_0 ≤ 0N_0N_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, 1, 2, 4, 4_var_snapshot, 4* }.

6.1.1 Transition Removal

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

0: 1 + 6⋅N_0 − 6⋅i_0
1: 6⋅N_0 − 6⋅i_0
2: 2 + 6⋅N_0 − 6⋅i_0
4: 4 + 6⋅N_0 − 6⋅i_0
4_var_snapshot: 3 + 6⋅N_0 − 6⋅i_0
4*: 5 + 6⋅N_0 − 6⋅i_0

6.1.2 Transition Removal

We remove transitions 17, 19, 0, 1, 4, 13 using the following ranking functions, which are bounded by −4.

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

6.1.3 Splitting Cut-Point Transitions

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

6.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 16.

6.1.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert