From 82de131735a3ed7714aa02a0d2a4daebbca89e7f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 29 Dec 2014 01:23:33 +0000 Subject: [PATCH] Small fix for previous commit. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9460 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/ProbModelChecker.java | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index d1107652..28242f22 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -521,7 +521,6 @@ public class ProbModelChecker extends NonProbModelChecker */ protected StateValues checkExpressionProb(Model model, ExpressionProb expr, boolean forAll, Coalition coalition) throws PrismException { - // Get info from P operator OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues); MinMax minMax = opInfo.getMinMax(model.getModelType()); @@ -541,7 +540,7 @@ public class ProbModelChecker extends NonProbModelChecker } // Otherwise, compare against bound to get set of satisfying states else { - BitSet sol = probs.getBitSetFromInterval(expr.getRelOp(), opInfo.getBound()); + BitSet sol = probs.getBitSetFromInterval(opInfo.getRelOp(), opInfo.getBound()); probs.clear(); return StateValues.createFromBitSet(sol, model); } @@ -761,7 +760,7 @@ public class ProbModelChecker extends NonProbModelChecker } // Otherwise, compare against bound to get set of satisfying states else { - BitSet sol = rews.getBitSetFromInterval(expr.getRelOp(), opInfo.getBound()); + BitSet sol = rews.getBitSetFromInterval(opInfo.getRelOp(), opInfo.getBound()); rews.clear(); return StateValues.createFromBitSet(sol, model); } @@ -948,7 +947,7 @@ public class ProbModelChecker extends NonProbModelChecker } // Otherwise, compare against bound to get set of satisfying states else { - BitSet sol = probs.getBitSetFromInterval(expr.getRelOp(), opInfo.getBound()); + BitSet sol = probs.getBitSetFromInterval(opInfo.getRelOp(), opInfo.getBound()); probs.clear(); return StateValues.createFromBitSet(sol, model); }