module Module {
  var C: real;
  var F: boolean;
  var G: boolean;
  var W: boolean;
  var allow1: boolean;
  var allow2: boolean;
  var cabbage: real;
  var carry: [integer]boolean;
  var cr: [integer]boolean;
  var ferryman: boolean;
  var goat: boolean;
  var wolf: boolean;

  procedure step()
    modifies G;
    modifies allow2;
    modifies allow1;
    modifies W;
    modifies ferryman;
    modifies C;
    modifies cr;
    modifies F;
  {
    F = ferryman;
    G = goat;
    C = cabbage;
    W = wolf;
    cr = carry;
    allow1 = ((F == G) && (cr[0] != G));
    allow2 = ((F == W) && (cr[0] != W));
    if (ferryman) {
      if (cr[2]) {
        cr = cr[0 -> !cr[0]];
      } else {
        if (((F == G) && allow1) || ((F == W) && allow2)) {
          ferryman = F;
        }
      }
    } else {
      if (cr[2]) {
        cr = cr[0 -> !cr[0]];
      } else {
        if (((F == G) && allow1) || ((F == W) && allow2)) {
          ferryman = F;
        }
      }
    }
  }

  next {
    call step();
  }
  invariant spec: (ferryman == true);

}
