Model gonnord1¶
Cited in: [Gonnord_thesis] fig. 4.3 p. 50.
Tag: fixpoint.
Figure¶
Source code¶
model gonnord_thesis_050 {
var x, y;
states p;
transition t2 := {
from := p;
to := p;
guard := x = 0;
action := x' = x + 1, y' = y + 1;
};
transition t1 := {
from := p;
to := p;
guard := x >= 0;
action := x' = x + 1;
};
}
strategy gonnord_thesis_050_s {
Region init := {state = p && x = 0 && y = 0};
}
Expected invariant¶
{ p[v1, v2] : v1 >= 0 and v2 >= 0 and v2 <= v1 and v2 <= 1 }
Results¶
- With Aspic: { p[x, y] : y <= x and y >= 0 and y <= 1 } (0.05s), OK.
- With ISL: { p[x__1, 1] : x__1 >= 2; p[x__1, 0] : x__1 >= 1; p[1, 1]; p[0, 0] } (0.00s), OK.