Figure¶

Source code¶

model gulwani_zuleger_pldi10_04c {

  var flag, n, n0, i, c;

  states q1, q2;

  transition t1 := {
    from   := q1;
    to     := q2;
    guard  := i < n;
    action := flag' = 0, c' = c + 1;
  };

  transition t4 := {
    from   := q2;
    to     := q1;
    guard  := flag = 0;
    action := i' = i + 1;
  };

  transition t3 := {
    from   := q2;
    to     := q1;
    guard  := flag = 1;
    action := ;
  };

  transition t2 := {
    from   := q2;
    to     := q2;
    guard  := true;
    action := flag' = 1, n' = n - 1;
  };

}

strategy gulwani_zuleger_pldi10_04c_s {

  Region init := {state = q1 && n >= 0 && n = n0 && flag = 1 && i = 0 && c = 0};

}

Expected invariant¶

{ q1[v1, v2, v3, v4, v5] : v5 <= v3; q2[v1, v2, v3, v4, v5] : v5 <= v3 }

Results¶

• With Aspic: { q2[flag, n, n0, i, 1 - flag - n + n0 + i] : n0 >= flag + n and i >= 0 and flag >= 0 and i <= -1 + flag + n; q1[flag, n, n0, i, -n + n0 + i] : n0 >= n and i <= 1 - flag + n0 and flag <= 1 and i <= n and i >= 1 - flag } (0.04s), OK.
• With ISL: { q1[1, n__1, n0__1, i__1, c__1] : n0__1 >= 1 and c__1 >= 1 + i__1 and n0__1 >= 1 + n__1 and i__1 >= 0; q1[0, n__1, n0__1, i__1, c__1] : n0__1 >= 0 and c__1 >= i__1 and i__1 <= n__1 and n0__1 >= 1 + n__1 and i__1 >= 1; q1[0, n__1, n__1, i__1, i__1] : n__1 >= 0 and i__1 >= 1 and i__1 <= n__1; q1[1, n, n, 0, 0] : n >= 0; q2[1, n__1, n0__1, i__1, c__1] : n0__1 >= 1 and c__1 >= 1 + i__1 and n0__1 >= 1 + n__1 and i__1 >= 0; q2[0, n__1, n0__1, i__1, c__1] : n0__1 >= 0 and c__1 >= 1 + i__1 and i__1 <= -1 + n__1 and n0__1 >= 1 + n__1 and i__1 >= 0; q2[0, n__1, n__1, i__1, 1 + i__1] : n__1 >= 0 and i__1 >= 0 and i__1 <= -1 + n__1 } (0.36s), failed.