by T2Cert
0 | 0 | 1: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg1P ≤ 0 ∧ arg1P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 | |
1 | 1 | 1: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ −10 + arg1 ≤ 0 ∧ −19 + arg1 ≤ 0 ∧ 2 − arg1P + arg1 ≤ 0 ∧ −2 + arg1P − arg1 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 | |
1 | 2 | 1: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 11 − arg1 ≤ 0 ∧ −19 + arg1 ≤ 0 ∧ 2 − arg1P + arg1 ≤ 0 ∧ −2 + arg1P − arg1 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 | |
2 | 3 | 0: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 |
1 | 4 | : | − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 |
We remove transitions
, using the following ranking functions, which are bounded by −11.2: | 0 |
0: | 0 |
1: | 0 |
: | −4 |
: | −5 |
: | −6 |
: | −6 |
: | −6 |
5 | lexWeak[ [0, 0, 0, 0] ] |
lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0] ] | |
lexStrict[ [0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0] ] | |
lexStrict[ [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.
7 : − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
5 : − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
We consider subproblems for each of the 1 SCC(s) of the program graph.
Here we consider the SCC {
, , }.We remove transitions
, using the following ranking functions, which are bounded by −20.: | 1 − arg1 |
: | − arg1 |
: | 1 − arg1 |
5 | lexWeak[ [0, 0, 0, 1] ] |
7 | lexWeak[ [0, 0, 0, 1] ] |
lexStrict[ [0, 0, 0, 0, 1, 0, 0, 1] , [0, 0, 0, 1, 0, 0, 0, 0] ] | |
lexStrict[ [0, 0, 0, 0, 1, 0, 0, 1] , [0, 0, 0, 1, 0, 0, 0, 0] ] |
We remove transitions 5, 7 using the following ranking functions, which are bounded by −1.
: | 0 |
: | −1 |
: | 1 |
5 | lexStrict[ [0, 0, 0, 0] , [0, 0, 0, 0] ] |
7 | lexStrict[ [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