From b8a2444e1e8b733c7912ae297b154bf8efd8a80b Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 19 Mar 2008 14:11:29 +0000 Subject: [PATCH] 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 | 26 ++- prism/src/prism/StateListMTBDD.java | 22 ++- prism/src/prism/StateModelChecker.java | 160 +++++++++--------- .../properties/GUIExperiment.java | 6 +- .../userinterface/properties/GUIProperty.java | 35 ++-- .../computation/ModelCheckThread.java | 2 +- .../computation/SimulateModelCheckThread.java | 4 +- .../GUISimulatorDistributionDialog.java | 2 +- 8 files changed, 147 insertions(+), 110 deletions(-) diff --git a/prism/src/prism/Result.java b/prism/src/prism/Result.java index 44eccf38..454ef810 100644 --- a/prism/src/prism/Result.java +++ b/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; } } diff --git a/prism/src/prism/StateListMTBDD.java b/prism/src/prism/StateListMTBDD.java index 7dc14731..3ae2d438 100644 --- a/prism/src/prism/StateListMTBDD.java +++ b/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 diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index c4f8b354..5a1f302d 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/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) diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java index e107b5e4..35d24ea8 100644 --- a/prism/src/userinterface/properties/GUIExperiment.java +++ b/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"); diff --git a/prism/src/userinterface/properties/GUIProperty.java b/prism/src/userinterface/properties/GUIProperty.java index a099e1a9..78e0c345 100644 --- a/prism/src/userinterface/properties/GUIProperty.java +++ b/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 = ""; constantsString = ""; @@ -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"; } } diff --git a/prism/src/userinterface/properties/computation/ModelCheckThread.java b/prism/src/userinterface/properties/computation/ModelCheckThread.java index 63620b01..d4c3b7f1 100644 --- a/prism/src/userinterface/properties/computation/ModelCheckThread.java +++ b/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); diff --git a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java b/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java index c71de9bf..1b7ecf4b 100644 --- a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java +++ b/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); diff --git a/prism/src/userinterface/simulator/networking/GUISimulatorDistributionDialog.java b/prism/src/userinterface/simulator/networking/GUISimulatorDistributionDialog.java index fde22b6c..4b311334 100644 --- a/prism/src/userinterface/simulator/networking/GUISimulatorDistributionDialog.java +++ b/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()); }