From 5b0d6b0a6b1a42d88001bb81c9e1ac32a0a8a679 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:25:23 +0200 Subject: [PATCH] imported patch explicit-fairness-warning.patch --- prism/src/explicit/CTMDPModelChecker.java | 6 ++++++ prism/src/explicit/MDPModelChecker.java | 5 +++++ prism/src/explicit/ProbModelChecker.java | 4 ---- prism/src/explicit/STPGModelChecker.java | 6 ++++++ 4 files changed, 17 insertions(+), 4 deletions(-) diff --git a/prism/src/explicit/CTMDPModelChecker.java b/prism/src/explicit/CTMDPModelChecker.java index e49accfc..2f06113e 100644 --- a/prism/src/explicit/CTMDPModelChecker.java +++ b/prism/src/explicit/CTMDPModelChecker.java @@ -34,6 +34,7 @@ import parser.ast.ExpressionTemporal; import prism.PrismComponent; import prism.PrismException; import prism.PrismNotSupportedException; +import prism.PrismSettings; /** * Explicit-state model checker for continuous-time Markov decision processes (CTMDPs). @@ -46,6 +47,11 @@ public class CTMDPModelChecker extends ProbModelChecker public CTMDPModelChecker(PrismComponent parent) throws PrismException { super(parent); + + // PRISM_FAIRNESS + if (settings != null && settings.getBoolean(PrismSettings.PRISM_FAIRNESS)) { + throw new PrismNotSupportedException("The explicit engine does not support model checking CTMDPs under fairness"); + } } // Model checking functions diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index ac95bca0..623095f3 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -79,6 +79,11 @@ public class MDPModelChecker extends ProbModelChecker public MDPModelChecker(PrismComponent parent) throws PrismException { super(parent); + + // PRISM_FAIRNESS + if (settings != null && settings.getBoolean(PrismSettings.PRISM_FAIRNESS)) { + throw new PrismNotSupportedException("The explicit engine does not support model checking MDPs under fairness"); + } } // Model checking functions diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 8a0bfae2..68c8c20c 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -233,10 +233,6 @@ public class ProbModelChecker extends NonProbModelChecker setProb1(settings.getBoolean(PrismSettings.PRISM_PROB1)); // PRISM_USE_PRE setPreRel(settings.getBoolean(PrismSettings.PRISM_PRE_REL)); - // PRISM_FAIRNESS - if (settings.getBoolean(PrismSettings.PRISM_FAIRNESS)) { - throw new PrismNotSupportedException("The explicit engine does not support model checking MDPs under fairness"); - } // PRISM_EXPORT_ADV s = settings.getString(PrismSettings.PRISM_EXPORT_ADV); diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index 2e1bc463..85577693 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/prism/src/explicit/STPGModelChecker.java @@ -39,6 +39,7 @@ import prism.PrismException; import prism.PrismFileLog; import prism.PrismLog; import prism.PrismNotSupportedException; +import prism.PrismSettings; import prism.PrismUtils; import explicit.rewards.STPGRewards; @@ -53,6 +54,11 @@ public class STPGModelChecker extends ProbModelChecker public STPGModelChecker(PrismComponent parent) throws PrismException { super(parent); + + // PRISM_FAIRNESS + if (settings != null && settings.getBoolean(PrismSettings.PRISM_FAIRNESS)) { + throw new PrismNotSupportedException("The explicit engine does not support model checking STGPs under fairness"); + } } // Model checking functions