Figure¶

Source code¶

model main {

  var i, j, length, tmp_1, value;

  states start, lbl_3_1, lbl_1_3, stop, lbl_4_3;

  transition t_19 := {
    from   := start;
    to     := lbl_3_1;
    guard  := 2 <= length;
    action := i' = 1, value' = ?;
  };

  transition t_18 := {
    from   := start;
    to     := stop;
    guard  := length <= 1;
    action := i' = 1;
  };

  transition t_23 := {
    from   := lbl_3_1;
    to     := lbl_1_3;
    guard  := true;
    action := i' = i + 1, j' = i - 1, tmp_1' = i;
  };

  transition t_22 := {
    from   := lbl_3_1;
    to     := lbl_4_3;
    guard  := 1 <= i;
    action := j' = i - 2;
  };

  transition t_17 := {
    from   := lbl_1_3;
    to     := lbl_3_1;
    guard  := i + 1 <= length;
    action := value' = ?;
  };

  transition t_16 := {
    from   := lbl_1_3;
    to     := stop;
    guard  := length <= i;
    action := ;
  };

  transition t_21 := {
    from   := lbl_4_3;
    to     := lbl_1_3;
    guard  := true;
    action := i' = i + 1, tmp_1' = i;
  };

  transition t_20 := {
    from   := lbl_4_3;
    to     := lbl_4_3;
    guard  := 0 <= j;
    action := j' = j - 1;
  };

}

strategy main_s {

  Region init := {state = start};

}

Expected invariant¶

{ lbl_4_3[v1, v2, v3, v4, v5] : v2 >= -1 and v2 <= -2 + v1 and v3 >= 1 + v1; lbl_3_1[v1, v2, v3, v4, v5] : v1 >= 1 and v3 >= 1 + v1; stop[v1, v2, v3, v4, v5] : v1 >= 1 and v3 <= v1; lbl_1_3[v1, v2, v3, -1 + v1, v5] : v1 >= 2 and v2 <= -2 + v1 and v2 >= -1 and v3 >= v1 }

Results¶

• With Aspic: { lbl_1_3[i, j, length, -1 + i, value] : j >= -1 and length >= i and i >= 2 and j <= -2 + i; start[i, j, length, tmp_1, value]; lbl_4_3[i, j, length, tmp_1, value] : j >= -1 and j <= -2 + i and length >= 1 + i; lbl_3_1[i, j, length, tmp_1, value] : i >= 1 and length >= 1 + i; stop[i, j, length, tmp_1, value] : i >= 1 and length <= i } (0.06s), OK.
• With ISL: { lbl_1_3[i__1, j__1, length__1, -1 + i__1, value__1] : length__1 >= 3 and i__1 >= 3 and j__1 >= -1; lbl_1_3[i__1, -2 + i__1, length__1, -1 + i__1, value__1] : length__1 >= 2 and i__1 >= 3 and length__1 >= i__1; lbl_1_3[i__1, -3 + i__1, length__1, -1 + i__1, value__1] : length__1 >= 2 and i__1 >= 3 and length__1 >= i__1; lbl_1_3[2, 0, length__1, 1, value__1] : length__1 >= 2; lbl_1_3[2, -1, length__1, 1, value__1] : length__1 >= 2; start[i, j, length, tmp_1, value]; lbl_3_1[1, j__1, length__1, tmp_1__1, value__1] : length__1 >= 2; lbl_3_1[i__1, j__1, length__1, -1 + i__1, value__1] : (length__1 >= 2 and j__1 >= -1 and length__1 >= 1 + i__1 and i__1 >= 2 and j__1 <= -3 + i__1) or (length__1 >= 2 and length__1 >= 1 + i__1 and i__1 >= 3 and j__1 >= -1); lbl_3_1[i__1, -2 + i__1, length__1, -1 + i__1, value__1] : length__1 >= 2 and i__1 >= 2 and length__1 >= 1 + i__1; stop[1, j__1, length__1, tmp_1__1, value__1] : length__1 <= 1; stop[i__1, j__1, length__1, -1 + i__1, value__1] : length__1 >= 3 and i__1 >= 3 and j__1 >= -1 and length__1 <= i__1; stop[i__1, -2 + i__1, i__1, -1 + i__1, value__1] : i__1 >= 3; stop[i__1, -3 + i__1, i__1, -1 + i__1, value__1] : i__1 >= 3; stop[2, 0, 2, 1, value__1]; stop[2, -1, 2, 1, value__1]; lbl_4_3[i__1, j__1, length__1, tmp_1__1, value__1] : length__1 >= 3 and i__1 >= 2 and j__1 >= -1; lbl_4_3[i__1, -2 + i__1, length__1, -1 + i__1, value__1] : length__1 >= 2 and i__1 >= 2 and length__1 >= 1 + i__1; lbl_4_3[1, -1, length__1, tmp_1__1, value__1] : length__1 >= 2 } (0.62s), failed.