Model gonnord4¶
Cited in: [Gonnord_thesis] fig. 7.3 p. 93.
Tag: fixpoint.
Figure¶
Source code¶
model gonnord_thesis_093a {
var x, z;
states q;
transition t2 := {
from := q;
to := q;
guard := z = 10;
action := z' = 0;
};
transition t1 := {
from := q;
to := q;
guard := z <= 9;
action := x' = x + 1, z' = z + 1;
};
}
strategy gonnord_thesis_093a_s {
Region init := {state = q && x = 0 && z = 0};
}
Expected invariant¶
{ q[v1, v2] : v2 <= v1 and v2 <= 10 and v2 >= 0 }
Results¶
- With Aspic: { q[x, z] : z <= 10 and z <= x and z >= 0 } (0.04s), OK.
- With ISL: { q[x__1, z__1] : exists (e0 = [(-x__1 + z__1)/10]: 10e0 = -x__1 + z__1 and z__1 <= -10 + 11x__1 and z__1 <= 10 and z__1 <= x__1 and x__1 >= 0); q[0, 0] } (0.00s), failed.