From 3d30f2c4f639bbd3cd1e1f6a593985349777d309 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Mon, 28 Aug 2017 12:45:47 +0200
Subject: [PATCH] param: Print warning if heuristic checking was used

To check that, for all parameter valuations in a region,
(1) some threshold property holds or (2) that a given
scheduler is optimal, a set of constraints is checked.

Currently, only heuristic checking is implemented, i.e., determining
via sampling if the constraints hold. This can produce false positives
in the region computations, i.e., a region is not sufficiently split.

We add a warning if the region computation relied on the heuristic
constraint check and thus can be imprecise.
---
 prism/src/param/ConstraintChecker.java | 9 +++++++++
 prism/src/param/ParamModelChecker.java | 4 ++++
 2 files changed, 13 insertions(+)

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 <emhahn@cs.ox.ac.uk> (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();