diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 380dfc77..81fa1b90 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3071,6 +3071,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener if (definedPFConstants != null && definedPFConstants.getNumValues() > 0) mainLog.println("Property constants: " + definedPFConstants); + if (currentModelType.nondeterministic() && currentModelType.removeNondeterminism() != currentModelType) { + mainLog.printWarning("For simulation, nondeterminism in " + currentModelType + " is resolved uniformly (resulting in " + currentModelType.removeNondeterminism() + ")."); + } + // Check that property is valid for this model type expr.checkValid(currentModelType); @@ -3115,6 +3119,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener if (definedPFConstants != null && definedPFConstants.getNumValues() > 0) mainLog.println("Property constants: " + definedPFConstants); + if (currentModelType.nondeterministic() && currentModelType.removeNondeterminism() != currentModelType) { + mainLog.printWarning("For simulation, nondeterminism in " + currentModelType + " is resolved uniformly (resulting in " + currentModelType.removeNondeterminism() + ")."); + } + // Check that properties are valid for this model type for (Expression expr : exprs) expr.checkValid(currentModelType);