Model wcet2¶
Cited in: [AliasDFG10].
Tag: complexity.
Figure¶
Source code¶
model main {
var i, j, tmp, tmp_1;
states start, lbl_8_2, lbl_9_2, stop;
transition t_22 := {
from := start;
to := lbl_8_2;
guard := i <= 4 && 3 <= i;
action := j' = 1, tmp_1' = 0;
};
transition t_21 := {
from := start;
to := lbl_9_2;
guard := i <= 2;
action := i' = i + 1, j' = 0, tmp' = i;
};
transition t_15 := {
from := start;
to := stop;
guard := 5 <= i;
action := ;
};
transition t_17 := {
from := lbl_8_2;
to := lbl_9_2;
guard := i <= 2 || 10 <= j;
action := i' = i + 1, tmp' = i;
};
transition t_18 := {
from := lbl_8_2;
to := lbl_8_2;
guard := 3 <= i && j <= 9;
action := j' = j + 1, tmp_1' = j;
};
transition t_20 := {
from := lbl_9_2;
to := lbl_8_2;
guard := i <= 4 && 3 <= i;
action := j' = 1, tmp_1' = 0;
};
transition t_13 := {
from := lbl_9_2;
to := stop;
guard := 5 <= i;
action := ;
};
transition t_19 := {
from := lbl_9_2;
to := lbl_9_2;
guard := i <= 2;
action := i' = i + 1, j' = 0, tmp' = i;
};
}
strategy main_s {
Region init := {state = start};
}
Expected invariant¶
{ lbl_9_2[v1, v2, -1 + v1, v4] : v2 <= 10 and v2 >= -15 + 5v1 and v2 >= 0; stop[v1, v2, v3, v4] : v1 >= 5; lbl_8_2[v1, v2, v3, -1 + v2] : v1 >= 3 and v2 >= 1 and v1 <= 4 and v2 <= 10 }
Results¶
- With Aspic: { start[i, j, tmp, tmp_1]; lbl_9_2[i, j, -1 + i, tmp_1] : j >= 0 and j <= 10 and j >= -15 + 5i; lbl_8_2[i, j, tmp, -1 + j] : i <= 4 and j <= 10 and i >= 3 and j >= 1; stop[i, j, tmp, tmp_1] : i >= 5 } (0.25s), OK.
- With ISL: { lbl_9_2[i__1, 0, -1 + i__1, tmp_1__1] : i__1 <= 3 or i__1 <= 3; lbl_9_2[5, 10, 4, 9]; lbl_9_2[i__1, 10, -1 + i__1, 9] : (i__1 <= 5 and i__1 >= 4) or (i__1 >= 4 and i__1 <= 5) or (i__1 <= 5 and i__1 >= 4); stop[i__1, j__1, tmp__1, tmp_1__1] : i__1 >= 5; stop[5, 10, 4, 9]; start[i, j, tmp, tmp_1]; lbl_8_2[i__1, j__1, tmp__1, -1 + j__1] : i__1 <= 4 and i__1 >= 3 and j__1 >= 2 and j__1 <= 10; lbl_8_2[i__1, 1, tmp__1, 0] : i__1 <= 4 and i__1 >= 3; lbl_8_2[4, j__1, 3, -1 + j__1] : (j__1 >= 1 and j__1 <= 10) or (j__1 >= 1 and j__1 <= 10); lbl_8_2[3, j__1, 2, -1 + j__1] : (j__1 <= 10 and j__1 >= 1) or (j__1 <= 10 and j__1 >= 1) } (0.18s), OK.