From 7bb4d897a3733453a89f8903b87f46cb7758129e Mon Sep 17 00:00:00 2001 From: nicodelpiano Date: Wed, 17 Aug 2016 20:12:08 -0300 Subject: [PATCH] Several bugfixes. --- prism/src/explicit/ProbModelChecker.java | 2 +- prism/src/prism/Prism.java | 2 +- prism/src/prism/PrismSettings.java | 12 ++++++------ 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 13a0d9ef3..6e75aedf3 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -222,7 +222,7 @@ public ProbModelChecker(PrismComponent parent) throws PrismException // PRISM_MAX_ITERS setMaxIters(settings.getInteger(PrismSettings.PRISM_MAX_ITERS)); // PRISM_PRECISION - setPrecision(settings.getInteger(PrismSettings.PRISM_PRECISION)); + setPrecision(settings.getInteger(PrismSettings.PRISM_EXACTLP_PRECISION)); // PRISM_PRECOMPUTATION setPrecomp(settings.getBoolean(PrismSettings.PRISM_PRECOMPUTATION)); // PRISM_PROB0 diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 574eee7df..70500718f 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2787,7 +2787,7 @@ public Result modelCheck(PropertiesFile propertiesFile, Property prop) throws Pr } // For exact model checking - if (settings.getBoolean(PrismSettings.PRISM_EXACT_ENABLED) && !settings.getBoolean(PrismSettings.PRISM_EXACT_LP_ENABLED)) { + if (settings.getBoolean(PrismSettings.PRISM_EXACT_ENABLED) && !settings.getBoolean(PrismSettings.PRISM_EXACTLP_ENABLED)) { return modelCheckExact(propertiesFile, prop); } // For fast adaptive uniformisation diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 3a91ddf1d..db94233ec 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -89,7 +89,7 @@ public class PrismSettings implements Observer public static final String PRISM_TERM_CRIT = "prism.termCrit";//"prism.termination"; public static final String PRISM_TERM_CRIT_PARAM = "prism.termCritParam";//"prism.terminationEpsilon"; public static final String PRISM_MAX_ITERS = "prism.maxIters";//"prism.maxIterations"; - public static final String PRISM_PRECISION = "prism.precision";//"prism.precision"; + public static final String PRISM_EXACTLP_PRECISION = "prism.exactlpPrecision";//"prism.exactlpPrecision"; public static final String PRISM_CUDD_MAX_MEM = "prism.cuddMaxMem"; public static final String PRISM_CUDD_EPSILON = "prism.cuddEpsilon"; @@ -103,7 +103,7 @@ public class PrismSettings implements Observer public static final String PRISM_SCC_METHOD = "prism.sccMethod"; public static final String PRISM_SYMM_RED_PARAMS = "prism.symmRedParams"; public static final String PRISM_EXACT_ENABLED = "prism.exact.enabled"; - public static final String PRISM_EXACT_LP_ENABLED = "prism.exact.enabled"; + public static final String PRISM_EXACTLP_ENABLED = "prism.exactlp.enabled"; public static final String PRISM_PTA_METHOD = "prism.ptaMethod"; public static final String PRISM_TRANSIENT_METHOD = "prism.transientMethod"; public static final String PRISM_AR_OPTIONS = "prism.arOptions"; @@ -230,7 +230,7 @@ public class PrismSettings implements Observer "Which engine (hybrid, sparse, MTBDD, explicit) should be used for model checking." }, { BOOLEAN_TYPE, PRISM_EXACT_ENABLED, "Do exact model checking", "4.2.1", new Boolean(false), "", "Perform exact model checking." }, - { BOOLEAN_TYPE, PRISM_EXACT_LP_ENABLED, "Do exact model checking using linear programming", "4.2.1", new Boolean(false), "", + { BOOLEAN_TYPE, PRISM_EXACTLP_ENABLED, "Do exact model checking using linear programming", "4.3.1", new Boolean(false), "", "Perform exact model checking using linear programming." }, { CHOICE_TYPE, PRISM_PTA_METHOD, "PTA model checking method", "3.3", "Stochastic games", "Digital clocks,Stochastic games,Backwards reachability", @@ -252,7 +252,7 @@ public class PrismSettings implements Observer "Epsilon value to use for checking termination of iterative numerical methods." }, { INTEGER_TYPE, PRISM_MAX_ITERS, "Termination max. iterations", "2.1", new Integer(10000), "0,", "Maximum number of iterations to perform if iterative methods do not converge." }, - { INTEGER_TYPE, PRISM_PRECISION, "Floating point precision", "2.1", new Integer(64), "1,", + { INTEGER_TYPE, PRISM_EXACTLP_PRECISION, "Exact linear programming precision", "4.3.1", new Integer(64), "1,", "The accuracy of the mantissa (in bits) is determined by this variable. This user-selectable precision is a minimum value: it is rounded up to a whole limb." }, // MODEL CHECKING OPTIONS: { BOOLEAN_TYPE, PRISM_PRECOMPUTATION, "Use precomputation", "2.1", new Boolean(true), "", @@ -917,7 +917,7 @@ else if (sw.equals("exact")) { } // Exact linear programming model checking else if (sw.equals("exact-lp")) { - set(PRISM_EXACT_LP_ENABLED, true); + set(PRISM_EXACTLP_ENABLED, true); set(PRISM_MDP_SOLN_METHOD, "Exact linear programming"); set(PRISM_LIN_EQ_METHOD, "Exact linear programming"); } @@ -1047,7 +1047,7 @@ else if (sw.equals("precision")) { j = Integer.parseInt(args[++i]); if (j <= 0) throw new NumberFormatException(""); - set(PRISM_PRECISION, j); + set(PRISM_EXACTLP_PRECISION, j); } catch (NumberFormatException e) { throw new PrismException("Invalid value for -" + sw + " switch"); }