Model ticket¶
Cited in: [BultanGP97] fig. 3 p. 8.
Tags: fixpoint, parallelism.
Figure¶
Source code¶
model bultan_gerber_pugh_cav97_08 {
var a, b, t, s, pc1, pc2;
states q;
transition e_C2 := {
from := q;
to := q;
guard := pc2 = 3;
action := pc2' = 1, s' = s + 1;
};
transition e_W2 := {
from := q;
to := q;
guard := pc2 = 2 && b <= s;
action := pc2' = 3;
};
transition e_T2 := {
from := q;
to := q;
guard := pc2 = 1;
action := pc2' = 2, b' = t, t' = t + 1;
};
transition e_C1 := {
from := q;
to := q;
guard := pc1 = 3;
action := pc1' = 1, s' = s + 1;
};
transition e_W1 := {
from := q;
to := q;
guard := pc1 = 2 && a <= s;
action := pc1' = 3;
};
transition e_T1 := {
from := q;
to := q;
guard := pc1 = 1;
action := pc1' = 2, a' = t, t' = t + 1;
};
}
strategy bultan_gerber_pugh_cav97_08_s {
Region init := {state = q && t = s && pc1 = 1 && pc2 = 1};
}
Expected invariant¶
{ q[v1, v2, v3, v4, v5, v6] : v6 <= 2 or v6 >= 4; q[v1, v2, v3, v4, v5, 3] : v5 <= 2 or v5 >= 4 }
Results¶
- With Aspic: { q[a, b, t, s, pc1, pc2] : pc2 >= 1 and pc1 >= 1 } (0.09s), failed.
- With ISL: { q[a__1, b__1, t__1, s__1, pc1__1, 3] : s__1 >= b__1 or s__1 >= b__1 or s__1 >= b__1 or (s__1 >= b__1 and pc1__1 >= 1 + 2t__1 - 2s__1 and s__1 >= t__1) or s__1 >= b__1 or s__1 >= b__1 or s__1 >= b__1 or (s__1 >= b__1 and s__1 >= t__1 and pc1__1 >= 1 + 2t__1 - 2s__1); q[a__1, b__1, 1 + b__1, s__1, pc1__1, 2]; q[a__1, b__1, t__1, s__1, 3, pc2__1] : s__1 >= a__1 or s__1 >= a__1 or s__1 >= a__1 or (s__1 >= a__1 and s__1 >= t__1 and pc2__1 >= 1 + 2t__1 - 2s__1) or s__1 >= a__1 or s__1 >= a__1 or s__1 >= a__1 or (s__1 >= a__1 and s__1 >= t__1 and pc2__1 >= 1 + 2t__1 - 2s__1); q[a, b, t, t, 1, 1]; q[a__1, b__1, t__1, s__1, 1, pc2__1]; q[a__1, b__1, t__1, s__1, pc1__1, 1]; q[a__1, b__1, 1 + a__1, s__1, 2, pc2__1] } (0.63s), failed.