More improvements to output of results of model checking.

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

prism/src/prism/Result.java

@@ -34,15 +34,27 @@ package prism;
 public class Result
 {
 	private Object result = null;
+	private String resultString = "";
 	
 	public Result()
 	{
 		this.result = null;
+		this.resultString = "";
 	}
 	
 	public Result(Object result)
 	{
 		this.result = result;
+		if (result instanceof Exception)
+				this.resultString = "Error: "+((Exception)result).getMessage();
+		else
+				this.resultString = ""+result;
+	}
+	
+	public Result(Object result, String resultString)
+	{
+		this.result = result;
+		this.resultString = resultString;
 	}
 	
 	public Object getResult()
@@ -50,8 +62,18 @@ public class Result
 		return result;
 	}
 
-	public void setResult(Object result)
+	public String getResultString()
 	{
-		this.result = result;
+		return resultString;
+	}
+
+	public void setResultString(String resultString)
+	{
+		this.resultString = resultString;
+	}
+	
+	public String toString()
+	{
+		return resultString;
 	}
 }

prism/src/prism/StateListMTBDD.java

@@ -210,8 +210,9 @@ public class StateListMTBDD implements StateList
 		varValues[currentVar] -= (1 << (varSizes[currentVar]-1-currentVarLevel));
 	}
 
-	// check for state inclusion (state given by bdd)
-	
+	/**
+	 * Check for (partial) state inclusion - state(s) given by BDD
+	 */
 	public boolean includes(JDDNode state)
 	{
 		JDDNode tmp;
@@ -226,6 +227,23 @@ public class StateListMTBDD implements StateList
 		return incl;	
 	}
 
+	/**
+	 * Check for (full) state inclusion - state(s) given by BDD
+	 */
+	public boolean includesAll(JDDNode state)
+	{
+		JDDNode tmp;
+		boolean incl;
+		
+		JDD.Ref(states);
+		JDD.Ref(state);
+		tmp = JDD.And(states, state);
+		incl = tmp.equals(state);
+		JDD.Deref(tmp);
+		
+		return incl;	
+	}
+
 	// get first state as Values object
 	
 	public Values getFirstAsValues() throws PrismException

prism/src/prism/StateModelChecker.java

@@ -59,7 +59,7 @@ public class StateModelChecker implements ModelChecker
 	protected JDDVars[] varDDRowVars;
 
 	// Options:
-	
+
 	// Which engine to use
 	protected int engine;
 	// Parameter for termination criterion
@@ -112,27 +112,17 @@ public class StateModelChecker implements ModelChecker
 		long timer = 0;
 		JDDNode ddFilter = null, tmp;
 		StateListMTBDD states;
-		boolean b;
 		StateProbs vals;
-		Object res;
 		String resultString;
 		double minRes = 0.0, maxRes = 0.0;
-		Result ret;
-		
+		Result res;
+
 		// Filters are only allowed for non-Boolean properties
 		if (expr.getType() == Expression.BOOLEAN && filter != null) {
 			throw new PrismException("Filters cannot be applied to Boolean-valued properties");
 		}
-		
+
 		// Translate filter (if present)
