SMurphi is an extended version of the
Murphi
verifier (version 3.1).
It includes three new symmetry reduction algorithms
explained in the report:
-
Tommi Junttila.
Symmetry Reduction Algorithms for Data Symmetries.
Research Report A72,
Helsinki University of Technology,
Laboratory for Theoretical Computer Science,
Espoo, Finland, May 2002.
Gzipped postscript
(988 Kb).
PDF (834 Kb).
Bibtex Entry.
The source code for SMurphi is available here.
In order to use all the new algorithms,
you also need the nauty tool
(version 2.0 beta 9 was used in obtaining the experimental results
in the paper above).
After compiling the SMurphi program,
there are two ways for compiling Murphi descriptions (files ending with ".m")
depending whether the nauty tool is available or not.
Without nauty,
the following procedure is used:
mu FILE.m
g++ -c FILE.C -I[SMURPHIPATH]/include
g++ -o FILE FILE.o
where [SMURPHIPATH] is the path to the SMurphi directory.
With nauty,
the following procedure is used:
mu FILE.m
g++ -c FILE.C -I[SMURPHIPATH]/include -DTJ_NAUTY -I[NAUTYPATH]
g++ -o FILE FILE.o [NAUTYPATH]/nautil.o [NAUTYPATH]/nauty.o
where [NAUTYPATH] is the directory for nauty.
After compiling the Murphi description FILE.m into the executable file FILE,
type FILE -h for the available options.
The new symmetry reduction algorithms are the numbers 5, 6, and 7.