# LTS Termination Proof

by manual

## Input

Integer Transition System
• Initial Location: l0
• Transitions: (pre-variables and post-variables)  l0 t1 l1: x = x ∧ y = y ∧ z = −1 l1 t2 l2: −5 ≤ x ∧ x = x + z ∧ y = 0 ∧ z = z − 1 l2 t3 l2: y < x ∧ x = x ∧ y = y + 1 ∧ z = z l2 t4 l1: x ≤ y ∧ x = x ∧ y = y ∧ z = z

## Proof

The following invariants are asserted.

 l0: TRUE l1: z < 0 l2: z < −1

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (l0) TRUE 1 (l1) z < 0 2 (l2) z < −1 3 (l2) z < −1 4 (l1) z < −1
• initial node: 0
• cover edges:  3 → 2 4 → 1
• transition edges:  0 t1 1 1 t2 2 2 t3 3 2 t4 4

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 l2 e l2: x = x ∧ y = y ∧ z = z
and for every transition t, a duplicate t is considered.

### 3 SCC Decomposition

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

### 3.1 SCC Subproblem 1/1

Here we consider the SCC { l1, l2 }.

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

l2 t5 l2a: x = xy = yz = z

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

l2b t6 l2: x = xy = yz = z

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

 t2: xs = xs t3: xs = xs t4: xs = xs t6: xs = xs t5: xs = x

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

 t2: ys = ys t3: ys = ys t4: ys = ys t6: ys = ys t5: ys = y

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

 t2: zs = zs t3: zs = zs t4: zs = zs t6: zs = zs t5: zs = z

The following invariants are asserted.

 l0: TRUE l1: TRUE l2: 0 ≤ y l1: x ≤ xs l2: 0 ≤ y l2a: 0 ≤ y ∧ ys + x ≤ xs + y ∧ x ≤ xs l2b: 0 ≤ y ∧ −5 ≤ xs ∧ ys + x < xs + y ∧ ys < xs ∧ x ≤ xs ∨ 0 ≤ y ∧ −5 ≤ xs ∧ x < xs

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (l0) TRUE 1 (l1) TRUE 2 (l2) 0 ≤ y 3 (l2) 0 ≤ y 4 (l2a) 0 ≤ y ∧ ys + x ≤ xs + y ∧ x ≤ xs 5 (l2b) 0 ≤ y ∧ −5 ≤ xs ∧ ys + x < xs + y ∧ ys < xs ∧ x ≤ xs 6 (l1) x ≤ xs 7 (l2) 0 ≤ y ∧ −5 ≤ xs ∧ ys + x < xs + y ∧ ys < xs ∧ x ≤ xs 8 (l2b) 0 ≤ y ∧ −5 ≤ xs ∧ x < xs 9 (l2) 0 ≤ y ∧ −5 ≤ xs ∧ x < xs
• initial node: 0
• cover edges:  7 → 3 9 → 3
• transition edges:  0 t1 1 1 t2 2 2 t3 2 2 t4 1 2 e 3 3 t5 4 4 t3 5 4 t4 6 5 t6 7 6 t2 8 8 t6 9

### 3.1.7 Transition Removal

We remove transition t6 using the following lexicographic ranking functions, which are bounded by [−5, 0].

 l2: [x, x − y] l1: [xs, xs − ys] l2a: [xs, xs − ys] l2b: [xs, xs − ys]
Hints:

### 3.1.8 SCC Decomposition

There exist no SCC in the program graph.

manual

• version: -