ALICe documentation

Model disj

«  Model determinant   ::   Contents   ::   Model disjbnd1  »

Model disj

Cited in: [BeyerHMR07] fig. 4 p. 7, [GulwaniZ10] fig. 9 p. 12.

Tag: fixpoint.

Figure

../_images/disj.png

Source code

model beyer_henzinger_majumdar_rybalchenko_pldi07_07 {

  var x, y;

  states q1, q3, q2;

  transition t4 := {
    from   := q1;
    to     := q3;
    guard  := x >= 100;
    action := ;
  };

  transition t1 := {
    from   := q1;
    to     := q2;
    guard  := x < 100;
    action := ;
  };

  transition t3 := {
    from   := q2;
    to     := q1;
    guard  := x >= 50;
    action := x' = x + 1, y' = y + 1;
  };

  transition t2 := {
    from   := q2;
    to     := q1;
    guard  := x < 50;
    action := x' = x + 1;
  };

}

strategy beyer_henzinger_majumdar_rybalchenko_pldi07_07_s {

  Region init := {state = q1 && x = 0 && y = 50};

}

Expected invariant

{ q1[v1, v2] : v2 >= v1 and v2 >= 50; q2[v1, v2] : v2 >= 50 and v2 >= v1 and v1 <= 99; q3[v1, v2] : v2 >= v1 and v1 >= 100 }

Results

  • With Aspic: { q1[x, y] : y >= x and y >= 50; q2[x, y] : y >= 50 and y >= x and x <= 99; q3[x, y] : y >= x and x >= 100 } (0.06s), OK.
  • With ISL: { q1[x__1, 50] : x__1 >= 1 and x__1 <= 50; q1[x__1, x__1] : x__1 >= 51 and x__1 <= 100; q1[0, 50]; q3[100, 100]; q2[x__1, 50] : x__1 >= 1 and x__1 <= 50; q2[x__1, x__1] : x__1 >= 51 and x__1 <= 99; q2[0, 50] } (0.02s), OK.

«  Model determinant   ::   Contents   ::   Model disjbnd1  »