added check for existence zero-reward loops

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1104 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/prism/ECComputer.java

@@ -0,0 +1,83 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
+//	* Carlos S. Bederian (Universidad Nacional de Cordoba)
+//  * Mark Kattenbelt <mark.kattenbelt@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package prism;
+
+import java.util.Vector;
+
+import jdd.*;
+
+//	interface for end-component computing classes
+
+public abstract class ECComputer
+{
+	protected Prism prism;
+	protected PrismLog mainLog;
+
+	// model info
+	protected JDDNode trans;
+	protected JDDNode trans01;
+	protected JDDNode reach;
+	protected JDDVars allDDRowVars;
+	protected JDDVars allDDColVars;
+	protected JDDVars allDDNondetVars;
+		
+	// stuff for ECs
+	protected Vector<JDDNode> vectECs;
+	protected JDDNode notInECs;
+		
+	// Constructor
+	/**
+	 * Find maximal EC of a sub-MDP by restricting reach and trans01.
+	 * This sub-MDP needs to be deadlock-free.
+	 */
+	public ECComputer(Prism prism, JDDNode reach, JDDNode trans, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars allDDNondetVars)
+	{
+		this.prism = prism;
+		mainLog = prism.getMainLog();
+		this.reach = reach;
+		this.trans = trans;
+		this.trans01 = trans01;		
+		this.allDDRowVars = allDDRowVars;
+		this.allDDColVars = allDDColVars;
+		this.allDDNondetVars = allDDNondetVars;
+	}
+	
+	// Get vector of EndComponents
+	// NB: these BDDs aren't derefed by EndComponentComputer classes
+	public Vector<JDDNode> getVectECs() { return vectECs; }
+	
+	// Get states not in any EndComponent
+	// NB: this BDD isn't derefed by SCCComputer classes
+	//public JDDNode getNotInECs() { return notInECs; }
+	
+	// End Components (EC) computation
+	// NB: This creates BDDs, obtainable from getVectECs() and getNotInECs(),
+	// which  the calling code is responsible for dereferencing.
+	public abstract void computeECs();
+}

prism/src/prism/ECComputerDefault.java

