LTS Termination Proof

by T2Cert

Input

Integer Transition System

Initial Location: 11

Transitions: (pre-variables and post-variables)

0	0	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ b_16_0 − b_16_post ≤ 0 ∧ − b_16_0 + b_16_post ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0
1	4	5:	0 ≤ 0 ∧ 0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ rt_11_post − st_15_0 ≤ 0 ∧ − rt_11_post + st_15_0 ≤ 0 ∧ rt_11_0 − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_post ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − b_16_post + b_16_post ≤ 0 ∧ b_16_post − b_16_post ≤ 0 ∧ − b_16_0 + b_16_0 ≤ 0 ∧ b_16_0 − b_16_0 ≤ 0
1	5	6:	1 − x_14_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − b_16_post + b_16_post ≤ 0 ∧ b_16_post − b_16_post ≤ 0 ∧ − b_16_0 + b_16_0 ≤ 0 ∧ b_16_0 − b_16_0 ≤ 0
1	6	6:	1 + x_14_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − b_16_post + b_16_post ≤ 0 ∧ b_16_post − b_16_post ≤ 0 ∧ − b_16_0 + b_16_0 ≤ 0 ∧ b_16_0 − b_16_0 ≤ 0
6	7	4:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − b_16_0 ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − x_14_0 + x_14_post ≤ 0 ∧ −1 + x_14_0 − x_14_post ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 − b_16_post ≤ 0 ∧ − b_16_0 + b_16_post ≤ 0 ∧ x_14_0 − x_14_post ≤ 0 ∧ − x_14_0 + x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0
7	8	5:	0 ≤ 0 ∧ 0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ rt_11_post − st_15_0 ≤ 0 ∧ − rt_11_post + st_15_0 ≤ 0 ∧ rt_11_0 − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_post ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − b_16_post + b_16_post ≤ 0 ∧ b_16_post − b_16_post ≤ 0 ∧ − b_16_0 + b_16_0 ≤ 0 ∧ b_16_0 − b_16_0 ≤ 0
7	9	8:	1 − x_14_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − b_16_post + b_16_post ≤ 0 ∧ b_16_post − b_16_post ≤ 0 ∧ − b_16_0 + b_16_0 ≤ 0 ∧ b_16_0 − b_16_0 ≤ 0
7	10	8:	1 + x_14_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − b_16_post + b_16_post ≤ 0 ∧ b_16_post − b_16_post ≤ 0 ∧ − b_16_0 + b_16_0 ≤ 0 ∧ b_16_0 − b_16_0 ≤ 0
8	11	9:	2 − b_16_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − b_16_post + b_16_post ≤ 0 ∧ b_16_post − b_16_post ≤ 0 ∧ − b_16_0 + b_16_0 ≤ 0 ∧ b_16_0 − b_16_0 ≤ 0
8	12	9:	b_16_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − b_16_post + b_16_post ≤ 0 ∧ b_16_post − b_16_post ≤ 0 ∧ − b_16_0 + b_16_0 ≤ 0 ∧ b_16_0 − b_16_0 ≤ 0
9	13	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − x_14_0 + x_14_1 ≤ 0 ∧ 1 + x_14_0 − x_14_1 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ x_14_1 + x_14_post ≤ 0 ∧ − x_14_1 − x_14_post ≤ 0 ∧ b_16_0 − b_16_post ≤ 0 ∧ − b_16_0 + b_16_post ≤ 0 ∧ x_14_0 − x_14_post ≤ 0 ∧ − x_14_0 + x_14_post ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0
4	14	7:	0 ≤ 0 ∧ 0 ≤ 0 ∧ x_14_0 + x_14_post ≤ 0 ∧ − x_14_0 − x_14_post ≤ 0 ∧ x_14_0 − x_14_post ≤ 0 ∧ − x_14_0 + x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − b_16_post + b_16_post ≤ 0 ∧ b_16_post − b_16_post ≤ 0 ∧ − b_16_0 + b_16_0 ≤ 0 ∧ b_16_0 − b_16_0 ≤ 0
11	16	0:	− x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − b_16_post + b_16_post ≤ 0 ∧ b_16_post − b_16_post ≤ 0 ∧ − b_16_0 + b_16_0 ≤ 0 ∧ b_16_0 − b_16_0 ≤ 0

Proof

1 Invariant Updates

The following invariants are asserted.

0:	TRUE
1:	−1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
4:	b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
5:	−1 + b_16_post ≤ 0 ∧ x_14_0 ≤ 0 ∧ −1 + b_16_0 ≤ 0
6:	−1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
7:	b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
8:	b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
9:	b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0
11:	TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

nodes (location) invariant:

0	(0)	TRUE
1	(1)	−1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
4	(4)	b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
5	(5)	−1 + b_16_post ≤ 0 ∧ x_14_0 ≤ 0 ∧ −1 + b_16_0 ≤ 0
6	(6)	−1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
7	(7)	b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
8	(8)	b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
9	(9)	b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0
11	(11)	TRUE

initial node: 11
cover edges:
transition edges:

0 0 1

1 4 5

1 5 6

1 6 6

4 14 7

6 7 4

7 8 5

7 9 8

7 10 8

8 11 9

8 12 9

9 13 1

11 16 0

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

− x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − b_16_post + b_16_post ≤ 0 ∧ b_16_post − b_16_post ≤ 0 ∧ − b_16_0 + b_16_0 ≤ 0 ∧ b_16_0 − b_16_0 ≤ 0

and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 4, 8, 16 using the following ranking functions, which are bounded by −13.

