ALICe documentation

Model relation1

«  Model realshellsort   ::   Contents   ::   Model rsd  »

Model relation1

Cited in: [AliasDFG10].

Tag: complexity.

Figure

../_images/relation1.png

Source code

model relation1 {

  var x, y;

  states start, lbl_4_1, stop;

  transition t_22 := {
    from   := start;
    to     := lbl_4_1;
    guard  := true;
    action := x' = ?;
  };

  transition t_18 := {
    from   := lbl_4_1;
    to     := stop;
    guard  := true;
    action := y' = x;
  };

}

strategy relation1_s {

  Region init := {state = start};

}

Expected invariant

{ stop[v1, v1] }

Results

  • With Aspic: { stop[x, x]; lbl_4_1[x, y]; start[x, y] } (0.08s), OK.
  • With ISL: { lbl_4_1[x__1, y__1]; start[x, y]; stop[x__1, x__1] } (0.00s), OK.

«  Model realshellsort   ::   Contents   ::   Model rsd  »