Figure¶

Source code¶

model gulwani_zuleger_pldi10_03b {

  var n, m, j;

  states q1, q2;

  transition t1b := {
    from   := q1;
    to     := q2;
    guard  := j > n;
    action := ;
  };

  transition t1a := {
    from   := q1;
    to     := q2;
    guard  := j < n;
    action := ;
  };

  transition t3 := {
    from   := q2;
    to     := q1;
    guard  := j <= m;
    action := j' = j + 1;
  };

  transition t2 := {
    from   := q2;
    to     := q1;
    guard  := j > m;
    action := j' = 0;
  };

}

strategy gulwani_zuleger_pldi10_03b_s {

  Region init := {state = q1 && 0 < n && n < m && j = n + 1};

}

Expected invariant¶

{ q2[v1, v2, v3] : v1 >= 1 and v3 <= 1 + v2 and v3 >= 0 and v2 >= 1 + v1; q1[v1, v2, v3] : v3 >= 0 and v3 <= 1 + v2 and v1 >= 1 and v2 >= 1 + v1 }

Results¶

• With Aspic: { q2[n, m, j] : n >= 1 and j <= 1 + m and j >= 0 and m >= 1 + n; q1[n, m, j] : j >= 0 and j <= 1 + m and n >= 1 and m >= 1 + n } (0.05s), OK.
• With ISL: { q2[n__1, m__1, j__1] : (n__1 >= 1 and m__1 >= 1 + n__1 and j__1 <= 1 + m__1 and j__1 <= -1 + n__1) or (n__1 >= 1 and m__1 >= 1 + n__1 and j__1 >= 1 + n__1 and j__1 <= 1 + m__1) or (n__1 >= 1 and m__1 >= 1 + n__1 and j__1 <= -1 + n__1) or (n__1 >= 1 and m__1 >= 1 + n__1 and j__1 >= 1 + n__1 and j__1 <= 1 + m__1); q2[n__1, m__1, 0] : n__1 >= 1 and m__1 >= 1 + n__1; q2[n__1, m__1, 1 + n__1] : n__1 >= 1 and m__1 >= 1 + n__1; q1[n__1, m__1, j__1] : (n__1 >= 1 and m__1 >= 1 + n__1 and j__1 <= n__1) or (n__1 >= 1 and m__1 >= 1 + n__1 and j__1 >= 2 + n__1 and j__1 <= 1 + m__1); q1[n__1, m__1, 0] : n__1 >= 1 and m__1 >= 1 + n__1; q1[n, m, 1 + n] : n >= 1 and m >= 1 + n } (2.93s), failed.