This program should be regarded as a DEBUGGING aid, not as a 
certifier of correctness.
Call with the -l flag or read the license file for terms
and conditions of use.
Run this program with "-h" for the list of options.

Bugs, questions, and comments should be directed to
"murphi@verify.stanford.edu".

Murphi compiler last modified date: Jan 29 1999
Include files   last modified date: Jan 29 1999
==========================================================================

==========================================================================
Murphi Release 3.1
Finite-state Concurrent System Verifier.

Copyright (C) 1992 - 1999 by the Board of Trustees of
Leland Stanford Junior University.

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

Protocol: chap

Algorithm:
	Verification by breadth first search.
	with symmetry algorithm 3 -- Heuristic Small Memory Normalization
	with permutation trial limit 10.

Memory usage:

	* The size of each state is 354 bits (rounded up to 48 bytes).
	* The memory allocated for the hash table and state queue is
	  104 Mbytes.
	  With two words of overhead per state, the maximum size of
	  the state space is 2001101 states.
	   * Use option "-k" or "-m" to increase this, if necessary.
	* Capacity in queue for breadth-first search: 200110 states.
	   * Change the constant gPercentActiveStates in mu_prolog.inc
	     to increase this, if necessary.

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

Status:

	No error found.

State Space Explored:

	426 states, 670 rules fired in 0.18s.

Analysis of State Space:

	There are rules that are never fired.
	If you are running with symmetry, this may be why.  Otherwise,
	please run this program with "-pr" for the rules information.
	The maximum size for the multiset "net" is: 1.
	The maximum size for the multiset "int[IntruderId_1].messages" is: 3.