LTS Termination Proof

by T2Cert

Input

Integer Transition System

Initial Location: 18

Transitions: (pre-variables and post-variables)

0	0	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − i_0 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
0	1	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ i_0 ≤ 0 ∧ i2_post − i_0 ≤ 0 ∧ − i2_post + i_0 ≤ 0 ∧ i2_0 − i2_post ≤ 0 ∧ − i2_0 + i2_post ≤ 0 ∧ − r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0
3	2	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
4	3	5:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
5	4	3:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
6	5	0:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
7	6	4:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
7	7	4:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
7	8	5:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
8	9	7:	0 ≤ 0 ∧ 0 ≤ 0 ∧ r_0 − r_post ≤ 0 ∧ − r_0 + r_post ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
9	10	8:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
9	11	3:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
9	12	8:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
10	13	11:	1 − i_0 ≤ 0 ∧ − r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
10	14	9:	i_0 ≤ 0 ∧ − r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
12	15	6:	0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
1	16	10:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
13	17	14:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
14	18	12:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
15	19	13:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
15	20	13:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
15	21	14:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
16	22	15:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
2	23	16:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
2	24	12:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
2	25	16:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
17	26	6:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
18	27	17:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0

Proof

1 Invariant Updates

The following invariants are asserted.

0:	i_1 ≤ 0 ∧ − i_1 ≤ 0
1:	i_1 ≤ 0 ∧ − i_1 ≤ 0
2:	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0 ∧ i2_post ≤ 0 ∧ i2_0 ≤ 0
3:	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0
4:	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0
5:	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0
6:	i_1 ≤ 0 ∧ − i_1 ≤ 0
7:	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0
8:	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0
9:	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0
10:	i_1 ≤ 0 ∧ − i_1 ≤ 0
11:	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ 1 − i_0 ≤ 0
12:	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0 ∧ i2_post ≤ 0 ∧ i2_0 ≤ 0
13:	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0 ∧ i2_post ≤ 0 ∧ i2_0 ≤ 0
14:	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0 ∧ i2_post ≤ 0 ∧ i2_0 ≤ 0
15:	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0 ∧ i2_post ≤ 0 ∧ i2_0 ≤ 0
16:	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0 ∧ i2_post ≤ 0 ∧ i2_0 ≤ 0
17:	TRUE
18:	TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

nodes (location) invariant:

0	(0)	i_1 ≤ 0 ∧ − i_1 ≤ 0
1	(1)	i_1 ≤ 0 ∧ − i_1 ≤ 0
2	(2)	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0 ∧ i2_post ≤ 0 ∧ i2_0 ≤ 0
3	(3)	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0
4	(4)	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0
5	(5)	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0
6	(6)	i_1 ≤ 0 ∧ − i_1 ≤ 0
7	(7)	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0
8	(8)	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0
9	(9)	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0
10	(10)	i_1 ≤ 0 ∧ − i_1 ≤ 0
11	(11)	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ 1 − i_0 ≤ 0
12	(12)	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0 ∧ i2_post ≤ 0 ∧ i2_0 ≤ 0
13	(13)	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0 ∧ i2_post ≤ 0 ∧ i2_0 ≤ 0
14	(14)	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0 ∧ i2_post ≤ 0 ∧ i2_0 ≤ 0
15	(15)	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0 ∧ i2_post ≤ 0 ∧ i2_0 ≤ 0
16	(16)	i_1 ≤ 0 ∧ − i_1 ≤ 0 ∧ i_0 ≤ 0 ∧ i2_post ≤ 0 ∧ i2_0 ≤ 0
17	(17)	TRUE
18	(18)	TRUE

initial node: 18
cover edges:

transition edges:

0	0 1
0	1 2
1	16 10
2	23 16
2	24 12
2	25 16
3	2 1
4	3 5
5	4 3
6	5 0
7	6 4
7	7 4
7	8 5
8	9 7
9	10 8
9	11 3
9	12 8
10	13 11
10	14 9
12	15 6
13	17 14
14	18 12
15	19 13
15	20 13
15	21 14
16	22 15
17	26 6
18	27 17

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

1	28	1:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0
6	35	6:	− r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0

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

3 Transition Removal

We remove transitions 0, 13, 26, 27 using the following ranking functions, which are bounded by −17.

18:	0
17:	0
0:	0
2:	0
6:	0
12:	0
13:	0
14:	0
15:	0
16:	0
1:	0
3:	0
4:	0
5:	0
7:	0
8:	0
9:	0
10:	0
11:	0
18:	−6
17:	−7
0:	−8
2:	−8
6:	−8
12:	−8
13:	−8
14:	−8
15:	−8
16:	−8
6_var_snapshot:	−8
6*:	−8
1:	−9
3:	−9
4:	−9
5:	−9
7:	−9
8:	−9
9:	−9
10:	−9
1_var_snapshot:	−9
1*:	−9
11:	−10

4 Location Addition

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

1* 31 1: − r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0

5 Location Addition

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

1 29 1_var_snapshot: − r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0

6 Location Addition

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

6* 38 6: − r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0

7 Location Addition

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

6 36 6_var_snapshot: − r_post + r_post ≤ 0 ∧ r_post − r_post ≤ 0 ∧ − r_0 + r_0 ≤ 0 ∧ r_0 − r_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_1 + i_1 ≤ 0 ∧ i_1 − i_1 ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i2_post + i2_post ≤ 0 ∧ i2_post − i2_post ≤ 0 ∧ − i2_0 + i2_0 ≤ 0 ∧ i2_0 − i2_0 ≤ 0

8 SCC Decomposition

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

8.1 SCC Subproblem 1/2

Here we consider the SCC { 1, 3, 4, 5, 7, 8, 9, 10, 1_var_snapshot, 1* }.

8.1.1 Transition Removal

We remove transitions 2, 3, 4, 6, 7, 8, 9, 10, 12, 14 using the following ranking functions, which are bounded by −8.

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

8.1.2 Transition Removal

We remove transitions 29, 31, 11, 16 using the following ranking functions, which are bounded by −3.

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

8.1.3 Splitting Cut-Point Transitions

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

8.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 28.

8.1.3.1.1 Splitting Cut-Point Transitions

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

8.2 SCC Subproblem 2/2

Here we consider the SCC { 0, 2, 6, 12, 13, 14, 15, 16, 6_var_snapshot, 6* }.

8.2.1 Transition Removal

We remove transitions 1, 15, 17, 18, 19, 20, 21, 22, 23, 24, 25 using the following ranking functions, which are bounded by −6.

0:	1 − 10⋅i_0
2:	−10⋅i_0
6:	3 − 10⋅i_0
12:	−5 − 10⋅i_0
13:	−3 − 10⋅i_0
14:	−4 − 10⋅i_0
15:	−2 − 10⋅i_0
16:	−1 − 10⋅i_0
6_var_snapshot:	2 − 10⋅i_0
6*:	4 − 10⋅i_0

8.2.2 Transition Removal

We remove transitions 36, 38 using the following ranking functions, which are bounded by −1.

0:	−2
2:	0
6:	0
12:	0
13:	0
14:	0
15:	0
16:	0
6_var_snapshot:	−1
6*:	1

8.2.3 Transition Removal

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

0:	0
2:	0
6:	0
12:	0
13:	0
14:	0
15:	0
16:	0
6_var_snapshot:	1
6*:	0

8.2.4 Splitting Cut-Point Transitions

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

8.2.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 35.

8.2.4.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert

version: 1.0