ALICe documentation

Model metro

«  Model maccarthy91   ::   Contents   ::   Model microsoftex2  »

Model metro

Also known as: train subway

Cited in: [Halbwachs93] fig. 9 p. 12, [HalbwachsPR97] fig. 8 p. 15.

Tag: fixpoint.

Figure

../_images/metro.png

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.

«  Model maccarthy91   ::   Contents   ::   Model microsoftex2  »