Model slam_bad¶
Cited in: [GulavaniHKNR06] fig. 1 p. 3.
Tag: termination.
Figure¶
Source code¶
model gulavani_henzinger_kannan_nori_rajamani_sigsoft06_03 {
var i, c;
states q;
transition t := {
from := q;
to := q;
guard := i < 1000;
action := c' = c + i, i' = i + 1;
};
}
strategy gulavani_henzinger_kannan_nori_rajamani_sigsoft06_03_s {
Region init := {state = q && i = 0 && c = 0};
}
Expected invariant¶
{ q[v1, v2] : v1 <= 1000 }
Results¶
- With Aspic: { q[i, c] : i <= 1000 } (0.22s), OK.
- With ISL: { q[i__1, c__1] : i__1 >= 1 and i__1 <= 1000 and c__1 <= 999i__1; q[0, 0] } (0.01s), OK.