s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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
master
Joachim Klein 9 years ago
parent
b030d707eb
commit
e36324ce54
1 changed files with 3 additions and 6 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 9
      prism/src/param/ParamModelChecker.java

9
prism/src/param/ParamModelChecker.java
View File

@ -863,8 +863,7 @@ final public class ParamModelChecker extends PrismComponent
relOp = expr.getRelOp(); relOp = expr.getRelOp();
pb = expr.getProb(); pb = expr.getProb();
if (pb != null) { 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) if (p.compareTo(0) == -1 || p.compareTo(1) == 1)
throw new PrismException("Invalid probability bound " + p + " in P operator"); throw new PrismException("Invalid probability bound " + p + " in P operator");
} }
@ -973,8 +972,7 @@ final public class ParamModelChecker extends PrismComponent
RelOp relOp = expr.getRelOp(); RelOp relOp = expr.getRelOp();
rb = expr.getReward(); rb = expr.getReward();
if (rb != null) { 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) if (r.compareTo(0) == -1)
throw new PrismException("Invalid reward bound " + r + " in R[] formula"); throw new PrismException("Invalid reward bound " + r + " in R[] formula");
} }
@ -1108,8 +1106,7 @@ final public class ParamModelChecker extends PrismComponent
relOp = expr.getRelOp(); relOp = expr.getRelOp();
pb = expr.getProb(); pb = expr.getProb();
if (pb != null) { 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) if (p.compareTo(0) == -1 || p.compareTo(1) == 1)
throw new PrismException("Invalid probability bound " + p + " in P operator"); throw new PrismException("Invalid probability bound " + p + " in P operator");
} }

Write Preview
Loading…
Cancel
Save