Tidy up output from parametric model checking.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7591 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/param/ModelBuilder.java

@@ -382,6 +382,8 @@ public final class ModelBuilder extends PrismComponent
 		}
 		model.setFunctionFactory(functionFactory);
 
+		mainLog.println();
+		
 		mainLog.print("Reachable states exploration and model construction");
 		mainLog.println(" done in " + ((System.currentTimeMillis() - timer) / 1000.0) + " secs.");
 

prism/src/param/ParamModelChecker.java

@@ -265,10 +265,20 @@ final public class ParamModelChecker extends PrismComponent
 		RegionValues vals = checkExpression(paramModel, expr, needStates);
 		timer = System.currentTimeMillis() - timer;
 		mainLog.println("\nTime for model checking: " + timer / 1000.0 + " seconds.");
+
+		// Store result
 		result = new Result();
 		vals.clearExceptInit();
 		result.setResult(vals);
-		mainLog.println(result);
+		
+		// Print result to log
+		String resultString = "Result";
+		if (!("Result".equals(expr.getResultName())))
+			resultString += " (" + expr.getResultName().toLowerCase() + ")";
+		resultString += ": " + result.getResultString();
+		mainLog.print("\n" + resultString);
+		
+		/* // Output plot to tex file
 		if (paramLower.length == 2) {
 			try {
 				FileOutputStream file = new FileOutputStream("out.tex");
@@ -281,7 +291,7 @@ final public class ParamModelChecker extends PrismComponent
 			} catch (Exception e) {
 				throw new PrismException("file could not be written");
 			}
-		}
+		}*/
 		
 		return result;
 	}

prism/src/prism/Prism.java

@@ -2887,10 +2887,21 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		if (paramNames == null) {
 			throw new PrismException("Must specify some parameters when using " + "the parametric analysis");
 		}
+
+		Values definedPFConstants = propertiesFile.getConstantValues();
 		Values constlist = currentModulesFile.getConstantValues();
 		for (int pnr = 0; pnr < paramNames.length; pnr++) {
 			constlist.removeValue(paramNames[pnr]);
 		}
+
+		// Print info
+		mainLog.printSeparator();
+		mainLog.println("\nParametric model checking: " + prop);
+		if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0)
+			mainLog.println("Model constants: " + currentDefinedMFConstants);
+		if (definedPFConstants != null && definedPFConstants.getNumValues() > 0)
+			mainLog.println("Property constants: " + definedPFConstants);
+
 		param.ModelBuilder builder = new ModelBuilder(this);
 		builder.setModulesFile(currentModulesFile);
 		builder.setParameters(paramNames, paramLowerBounds, paramUpperBounds);