From f24243ff507c1f284d9c5c75c3d85d55ef46c63f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 30 Jun 2014 17:59:16 +0000 Subject: [PATCH] Finish refactoring from last commit (missed something in STPG model checker). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8687 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/ProbModelChecker.java | 4 ++++ prism/src/explicit/STPGModelChecker.java | 21 --------------------- 2 files changed, 4 insertions(+), 21 deletions(-) diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 708817e9..1242f4bb 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -44,6 +44,7 @@ import explicit.rewards.ConstructRewards; import explicit.rewards.MCRewards; import explicit.rewards.MDPRewards; import explicit.rewards.Rewards; +import explicit.rewards.STPGRewards; /** * Super class for explicit-state probabilistic model checkers. @@ -808,6 +809,9 @@ public class ProbModelChecker extends NonProbModelChecker res = ((MDPModelChecker) this).computeReachRewards((MDP) model, (MDPRewards) modelRewards, target, minMax.isMin()); result.setStrategy(res.strat); break; + case STPG: + res = ((STPGModelChecker) this).computeReachRewards((STPG) model, (STPGRewards) modelRewards, target, minMax.isMin1(), minMax.isMin2()); + break; default: throw new PrismException("Explicit engine does not yet handle the " + expr.getOperatorSymbol() + " reward operator for " + model.getModelType() + "s"); diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index 684026cc..626cb28c 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/prism/src/explicit/STPGModelChecker.java @@ -32,7 +32,6 @@ import java.util.List; import java.util.Map; import parser.ast.Expression; -import parser.ast.ExpressionTemporal; import prism.PrismComponent; import prism.PrismException; import prism.PrismFileLog; @@ -61,26 +60,6 @@ public class STPGModelChecker extends ProbModelChecker throw new PrismException("LTL model checking not yet supported for stochastic games"); } - /** - * Compute rewards for the contents of an R operator. - */ - protected StateValues checkRewardFormula(Model model, STPGRewards rewards, ExpressionTemporal expr, boolean min1, boolean min2) throws PrismException - { - // Assume R [F ] for now... - - BitSet target; - StateValues rews = null; - ModelCheckerResult res = null; - - // model check operands first - target = checkExpression(model, expr.getOperand2()).getBitSet(); - - res = computeReachRewards((STPG) model, rewards, target, min1, min2); - rews = StateValues.createFromDoubleArray(res.soln, model); - - return rews; - } - // Numerical computation functions /**