CPSC 513: Introduction to Formal Verification (2008-2009)

Links for the Murphi Components of Homework 2

• Code stopsign.m for the stopsign protocol.
• Murphi is an old software package, so it can sometimes be frustrating getting it to work because of incompatibilities between current C++ compilers and the Murphi source, as well as the fact that it relies on numerous include files. The basic process is to take a Murphi file (with the ".m" extension), compile it using the Murphi compiler to a C++ program (with the ".C" extension) and then compile it using g++ (or some other C++ compiler) to an executable (with no extension on *nix machines, or with a ".exe" extension in Windows). The executable performs the actual verification for your problem.
• The Murphi package is installed in the directory /isd/users/software/Murphi3.1/ on the departmental machines. On a departmental Linux machine (I used mongoose.cs.ubc.ca) you can compile your Murphi code to C++. For example, you can copy the file /isd/users/software/Murphi3.1/ex/toy/down.m to your own directory, and then use the command "/isd/users/software/Murphi3.1/bin/mu down.m" to produce down.C.
• Once Murphi produces C++ code, you need to compile it to an executable. On a departmental Linux machine I was able to compile the down.C example using the command "g++ -DCATCH_DIV -o down down.C -I/isd/users/software/Murphi3.1/include/ -lm -Wno-deprecated".
• You can then run the resulting executable to perform model checking. To see all the possible flags for the executable, use the -h flag; for example, the command "./down -h" shows the flags available for the example executable created by the commands above. A flag that you will probably want to use is -td, which generates a trace if an error is detected.
• While I was able to compile the Murphi code to C++ on the departmental Sun machines (such as cascade.cs.ubc.ca), I was not able to compile the resulting C++ code; it appears that there is some kind of compiler/library issues with our version of Solaris. Just use a Linux machine.
• You can also download the Murphi package for your own machine from the University of Utah archive (choose the "Standard Murphi"). I was able to get it running on my home WindowsXP machine with Cygwin and g++ (modulo a few deprecation warnings).
• For more details on how to use Murphi, consult the Murphi user's manual, which can be found in /isd/users/software/Murphi3.1/doc/ or the download package linked above.

Back to CPSC 513 Home Page.