Spin is one of the most stable and useable model checkers to date. It is relatively easy to install, and it has a graphical interface for those less accustomed to the command line. If you are using Mac OSX, then the easiest way to install Spin is with homebrew: brew install spin.

Otherwise, follow the directions on the spin website to download and install Spin (Linux or Mac OSX are highly recommended though Cycwin on windows works well too). Here are a few notes that might be helpful:

• You do not need to be root to install Spin
• On the command line, when you go to test Spin, if you are getting command not found, then try to add . before the command to search the current directory as the current directly may not be in your search path: ./spin

When you have Spin built and working, here are the most important commands:

• spin -n <some number> <promela file>: random simulation of the promela file using <some number> as the random seed (makes the execution deterministic.
• You may put in your Promela file printf commands. These will output when you run in simulation above as in the previous bullet. It is a great way to printf-debug your Promela mode.
• spin -run <file>.pml or spin -search <file>.pml will model check your Promela model. If you have more than one ltl property specified, then spin -run -ltl <property-name> <file>.pml lets you name the property to verify.
• If spin finds a error in model checking mode, then spin -p -t <file>.pml will display the error trace with line number.
• Fairness constraints are added with an implication on your property: ltl p0 {<fair-path-property> → <property-to-verify>}.
• Always check the left side of any implication to be sure it exists. For example, ltl p1 {!<fair-path-property>}, should report an error. That means a fair path exists in the model so the implication is not vacuously true.
• Always try to modify your model to make your property pass and fail. That way you are absolutely ensured that your model is doing what you think it is doing.
• If you want to use a specific program location in an ltl-property, then you can use remoterefs. See the SPIN manual page for details. To map control locations to line numbers, you need to generate a pan program, and run pan -d (see below).

Older more esoteric way to have spin do the model checking (I generally do not use this interface).

• spin -a <file>.pml: generates a pan.c file which is a model checker just for your Promela model <file>.pml
• gcc pan.c -o <file> : builds the model checker executable for your Promela model.
• ./<file> -a : checks for accepting cycles
• ./<file -a -N <name>: indicates the property you want to check if multiple LTL properties are in the file

The CUDD Tutorials detail various ways to get CUDD with the easiest being the CUDD 3.0.0 direct link. There is also a GitHub CUDD 3.0.0 snapshot for cloning.

For the OS X build, I did the following:

$ ./configure CC=clang CXX=clang++
$ make
...
$ make check

All the tests should pass.

Since most likely you do _not_ have install privileges, then you can do the following to add the header and libs into single directories.

$ cd cudd-3.0.0
$ mkdir lib
$ cd lib
$ ln -s ../cudd/.libs/libcudd.a . 
$ ln -s ../cplusplus/.libs/libobj.a .
$ cd ..
$ mkdir include
$ cd include
$ ln -s ../cplusplus/cuddObj.hh . 
$ ln -s ../cudd/cudd.h .

You should be able to use -I and -L to set the include and library path to CUDD.

$ clang++ -g -Wall -D USE_CUDD -std=c++0x -I/Users/egm/Documents/cudd-3.0.0/include -c mutex-one-bdd.cc
$ clang++ -g -Wall -D USE_CUDD -std=c++0x mutex-one-bdd.o -o mutex-one-bdd -L/Users/egm/Documents/cudd-3.0.0/lib -lobj -lcudd 

If you are having linking errors, then be sure you are using the same std library as CUDD is using in its build.

Install Graphviz to visualize BDDs. Once it is installed, Cudd::DumpDot will generate DOT files. These files are converted to PDF with

$ dot -Tpdf -o file.pdf file.dot

Please note that CUDD uses complement edges. These are depicted as doted lines as opposed to long-dash lines. You have to traverse from the label to the root node as that edge may be a complement edge. In the BDD, the complement edge has the same meaning as the dashed edge: set the variable low. Additionally, the complement edge tells you if you need to complement the terminal when you reach the terminal. If the path being considered from the function label includes an ever number of complement edges, then the terminal is unchanged. If the path from the function label being considered includes an odd number of complement edges, then the terminal is complimented (i.e., terminal one with an even number of compliment edges in the path and terminal zero with an odd number of edges in the path).