Figure¶

Source code¶

model main {

  var a, mx, x;

  states start, lbl_10_1, stop;

  transition t_31 := {
    from   := start;
    to     := lbl_10_1;
    guard  := 1 <= mx;
    action := a' = -1, x' = 2;
  };

  transition t_30 := {
    from   := start;
    to     := lbl_10_1;
    guard  := 1 <= mx;
    action := a' = 1, x' = 2;
  };

  transition t_22 := {
    from   := start;
    to     := stop;
    guard  := mx <= 0;
    action := ;
  };

  transition t_26 := {
    from   := lbl_10_1;
    to     := stop;
    guard  := mx + 1 <= x;
    action := ;
  };

  transition t_28 := {
    from   := lbl_10_1;
    to     := lbl_10_1;
    guard  := x <= mx;
    action := a' = a - 1, x' = x + 1;
  };

  transition t_27 := {
    from   := lbl_10_1;
    to     := lbl_10_1;
    guard  := x <= mx;
    action := a' = a + 1, x' = x + 1;
  };

}

strategy main_s {

  Region init := {state = start};

}

Expected invariant¶

{ lbl_10_1[v1, v2, v3] : v3 >= 1 - v1 and v3 <= 1 + v2 and v3 >= 2 and v3 >= 1 + v1 }

Results¶

• With Aspic: { start[a, mx, x]; lbl_10_1[a, mx, x] : x >= 1 - a and x <= 1 + mx and x >= 2 and x >= 1 + a; stop[a, mx, x] } (0.05s), OK.
• With ISL: { lbl_10_1[a__1, mx__1, x__1] : (exists (e0 = [(-1 - a__1 + x__1)/2]: 2e0 = -1 - a__1 + x__1 and mx__1 >= 2 and x__1 >= 5 - a__1 and x__1 <= -1 - a__1 + 2mx__1 and x__1 >= 3 + a__1 and x__1 <= 1 + mx__1)) or (exists (e0 = [(-1 - a__1 + x__1)/2]: 2e0 = -1 - a__1 + x__1 and mx__1 >= 2 and x__1 >= 3 - a__1 and x__1 <= -3 - a__1 + 2mx__1 and x__1 >= 5 + a__1 and x__1 <= 1 + mx__1)); lbl_10_1[-1, mx__1, 2] : mx__1 >= 1; lbl_10_1[a__1, mx__1, 3 + a__1] : mx__1 >= 2 and a__1 >= 0 and mx__1 >= 2 + a__1; lbl_10_1[a__1, mx__1, 3 - a__1] : mx__1 >= 2 and a__1 <= 0 and mx__1 >= 2 - a__1; lbl_10_1[a__1, mx__1, 1 + a__1] : mx__1 >= 2 and a__1 >= 2 and mx__1 >= a__1; lbl_10_1[a__1, mx__1, 1 - a__1] : mx__1 >= 2 and a__1 <= -2 and mx__1 >= -a__1; lbl_10_1[1, mx__1, 2] : mx__1 >= 1; start[a, mx, x]; stop[a__1, mx__1, x__1] : mx__1 <= 0; stop[a__1, mx__1, 1 + mx__1] : (exists (e0 = [(-a__1 + mx__1)/2]: 2e0 = -a__1 + mx__1 and mx__1 >= 2 and mx__1 >= 4 - a__1 and mx__1 >= 2 + a__1)) or (exists (e0 = [(-a__1 + mx__1)/2]: 2e0 = -a__1 + mx__1 and mx__1 >= 2 and mx__1 >= 2 - a__1 and mx__1 >= 4 + a__1)); stop[-1, 1, 2]; stop[a__1, 2 + a__1, 3 + a__1] : a__1 >= 0; stop[a__1, 2 - a__1, 3 - a__1] : a__1 <= 0; stop[a__1, a__1, 1 + a__1] : a__1 >= 2; stop[a__1, -a__1, 1 - a__1] : a__1 <= -2; stop[1, 1, 2] } (0.00s), OK.