Model metro¶
Also known as: train subway
Cited in: [Halbwachs93] fig. 9 p. 12, [HalbwachsPR97] fig. 8 p. 15.
Tag: fixpoint.
Figure¶
Source code¶
model halbwachs_cav93_9 {
var s, b, d;
states T, B, S, L;
transition t6 := {
from := T;
to := B;
guard := b - s = 9;
action := b' = b + 1, d' = 0;
};
transition t3 := {
from := T;
to := L;
guard := b - s = -9;
action := s' = s + 1;
};
transition t2 := {
from := T;
to := T;
guard := b - s > -9;
action := s' = s + 1;
};
transition t1 := {
from := T;
to := T;
guard := b - s < 9;
action := b' = b + 1;
};
transition t10 := {
from := B;
to := S;
guard := d <= 9;
action := b' = b + 1;
};
transition t7 := {
from := B;
to := T;
guard := b - s = 1;
action := s' = s + 1;
};
transition t9 := {
from := B;
to := B;
guard := b - s > 1;
action := s' = s + 1;
};
transition t8 := {
from := B;
to := B;
guard := d < 9;
action := b' = b + 1, d' = d + 1;
};
transition t12 := {
from := S;
to := T;
guard := b - s = 1;
action := s' = s + 1;
};
transition t11 := {
from := S;
to := S;
guard := b - s > 1;
action := s' = s + 1;
};
transition t4 := {
from := L;
to := T;
guard := b - s = -1;
action := b' = b + 1;
};
transition t5 := {
from := L;
to := L;
guard := b - s < -1;
action := b' = b + 1;
};
}
strategy halbwachs_cav93_9_s {
Region init := {state = T && s = 0 && b = 0 && d = 0};
}
Expected invariant¶
{ S[v1, v2, v3] : v2 >= -10 + v1 and v2 <= 20 + v1; L[v1, v2, v3] : v2 >= -10 + v1 and v2 <= 20 + v1; B[v1, v2, v3] : v2 >= -10 + v1 and v2 <= 20 + v1; T[v1, v2, v3] : v2 >= -10 + v1 and v2 <= 20 + v1 }
Results¶
- With Aspic: { L[s, b, d] : b >= -10 + s and d <= 9 and d >= 0 and b <= -1 + s and 2d <= -10 + s; B[s, b, d] : d >= -10 - s + b and d <= -10 + b and d >= 0 and d <= 9 and b >= 1 + s; S[s, b, d] : d >= -11 - s + b and d <= 9 and b >= 1 + s and d >= 0 and d <= -11 + b; T[s, b, d] : b >= -9 + s and d >= 0 and 2d <= b and b <= 9 + s and 2d <= s and d <= 9 } (0.06s), OK.
- With ISL: timeout.