LTS Termination Proof

by T2Cert

Input

• Initial Location: 17
• Transitions: (pre-variables and post-variables)

  0	0	1:		− y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  2	1	3:		− i_0 + nodecount_0 ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  2	2	4:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + i_0 − nodecount_0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  5	3	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 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  5	4	3:		− y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  7	5	8:		− y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  9	6	4:		0 ≤ 0 ∧ 0 ≤ 0 ∧ edgecount_0 − i_0 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  9	7	5:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − edgecount_0 + i_0 ≤ 0 ∧ x_0 − x_post ≤ 0 ∧ − x_0 + x_post ≤ 0 ∧ y_0 − y_post ≤ 0 ∧ − y_0 + y_post ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  10	8	11:		0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − j_0 + j_post ≤ 0 ∧ 1 + j_0 − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  11	9	12:		− y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  12	10	7:		0 ≤ 0 ∧ 0 ≤ 0 ∧ edgecount_0 − j_0 ≤ 0 ∧ −1 − i_0 + i_post ≤ 0 ∧ 1 + i_0 − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  12	11	10:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − edgecount_0 + j_0 ≤ 0 ∧ x_0 − x_post ≤ 0 ∧ − x_0 + x_post ≤ 0 ∧ y_0 − y_post ≤ 0 ∧ − y_0 + y_post ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  8	12	6:		0 ≤ 0 ∧ 0 ≤ 0 ∧ − i_0 + nodecount_0 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  8	13	11:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + i_0 − nodecount_0 ≤ 0 ∧ j_post ≤ 0 ∧ − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  13	14	14:		− y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  6	15	9:		− y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  14	16	0:		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 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  15	17	13:		1 − i_0 + source_0 ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  15	18	13:		1 + i_0 − source_0 ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  15	19	14:		i_0 − source_0 ≤ 0 ∧ − i_0 + source_0 ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  1	20	7:		0 ≤ 0 ∧ 0 ≤ 0 ∧ − i_0 + nodecount_0 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  1	21	15:		1 + i_0 − nodecount_0 ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  4	22	2:		− y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0
  16	23	0:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ −5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ edgecount_0 − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ nodecount_0 − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_post ≤ 0 ∧ source_0 − source_post ≤ 0 ∧ − source_0 + source_post ≤ 0 ∧ − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0
  17	24	16:		− y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0

Proof

1 Invariant Updates

The following invariants are asserted.

The invariants are proved as follows.

IMPACT Invariant Proof

• nodes (location) invariant:

  0		(0)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ −5 + edgecount_0 ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ −5 + nodecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  1		(1)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ −5 + edgecount_0 ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ −5 + nodecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  2		(2)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  3		(3)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  4		(4)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  5		(5)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ −5 + edgecount_0 ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  6		(6)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ −5 + edgecount_0 ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  7		(7)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ −5 + edgecount_0 ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  8		(8)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ −5 + edgecount_0 ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  9		(9)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ −5 + edgecount_0 ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  10		(10)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ −5 + edgecount_0 ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  11		(11)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ −5 + edgecount_0 ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  12		(12)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ −5 + edgecount_0 ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  13		(13)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ −5 + edgecount_0 ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ −5 + nodecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  14		(14)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ −5 + edgecount_0 ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ −5 + nodecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  15		(15)		−5 + edgecount_post ≤ 0 ∧ 5 − edgecount_post ≤ 0 ∧ −5 + nodecount_post ≤ 0 ∧ 5 − nodecount_post ≤ 0 ∧ source_post ≤ 0 ∧ − source_post ≤ 0 ∧ −5 + edgecount_0 ≤ 0 ∧ 5 − edgecount_0 ≤ 0 ∧ −5 + nodecount_0 ≤ 0 ∧ 5 − nodecount_0 ≤ 0 ∧ − source_0 ≤ 0
  16		(16)		TRUE
  17		(17)		TRUE

