From 3a718795f84b6e5d8d06ae061bad82a8315c2fc3 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 17 Mar 2008 23:12:04 +0000 Subject: [PATCH] Small improvements to model checking output. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@687 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/ExpressionProb.java | 5 +++- prism/src/parser/ast/ExpressionReward.java | 9 ++++-- prism/src/prism/Prism.java | 4 +++ prism/src/prism/StateModelChecker.java | 32 ++++++++++++---------- 4 files changed, 33 insertions(+), 17 deletions(-) diff --git a/prism/src/parser/ast/ExpressionProb.java b/prism/src/parser/ast/ExpressionProb.java index fbbcd4b5..4751a01d 100644 --- a/prism/src/parser/ast/ExpressionProb.java +++ b/prism/src/parser/ast/ExpressionProb.java @@ -138,7 +138,10 @@ public class ExpressionProb extends Expression */ public String getResultName() { - return (prob == null) ? "Probability" : "Result"; + if (prob != null) return "Result"; + else if (relOp.equals("min=")) return "Minimum probability"; + else if (relOp.equals("max=")) return "Maximum probability"; + else return "Probability"; } // Methods required for ASTElement: diff --git a/prism/src/parser/ast/ExpressionReward.java b/prism/src/parser/ast/ExpressionReward.java index fb013c80..6075b060 100644 --- a/prism/src/parser/ast/ExpressionReward.java +++ b/prism/src/parser/ast/ExpressionReward.java @@ -151,9 +151,14 @@ public class ExpressionReward extends Expression { // For R=? properties, use name of reward structure where applicable if (reward == null) { - if (rewardStructIndex instanceof String) return "Expected "+rewardStructIndex; + String s = "E"; + if (relOp.equals("min=")) s = "Minimum e"; + else if (relOp.equals("max=")) s = "Maximum e"; + else s = "E"; + if (rewardStructIndex instanceof String) s += "xpected "+rewardStructIndex; // Or just call it "Expected reward" - else return "Expected reward"; + else s += "xpected reward"; + return s; } // For R>r etc., just use "Result" else { diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index a2dba115..3aed0a42 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1158,6 +1158,10 @@ public class Prism implements PrismSettingsListener // Do model checking if (expr instanceof ExpressionProb) filter = ((ExpressionProb)expr).getFilter(); + else if (expr instanceof ExpressionReward) + filter = ((ExpressionReward)expr).getFilter(); + else if (expr instanceof ExpressionSS) + filter = ((ExpressionSS)expr).getFilter(); else filter = null; res = mc.check(expr, filter); diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index bb676199..c3e62479 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -111,7 +111,7 @@ public class StateModelChecker implements ModelChecker { long timer = 0; JDDNode ddFilter, tmp; - StateList states; + StateListMTBDD states; boolean b; StateProbs vals; Object res; @@ -142,13 +142,16 @@ public class StateModelChecker implements ModelChecker 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 mainLog.print("\nNumber of satisfying states: "); mainLog.print(states.size()); - if (states.size() == model.getNumStates()) { + if (satAll) { mainLog.print(" (all)"); - } else if (states.includes(model.getStart())) { + } else if (satInit) { mainLog.print((model.getNumStartStates() == 1) ? " (including initial state)" : " (including all initial states)"); } else { @@ -169,7 +172,7 @@ public class StateModelChecker implements ModelChecker } // result is true if all states satisfy, false otherwise - b = (states.size() == model.getNumStates()); + b = satAll; res = b ? new Boolean(true) : new Boolean(false); states.clear(); @@ -178,16 +181,13 @@ public class StateModelChecker implements ModelChecker } else { if (filter.minRequested()) { minRes = vals.minOverBDD(ddFilter); - // TODO probability -> value? - // (what about min/max vals for MDPs?) - // (see also poss use of getresultname below) - mainLog.print("\nMinimum probability for states satisfying " + filter.getExpression() + ": " + minRes + 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 probability (+/- " + 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"); @@ -200,13 +200,13 @@ public class StateModelChecker implements ModelChecker } if (filter.maxRequested()) { maxRes = vals.maxOverBDD(ddFilter); - mainLog.print("\nMaximum probability for states satisfying " + filter.getExpression() + ": " + maxRes + 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 probability (+/- " + 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"); @@ -223,9 +223,13 @@ public class StateModelChecker implements ModelChecker res = maxRes; else res = vals.firstFromBDD(ddFilter); + // print result - mainLog.print("\nResult: " + res + "\n"); - // TODO: use expr.getresultname? + String resultString = "Result"; + if (!("Result".equals(expr.getResultName()))) + resultString += " ("+expr.getResultName().toLowerCase()+")"; + resultString += ": " + res; + mainLog.print("\n"+resultString+"\n"); } // clean up