# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 2
• Transitions: (pre-variables and post-variables)  0 0 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ arg1P + arg2P − arg4P ≤ 0 ∧ − arg1P − arg2P + arg4P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 1 1 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg3 + arg4 ≤ 0 ∧ −1 − arg1 ≤ 0 ∧ −1 − arg2 ≤ 0 ∧ 1 − arg1P + arg1 ≤ 0 ∧ −1 + arg1P − arg1 ≤ 0 ∧ 1 − arg2P + arg2 ≤ 0 ∧ −1 + arg2P − arg2 ≤ 0 ∧ 2 + arg1 + arg2 − arg4P ≤ 0 ∧ −2 − arg1 − arg2 + arg4P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 2 2 0: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0

## Proof

The following invariants are asserted.

 0: TRUE 1: − arg3P ≤ 0 ∧ − arg3 ≤ 0 2: TRUE

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (0) TRUE 1 (1) − arg3P ≤ 0 ∧ − arg3 ≤ 0 2 (2) TRUE
• initial node: 2
• cover edges:
• transition edges:  0 0 1 1 1 1 2 2 0

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 1 3 1: − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
and for every transition t, a duplicate t is considered.

### 3 Transition Removal

We remove transitions 0, 2 using the following ranking functions, which are bounded by −11.

 2: 0 0: 0 1: 0 2: −4 0: −5 1: −6 1_var_snapshot: −6 1*: −6

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

1* 6 1: arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

1 4 1_var_snapshot: arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 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 { 1, 1_var_snapshot, 1* }.

### 6.1.1 Splitting Cut-Point Transitions

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

### 6.1.1.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 3.

The new variable __snapshot_1_arg4P is introduced. The transition formulas are extended as follows:

 4: __snapshot_1_arg4P ≤ arg4P ∧ arg4P ≤ __snapshot_1_arg4P 6: __snapshot_1_arg4P ≤ __snapshot_1_arg4P ∧ __snapshot_1_arg4P ≤ __snapshot_1_arg4P 1: __snapshot_1_arg4P ≤ __snapshot_1_arg4P ∧ __snapshot_1_arg4P ≤ __snapshot_1_arg4P

The new variable __snapshot_1_arg4 is introduced. The transition formulas are extended as follows:

 4: __snapshot_1_arg4 ≤ arg4 ∧ arg4 ≤ __snapshot_1_arg4 6: __snapshot_1_arg4 ≤ __snapshot_1_arg4 ∧ __snapshot_1_arg4 ≤ __snapshot_1_arg4 1: __snapshot_1_arg4 ≤ __snapshot_1_arg4 ∧ __snapshot_1_arg4 ≤ __snapshot_1_arg4

The new variable __snapshot_1_arg3P is introduced. The transition formulas are extended as follows:

 4: __snapshot_1_arg3P ≤ arg3P ∧ arg3P ≤ __snapshot_1_arg3P 6: __snapshot_1_arg3P ≤ __snapshot_1_arg3P ∧ __snapshot_1_arg3P ≤ __snapshot_1_arg3P 1: __snapshot_1_arg3P ≤ __snapshot_1_arg3P ∧ __snapshot_1_arg3P ≤ __snapshot_1_arg3P

The new variable __snapshot_1_arg3 is introduced. The transition formulas are extended as follows:

 4: __snapshot_1_arg3 ≤ arg3 ∧ arg3 ≤ __snapshot_1_arg3 6: __snapshot_1_arg3 ≤ __snapshot_1_arg3 ∧ __snapshot_1_arg3 ≤ __snapshot_1_arg3 1: __snapshot_1_arg3 ≤ __snapshot_1_arg3 ∧ __snapshot_1_arg3 ≤ __snapshot_1_arg3

The new variable __snapshot_1_arg2P is introduced. The transition formulas are extended as follows:

 4: __snapshot_1_arg2P ≤ arg2P ∧ arg2P ≤ __snapshot_1_arg2P 6: __snapshot_1_arg2P ≤ __snapshot_1_arg2P ∧ __snapshot_1_arg2P ≤ __snapshot_1_arg2P 1: __snapshot_1_arg2P ≤ __snapshot_1_arg2P ∧ __snapshot_1_arg2P ≤ __snapshot_1_arg2P

The new variable __snapshot_1_arg2 is introduced. The transition formulas are extended as follows:

 4: __snapshot_1_arg2 ≤ arg2 ∧ arg2 ≤ __snapshot_1_arg2 6: __snapshot_1_arg2 ≤ __snapshot_1_arg2 ∧ __snapshot_1_arg2 ≤ __snapshot_1_arg2 1: __snapshot_1_arg2 ≤ __snapshot_1_arg2 ∧ __snapshot_1_arg2 ≤ __snapshot_1_arg2

