
module main
{
  type side_t = enum { LEFT, RIGHT };
  type item_t = enum { NONE, FERRYMAN, GOAT, CABBAGE, WOLF };

  var ferryman : side_t;
  var goat : side_t;
  var cabbage : side_t;
  var wolf : side_t;
  var carry : item_t;

  init {
    ferryman = LEFT;
    goat = LEFT;
    cabbage = LEFT;
    wolf = LEFT;
    carry = NONE;
  }

  procedure cross(item : item_t)
    modifies ferryman;
    modifies goat;
    modifies cabbage;
    modifies wolf;
    modifies carry;
  {
    if (ferryman == LEFT) {
      ferryman' = RIGHT;
      carry' = item;
      if (item == GOAT) {
        goat' = RIGHT;
      } else if (item == CABBAGE) {
        cabbage' = RIGHT;
      } else if (item == WOLF) {
        wolf' = RIGHT;
      }
    } else {
      ferryman' = LEFT;
      carry' = NONE;
      if (item == GOAT) {
        goat' = LEFT;
      } else if (item == CABBAGE) {
        cabbage' = LEFT;
      } else if (item == WOLF) {
        wolf' = LEFT;
      }
    }
  }

  transition {
    // All possible moves
    cross(NONE);
    cross(GOAT);
    cross(CABBAGE);
    cross(WOLF);
  }

  function goal_state_reached() : boolean
  {
    return (ferryman == RIGHT) && (goat == RIGHT) && (cabbage == RIGHT) && (wolf == RIGHT);
  }

  property no_conflict()
  {
    assert !( (goat == cabbage && goat != ferryman) || (goat == wolf && goat != ferryman) );
  }

  control {
    while (!goal_state_reached()) {
      next;
    }
    check no_conflict();
  }
}
