LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
2 56 2: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0
4 63 4: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0
12 70 12: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0
17 77 17: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0
19 84 19: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 0, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 14, 15, 16, 17, 19, 21, 22, 28, 29, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55 using the following ranking functions, which are bounded by −45.

22: 0
21: 0
15: 0
9: 0
6: 0
7: 0
10: 0
0: 0
2: 0
18: 0
19: 0
20: 0
1: 0
16: 0
17: 0
11: 0
12: 0
13: 0
14: 0
3: 0
4: 0
5: 0
8: 0
22: −17
21: −18
15: −19
9: −20
6: −21
7: −22
10: −23
0: −24
2: −24
18: −24
19: −24
20: −24
2_var_snapshot: −24
2*: −24
19_var_snapshot: −24
19*: −24
1: −25
16: −26
17: −26
17_var_snapshot: −26
17*: −26
11: −29
12: −29
12_var_snapshot: −29
12*: −29
13: −32
14: −33
3: −38
4: −38
4_var_snapshot: −38
4*: −38
5: −42
8: −43

3 Location Addition

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

2* 59 2: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

4 Location Addition

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

2 57 2_var_snapshot: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

5 Location Addition

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

4* 66 4: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

6 Location Addition

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

4 64 4_var_snapshot: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

7 Location Addition

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

12* 73 12: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

8 Location Addition

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

12 71 12_var_snapshot: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

9 Location Addition

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

17* 80 17: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

10 Location Addition

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

17 78 17_var_snapshot: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

11 Location Addition

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

19* 87 19: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

12 Location Addition

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

19 85 19_var_snapshot: x7_post + x7_post ≤ 0x7_postx7_post ≤ 0x7_0 + x7_0 ≤ 0x7_0x7_0 ≤ 0x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x5_post + x5_post ≤ 0x5_postx5_post ≤ 0x5_0 + x5_0 ≤ 0x5_0x5_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0x3_post + x3_post ≤ 0x3_postx3_post ≤ 0x3_0 + x3_0 ≤ 0x3_0x3_0 ≤ 0x2_post + x2_post ≤ 0x2_postx2_post ≤ 0x2_0 + x2_0 ≤ 0x2_0x2_0 ≤ 0x1_post + x1_post ≤ 0x1_postx1_post ≤ 0x1_0 + x1_0 ≤ 0x1_0x1_0 ≤ 0x0_post + x0_post ≤ 0x0_postx0_post ≤ 0x0_0 + x0_0 ≤ 0x0_0x0_0 ≤ 0oldX9_post + oldX9_post ≤ 0oldX9_postoldX9_post ≤ 0oldX9_0 + oldX9_0 ≤ 0oldX9_0oldX9_0 ≤ 0oldX8_post + oldX8_post ≤ 0oldX8_postoldX8_post ≤ 0oldX8_0 + oldX8_0 ≤ 0oldX8_0oldX8_0 ≤ 0oldX7_post + oldX7_post ≤ 0oldX7_postoldX7_post ≤ 0oldX7_0 + oldX7_0 ≤ 0oldX7_0oldX7_0 ≤ 0oldX6_post + oldX6_post ≤ 0oldX6_postoldX6_post ≤ 0oldX6_0 + oldX6_0 ≤ 0oldX6_0oldX6_0 ≤ 0oldX5_post + oldX5_post ≤ 0oldX5_postoldX5_post ≤ 0oldX5_0 + oldX5_0 ≤ 0oldX5_0oldX5_0 ≤ 0oldX4_post + oldX4_post ≤ 0oldX4_postoldX4_post ≤ 0oldX4_0 + oldX4_0 ≤ 0oldX4_0oldX4_0 ≤ 0oldX3_post + oldX3_post ≤ 0oldX3_postoldX3_post ≤ 0oldX3_0 + oldX3_0 ≤ 0oldX3_0oldX3_0 ≤ 0oldX2_post + oldX2_post ≤ 0oldX2_postoldX2_post ≤ 0oldX2_0 + oldX2_0 ≤ 0oldX2_0oldX2_0 ≤ 0oldX1_post + oldX1_post ≤ 0oldX1_postoldX1_post ≤ 0oldX1_0 + oldX1_0 ≤ 0oldX1_0oldX1_0 ≤ 0oldX16_post + oldX16_post ≤ 0oldX16_postoldX16_post ≤ 0oldX16_0 + oldX16_0 ≤ 0oldX16_0oldX16_0 ≤ 0oldX15_post + oldX15_post ≤ 0oldX15_postoldX15_post ≤ 0oldX15_0 + oldX15_0 ≤ 0oldX15_0oldX15_0 ≤ 0oldX14_post + oldX14_post ≤ 0oldX14_postoldX14_post ≤ 0oldX14_0 + oldX14_0 ≤ 0oldX14_0oldX14_0 ≤ 0oldX13_post + oldX13_post ≤ 0oldX13_postoldX13_post ≤ 0oldX13_0 + oldX13_0 ≤ 0oldX13_0oldX13_0 ≤ 0oldX12_post + oldX12_post ≤ 0oldX12_postoldX12_post ≤ 0oldX12_0 + oldX12_0 ≤ 0oldX12_0oldX12_0 ≤ 0oldX11_post + oldX11_post ≤ 0oldX11_postoldX11_post ≤ 0oldX11_0 + oldX11_0 ≤ 0oldX11_0oldX11_0 ≤ 0oldX10_post + oldX10_post ≤ 0oldX10_postoldX10_post ≤ 0oldX10_0 + oldX10_0 ≤ 0oldX10_0oldX10_0 ≤ 0oldX0_post + oldX0_post ≤ 0oldX0_postoldX0_post ≤ 0oldX0_0 + oldX0_0 ≤ 0oldX0_0oldX0_0 ≤ 0

