by T2Cert
0 | 0 | 1: | ___const_20_0 − j_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 | |
0 | 1 | 2: | 1 − ___const_20_0 + j_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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 | |
2 | 2 | 0: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −2 − j_0 + j_post ≤ 0 ∧ 2 + j_0 − j_post ≤ 0 ∧ −2 + i_post − j_post ≤ 0 ∧ 2 − i_post + j_post ≤ 0 ∧ i_0 − i_post ≤ 0 ∧ − i_0 + i_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 | |
3 | 3 | 2: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ j_post ≤ 0 ∧ − j_post ≤ 0 ∧ j_0 − j_post ≤ 0 ∧ − j_0 + j_post ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 | |
4 | 4 | 3: | − 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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 |
2 | 5 | : | − 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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0 |
We remove transitions
, , using the following ranking functions, which are bounded by −13.4: | 0 |
3: | 0 |
0: | 0 |
2: | 0 |
1: | 0 |
: | −5 |
: | −6 |
: | −7 |
: | −7 |
: | −7 |
: | −7 |
: | −8 |
6 | lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] |
lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexWeak[ [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] ] | |
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] ] | |
lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] |
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
8 : − 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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
6 : − 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 ∧ − ___const_20_0 + ___const_20_0 ≤ 0 ∧ ___const_20_0 − ___const_20_0 ≤ 0
We consider subproblems for each of the 1 SCC(s) of the program graph.
Here we consider the SCC {
, , , }.We remove transition
using the following ranking functions, which are bounded by 7.: | 5 + 3⋅___const_20_0 − 3⋅j_0 |
: | 1 + 3⋅___const_20_0 − 3⋅j_0 |
: | 3⋅___const_20_0 − 3⋅j_0 |
: | 2 + 3⋅___const_20_0 − 3⋅j_0 |
6 | lexWeak[ [0, 0, 0, 3, 0, 0, 0, 0, 3, 0] ] |
8 | lexWeak[ [0, 0, 0, 3, 0, 0, 0, 0, 3, 0] ] |
lexStrict[ [0, 0, 0, 0, 3, 0, 0, 0, 0, 3, 0] , [3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexWeak[ [0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 3, 3, 0] ] |
We remove transitions 6, 8, using the following ranking functions, which are bounded by −1.
: | −1 |
: | 1 |
: | 0 |
: | 2 |
6 | lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] |
8 | lexStrict[ [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] ] |
We consider 1 subproblems corresponding to sets of cut-point transitions as follows.
There remain no cut-point transition to consider. Hence the cooperation termination is trivial.
T2Cert