                           MPI-Spin README

Spin is a popular open-source model checking tool originally developed
at Bell Labs.  To learn more about Spin, visit http://spinroot.com.

The Message Passing Interface (MPI) is a specification for a library
of message-passing functions, with bindings in C, C++, and Fortran.
There are numerous open-source and proprietary implementations of MPI.
MPI is widely used to construct high-performance parallel programs,
especially for scientific computation.  For more information on MPI,
see http://www-unix.mcs.anl.gov/mpi/ or http://www.mpi-forum.org/.

MPI-Spin is an extension to Spin that can be used to verify models of
MPI programs.  It adds to Spin's input language a number of functions,
types, and constants that correspond closely to many of the primitives
described in the MPI Standard.

MPI-Spin works with a (very slightly) modified version of Spin called
Spin-M, which comes with its own copyright and license and must be
downloaded separately.  The instructions for building and installing
MPI-Spin can be found in the file INSTALL.

MPI-Spin (but not Spin or Spin-M) is licensed under the GNU General
Public License.  In particular, MPI-Spin is distributed WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or
FITNESS FOR A PARTICULAR PURPOSE.  See the file LICENSE for details.

The examples directory contains a number of examples, complete with
Makefiles, of applications of MPI-Spin.  This is a good place to start
to learn how to use MPI-Spin.
