Figure¶

Source code¶

model halbwachs_aussois10_40 {

  var v, t, x, d;

  states k;

  transition t3 := {
    from   := k;
    to     := k;
    guard  := d = 10 && x >= 2;
    action := x' = 0, d' = 0;
  };

  transition t2 := {
    from   := k;
    to     := k;
    guard  := d <= 9;
    action := d' = d + 1, t' = t + 1;
  };

  transition t1 := {
    from   := k;
    to     := k;
    guard  := x <= 4;
    action := x' = x + 1, v' = v + 1;
  };

}

strategy halbwachs_aussois10_40_s {

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

}

Expected invariant¶

{ k[v1, v2, v3, v4] : v1 >= 0 and v2 >= 0 and v2 >= -10 + 2v1 and v2 <= 10 + 5v1 }

Results¶

• With Aspic: { k[v, t, x, d] : x <= 5 and x <= v and d <= t and x >= 0 and d >= 0 and d <= 10 } (0.05s), failed.
• With ISL: { k[v__1, t__1, x__1, d__1] : (exists (e0 = [(-t__1 + d__1)/10]: 10e0 = -t__1 + d__1 and d__1 <= -10 + 10v__1 + 11t__1 and d__1 <= 10 and d__1 >= -5v__1 + t__1 + 5x__1 and d__1 <= -10 + t__1 and t__1 >= 0 and v__1 >= 0)) or (exists (e0 = [(-t__1 + d__1)/10]: 10e0 = -t__1 + d__1 and d__1 <= -10 + 10v__1 + 11t__1 and x__1 <= 5 and d__1 >= -5v__1 + t__1 + 5x__1 and d__1 <= -10 + t__1 and t__1 >= 0 and v__1 >= 0)) or (exists (e0 = [(-t__1 + d__1)/10]: 10e0 = -t__1 + d__1 and d__1 <= -10 + 10v__1 + 11t__1 and d__1 <= 10 and d__1 >= -5v__1 + t__1 + 5x__1 and d__1 <= -10 + t__1 and t__1 >= 0 and v__1 >= 0)) or (exists (e0 = [(-t__1 + d__1)/10]: 10e0 = -t__1 + d__1 and d__1 <= -10 + 10v__1 + 11t__1 and x__1 <= 5 and d__1 >= -5v__1 + t__1 + 5x__1 and d__1 <= -10 + t__1 and t__1 >= 0 and v__1 >= 0)); k[0, 0, 0, 0]; k[v__1, t__1, v__1, t__1] : (t__1 >= 1 - v__1 and t__1 <= 10 and t__1 >= 0 and v__1 >= 0) or (t__1 >= 1 - v__1 and v__1 <= 5 and t__1 >= 0 and v__1 >= 0) or (t__1 >= 1 - v__1 and t__1 <= 10 and t__1 >= 0 and v__1 >= 0) or (t__1 >= 1 - v__1 and v__1 <= 5 and t__1 >= 0 and v__1 >= 0) } (0.02s), failed.