ALICe documentation

Model car_simple

«  Model car   ::   Contents   ::   Model counterex1  »

Model car_simple

Cited in: [Gonnord_thesis] fig. 7.5 p. 96, [HalbwachsPR97].

Tag: fixpoint.

Figure

../_images/car_simple.png

Source code

model gonnord_thesis_096a {

  var s, t, d;

  states q;

  transition t2 := {
    from   := q;
    to     := q;
    guard  := true;
    action := s' = 0, t' = t + 1;
  };

  transition t1 := {
    from   := q;
    to     := q;
    guard  := s <= 3;
    action := d' = d + 1, s' = s + 1;
  };

}

strategy gonnord_thesis_096a_s {

  Region init := {state = q && s = 0 && t = 0 && d = 0};

}

Expected invariant

{ q[v1, v2, v3] : v2 >= 0 and v1 >= 0 and v1 <= 4 and v3 >= 0 and v3 <= v1 + 4v2 }

Results

  • With Aspic: { q[s, t, d] : d <= s + 4t and s >= 0 and d >= s and s <= 4 } (0.06s), OK.
  • With ISL: { q[s__1, t__1, d__1] : s__1 <= 4 and t__1 >= 1 and d__1 >= 0 and d__1 >= 1 - t__1; q[s__1, 0, s__1] : s__1 <= 4 and s__1 >= 1; q[0, 0, 0] } (0.01s), failed.

«  Model car   ::   Contents   ::   Model counterex1  »