== Spin ==
[http://spinroot.com/spin/whatispin.html 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 [http://spinroot.com/spin/Man/README.html 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

== Cudd ==
The [https://davidkebo.com/cudd CUDD Tutorials] detail various ways to get CUDD with the easiest being the [https://davidkebo.com/source/cudd_versions/cudd-3.0.0.tar.gz CUDD 3.0.0] direct link. There is also a [https://github.com/ivmai/cudd 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.
=== Graphviz ===

Install [http://www.graphviz.org 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).