s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Refactor explicit engine model checking of reward and steady state operators, as done recently for probabilistic stuff. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8686 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 12 years ago
parent
f67aee8fca
commit
22e7009d7b
4 changed files with 199 additions and 280 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 33
      prism/src/explicit/CTMCModelChecker.java
  2. 115
      prism/src/explicit/DTMCModelChecker.java
  3. 92
      prism/src/explicit/MDPModelChecker.java
  4. 239
      prism/src/explicit/ProbModelChecker.java

33
prism/src/explicit/CTMCModelChecker.java
View File

@ -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);

115
prism/src/explicit/DTMCModelChecker.java
View File

@ -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<Model, int[]> 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
/**

92
prism/src/explicit/MDPModelChecker.java
View File

@ -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<NondetModel, int[]> 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;

239
prism/src/explicit/ProbModelChecker.java
View File

@ -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);
}
}
Write Preview
Loading…
Cancel
Save