This is a simple introduction to model checking, written in literate Haskell. See src/ModelChecking*.lhs. The build.sh script runs cabal build to compile the code, and builds documentation using pandoc.