Figure¶

Source code¶

model gulwani_jain_koskinen_pldi09_02 {

  var id, tmp, max_id, i;

  states q;

  transition t2 := {
    from   := q;
    to     := q;
    guard  := tmp != id && tmp > max_id;
    action := tmp' = 0, i' = i + 1;
  };

  transition t1 := {
    from   := q;
    to     := q;
    guard  := tmp != id && tmp <= max_id;
    action := tmp' = tmp + 1, i' = i + 1;
  };

}

strategy gulwani_jain_koskinen_pldi09_02_s {

  Region init := {state = q && 0 <= id && id < max_id && tmp = id + 1 && i = 0};

}

Expected invariant¶

{ q[v1, v2, v3, v4] : v4 <= 1 + v3 }

Results¶

• With Aspic: { q[id, tmp, max_id, i] : max_id >= 1 + id and max_id >= -1 + tmp and i >= 0 and tmp >= 0 and i >= 1 - tmp and i >= 1 - 2tmp and i >= -1 - id + tmp and id >= 0 } (0.05s), failed.
• With ISL: { q[id__1, tmp__1, max_id__1, i__1] : (id__1 >= 0 and max_id__1 >= 1 + id__1 and i__1 >= 1 and tmp__1 <= id__1 and max_id__1 >= -1 + tmp__1) or (id__1 >= 0 and max_id__1 >= 1 + id__1 and i__1 >= 1 and tmp__1 >= 2 + id__1 and max_id__1 >= -1 + tmp__1); q[id, 1 + id, max_id, 0] : id >= 0 and max_id >= 1 + id; q[id__1, 0, max_id__1, i__1] : id__1 >= 0 and max_id__1 >= 1 + id__1 and i__1 >= 1; q[id__1, tmp__1, max_id__1, -1 - id__1 + tmp__1] : id__1 >= 0 and max_id__1 >= 1 + id__1 and max_id__1 >= -1 + tmp__1 and tmp__1 >= 2 + id__1 } (0.02s), failed.