Figure¶

Source code¶

model halbwachs_aussois10_08 {

  var x, y;

  states k;

  transition t2 := {
    from   := k;
    to     := k;
    guard  := x <= 100;
    action := x' = x + 1, y' = y + 1;
  };

  transition t1 := {
    from   := k;
    to     := k;
    guard  := x <= 100;
    action := x' = x + 2;
  };

}

strategy halbwachs_aussois10_08_s {

  Region init := {state = k && x = 0 && y = 0};

}

Expected invariant¶

{ k[v1, v2] : v2 <= v1 and v2 >= 0 }

Results¶

• With Aspic: { k[x, y] : y <= x and y >= 0 and x <= 102 and y <= 202 - x } (0.05s), OK.
• With ISL: { k[x__1, y__1] : exists (e0 = [(-x__1 + y__1)/2]: 2e0 = -x__1 + y__1 and x__1 <= 102 and y__1 <= 100 and y__1 >= 1 and y__1 <= -2 + x__1); k[x__1, x__1] : x__1 >= 1 and x__1 <= 101; k[x__1, 0] : exists (e0 = [(x__1)/2]: 2e0 = x__1 and x__1 >= 2 and x__1 <= 102); k[0, 0] } (0.00s), OK.