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