# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 31

## Proof

The following invariants are asserted.

 6: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 9: TRUE 10: TRUE 11: i_27_post ≤ 0 ∧ − i_27_post ≤ 0 ∧ i_27_0 ≤ 0 ∧ − i_27_0 ≤ 0 12: −1 + i_27_post ≤ 0 ∧ 1 − i_27_post ≤ 0 ∧ −1 + i_27_0 ≤ 0 ∧ 1 − i_27_0 ≤ 0 ∧ 1 − length_25_0 ≤ 0 13: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 14: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 15: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 16: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 17: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 18: 2 − length_25_0 ≤ 0 19: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − a_163_0 ≤ 0 20: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − a_163_0 ≤ 0 21: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − a_163_0 ≤ 0 22: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − a_163_0 ≤ 0 23: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − a_163_0 ≤ 0 24: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 25: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 26: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 27: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 28: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 29: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 30: 2 − length_25_0 ≤ 0 31: TRUE

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  6 (6) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 9 (9) TRUE 10 (10) TRUE 11 (11) i_27_post ≤ 0 ∧ − i_27_post ≤ 0 ∧ i_27_0 ≤ 0 ∧ − i_27_0 ≤ 0 12 (12) −1 + i_27_post ≤ 0 ∧ 1 − i_27_post ≤ 0 ∧ −1 + i_27_0 ≤ 0 ∧ 1 − i_27_0 ≤ 0 ∧ 1 − length_25_0 ≤ 0 13 (13) −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 14 (14) −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 15 (15) −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 16 (16) −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 17 (17) −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 18 (18) 2 − length_25_0 ≤ 0 19 (19) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − a_163_0 ≤ 0 20 (20) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − a_163_0 ≤ 0 21 (21) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − a_163_0 ≤ 0 22 (22) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − a_163_0 ≤ 0 23 (23) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − a_163_0 ≤ 0 24 (24) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 25 (25) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 26 (26) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 27 (27) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 28 (28) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 29 (29) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0 30 (30) 2 − length_25_0 ≤ 0 31 (31) TRUE
• initial node: 31
• cover edges:
• transition edges:  6 17 9 6 18 19 10 9 11 11 33 9 11 34 12 12 10 13 12 16 18 13 11 14 14 12 15 15 13 16 16 14 17 17 15 9 18 25 25 18 31 30 19 19 20 20 20 21 21 21 22 22 22 23 23 23 24 24 24 6 25 26 26 26 27 27 27 28 28 28 29 29 29 30 6 30 32 18 31 35 10

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
and for every transition t, a duplicate t is considered.

### 3 Transition Removal

We remove transitions 9, 10, 11, 12, 13, 14, 15, 16, 17, 25, 26, 27, 28, 29, 30, 33, 34, 35 using the following ranking functions, which are bounded by −41.

 31: 0 10: 0 11: 0 12: 0 13: 0 14: 0 15: 0 16: 0 17: 0 18: 0 30: 0 25: 0 26: 0 27: 0 28: 0 29: 0 6: 0 19: 0 20: 0 21: 0 22: 0 23: 0 24: 0 9: 0 31: −18 10: −19 11: −20 12: −21 13: −22 14: −23 15: −24 16: −25 17: −26 18: −27 30: −27 18_var_snapshot: −27 18*: −27 25: −30 26: −31 27: −32 28: −33 29: −34 6: −35 19: −35 20: −35 21: −35 22: −35 23: −35 24: −35 6_var_snapshot: −35 6*: −35 9: −39

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

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

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

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

### 8 SCC Decomposition

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

### 8.1 SCC Subproblem 1/2

Here we consider the SCC { 6, 19, 20, 21, 22, 23, 24, 6_var_snapshot, 6* }.

### 8.1.1 Transition Removal

We remove transitions 18, 19 using the following ranking functions, which are bounded by −4.

 6: −1 + 9⋅a_163_0 19: −3 + 9⋅a_163_0 20: −4 + 9⋅a_163_0 21: 4 + 9⋅a_193_0 22: 3 + 9⋅a_193_0 23: 2 + 9⋅a_193_0 24: 1 + 9⋅a_163_0 6_var_snapshot: −2 + 9⋅a_163_0 6*: 9⋅a_163_0

### 8.1.2 Transition Removal

We remove transitions 37, 39, 20, 22, 23, 24 using the following ranking functions, which are bounded by −5.

 6: −4 19: 0 20: 1 + 3⋅result_dot_nondet_sdv_special_RETURN_VALUE_14_1 21: 3⋅result_dot_nondet_sdv_special_RETURN_VALUE_14_1 22: 2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 23: result_dot_nondet_sdv_special_RETURN_VALUE_14_1 24: 0 6_var_snapshot: −3⋅result_dot_nondet_sdv_special_RETURN_VALUE_14_1 6*: −2

### 8.1.3 Transition Removal

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

 6: 0 19: 0 20: 0 21: result_dot_nondet_sdv_special_RETURN_VALUE_14_1 22: 0 23: 0 24: 0 6_var_snapshot: 0 6*: 0

### 8.1.4 Splitting Cut-Point Transitions

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

### 8.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 36.

### 8.1.4.1.1 Splitting Cut-Point Transitions

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

### 8.2 SCC Subproblem 2/2

Here we consider the SCC { 18, 30, 18_var_snapshot, 18* }.

### 8.2.1 Transition Removal

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

 18: −2 − 4⋅i_27_0 + 4⋅length_25_0 30: −4⋅i_27_0 + 4⋅length_25_0 18_var_snapshot: −3 − 4⋅i_27_0 + 4⋅length_25_0 18*: −1 − 4⋅i_27_0 + 4⋅length_25_0

### 8.2.2 Transition Removal

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

 18: 0 30: 1 + length_25_0 18_var_snapshot: −1 18*: length_25_0

### 8.2.3 Transition Removal

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

 18: 1 30: 0 18_var_snapshot: 0 18*: 0

### 8.2.4 Splitting Cut-Point Transitions

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

### 8.2.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 43.

### 8.2.4.1.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0