From 96442e5a3abb25d307af1420d8127b32f9fea22d Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Sat, 16 Jun 2018 10:47:03 +0200 Subject: [PATCH] =?UTF-8?q?Statistical=20MC:=20Don't=20complain=20about=20?= =?UTF-8?q?P=3D=3F/R=3D=3F/...=20for=20nondeterministic=20models?= As the nondeterminism is resolved to generate the paths, e.g., for an MDP the model checking happens in the resulting DTMC, allow the use of the DTMC-style operators. --- prism/src/prism/Prism.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 81fa1b90..2934f0e0 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3076,7 +3076,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener } // Check that property is valid for this model type - expr.checkValid(currentModelType); + expr.checkValid(currentModelType.removeNondeterminism()); // Do simulation res = getSimulator().modelCheckSingleProperty(currentModulesFile, propertiesFile, expr, initialState, maxPathLength, simMethod); @@ -3125,7 +3125,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener // Check that properties are valid for this model type for (Expression expr : exprs) - expr.checkValid(currentModelType); + expr.checkValid(currentModelType.removeNondeterminism()); // Do simulation res = getSimulator().modelCheckMultipleProperties(currentModulesFile, propertiesFile, exprs, initialState, maxPathLength, simMethod);