The new variable __snapshot_1_arg1P is introduced. The transition formulas are extended as follows:

 4: __snapshot_1_arg1P ≤ arg1P ∧ arg1P ≤ __snapshot_1_arg1P 6: __snapshot_1_arg1P ≤ __snapshot_1_arg1P ∧ __snapshot_1_arg1P ≤ __snapshot_1_arg1P 1: __snapshot_1_arg1P ≤ __snapshot_1_arg1P ∧ __snapshot_1_arg1P ≤ __snapshot_1_arg1P

The new variable __snapshot_1_arg1 is introduced. The transition formulas are extended as follows:

 4: __snapshot_1_arg1 ≤ arg1 ∧ arg1 ≤ __snapshot_1_arg1 6: __snapshot_1_arg1 ≤ __snapshot_1_arg1 ∧ __snapshot_1_arg1 ≤ __snapshot_1_arg1 1: __snapshot_1_arg1 ≤ __snapshot_1_arg1 ∧ __snapshot_1_arg1 ≤ __snapshot_1_arg1

The following invariants are asserted.

 0: TRUE 1: arg3 − arg3P ≤ 0 ∧ arg2 + arg3 − arg3P − arg4 ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg3 ≤ 0 2: TRUE 1: arg3 − arg3P ≤ 0 ∧ arg2 + arg3 − arg3P − arg4 ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg3 ≤ 0 ∨ arg3 − arg3P ≤ 0 ∧ 1 + __snapshot_1_arg2 − __snapshot_1_arg3P − arg2 + arg3P ≤ 0 ∧ arg2 + arg3 − arg3P − arg4 ≤ 0 ∧ 1 + __snapshot_1_arg2 − __snapshot_1_arg3P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg3 ≤ 0 1_var_snapshot: arg3 − arg3P ≤ 0 ∧ __snapshot_1_arg2 − __snapshot_1_arg3P − arg2 + arg3P ≤ 0 ∧ __snapshot_1_arg2 − __snapshot_1_arg3P + arg3 − arg4 ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg3 ≤ 0 1*: arg3 − arg3P ≤ 0 ∧ 1 + __snapshot_1_arg2 − __snapshot_1_arg3P − arg2 + arg3P ≤ 0 ∧ arg2 + arg3 − arg3P − arg4 ≤ 0 ∧ 1 + __snapshot_1_arg2 − __snapshot_1_arg3P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg3 ≤ 0

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (2) TRUE 1 (0) TRUE 2 (1) arg3 − arg3P ≤ 0 ∧ arg2 + arg3 − arg3P − arg4 ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg3 ≤ 0 3 (1) arg3 − arg3P ≤ 0 ∧ arg2 + arg3 − arg3P − arg4 ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg3 ≤ 0 4 (1) arg3 − arg3P ≤ 0 ∧ arg2 + arg3 − arg3P − arg4 ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg3 ≤ 0 5 (1_var_snapshot) arg3 − arg3P ≤ 0 ∧ __snapshot_1_arg2 − __snapshot_1_arg3P − arg2 + arg3P ≤ 0 ∧ __snapshot_1_arg2 − __snapshot_1_arg3P + arg3 − arg4 ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg3 ≤ 0 12 (1*) arg3 − arg3P ≤ 0 ∧ 1 + __snapshot_1_arg2 − __snapshot_1_arg3P − arg2 + arg3P ≤ 0 ∧ arg2 + arg3 − arg3P − arg4 ≤ 0 ∧ 1 + __snapshot_1_arg2 − __snapshot_1_arg3P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg3 ≤ 0 13 (1) arg3 − arg3P ≤ 0 ∧ 1 + __snapshot_1_arg2 − __snapshot_1_arg3P − arg2 + arg3P ≤ 0 ∧ arg2 + arg3 − arg3P − arg4 ≤ 0 ∧ 1 + __snapshot_1_arg2 − __snapshot_1_arg3P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg3 ≤ 0 14 (1_var_snapshot) arg3 − arg3P ≤ 0 ∧ __snapshot_1_arg2 − __snapshot_1_arg3P − arg2 + arg3P ≤ 0 ∧ __snapshot_1_arg2 − __snapshot_1_arg3P + arg3 − arg4 ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg3 ≤ 0
• initial node: 0
• cover edges:  3 → 2 14 → 5
• transition edges:  0 2 1 1 0 2 2 1 3 2 3 4 4 4 5 5 1 12 12 6 13 13 4 14

### 6.1.1.1.10 Transition Removal

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

 1: − arg2 + arg3P 1_var_snapshot: − __snapshot_1_arg2 + __snapshot_1_arg3P 1*: − __snapshot_1_arg2 + __snapshot_1_arg3P

### 6.1.1.1.11 Transition Removal

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

 1: −1 1_var_snapshot: −2 1*: −3

### 6.1.1.1.12 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0