Model gonnord6¶
Cited in: [Gonnord_thesis] fig. 7.6 p. 96.
Tag: fixpoint.
Figure¶
Source code¶
model gonnord_thesis_096b {
var x, y, z;
states q;
transition t2 := {
from := q;
to := q;
guard := true;
action := z' = 0;
};
transition t1 := {
from := q;
to := q;
guard := x >= 2 * z;
action := x' = x + 1, y' = y + 1, z' = z + 1;
};
}
strategy gonnord_thesis_096b_s {
Region init := {state = q && x = 0 && y = 0 && z = 0};
}
Expected invariant¶
{ q[v1, v2, v3] : v1 >= 0 and v2 >= 0 and v3 >= 0 and v3 <= v1 and v2 >= v1 }
Results¶
- With Aspic: { q[x, x, z] : 2z <= 1 + x and z <= x and z >= 0 } (0.05s), OK.
- With ISL: { q[x__1, x__1, z__1] : 2z__1 <= 1 + x__1 and x__1 >= 0; q[x__1, x__1, 0] : x__1 >= 0; q[1, 1, 1]; q[0, 0, 0] } (0.01s), failed.