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