ALICe documentation

Model gonnord5

«  Model gonnord4   ::   Contents   ::   Model gonnord6  »

Model gonnord5

Cited in: [Gonnord_thesis] fig. 7.4 p. 93.

Tag: fixpoint.

Figure

../_images/gonnord5.png

Source code

model gonnord_thesis_93b {

  var x, z;

  states q;

  transition t2 := {
    from   := q;
    to     := q;
    guard  := true;
    action := z' = 0;
  };

  transition t1 := {
    from   := q;
    to     := q;
    guard  := x >= 2 * z;
    action := x' = x + 1, z' = z + 1;
  };

}

strategy gonnord_thesis_93b_s {

  Region init := {state = q && x = 0 && z = 0};

}

Expected invariant

{ q[v1, v2] : v2 <= v1 and v2 >= 0 and 2v2 <= 1 + v1 }

Results

  • With Aspic: { q[x, z] : 2z <= 1 + x and z <= x and z >= 0 } (0.05s), OK.
  • With ISL: { q[x__1, z__1] : 2z__1 <= 1 + x__1 and x__1 >= 0; q[x__1, 0] : x__1 >= 0; q[1, 1]; q[0, 0] } (0.00s), failed.

«  Model gonnord4   ::   Contents   ::   Model gonnord6  »