@@ -0,0 +1,187 @@
+package prism;
+
+import java.util.Stack;
+import java.util.Vector;
+
+import jdd.JDD;
+import jdd.JDDNode;
+import jdd.JDDVars;
+
+public class ECComputerDefault extends ECComputer
+{	
+	public ECComputerDefault(Prism prism, JDDNode reach, JDDNode trans, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars,
+			JDDVars allDDNondetVars)
+	{
+		super(prism, reach, trans, trans01, allDDRowVars, allDDColVars, allDDNondetVars);
+	}
+
+	public void computeECs()
+	{
+		vectECs = new Vector<JDDNode>();
+
+		boolean initialCandidate = true;
+		Stack<JDDNode> candidates = new Stack<JDDNode>();
+		JDD.Ref(reach);
+		candidates.push(reach);
+		SCCComputer sccComputer;
+
+		while (!candidates.isEmpty()) 
+		{
+			System.out.println("Checking candidate");
+			
+			JDDNode candidate = candidates.pop();
+
+			// Compute the stable set
+			JDD.Ref(candidate);
+			JDDNode stableSet = findMaximalStableSet(candidate);
+
+			System.out.println("found max stable set");
+			
+			// Drop empty sets
+			if (stableSet.equals(JDD.ZERO)) 
+			{
+				System.out.println("empty set");
+				JDD.Deref(stableSet);
+				JDD.Deref(candidate);
+				continue;
+			}
+
+			if (!initialCandidate) 
+			{
+				System.out.println("not initial");
+				
+				// candidate is an SCC, check if it's stable
+				if (stableSet.equals(candidate)) 
+				{
+					vectECs.add(maxStableSetChoices(candidate));
+					JDD.Deref(stableSet);
+					continue;
+				}
+			} 
+			else 
+			{
+				initialCandidate = false;
+			}
+			
+			JDD.Deref(candidate);
+
+			// Filter bad transitions
+			JDD.Ref(stableSet);
+			JDDNode stableSetTrans = maxStableSetTrans(stableSet);
+
+			// now find the maximal SCCs in (stableSet, stableSetTrans)
+			Vector<JDDNode> sccs;
+			sccComputer = prism.getSCCComputer(stableSet, stableSetTrans, allDDRowVars, allDDColVars);
+			sccComputer.computeSCCs();
+			JDD.Deref(stableSet);
+			JDD.Deref(stableSetTrans);
+			sccs = sccComputer.getVectSCCs();
+			JDD.Deref(sccComputer.getNotInSCCs());
+			candidates.addAll(sccs);
+		}
+	}
+	
+	/**
+	 * Returns a stable set of states contained in candidateStates
+	 * 
+	 * @param candidateStates
+	 *            set of candidate states S x H_i (dereferenced after calling this function)
+	 * @return a referenced BDD with the maximal stable set in c
+	 */
+	private JDDNode findMaximalStableSet(JDDNode candidateStates)
+	{
+		System.out.println("findMaximalStableSet");
+
+		
+		
+		JDDNode old = JDD.Constant(0);
+		JDDNode current = candidateStates;
+		
+		if (current.isConstant())
+			System.out.println("current = " + current.getValue());
+
+		while (!current.equals(old)) 
+		{
+			JDD.Deref(old);
+			JDD.Ref(current);
+			old = current;
+
+			JDD.Ref(current);
+			JDD.Ref(trans);
+			// Select transitions starting in current
+			JDDNode currTrans = JDD.Apply(JDD.TIMES, trans, current);
+			// Select transitions starting in current and ending in current
+			JDDNode tmp = JDD.PermuteVariables(current, allDDRowVars, allDDColVars);
+			tmp = JDD.Apply(JDD.TIMES, currTrans, tmp);
+			// Sum all successor probabilities for each (state, action) tuple
+			tmp = JDD.SumAbstract(tmp, allDDColVars);
+			// If the sum for a (state,action) tuple is 1,
+			// there is an action that remains in the stable set with prob 1
+			tmp = JDD.GreaterThan(tmp, 1 - prism.getSumRoundOff());
+			// Without fairness, we just need one action per state
+			current = JDD.ThereExists(tmp, allDDNondetVars);
+		}
+		JDD.Deref(old);
+		return current;
+	}
+	
+	/**
+	 * Returns the transition relation of a stable set
+	 * 
+	 * @param b
+	 *            BDD of a stable set (dereferenced after calling this function)
+	 * @return referenced BDD of the transition relation restricted to the stable set
+	 */
+	private JDDNode maxStableSetTrans(JDDNode b)
+	{
+		System.out.println("maxStableSetTrans");
+		JDD.Ref(b);
+		JDD.Ref(trans);
+		// Select transitions starting in b
+		JDDNode currTrans = JDD.Apply(JDD.TIMES, trans, b);
+		JDDNode mask = JDD.PermuteVariables(b, allDDRowVars, allDDColVars);
+		// Select transitions starting in current and ending in current
+		mask = JDD.Apply(JDD.TIMES, currTrans, mask);
+		// Sum all successor probabilities for each (state, action) tuple
+		mask = JDD.SumAbstract(mask, allDDColVars);
+		// If the sum for a (state,action) tuple is 1,
+		// there is an action that remains in the stable set with prob 1
+		mask = JDD.GreaterThan(mask, 1 - prism.getSumRoundOff());
+		// select the transitions starting in these tuples
+		JDD.Ref(trans01);
+		JDDNode stableTrans01 = JDD.And(trans01, mask);
+		// Abstract over actions
+		return JDD.ThereExists(stableTrans01, allDDNondetVars);
+	}
+	
+	/**
+	 * Returns the transition relation of a stable set
+	 * 
+	 * @param b
+	 *            BDD of a stable set (dereferenced after calling this function)
+	 * @return referenced BDD of the transition relation restricted to the stable set
+	 */
+	public JDDNode maxStableSetChoices(JDDNode b)
+	{
+		System.out.println("maxStableSetChoices");
+		
+		JDD.Ref(b);
+		JDD.Ref(trans);
+		// Select transitions starting in b
+		JDDNode currTrans = JDD.Apply(JDD.TIMES, trans, b);
+		JDDNode mask = JDD.PermuteVariables(b, allDDRowVars, allDDColVars);
+		// Select transitions starting in current and ending in current
+		mask = JDD.Apply(JDD.TIMES, currTrans, mask);
+		// Sum all successor probabilities for each (state, action) tuple
+		mask = JDD.SumAbstract(mask, allDDColVars);
+		// If the sum for a (state,action) tuple is 1,
+		// there is an action that remains in the stable set with prob 1
+		mask = JDD.GreaterThan(mask, 1 - prism.getSumRoundOff());
+		// select the transitions starting in these tuples
+		JDD.Ref(trans01);
+		JDDNode stableTrans01 = JDD.And(trans01, mask);
+		// Abstract over actions
+		return JDD.ThereExists(stableTrans01, allDDColVars);
+	}
+
+}

