Model halbwachs7¶
Cited in: [Halbwachs_misc10] p. 43.
Tag: fixpoint.
Figure¶
Source code¶
model halbwachs_aussois10_43 {
var t, s, d;
states k;
transition t2 := {
from := k;
to := k;
guard := true;
action := t' = t + 1, s' = 0;
};
transition t1 := {
from := k;
to := k;
guard := s <= 3;
action := s' = s + 1, d' = d + 1;
};
}
strategy halbwachs_aussois10_43_s {
Region init := {state = k && t = 0 && s = 0 && d = 0};
}
Expected invariant¶
{ k[v1, v2, v3] : v1 >= 0 and v2 >= 0 and v2 <= 4 and v3 >= 0 and v3 <= 4v1 + v2 }
Results¶
- With Aspic: { k[t, s, d] : d <= 4t + s and s >= 0 and d >= s and s <= 4 } (0.05s), OK.
- With ISL: { k[t__1, s__1, d__1] : s__1 <= 4 and t__1 >= 1 and d__1 >= 0 and d__1 >= 1 - t__1; k[0, s__1, s__1] : s__1 <= 4 and s__1 >= 1; k[0, 0, 0] } (0.00s), failed.