11:	0
0:	0
1:	0
4:	0
6:	0
7:	0
8:	0
9:	0
5:	0
11:	−5
0:	−6
1:	−7
4:	−7
6:	−7
7:	−7
8:	−7
9:	−7
1_var_snapshot:	−7
1*:	−7
5:	−11

4 Location Addition

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

1* 20 1: − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − b_16_post + b_16_post ≤ 0 ∧ b_16_post − b_16_post ≤ 0 ∧ − b_16_0 + b_16_0 ≤ 0 ∧ b_16_0 − b_16_0 ≤ 0

5 Location Addition

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

1 18 1_var_snapshot: − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_1 + x_14_1 ≤ 0 ∧ x_14_1 − x_14_1 ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − st_15_0 + st_15_0 ≤ 0 ∧ st_15_0 − st_15_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − b_16_post + b_16_post ≤ 0 ∧ b_16_post − b_16_post ≤ 0 ∧ − b_16_0 + b_16_0 ≤ 0 ∧ b_16_0 − b_16_0 ≤ 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, 4, 6, 7, 8, 9, 1_var_snapshot, 1* }.

6.1.1 Transition Removal

We remove transition 10 using the following ranking functions, which are bounded by 7.

1:	−5 + 8⋅x_14_0
4:	1 + 8⋅x_14_0
6:	−6⋅b_16_0 + 8⋅x_14_0
7:	−8⋅x_14_0
8:	−11 − 8⋅x_14_0
9:	−12 − 8⋅x_14_0
1_var_snapshot:	−5⋅b_16_post + 8⋅x_14_0
1*:	−4⋅b_16_0 + 8⋅x_14_0

6.1.2 Transition Removal

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

1:	2⋅b_16_post + 3⋅x_14_0
4:	2 + 3⋅x_14_0
6:	3⋅x_14_0
7:	1 − 3⋅x_14_0
8:	−3⋅x_14_0
9:	−3⋅x_14_0
1_var_snapshot:	b_16_0 + 3⋅x_14_0
1*:	2 − 2⋅b_16_0 + 2⋅b_16_post + 3⋅x_14_0

6.1.3 Transition Removal

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

1:	0
4:	0
6:	0
7:	0
8:	0
9:	0
1_var_snapshot:	0
1*:	0

6.1.4 Splitting Cut-Point Transitions

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

6.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 17.

6.1.4.1.1 Invariant Updates

The following invariants are asserted.

0:	TRUE
1:	1 − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0 ∨ − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
4:	− x_14_0 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
5:	−1 + b_16_post ≤ 0 ∧ x_14_0 ≤ 0 ∧ −1 + b_16_0 ≤ 0
6:	1 − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0 ∨ 1 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
7:	x_14_0 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
8:	1 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0 ∨ 1 + x_14_0 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
9:	1 + x_14_0 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0
11:	TRUE
1:	1 − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0 ∨ − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
4:	− x_14_0 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
6:	1 − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0 ∨ 1 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
7:	x_14_0 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
8:	1 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
9:	1 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0
1_var_snapshot:	1 − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0 ∨ − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
1*:	1 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

nodes (location) invariant:

0	(11)	TRUE
1	(0)	TRUE
2	(1)	1 − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
3	(5)	−1 + b_16_post ≤ 0 ∧ x_14_0 ≤ 0 ∧ −1 + b_16_0 ≤ 0
4	(6)	1 − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
5	(6)	1 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
6	(1)	1 − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
7	(1_var_snapshot)	1 − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
20	(6)	1 − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
21	(4)	− x_14_0 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
22	(7)	x_14_0 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
23	(8)	1 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
32	(4)	− x_14_0 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
33	(7)	x_14_0 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
34	(5)	−1 + b_16_post ≤ 0 ∧ x_14_0 ≤ 0 ∧ −1 + b_16_0 ≤ 0
35	(8)	1 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
36	(8)	1 + x_14_0 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0 ∧ − b_16_0 ≤ 0
37	(9)	1 + x_14_0 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0
38	(9)	1 + x_14_0 ≤ 0 ∧ b_16_post ≤ 0 ∧ − b_16_post ≤ 0 ∧ b_16_0 ≤ 0
39	(1)	− x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
40	(5)	−1 + b_16_post ≤ 0 ∧ x_14_0 ≤ 0 ∧ −1 + b_16_0 ≤ 0
41	(6)	1 − x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
42	(6)	1 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
43	(1)	− x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
44	(1_var_snapshot)	− x_14_0 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0
49	(6)	1 ≤ 0 ∧ −1 + b_16_post ≤ 0 ∧ 1 − b_16_post ≤ 0 ∧ −1 + b_16_0 ≤ 0 ∧ 1 − b_16_0 ≤ 0

initial node: 0
cover edges:

34 → 3

37 → 38

40 → 3

41 → 4

transition edges:

0	16 1
1	0 2
2	4 3
2	5 4
2	6 5
2	17 6
4	7 32
6	18 7
7	6 20
20	7 21
21	14 22
22	9 23
32	14 33
33	8 34
33	9 35
33	10 36
36	11 37
36	12 38
38	13 39
39	4 40
39	5 41
39	6 42
39	17 43
43	18 44
44	6 49

6.1.4.1.2 Transition Removal

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

1:	−1
9:	−2
1_var_snapshot:	−3
6:	−4
4:	−5
7:	−6
8:	−7
1*:	−8

6.1.4.1.3 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert

version: 1.0

34	→ 3
37	→ 38
40	→ 3
41	→ 4