« Model gasburner :: Contents :: Model gcd »

Model gasburner_alt¶

Cited in: [Gonnord_thesis] fig. 7.7 p. 99.

Tag: fixpoint.

Figure¶

../_images/gasburner_alt.png

Source code¶

model gonnord_thesis_099 {

  var u, t, l, v;

  states q;

  transition t3 := {
    from   := q;
    to     := q;
    guard  := u = 60;
    action := u' = 0, v' = 0;
  };

  transition t2 := {
    from   := q;
    to     := q;
    guard  := u <= 59;
    action := u' = u + 1, t' = t + 1;
  };

  transition t1 := {
    from   := q;
    to     := q;
    guard  := u <= 59 && v <= 9;
    action := u' = u + 1, t' = t + 1, l' = l + 1, v' = v + 1;
  };

}

strategy gonnord_thesis_099_s {

  Region init := {state = q && u = 0 && t = 0 && l = 0 && v = 0};

}

Expected invariant¶

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

Results¶

With Aspic: { q[u, t, l, v] : v <= 10 and v <= u and v <= l and v >= 0 and v >= u - t + l and u <= 60 } (0.05s), failed.
With ISL: { q[u__1, t__1, l__1, v__1] : exists (e0 = [(-u__1 + t__1)/60]: 60e0 = -u__1 + t__1 and 61t__1 >= 60 + u__1 and u__1 <= 60 and t__1 >= 60 + u__1 and l__1 <= t__1 and l__1 >= 0); q[u__1, u__1, l__1, l__1] : u__1 >= 1 and u__1 <= 60 and l__1 <= u__1 and l__1 >= 0; q[0, 0, 0, 0] } (0.02s), failed.

« Model gasburner :: Contents :: Model gcd »