From 69b62449fd9a783d0dd24e5300470c13d08b3db7 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 19 Mar 2008 12:34:00 +0000 Subject: [PATCH] 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 | 4 +- prism/src/prism/Prism.java | 14 +++-- prism/src/prism/PrismCL.java | 6 +- prism/src/prism/Result.java | 57 +++++++++++++++++++ prism/src/prism/StateModelChecker.java | 32 +++++++---- .../properties/GUIExperiment.java | 8 +-- .../properties/GUIMultiProperties.java | 4 ++ .../properties/GUIPropertiesEvent.java | 1 + .../properties/GUIPropertyResultDialog.java | 4 ++ .../computation/ModelCheckThread.java | 7 ++- .../computation/SimulateModelCheckThread.java | 10 ++-- 11 files changed, 113 insertions(+), 34 deletions(-) create mode 100644 prism/src/prism/Result.java diff --git a/prism/src/prism/ModelChecker.java b/prism/src/prism/ModelChecker.java index 44c07a98..a403311b 100644 --- a/prism/src/prism/ModelChecker.java +++ b/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; } //------------------------------------------------------------------------------ diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 3aed0a42..622a2007 100644 --- a/prism/src/prism/Prism.java +++ b/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) diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index cb01b6fb..ebd9f4cc 100644 --- a/prism/src/prism/PrismCL.java +++ b/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"); diff --git a/prism/src/prism/Result.java b/prism/src/prism/Result.java new file mode 100644 index 00000000..44eccf38 --- /dev/null +++ b/prism/src/prism/Result.java @@ -0,0 +1,57 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford, formerly University of Birmingham) +// * Andrew Hinton (University of Birmingham) +// * Mark Kattenbelt (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; + } +} diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index c3e62479..c4f8b354 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/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) diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java index 24767095..e107b5e4 100644 --- a/prism/src/userinterface/properties/GUIExperiment.java +++ b/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"); diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index 5d952700..cc60a4c8 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/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) { diff --git a/prism/src/userinterface/properties/GUIPropertiesEvent.java b/prism/src/userinterface/properties/GUIPropertiesEvent.java index 5b117a8c..c1e6673b 100644 --- a/prism/src/userinterface/properties/GUIPropertiesEvent.java +++ b/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; diff --git a/prism/src/userinterface/properties/GUIPropertyResultDialog.java b/prism/src/userinterface/properties/GUIPropertyResultDialog.java index 2fc9081f..da728e36 100644 --- a/prism/src/userinterface/properties/GUIPropertyResultDialog.java +++ b/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 diff --git a/prism/src/userinterface/properties/computation/ModelCheckThread.java b/prism/src/userinterface/properties/computation/ModelCheckThread.java index 233f2e04..63620b01 100644 --- a/prism/src/userinterface/properties/computation/ModelCheckThread.java +++ b/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)); } }); } diff --git a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java b/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java index fcd48190..71aafaf0 100644 --- a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java +++ b/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);