From 4fc79a68fc442da3318db5922242becb91fba4cb Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 11 Dec 2018 20:57:22 +0100 Subject: [PATCH] Simulation results: Note if nondeterminism was resolved uniformly Print explanation after result to indicate uniform resolution of nondeterminism in the model by statistical model checking engine. --- prism/src/simulator/SimulatorEngine.java | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 1d985c6c..fa7d4d0e 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -1542,6 +1542,14 @@ public class SimulatorEngine extends PrismComponent } } + String resultNote = ""; + if (results.length > 0) { + ModelType currentModelType = modulesFile.getModelType(); + if (currentModelType.nondeterministic() && currentModelType.removeNondeterminism() != currentModelType) { + resultNote += " (with nondeterminism in " + currentModelType.name() + " being resolved uniformly)"; + } + } + // Display results to log if (results.length == 1) { mainLog.print("\nSimulation method parameters: "); @@ -1549,7 +1557,7 @@ public class SimulatorEngine extends PrismComponent mainLog.print("\nSimulation result details: "); mainLog.println((indices[0] == -1) ? "no simulation" : propertySamplers.get(indices[0]).getSimulationMethodResultExplanation()); if (!(results[0] instanceof PrismException)) - mainLog.println("\nResult: " + results[0]); + mainLog.println("\nResult: " + results[0] + resultNote); } else { mainLog.println("\nSimulation method parameters:"); for (int i = 0; i < results.length; i++) { @@ -1563,7 +1571,7 @@ public class SimulatorEngine extends PrismComponent } mainLog.println("\nResults:"); for (int i = 0; i < results.length; i++) - mainLog.println(exprs.get(i) + " : " + results[i]); + mainLog.println(exprs.get(i) + " : " + results[i] + resultNote); } return results;