prism/src/prism/NondetModelChecker.java

@@ -1077,6 +1077,8 @@ public class NondetModelChecker extends NonProbModelChecker
 		DoubleVector rewardsDV;
 		StateProbs rewards = null;
 
+		Vector<JDDNode> zeroCostEndComponents = null;
+		
 		// compute states which can't reach goal with probability 1
 		if (b.equals(JDD.ZERO)) {
 			JDD.Ref(reach);
@@ -1096,6 +1098,33 @@ public class NondetModelChecker extends NonProbModelChecker
 				JDD.Ref(reach);
 				inf = JDD.And(reach, JDD.Not(prob1));
 			} else {
+				
+				if (prism.getCheckZeroLoops())
+				{
+					// find states transitions that have no cost
+					JDD.Ref(sr);
+					JDD.Ref(reach);
+					JDDNode zeroReach = JDD.And(reach, JDD.Apply(JDD.EQUALS, sr, JDD.Constant(0)));
+					JDD.Ref(b);
+					zeroReach = JDD.And(zeroReach, JDD.Not(b));
+					JDD.Ref(trr);
+					JDDNode zeroTrr = JDD.Apply(JDD.EQUALS, trr, JDD.Constant(0));
+					JDD.Ref(trans);
+					JDD.Ref(zeroTrr);
+					JDDNode zeroTrans = JDD.And(trans, zeroTrr);
+					JDD.Ref(trans01);
+					JDDNode zeroTrans01 = JDD.And(trans01, zeroTrr);
+						
+					ECComputer ecComp = new ECComputerDefault(prism, zeroReach, zeroTrans, zeroTrans01, model.getAllDDRowVars(), model.getAllDDColVars(), model.getAllDDNondetVars());
+					ecComp.computeECs();
+					
+					zeroCostEndComponents =  ecComp.getVectECs();
+									
+					JDD.Deref(zeroReach);
+					JDD.Deref(zeroTrans);				
+					JDD.Deref(zeroTrans01);				
+				}
+				
 				// compute states for which all adversaries don't reach goal with probability 1
 				no = PrismMTBDD.Prob0A(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, reach, b);
 				prob1 = PrismMTBDD.Prob1E(tr01, reach, allDDRowVars, allDDColVars, allDDNondetVars, reach, b, no);
@@ -1109,8 +1138,15 @@ public class NondetModelChecker extends NonProbModelChecker
 			maybe = JDD.And(reach, JDD.Not(JDD.Or(inf, b)));
 		}
 
-		// need to deal with zero loops yet
-		if (min) {
+		if (prism.getCheckZeroLoops())
+		{
+			// need to deal with zero loops yet
+			if (min && zeroCostEndComponents != null && zeroCostEndComponents.size() > 0) {
+				mainLog.println("\nWarning: PRISM detected your model contains " +  zeroCostEndComponents.size() + " zero-reward " + ((zeroCostEndComponents.size() == 1) ? "loop." : "loops."));
+				mainLog.println("Your minimum rewards may be too low...");
+			}
+		}
+		else if (min) {
 			mainLog.println("\nWarning: PRISM hasn't checked for zero-reward loops.");
 			mainLog.println("Your minimum rewards may be too low...");
 		}
@@ -1156,6 +1192,11 @@ public class NondetModelChecker extends NonProbModelChecker
 				throw e;
 			}
 		}
+		
+		if (zeroCostEndComponents != null) 
+			for (JDDNode zcec : zeroCostEndComponents)
+				JDD.Deref(zcec);
+		
 
 		// derefs
 		JDD.Deref(inf);

prism/src/prism/Prism.java

