Figure¶

Source code¶

model bultan_gerber_pugh_cav97_03 {

  var a, b, pc1, pc2;

  states q;

  transition e_C2 := {
    from   := q;
    to     := q;
    guard  := pc2 = 3;
    action := pc2' = 1, b' = 0;
  };

  transition e_W2b := {
    from   := q;
    to     := q;
    guard  := pc2 = 2 && a = 0;
    action := pc2' = 3;
  };

  transition e_W2a := {
    from   := q;
    to     := q;
    guard  := pc2 = 2 && b < a;
    action := pc2' = 3;
  };

  transition e_T2 := {
    from   := q;
    to     := q;
    guard  := pc2 = 1;
    action := pc2' = 2, b' = a + 2;
  };

  transition e_C1 := {
    from   := q;
    to     := q;
    guard  := pc1 = 3;
    action := pc1' = 1, a' = 0;
  };

  transition e_W1b := {
    from   := q;
    to     := q;
    guard  := pc1 = 2 && b = 0;
    action := pc1' = 3;
  };

  transition e_W1a := {
    from   := q;
    to     := q;
    guard  := pc1 = 2 && a < b;
    action := pc1' = 3;
  };

  transition e_T1 := {
    from   := q;
    to     := q;
    guard  := pc1 = 1;
    action := pc1' = 2, a' = b + 1;
  };

}

strategy bultan_gerber_pugh_cav97_03_s {

  Region init := {state = q && a = 0 && b = 0 && pc1 = 1 && pc2 = 1};

}

Expected invariant¶

{ q[v1, v2, v3, v4] : v4 <= 2 or v4 >= 4; q[v1, v2, v3, 3] : v3 <= 2 or v3 >= 4 }

Results¶

