LTS Termination Proof

by manual

Input

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

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

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 Transition Removal

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

3.1.2 SCC Decomposition

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

3.1.2.1 SCC Subproblem 1/1

Here we consider the SCC { l2 }.

3.1.2.1.1 Transition Removal

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

3.1.2.1.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

Tool configuration

manual

• version: -