13 SCC Decomposition

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

13.1 SCC Subproblem 1/4

Here we consider the SCC { 11, 12, 12_var_snapshot, 12* }.

13.1.1 Transition Removal

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

11: 3 + 4⋅x7_0
12: 1 + 4⋅x6_0
12_var_snapshot: 4⋅x6_0
12*: 2 + 4⋅x6_0

13.1.2 Transition Removal

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

11: 2
12: 0
12_var_snapshot: −1
12*: 1

13.1.3 Splitting Cut-Point Transitions

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

13.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 70.

13.1.3.1.1 Splitting Cut-Point Transitions

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

13.2 SCC Subproblem 2/4

Here we consider the SCC { 16, 17, 17_var_snapshot, 17* }.

13.2.1 Transition Removal

We remove transition 23 using the following ranking functions, which are bounded by 63.

16: −16 + 4⋅x5_0
17: 16 + 4⋅x5_0
17_var_snapshot: 4⋅x5_0
17*: 32 + 4⋅x5_0

13.2.2 Transition Removal

We remove transitions 78, 80, 20 using the following ranking functions, which are bounded by −2.

16: 1
17: −1
17_var_snapshot: −2
17*: 0

13.2.3 Splitting Cut-Point Transitions

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

13.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 77.

13.2.3.1.1 Splitting Cut-Point Transitions

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

13.3 SCC Subproblem 3/4

Here we consider the SCC { 0, 2, 18, 19, 20, 2_var_snapshot, 2*, 19_var_snapshot, 19* }.

13.3.1 Transition Removal

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

0: −49964 + 9⋅x4_0
2: −49966 + 9⋅x4_0
18: −49963 + 9⋅x5_0
19: 9⋅x5_0
20: 9⋅x5_0
2_var_snapshot: −49967 + 9⋅x4_0
2*: −49965 + 9⋅x4_0
19_var_snapshot: 9⋅x5_0
19*: 9⋅x5_0

13.3.2 Transition Removal

We remove transitions 57, 26, 30 using the following ranking functions, which are bounded by −1384.

0: −1393 + 4⋅oldX6_post
2: 1
18: −1392 + 4⋅x6_0
19: −1390 + 4⋅x6_0
20: −1388 + 4⋅x6_0