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

@@ -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;
+	}
+
 }

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();