From e36324ce54a54618b918db9129c9b2552e68fddf Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 17 Aug 2016 17:10:09 +0000 Subject: [PATCH] ParamModelChecker: use evaluateExact to determine the P/R operator bounds git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11640 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/param/ParamModelChecker.java | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index e02c01ed..293baa26 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -863,8 +863,7 @@ final public class ParamModelChecker extends PrismComponent relOp = expr.getRelOp(); pb = expr.getProb(); if (pb != null) { - // TODO check whether actually evaluated as such - p = modelBuilder.expr2function(functionFactory, pb).asBigRational(); + p = pb.evaluateExact(constantValues); if (p.compareTo(0) == -1 || p.compareTo(1) == 1) throw new PrismException("Invalid probability bound " + p + " in P operator"); } @@ -973,8 +972,7 @@ final public class ParamModelChecker extends PrismComponent RelOp relOp = expr.getRelOp(); rb = expr.getReward(); if (rb != null) { - // TODO check whether actually evaluated as such, take constantValues into account - r = modelBuilder.expr2function(functionFactory, rb).asBigRational(); + r = rb.evaluateExact(constantValues); if (r.compareTo(0) == -1) throw new PrismException("Invalid reward bound " + r + " in R[] formula"); } @@ -1108,8 +1106,7 @@ final public class ParamModelChecker extends PrismComponent relOp = expr.getRelOp(); pb = expr.getProb(); if (pb != null) { - // TODO check whether actually evaluated as such - p = modelBuilder.expr2function(functionFactory, pb).asBigRational(); + p = pb.evaluateExact(constantValues); if (p.compareTo(0) == -1 || p.compareTo(1) == 1) throw new PrismException("Invalid probability bound " + p + " in P operator"); }