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 ∧ 1 − arg1P + arg1 ≤ 0 ∧ −1 + arg1P − arg1 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 | |
1 | 2 | 1: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ −9 + arg1 ≤ 0 ∧ −19 + arg1 ≤ 0 ∧ 1 − arg1P + arg1 ≤ 0 ∧ −1 + 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 |
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 −58.: | 1 − 3⋅arg1 |
: | −3⋅arg1 |
: | 2 − 3⋅arg1 |
We remove transitions 5, 7 using the following ranking functions, which are bounded by −1.
: | 0 |
: | −1 |
: | 1 |
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