• With Aspic: { q[a, b, pc1, pc2] } (0.07s), failed.
• With ISL: { q[a__1, b__1, pc1__1, 3] : b__1 <= -1 + a__1 or b__1 <= -1 + a__1 or (b__1 <= -1 + a__1 and pc1__1 >= 2) or b__1 <= -1 + a__1 or (exists (e0, e1, e2, e3 = [(5 + 2pc1__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 5 + 2pc1__1 - 2e0 + 2e1 - 3e2 and b__1 <= -1 + a__1 and 3e2 >= 11 + 2pc1__1 - 2e0 + 2e1 and e2 <= -1 and e2 <= pc1__1 and e1 <= -1 + e0)) or (b__1 <= -1 + a__1 and pc1__1 >= 2) or b__1 <= -1 + a__1 or b__1 <= -1 + a__1 or (b__1 <= -1 + a__1 and pc1__1 >= 2) or b__1 <= -1 + a__1 or b__1 <= -1 + a__1 or (b__1 <= -1 + a__1 and pc1__1 >= 2) or b__1 <= -1 + a__1 or (exists (e0, e1, e2, e3 = [(5 + 2pc1__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 5 + 2pc1__1 - 2e0 + 2e1 - 3e2 and b__1 <= -1 + a__1 and 3e2 >= 11 + 2pc1__1 - 2e0 + 2e1 and e2 <= -1 and e2 <= pc1__1 and e1 <= -1 + e0)) or (b__1 <= -1 + a__1 and pc1__1 >= 2) or b__1 <= -1 + a__1 or b__1 <= -1 + a__1 or (b__1 <= -1 + a__1 and pc1__1 >= 2); q[a__1, 0, pc1__1, 1] : (exists (e0, e1, e2, e3 = [(1 + 2pc1__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 1 + 2pc1__1 - 2e0 + 2e1 - 3e2 and 3e2 >= 7 + 2pc1__1 - 2e0 + 2e1 and e2 <= -1 and e2 <= pc1__1 and e1 <= -1 + e0)) or (exists (e0, e1, e2, e3 = [(1 + 2pc1__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 1 + 2pc1__1 - 2e0 + 2e1 - 3e2 and 3e2 >= 7 + 2pc1__1 - 2e0 + 2e1 and e2 <= -1 and e2 <= pc1__1 and e1 <= -1 + e0)); q[a__1, 0, 3, pc2__1]; q[0, 0, 1, 1]; q[0, b__1, pc1__1, 3] : (exists (e0, e1, e2, e3 = [(5 + 2pc1__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 5 + 2pc1__1 - 2e0 + 2e1 - 3e2 and 3e2 >= 11 + 2pc1__1 - 2e0 + 2e1 and e2 <= -1 and e2 <= pc1__1 and e1 <= -1 + e0)) or (exists (e0, e1, e2, e3 = [(5 + 2pc1__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 5 + 2pc1__1 - 2e0 + 2e1 - 3e2 and 3e2 >= 11 + 2pc1__1 - 2e0 + 2e1 and e2 <= -1 and e2 <= pc1__1 and e1 <= -1 + e0)); q[0, 0, 1, pc2__1] : pc2__1 >= 1 or pc2__1 >= 1 or pc2__1 >= 2 or pc2__1 >= 1 or pc2__1 >= 1 or pc2__1 >= 2; q[0, b__1, 1, pc2__1] : (exists (e0, e1, e2, e3 = [(1 + 2pc2__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 1 + 2pc2__1 - 2e0 + 2e1 - 3e2 and 3e2 >= 7 + 2pc2__1 - 2e0 + 2e1 and e2 <= -1 and e1 <= -1 + e0 and 3e2 >= 4 - pc2__1 - 2e0 + 2e1)) or (exists (e0, e1, e2, e3 = [(1 + 2pc2__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 1 + 2pc2__1 - 2e0 + 2e1 - 3e2 and 3e2 >= 7 + 2pc2__1 - 2e0 + 2e1 and e2 <= -1 and 3e2 >= 4 - pc2__1 - 2e0 + 2e1 and e1 <= -1 + e0)); q[-2, 0, pc1__1, 2]; q[a__1, -1 + a__1, 2, pc2__1] : (exists (e0, e1, e2, e3 = [(3 + 2pc2__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 3 + 2pc2__1 - 2e0 + 2e1 - 3e2 and 3e2 >= 9 + 2pc2__1 - 2e0 + 2e1 and e2 <= -1 and e1 <= -1 + e0 and 3e2 >= 6 - pc2__1 - 2e0 + 2e1)) or (exists (e0, e1, e2, e3 = [(3 + 2pc2__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 3 + 2pc2__1 - 2e0 + 2e1 - 3e2 and 3e2 >= 9 + 2pc2__1 - 2e0 + 2e1 and e2 <= -1 and 3e2 >= 6 - pc2__1 - 2e0 + 2e1 and e1 <= -1 + e0)); q[0, 0, 3, pc2__1]; q[0, b__1, 3, pc2__1] : b__1 >= 1 or b__1 >= 1 or (b__1 >= 1 and pc2__1 >= 2) or b__1 >= 1 or b__1 >= 1 or (b__1 >= 1 and pc2__1 >= 2); q[0, 0, pc1__1, 3]; q[a__1, 0, pc1__1, 3] : a__1 >= 1 or a__1 >= 1 or (a__1 >= 1 and pc1__1 >= 2) or a__1 >= 1 or a__1 >= 1 or (a__1 >= 1 and pc1__1 >= 2); q[0, 2, pc1__1, 2] : pc1__1 >= 1 or pc1__1 >= 1 or pc1__1 >= 1 or pc1__1 >= 1 or pc1__1 >= 1 or pc1__1 >= 1; q[1, 0, 2, pc2__1] : pc2__1 >= 1 or pc2__1 >= 1 or pc2__1 >= 1 or pc2__1 >= 1 or pc2__1 >= 1 or pc2__1 >= 1; q[a__1, 0, pc1__1, 1]; q[a__1, -1 + a__1, 2, pc2__1]; q[a__1, 2 + a__1, pc1__1, 2] : (exists (e0, e1, e2, e3 = [(3 + 2pc1__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 3 + 2pc1__1 - 2e0 + 2e1 - 3e2 and 3e2 >= 9 + 2pc1__1 - 2e0 + 2e1 and e2 <= -1 and e2 <= pc1__1 and e1 <= -1 + e0)) or (exists (e0, e1, e2, e3 = [(3 + 2pc1__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 3 + 2pc1__1 - 2e0 + 2e1 - 3e2 and 3e2 >= 9 + 2pc1__1 - 2e0 + 2e1 and e2 <= -1 and e2 <= pc1__1 and e1 <= -1 + e0)); q[a__1, b__1, 3, pc2__1] : b__1 >= 1 + a__1 or b__1 >= 1 + a__1 or b__1 >= 1 + a__1 or b__1 >= 1 + a__1 or (exists (e0, e1, e2, e3 = [(5 + 2pc2__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 5 + 2pc2__1 - 2e0 + 2e1 - 3e2 and b__1 >= 1 + a__1 and 3e2 >= 11 + 2pc2__1 - 2e0 + 2e1 and e2 <= -1 and e1 <= -1 + e0 and 3e2 >= 8 - pc2__1 - 2e0 + 2e1)) or b__1 >= 1 + a__1 or (b__1 >= 1 + a__1 and pc2__1 >= 2) or (b__1 >= 1 + a__1 and pc2__1 >= 2) or (b__1 >= 1 + a__1 and pc2__1 >= 2) or b__1 >= 1 + a__1 or b__1 >= 1 + a__1 or b__1 >= 1 + a__1 or b__1 >= 1 + a__1 or (exists (e0, e1, e2, e3 = [(5 + 2pc2__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 5 + 2pc2__1 - 2e0 + 2e1 - 3e2 and b__1 >= 1 + a__1 and 3e2 >= 11 + 2pc2__1 - 2e0 + 2e1 and e2 <= -1 and 3e2 >= 8 - pc2__1 - 2e0 + 2e1 and e1 <= -1 + e0)) or b__1 >= 1 + a__1 or (b__1 >= 1 + a__1 and pc2__1 >= 2) or (b__1 >= 1 + a__1 and pc2__1 >= 2) or (b__1 >= 1 + a__1 and pc2__1 >= 2); q[0, b__1, pc1__1, 3]; q[0, b__1, 1, pc2__1]; q[a__1, 2 + a__1, pc1__1, 2]; q[0, 0, pc1__1, 1] : pc1__1 >= 1 or pc1__1 >= 1 or pc1__1 >= 2 or pc1__1 >= 1 or pc1__1 >= 1 or pc1__1 >= 2; q[a__1, 0, 3, pc2__1] : (exists (e0, e1, e2, e3 = [(5 + 2pc2__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 5 + 2pc2__1 - 2e0 + 2e1 - 3e2 and 3e2 >= 11 + 2pc2__1 - 2e0 + 2e1 and e2 <= -1 and e1 <= -1 + e0 and 3e2 >= 8 - pc2__1 - 2e0 + 2e1)) or (exists (e0, e1, e2, e3 = [(5 + 2pc2__1 - 2e0 + 2e1 - 3e2)/6]: 6e3 = 5 + 2pc2__1 - 2e0 + 2e1 - 3e2 and 3e2 >= 11 + 2pc2__1 - 2e0 + 2e1 and e2 <= -1 and 3e2 >= 8 - pc2__1 - 2e0 + 2e1 and e1 <= -1 + e0)); q[0, -1, 2, pc2__1] } (0.24s), failed.