by T2Cert
0 | 0 | 1: | − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 ∧ − tmp2_post + tmp2_post ≤ 0 ∧ tmp2_post − tmp2_post ≤ 0 ∧ − tmp2_0 + tmp2_0 ≤ 0 ∧ tmp2_0 − tmp2_0 ≤ 0 ∧ − tmp1_post + tmp1_post ≤ 0 ∧ tmp1_post − tmp1_post ≤ 0 ∧ − tmp1_0 + tmp1_0 ≤ 0 ∧ tmp1_0 − tmp1_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 | |
2 | 1 | 0: | − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 ∧ − tmp2_post + tmp2_post ≤ 0 ∧ tmp2_post − tmp2_post ≤ 0 ∧ − tmp2_0 + tmp2_0 ≤ 0 ∧ tmp2_0 − tmp2_0 ≤ 0 ∧ − tmp1_post + tmp1_post ≤ 0 ∧ tmp1_post − tmp1_post ≤ 0 ∧ − tmp1_0 + tmp1_0 ≤ 0 ∧ tmp1_0 − tmp1_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 | |
2 | 2 | 0: | − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 ∧ − tmp2_post + tmp2_post ≤ 0 ∧ tmp2_post − tmp2_post ≤ 0 ∧ − tmp2_0 + tmp2_0 ≤ 0 ∧ tmp2_0 − tmp2_0 ≤ 0 ∧ − tmp1_post + tmp1_post ≤ 0 ∧ tmp1_post − tmp1_post ≤ 0 ∧ − tmp1_0 + tmp1_0 ≤ 0 ∧ tmp1_0 − tmp1_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 | |
3 | 3 | 2: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ i_post ≤ 0 ∧ − i_post ≤ 0 ∧ −1 + j_post ≤ 0 ∧ 1 − j_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ tmp1_0 − tmp1_post ≤ 0 ∧ − tmp1_0 + tmp1_post ≤ 0 ∧ tmp2_0 − tmp2_post ≤ 0 ∧ − tmp2_0 + tmp2_post ≤ 0 ∧ tmp3_0 − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_post ≤ 0 | |
4 | 4 | 3: | − tmp3_post + tmp3_post ≤ 0 ∧ tmp3_post − tmp3_post ≤ 0 ∧ − tmp3_0 + tmp3_0 ≤ 0 ∧ tmp3_0 − tmp3_0 ≤ 0 ∧ − tmp2_post + tmp2_post ≤ 0 ∧ tmp2_post − tmp2_post ≤ 0 ∧ − tmp2_0 + tmp2_0 ≤ 0 ∧ tmp2_0 − tmp2_0 ≤ 0 ∧ − tmp1_post + tmp1_post ≤ 0 ∧ tmp1_post − tmp1_post ≤ 0 ∧ − tmp1_0 + tmp1_0 ≤ 0 ∧ tmp1_0 − tmp1_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 |
The following invariants are asserted.
0: | i_post ≤ 0 ∧ − i_post ≤ 0 ∧ −1 + j_post ≤ 0 ∧ 1 − j_post ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ −1 + j_0 ≤ 0 ∧ 1 − j_0 ≤ 0 |
1: | i_post ≤ 0 ∧ − i_post ≤ 0 ∧ −1 + j_post ≤ 0 ∧ 1 − j_post ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ −1 + j_0 ≤ 0 ∧ 1 − j_0 ≤ 0 |
2: | i_post ≤ 0 ∧ − i_post ≤ 0 ∧ −1 + j_post ≤ 0 ∧ 1 − j_post ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ −1 + j_0 ≤ 0 ∧ 1 − j_0 ≤ 0 |
3: | TRUE |
4: | TRUE |
The invariants are proved as follows.
0 | (0) | i_post ≤ 0 ∧ − i_post ≤ 0 ∧ −1 + j_post ≤ 0 ∧ 1 − j_post ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ −1 + j_0 ≤ 0 ∧ 1 − j_0 ≤ 0 | ||
1 | (1) | i_post ≤ 0 ∧ − i_post ≤ 0 ∧ −1 + j_post ≤ 0 ∧ 1 − j_post ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ −1 + j_0 ≤ 0 ∧ 1 − j_0 ≤ 0 | ||
2 | (2) | i_post ≤ 0 ∧ − i_post ≤ 0 ∧ −1 + j_post ≤ 0 ∧ 1 − j_post ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ −1 + j_0 ≤ 0 ∧ 1 − j_0 ≤ 0 | ||
3 | (3) | TRUE | ||
4 | (4) | TRUE |
0 | 0 1 | |
2 | 1 0 | |
2 | 2 0 | |
3 | 3 2 | |
4 | 4 3 |
We remove transitions
, , , , using the following ranking functions, which are bounded by −12.4: | 0 |
3: | 0 |
2: | 0 |
0: | 0 |
1: | 0 |
: | −6 |
: | −7 |
: | −8 |
: | −9 |
: | −10 |
lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] |
There exist no SCC in the program graph.
T2Cert