Figure¶

Source code¶

model main {

  var n, tmp, x, y;

  states start, lbl_7_2, cut, lbl_4_2, stop;

  transition t_28 := {
    from   := start;
    to     := lbl_7_2;
    guard  := y <= n && 0 <= x;
    action := tmp' = y, x' = x - 1, y' = y + 1;
  };

  transition t_27 := {
    from   := start;
    to     := cut;
    guard  := 0 <= x;
    action := x' = x - 1;
  };

  transition t_19 := {
    from   := start;
    to     := lbl_4_2;
    guard  := 0 <= x && 0 <= y;
    action := y' = y - 1;
  };

  transition t_17 := {
    from   := start;
    to     := stop;
    guard  := x + 1 <= 0;
    action := ;
  };

  transition t_23 := {
    from   := lbl_7_2;
    to     := cut;
    guard  := true;
    action := ;
  };

  transition t_24 := {
    from   := lbl_7_2;
    to     := lbl_7_2;
    guard  := y <= n;
    action := tmp' = y, y' = y + 1;
  };

  transition t_30 := {
    from   := cut;
    to     := lbl_7_2;
    guard  := y <= n && 0 <= x;
    action := tmp' = y, x' = x - 1, y' = y + 1;
  };

  transition t_22 := {
    from   := cut;
    to     := lbl_4_2;
    guard  := 0 <= x && 0 <= y;
    action := y' = y - 1;
  };

  transition t_20 := {
    from   := cut;
    to     := stop;
    guard  := x + 1 <= 0;
    action := ;
  };

  transition t_29 := {
    from   := cut;
    to     := cut;
    guard  := 0 <= x;
    action := x' = x - 1;
  };

  transition t_26 := {
    from   := lbl_4_2;
    to     := lbl_7_2;
    guard  := y <= n;
    action := tmp' = y, x' = x - 1, y' = y + 1;
  };

  transition t_25 := {
    from   := lbl_4_2;
    to     := cut;
    guard  := true;
    action := x' = x - 1;
  };

  transition t_14 := {
    from   := lbl_4_2;
    to     := lbl_4_2;
    guard  := 0 <= y;
    action := y' = y - 1;
  };

}

strategy main_s {

  Region init := {state = start};

}

Expected invariant¶

{ stop[v1, v2, v3, v4] : v3 <= -1; lbl_4_2[v1, v2, v3, v4] : v3 >= 0 and v4 >= -1; lbl_7_2[v1, v2, v3, 1 + v2] : v2 <= v1 and v3 >= -1; cut[v1, v2, v3, v4] : v3 >= -1 }

Results¶

