==========================================================================

MPI Port of Parallel Murphi - Alpha Version 0.1

Responsible for this release: Hemanthkumar Sivaraj (hemanth@cs.utah.edu)
Responsible for the original parallel Murphi: Ulrich Stern 
(uli@verify.stanford.edu)
								
==========================================================================

This distribution is the MPI port of Parallel Murphi. The original parallel
murphi was developed at Stanford by Ulrich Stern. It used Berkeley Active 
Messages for message passing. Here, we have ported it to use the MPI message 
passing layer. The code is designed to run on a distributed memory machine 
with MPI installed on it, typically a network of workstations. We typically 
use it on a set of workstations connected by a 100Mbps LAN.

The implementation of MPI we have ported to is the MPICH implementation from
Argonne National Laboratories, version 1.2.2.2.

This distribution comes along with a Murphi executable for the x86 platform.
More specifically, it was compiled using:
g++ version 2.95.3 on FreeBSD 4.3 for x86 platform.
You may have to recompile the murphi executable for your architecture. Please
refer to the Readme file in the 'src' directory for that.

Typical steps for a model checking run are (taking ldash as the example):

1. Construct the model checker source (.C file) from the specification (.m
file). From the 'ex' directory, do:

> mu -p ldash.m	

This creates ldash.C, the source for the model checker.

2. Create the model checker executable.

> make -f Makefile.MPI ldash

This uses mpiCC instead of CC to compile. ldash is the executable created.

3. Use mpirun to execute the parallel model checking run. Typically, it is
something like:

> mpirun -np <number of nodes> -machinefile <file containing names of nodes to use> 
			ldash <runtime args>

===================================================================================