Add an (as yet unimplemented) option to Prism to store the vector of results during model checking.

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

prism/src/explicit/StateModelChecker.java

@@ -85,6 +85,9 @@ public class StateModelChecker extends PrismComponent
 
 	// Additional flags/settings not included in PrismSettings
 
+	// Store the final results vector after model checking?
+	protected boolean storeVector = false;
+	
 	// Generate/store a strategy during model checking?
 	protected boolean genStrat = false;
 
@@ -192,6 +195,14 @@ public class StateModelChecker extends PrismComponent
 		this.verbosity = verbosity;
 	}
 
+	/**
+	 * Specify whether or not to store the final results vector after model checking.
+	 */
+	public void setStoreVector(boolean storeVector)
+	{
+		this.storeVector = storeVector;
+	}
+
 	/**
 	 * Specify whether or not a strategy should be generated during model checking.
 	 */
@@ -215,6 +226,14 @@ public class StateModelChecker extends PrismComponent
 		return verbosity;
 	}
 
+	/**
+	 * Whether or not to store the final results vector after model checking.
+	 */
+	public boolean getStoreVector()
+	{
+		return storeVector;
+	}
+
 	/**
 	 * Whether or not a strategy should be generated during model checking.
 	 */
@@ -271,7 +290,11 @@ public class StateModelChecker extends PrismComponent
 		
 		// Wrap a filter round the property, if needed
 		// (in order to extract the final result of model checking) 
-		expr = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumInitialStates() == 1);
+		ExpressionFilter exprFilter = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumInitialStates() == 1);
+		// And if we need to store a copy of the results vector, make a note of this
+		if (storeVector) {
+			exprFilter.setStoreVector(true);
+		}
 
 		// If required, do bisimulation minimisation
 		if (doBisim) {

prism/src/parser/ast/ExpressionFilter.java

@@ -54,8 +54,11 @@ public class ExpressionFilter extends Expression
 	private boolean invisible = false;
 	// Whether or not an explanation should be displayed when model checking
 	private boolean explanationEnabled = true;
+	// Do we need to store a copy of the results vector when model checking this?
+	private boolean storeVector = false;
 	// whether this is a filter over parameters
 	private boolean param = false;
+	
 
 	// Constructors
 
@@ -127,6 +130,11 @@ public class ExpressionFilter extends Expression
 		this.explanationEnabled = explanationEnabled;
 	}
 	
+	public void setStoreVector(boolean storeVector)
+	{
+		this.storeVector = storeVector;
+	}
+	
 	public void setParam()
 	{
 		param = true;
@@ -164,6 +172,11 @@ public class ExpressionFilter extends Expression
 		return explanationEnabled;
 	}
 	
+	public boolean getStoreVector()
+	{
+		return storeVector;
+	}
+	
 	public boolean isParam()
 	{
 		return param;
@@ -257,7 +270,7 @@ public class ExpressionFilter extends Expression
 	 * @param expr Expression to be model checked
 	 * @param singleInit Does the model on which it is being checked have a single initial states? 
 	 */
-	public static Expression addDefaultFilterIfNeeded(Expression expr, boolean singleInit) throws PrismLangException
+	public static ExpressionFilter addDefaultFilterIfNeeded(Expression expr, boolean singleInit) throws PrismLangException
 	{
 		ExpressionFilter exprFilter = null;
 		
@@ -301,7 +314,8 @@ public class ExpressionFilter extends Expression
 			exprFilter.typeCheck();
 			return exprFilter;
 		} else {
-			return expr;
+			// If no new filter was created, we no expr is an ExpressionFilter
+			return (ExpressionFilter) expr;
 		}
 	}
 }

prism/src/prism/Prism.java

@@ -193,6 +193,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	protected String exportProductTransFilename = null;
 	protected boolean exportProductStates = false;
 	protected String exportProductStatesFilename = null;
+	// Store the final results vector after model checking?
+	protected boolean storeVector = false; 
 	// Generate/store a strategy during model checking?
 	protected boolean genStrat = false; 
 	// Do bisimulation minimisation before model checking?
@@ -588,6 +590,14 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		exportProductStatesFilename = s;
 	}
 
+	/**
+	 * Specify whether or not to store the final results vector after model checking.
+	 */
+	public void setStoreVector(boolean storeVector)
+	{
+		this.storeVector = storeVector;
+	}
+
 	/**
 	 * Specify whether or not a strategy should be generated during model checking.
 	 */
@@ -886,6 +896,14 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		return exportProductStatesFilename;
 	}
 
+	/**
+	 * Whether or not to store the final results vector after model checking.
+	 */
+	public boolean getStoreVector()
+	{
+		return storeVector;
+	}
+
 	/**
 	 * Whether or not a strategy should be generated during model checking.
 	 */
@@ -3461,6 +3479,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		explicit.StateModelChecker mc = explicit.StateModelChecker.createModelChecker(currentModelType, this);
 		mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile);
 		// Pass any additional local settings
+		mc.setStoreVector(storeVector);
 		mc.setGenStrat(genStrat);
 		mc.setDoBisim(doBisim);
 		

prism/src/prism/StateModelChecker.java

@@ -76,6 +76,8 @@ public class StateModelChecker implements ModelChecker
 	protected double termCritParam;
 	// Verbose mode?
 	protected boolean verbose;
+	// Store the final results vector after model checking?
+	protected boolean storeVector = false; 
 	// Generate/store a strategy during model checking?
 	protected boolean genStrat = false;
 
@@ -179,7 +181,12 @@ public class StateModelChecker implements ModelChecker
 
 		// Wrap a filter round the property, if needed
 		// (in order to extract the final result of model checking) 
-		expr = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumStartStates() == 1);
+		ExpressionFilter exprFilter = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumStartStates() == 1);
+		// And if we need to store a copy of the results vector, make a note of this
+		if (storeVector) {
+			exprFilter.setStoreVector(true);
+		}
+		expr = exprFilter;
 		
 		// Do model checking and store result vector
 		timer = System.currentTimeMillis();