@@ -99,6 +99,7 @@ public class Prism implements PrismSettingsListener
 	
 	private boolean doReach;	// do reachability? (sometimes might want to skip it)
 	private boolean bsccComp;	// do bscc computation before steady-state?
+	private boolean checkZeroLoops;
 	
 	// MTBDD construction method (NOW DEFUNCT)
 	//  1 - use with ordering 1: nondet vars form a tree at the top
@@ -143,6 +144,8 @@ public class Prism implements PrismSettingsListener
 	//------------------------------------------------------------------------------
 	
 	private boolean cuddStarted = false;
+
+	
 	
 	//------------------------------------------------------------------------------
 	// methods
@@ -179,6 +182,7 @@ public class Prism implements PrismSettingsListener
 		// default values for miscellaneous options 
 		doReach = true;
 		bsccComp = true;
+		checkZeroLoops = false;
 		construction = 3;
 		ordering = 1;
 		sumRoundOff = 1e-5;
@@ -1508,6 +1512,16 @@ public class Prism implements PrismSettingsListener
 	{
 		return settings;
 	}
+
+	public void setCheckZeroLoops(boolean checkZeroLoops)
+	{
+		this.checkZeroLoops  = checkZeroLoops;		
+	}
+
+	public boolean getCheckZeroLoops()
+	{
+		return this.checkZeroLoops;
+	}		
 }
 
 //------------------------------------------------------------------------------

prism/src/prism/PrismCL.java

@@ -255,28 +255,27 @@ public class PrismCL
 						error(e.getMessage());
 					}
 				}
-				
-				// export labels/states
-				if (exportlabels) {
-					try {
-						if (propertiesFile != null) {
-							definedPFConstants = undefinedConstants.getPFConstantValues();
-							propertiesFile.setUndefinedConstants(definedPFConstants);
-						}
-						File f = (exportLabelsFilename.equals("stdout")) ? null : new File(exportLabelsFilename);
-						prism.exportLabelsToFile(model, modulesFile, propertiesFile, exportType, f);
-					}
-					// in case of error, report it and proceed
-					catch (FileNotFoundException e) {
-						mainLog.println("Couldn't open file \"" + exportLabelsFilename + "\" for output");
-					}
-					catch (PrismException e) {
-						mainLog.println("\nError: " + e.getMessage() + ".");
+			}
+			
+			// export labels/states
+			if (exportlabels) {
+				try {
+					if (propertiesFile != null) {
+						definedPFConstants = undefinedConstants.getPFConstantValues();
+						propertiesFile.setUndefinedConstants(definedPFConstants);
 					}
+					File f = (exportLabelsFilename.equals("stdout")) ? null : new File(exportLabelsFilename);
+					prism.exportLabelsToFile(model, modulesFile, propertiesFile, exportType, f);
+				}
+				// in case of error, report it and proceed
+				catch (FileNotFoundException e) {
+					mainLog.println("Couldn't open file \"" + exportLabelsFilename + "\" for output");
+				}
+				catch (PrismException e) {
+					mainLog.println("\nError: " + e.getMessage() + ".");
 				}
 			}
 			
-			
 			// work through list of properties to be checked
 			for (j = 0; j < numPropertiesToCheck; j++) {
 				
@@ -1122,6 +1121,10 @@ public class PrismCL
 				else if (sw.equals("o2")) {
 					prism.setOrdering(2);
 				}
+				// zero-reward loops check on
+				else if (sw.equals("zerorewardcheck")) {
+					prism.setCheckZeroLoops(true);
+				}
 				// reachability off
 				else if (sw.equals("noreach")) {
 					prism.setDoReach(false);
@@ -1589,6 +1592,7 @@ public class PrismCL
 		mainLog.println("-fixdl ......................... Automatically put self-loops in deadlock states");
 		mainLog.println("-nocompact ..................... Switch off \"compact\" sparse storage schemes");
 		mainLog.println("-noprobchecks .................. Disable checks on model probabilities/rates");
+		mainLog.println("-zerorewardchecks .............. Check for absence of zero-reward loops");
 		mainLog.println("-nossdetect .................... Disable steady-state detection for CTMC transient computations");
 		mainLog.println("-sccmethod <name> .............. Specify SCC computation method (xiebeerel, lockstep, sccfind)");
 		mainLog.println();