Figure¶

Source code¶

model gonnord_thesis_053 {

  var d, v, t;

  states P, P_toofast, P_wall, P_stop;

  transition t5 := {
    from   := P;
    to     := P_toofast;
    guard  := v >= 3;
    action := ;
  };

  transition t4 := {
    from   := P;
    to     := P_wall;
    guard  := d >= 10;
    action := ;
  };

  transition t3 := {
    from   := P;
    to     := P_stop;
    guard  := t >= 3;
    action := ;
  };

  transition t2 := {
    from   := P;
    to     := P;
    guard  := v <= 1 && d <= 8;
    action := v' = v + 1, d' = d + 1;
  };

  transition t1 := {
    from   := P;
    to     := P;
    guard  := t <= 2;
    action := v' = 0, t' = t + 1;
  };

}

strategy gonnord_thesis_053_s {

  Region init := {state = P && d = 0 && v = 0 && t = 0};

}

Expected invariant¶

{  }

Results¶

• With Aspic: { P[d, v, t] : v <= d and v >= 0 and t <= 3 and v <= 2 and 2t >= d - v; P_stop[d, v, 3] : v <= d and v >= 0 and v >= -6 + d and v <= 2 } (0.05s), OK.
• With ISL: { P[d__1, v__1, t__1] : (d__1 >= 0 and t__1 >= 1 - d__1 and v__1 <= 2 and d__1 <= 9 and t__1 >= 1) or (t__1 >= 1 - d__1 and v__1 <= 2 and d__1 <= 9 and t__1 >= 1 and d__1 >= 0); P[d__1, d__1, 0] : (d__1 <= 2 and d__1 >= 1) or (d__1 >= 1 and d__1 <= 2); P[d__1, 0, t__1] : (d__1 >= 0 and t__1 >= 1 - d__1 and t__1 <= 3 and t__1 >= 1) or (t__1 >= 1 - d__1 and t__1 <= 3 and t__1 >= 1 and d__1 >= 0); P[0, 0, 0]; P_wall[d__1, 0, t__1] : (t__1 >= 1 - d__1 and d__1 >= 10 and t__1 <= 3 and t__1 >= 1) or (t__1 >= 1 - d__1 and t__1 <= 3 and t__1 >= 1 and d__1 >= 10); P_stop[d__1, v__1, t__1] : (d__1 >= 0 and t__1 >= 3 and v__1 <= 2 and d__1 <= 9 and t__1 >= 1 - d__1) or (t__1 >= 1 - d__1 and v__1 <= 2 and d__1 <= 9 and t__1 >= 3 and d__1 >= 0); P_stop[d__1, 0, 3] : d__1 >= 0 or d__1 >= 0 } (0.02s), failed.