-- A solution to the "man wolf goat cabbage" problem --
-- Prepared by Ganesh, CS 6110, Spring 2011          --

Var
 wolf 	: Boolean;
 goat	: Boolean;
 cabbage: Boolean;
 boat	: Boolean;

Function safe(boat:boolean; wolf:boolean;
	      goat:boolean; cabbage:boolean):boolean;
Begin
 return
  !(!boat & wolf & goat |
    !boat & goat & cabbage |
    boat & !wolf & !goat |
    boat & !goat & !cabbage);
End;

Startstate
 boat	:= false; -- man with boat always
 wolf 	:= false; -- left bank
 goat	:= false;
 cabbage:= false;
Endstartstate;

Rule "boat"
 safe(boat, wolf, goat, cabbage)
 &
 safe(!boat, wolf, goat, cabbage)
 ==>
 boat := !boat;
Endrule;

Rule "boat + wolf"
 safe(boat, wolf, goat, cabbage)
 &
 (boat=wolf)
 &
 safe(!boat, !wolf, goat, cabbage)
 ==>
 boat := !boat;
 wolf := !wolf;
Endrule;

Rule "boat + goat"
 safe(boat, wolf, goat, cabbage)
 &
 (boat=goat)
 &
 safe(!boat, wolf, !goat, cabbage)
 ==>
 boat := !boat;
 goat := !goat;
Endrule;

Rule "boat + cabbage"
 safe(boat, wolf, goat, cabbage)
 &
 (boat=cabbage)
 &
 safe(!boat, wolf, goat, !cabbage)
 ==>
 boat := !boat;
 cabbage := !cabbage;
Endrule;

Invariant
!(boat & wolf & goat & cabbage);

--
-- mu mwgc.m
-- 
-- ===========================================================================
-- Caching Murphi Release 5.4.4
-- Finite-state Concurrent System Compiler.
-- 
-- Caching Murphi Release 5.4.4 is based on Murphi release 3.1.
-- Caching Murphi Release 5.4.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.
-- ===========================================================================
-- 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 compiled date: Jan  8 2011
-- ===========================================================================
-- Code generated in file mwgc.cpp
-- [ganesh@line-ganesh mux]$ make mwgc
-- g++  -ggdb -o mwgc mwgc.cpp -I../../include -lm
-- 
-- [ganesh@line-ganesh mux]$ mwgc -tv
-- 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: Jan  8 2011
-- Include files last modified date:    Feb 03 2010
-- ==========================================================================
-- 
-- ==========================================================================
-- Caching Murphi Release 5.4.4
-- Finite-state Concurrent System Verifier.
-- 
-- Caching Murphi Release 5.4.4 is based on various versions of Murphi.
-- Caching Murphi Release 5.4.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: mwgc
-- 
-- 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 32 bits (rounded up to 8 bytes).
-- 	* The memory allocated for the hash table and state queue is
-- 	  8 Mbytes.
-- 	  With two words of overhead per state, the maximum size of
-- 	  the 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.inc
-- 	     to increase this, if necessary.
-- 
-- The following is the error trace for the error:
-- 
-- 	Invariant "Invariant 0" failed.
-- 
-- Startstate Startstate 0 fired.
-- wolf:false
-- goat:false
-- cabbage:false
-- boat:false
-- ----------
-- 
-- Rule boat + goat fired.
-- goat:true
-- boat:true
-- ----------
-- 
-- Rule boat fired.
-- boat:false
-- ----------
-- 
-- Rule boat + cabbage fired.
-- cabbage:true
-- boat:true
-- ----------
-- 
-- Rule boat + goat fired.
-- goat:false
-- boat:false
-- ----------
-- 
-- Rule boat + wolf fired.
-- wolf:true
-- boat:true
-- ----------
-- 
-- Rule boat fired.
-- boat:false
-- ----------
-- 
-- Rule boat + goat fired.
-- The last state of the trace (in full) is:
-- wolf:true
-- goat:true
-- cabbage:true
-- boat:true
-- ----------
-- 
-- End of the error trace.
-- 
-- ==========================================================================
-- 
-- Result:
-- 
-- 	Invariant "Invariant 0" failed.
-- 
-- State Space Explored:
-- 
-- 	10 states, 18 rules fired in 0.10s.
--=================================================================