by T2Cert
0 | 0 | 1: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 9 − arg1P ≤ 0 ∧ −9 + arg1P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 | |
1 | 1 | 1: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg1 ≤ 0 ∧ −1 − arg1P + arg1 ≤ 0 ∧ 1 + arg1P − arg1 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 | |
2 | 2 | 0: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 |
1 | 3 | : | − 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 |
4 | lexWeak[ [0, 0, 0, 0] ] |
lexWeak[ [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.
6 : − 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.
4 : − 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 transition
using the following ranking functions, which are bounded by −1.: | 1 + 3⋅arg1 |
: | 3⋅arg1 |
: | 2 + 3⋅arg1 |
4 | lexWeak[ [0, 0, 3, 0] ] |
6 | lexWeak[ [0, 0, 3, 0] ] |
lexStrict[ [0, 0, 0, 0, 3, 3, 0] , [0, 0, 3, 0, 0, 0, 0] ] |
We remove transitions 4, 6 using the following ranking functions, which are bounded by −2.
: | −1 |
: | −2 |
: | 0 |
4 | lexStrict[ [0, 0, 0, 0] , [0, 0, 0, 0] ] |
6 | 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