Figure¶

Source code¶

model main {

  var x, y1, y2, y3;

  states start, lbl_11_1, lbl_8_2, lbl_16, stop;

  transition t_47 := {
    from   := start;
    to     := lbl_11_1;
    guard  := 2 <= x;
    action := y1' = x - 1, y2' = 1, y3' = x;
  };

  transition t_33 := {
    from   := start;
    to     := stop;
    guard  := x <= 1;
    action := ;
  };

  transition t_43 := {
    from   := lbl_11_1;
    to     := lbl_8_2;
    guard  := 1 <= y1 && 0 = y2;
    action := y1' = y1 - 1, y2' = x, y3' = y3 - y1;
  };

  transition t_42 := {
    from   := lbl_11_1;
    to     := lbl_8_2;
    guard  := y2 + 1 <= y1 && y2 + 1 <= 0 || y2 + 1 <= y1 && 1 <= y2;
    action := y1' = y1 - 1, y2' = x;
  };

  transition t_41 := {
    from   := lbl_11_1;
    to     := lbl_11_1;
    guard  := y1 <= y2;
    action := y2' = y2 - y1;
  };

  transition t_44 := {
    from   := lbl_8_2;
    to     := lbl_11_1;
    guard  := y1 <= y2 && 1 <= y1;
    action := y2' = y2 - y1;
  };

  transition t_37 := {
    from   := lbl_8_2;
    to     := lbl_16;
    guard  := y1 <= 0;
    action := ;
  };

  transition t_46 := {
    from   := lbl_8_2;
    to     := lbl_8_2;
    guard  := 1 <= y1 && 0 = y2;
    action := y1' = y1 - 1, y2' = x, y3' = y3 - y1;
  };

  transition t_45 := {
    from   := lbl_8_2;
    to     := lbl_8_2;
    guard  := y2 + 1 <= y1 && 1 <= y2 || 1 <= y1 && y2 + 1 <= 0;
    action := y1' = y1 - 1, y2' = x;
  };

  transition t := {
    from   := lbl_16;
    to     := stop;
    guard  := true;
    action := ;
  };

}

strategy main_s {

  Region init := {state = start};

}

Expected invariant¶

{ lbl_16[v1, 0, v1, v4] : v4 <= -1 + v1 and v1 >= 2; lbl_11_1[v1, v2, v3, v4] : v3 >= 0 and v2 >= 1 and v3 <= v1 - v2 and v2 <= -1 + v1 and v4 <= v1; lbl_8_2[v1, v2, v1, v4] : v4 <= v1 and v4 <= -1 + v1 + v2 and v2 >= 0 and v2 <= -2 + v1 }

Results¶

• With Aspic: { start[x, y1, y2, y3]; lbl_8_2[x, y1, x, y3] : y1 >= 0 and y1 <= -2 + x and y3 <= x and y3 <= -1 + x + y1; lbl_11_1[x, y1, y2, y3] : y2 >= 0 and y1 >= 1 and y2 <= x - y1 and y1 <= -1 + x and y3 <= x; lbl_16[x, 0, x, y3] : y3 <= -1 + x and x >= 2; stop[x, y1, y2, y3] } (0.04s), OK.
• With ISL: { stop[x__1, y1__1, y2__1, y3__1] : x__1 <= 1; stop[x__1, 0, x__1, y3__1] : x__1 >= 3 and y3__1 <= -9 + 3x__1 and y3__1 <= -1 + x__1; stop[x__1, 0, x__1, -1 + x__1] : x__1 >= 3; stop[2, 0, 2, 1]; lbl_16[x__1, 0, x__1, y3__1] : x__1 >= 3 and y3__1 <= -9 + 3x__1 and y3__1 <= -1 + x__1; lbl_16[x__1, 0, x__1, -1 + x__1] : x__1 >= 3; lbl_16[2, 0, 2, 1]; lbl_11_1[x__1, y1__1, y2__1, y3__1] : (x__1 >= 3 and y2__1 >= 1 and y2__1 <= -2 + x__1 - y1__1 and y3__1 <= y1__1) or (x__1 >= 3 and y1__1 <= -2 + x__1 and y3__1 <= -6 + 3x__1 - 2y1__1 and y3__1 <= x__1 and y2__1 >= 0) or (x__1 >= 3 and y1__1 <= -2 + x__1 and y2__1 >= 1 and y3__1 <= 2 - x__1 + 2y1__1) or (x__1 >= 3 and y2__1 <= -3 + x__1 - y1__1 and y3__1 <= x__1 and y1__1 <= -3 + x__1 and y2__1 >= 0); lbl_11_1[x__1, y1__1, y2__1, x__1] : x__1 >= 3 and y1__1 <= -1 + x__1 and y2__1 >= 0; lbl_11_1[2, y1__1, y2__1, 2] : y2__1 >= 0 and y1__1 <= 1; lbl_11_1[x__1, -1 + x__1, 1, x__1] : x__1 >= 2; lbl_11_1[2, y1__1, y2__1, y3__1] : (y2__1 <= -y1__1 and y3__1 <= y1__1 and y2__1 >= 1) or (y3__1 <= -2y1__1 and y1__1 <= 0 and y2__1 >= 0 and y3__1 <= 2) or (y3__1 <= 2y1__1 and y1__1 <= 0 and y2__1 >= 1) or (y3__1 <= 2 and y2__1 <= -1 - y1__1 and y2__1 >= 0 and y1__1 <= -1); start[x, y1, y2, y3]; lbl_8_2[x__1, y1__1, x__1, y3__1] : x__1 >= 3 and y1__1 <= -3 + x__1 and y3__1 <= -1 + x__1 + y1__1 and y3__1 <= x__1 and y1__1 >= 0 and y3__1 <= -8 + 3x__1 - 2y1__1 and y3__1 <= -9 + 3x__1 - y1__1; lbl_8_2[x__1, y1__1, x__1, x__1] : x__1 >= 3 and y1__1 >= 1 and y1__1 <= -2 + x__1; lbl_8_2[x__1, y1__1, x__1, -1 + x__1 - y1__1] : x__1 >= 3 and y1__1 <= -2 + x__1 and y1__1 >= 0; lbl_8_2[x__1, -2 + x__1, x__1, x__1] : x__1 >= 3; lbl_8_2[2, 0, 2, 1] } (3.86s), failed.