New class to encapsulate results from PRISM engine.

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

prism/src/prism/ModelChecker.java

@@ -32,8 +32,8 @@ import parser.ast.*;
 
 public interface ModelChecker
 {
-	public Object check(Expression expr) throws PrismException;
-	public Object check(Expression expr, Filter filter) throws PrismException;
+	public Result check(Expression expr) throws PrismException;
+	public Result check(Expression expr, Filter filter) throws PrismException;
 }
 
 //------------------------------------------------------------------------------

prism/src/prism/Prism.java

@@ -1128,9 +1128,9 @@ public class Prism implements PrismSettingsListener
 	// model checking
 	// returns result or throws an exception in case of error
 	
-	public Object modelCheck(Model model, PropertiesFile propertiesFile, Expression expr) throws PrismException, PrismLangException
+	public Result modelCheck(Model model, PropertiesFile propertiesFile, Expression expr) throws PrismException, PrismLangException
 	{
-		Object res;
+		Result res;
 		Filter filter;
 		
 		// Check that property is valid for this model type
@@ -1200,7 +1200,7 @@ public class Prism implements PrismSettingsListener
 	// model check using simulator
 	// returns result or throws an exception in case of error
 	
-	public Object modelCheckSimulator(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression f, Values initialState, int noIterations, int maxPathLength) throws PrismException
+	public Result modelCheckSimulator(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression f, Values initialState, int noIterations, int maxPathLength) throws PrismException
 	{
 		Object res = null;
 		
@@ -1214,14 +1214,14 @@ public class Prism implements PrismSettingsListener
 			throw new PrismException(e.getMessage());
 		}
 		
-		return res;
+		return new Result(res);
 	}
 	
 	// model check using simulator (several properties simultaneously)
 	// returns an array of results, some of which may be Exception objects if there were errors
 	// in the case of an error which affects all properties, an exception is thrown
 	
-	public Object[] modelCheckSimulatorSimultaneously(ModulesFile modulesFile, PropertiesFile propertiesFile, ArrayList fs, Values initialState, int noIterations, int maxPathLength) throws PrismException
+	public Result[] modelCheckSimulatorSimultaneously(ModulesFile modulesFile, PropertiesFile propertiesFile, ArrayList fs, Values initialState, int noIterations, int maxPathLength) throws PrismException
 	{
 		Object[] res = null;
 		
@@ -1234,7 +1234,9 @@ public class Prism implements PrismSettingsListener
 			throw new PrismException(e.getMessage());
 		}
 		
-		return res;
+		Result[] resArray = new Result[res.length];
+		for (int i = 0; i < res.length; i++) resArray[i] = new Result(res[i]);
+		return resArray;
 	}
 	
 	// model check using simulator (ranging over some constants - from properties file only)

prism/src/prism/PrismCL.java

