LTS Termination Proof

by AProVE

Input

• Initial Location: l4, l7, l6, l1, l3, l0, l2
• Transitions: (pre-variables and post-variables)

  l0	1	l1:		x1 = ___const_42HAT0 ∧ x2 = _i1HAT0 ∧ x1 = ___const_42HATpost ∧ x2 = _i1HATpost ∧ ___const_42HAT0 = ___const_42HATpost ∧ _i1HATpost = 1 + _i1HAT0
  l2	2	l0:		x1 = _x ∧ x2 = _x1 ∧ x1 = _x2 ∧ x2 = _x3 ∧ _x1 = _x3 ∧ _x = _x2
  l3	3	l2:		x1 = _x4 ∧ x2 = _x5 ∧ x1 = _x6 ∧ x2 = _x7 ∧ _x5 = _x7 ∧ _x4 = _x6
  l3	4	l0:		x1 = _x8 ∧ x2 = _x9 ∧ x1 = _x10 ∧ x2 = _x11 ∧ _x9 = _x11 ∧ _x8 = _x10
  l4	5	l5:		x1 = _x12 ∧ x2 = _x13 ∧ x1 = _x14 ∧ x2 = _x15 ∧ _x13 = _x15 ∧ _x12 = _x14 ∧ _x12 ≤ _x13
  l4	6	l3:		x1 = _x16 ∧ x2 = _x17 ∧ x1 = _x18 ∧ x2 = _x19 ∧ _x17 = _x19 ∧ _x16 = _x18 ∧ 1 + _x17 ≤ _x16
  l1	7	l4:		x1 = _x20 ∧ x2 = _x21 ∧ x1 = _x22 ∧ x2 = _x23 ∧ _x21 = _x23 ∧ _x20 = _x22
  l6	8	l1:		x1 = _x24 ∧ x2 = _x25 ∧ x1 = _x26 ∧ x2 = _x27 ∧ _x24 = _x26 ∧ _x27 = 0
  l7	9	l6:		x1 = _x28 ∧ x2 = _x29 ∧ x1 = _x30 ∧ x2 = _x31 ∧ _x29 = _x31 ∧ _x28 = _x30

Proof

1 Switch to Cooperation Termination Proof

2 SCC Decomposition

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

2.1 SCC Subproblem 1/1

Here we consider the SCC { l4, l1, l3, l0, l2 }.

2.1.1 Transition Removal

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

2.1.2 Transition Removal

We remove transitions 1, 4, 2, 3, 7 using the following ranking functions, which are bounded by 0.

2.1.3 Trivial Cooperation Program

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

Tool configuration

AProVE

• version: AProVE Commit ID: unknown
• strategy: Statistics for single proof: 100.00 % (5 real / 0 unknown / 0 assumptions / 5 total proof steps)