Model jeannet5¶
Cited in: [Jeannet_thesis] fig. 8.4 p. 109.
Tag: fixpoint.
Figure¶
Source code¶
model jeannet_thesis_109 {
var x, y, e;
states i, b, a;
transition t2 := {
from := i;
to := b;
guard := e = 0;
action := ;
};
transition t1 := {
from := i;
to := a;
guard := e = 1;
action := ;
};
transition t6 := {
from := b;
to := a;
guard := true;
action := x' = x + 1, y' = y + 2;
};
transition t5 := {
from := a;
to := b;
guard := e = 0;
action := ;
};
transition t4 := {
from := a;
to := a;
guard := e = 1;
action := x' = x + 1, y' = y + 1;
};
transition t3 := {
from := a;
to := a;
guard := e = 1;
action := x' = x + 1;
};
}
strategy jeannet_thesis_109_s {
Region init := {state = i && x = 0 && y = 0 && 0 <= e && e <= 1};
}
Expected invariant¶
{ b[v1, 2v1, v3] }
Results¶
- With Aspic: { b[x, y, 0] : y >= 0; a[x, y, e] : e <= 1 and e >= 0 and 2e >= 2 - y; i[0, 0, e] : e >= 0 and e <= 1 } (0.06s), failed.
- With ISL: { i[0, 0, e] : e >= 0 and e <= 1; b[x__1, 2x__1, 0] : x__1 >= 1; b[0, 0, 0]; a[x__1, y__1, 1] : y__1 <= x__1 and x__1 >= 1 and y__1 >= 0; a[x__1, 2x__1, 0] : x__1 >= 2; a[0, 0, 1]; a[1, 2, 0] } (0.01s), OK.