LTS Termination Proof

by T2Cert

Input

Integer Transition System
• Initial Location: 3
• Transitions: (pre-variables and post-variables)  0 0 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ −1 + arg1P − arg2P ≤ 0 ∧ 1 − arg1P + arg2P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 1 1 2: 1 + arg2 − arg3 ≤ 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 1 2 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ − arg2P + arg3 ≤ 0 ∧ arg2P − arg3 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 2 3 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg1 ≤ 0 ∧ arg2 − arg3 ≤ 0 ∧ − arg2 + arg3 ≤ 0 ∧ −1 + arg1 − arg2P ≤ 0 ∧ 1 − arg1 + arg2P ≤ 0 ∧ 1 + arg2 − arg3P ≤ 0 ∧ −1 − arg2 + arg3P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 3 4 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

Proof

1 Invariant Updates

The following invariants are asserted.

 0: TRUE 1: − arg1P ≤ 0 ∧ − arg1 ≤ 0 2: − arg1P ≤ 0 ∧ − arg1 ≤ 0 3: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

• nodes (location) invariant:  0 (0) TRUE 1 (1) − arg1P ≤ 0 ∧ − arg1 ≤ 0 2 (2) − arg1P ≤ 0 ∧ − arg1 ≤ 0 3 (3) TRUE
• initial node: 3
• cover edges:
• transition edges:  0 0 1 1 1 2 1 2 2 2 3 1 3 4 0

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 1 5 1: − 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, 4 using the following ranking functions, which are bounded by −11.

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

4 Location Addition

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

1* 8 1: arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

5 Location Addition

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

1 6 1_var_snapshot: arg3P + 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, 2, 1_var_snapshot, 1* }.

6.1.1 Transition Removal

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

 1: 0 2: arg2 − arg3 1_var_snapshot: 0 1*: 0

6.1.2 Splitting Cut-Point Transitions

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

6.1.2.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 5.

6.1.2.1.1 Fresh Variable Addition

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

 6: __snapshot_1_arg3P ≤ arg3P ∧ arg3P ≤ __snapshot_1_arg3P 8: __snapshot_1_arg3P ≤ __snapshot_1_arg3P ∧ __snapshot_1_arg3P ≤ __snapshot_1_arg3P 2: __snapshot_1_arg3P ≤ __snapshot_1_arg3P ∧ __snapshot_1_arg3P ≤ __snapshot_1_arg3P 3: __snapshot_1_arg3P ≤ __snapshot_1_arg3P ∧ __snapshot_1_arg3P ≤ __snapshot_1_arg3P

6.1.2.1.2 Fresh Variable Addition

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

 6: __snapshot_1_arg3 ≤ arg3 ∧ arg3 ≤ __snapshot_1_arg3 8: __snapshot_1_arg3 ≤ __snapshot_1_arg3 ∧ __snapshot_1_arg3 ≤ __snapshot_1_arg3 2: __snapshot_1_arg3 ≤ __snapshot_1_arg3 ∧ __snapshot_1_arg3 ≤ __snapshot_1_arg3 3: __snapshot_1_arg3 ≤ __snapshot_1_arg3 ∧ __snapshot_1_arg3 ≤ __snapshot_1_arg3

6.1.2.1.3 Fresh Variable Addition

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

 6: __snapshot_1_arg2P ≤ arg2P ∧ arg2P ≤ __snapshot_1_arg2P 8: __snapshot_1_arg2P ≤ __snapshot_1_arg2P ∧ __snapshot_1_arg2P ≤ __snapshot_1_arg2P 2: __snapshot_1_arg2P ≤ __snapshot_1_arg2P ∧ __snapshot_1_arg2P ≤ __snapshot_1_arg2P 3: __snapshot_1_arg2P ≤ __snapshot_1_arg2P ∧ __snapshot_1_arg2P ≤ __snapshot_1_arg2P

6.1.2.1.4 Fresh Variable Addition

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

 6: __snapshot_1_arg2 ≤ arg2 ∧ arg2 ≤ __snapshot_1_arg2 8: __snapshot_1_arg2 ≤ __snapshot_1_arg2 ∧ __snapshot_1_arg2 ≤ __snapshot_1_arg2 2: __snapshot_1_arg2 ≤ __snapshot_1_arg2 ∧ __snapshot_1_arg2 ≤ __snapshot_1_arg2 3: __snapshot_1_arg2 ≤ __snapshot_1_arg2 ∧ __snapshot_1_arg2 ≤ __snapshot_1_arg2

6.1.2.1.5 Fresh Variable Addition

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

 6: __snapshot_1_arg1P ≤ arg1P ∧ arg1P ≤ __snapshot_1_arg1P 8: __snapshot_1_arg1P ≤ __snapshot_1_arg1P ∧ __snapshot_1_arg1P ≤ __snapshot_1_arg1P 2: __snapshot_1_arg1P ≤ __snapshot_1_arg1P ∧ __snapshot_1_arg1P ≤ __snapshot_1_arg1P 3: __snapshot_1_arg1P ≤ __snapshot_1_arg1P ∧ __snapshot_1_arg1P ≤ __snapshot_1_arg1P