• With Aspic: { lbl_7_2[n, tmp, x, 1 + tmp] : tmp <= n and x >= -1; start[n, tmp, x, y]; cut[n, tmp, x, y] : x >= -1; lbl_4_2[n, tmp, x, y] : x >= 0 and y >= -1; stop[n, tmp, x, y] : x <= -1 } (0.05s), OK.
• With ISL: { stop[n__1, tmp__1, x__1, y__1] : x__1 <= -1; stop[n__1, tmp__1, x__1, 1 + tmp__1] : (x__1 <= -1 and tmp__1 <= n__1) or (x__1 <= -1 and tmp__1 <= n__1) or (x__1 <= -1 and tmp__1 <= n__1 and n__1 >= -1) or (tmp__1 <= n__1 and x__1 <= -1 and n__1 >= 0) or (tmp__1 >= 0 and x__1 <= -1 and tmp__1 <= n__1) or (n__1 >= -1 and x__1 <= -1 and tmp__1 <= n__1) or (tmp__1 <= n__1 and x__1 <= -1 and tmp__1 >= 0) or (tmp__1 <= n__1 and x__1 <= -1 and n__1 >= 0) or (x__1 <= -1 and tmp__1 <= n__1 and tmp__1 >= 0) or (x__1 <= -1 and tmp__1 <= n__1) or (tmp__1 <= n__1 and x__1 <= -1 and n__1 >= -1) or (x__1 <= -1 and tmp__1 <= n__1); stop[n__1, tmp__1, -1, 1 + tmp__1] : tmp__1 <= n__1 or tmp__1 <= n__1 or (tmp__1 <= n__1 and tmp__1 >= -1) or (tmp__1 <= n__1 and tmp__1 >= -1) or (tmp__1 <= n__1 and tmp__1 >= -1) or tmp__1 <= n__1 or (tmp__1 <= n__1 and tmp__1 >= -1); stop[n__1, tmp__1, -1, y__1]; lbl_4_2[n__1, tmp__1, x__1, y__1] : (x__1 >= 0 and y__1 >= -1) or (tmp__1 <= n__1 and y__1 <= tmp__1 and y__1 >= -1 and x__1 >= 0) or (x__1 >= 0 and y__1 <= tmp__1 and y__1 >= -1 and tmp__1 <= n__1) or (y__1 >= -1 and y__1 <= tmp__1 and x__1 >= 0 and tmp__1 <= n__1) or (y__1 >= -1 and tmp__1 <= n__1 and y__1 <= tmp__1 and x__1 >= 0) or (y__1 <= tmp__1 and tmp__1 <= n__1 and y__1 >= -1 and x__1 >= 0) or (x__1 >= 0 and y__1 >= -1) or (y__1 >= -1 and x__1 >= 0) or (y__1 >= -1 and tmp__1 <= n__1 and x__1 >= 0 and y__1 <= tmp__1) or (y__1 <= tmp__1 and y__1 >= -1 and x__1 >= 0 and tmp__1 <= n__1) or (tmp__1 <= n__1 and y__1 <= tmp__1 and x__1 >= 0 and y__1 >= -1) or (x__1 >= 0 and y__1 >= -1) or (x__1 >= 0 and y__1 >= -1 and y__1 <= tmp__1 and tmp__1 <= n__1) or (tmp__1 <= n__1 and y__1 <= tmp__1 and x__1 >= 0 and y__1 >= -1) or (y__1 <= tmp__1 and y__1 >= -1 and tmp__1 <= n__1 and x__1 >= 0); lbl_7_2[n__1, tmp__1, x__1, 1 + tmp__1] : (tmp__1 <= n__1 and x__1 >= -1) or tmp__1 <= n__1 or tmp__1 <= n__1 or (tmp__1 <= n__1 and n__1 >= -1) or (tmp__1 >= 0 and tmp__1 <= n__1) or (x__1 >= -1 and tmp__1 >= -1 and tmp__1 <= n__1) or (x__1 >= -1 and tmp__1 >= -1 and tmp__1 <= n__1) or (x__1 >= -1 and tmp__1 >= -1 and tmp__1 <= n__1) or (tmp__1 >= 0 and tmp__1 <= n__1) or (n__1 >= 0 and tmp__1 <= n__1) or (tmp__1 >= 0 and tmp__1 <= n__1) or (tmp__1 <= n__1 and n__1 >= 0) or (tmp__1 <= n__1 and n__1 >= -1) or (x__1 >= -1 and tmp__1 <= n__1) or (tmp__1 <= n__1 and tmp__1 >= -1 and x__1 >= -1) or tmp__1 <= n__1 or tmp__1 <= n__1 or (tmp__1 <= n__1 and n__1 >= -1) or (n__1 >= -1 and tmp__1 <= n__1) or (tmp__1 >= 0 and tmp__1 <= n__1); start[n, tmp, x, y]; cut[n__1, tmp__1, x__1, y__1] : x__1 >= -1 or (tmp__1 <= n__1 and x__1 >= -1 and y__1 >= -1 and y__1 <= tmp__1) or (x__1 >= -1 and tmp__1 <= n__1 and y__1 >= -1 and y__1 <= tmp__1) or (y__1 <= tmp__1 and y__1 >= -1 and x__1 >= -1 and tmp__1 <= n__1) or (y__1 <= 1 + tmp__1 and tmp__1 >= 0 and tmp__1 <= n__1 and y__1 >= -1 and x__1 >= -1) or (y__1 >= -1 and y__1 <= tmp__1 and x__1 >= -1 and tmp__1 <= n__1) or (x__1 >= -1 and tmp__1 <= n__1 and tmp__1 >= 1 and y__1 >= -1 and y__1 <= 1 + tmp__1) or (x__1 >= -1 and y__1 >= -1) or (x__1 >= -1 and y__1 >= -1) or (x__1 >= -1 and y__1 >= -1) or (x__1 >= -1 and y__1 >= -1) or (tmp__1 >= 0 and y__1 >= -1 and y__1 <= tmp__1 and x__1 >= -1 and tmp__1 <= n__1) or (y__1 >= -1 and y__1 <= tmp__1 and n__1 >= 0 and x__1 >= -1 and tmp__1 <= n__1) or (tmp__1 <= n__1 and tmp__1 >= -1 and y__1 >= -1 and y__1 <= 1 + tmp__1 and x__1 >= -1) or (y__1 >= -1 and tmp__1 <= n__1 and x__1 >= -1 and tmp__1 >= -1 and y__1 <= 1 + tmp__1) or x__1 >= -1 or (y__1 >= -1 and x__1 >= -1) or (x__1 >= -1 and y__1 >= -1 and y__1 <= tmp__1 and tmp__1 <= n__1) or (y__1 <= tmp__1 and y__1 >= -1 and tmp__1 <= n__1 and x__1 >= -1) or (x__1 >= -1 and y__1 >= -1 and tmp__1 >= -1 and y__1 <= 1 + tmp__1 and tmp__1 <= n__1) or (y__1 >= -1 and tmp__1 <= n__1 and x__1 >= -1 and y__1 <= tmp__1) or (tmp__1 <= n__1 and y__1 >= -1 and y__1 <= 1 + tmp__1 and x__1 >= -1 and tmp__1 >= 0); cut[n__1, tmp__1, x__1, 1 + tmp__1] : (tmp__1 <= n__1 and x__1 >= -1) or (tmp__1 <= n__1 and x__1 >= -1) or tmp__1 <= n__1 or tmp__1 <= n__1 or (tmp__1 <= n__1 and n__1 >= -1) or (x__1 >= -1 and tmp__1 >= -1 and tmp__1 <= n__1) or (x__1 >= -1 and tmp__1 >= -1 and tmp__1 <= n__1) or (n__1 >= 0 and tmp__1 <= n__1) or (tmp__1 >= 0 and tmp__1 <= n__1) or (x__1 >= -1 and tmp__1 >= -1 and tmp__1 <= n__1) or (tmp__1 <= n__1 and n__1 >= -1) or (tmp__1 >= 0 and tmp__1 <= n__1) or (tmp__1 <= n__1 and n__1 >= 0) or (x__1 >= -1 and tmp__1 <= n__1) or (tmp__1 <= n__1 and tmp__1 >= -1 and x__1 >= -1) or (tmp__1 >= 0 and tmp__1 <= n__1) or tmp__1 <= n__1 or (n__1 >= -1 and tmp__1 <= n__1) or tmp__1 <= n__1 } (1.70s), failed.