From 01c8e4872d20c4ce52b3e161bcc743a946c42f4b Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 18 Dec 2012 00:56:22 +0000 Subject: [PATCH] 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 | 6 +- prism/src/prism/StateModelChecker.java | 37 ++-- prism/src/prism/StateValuesVoid.java | 205 ++++++++++++++++++ prism/src/prism/TileList.java | 2 +- .../userinterface/properties/GUIProperty.java | 2 +- 5 files changed, 234 insertions(+), 18 deletions(-) create mode 100644 prism/src/prism/StateValuesVoid.java diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index ece1ad2b..63548be8 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/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); } diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 2f70625b..65bb13a0 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/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) { diff --git a/prism/src/prism/StateValuesVoid.java b/prism/src/prism/StateValuesVoid.java new file mode 100644 index 00000000..95b14898 --- /dev/null +++ b/prism/src/prism/StateValuesVoid.java @@ -0,0 +1,205 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (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(); + } +} diff --git a/prism/src/prism/TileList.java b/prism/src/prism/TileList.java index 06c4182c..abe5674a 100644 --- a/prism/src/prism/TileList.java +++ b/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) diff --git a/prism/src/userinterface/properties/GUIProperty.java b/prism/src/userinterface/properties/GUIProperty.java index 1dc24d46..d2fa29cc 100644 --- a/prism/src/userinterface/properties/GUIProperty.java +++ b/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);