-		if (filter == null) {//TODO: remove
-			filter = new Filter(new ExpressionLabel("init"));
-			if (model.getNumStartStates() > 1) {
-				mainLog
-						.print("\nWarning: There are multiple initial states; the result of model checking is for the first one: ");
-				model.getStartStates().print(mainLog, 1);
-			}
-		}
 		if (filter != null) {
 			ddFilter = checkExpressionDD(filter.getExpression());
 			if (ddFilter.equals(JDD.ZERO)) {
@@ -146,16 +136,20 @@ public class StateModelChecker implements ModelChecker
 		timer = System.currentTimeMillis() - timer;
 		mainLog.println("\nTime for model checking: " + timer / 1000.0 + " seconds.");
 
-		// Process results of model checking using filter
+		// Process results of model checking - depends on type
+
+		// Boolean results
 		if (expr.getType() == Expression.BOOLEAN) {
 
+			// Convert to StateList object
 			states = new StateListMTBDD(((StateProbsMTBDD) vals).getJDDNode(), model);
 			JDD.Ref(((StateProbsMTBDD) vals).getJDDNode());
-			
-			boolean satAll = states.includes(reach);
-			boolean satInit = states.includes(start);
-			
-			// print out number of satisfying states
+
+			// See if satisfied in all/initial states
+			boolean satAll = states.includesAll(reach);
+			boolean satInit = states.includesAll(start);
+
+			// Print number of satisfying states to log
 			mainLog.print("\nNumber of satisfying states: ");
 			mainLog.print(states.size());
 			if (satAll) {
@@ -169,7 +163,7 @@ public class StateModelChecker implements ModelChecker
 			}
 			mainLog.print("\n");
 
-			// if "verbose", print out satisfying states
+			// If in "verbose" mode, print out satisfying states to log
 			if (verbose) {
 				mainLog.print("\nSatisfying states:");
 				if (states.size() > 0) {
@@ -180,74 +174,88 @@ public class StateModelChecker implements ModelChecker
 				}
 			}
 
-			// result is true if all states satisfy, false otherwise
-			b = satAll;
-			res = b ? new Boolean(true) : new Boolean(false);
+			// Result is true if all states satisfy, false otherwise
+			resultString = satAll + " (property " + (satAll ? "" : "not ") + "satisfied in all states)";
+			res = new Result(satAll ? new Boolean(true) : new Boolean(false), resultString);
+
+			// Print result to log
+			mainLog.print("\nResult: " + resultString + "\n");
+
+			// Clean up
 			states.clear();
+		}
 
-			// print result
-			mainLog.print("\nResult: " + b + " (property " + (b ? "" : "not ") + "satisfied in all states)\n");
-		} else {
-			if (filter.minRequested()) {
-				minRes = vals.minOverBDD(ddFilter);
-				mainLog.print("\nMinimum value for states satisfying " + filter.getExpression() + ": " + minRes
-						+ "\n");
-				tmp = vals.getBDDFromInterval(minRes - termCritParam, minRes + termCritParam);
-				JDD.Ref(ddFilter);
-				tmp = JDD.And(tmp, ddFilter);
-				states = new StateListMTBDD(tmp, model);
-				mainLog.print("There are " + states.size() + " states with this minimum value (+/- "
-						+ termCritParam + ")");
-				if (!verbose && states.size() > 10) {
-					mainLog.print(".\nThe first 10 states are displayed below. To view them all, use verbose mode.\n");
-					states.print(mainLog, 10);
-				} else {
-					mainLog.print(":\n");
-					states.print(mainLog);
+		// Non-Boolean results
+		else {
+			if (filter == null) {
+				if (model.getNumStartStates() > 1) {
+					mainLog.print("\nWarning: There are multiple initial states;");
+					mainLog.print(" the result of model checking is for the first one: ");
+					model.getStartStates().print(mainLog, 1);
 				}
-				JDD.Deref(tmp);
-			}
-			if (filter.maxRequested()) {
-				maxRes = vals.maxOverBDD(ddFilter);
-				mainLog.print("\nMaximum value for states satisfying " + filter.getExpression() + ": " + maxRes
-						+ "\n");
-				tmp = vals.getBDDFromInterval(maxRes - termCritParam, maxRes + termCritParam);
-				JDD.Ref(ddFilter);
-				tmp = JDD.And(tmp, ddFilter);
-				states = new StateListMTBDD(tmp, model);
-				mainLog.print("There are " + states.size() + " states with this maximum value (+/- "
-						+ termCritParam + ")");
-				if (!verbose && states.size() > 10) {
-					mainLog.print(".\nThe first 10 states are displayed below. To view them all, use verbose mode.\n");
-					states.print(mainLog, 10);
-				} else {
-					mainLog.print(":\n");
-					states.print(mainLog);
+			} else {
+				if (filter.minRequested()) {
+					minRes = vals.minOverBDD(ddFilter);
+					mainLog.print("\nMinimum value for states satisfying " + filter.getExpression() + ": " + minRes
+							+ "\n");
+					tmp = vals.getBDDFromInterval(minRes - termCritParam, minRes + termCritParam);
+					JDD.Ref(ddFilter);
+					tmp = JDD.And(tmp, ddFilter);
+					states = new StateListMTBDD(tmp, model);
+					mainLog.print("There are " + states.size() + " states with this minimum value (+/- "
+							+ termCritParam + ")");
+					if (!verbose && states.size() > 10) {
+						mainLog
+								.print(".\nThe first 10 states are displayed below. To view them all, use verbose mode.\n");
+						states.print(mainLog, 10);
+					} else {
+						mainLog.print(":\n");
+						states.print(mainLog);
+					}
+					JDD.Deref(tmp);
+				}
+				if (filter.maxRequested()) {
+					maxRes = vals.maxOverBDD(ddFilter);
+					mainLog.print("\nMaximum value for states satisfying " + filter.getExpression() + ": " + maxRes
+							+ "\n");
+					tmp = vals.getBDDFromInterval(maxRes - termCritParam, maxRes + termCritParam);
+					JDD.Ref(ddFilter);
+					tmp = JDD.And(tmp, ddFilter);
+					states = new StateListMTBDD(tmp, model);
+					mainLog.print("There are " + states.size() + " states with this maximum value (+/- "
+							+ termCritParam + ")");
+					if (!verbose && states.size() > 10) {
+						mainLog
+								.print(".\nThe first 10 states are displayed below. To view them all, use verbose mode.\n");
+						states.print(mainLog, 10);
+					} else {
+						mainLog.print(":\n");
+						states.print(mainLog);
+					}
+					JDD.Deref(tmp);
 				}
-				JDD.Deref(tmp);
 			}
-			if (filter.minRequested())
-				res = minRes;
-			else if (filter.maxRequested())
-				res = maxRes;
+			if (filter != null && filter.minRequested())
+				res = new Result(minRes);
+			else if (filter != null && filter.maxRequested())
+				res = new Result(maxRes);
 			else
-				res = vals.firstFromBDD(ddFilter);
-			
-			// print result
+				res = new Result(vals.firstFromBDD(filter != null ? ddFilter : start));
+
+			// Print result to log
 			resultString = "Result";
 			if (!("Result".equals(expr.getResultName())))
-				resultString += " ("+expr.getResultName().toLowerCase()+")";
+				resultString += " (" + expr.getResultName().toLowerCase() + ")";
 			resultString += ": " + res;
-			mainLog.print("\n"+resultString+"\n");
+			mainLog.print("\n" + resultString + "\n");
 		}
 
-		// clean up
-		JDD.Deref(ddFilter);
+		// Clean up
+		if (ddFilter != null) JDD.Deref(ddFilter);
 		vals.clear();
 
-		// return result
-		ret = new Result(res);
-		return ret;
+		// Return result
+		return res;
 	}
 
 	// Check expression (recursive)

prism/src/userinterface/properties/GUIExperiment.java

@@ -167,9 +167,9 @@ public class GUIExperiment
 		table.repaint();
 	}
 	
-	public synchronized void setResult(Values mfValues, Values pfValues, Object c) throws PrismException
+	public synchronized void setResult(Values mfValues, Values pfValues, Result res) throws PrismException
 	{
-		results.setResult(mfValues, pfValues, c);
+		results.setResult(mfValues, pfValues, res.getResult());
 	}
 	
 	public synchronized void setMultipleErrors(Values mfValues, Values pfValues, Exception e) throws PrismException
@@ -422,7 +422,7 @@ public class GUIExperiment
 								public void run()
 								{
 									try {
-										GUIExperiment.this.setResult(definedMFConstants, definedPFConstants, res.getResult());
+										GUIExperiment.this.setResult(definedMFConstants, definedPFConstants, res);
 									}
 									catch (PrismException e) {
 										error("Problem storing results");

prism/src/userinterface/properties/GUIProperty.java

@@ -85,8 +85,7 @@ public class GUIProperty
 	private Expression expr;		// The parsed property
 	private String comment;			// The property's comment
 	
-	private Object result;			// Result of model checking etc. (if done, null if not)
-	private String resultString;	// Result of model checking etc. (if done, null if not)
+	private Result result;			// Result of model checking etc. (if done, null if not)
 	private String parseError;		// Parse error (if property is invalid)
 	
 	private String method;			// Method used (verification, simulation)
@@ -110,7 +109,6 @@ public class GUIProperty
 		this.comment = comment;
 		
 		result = null;
-		resultString = "Unknown";
 		parseError = "";
 		method = "<none>";
 		constantsString = "<none>";
@@ -195,14 +193,14 @@ public class GUIProperty
 		else return false;
 	}
 	
-	public Object getResult()
+	public Result getResult()
 	{
 		return result;
 	}
 	
 	public String getResultString()
 	{
-		return resultString;
+		return result == null ? "Unknown" : result.getResultString();
 	}
 	
 	public String getToolTipText()
@@ -210,8 +208,8 @@ public class GUIProperty
 		switch (status) {
 		case STATUS_DOING: return "In progress...";
 		case STATUS_PARSE_ERROR: return "Invalid property: " + parseError;
-		case STATUS_RESULT_ERROR: return resultString;
-		default: return "Result: " + resultString;
+		case STATUS_RESULT_ERROR: return getResultString();
+		default: return "Result: " + getResultString();
 		}
 	}
 	
@@ -259,38 +257,29 @@ public class GUIProperty
 		this.beingEdited = beingEdited;
 	}
 	
-	public void setResult(Object obj)
+	public void setResult(Result res)
 	{
-		result = obj;
-		if (obj instanceof Boolean)
+		result = res;
+		if (result.getResult() instanceof Boolean)
 		{
-			boolean res = ((Boolean)obj).booleanValue();
-			if(res) 
-			{
+			if (((Boolean)result.getResult()).booleanValue()) {
 				setStatus(STATUS_RESULT_TRUE);
-				resultString = "True";
-			}
-			else
-			{
+			} else {
 				setStatus(STATUS_RESULT_FALSE);
-				resultString = "False";
 			}
 		}
-		else if (obj instanceof Double)
+		else if (result.getResult() instanceof Double)
 		{
 			setStatus(STATUS_RESULT_NUMBER);
-			resultString = "" + ((Double)obj).doubleValue();
 		}
-		else if (obj instanceof Exception)
+		else if (result.getResult() instanceof Exception)
 		{
 			setStatus(STATUS_RESULT_ERROR);
-			resultString = "Error: " + ((Exception)obj).getMessage();
 		}
 		else
 		{
 			setStatus(STATUS_NOT_DONE);
 			result = null;
-			resultString = "Unknown";
 		}
 	}
 	

prism/src/userinterface/properties/computation/ModelCheckThread.java

@@ -118,7 +118,7 @@ public class ModelCheckThread extends GUIComputationThread
 			catch(InterruptedException e)
 			{}
 			//while(!ic.canContinue){}
-			gp.setResult(result.getResult());
+			gp.setResult(result);
 			gp.setMethodString("Verification");
 			gp.setConstants(definedMFConstants, definedPFConstants);
 			

prism/src/userinterface/properties/computation/SimulateModelCheckThread.java

@@ -163,7 +163,7 @@ public class SimulateModelCheckThread extends GUIComputationThread
 			for(int i = 0; i < guiProps.size(); i++)
 			{
 				GUIProperty gp = (GUIProperty)guiProps.get(i);
-				gp.setResult((results == null) ? resultError : results[i].getResult());
+				gp.setResult((results == null) ? new Result(resultError) : results[i]);
 				gp.setMethodString("Simulation");
 				gp.setConstants(definedMFConstants, definedPFConstants);
 			}
@@ -196,7 +196,7 @@ public class SimulateModelCheckThread extends GUIComputationThread
 				}
 				ic.interrupt();
 				while(!ic.canContinue) {}
-				gp.setResult(result.getResult());
+				gp.setResult(result);
 				gp.setMethodString("Simulation");
 				gp.setConstants(definedMFConstants, definedPFConstants);
 				

prism/src/userinterface/simulator/networking/GUISimulatorDistributionDialog.java

@@ -213,7 +213,7 @@ public class GUISimulatorDistributionDialog extends javax.swing.JDialog implemen
 				double result = network.getResultsFile().getResult(i);
 				if(result >= 0.0)
 				{
-					guiProp.setResult(new Double(result));
+					guiProp.setResult(new Result(result));
 					guiProp.setMethodString("Distributed Simulation");
 					guiProp.setConstants(undefinedConstants.getMFConstantValues(), undefinedConstants.getPFConstantValues());
 				}