Figure¶

Source code¶

model gulwani_jain_koskinen_pldi09_05d {

  var i, m, n, b, c;

  states q;

  transition t2 := {
    from   := q;
    to     := q;
    guard  := 0 < i && i < n && b = 0;
    action := i' = i - 1, c' = c + 1;
  };

  transition t1 := {
    from   := q;
    to     := q;
    guard  := 0 < i && i < n && b = 1;
    action := i' = i + 1, c' = c + 1;
  };

}

strategy gulwani_jain_koskinen_pldi09_05d_s {

  Region init := {state = q && 0 < m && m < n && i = m && c = 0};

}

Expected invariant¶

{ q[v1, v2, v3, v4, v5] : v5 <= v2 or (v5 >= 1 + v2 and v5 <= -v2 + v3) }

Results¶

• With Aspic: { q[i, m, n, b, c] : m >= 1 and c >= -i + m and i >= 0 and n >= 1 + m and c >= i - m and n >= i } (0.05s), failed.
• With ISL: { q[i__1, m__1, n__1, 1, i__1 - m__1] : m__1 >= 1 and n__1 >= 1 + m__1 and m__1 <= -1 + i__1 and n__1 >= i__1 and i__1 >= 2; q[i, i, n, b, 0] : i >= 1 and n >= 1 + i; q[i__1, m__1, n__1, 0, -i__1 + m__1] : m__1 >= 1 and n__1 >= 1 + m__1 and m__1 >= 1 + i__1 and n__1 >= 2 + i__1 and i__1 >= 0 } (0.02s), OK.