ALICe documentation

Model nd_loop

«  Model multcounters4   ::   Contents   ::   Model ndecr  »

Model nd_loop

Cited in: [AliasDFG10].

Tag: fixpoint.

Figure

../_images/nd_loop.png

Source code

model nd_loop {

  var x, y;

  states start, lbl_5_1, stop, cut;

  transition t_22 := {
    from   := start;
    to     := lbl_5_1;
    guard  := true;
    action := x' = ?, y' = 0;
  };

  transition t_20 := {
    from   := lbl_5_1;
    to     := stop;
    guard  := x <= y + 2 && y + 1 <= x && 10 <= x;
    action := ;
  };

  transition t_19 := {
    from   := lbl_5_1;
    to     := cut;
    guard  := x <= y + 2 && x <= 9 && y + 1 <= x;
    action := ;
  };

  transition t_18 := {
    from   := lbl_5_1;
    to     := stop;
    guard  := x <= y || y + 3 <= x;
    action := ;
  };

  transition t_21 := {
    from   := cut;
    to     := lbl_5_1;
    guard  := true;
    action := x' = ?, y' = x;
  };

}

strategy nd_loop_s {

  Region init := {state = start};

}

Expected invariant

{ lbl_5_1[v1, v2] : v2 >= 0; cut[v1, v2] : v2 >= -2 + v1 and v2 >= 0 and v1 <= 9 and v2 <= -1 + v1; stop[v1, v2] : v2 >= 0 }

Results

  • With Aspic: { stop[x, y] : y >= 0; lbl_5_1[x, y] : y >= 0; start[x, y]; cut[x, y] : y >= -2 + x and y >= 0 and x <= 9 and y <= -1 + x } (0.04s), OK.
  • With ISL: { lbl_5_1[x__1, y__1] : y__1 >= 1 and y__1 <= 9; lbl_5_1[x__1, 0]; cut[x__1, y__1] : y__1 >= -2 + x__1 and x__1 <= 9 and y__1 >= 1 and y__1 <= -1 + x__1; cut[x__1, 0] : x__1 <= 2 and x__1 >= 1; stop[x__1, y__1] : (y__1 >= 1 and y__1 <= 9 and y__1 <= -3 + x__1) or (y__1 >= 1 and y__1 <= 9 and y__1 >= x__1) or (y__1 >= 1 and y__1 <= 9 and y__1 >= -2 + x__1 and y__1 <= -1 + x__1 and x__1 >= 10); stop[x__1, 0] : x__1 >= 3 or x__1 <= 0; start[x, y] } (0.00s), OK.

«  Model multcounters4   ::   Contents   ::   Model ndecr  »