From 36997ee08cdca1aa33ddcbaa0bcc1eb2439d695a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 28 Jun 2014 00:20:21 +0000 Subject: [PATCH] Refactor explicit model checkers a bit, including changes to way min/max info is passed around (should generalise to games more nicely). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8643 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/CTMCModelChecker.java | 6 +- prism/src/explicit/CTMDPModelChecker.java | 5 +- prism/src/explicit/DTMCModelChecker.java | 89 ++------------- prism/src/explicit/MDPModelChecker.java | 99 +++-------------- prism/src/explicit/MinMax.java | 78 +++++++++++++ prism/src/explicit/ProbModelChecker.java | 128 ++++++++++++++++++---- 6 files changed, 209 insertions(+), 196 deletions(-) create mode 100644 prism/src/explicit/MinMax.java diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index ef2ecc08..67db7f15 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -53,10 +53,8 @@ public class CTMCModelChecker extends DTMCModelChecker // Model checking functions - /** - * Model check a time-bounded until operator; return vector of probabilities for all states. - */ - protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr) throws PrismException + @Override + protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException { double lTime, uTime; // time bounds Expression exprTmp; diff --git a/prism/src/explicit/CTMDPModelChecker.java b/prism/src/explicit/CTMDPModelChecker.java index 7b6d47a1..bee2963d 100644 --- a/prism/src/explicit/CTMDPModelChecker.java +++ b/prism/src/explicit/CTMDPModelChecker.java @@ -51,7 +51,8 @@ public class CTMDPModelChecker extends MDPModelChecker // Model checking functions - protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, boolean min) throws PrismException + @Override + protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException { double uTime; BitSet b1, b2; @@ -76,7 +77,7 @@ public class CTMDPModelChecker extends MDPModelChecker // prob is 1 in b2 states, 0 otherwise probs = StateValues.createFromBitSetAsDoubles(b2, model); } else { - res = computeBoundedUntilProbs((CTMDP) model, b1, b2, uTime, min); + res = computeBoundedUntilProbs((CTMDP) model, b1, b2, uTime, minMax.isMin()); probs = StateValues.createFromDoubleArray(res.soln, model); } diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 3099eccc..580771f4 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -34,7 +34,6 @@ import java.util.Vector; import parser.ast.Expression; import parser.ast.ExpressionTemporal; -import parser.ast.ExpressionUnaryOp; import parser.type.TypeDouble; import prism.DRA; import prism.Pair; @@ -58,74 +57,8 @@ public class DTMCModelChecker extends ProbModelChecker // Model checking functions - /** - * Compute probabilities for the contents of a P operator. - */ - protected StateValues checkProbPathFormula(Model model, Expression expr) throws PrismException - { - // Test whether this is a simple path formula (i.e. PCTL) - // and then pass control to appropriate method. - if (expr.isSimplePathFormula()) { - return checkProbPathFormulaSimple(model, expr); - } else { - return checkProbPathFormulaLTL(model, expr, false); - } - } - - /** - * Compute probabilities for a simple, non-LTL path operator. - */ - protected StateValues checkProbPathFormulaSimple(Model model, Expression expr) throws PrismException - { - StateValues probs = null; - - // Negation/parentheses - if (expr instanceof ExpressionUnaryOp) { - ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr; - // Parentheses - if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) { - // Recurse - probs = checkProbPathFormulaSimple(model, exprUnary.getOperand()); - } - // Negation - else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) { - // Compute, then subtract from 1 - probs = checkProbPathFormulaSimple(model, exprUnary.getOperand()); - probs.timesConstant(-1.0); - probs.plusConstant(1.0); - } - } - // Temporal operators - else if (expr instanceof ExpressionTemporal) { - ExpressionTemporal exprTemp = (ExpressionTemporal) expr; - // Next - if (exprTemp.getOperator() == ExpressionTemporal.P_X) { - probs = checkProbNext(model, exprTemp); - } - // Until - else if (exprTemp.getOperator() == ExpressionTemporal.P_U) { - if (exprTemp.hasBounds()) { - probs = checkProbBoundedUntil(model, exprTemp); - } else { - probs = checkProbUntil(model, exprTemp); - } - } - // Anything else - convert to until and recurse - else { - probs = checkProbPathFormulaSimple(model, exprTemp.convertToUntilForm()); - } - } - - if (probs == null) - throw new PrismException("Unrecognised path operator in P operator"); - - return probs; - } - - /** - * Compute probabilities for a next operator. - */ - protected StateValues checkProbNext(Model model, ExpressionTemporal expr) throws PrismException + @Override + protected StateValues checkProbNext(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException { BitSet target = null; ModelCheckerResult res = null; @@ -137,10 +70,8 @@ public class DTMCModelChecker extends ProbModelChecker return StateValues.createFromDoubleArray(res.soln, model); } - /** - * Compute probabilities for a bounded until operator. - */ - protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr) throws PrismException + @Override + protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException { int time; BitSet b1, b2; @@ -174,10 +105,8 @@ public class DTMCModelChecker extends ProbModelChecker return probs; } - /** - * Compute probabilities for an (unbounded) until operator. - */ - protected StateValues checkProbUntil(Model model, ExpressionTemporal expr) throws PrismException + @Override + protected StateValues checkProbUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException { BitSet b1, b2; StateValues probs = null; @@ -199,10 +128,8 @@ public class DTMCModelChecker extends ProbModelChecker return probs; } - /** - * Compute probabilities for an LTL path formula - */ - protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual) throws PrismException + @Override + protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException { LTLModelChecker mcLtl; StateValues probsProduct, probs; diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 55902975..2f5c7ea2 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -34,7 +34,6 @@ import java.util.Vector; import parser.ast.Expression; import parser.ast.ExpressionTemporal; -import parser.ast.ExpressionUnaryOp; import parser.type.TypeDouble; import prism.DRA; import prism.Pair; @@ -64,74 +63,8 @@ public class MDPModelChecker extends ProbModelChecker // Model checking functions - /** - * Compute probabilities for the contents of a P operator. - */ - protected StateValues checkProbPathFormula(NondetModel model, Expression expr, boolean min) throws PrismException - { - // Test whether this is a simple path formula (i.e. PCTL) - // and then pass control to appropriate method. - if (expr.isSimplePathFormula()) { - return checkProbPathFormulaSimple(model, expr, min); - } else { - return checkProbPathFormulaLTL(model, expr, min); - } - } - - /** - * Compute probabilities for a simple, non-LTL path operator. - */ - protected StateValues checkProbPathFormulaSimple(NondetModel model, Expression expr, boolean min) throws PrismException - { - StateValues probs = null; - - // Negation/parentheses - if (expr instanceof ExpressionUnaryOp) { - ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr; - // Parentheses - if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) { - // Recurse - probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), min); - } - // Negation - else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) { - // Compute, then subtract from 1 - probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), !min); - probs.timesConstant(-1.0); - probs.plusConstant(1.0); - } - } - // Temporal operators - else if (expr instanceof ExpressionTemporal) { - ExpressionTemporal exprTemp = (ExpressionTemporal) expr; - // Next - if (exprTemp.getOperator() == ExpressionTemporal.P_X) { - probs = checkProbNext(model, exprTemp, min); - } - // Until - else if (exprTemp.getOperator() == ExpressionTemporal.P_U) { - if (exprTemp.hasBounds()) { - probs = checkProbBoundedUntil(model, exprTemp, min); - } else { - probs = checkProbUntil(model, exprTemp, min); - } - } - // Anything else - convert to until and recurse - else { - probs = checkProbPathFormulaSimple(model, exprTemp.convertToUntilForm(), min); - } - } - - if (probs == null) - throw new PrismException("Unrecognised path operator in P operator"); - - return probs; - } - - /** - * Compute probabilities for a next operator. - */ - protected StateValues checkProbNext(NondetModel model, ExpressionTemporal expr, boolean min) throws PrismException + @Override + protected StateValues checkProbNext(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException { BitSet target = null; ModelCheckerResult res = null; @@ -139,14 +72,12 @@ public class MDPModelChecker extends ProbModelChecker // Model check the operand target = checkExpression(model, expr.getOperand2()).getBitSet(); - res = computeNextProbs((MDP) model, target, min); + res = computeNextProbs((MDP) model, target, minMax.isMin()); return StateValues.createFromDoubleArray(res.soln, model); } - /** - * Compute probabilities for a bounded until operator. - */ - protected StateValues checkProbBoundedUntil(NondetModel model, ExpressionTemporal expr, boolean min) throws PrismException + @Override + protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException { int time; BitSet b1, b2; @@ -179,17 +110,15 @@ public class MDPModelChecker extends ProbModelChecker // prob is 1 in b2 states, 0 otherwise probs = StateValues.createFromBitSetAsDoubles(b2, model); } else { - res = computeBoundedUntilProbs((MDP) model, b1, b2, time, min); + res = computeBoundedUntilProbs((MDP) model, b1, b2, time, minMax.isMin()); probs = StateValues.createFromDoubleArray(res.soln, model); } return probs; } - /** - * Compute probabilities for an (unbounded) until operator. - */ - protected StateValues checkProbUntil(NondetModel model, ExpressionTemporal expr, boolean min) throws PrismException + @Override + protected StateValues checkProbUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException { BitSet b1, b2; StateValues probs = null; @@ -205,17 +134,15 @@ public class MDPModelChecker extends ProbModelChecker // mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(b2, // allDDRowVars.n()) + " states\n"); - res = computeUntilProbs((MDP) model, b1, b2, min); + res = computeUntilProbs((MDP) model, b1, b2, minMax.isMin()); probs = StateValues.createFromDoubleArray(res.soln, model); result.setStrategy(res.strat); return probs; } - /** - * Compute probabilities for an LTL path formula - */ - protected StateValues checkProbPathFormulaLTL(NondetModel model, Expression expr, boolean min) throws PrismException + @Override + protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException { LTLModelChecker mcLtl; StateValues probsProduct, probs; @@ -240,7 +167,7 @@ public class MDPModelChecker extends ProbModelChecker // Convert LTL formula to deterministic Rabin automaton (DRA) // For min probabilities, need to negate the formula // (add parentheses to allow re-parsing if required) - if (min) { + if (minMax.isMin()) { ltl = Expression.Not(Expression.Parenth(ltl)); } mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); @@ -268,7 +195,7 @@ public class MDPModelChecker extends ProbModelChecker probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs((MDP) modelProduct, acceptingMECs, false).soln, modelProduct); // Subtract from 1 if we're model checking a negated formula for regular Pmin - if (min) { + if (minMax.isMin()) { probsProduct.timesConstant(-1.0); probsProduct.plusConstant(1.0); } diff --git a/prism/src/explicit/MinMax.java b/prism/src/explicit/MinMax.java new file mode 100644 index 00000000..7b4efdc2 --- /dev/null +++ b/prism/src/explicit/MinMax.java @@ -0,0 +1,78 @@ +//============================================================================== +// +// Copyright (c) 2014- +// Authors: +// * Dave Parker (University of Birmingham/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 explicit; + +/** + * Class to store info about types of probabilities that are to be computed + * (typically how to quantify over strategies, e.g. "min" or "max"). + */ +public class MinMax +{ + // Info about quantification over a single class of strategies/adversaries + + protected boolean min; + + public void setMin(boolean min) + { + this.min = min; + } + + public boolean isMin() + { + return min; + } + + public boolean isMax() + { + return !min; + } + + // Create a new instance by applying some operation + + public MinMax negate() + { + MinMax neg = new MinMax(); + neg.setMin(!isMin()); + return neg; + } + + // Utility methods to create instances of this class + + public static MinMax min() + { + MinMax minMax = new MinMax(); + minMax.setMin(true); + return minMax; + } + + public static MinMax max() + { + MinMax minMax = new MinMax(); + minMax.setMin(false); + return minMax; + } +} diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 238e5722..dc63a4fe 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -32,6 +32,8 @@ import parser.ast.Expression; import parser.ast.ExpressionProb; import parser.ast.ExpressionReward; import parser.ast.ExpressionSS; +import parser.ast.ExpressionTemporal; +import parser.ast.ExpressionUnaryOp; import parser.ast.RelOp; import parser.ast.RewardStruct; import prism.ModelType; @@ -466,8 +468,6 @@ public class ProbModelChecker extends NonProbModelChecker Expression pb; // Probability bound (expression) double p = 0; // Probability bound (actual value) RelOp relOp; // Relational operator - boolean min = false; // For nondeterministic models, are we finding min (true) or max (false) probs - ModelType modelType = model.getModelType(); StateValues probs = null; @@ -479,29 +479,11 @@ public class ProbModelChecker extends NonProbModelChecker if (p < 0 || p > 1) throw new PrismException("Invalid probability bound " + p + " in P operator"); } - min = relOp.isLowerBound() || relOp.isMin(); // Compute probabilities - switch (modelType) { - case CTMC: - probs = ((CTMCModelChecker) this).checkProbPathFormula(model, expr.getExpression()); - break; - case CTMDP: - probs = ((CTMDPModelChecker) this).checkProbPathFormula((NondetModel) model, expr.getExpression(), min); - break; - case DTMC: - probs = ((DTMCModelChecker) this).checkProbPathFormula(model, expr.getExpression()); - break; - case MDP: - probs = ((MDPModelChecker) this).checkProbPathFormula((NondetModel) model, expr.getExpression(), min); - break; - /*case STPG: - probs = ((STPGModelChecker) this).checkProbPathFormula(model, expr.getExpression(), min); - break;*/ - default: - throw new PrismException("Cannot model check " + expr + " for a " + modelType); - } - + MinMax minMax = (relOp.isLowerBound() || relOp.isMin()) ? MinMax.min() : MinMax.max(); + probs = checkProbPathFormula(model, expr.getExpression(), minMax); + // Print out probabilities if (getVerbosity() > 5) { mainLog.print("\nProbabilities (non-zero only) for all states:\n"); @@ -520,6 +502,106 @@ public class ProbModelChecker extends NonProbModelChecker } } + /** + * Compute probabilities for the contents of a P operator. + */ + protected StateValues checkProbPathFormula(Model model, Expression expr, MinMax minMax) throws PrismException + { + // Test whether this is a simple path formula (i.e. PCTL) + // and then pass control to appropriate method. + if (expr.isSimplePathFormula()) { + return checkProbPathFormulaSimple(model, expr, minMax); + } else { + return checkProbPathFormulaLTL(model, expr, false, minMax); + } + } + + /** + * Compute probabilities for a simple, non-LTL path operator. + */ + protected StateValues checkProbPathFormulaSimple(Model model, Expression expr, MinMax minMax) throws PrismException + { + StateValues probs = null; + + // Negation/parentheses + if (expr instanceof ExpressionUnaryOp) { + ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr; + // Parentheses + if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) { + // Recurse + probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), minMax); + } + // Negation + else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) { + // Compute, then subtract from 1 + probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), minMax.negate()); + probs.timesConstant(-1.0); + probs.plusConstant(1.0); + } + } + // Temporal operators + else if (expr instanceof ExpressionTemporal) { + ExpressionTemporal exprTemp = (ExpressionTemporal) expr; + // Next + if (exprTemp.getOperator() == ExpressionTemporal.P_X) { + probs = checkProbNext(model, exprTemp, minMax); + } + // Until + else if (exprTemp.getOperator() == ExpressionTemporal.P_U) { + if (exprTemp.hasBounds()) { + probs = checkProbBoundedUntil(model, exprTemp, minMax); + } else { + probs = checkProbUntil(model, exprTemp, minMax); + } + } + // Anything else - convert to until and recurse + else { + probs = checkProbPathFormulaSimple(model, exprTemp.convertToUntilForm(), minMax); + } + } + + if (probs == null) + throw new PrismException("Unrecognised path operator in P operator"); + + return probs; + } + + /** + * Compute probabilities for a next operator. + */ + protected StateValues checkProbNext(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException + { + // To be overridden by subclasses + throw new PrismException("Computation not implemented yet"); + } + + /** + * Compute probabilities for a bounded until operator. + */ + protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException + { + // To be overridden by subclasses + throw new PrismException("Computation not implemented yet"); + } + + /** + * Compute probabilities for an (unbounded) until operator. + */ + protected StateValues checkProbUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException + { + // To be overridden by subclasses + throw new PrismException("Computation not implemented yet"); + } + + /** + * Compute probabilities for an LTL path formula + */ + protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException + { + // To be overridden by subclasses + throw new PrismException("Computation not implemented yet"); + } + /** * Model check an R operator expression and return the values for all states. */