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

Further refactoring in explicit model checkers: push more duplicated code into ProbModelChecker. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8653 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 12 years ago
parent
274ef86286
commit
f0a486b0c7
4 changed files with 83 additions and 232 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. 71
      prism/src/explicit/DTMCModelChecker.java
  2. 78
      prism/src/explicit/MDPModelChecker.java
  3. 89
      prism/src/explicit/ProbModelChecker.java
  4. 77
      prism/src/explicit/STPGModelChecker.java

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

@ -57,77 +57,6 @@ public class DTMCModelChecker extends ProbModelChecker
// Model checking functions
@Override
protected StateValues checkProbNext(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
{
BitSet target = null;
ModelCheckerResult res = null;
// Model check the operand
target = checkExpression(model, expr.getOperand2()).getBitSet();
res = computeNextProbs((DTMC) model, target);
return StateValues.createFromDoubleArray(res.soln, model);
}
@Override
protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
{
int time;
BitSet b1, b2;
StateValues probs = null;
ModelCheckerResult res = null;
// get info from bounded until
time = expr.getUpperBound().evaluateInt(constantValues);
if (expr.upperBoundIsStrict())
time--;
if (time < 0) {
String bound = expr.upperBoundIsStrict() ? "<" + (time + 1) : "<=" + time;
throw new PrismException("Invalid bound " + bound + " in bounded until formula");
}
// model check operands first
b1 = checkExpression(model, expr.getOperand1()).getBitSet();
b2 = checkExpression(model, expr.getOperand2()).getBitSet();
// compute probabilities
// a trivial case: "U<=0"
if (time == 0) {
// prob is 1 in b2 states, 0 otherwise
probs = StateValues.createFromBitSetAsDoubles(b2, model);
} else {
res = computeBoundedUntilProbs((DTMC) model, b1, b2, time);
probs = StateValues.createFromDoubleArray(res.soln, model);
}
return probs;
}
@Override
protected StateValues checkProbUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
{
BitSet b1, b2;
StateValues probs = null;
ModelCheckerResult res = null;
// model check operands first
b1 = checkExpression(model, expr.getOperand1()).getBitSet();
b2 = checkExpression(model, expr.getOperand2()).getBitSet();
// print out some info about num states
// mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1,
// allDDRowVars.n()));
// mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(b2,
// allDDRowVars.n()) + " states\n");
res = computeUntilProbs((DTMC) model, b1, b2);
probs = StateValues.createFromDoubleArray(res.soln, model);
return probs;
}
@Override
protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException
{

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

@ -63,84 +63,6 @@ public class MDPModelChecker extends ProbModelChecker
// Model checking functions
@Override
protected StateValues checkProbNext(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
{
BitSet target = null;
ModelCheckerResult res = null;
// Model check the operand
target = checkExpression(model, expr.getOperand2()).getBitSet();
res = computeNextProbs((MDP) model, target, minMax.isMin());
return StateValues.createFromDoubleArray(res.soln, model);
}
@Override
protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
{
int time;
BitSet b1, b2;
StateValues probs = null;
ModelCheckerResult res = null;
// get info from bounded until
time = expr.getUpperBound().evaluateInt(constantValues);
if (expr.upperBoundIsStrict())
time--;
if (time < 0) {
String bound = expr.upperBoundIsStrict() ? "<" + (time + 1) : "<=" + time;
throw new PrismException("Invalid bound " + bound + " in bounded until formula");
}
// model check operands first
b1 = checkExpression(model, expr.getOperand1()).getBitSet();
b2 = checkExpression(model, expr.getOperand2()).getBitSet();
// print out some info about num states
// mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1,
// allDDRowVars.n()));
// mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(b2,
// allDDRowVars.n()) + " states\n");
// Compute probabilities
// a trivial case: "U<=0"
if (time == 0) {
// prob is 1 in b2 states, 0 otherwise
probs = StateValues.createFromBitSetAsDoubles(b2, model);
} else {
res = computeBoundedUntilProbs((MDP) model, b1, b2, time, minMax.isMin());
probs = StateValues.createFromDoubleArray(res.soln, model);
}
return probs;
}
@Override
protected StateValues checkProbUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
{
BitSet b1, b2;
StateValues probs = null;
ModelCheckerResult res = null;
// model check operands first
b1 = checkExpression(model, expr.getOperand1()).getBitSet();
b2 = checkExpression(model, expr.getOperand2()).getBitSet();
// print out some info about num states
// mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1,
// allDDRowVars.n()));
// mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(b2,
// allDDRowVars.n()) + " states\n");
res = computeUntilProbs((MDP) model, b1, b2, minMax.isMin());
probs = StateValues.createFromDoubleArray(res.soln, model);
result.setStrategy(res.strat);
return probs;
}
@Override
protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException
{

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

@ -571,8 +571,28 @@ public class ProbModelChecker extends NonProbModelChecker
*/
protected StateValues checkProbNext(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
{
// To be overridden by subclasses
throw new PrismException("Computation not implemented yet");
// Model check the operand
BitSet target = checkExpression(model, expr.getOperand2()).getBitSet();
// Compute/return the probabilities
ModelCheckerResult res = null;
switch (model.getModelType()) {
case CTMC:
res = ((CTMCModelChecker) this).computeNextProbs((CTMC) model, target);
break;
case DTMC:
res = ((DTMCModelChecker) this).computeNextProbs((DTMC) model, target);
break;
case MDP:
res = ((MDPModelChecker) this).computeNextProbs((MDP) model, target, minMax.isMin());
break;
case STPG:
res = ((STPGModelChecker) this).computeNextProbs((STPG) model, target, minMax.isMin1(), minMax.isMin2());
break;
default:
throw new PrismException("Cannot model check " + expr + " for " + model.getModelType() + "s");
}
return StateValues.createFromDoubleArray(res.soln, model);
}
/**
@ -580,8 +600,43 @@ public class ProbModelChecker extends NonProbModelChecker
*/
protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
{
// To be overridden by subclasses
throw new PrismException("Computation not implemented yet");
// This method just handles discrete time
// Continuous-time model checkers will override this method
// Get info from bounded until
int time = expr.getUpperBound().evaluateInt(constantValues);
if (expr.upperBoundIsStrict())
time--;
if (time < 0) {
String bound = expr.upperBoundIsStrict() ? "<" + (time + 1) : "<=" + time;
throw new PrismException("Invalid bound " + bound + " in bounded until formula");
}
// Model check operands first
BitSet b1 = checkExpression(model, expr.getOperand1()).getBitSet();
BitSet b2 = checkExpression(model, expr.getOperand2()).getBitSet();
// Compute/return the probabilities
// A trivial case: "U<=0" (prob is 1 in b2 states, 0 otherwise)
if (time == 0) {
return StateValues.createFromBitSetAsDoubles(b2, model);
}
// Otherwise: numerical solution
ModelCheckerResult res = null;
switch (model.getModelType()) {
case DTMC:
res = ((DTMCModelChecker) this).computeBoundedUntilProbs((DTMC) model, b1, b2, time);
break;
case MDP:
res = ((MDPModelChecker) this).computeBoundedUntilProbs((MDP) model, b1, b2, time, minMax.isMin());
break;
case STPG:
res = ((STPGModelChecker) this).computeBoundedUntilProbs((STPG) model, b1, b2, time, minMax.isMin1(), minMax.isMin2());
break;
default:
throw new PrismException("Cannot model check " + expr + " for " + model.getModelType() + "s");
}
return StateValues.createFromDoubleArray(res.soln, model);
}
/**
@ -589,8 +644,30 @@ public class ProbModelChecker extends NonProbModelChecker
*/
protected StateValues checkProbUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
{
// To be overridden by subclasses
throw new PrismException("Computation not implemented yet");
// Model check operands first
BitSet b1 = checkExpression(model, expr.getOperand1()).getBitSet();
BitSet b2 = checkExpression(model, expr.getOperand2()).getBitSet();
// Compute/return the probabilities
ModelCheckerResult res = null;
switch (model.getModelType()) {
case CTMC:
res = ((CTMCModelChecker) this).computeUntilProbs((CTMC) model, b1, b2);
break;
case DTMC:
res = ((DTMCModelChecker) this).computeUntilProbs((DTMC) model, b1, b2);
break;
case MDP:
res = ((MDPModelChecker) this).computeUntilProbs((MDP) model, b1, b2, minMax.isMin());
result.setStrategy(res.strat);
break;
case STPG:
res = ((STPGModelChecker) this).computeUntilProbs((STPG) model, b1, b2, minMax.isMin1(), minMax.isMin2());
break;
default:
throw new PrismException("Cannot model check " + expr + " for " + model.getModelType() + "s");
}
return StateValues.createFromDoubleArray(res.soln, model);
}
/**

77
prism/src/explicit/STPGModelChecker.java
View File

@ -55,83 +55,6 @@ public class STPGModelChecker extends ProbModelChecker
// Model checking functions
@Override
protected StateValues checkProbNext(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
{
BitSet target = null;
ModelCheckerResult res = null;
// Model check the operand
target = checkExpression(model, expr.getOperand2()).getBitSet();
res = computeNextProbs((STPG) model, target, minMax.isMin1(), minMax.isMin2());
return StateValues.createFromDoubleArray(res.soln, model);
}
@Override
protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
{
int time;
BitSet b1, b2;
StateValues probs = null;
ModelCheckerResult res = null;
// get info from bounded until
time = expr.getUpperBound().evaluateInt(constantValues);
if (expr.upperBoundIsStrict())
time--;
if (time < 0) {
String bound = expr.upperBoundIsStrict() ? "<" + (time + 1) : "<=" + time;
throw new PrismException("Invalid bound " + bound + " in bounded until formula");
}
// model check operands first
b1 = checkExpression(model, expr.getOperand1()).getBitSet();
b2 = checkExpression(model, expr.getOperand2()).getBitSet();
// print out some info about num states
// mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1,
// allDDRowVars.n()));
// mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(b2,
// allDDRowVars.n()) + " states\n");
// Compute probabilities
// a trivial case: "U<=0"
if (time == 0) {
// prob is 1 in b2 states, 0 otherwise
probs = StateValues.createFromBitSetAsDoubles(b2, model);
} else {
res = computeBoundedUntilProbs((STPG) model, b1, b2, time, minMax.isMin1(), minMax.isMin2());
probs = StateValues.createFromDoubleArray(res.soln, model);
}
return probs;
}
@Override
protected StateValues checkProbUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
{
BitSet b1, b2;
StateValues probs = null;
ModelCheckerResult res = null;
// model check operands first
b1 = checkExpression(model, expr.getOperand1()).getBitSet();
b2 = checkExpression(model, expr.getOperand2()).getBitSet();
// print out some info about num states
// mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1,
// allDDRowVars.n()));
// mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(b2,
// allDDRowVars.n()) + " states\n");
res = computeUntilProbs((STPG) model, b1, b2, minMax.isMin1(), minMax.isMin2());
probs = StateValues.createFromDoubleArray(res.soln, model);
return probs;
}
@Override
protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException
{

Write Preview
Loading…
Cancel
Save