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:
When you have Spin built and working, here are the most important commands:
Older more esoteric way to have spin do the model checking (I generally do not use this interface).
The newest version of [ftp://vlsi.colorado.edu/pub/cudd-3.0.0.tar.gz CUDD] includes a configure script. 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.dotPlease note that CUDD uses complement edges. These are depicted as short-dash lines as opposed to long-dash lines. If you traverse each time you traverse a complement edge on the way to the terminal, you complement that terminal. Thus, an even number of complement edges leaves the terminal unchanged (i.e., terminal one) while an odd number of complement edges flips the terminal to zero.