This is a model checker and a paper about Norm Compliance logic.
The file manual-simple-example.pdf contains documentation of the model checker, along with an example that illustrates usage. This PDF file is generated with LaTeX from manual-simple-example.lhs file, which is a Literate Haskell program and can be interpreted with GHCi.