ferryman(1).smv

-- Ferryman by Bow-Yaw Wang
MODULE main
VAR
  ferryman : boolean;
  goat : boolean;
  cabbage : boolean;
  wolf : boolean;
  carry : { g, c, w, n };
ASSIGN
  init (ferryman) := FALSE;
  init (goat) := FALSE;
  init (cabbage) := FALSE;
  init (wolf) := FALSE;
  init (carry) := n;

  next (ferryman) := { FALSE, TRUE };

  next (goat) := case
    ferryman = goat & next (carry) = g: next (ferryman);
    TRUE: goat;
  esac;

  next (cabbage) := case
    ferryman = cabbage & next (carry) = c: next (ferryman);
    TRUE: cabbage;
  esac;

  next (wolf) := case
    ferryman = wolf & next (carry) = w: next (ferryman);
    TRUE: wolf;
  esac;

TRANS
  (next(carry) = n) |
  (ferryman = goat & next(carry) = g) |
  (ferryman = cabbage & next(carry) = c) |
  (ferryman = wolf & next(carry) = w);

LTLSPEC
  !( ((goat = cabbage | goat = wolf) -> goat = ferryman)
      U (cabbage & goat & wolf & ferryman) )