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

1 Invariant Updates

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:

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 }.

3.1.1 Location Addition

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

l2 t5 l2a: x = x ∧ y = y ∧ z = z

3.1.2 Location Addition

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

l2b t6 l2: x = x ∧ y = y ∧ z = z

3.1.3 Fresh Variable Addition

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

3.1.4 Fresh Variable Addition

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

3.1.5 Fresh Variable Addition

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

3.1.6 Invariant Updates

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.

Tool configuration

manual

version: -

3	→ 2
4	→ 1

7	→ 3
9	→ 3