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
"melatti@di.uniroma1.it".CMurphi compiler last modified date: Nov 14 2017
Include files last modified date:    Sep 01 2009
====================================================================================================================================================
Caching Murphi Release 5.4
Finite-state Concurrent System Verifier.Caching Murphi Release 5.4 is based on various versions of Murphi.
Caching Murphi Release 5.4 :
Copyright (C) 2009-2012 by Sapienza University of Rome.
Murphi release 3.1 :
Copyright (C) 1992 - 1999 by the Board of Trustees of
Leland Stanford Junior University.==========================================================================Protocol: pingpongAlgorithm:Verification by breadth first search.with symmetry algorithm 3 -- Heuristic Small Memory Normalizationwith permutation trial limit 10.Memory usage:* The size of each state is 32 bits (rounded up to 8 bytes).* The memory allocated for the hash table and state queue is8 Mbytes.With two words of overhead per state, the maximum size ofthe state space is 476219 states.* Use option "-k" or "-m" to increase this, if necessary.* Capacity in queue for breadth-first search: 47621 states.* Change the constant gPercentActiveStates in mu_prolog.incto increase this, if necessary.Warning: No trace will not be printed in the case of protocol errors!Check the options if you want to have error traces.==========================================================================Status:No error found.State Space Explored:4 states, 6 rules fired in 0.10s.

在进一步演示：

gunther@ubuntu:~/cmurphi5.4/src$ ./pingpong.o  -p
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
"melatti@di.uniroma1.it".CMurphi compiler last modified date: Nov 14 2017
Include files last modified date:    Sep 01 2009
====================================================================================================================================================
Caching Murphi Release 5.4
Finite-state Concurrent System Verifier.Caching Murphi Release 5.4 is based on various versions of Murphi.
Caching Murphi Release 5.4 :
Copyright (C) 2009-2012 by Sapienza University of Rome.
Murphi release 3.1 :
Copyright (C) 1992 - 1999 by the Board of Trustees of
Leland Stanford Junior University.==========================================================================Protocol: pingpongAlgorithm:Verification by breadth first search.with symmetry algorithm 3 -- Heuristic Small Memory Normalizationwith permutation trial limit 10.Memory usage:* The size of each state is 32 bits (rounded up to 8 bytes).* The memory allocated for the hash table and state queue is8 Mbytes.With two words of overhead per state, the maximum size ofthe state space is 476219 states.* Use option "-k" or "-m" to increase this, if necessary.* Capacity in queue for breadth-first search: 47621 states.* Change the constant gPercentActiveStates in mu_prolog.incto increase this, if necessary.Warning: No trace will not be printed in the case of protocol errors!Check the options if you want to have error traces.==========================================================================
Verbose option selected.  The following is the detailed progress.Firing startstate Startstate 0, p:0
Obtained state:
Players[0].hasball:true
Players[0].gotball:false
Players[1].hasball:false
Players[1].gotball:falseFiring startstate Startstate 0, p:1
Obtained state:
Players[0].hasball:false
Players[0].gotball:false
Players[1].hasball:true
Players[1].gotball:false------------------------------
Unpacking state from queue:
Players[0].hasball:true
Players[0].gotball:false
Players[1].hasball:false
Players[1].gotball:falseThe following next states are obtained:Firing rule Pass ball, p:0
Obtained state:
Players[0].hasball:false
Players[0].gotball:false
Players[1].hasball:false
Players[1].gotball:trueFiring rule Keep ball, p:0
Obtained state:
Players[0].hasball:true
Players[0].gotball:false
Players[1].hasball:false
Players[1].gotball:false------------------------------
Unpacking state from queue:
Players[0].hasball:false
Players[0].gotball:false
Players[1].hasball:true
Players[1].gotball:falseThe following next states are obtained:Firing rule Pass ball, p:1
Obtained state:
Players[0].hasball:false
Players[0].gotball:true
Players[1].hasball:false
Players[1].gotball:falseFiring rule Keep ball, p:1
Obtained state:
Players[0].hasball:false
Players[0].gotball:false
Players[1].hasball:true
Players[1].gotball:false------------------------------
Unpacking state from queue:
Players[0].hasball:false
Players[0].gotball:false
Players[1].hasball:false
Players[1].gotball:trueThe following next states are obtained:Firing rule Get ball, p:1
Obtained state:
Players[0].hasball:false
Players[0].gotball:false
Players[1].hasball:true
Players[1].gotball:false------------------------------
Unpacking state from queue:
Players[0].hasball:false
Players[0].gotball:true
Players[1].hasball:false
Players[1].gotball:falseThe following next states are obtained:Firing rule Get ball, p:0
Obtained state:
Players[0].hasball:true
Players[0].gotball:false
Players[1].hasball:false
Players[1].gotball:false==========================================================================Status:No error found.State Space Explored:4 states, 6 rules fired in 0.10s.