From 3570b3e9bd8a63b103b5f06dfdbf8e80e001a1df Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 23 Jul 2013 07:04:06 +0000 Subject: [PATCH] Promote sumRoundOff setting in Prism to a proper option (for easier access from ECComputers). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7127 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Prism.java | 24 ++++++++++-------------- prism/src/prism/PrismSettings.java | 19 +++++++++++++++++++ 2 files changed, 29 insertions(+), 14 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 20271107..f28408e8 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -194,10 +194,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener // 2 - (s l ... l r c ... r c) (s l ... l r c ... r c) ... private int ordering = 1; - // Round-off threshold for places where doubles are summed and compared to integers - // (e.g. checking that probabilities sum to 1 in an update). - private double sumRoundOff = 1e-5; - // Method to use for (symbolic) state-space reachability private int reachMethod = REACH_BFS; @@ -385,6 +381,11 @@ public class Prism extends PrismComponent implements PrismSettingsListener settings.set(PrismSettings.PRISM_DO_PROB_CHECKS, b); } + public void setSumRoundOff(double d) throws PrismException + { + settings.set(PrismSettings.PRISM_SUM_ROUND_OFF, d); + } + public void setCompact(boolean b) throws PrismException { settings.set(PrismSettings.PRISM_COMPACT, b); @@ -589,11 +590,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener ordering = i; } - public void setSumRoundOff(double d) throws PrismException - { - sumRoundOff = d; - } - public static int REACH_BFS = 1; public static int REACH_FRONTIER = 2; @@ -669,6 +665,11 @@ public class Prism extends PrismComponent implements PrismSettingsListener return settings.getBoolean(PrismSettings.PRISM_DO_PROB_CHECKS); } + public double getSumRoundOff() + { + return settings.getDouble(PrismSettings.PRISM_SUM_ROUND_OFF); + } + public int getLinEqMethod() { return settings.getChoice(PrismSettings.PRISM_LIN_EQ_METHOD); @@ -879,11 +880,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener return ordering; } - public double getSumRoundOff() - { - return sumRoundOff; - } - public int getReachMethod() { return reachMethod; diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 9ea255f4..0fc8af17 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -78,6 +78,7 @@ public class PrismSettings implements Observer public static final String PRISM_PROB1 = "prism.prob1"; public static final String PRISM_FIX_DEADLOCKS = "prism.fixDeadlocks"; public static final String PRISM_DO_PROB_CHECKS = "prism.doProbChecks"; + public static final String PRISM_SUM_ROUND_OFF = "prism.sumRoundOff"; public static final String PRISM_COMPACT = "prism.compact"; public static final String PRISM_LIN_EQ_METHOD = "prism.linEqMethod";//"prism.iterativeMethod"; public static final String PRISM_LIN_EQ_METHOD_PARAM = "prism.linEqMethodParam";//"prism.overRelaxation"; @@ -246,6 +247,8 @@ public class PrismSettings implements Observer "Automatically fix deadlocks, where necessary, when constructing probabilistic models." }, { BOOLEAN_TYPE, PRISM_DO_PROB_CHECKS, "Do probability/rate checks", "2.1", new Boolean(true), "", "Perform sanity checks on model probabilities/rates when constructing probabilistic models." }, + { DOUBLE_TYPE, PRISM_SUM_ROUND_OFF, "Probability sum threshold", "2.1", new Double(1.0E-5), "0.0,", + "Round-off threshold for places where doubles are summed and compared to integers (e.g. checking that probabilities sum to 1 in an update)." }, { BOOLEAN_TYPE, PRISM_DO_SS_DETECTION, "Use steady-state detection", "2.1", new Boolean(true), "0,", "Use steady-state detection during CTMC transient probability computation." }, { CHOICE_TYPE, PRISM_SCC_METHOD, "SCC decomposition method", "3.2", "Lockstep", "Xie-Beerel,Lockstep,SCC-Find", @@ -969,6 +972,21 @@ public class PrismSettings implements Observer else if (sw.equals("noprobchecks")) { set(PRISM_DO_PROB_CHECKS, false); } + // Sum round-off threshold + else if (sw.equals("sumroundoff")) { + if (i < args.length - 1) { + try { + d = Double.parseDouble(args[++i]); + if (d < 0) + throw new NumberFormatException(""); + set(PRISM_SUM_ROUND_OFF, d); + } catch (NumberFormatException e) { + throw new PrismException("Invalid value for -" + sw + " switch"); + } + } else { + throw new PrismException("No value specified for -" + sw + " switch"); + } + } // No steady-state detection else if (sw.equals("nossdetect")) { set(PRISM_DO_SS_DETECTION, false); @@ -1402,6 +1420,7 @@ public class PrismSettings implements Observer mainLog.println("-fixdl ......................... Automatically put self-loops in deadlock states [default]"); mainLog.println("-nofixdl ....................... Do not automatically put self-loops in deadlock states"); mainLog.println("-noprobchecks .................. Disable checks on model probabilities/rates"); + mainLog.println("-sumroundoff ............... Set probability sum threshold [default: 1-e5]"); mainLog.println("-zerorewardcheck ............... Check for absence of zero-reward loops"); mainLog.println("-nossdetect .................... Disable steady-state detection for CTMC transient computations"); mainLog.println("-sccmethod .............. Specify (symbolic) SCC computation method (xiebeerel, lockstep, sccfind)");