From 397fc1b4aa3594fc822ef39da348daf13d09755b Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 17 Feb 2012 13:24:38 +0000 Subject: [PATCH] Tidy of explicit engine settings import, to identify some missing features. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4653 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/ProbModelChecker.java | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 7ae0a3eb..f2451e7d 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -176,22 +176,35 @@ public class ProbModelChecker extends StateModelChecker } else { throw new PrismException("Explicit engine does not support MDP solution method \"" + s + "\""); } - + // PRISM_TERM_CRIT s = settings.getString(PrismSettings.PRISM_TERM_CRIT); if (s.equals("Absolute")) { setTermCrit(TermCrit.ABSOLUTE); } else if (s.equals("Relative")) { setTermCrit(TermCrit.RELATIVE); + } else { + throw new PrismException("Unknown termination criterion \"" + s + "\""); } + // PRISM_TERM_CRIT_PARAM setTermCritParam(settings.getDouble(PrismSettings.PRISM_TERM_CRIT_PARAM)); + // PRISM_MAX_ITERS setMaxIters(settings.getInteger(PrismSettings.PRISM_MAX_ITERS)); + // PRISM_PRECOMPUTATION setPrecomp(settings.getBoolean(PrismSettings.PRISM_PRECOMPUTATION)); + // PRISM_PROB0 setProb0(settings.getBoolean(PrismSettings.PRISM_PROB0)); + // PRISM_PROB1 setProb1(settings.getBoolean(PrismSettings.PRISM_PROB1)); - // valiterdir + // PRISM_FAIRNESS + if (settings.getBoolean(PrismSettings.PRISM_FAIRNESS)) { + throw new PrismException("The explicit engine does not support model checking MDPs under fairness"); + } + + // PRISM_EXPORT_ADV s = settings.getString(PrismSettings.PRISM_EXPORT_ADV); if (!(s.equals("None"))) exportAdv = true; + // PRISM_EXPORT_ADV_FILENAME exportAdvFilename = settings.getString(PrismSettings.PRISM_EXPORT_ADV_FILENAME); }