Model nd_loop¶
Cited in: [AliasDFG10].
Tag: fixpoint.
Figure¶
Source code¶
model nd_loop {
var x, y;
states start, lbl_5_1, stop, cut;
transition t_22 := {
from := start;
to := lbl_5_1;
guard := true;
action := x' = ?, y' = 0;
};
transition t_20 := {
from := lbl_5_1;
to := stop;
guard := x <= y + 2 && y + 1 <= x && 10 <= x;
action := ;
};
transition t_19 := {
from := lbl_5_1;
to := cut;
guard := x <= y + 2 && x <= 9 && y + 1 <= x;
action := ;
};
transition t_18 := {
from := lbl_5_1;
to := stop;
guard := x <= y || y + 3 <= x;
action := ;
};
transition t_21 := {
from := cut;
to := lbl_5_1;
guard := true;
action := x' = ?, y' = x;
};
}
strategy nd_loop_s {
Region init := {state = start};
}
Expected invariant¶
{ lbl_5_1[v1, v2] : v2 >= 0; cut[v1, v2] : v2 >= -2 + v1 and v2 >= 0 and v1 <= 9 and v2 <= -1 + v1; stop[v1, v2] : v2 >= 0 }
Results¶
- With Aspic: { stop[x, y] : y >= 0; lbl_5_1[x, y] : y >= 0; start[x, y]; cut[x, y] : y >= -2 + x and y >= 0 and x <= 9 and y <= -1 + x } (0.04s), OK.
- With ISL: { lbl_5_1[x__1, y__1] : y__1 >= 1 and y__1 <= 9; lbl_5_1[x__1, 0]; cut[x__1, y__1] : y__1 >= -2 + x__1 and x__1 <= 9 and y__1 >= 1 and y__1 <= -1 + x__1; cut[x__1, 0] : x__1 <= 2 and x__1 >= 1; stop[x__1, y__1] : (y__1 >= 1 and y__1 <= 9 and y__1 <= -3 + x__1) or (y__1 >= 1 and y__1 <= 9 and y__1 >= x__1) or (y__1 >= 1 and y__1 <= 9 and y__1 >= -2 + x__1 and y__1 <= -1 + x__1 and x__1 >= 10); stop[x__1, 0] : x__1 >= 3 or x__1 <= 0; start[x, y] } (0.00s), OK.