From 0472c03e5ff373b298923f0f86ed1329f280d9e5 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 28 Aug 2017 12:45:46 +0200 Subject: [PATCH] Parametric / exact engine: fairness unsupported for MDPs --- prism/src/prism/Prism.java | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index a77fb29b..81bdfade 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3149,7 +3149,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener { // Some checks if (!(currentModelType == ModelType.DTMC || currentModelType == ModelType.CTMC || currentModelType == ModelType.MDP)) - throw new PrismException("Exact model checking is only supported for DTMCs, CTMCs and MDPs"); + throw new PrismNotSupportedException("Exact model checking is only supported for DTMCs, CTMCs and MDPs"); + + if (currentModelType == ModelType.MDP && getFairness()) + throw new PrismNotSupportedException("Exact model checking does not support checking MDPs under fairness"); // Set up a dummy parameter (not used) String[] paramNames = new String[] { "dummy" }; @@ -3200,7 +3203,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener throw new PrismException("Must specify some parameters when using " + "the parametric analysis"); } if (!(currentModelType == ModelType.DTMC || currentModelType == ModelType.CTMC || currentModelType == ModelType.MDP)) - throw new PrismException("Parametric model checking is only supported for DTMCs, CTMCs and MDPs"); + throw new PrismNotSupportedException("Parametric model checking is only supported for DTMCs, CTMCs and MDPs"); + + if (currentModelType == ModelType.MDP && getFairness()) + throw new PrismNotSupportedException("Parametric model checking does not support checking MDPs under fairness"); Values definedPFConstants = propertiesFile.getConstantValues(); Values constlist = currentModulesFile.getConstantValues();