Installation:

For using MMC, the XSB system (version 2.0 or higher) must be installed first. XSB is a full-fledged Prolog system extended with tabled resolution, and is available for many platforms including Unix (SunOS, Solaris, HPUX, Linux, IRIX, etc.), Windows 95, and Windows NT. To obtain a free copy of XSB and associated documentation (including installation notes) see http://xsb.sourceforge.net.

The MMC system release consists of source files and examples in tarred, compressed (gzip) form. Once unpacked, the MMC system will contain two directories: mona_mmc/: the model checker for the monadic pi-calculus and poly_mmc/: the model checker for the polyadic pi-calculus. Both directories contain the following files and directories: System/: source programs for the MMC model checker; Examples/: a collection of example specifications Readme.txt plain-text version of this file; util/: short-cut for running the model checker; and install.sh: installation script.

MMC is implemented starting from a simple specification of the SOS semantics of the pi-calculus and modal mu-calculus as logic programs, (see files System/piopt.P and System/mucalculus.P). The file System/mmc.P contains the top-level code for the MMC system. To install the MMC system, first unpack the tarball using 

   tar zxvf mmc.tar.gz
or 
   gunzip -c mmc.tar.gz | tar xvf -
This will create a directory mmc which contains install.sh. Simply run ./install.sh to install the MMC system; the script will prompt you the full path name of the XSB executable. At the end of the installation, the script will give you an option to send the installation summary by email, along with a user registration. Registered users will be informed of major MMC releases and bug fixes.

Usage Notes:

	$ mmc
	xsb_configuration loaded]
	[sysinitrc loaded]
	[packaging loaded]

	XSB Version 2.5 (Okocim) of March 11, 2002
	[i686-pc-linux-gnu; mode: optimal; engine: slg-wam; gc: indirection; scheduling: batched]


	Evaluating command line goal:
	| ?-  consult('/home/pyang/mmc/mmc1.0/mona_mmc/System/mmc').
	[mmc loaded]
	[piopt2 loaded]
	[mucalculus loaded]

	yes
	|- ['../Examples/handover'].
	[Compiling ../Examples/handover]
	[handover compiled, cpu time used: 0.1600 seconds]
	[handover loaded]

	yes
	| ?- mck(system,deadlock).

	no
	| ?- halt.
	     ^^^^^
	End XSB (cputime 1.10 secs, elapsetime 125.61 secs)
	$
For measuring the time taken to modelcheck or the space consumed, you can use XSB's builtin predicates cputime(_) and statisitics. Please see XSB manual for usage notes on these builtins.

Please send comments about the MMC system, suggestions for improvements, and bug reports to pyang@cs.sunysb.edu.