Browse Source

Bugfix: incorrect output for Pmax=?[...{max}] properties.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@193 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 19 years ago
parent
commit
b9791ec2a8
  1. 2
      prism/src/prism/NondetModelChecker.java

2
prism/src/prism/NondetModelChecker.java

@ -554,7 +554,7 @@ public class NondetModelChecker implements ModelChecker
// compute/print min info
if (pctl.filterMaxRequested()) {
maxRes = probs.maxOverBDD(filter);
mainLog.print("\nMaximum " + (min?"minimum":"maximum") + " probability for states satisfying " + pctl.getFilter() + ": " + minRes + "\n");
mainLog.print("\nMaximum " + (min?"minimum":"maximum") + " probability for states satisfying " + pctl.getFilter() + ": " + maxRes + "\n");
tmp = probs.getBDDFromInterval(maxRes-termCritParam, maxRes+termCritParam);
JDD.Ref(filter);
tmp = JDD.And(tmp, filter);

Loading…
Cancel
Save