@@ -133,7 +133,7 @@ public class PrismCL
 	public void run(String[] args)
 	{
 		int i, j, k;
-		Object res;
+		Result res;
 		
 		// initialise
 		try {
@@ -331,12 +331,12 @@ public class PrismCL
 						catch (PrismException e) {
 							// in case of error, report it, store exception as the result and proceed
 							error(e.getMessage());
-							res = e;
+							res = new Result(e);
 						}
 						
 						// store result of model checking
 						try {
-							results[j].setResult(definedMFConstants, definedPFConstants, res);
+							results[j].setResult(definedMFConstants, definedPFConstants, res.getResult());
 						}
 						catch (PrismException e) {
 							error("Problem storing results");

prism/src/prism/Result.java

@@ -0,0 +1,57 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
+//	* Andrew Hinton <ug60axh@cs.bham.ac.uk> (University of Birmingham)
+//	* 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;
+
+/**
+ * This class stores the result of a single verification/simulation.
+ */
+public class Result
+{
+	private Object result = null;
+	
+	public Result()
+	{
+		this.result = null;
+	}
+	
+	public Result(Object result)
+	{
+		this.result = result;
+	}
+	
+	public Object getResult()
+	{
+		return result;
+	}
+
+	public void setResult(Object result)
+	{
+		this.result = result;
+	}
+}

prism/src/prism/StateModelChecker.java

@@ -102,23 +102,30 @@ public class StateModelChecker implements ModelChecker
 	// Check a property, i.e. an expression
 	// -----------------------------------------------------------------------------------
 
-	public Object check(Expression expr) throws PrismException
+	public Result check(Expression expr) throws PrismException
 	{
 		return check(expr, null);
 	}
 
-	public Object check(Expression expr, Filter filter) throws PrismException
+	public Result check(Expression expr, Filter filter) throws PrismException
 	{
 		long timer = 0;
-		JDDNode ddFilter, tmp;
+		JDDNode ddFilter = null, tmp;
 		StateListMTBDD states;
 		boolean b;
 		StateProbs vals;
 		Object res;
+		String resultString;
 		double minRes = 0.0, maxRes = 0.0;
-
-		// Translate filter (creating default one first if none present)
-		if (filter == null) {
+		Result ret;
+		
+		// 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
@@ -126,9 +133,11 @@ public class StateModelChecker implements ModelChecker
 				model.getStartStates().print(mainLog, 1);
 			}
 		}
-		ddFilter = checkExpressionDD(filter.getExpression());
-		if (ddFilter.equals(JDD.ZERO)) {
-			throw new PrismException("Filter " + filter + " satisfies no states");
+		if (filter != null) {
+			ddFilter = checkExpressionDD(filter.getExpression());
+			if (ddFilter.equals(JDD.ZERO)) {
+				throw new PrismException("Filter " + filter + " satisfies no states");
+			}
 		}
 
 		// Do model checking and store result
@@ -225,7 +234,7 @@ public class StateModelChecker implements ModelChecker
 				res = vals.firstFromBDD(ddFilter);
 			
 			// print result
-			String resultString = "Result";
+			resultString = "Result";
 			if (!("Result".equals(expr.getResultName())))
 				resultString += " ("+expr.getResultName().toLowerCase()+")";
 			resultString += ": " + res;
@@ -237,7 +246,8 @@ public class StateModelChecker implements ModelChecker
 		vals.clear();
 
 		// return result
-		return res;
+		ret = new Result(res);
+		return ret;
 	}
 
 	// Check expression (recursive)

prism/src/userinterface/properties/GUIExperiment.java

@@ -59,7 +59,7 @@ public class GUIExperiment
 	
 	private Values definedMFConstants;
 	private Values definedPFConstants;
-	private Object res;
+	private Result res;
 	
 	/** Creates a new instance of GUIExperiment */
 	public GUIExperiment(GUIExperimentTable table, GUIMultiProperties guiProp, PropertiesFile prop, UndefinedConstants cons, ModulesFile mod, String modString, boolean useSimulation)
@@ -219,7 +219,7 @@ public class GUIExperiment
 			
 			definedMFConstants = null;
 			definedPFConstants = null;
-			res= null;
+			res = null;
 			
 			try
 			{
@@ -414,7 +414,7 @@ public class GUIExperiment
 							{
 								// in case of error, report it (in log only), store exception as the result and proceed
 								errorLog(e.getMessage());
-								res = e;
+								res = new Result(e);
 							}
 							// store result of model checking
 							SwingUtilities.invokeAndWait(new Runnable()
@@ -422,7 +422,7 @@ public class GUIExperiment
 								public void run()
 								{
 									try {
-										GUIExperiment.this.setResult(definedMFConstants, definedPFConstants, res);
+										GUIExperiment.this.setResult(definedMFConstants, definedPFConstants, res.getResult());
 									}
 									catch (PrismException e) {
 										error("Problem storing results");

prism/src/userinterface/properties/GUIMultiProperties.java

@@ -1202,6 +1202,10 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 			{
 				stopExperiment.setEnabled(false);
 			}
+			else if(pr.getID() == GUIPropertiesEvent.VERIFY_END)
+			{
+				a_detailSelected();
+			}
 		}
 		else if (e instanceof GUIExitEvent)
 		{

prism/src/userinterface/properties/GUIPropertiesEvent.java

@@ -39,6 +39,7 @@ public class GUIPropertiesEvent extends GUIEvent
     public static final int EXPERIMENT_START =3;
     public static final int EXPERIMENT_END = 4;
     public static final int PROPERTIES_LIST_CHANGED = 5;
+    public static final int VERIFY_END = 6;
     //private UndefinedConstants mfUndefined;
     private Values buildValues;
     

prism/src/userinterface/properties/GUIPropertyResultDialog.java

@@ -46,6 +46,9 @@ public class GUIPropertyResultDialog extends javax.swing.JDialog
 		initComponents();
 		getRootPane().setDefaultButton(jButton1);
 		setTitle("Property Details");
+
+		if (!("Result".equals(gp.getProperty().getResultName())))
+			jLabel8.setText("Result ("+gp.getProperty().getResultName().toLowerCase()+"):");
 		
 		propertyLabel.setText(gp.getPropString());
 		constantsLabel.setText(gp.getConstantsString());
@@ -56,6 +59,7 @@ public class GUIPropertyResultDialog extends javax.swing.JDialog
 		this.gmp = gmp;
 		
 		pack();
+		setLocation(getParent().getX(), getParent().getY());
 	}
 	
 	/** This method is called from within the constructor to

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

@@ -77,7 +77,7 @@ public class ModelCheckThread extends GUIComputationThread
 			}
 		});
 		
-		Object result = null;
+		Result result = null;
 		
 		//Set icon for all properties to be verified to a clock
 		for(int i = 0; i < guiProps.size(); i++)
@@ -107,7 +107,7 @@ public class ModelCheckThread extends GUIComputationThread
 			}
 			catch(PrismException e)
 			{
-				result = e;
+				result = new Result(e);
 				error(e.getMessage());
 			}
 			ic.interrupt();
@@ -118,7 +118,7 @@ public class ModelCheckThread extends GUIComputationThread
 			catch(InterruptedException e)
 			{}
 			//while(!ic.canContinue){}
-			gp.setResult(result);
+			gp.setResult(result.getResult());
 			gp.setMethodString("Verification");
 			gp.setConstants(definedMFConstants, definedPFConstants);
 			
@@ -131,6 +131,7 @@ public class ModelCheckThread extends GUIComputationThread
 				parent.stopProgress();
 				parent.setTaskBarText("Verifying properties... done.");
 				parent.notifyEventListeners(new GUIComputationEvent(GUIComputationEvent.COMPUTATION_DONE, parent));
+				parent.notifyEventListeners(new GUIPropertiesEvent(GUIPropertiesEvent.VERIFY_END));
 			}
 		});
 	}

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

@@ -112,7 +112,7 @@ public class SimulateModelCheckThread extends GUIComputationThread
 		// do all at once if requested
 		if(allAtOnce)
 		{
-			Object results[] = null;
+			Result results[] = null;
 			Exception resultError = null;
 			ArrayList properties = new ArrayList();
 			ArrayList clkThreads = new ArrayList();
@@ -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]);
+				gp.setResult((results == null) ? resultError : results[i].getResult());
 				gp.setMethodString("Simulation");
 				gp.setConstants(definedMFConstants, definedPFConstants);
 			}
@@ -171,7 +171,7 @@ public class SimulateModelCheckThread extends GUIComputationThread
 		// do each property individually
 		else
 		{
-			Object result = null;
+			Result result = null;
 			for(int i = 0; i < pf.getNumProperties(); i++)
 			{
 				// get property
@@ -191,12 +191,12 @@ public class SimulateModelCheckThread extends GUIComputationThread
 				}
 				catch(PrismException e)
 				{
-					result = e;
+					result = new Result(e);
 					error(e.getMessage());
 				}
 				ic.interrupt();
 				while(!ic.canContinue) {}
-				gp.setResult(result);
+				gp.setResult(result.getResult());
 				gp.setMethodString("Simulation");
 				gp.setConstants(definedMFConstants, definedPFConstants);