6.1.2.1.6 Fresh Variable Addition

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

 6: __snapshot_1_arg1 ≤ arg1 ∧ arg1 ≤ __snapshot_1_arg1 8: __snapshot_1_arg1 ≤ __snapshot_1_arg1 ∧ __snapshot_1_arg1 ≤ __snapshot_1_arg1 2: __snapshot_1_arg1 ≤ __snapshot_1_arg1 ∧ __snapshot_1_arg1 ≤ __snapshot_1_arg1 3: __snapshot_1_arg1 ≤ __snapshot_1_arg1 ∧ __snapshot_1_arg1 ≤ __snapshot_1_arg1

6.1.2.1.7 Invariant Updates

The following invariants are asserted.

 0: TRUE 1: arg2 − arg2P ≤ 0 ∧ −1 + arg1 − arg2P ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg1 ≤ 0 2: − arg1P ≤ 0 ∧ − arg1 ≤ 0 3: TRUE 1: arg2 − arg2P ≤ 0 ∧ −1 + arg1 − arg2P ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg1 ≤ 0 ∨ − __snapshot_1_arg2P + __snapshot_1_arg3 ≤ 0 ∧ arg2 − arg2P ≤ 0 ∧ 1 − __snapshot_1_arg2P + __snapshot_1_arg3 + arg2P − arg3 ≤ 0 ∧ −1 + arg1 − arg2P ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg1 ≤ 0 2: − __snapshot_1_arg2P + __snapshot_1_arg3 ≤ 0 ∧ −1 − __snapshot_1_arg2P + __snapshot_1_arg3 + arg1 − arg2 ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg1 ≤ 0 1_var_snapshot: −1 − __snapshot_1_arg2P + __snapshot_1_arg3 + arg1 − arg3 ≤ 0 ∧ − __snapshot_1_arg2P + __snapshot_1_arg3 + arg2 − arg3 ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg1 ≤ 0 1*: − __snapshot_1_arg2P + __snapshot_1_arg3 ≤ 0 ∧ arg2 − arg2P ≤ 0 ∧ 1 − __snapshot_1_arg2P + __snapshot_1_arg3 + arg2P − arg3 ≤ 0 ∧ −1 + arg1 − arg2P ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg1 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

• nodes (location) invariant:  0 (3) TRUE 1 (0) TRUE 2 (1) arg2 − arg2P ≤ 0 ∧ −1 + arg1 − arg2P ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg1 ≤ 0 3 (2) − arg1P ≤ 0 ∧ − arg1 ≤ 0 4 (2) − arg1P ≤ 0 ∧ − arg1 ≤ 0 5 (1) arg2 − arg2P ≤ 0 ∧ −1 + arg1 − arg2P ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg1 ≤ 0 6 (1_var_snapshot) −1 − __snapshot_1_arg2P + __snapshot_1_arg3 + arg1 − arg3 ≤ 0 ∧ − __snapshot_1_arg2P + __snapshot_1_arg3 + arg2 − arg3 ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg1 ≤ 0 11 (1) arg2 − arg2P ≤ 0 ∧ −1 + arg1 − arg2P ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg1 ≤ 0 15 (2) − __snapshot_1_arg2P + __snapshot_1_arg3 ≤ 0 ∧ −1 − __snapshot_1_arg2P + __snapshot_1_arg3 + arg1 − arg2 ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg1 ≤ 0 16 (1*) − __snapshot_1_arg2P + __snapshot_1_arg3 ≤ 0 ∧ arg2 − arg2P ≤ 0 ∧ 1 − __snapshot_1_arg2P + __snapshot_1_arg3 + arg2P − arg3 ≤ 0 ∧ −1 + arg1 − arg2P ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg1 ≤ 0 17 (1) − __snapshot_1_arg2P + __snapshot_1_arg3 ≤ 0 ∧ arg2 − arg2P ≤ 0 ∧ 1 − __snapshot_1_arg2P + __snapshot_1_arg3 + arg2P − arg3 ≤ 0 ∧ −1 + arg1 − arg2P ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg1 ≤ 0 18 (1_var_snapshot) −1 − __snapshot_1_arg2P + __snapshot_1_arg3 + arg1 − arg3 ≤ 0 ∧ − __snapshot_1_arg2P + __snapshot_1_arg3 + arg2 − arg3 ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg1 ≤ 0
• initial node: 0
• cover edges:  3 → 4 11 → 2 18 → 6
• transition edges:  0 4 1 1 0 2 2 1 3 2 2 4 2 5 5 4 3 11 5 6 6 6 2 15 15 3 16 16 8 17 17 6 18

6.1.2.1.8 Transition Removal

We remove transition 8 using the following ranking functions, which are bounded by −2.

 1: arg2P − arg3 2: __snapshot_1_arg2P − __snapshot_1_arg3 1_var_snapshot: __snapshot_1_arg2P − __snapshot_1_arg3 1*: __snapshot_1_arg2P − __snapshot_1_arg3

6.1.2.1.9 Transition Removal

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

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

6.1.2.1.10 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0