diff --git a/prism/src/param/ConstraintChecker.java b/prism/src/param/ConstraintChecker.java index 4944d786..00902ee4 100644 --- a/prism/src/param/ConstraintChecker.java +++ b/prism/src/param/ConstraintChecker.java @@ -40,6 +40,8 @@ import java.util.HashMap; * @author Ernst Moritz Hahn (University of Oxford) */ class ConstraintChecker { + private boolean usedUnsoundCheck = false; + /** * Class to store keys for the cache of the decision procedure. */ @@ -124,6 +126,7 @@ class ConstraintChecker { */ boolean mainCheck(Region region, Function constraint, boolean strict) { + usedUnsoundCheck = true; return true; } @@ -197,4 +200,10 @@ class ConstraintChecker { return result; } + + public boolean unsoundCheckWasUsed() + { + return usedUnsoundCheck; + } + } diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index 44b86dc9..d62d4aa6 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -253,6 +253,10 @@ final public class ParamModelChecker extends PrismComponent timer = System.currentTimeMillis() - timer; mainLog.println("\nTime for model checking: " + timer / 1000.0 + " seconds."); + if (constraintChecker.unsoundCheckWasUsed()) { + mainLog.printWarning("Computation of Boolean values / parameter regions used heuristic sampling, results are potentially inaccurate."); + } + // Store result result = new Result(); vals.clearExceptInit();