• initial node: 17
• cover edges:
• transition edges:

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

2 Switch to Cooperation Termination Proof

3 Transition Removal

We remove transitions 1, 4, 6, 12, 20, 23, 24 using the following ranking functions, which are bounded by −27.

4 Location Addition

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

0* 28 0: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0

5 Location Addition

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

0 26 0_var_snapshot: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0

6 Location Addition

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

4* 35 4: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0

7 Location Addition

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

4 33 4_var_snapshot: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0

8 Location Addition

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

6* 42 6: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0

9 Location Addition

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

6 40 6_var_snapshot: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0

10 Location Addition

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

7* 49 7: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0

11 Location Addition

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

7 47 7_var_snapshot: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0

12 Location Addition

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

11* 56 11: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0

13 Location Addition

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

11 54 11_var_snapshot: − y_post + y_post ≤ 0 ∧ y_post − y_post ≤ 0 ∧ − y_0 + y_0 ≤ 0 ∧ y_0 − y_0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 ∧ − source_post + source_post ≤ 0 ∧ source_post − source_post ≤ 0 ∧ − source_0 + source_0 ≤ 0 ∧ source_0 − source_0 ≤ 0 ∧ − nodecount_post + nodecount_post ≤ 0 ∧ nodecount_post − nodecount_post ≤ 0 ∧ − nodecount_0 + nodecount_0 ≤ 0 ∧ nodecount_0 − nodecount_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − edgecount_post + edgecount_post ≤ 0 ∧ edgecount_post − edgecount_post ≤ 0 ∧ − edgecount_0 + edgecount_0 ≤ 0 ∧ edgecount_0 − edgecount_0 ≤ 0

14 SCC Decomposition

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

14.1 SCC Subproblem 1/4

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

14.1.1 Transition Removal

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

14.1.2 Transition Removal

We remove transitions 33, 35, 22 using the following ranking functions, which are bounded by −1.

14.1.3 Splitting Cut-Point Transitions

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

14.1.3.1 Cut-Point Subproblem 1/1

14.1.3.1.1 Splitting Cut-Point Transitions

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

14.2 SCC Subproblem 2/4

Here we consider the SCC { 5, 6, 9, 6_var_snapshot, 6* }.

14.2.1 Transition Removal

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

14.2.2 Transition Removal

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

14.2.3 Transition Removal

We remove transition 40 using the following ranking functions, which are bounded by 4.

14.2.4 Splitting Cut-Point Transitions

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

14.2.4.1 Cut-Point Subproblem 1/1

14.2.4.1.1 Splitting Cut-Point Transitions

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

14.3 SCC Subproblem 3/4

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

14.3.1 Transition Removal

We remove transition 13 using the following ranking functions, which are bounded by 15.

14.3.2 Transition Removal

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

14.3.3 Transition Removal

We remove transitions 47, 49, 54, 5, 8, 9, 10 using the following ranking functions, which are bounded by −21.

14.3.4 Transition Removal

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

14.3.5 Splitting Cut-Point Transitions

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

14.3.5.1 Cut-Point Subproblem 1/2

14.3.5.1.1 Splitting Cut-Point Transitions

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

14.3.5.2 Cut-Point Subproblem 2/2

14.3.5.2.1 Splitting Cut-Point Transitions

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

14.4 SCC Subproblem 4/4

Here we consider the SCC { 0, 1, 13, 14, 15, 0_var_snapshot, 0* }.

14.4.1 Transition Removal

We remove transitions 18, 19, 21 using the following ranking functions, which are bounded by −26.

14.4.2 Transition Removal

We remove transitions 26, 28, 0, 14, 16 using the following ranking functions, which are bounded by −11.

14.4.3 Transition Removal

We remove transition 17 using the following ranking functions, which are bounded by 4.

14.4.4 Splitting Cut-Point Transitions

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

14.4.4.1 Cut-Point Subproblem 1/1

14.4.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