From 1f27c2846550c083b65772959b6df99942142274 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 4 Jan 2015 01:41:01 +0000 Subject: [PATCH] Re-factoring in multi-objective model checking. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9481 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/ExpressionProb.java | 2 +- prism/src/parser/ast/ExpressionQuant.java | 44 ++++++++++++++++++++++ prism/src/parser/ast/ExpressionReward.java | 2 +- prism/src/parser/ast/ExpressionSS.java | 2 +- prism/src/prism/MultiObjModelChecker.java | 6 +-- prism/src/prism/NondetModelChecker.java | 25 +++++++----- prism/src/prism/OpsAndBoundsList.java | 30 ++++++++++----- 7 files changed, 85 insertions(+), 26 deletions(-) create mode 100644 prism/src/parser/ast/ExpressionQuant.java diff --git a/prism/src/parser/ast/ExpressionProb.java b/prism/src/parser/ast/ExpressionProb.java index 84b7b10c..b3f9782a 100644 --- a/prism/src/parser/ast/ExpressionProb.java +++ b/prism/src/parser/ast/ExpressionProb.java @@ -33,7 +33,7 @@ import prism.OpRelOpBound; import prism.PrismException; import prism.PrismLangException; -public class ExpressionProb extends Expression +public class ExpressionProb extends Expression implements ExpressionQuant { RelOp relOp = null; Expression prob = null; diff --git a/prism/src/parser/ast/ExpressionQuant.java b/prism/src/parser/ast/ExpressionQuant.java new file mode 100644 index 00000000..7b7364ae --- /dev/null +++ b/prism/src/parser/ast/ExpressionQuant.java @@ -0,0 +1,44 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford, formerly 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 parser.ast; + +import parser.Values; +import prism.OpRelOpBound; +import prism.PrismException; + +/** + * Interface containing (some) common features of "quantitative" operators (P,R,S), + * i.e., classes ExpressionProb, ExpressionReward, ExpressionSS + */ +public interface ExpressionQuant +{ + public RelOp getRelOp(); + public Expression getExpression(); + public OpRelOpBound getRelopBoundInfo(Values constantValues) throws PrismException; +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/parser/ast/ExpressionReward.java b/prism/src/parser/ast/ExpressionReward.java index f3762ad9..473f5e37 100644 --- a/prism/src/parser/ast/ExpressionReward.java +++ b/prism/src/parser/ast/ExpressionReward.java @@ -33,7 +33,7 @@ import prism.OpRelOpBound; import prism.PrismException; import prism.PrismLangException; -public class ExpressionReward extends Expression +public class ExpressionReward extends Expression implements ExpressionQuant { Object rewardStructIndex = null; Object rewardStructIndexDiv = null; diff --git a/prism/src/parser/ast/ExpressionSS.java b/prism/src/parser/ast/ExpressionSS.java index d365eb21..460cf7ef 100644 --- a/prism/src/parser/ast/ExpressionSS.java +++ b/prism/src/parser/ast/ExpressionSS.java @@ -33,7 +33,7 @@ import prism.OpRelOpBound; import prism.PrismException; import prism.PrismLangException; -public class ExpressionSS extends Expression +public class ExpressionSS extends Expression implements ExpressionQuant { RelOp relOp = null; Expression prob = null; diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index d8083e26..216785cf 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -36,6 +36,7 @@ import java.util.List; import java.util.Vector; import parser.ast.Expression; +import parser.ast.RelOp; import dv.DoubleVector; @@ -257,11 +258,10 @@ public class MultiObjModelChecker extends PrismComponent for (int i = 0; i < opsAndBounds.probSize(); i++) { if (opsAndBounds.getProbOperator(i) != Operator.P_MAX) { - tmpOpsAndBounds.add(opsAndBounds.getProbOperator(i), opsAndBounds.getProbBound(i), opsAndBounds.getProbStepBound(i)); + tmpOpsAndBounds.add(opsAndBounds.getOpRelOpBound(i), opsAndBounds.getProbOperator(i), opsAndBounds.getProbBound(i), opsAndBounds.getProbStepBound(i)); } } - - tmpOpsAndBounds.add(Operator.R_MAX, -1.0, -1); + tmpOpsAndBounds.add(new OpRelOpBound("R", RelOp.MAX, -1.0), Operator.R_MAX, -1.0, -1); ArrayList tmprewards = new ArrayList(1); tmprewards.add(rtarget); diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index f897ac55..250871e8 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -299,7 +299,7 @@ public class NondetModelChecker extends NonProbModelChecker ArrayList targetName = new ArrayList(); List targetExprs = new ArrayList(numObjectives); for (int i = 0; i < numObjectives; i++) { - extractInfoFromMultiObjectiveOperand(expr.getOperand(i), opsAndBounds, rewardsIndex, targetName, targetExprs); + extractInfoFromMultiObjectiveOperand((ExpressionQuant) expr.getOperand(i), opsAndBounds, rewardsIndex, targetName, targetExprs); } //currently we do 1 numerical subject to booleans, or multiple numericals only @@ -507,7 +507,7 @@ public class NondetModelChecker extends NonProbModelChecker * Extract the information from the operator defining one objective of a multi-objective query, * store the info in the passed in arrays and so some checks. */ - protected void extractInfoFromMultiObjectiveOperand(Expression operand, OpsAndBoundsList opsAndBounds, List rewardsIndex, List targetName, + protected void extractInfoFromMultiObjectiveOperand(ExpressionQuant exprQuant, OpsAndBoundsList opsAndBounds, List rewardsIndex, List targetName, List targetExprs) throws PrismException { int stepBound = 0; @@ -515,12 +515,13 @@ public class NondetModelChecker extends NonProbModelChecker ExpressionReward exprReward = null; ExpressionTemporal exprTemp; RelOp relOp; - if (operand instanceof ExpressionProb) { - exprProb = (ExpressionProb) operand; + + if (exprQuant instanceof ExpressionProb) { + exprProb = (ExpressionProb) exprQuant; exprReward = null; relOp = exprProb.getRelOp(); - } else if (operand instanceof ExpressionReward) { - exprReward = (ExpressionReward) operand; + } else if (exprQuant instanceof ExpressionReward) { + exprReward = (ExpressionReward) exprQuant; exprProb = null; relOp = exprReward.getRelOp(); Object rs = exprReward.getRewardStructIndex(); @@ -567,9 +568,12 @@ public class NondetModelChecker extends NonProbModelChecker } // Get info from P/R operator + OpRelOpBound opInfo = exprQuant.getRelopBoundInfo(constantValues); + // Store relational operator - if (relOp.isStrict()) + if (opInfo.getRelOp().isStrict()) throw new PrismException("Multi-objective properties can not use strict inequalities on P/R operators"); + Operator op; if (relOp == RelOp.MAX) { op = (exprProb != null) ? Operator.P_MAX : Operator.R_MAX; @@ -592,9 +596,9 @@ public class NondetModelChecker extends NonProbModelChecker if (exprProb != null && relOp == RelOp.LEQ) p = 1 - p; - opsAndBounds.add(op, p, stepBound); + opsAndBounds.add(opInfo, op, p, stepBound); } else { - opsAndBounds.add(op, -1.0, stepBound); + opsAndBounds.add(opInfo, op, -1.0, stepBound); } // Now extract targets @@ -615,7 +619,8 @@ public class NondetModelChecker extends NonProbModelChecker for (JDDNode set : tmpecs) acceptingStates = JDD.Or(acceptingStates, set); targetDDs.add(acceptingStates); - opsAndBounds.add(Operator.P_GE, 0.0, -1); + OpRelOpBound opInfo = new OpRelOpBound("P", RelOp.GEQ, 0.0); + opsAndBounds.add(opInfo, Operator.P_GE, 0.0, -1); } //Prints info about the product model in multi-objective diff --git a/prism/src/prism/OpsAndBoundsList.java b/prism/src/prism/OpsAndBoundsList.java index d91ff2c0..8c20f476 100644 --- a/prism/src/prism/OpsAndBoundsList.java +++ b/prism/src/prism/OpsAndBoundsList.java @@ -31,8 +31,7 @@ import java.util.BitSet; import java.util.List; /** - * This class keeps lists of operators and bounds used in multi-objective - * verification. + * This class keeps lists of operators and bounds used in multi-objective verification. * * The instance keeps an ordered instance of (operator,bound) values. * These are currently held in two separate lists internally. A tuple @@ -52,6 +51,7 @@ public class OpsAndBoundsList */ private BitSet probNegated; + protected List opInfos; protected List relOps, relOpsProb, relOpsReward; protected List bounds, boundsProb, boundsReward; protected List stepBounds, stepBoundsProb, stepBoundsReward; @@ -67,20 +67,21 @@ public class OpsAndBoundsList /** * Creates an instance of the class in which the "big" lists * are allocated with size numTargets. - * @param numTargets The expected number of elements that would be added to the list. + * @param numObjectives The expected number of elements that would be added to the list. */ - public OpsAndBoundsList(int numTargets) + public OpsAndBoundsList(int numObjectives) { probNegated = new BitSet(); - relOps = new ArrayList(numTargets); - bounds = new ArrayList(numTargets); - stepBounds = new ArrayList(numTargets); + opInfos = new ArrayList(numObjectives); + relOps = new ArrayList(numObjectives); + bounds = new ArrayList(numObjectives); + stepBounds = new ArrayList(numObjectives); relOpsProb = new ArrayList(); boundsProb = new ArrayList(); - stepBoundsProb = new ArrayList(numTargets); + stepBoundsProb = new ArrayList(numObjectives); relOpsReward = new ArrayList(); boundsReward = new ArrayList(); - stepBoundsReward = new ArrayList(numTargets); + stepBoundsReward = new ArrayList(numObjectives); } /** @@ -89,8 +90,9 @@ public class OpsAndBoundsList * @param quantityBound * @param stepBound */ - public void add(Operator op, double quantityBound, int stepBound) + public void add(OpRelOpBound opInfo, Operator op, double quantityBound, int stepBound) { + opInfos.add(opInfo); relOps.add(op); bounds.add(quantityBound); stepBounds.add(stepBound); @@ -143,6 +145,14 @@ public class OpsAndBoundsList return stepBounds.get(i); } + /** + * Returns the operator/relop info at i-th position. + */ + public OpRelOpBound getOpRelOpBound(int i) + { + return opInfos.get(i); + } + /** * Returns the operator at i-th position in the subsequence containing only probabilistic * operators.