diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index 67db7f15..44007984 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -210,13 +210,13 @@ public class CTMCModelChecker extends DTMCModelChecker /** * Compute next=state probabilities. * i.e. compute the probability of being in a state in {@code target} in the next step. - * @param dtmc The DTMC + * @param ctmc The CTMC * @param target Target states */ - public ModelCheckerResult computeNextProbs(DTMC dtmc, BitSet target) throws PrismException + public ModelCheckerResult computeNextProbs(CTMC ctmc, BitSet target) throws PrismException { mainLog.println("Building embedded DTMC..."); - DTMC dtmcEmb = ((CTMC) dtmc).buildImplicitEmbeddedDTMC(); + DTMC dtmcEmb = ctmc.buildImplicitEmbeddedDTMC(); return super.computeNextProbs(dtmcEmb, target); } @@ -224,17 +224,17 @@ public class CTMCModelChecker extends DTMCModelChecker * Compute reachability/until probabilities. * i.e. compute the probability of reaching a state in {@code target}, * while remaining in those in @{code remain}. - * @param dtmc The CTMC + * @param ctmc The CTMC * @param remain Remain in these states (optional: null means "all") * @param target Target states * @param init Optionally, an initial solution vector (may be overwritten) * @param known Optionally, a set of states for which the exact answer is known * Note: if 'known' is specified (i.e. is non-null, 'init' must also be given and is used for the exact values. */ - public ModelCheckerResult computeReachProbs(DTMC dtmc, BitSet remain, BitSet target, double init[], BitSet known) throws PrismException + public ModelCheckerResult computeReachProbs(CTMC ctmc, BitSet remain, BitSet target, double init[], BitSet known) throws PrismException { mainLog.println("Building embedded DTMC..."); - DTMC dtmcEmb = ((CTMC) dtmc).buildImplicitEmbeddedDTMC(); + DTMC dtmcEmb = ctmc.buildImplicitEmbeddedDTMC(); return super.computeReachProbs(dtmcEmb, remain, target, init, known); } @@ -398,8 +398,7 @@ public class CTMCModelChecker extends DTMCModelChecker * @param mcRewards The rewards * @param t Time bound */ - @Override - public ModelCheckerResult computeCumulativeRewards(DTMC dtmc, MCRewards mcRewards, double t) throws PrismException + public ModelCheckerResult computeCumulativeRewards(CTMC ctmc, MCRewards mcRewards, double t) throws PrismException { ModelCheckerResult res = null; int i, n, iters; @@ -413,7 +412,7 @@ public class CTMCModelChecker extends DTMCModelChecker // Optimisation: If t = 0, this is easy. if (t == 0) { res = new ModelCheckerResult(); - res.soln = new double[dtmc.getNumStates()]; + res.soln = new double[ctmc.getNumStates()]; return res; } @@ -421,8 +420,6 @@ public class CTMCModelChecker extends DTMCModelChecker timer = System.currentTimeMillis(); mainLog.println("\nStarting backwards cumulative rewards computation..."); - CTMC ctmc = (CTMC) dtmc; - // Store num states n = ctmc.getNumStates(); @@ -455,7 +452,7 @@ public class CTMCModelChecker extends DTMCModelChecker mainLog.println("Fox-Glynn (" + acc + "): left = " + left + ", right = " + right); // Build (implicit) uniformised DTMC - dtmc = ctmc.buildImplicitUniformisedDTMC(q); + DTMC dtmcUnif = ctmc.buildImplicitUniformisedDTMC(q); // Create solution vector(s) soln = new double[n]; @@ -479,7 +476,7 @@ public class CTMCModelChecker extends DTMCModelChecker iters = 1; while (iters <= right) { // Matrix-vector multiply - dtmc.mvMult(soln, soln2, null, false); + dtmcUnif.mvMult(soln, soln2, null, false); // Swap vectors for next iter tmpsoln = soln; soln = soln2; @@ -618,21 +615,21 @@ public class CTMCModelChecker extends DTMCModelChecker /** * Compute expected reachability rewards. - * @param dtmc The CTMC + * @param ctmc The CTMC * @param mcRewards The rewards * @param target Target states */ - public ModelCheckerResult computeReachRewards(DTMC dtmc, MCRewards mcRewards, BitSet target) throws PrismException + public ModelCheckerResult computeReachRewards(CTMC ctmc, MCRewards mcRewards, BitSet target) throws PrismException { int i, n; // Build embedded DTMC mainLog.println("Building embedded DTMC..."); - DTMC dtmcEmb = ((CTMC) dtmc).buildImplicitEmbeddedDTMC(); + DTMC dtmcEmb = ctmc.buildImplicitEmbeddedDTMC(); // Convert rewards - n = dtmc.getNumStates(); + n = ctmc.getNumStates(); StateRewardsArray rewEmb = new StateRewardsArray(n); for (i = 0; i < n; i++) { - rewEmb.setStateReward(i, mcRewards.getStateReward(i) / ((CTMC) dtmc).getExitRate(i)); + rewEmb.setStateReward(i, mcRewards.getStateReward(i) / ctmc.getExitRate(i)); } // Do computation on DTMC return super.computeReachRewards(dtmcEmb, rewEmb, target); diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index c92b6487..94f0a657 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -33,7 +33,6 @@ import java.util.Map; import java.util.Vector; import parser.ast.Expression; -import parser.ast.ExpressionTemporal; import parser.type.TypeDouble; import prism.DRA; import prism.Pair; @@ -95,7 +94,6 @@ public class DTMCModelChecker extends ProbModelChecker Pair pair = mcLtl.constructProductMC(dra, (DTMC) model, labelBS); modelProduct = pair.first; int invMap[] = pair.second; - int modelProductSize = modelProduct.getNumStates(); mainLog.print("\n" + modelProduct.infoStringTable()); // Find accepting BSCCs + compute reachability probabilities @@ -123,100 +121,6 @@ public class DTMCModelChecker extends ProbModelChecker return probs; } - /** - * Compute rewards for the contents of an R operator. - */ - protected StateValues checkRewardFormula(Model model, MCRewards modelRewards, Expression expr) throws PrismException - { - StateValues rewards = null; - - if (expr instanceof ExpressionTemporal) { - ExpressionTemporal exprTemp = (ExpressionTemporal) expr; - switch (exprTemp.getOperator()) { - case ExpressionTemporal.R_F: - rewards = checkRewardReach(model, modelRewards, exprTemp); - break; - case ExpressionTemporal.R_I: - rewards = checkRewardInstantaneous(model, modelRewards, exprTemp); - break; - case ExpressionTemporal.R_C: - rewards = checkRewardCumulative(model, modelRewards, exprTemp); - break; - default: - throw new PrismException("Explicit engine does not yet handle the " + exprTemp.getOperatorSymbol() + " operator in the R operator"); - } - } - - if (rewards == null) - throw new PrismException("Unrecognised operator in R operator"); - - return rewards; - } - - /** - * Compute rewards for a reachability reward operator. - */ - protected StateValues checkRewardReach(Model model, MCRewards modelRewards, ExpressionTemporal expr) throws PrismException - { - BitSet b; - StateValues rewards = null; - ModelCheckerResult res = null; - - // model check operand first - b = checkExpression(model, expr.getOperand2()).getBitSet(); - - // print out some info about num states - // mainLog.print("\nb = " + JDD.GetNumMintermsString(b1, - // allDDRowVars.n())); - - res = computeReachRewards((DTMC) model, modelRewards, b); - rewards = StateValues.createFromDoubleArray(res.soln, model); - - return rewards; - } - - /** - * Compute rewards for an instantaneous reward operator. - */ - protected StateValues checkRewardInstantaneous(Model model, MCRewards modelRewards, ExpressionTemporal expr) throws PrismException - { - StateValues rewards = null; - ModelCheckerResult res = null; - - // get time bound - double t = expr.getUpperBound().evaluateDouble(constantValues); - - // print out some info about num states - // mainLog.print("\nb = " + JDD.GetNumMintermsString(b1, - // allDDRowVars.n())); - - res = computeInstantaneousRewards((DTMC) model, modelRewards, t); - rewards = StateValues.createFromDoubleArray(res.soln, model); - - return rewards; - } - - /** - * Compute rewards for a cumulative reward operator. - */ - protected StateValues checkRewardCumulative(Model model, MCRewards modelRewards, ExpressionTemporal expr) throws PrismException - { - StateValues rewards = null; - ModelCheckerResult res = null; - - // get time bound - double t = expr.getUpperBound().evaluateDouble(constantValues); - - // print out some info about num states - // mainLog.print("\nb = " + JDD.GetNumMintermsString(b1, - // allDDRowVars.n())); - - res = computeCumulativeRewards((DTMC) model, modelRewards, t); - rewards = StateValues.createFromDoubleArray(res.soln, model); - - return rewards; - } - public ModelCheckerResult computeInstantaneousRewards(DTMC dtmc, MCRewards mcRewards, double t) throws PrismException { ModelCheckerResult res = null; @@ -312,25 +216,6 @@ public class DTMCModelChecker extends ProbModelChecker return res; } - /** - * Compute steady-state probabilities for an S operator. - */ - protected StateValues checkSteadyStateFormula(Model model, Expression expr) throws PrismException - { - BitSet b; - StateValues probs = null; - ModelCheckerResult res = null; - - // Model check operand first - b = checkExpression(model, expr).getBitSet(); - - double multProbs[] = Utils.bitsetToDoubleArray(b, model.getNumStates()); - res = computeSteadyStateBackwardsProbs((DTMC) model, multProbs); - probs = StateValues.createFromDoubleArray(res.soln, model); - - return probs; - } - // Steady-state/transient probability computation /** diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index b4c9cddd..4aef3652 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -33,8 +33,6 @@ import java.util.Map; import java.util.Vector; import parser.ast.Expression; -import parser.ast.ExpressionTemporal; -import parser.type.TypeDouble; import prism.DRA; import prism.Pair; import prism.PrismComponent; @@ -106,7 +104,6 @@ public class MDPModelChecker extends ProbModelChecker Pair pair = mcLtl.constructProductMDP(dra, (MDP) model, labelBS); modelProduct = pair.first; int invMap[] = pair.second; - int modelProductSize = modelProduct.getNumStates(); // Find accepting MECs + compute reachability probabilities mainLog.println("\nFinding accepting MECs..."); @@ -139,93 +136,6 @@ public class MDPModelChecker extends ProbModelChecker return probs; } - /** - * Compute rewards for the contents of an R operator. - */ - protected StateValues checkRewardFormula(NondetModel model, MDPRewards modelRewards, Expression expr, boolean min) throws PrismException - { - StateValues rewards = null; - - if (expr instanceof ExpressionTemporal) { - ExpressionTemporal exprTemp = (ExpressionTemporal) expr; - switch (exprTemp.getOperator()) { - case ExpressionTemporal.R_C: - rewards = checkRewardCumul(model, modelRewards, exprTemp, min); - break; - case ExpressionTemporal.R_F: - rewards = checkRewardReach(model, modelRewards, exprTemp, min); - break; - default: - throw new PrismException("Explicit engine does not yet handle the " + exprTemp.getOperatorSymbol() + " operator in the R operator"); - } - } - - if (rewards == null) - throw new PrismException("Unrecognised operator in R operator"); - - return rewards; - } - - /** - * Compute rewards for a cumulative reward operator. - */ - protected StateValues checkRewardCumul(NondetModel model, MDPRewards modelRewards, ExpressionTemporal expr, boolean min) throws PrismException - { - int time; // time - StateValues rewards = null; - ModelCheckerResult res = null; - - // check that there is an upper time bound - if (expr.getUpperBound() == null) { - throw new PrismException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries"); - } - - // get info from inst reward - time = expr.getUpperBound().evaluateInt(constantValues); - if (time < 0) { - throw new PrismException("Invalid time bound " + time + " in cumulative reward formula"); - } - - // a trivial case: "<=0" - if (time == 0) { - rewards = new StateValues(TypeDouble.getInstance(), model.getNumStates(), new Double(0)); - } else { - // compute rewards - try { - res = computeCumulRewards((MDP) model, modelRewards, time, min); - rewards = StateValues.createFromDoubleArray(res.soln, model); - result.setStrategy(res.strat); - } catch (PrismException e) { - throw e; - } - } - - return rewards; - } - - /** - * Compute rewards for a reachability reward operator. - */ - protected StateValues checkRewardReach(NondetModel model, MDPRewards modelRewards, ExpressionTemporal expr, boolean min) throws PrismException - { - BitSet b; - StateValues rewards = null; - ModelCheckerResult res = null; - - // model check operand first - b = checkExpression(model, expr.getOperand2()).getBitSet(); - - // print out some info about num states - // mainLog.print("\nb = " + JDD.GetNumMintermsString(b1, - // allDDRowVars.n())); - - res = computeReachRewards((MDP) model, modelRewards, b, min); - rewards = StateValues.createFromDoubleArray(res.soln, model); - result.setStrategy(res.strat); - - return rewards; - } - // Numerical computation functions /** @@ -1148,7 +1058,7 @@ public class MDPModelChecker extends ProbModelChecker * @param target Target states * @param min Min or max rewards (true=min, false=max) */ - public ModelCheckerResult computeCumulRewards(MDP mdp, MDPRewards mdpRewards, int k, boolean min) throws PrismException + public ModelCheckerResult computeCumulativeRewards(MDP mdp, MDPRewards mdpRewards, int k, boolean min) throws PrismException { ModelCheckerResult res = null; int i, n, iters; diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 9cf828ac..708817e9 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -36,13 +36,14 @@ import parser.ast.ExpressionTemporal; import parser.ast.ExpressionUnaryOp; import parser.ast.RelOp; import parser.ast.RewardStruct; -import prism.ModelType; +import parser.type.TypeDouble; import prism.PrismComponent; import prism.PrismException; import prism.PrismSettings; import explicit.rewards.ConstructRewards; import explicit.rewards.MCRewards; import explicit.rewards.MDPRewards; +import explicit.rewards.Rewards; /** * Super class for explicit-state probabilistic model checkers. @@ -71,7 +72,7 @@ public class ProbModelChecker extends NonProbModelChecker // Method used for numerical solution protected SolnMethod solnMethod = SolnMethod.VALUE_ITERATION; // Is non-convergence of an iterative method an error? - protected boolean errorOnNonConverge = true; + protected boolean errorOnNonConverge = true; // Adversary export protected boolean exportAdv = false; protected String exportAdvFilename; @@ -208,7 +209,7 @@ public class ProbModelChecker extends NonProbModelChecker if (settings.getBoolean(PrismSettings.PRISM_FAIRNESS)) { throw new PrismException("The explicit engine does not support model checking MDPs under fairness"); } - + // PRISM_EXPORT_ADV s = settings.getString(PrismSettings.PRISM_EXPORT_ADV); if (!(s.equals("None"))) @@ -217,7 +218,7 @@ public class ProbModelChecker extends NonProbModelChecker setExportAdvFilename(settings.getString(PrismSettings.PRISM_EXPORT_ADV_FILENAME)); } } - + // Settings methods /** @@ -362,12 +363,12 @@ public class ProbModelChecker extends NonProbModelChecker { this.exportAdv = exportAdv; } - + public void setExportAdvFilename(String exportAdvFilename) { this.exportAdvFilename = exportAdvFilename; } - + // Get methods for flags/settings public int getVerbosity() @@ -450,7 +451,7 @@ public class ProbModelChecker extends NonProbModelChecker } // S operator else if (expr instanceof ExpressionSS) { - res = checkExpressionSteadyState(model, (ExpressionSS) expr); + res = checkExpressionSteadyState(model, (ExpressionSS) expr); } // Otherwise, use the superclass else { @@ -468,10 +469,9 @@ public class ProbModelChecker extends NonProbModelChecker Expression pb; // Probability bound (expression) double p = 0; // Probability bound (actual value) RelOp relOp; // Relational operator - StateValues probs = null; - // Get info from prob operator + // Get info from P operator relOp = expr.getRelOp(); pb = expr.getProb(); if (pb != null) { @@ -483,7 +483,7 @@ public class ProbModelChecker extends NonProbModelChecker // Compute probabilities 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"); @@ -594,7 +594,7 @@ public class ProbModelChecker extends NonProbModelChecker } return StateValues.createFromDoubleArray(res.soln, model); } - + /** * Compute probabilities for a bounded until operator. */ @@ -612,7 +612,7 @@ public class ProbModelChecker extends NonProbModelChecker throw new PrismException("Invalid bound " + bound + " in bounded until formula"); } - // Model check operands first + // Model check operands BitSet remain = checkExpression(model, expr.getOperand1()).getBitSet(); BitSet target = checkExpression(model, expr.getOperand2()).getBitSet(); @@ -638,13 +638,13 @@ public class ProbModelChecker extends NonProbModelChecker } return StateValues.createFromDoubleArray(res.soln, model); } - + /** * Compute probabilities for an (unbounded) until operator. */ protected StateValues checkProbUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException { - // Model check operands first + // Model check operands BitSet remain = checkExpression(model, expr.getOperand1()).getBitSet(); BitSet target = checkExpression(model, expr.getOperand2()).getBitSet(); @@ -669,7 +669,7 @@ public class ProbModelChecker extends NonProbModelChecker } return StateValues.createFromDoubleArray(res.soln, model); } - + /** * Compute probabilities for an LTL path formula */ @@ -678,7 +678,7 @@ public class ProbModelChecker extends NonProbModelChecker // 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. */ @@ -689,14 +689,11 @@ public class ProbModelChecker extends NonProbModelChecker Expression rb; // Reward bound (expression) double r = 0; // Reward bound (actual value) RelOp relOp; // Relational operator - boolean min = false; // For nondeterministic models, are we finding min (true) or max (false) rewards - ModelType modelType = model.getModelType(); StateValues rews = null; - MCRewards mcRewards = null; - MDPRewards mdpRewards = null; + Rewards rewards = null; int i; - // Get info from reward operator + // Get info from R operator rs = expr.getRewardStructIndex(); relOp = expr.getRelOp(); rb = expr.getReward(); @@ -705,7 +702,6 @@ public class ProbModelChecker extends NonProbModelChecker if (r < 0) throw new PrismException("Invalid reward bound " + r + " in R[] formula"); } - min = relOp.isLowerBound() || relOp.isMin(); // Get reward info if (modulesFile == null) @@ -725,36 +721,25 @@ public class ProbModelChecker extends NonProbModelChecker throw new PrismException("Invalid reward structure index \"" + rs + "\""); // Build rewards + mainLog.println("Building reward structure..."); ConstructRewards constructRewards = new ConstructRewards(mainLog); - switch (modelType) { + switch (model.getModelType()) { case CTMC: case DTMC: - mcRewards = constructRewards.buildMCRewardStructure((DTMC) model, rewStruct, constantValues); + rewards = constructRewards.buildMCRewardStructure((DTMC) model, rewStruct, constantValues); break; case MDP: - mdpRewards = constructRewards.buildMDPRewardStructure((MDP) model, rewStruct, constantValues); + rewards = constructRewards.buildMDPRewardStructure((MDP) model, rewStruct, constantValues); break; default: - throw new PrismException("Cannot build rewards for " + modelType + "s"); + throw new PrismException("Cannot build rewards for " + model.getModelType() + "s"); } // Compute rewards - mainLog.println("Building reward structure..."); - switch (modelType) { - case CTMC: - rews = ((CTMCModelChecker) this).checkRewardFormula(model, mcRewards, expr.getExpression()); - break; - case DTMC: - rews = ((DTMCModelChecker) this).checkRewardFormula(model, mcRewards, expr.getExpression()); - break; - case MDP: - rews = ((MDPModelChecker) this).checkRewardFormula((NondetModel) model, mdpRewards, expr.getExpression(), min); - break; - default: - throw new PrismException("Cannot model check " + expr + " for " + modelType + "s"); - } + MinMax minMax = (relOp.isLowerBound() || relOp.isMin()) ? MinMax.min() : MinMax.max(); + rews = checkRewardFormula(model, rewards, expr.getExpression(), minMax); - // Print out probabilities + // Print out rewards if (getVerbosity() > 5) { mainLog.print("\nRewards (non-zero only) for all states:\n"); rews.print(mainLog); @@ -772,6 +757,139 @@ public class ProbModelChecker extends NonProbModelChecker } } + /** + * Compute rewards for the contents of an R operator. + */ + protected StateValues checkRewardFormula(Model model, Rewards modelRewards, Expression expr, MinMax minMax) throws PrismException + { + StateValues rewards = null; + + if (expr instanceof ExpressionTemporal) { + ExpressionTemporal exprTemp = (ExpressionTemporal) expr; + switch (exprTemp.getOperator()) { + case ExpressionTemporal.R_F: + rewards = checkRewardReach(model, modelRewards, exprTemp, minMax); + break; + case ExpressionTemporal.R_I: + rewards = checkRewardInstantaneous(model, modelRewards, exprTemp, minMax); + break; + case ExpressionTemporal.R_C: + rewards = checkRewardCumulative(model, modelRewards, exprTemp, minMax); + break; + default: + throw new PrismException("Explicit engine does not yet handle the " + exprTemp.getOperatorSymbol() + " reward operator"); + } + } + + if (rewards == null) + throw new PrismException("Unrecognised operator in R operator"); + + return rewards; + } + + /** + * Compute rewards for a reachability reward operator. + */ + protected StateValues checkRewardReach(Model model, Rewards modelRewards, ExpressionTemporal expr, MinMax minMax) throws PrismException + { + // Model check the operand + BitSet target = checkExpression(model, expr.getOperand2()).getBitSet(); + + // Compute/return the rewards + ModelCheckerResult res = null; + switch (model.getModelType()) { + case DTMC: + res = ((DTMCModelChecker) this).computeReachRewards((DTMC) model, (MCRewards) modelRewards, target); + break; + case CTMC: + res = ((CTMCModelChecker) this).computeReachRewards((CTMC) model, (MCRewards) modelRewards, target); + break; + case MDP: + res = ((MDPModelChecker) this).computeReachRewards((MDP) model, (MDPRewards) modelRewards, target, minMax.isMin()); + result.setStrategy(res.strat); + break; + default: + throw new PrismException("Explicit engine does not yet handle the " + expr.getOperatorSymbol() + " reward operator for " + model.getModelType() + + "s"); + } + return StateValues.createFromDoubleArray(res.soln, model); + } + + /** + * Compute rewards for an instantaneous reward operator. + */ + protected StateValues checkRewardInstantaneous(Model model, Rewards modelRewards, ExpressionTemporal expr, MinMax minMax) throws PrismException + { + // Get time bound + double t = expr.getUpperBound().evaluateDouble(constantValues); + + // Compute/return the rewards + ModelCheckerResult res = null; + switch (model.getModelType()) { + case DTMC: + res = ((DTMCModelChecker) this).computeInstantaneousRewards((DTMC) model, (MCRewards) modelRewards, t); + break; + case CTMC: + res = ((CTMCModelChecker) this).computeInstantaneousRewards((CTMC) model, (MCRewards) modelRewards, t); + break; + default: + throw new PrismException("Explicit engine does not yet handle the " + expr.getOperatorSymbol() + " reward operator for " + model.getModelType() + + "s"); + } + return StateValues.createFromDoubleArray(res.soln, model); + } + + /** + * Compute rewards for a cumulative reward operator. + */ + protected StateValues checkRewardCumulative(Model model, Rewards modelRewards, ExpressionTemporal expr, MinMax minMax) throws PrismException + { + int timeInt = -1; + double timeDouble = -1; + + // Check that there is an upper time bound + if (expr.getUpperBound() == null) { + throw new PrismException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries"); + } + + // Get time bound + if (model.getModelType().continuousTime()) { + timeDouble = expr.getUpperBound().evaluateDouble(constantValues); + if (timeDouble < 0) { + throw new PrismException("Invalid time bound " + timeDouble + " in cumulative reward formula"); + } + } else { + timeInt = expr.getUpperBound().evaluateInt(constantValues); + if (timeInt < 0) { + throw new PrismException("Invalid time bound " + timeInt + " in cumulative reward formula"); + } + } + + // Compute/return the rewards + // A trivial case: "C<=0" (prob is 1 in target states, 0 otherwise) + if (timeInt == 0 || timeDouble == 0) { + return new StateValues(TypeDouble.getInstance(), model.getNumStates(), new Double(0)); + } + // Otherwise: numerical solution + ModelCheckerResult res = null; + switch (model.getModelType()) { + case DTMC: + res = ((DTMCModelChecker) this).computeCumulativeRewards((DTMC) model, (MCRewards) modelRewards, timeInt); + break; + case CTMC: + res = ((CTMCModelChecker) this).computeCumulativeRewards((CTMC) model, (MCRewards) modelRewards, timeDouble); + break; + case MDP: + res = ((MDPModelChecker) this).computeCumulativeRewards((MDP) model, (MDPRewards) modelRewards, timeInt, minMax.isMin()); + result.setStrategy(res.strat); + break; + default: + throw new PrismException("Explicit engine does not yet handle the " + expr.getOperatorSymbol() + " reward operator for " + model.getModelType() + + "s"); + } + return StateValues.createFromDoubleArray(res.soln, model); + } + /** * Model check an S operator expression and return the values for all states. */ @@ -780,11 +898,9 @@ public class ProbModelChecker extends NonProbModelChecker Expression pb; // Probability bound (expression) double p = 0; // Probability bound (actual value) RelOp relOp; // Relational operator - ModelType modelType = model.getModelType(); - StateValues probs = null; - // Get info from prob operator + // Get info from S operator relOp = expr.getRelOp(); pb = expr.getProb(); if (pb != null) { @@ -793,19 +909,9 @@ public class ProbModelChecker extends NonProbModelChecker throw new PrismException("Invalid probability bound " + p + " in P operator"); } - // Compute probabilities - switch (modelType) { - case CTMC: - //probs = ((CTMCModelChecker) this).checkSteadyStateFormula(model, expr.getExpression()); - //break; - throw new PrismException("Explicit engine does not yet support the S operator for CTMCs"); - case DTMC: - probs = ((DTMCModelChecker) this).checkSteadyStateFormula(model, expr.getExpression()); - break; - default: - throw new PrismException("Cannot model check " + expr + " for a " + modelType); - } + MinMax minMax = (relOp.isLowerBound() || relOp.isMin()) ? MinMax.min() : MinMax.max(); + probs = checkSteadyStateFormula(model, expr.getExpression(), minMax); // Print out probabilities if (getVerbosity() > 5) { @@ -824,4 +930,25 @@ public class ProbModelChecker extends NonProbModelChecker return StateValues.createFromBitSet(sol, model); } } + + /** + * Compute steady-state probabilities for an S operator. + */ + protected StateValues checkSteadyStateFormula(Model model, Expression expr, MinMax minMax) throws PrismException + { + // Model check operand + BitSet b = checkExpression(model, expr).getBitSet(); + + // Compute/return the probabilities + ModelCheckerResult res = null; + switch (model.getModelType()) { + case DTMC: + double multProbs[] = Utils.bitsetToDoubleArray(b, model.getNumStates()); + res = ((DTMCModelChecker) this).computeSteadyStateBackwardsProbs((DTMC) model, multProbs); + break; + default: + throw new PrismException("Explicit engine does not yet handle the S operator for " + model.getModelType() + "s"); + } + return StateValues.createFromDoubleArray(res.soln, model); + } }