From f0a486b0c71d445feb742d5624665fa65ddc05e7 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 28 Jun 2014 17:35:25 +0000 Subject: [PATCH] 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 --- prism/src/explicit/DTMCModelChecker.java | 71 ------------------- prism/src/explicit/MDPModelChecker.java | 78 --------------------- prism/src/explicit/ProbModelChecker.java | 89 ++++++++++++++++++++++-- prism/src/explicit/STPGModelChecker.java | 77 -------------------- 4 files changed, 83 insertions(+), 232 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 580771f4..c92b6487 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -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 { diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 2f5c7ea2..b4c9cddd 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -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 { diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index dc63a4fe..29069e89 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -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); } /** diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index 2050574b..684026cc 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/prism/src/explicit/STPGModelChecker.java @@ -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 {