Source code and binaries for NuSMV are available at http://nusmv.fbk.eu.

Start NuSMV in interactive mode:
  NuSMV -int
Whenever you want to read a new model, enter the "reset" command first.

CTL EXAMPLE
-----------
To check Exercise 2:
  read_model -i example2.txt
  go
  print_reachable_states -v
  check_ctlspec

LTL EXAMPLE
-----------
To verify that the ferryman can bring goat, wolf, and cabbage to the other side:
  read_model -i ferryman.txt
  go
  print_reachable_states -v
  check_ltlspec