Pareto queries return actual point list (TileList), not void.

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

prism/src/prism/NondetModelChecker.java

@@ -1046,7 +1046,8 @@ public class NondetModelChecker extends NonProbModelChecker
 					TileList.storedTileLists.add((TileList) value);
 				}
 			} //else, i.e. in 3D, the output was treated in the algorithm itself.
-			return new StateValuesMTBDD(JDD.Constant(1), model); //returning something dummy
+
+			return new StateValuesVoid(value);
 		}
 		else if (value instanceof Double) {
 			// Return result. Note: we only compute the value for a single state.
@@ -1055,7 +1056,8 @@ public class NondetModelChecker extends NonProbModelChecker
 			}
 	
 			return new StateValuesMTBDD(JDD.Constant((Double) value), model);
-		} else throw new PrismException("Do not know how to tread the returned value " + value);
+		}
+		else throw new PrismException("Do not know how to treat the returned value " + value);
 			
 	}
 

prism/src/prism/StateModelChecker.java

@@ -1300,21 +1300,30 @@ public class StateModelChecker implements ModelChecker
 				s += " (but \"" + filter + "\" is true in " + statesFilter.size() + " states)";
 				throw new PrismException(s);
 			}
-			// Find first (only) value
-			d = vals.firstFromBDD(ddFilter);
-			// Store as object/vector
-			if (expr.getType() instanceof TypeInt) {
-				resObj = new Integer((int) d);
-			} else if (expr.getType() instanceof TypeDouble) {
-				resObj = new Double(d);
-			} else if (expr.getType() instanceof TypeBool) {
-				resObj = new Boolean(d > 0);
-			} else if (expr.getType() instanceof TypeVoid) {
-				resObj = TypeVoid.getInstance(); //we can't really return anything better
-			} else {
-				throw new PrismException("Don't know how to handle result of type " + expr.getType());
+			// Results of type void are handled differently
+			if (expr.getType() instanceof TypeVoid) {
+				// Extract result from StateValuesVoid object 
+				resObj = ((StateValuesVoid) vals).getValue();
+				// Leave result vector unchanged: for a range, result is only available from Result object
+				resVals = vals;
+				// Set vals to null to stop it being cleared below
+				vals = null;
+			}
+			else {
+				// Find first (only) value
+				d = vals.firstFromBDD(ddFilter);
+				// Store as object/vector
+				if (expr.getType() instanceof TypeInt) {
+					resObj = new Integer((int) d);
+				} else if (expr.getType() instanceof TypeDouble) {
+					resObj = new Double(d);
+				} else if (expr.getType() instanceof TypeBool) {
+					resObj = new Boolean(d > 0);
+				} else {
+					throw new PrismException("Don't know how to handle result of type " + expr.getType());
+				}
+				resVals = new StateValuesMTBDD(JDD.Constant(d), model);
 			}
-			resVals = new StateValuesMTBDD(JDD.Constant(d), model);
 			// Create explanation of result and print some details to log
 			resultExpl = "Value in ";
 			if (filterInit) {

prism/src/prism/StateValuesVoid.java

@@ -0,0 +1,205 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham)
+//	
+//------------------------------------------------------------------------------
+//	
+//	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.io.File;
+
+import jdd.JDDNode;
+import jdd.JDDVars;
+
+/**
+ * Dummy class implementing StateValues to return miscellaneous (single valued) results, typically of type "void".
+ */
+public class StateValuesVoid implements StateValues
+{
+	private Object value = null;
+	
+	public StateValuesVoid(Object value)
+	{
+		this.value = value;
+	}
+	
+	public Object getValue()
+	{
+		return value;
+	}
+
+	public void setValue(Object value)
+	{
+		this.value = value;
+	}
+
+	public StateValuesDV convertToStateValuesDV()
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public StateValuesMTBDD convertToStateValuesMTBDD()
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public void readFromFile(File file) throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public void roundOff(int places)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public void subtractFromOne()
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public void add(StateValues sp)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public void timesConstant(double d)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public double dotProduct(StateValues sp)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public void filter(JDDNode filter)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public void maxMTBDD(JDDNode vec2)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public void clear()
+	{
+		// Do nothing
+	}
+	
+	public int getNNZ()
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public String getNNZString()
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public double firstFromBDD(JDDNode filter)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public double minOverBDD(JDDNode filter)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public double maxOverBDD(JDDNode filter)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public double sumOverBDD(JDDNode filter)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public double sumOverMTBDD(JDDNode mult)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public StateValues sumOverDDVars(JDDVars sumVars, Model newModel) throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public JDDNode getBDDFromInterval(String relOp, double bound)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public JDDNode getBDDFromInterval(double lo, double hi)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public JDDNode getBDDFromCloseValue(double val, double epsilon, boolean abs)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public JDDNode getBDDFromCloseValueAbs(double val, double epsilon)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public JDDNode getBDDFromCloseValueRel(double val, double epsilon)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public void print(PrismLog log) throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public void printFiltered(PrismLog log, JDDNode filter) throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	public StateValues deepCopy() throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+}

prism/src/prism/TileList.java

@@ -158,7 +158,7 @@ public class TileList
 				if (first)
 					first = false;
 				else
-					s += ",";
+					s += ",\n";
 				s += "(";
 				for (int i = 0; i < p.getDimension(); i++) {
 					if (i > 0)

prism/src/userinterface/properties/GUIProperty.java

@@ -322,7 +322,7 @@ public class GUIProperty
 			setStatus(STATUS_RESULT_NUMBER);
 		} else if (result.getResult() instanceof Exception) {
 			setStatus(STATUS_RESULT_ERROR);
-		} else if (result.getResult() instanceof TypeVoid) {
+		} else if (result.getResult() instanceof TileList) {
 			setStatus(STATUS_RESULT_PARETO);
 		} else {
 			setStatus(STATUS_NOT_DONE);