LTS Termination Proof

by T2Cert

Input

Integer Transition System
• Initial Location: 6
• Transitions: (pre-variables and post-variables)  0 0 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ − oldX1_post + x0_post ≤ 0 ∧ oldX1_post − x0_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 2 1 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ −1 − oldX0_post + x0_post ≤ 0 ∧ 1 + oldX0_post − x0_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 3 2 0: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ 20 − oldX0_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 3 3 2: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ −19 + oldX0_post ≤ 0 ∧ − oldX0_post + x0_post ≤ 0 ∧ oldX0_post − x0_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 4 4 3: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ x0_post ≤ 0 ∧ − x0_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 5 5 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ oldX0_post − x0_0 ≤ 0 ∧ − oldX0_post + x0_0 ≤ 0 ∧ − oldX1_post + x0_post ≤ 0 ∧ oldX1_post − x0_post ≤ 0 ∧ oldX0_0 − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_post ≤ 0 ∧ oldX1_0 − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_post ≤ 0 ∧ x0_0 − x0_post ≤ 0 ∧ − x0_0 + x0_post ≤ 0 5 6 1: − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0 5 7 0: − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0 5 8 2: − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0 5 9 3: − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0 5 10 4: − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0 6 11 5: − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 3 12 3: − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 0, 2, 4, 5, 6, 7, 8, 9, 10, 11 using the following ranking functions, which are bounded by −17.

 6: 0 5: 0 4: 0 2: 0 3: 0 0: 0 1: 0 6: −7 5: −8 4: −9 2: −10 3: −10 3_var_snapshot: −10 3*: −10 0: −14 1: −15

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

3* 15 3: x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

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

3 13 3_var_snapshot: x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

5 SCC Decomposition

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

5.1 SCC Subproblem 1/1

Here we consider the SCC { 2, 3, 3_var_snapshot, 3* }.

5.1.1 Transition Removal

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

 2: −1 − 2⋅x0_0 3: −2⋅x0_0 3_var_snapshot: −2⋅x0_0 3*: −2⋅x0_0

5.1.2 Transition Removal

We remove transitions 13, 15, 1 using the following ranking functions, which are bounded by −3.

 2: 0 3: −2 3_var_snapshot: −3 3*: −1

5.1.3 Splitting Cut-Point Transitions

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

5.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 12.

5.1.3.1.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0