by T2Cert
0 | 0 | 1: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ i_13_post ≤ 0 ∧ − i_13_post ≤ 0 ∧ − i_13_post ≤ 0 ∧ i_13_post ≤ 0 ∧ i_13_0 − i_13_post ≤ 0 ∧ − i_13_0 + i_13_post ≤ 0 ∧ − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − i_21_post + i_21_post ≤ 0 ∧ i_21_post − i_21_post ≤ 0 ∧ − i_21_0 + i_21_0 ≤ 0 ∧ i_21_0 − i_21_0 ≤ 0 ∧ − i_13_1 + i_13_1 ≤ 0 ∧ i_13_1 − i_13_1 ≤ 0 ∧ − a_20_post + a_20_post ≤ 0 ∧ a_20_post − a_20_post ≤ 0 ∧ − a_20_0 + a_20_0 ≤ 0 ∧ a_20_0 − a_20_0 ≤ 0 | |
1 | 3 | 4: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 10 − i_13_0 ≤ 0 ∧ rt_11_post − st_14_0 ≤ 0 ∧ − rt_11_post + st_14_0 ≤ 0 ∧ rt_11_0 − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_post ≤ 0 ∧ − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 ∧ − i_21_post + i_21_post ≤ 0 ∧ i_21_post − i_21_post ≤ 0 ∧ − i_21_0 + i_21_0 ≤ 0 ∧ i_21_0 − i_21_0 ≤ 0 ∧ − i_13_post + i_13_post ≤ 0 ∧ i_13_post − i_13_post ≤ 0 ∧ − i_13_1 + i_13_1 ≤ 0 ∧ i_13_1 − i_13_1 ≤ 0 ∧ − i_13_0 + i_13_0 ≤ 0 ∧ i_13_0 − i_13_0 ≤ 0 ∧ − a_20_post + a_20_post ≤ 0 ∧ a_20_post − a_20_post ≤ 0 ∧ − a_20_0 + a_20_0 ≤ 0 ∧ a_20_0 − a_20_0 ≤ 0 | |
1 | 4 | 5: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −9 + i_13_0 ≤ 0 ∧ −1 − i_13_0 + i_13_post ≤ 0 ∧ 1 + i_13_0 − i_13_post ≤ 0 ∧ −1 + i_13_post − i_21_post ≤ 0 ∧ 1 − i_13_post + i_21_post ≤ 0 ∧ −9 + i_21_post ≤ 0 ∧ i_13_0 − i_13_post ≤ 0 ∧ − i_13_0 + i_13_post ≤ 0 ∧ i_21_0 − i_21_post ≤ 0 ∧ − i_21_0 + i_21_post ≤ 0 ∧ − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − i_13_1 + i_13_1 ≤ 0 ∧ i_13_1 − i_13_1 ≤ 0 ∧ − a_20_post + a_20_post ≤ 0 ∧ a_20_post − a_20_post ≤ 0 ∧ − a_20_0 + a_20_0 ≤ 0 ∧ a_20_0 − a_20_0 ≤ 0 | |
5 | 5 | 1: | − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − i_21_post + i_21_post ≤ 0 ∧ i_21_post − i_21_post ≤ 0 ∧ − i_21_0 + i_21_0 ≤ 0 ∧ i_21_0 − i_21_0 ≤ 0 ∧ − i_13_post + i_13_post ≤ 0 ∧ i_13_post − i_13_post ≤ 0 ∧ − i_13_1 + i_13_1 ≤ 0 ∧ i_13_1 − i_13_1 ≤ 0 ∧ − i_13_0 + i_13_0 ≤ 0 ∧ i_13_0 − i_13_0 ≤ 0 ∧ − a_20_post + a_20_post ≤ 0 ∧ a_20_post − a_20_post ≤ 0 ∧ − a_20_0 + a_20_0 ≤ 0 ∧ a_20_0 − a_20_0 ≤ 0 | |
6 | 6 | 0: | − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − i_21_post + i_21_post ≤ 0 ∧ i_21_post − i_21_post ≤ 0 ∧ − i_21_0 + i_21_0 ≤ 0 ∧ i_21_0 − i_21_0 ≤ 0 ∧ − i_13_post + i_13_post ≤ 0 ∧ i_13_post − i_13_post ≤ 0 ∧ − i_13_1 + i_13_1 ≤ 0 ∧ i_13_1 − i_13_1 ≤ 0 ∧ − i_13_0 + i_13_0 ≤ 0 ∧ i_13_0 − i_13_0 ≤ 0 ∧ − a_20_post + a_20_post ≤ 0 ∧ a_20_post − a_20_post ≤ 0 ∧ − a_20_0 + a_20_0 ≤ 0 ∧ a_20_0 − a_20_0 ≤ 0 |
The following invariants are asserted.
0: | TRUE |
1: | TRUE |
4: | 10 − i_13_0 ≤ 0 |
5: | −9 + i_21_post ≤ 0 ∧ −9 + i_21_0 ≤ 0 |
6: | TRUE |
The invariants are proved as follows.
0 | (0) | TRUE | ||
1 | (1) | TRUE | ||
4 | (4) | 10 − i_13_0 ≤ 0 | ||
5 | (5) | −9 + i_21_post ≤ 0 ∧ −9 + i_21_0 ≤ 0 | ||
6 | (6) | TRUE |
0 | 0 1 | |
1 | 3 4 | |
1 | 4 5 | |
5 | 5 1 | |
6 | 6 0 |
1 | 7 | : | − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − i_21_post + i_21_post ≤ 0 ∧ i_21_post − i_21_post ≤ 0 ∧ − i_21_0 + i_21_0 ≤ 0 ∧ i_21_0 − i_21_0 ≤ 0 ∧ − i_13_post + i_13_post ≤ 0 ∧ i_13_post − i_13_post ≤ 0 ∧ − i_13_1 + i_13_1 ≤ 0 ∧ i_13_1 − i_13_1 ≤ 0 ∧ − i_13_0 + i_13_0 ≤ 0 ∧ i_13_0 − i_13_0 ≤ 0 ∧ − a_20_post + a_20_post ≤ 0 ∧ a_20_post − a_20_post ≤ 0 ∧ − a_20_0 + a_20_0 ≤ 0 ∧ a_20_0 − a_20_0 ≤ 0 |
We remove transitions
, , using the following ranking functions, which are bounded by −13.6: | 0 |
0: | 0 |
1: | 0 |
5: | 0 |
4: | 0 |
: | −5 |
: | −6 |
: | −7 |
: | −7 |
: | −7 |
: | −7 |
: | −11 |
8 | lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 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, 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, 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] ] |
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
10 : − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − i_21_post + i_21_post ≤ 0 ∧ i_21_post − i_21_post ≤ 0 ∧ − i_21_0 + i_21_0 ≤ 0 ∧ i_21_0 − i_21_0 ≤ 0 ∧ − i_13_post + i_13_post ≤ 0 ∧ i_13_post − i_13_post ≤ 0 ∧ − i_13_1 + i_13_1 ≤ 0 ∧ i_13_1 − i_13_1 ≤ 0 ∧ − i_13_0 + i_13_0 ≤ 0 ∧ i_13_0 − i_13_0 ≤ 0 ∧ − a_20_post + a_20_post ≤ 0 ∧ a_20_post − a_20_post ≤ 0 ∧ − a_20_0 + a_20_0 ≤ 0 ∧ a_20_0 − a_20_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
8 : − st_14_0 + st_14_0 ≤ 0 ∧ st_14_0 − st_14_0 ≤ 0 ∧ − rt_11_post + rt_11_post ≤ 0 ∧ rt_11_post − rt_11_post ≤ 0 ∧ − rt_11_0 + rt_11_0 ≤ 0 ∧ rt_11_0 − rt_11_0 ≤ 0 ∧ − i_21_post + i_21_post ≤ 0 ∧ i_21_post − i_21_post ≤ 0 ∧ − i_21_0 + i_21_0 ≤ 0 ∧ i_21_0 − i_21_0 ≤ 0 ∧ − i_13_post + i_13_post ≤ 0 ∧ i_13_post − i_13_post ≤ 0 ∧ − i_13_1 + i_13_1 ≤ 0 ∧ i_13_1 − i_13_1 ≤ 0 ∧ − i_13_0 + i_13_0 ≤ 0 ∧ i_13_0 − i_13_0 ≤ 0 ∧ − a_20_post + a_20_post ≤ 0 ∧ a_20_post − a_20_post ≤ 0 ∧ − a_20_0 + a_20_0 ≤ 0 ∧ a_20_0 − a_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 −30.: | −2 − 3⋅i_13_0 |
: | −3⋅i_13_0 |
: | −2 − 3⋅i_13_0 |
: | −1 − 3⋅i_13_0 |
8 | lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0] ] |
10 | lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0] ] |
lexStrict[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 3, 0, 0, 0, 0] ] |
We remove transitions 8, 10 using the following ranking functions, which are bounded by −2.
: | −1 |
: | 1 |
: | −2 |
: | 0 |
8 | 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] ] |
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] ] |
lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] |
We remove transition
using the following ranking functions, which are bounded by −1.: | 0 |
: | 0 |
: | 0 |
: | −1 |
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] ] |
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