From 6f1cbdf6d3001ba6be8b8fcaf77cd71e9cd2614b Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 8 Jun 2011 22:26:14 +0000 Subject: [PATCH] Tidy up of settings and -help text (from prism-sift). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3060 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/PrismCL.java | 4 ++-- prism/src/prism/PrismSettings.java | 35 ++++++++++++++++-------------- 2 files changed, 21 insertions(+), 18 deletions(-) diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index dcaf3550..3be5838b 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -1831,10 +1831,10 @@ public class PrismCL mainLog.println(); mainLog.println("SPARSE/HYBRID/MTBDD OPTIONS:"); mainLog.println("-nocompact ..................... Switch off \"compact\" sparse storage schemes"); - mainLog.println("-sbmax ..................... Set memory limit (KB) (for hybrid engine) [default: 1024]"); mainLog.println("-sbl ....................... Set number of levels (for hybrid engine) [default: -1]"); - mainLog.println("-gsmax (or sormax ) ..... Set memory limit (KB) for hybrid GS/SOR [default: 1024]"); + mainLog.println("-sbmax ..................... Set memory limit (KB) (for hybrid engine) [default: 1024]"); mainLog.println("-gsl (or sorl ) ......... Set number of levels for hybrid GS/SOR [default: -1]"); + mainLog.println("-gsmax (or sormax ) ..... Set memory limit (KB) for hybrid GS/SOR [default: 1024]"); mainLog.println("-cuddmaxmem ................ Set max memory for CUDD package (KB) [default: 200x1024]"); mainLog.println("-cuddepsilon ............... Set epsilon value for CUDD package [default: 1e-15]"); mainLog.println(); diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 9237794f..9a7499bf 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -192,6 +192,8 @@ public class PrismSettings implements Observer // NUMERICAL SOLUTION OPTIONS: { CHOICE_TYPE, PRISM_LIN_EQ_METHOD, "Linear equations method", "2.1", "Jacobi", "Power,Jacobi,Gauss-Seidel,Backwards Gauss-Seidel,Pseudo-Gauss-Seidel,Backwards Pseudo-Gauss-Seidel,JOR,SOR,Backwards SOR,Pseudo-SOR,Backwards Pseudo-SOR", "Which iterative method to use when solving linear equation systems." }, + { DOUBLE_TYPE, PRISM_LIN_EQ_METHOD_PARAM, "Over-relaxation parameter", "2.1", new Double(0.9), "", + "Over-relaxation parameter for iterative numerical methods such as JOR/SOR." }, { CHOICE_TYPE, PRISM_MDP_SOLN_METHOD, "MDP solution method", "4.0", "Value iteration", "Value iteration,Gauss-Seidel,Policy iteration,Modified policy iteration,Linear programming", "Which method to use when solving Markov decision processes." }, { CHOICE_TYPE, PRISM_TERM_CRIT, "Termination criteria", "2.1", "Relative", "Absolute,Relative", @@ -200,8 +202,6 @@ 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." }, - { DOUBLE_TYPE, PRISM_LIN_EQ_METHOD_PARAM, "Over-relaxation parameter", "2.1", new Double(0.9), "", - "Over-relaxation parameter for iterative numerical methods such as JOR/SOR." }, // MODEL CHECKING OPTIONS: { BOOLEAN_TYPE, PRISM_PRECOMPUTATION, "Use precomputation", "2.1", new Boolean(true), "", "Use model checking precomputation algorithms (Prob0, Prob1, etc.), where optional." }, @@ -713,6 +713,8 @@ public class PrismSettings implements Observer sw = args[i].substring(1); + // Note: the order of these switches should match the -help output (just to help keep track of things). + // ENGINES/METHODS: // Main model checking engine @@ -768,20 +770,12 @@ public class PrismSettings implements Observer } else if (sw.equals("bpsor")) { set(PRISM_LIN_EQ_METHOD, "Backwards Pseudo-SOR"); } - // Termination criterion (iterative methods) - else if (sw.equals("absolute") || sw.equals("abs")) { - set(PRISM_TERM_CRIT, "Absolute"); - } else if (sw.equals("relative") || sw.equals("rel")) { - set(PRISM_TERM_CRIT, "Relative"); - } - // Termination criterion parameter - else if (sw.equals("epsilon") || sw.equals("e")) { + // Linear equation solver over-relaxation parameter + else if (sw.equals("omega")) { if (i < args.length - 1) { try { d = Double.parseDouble(args[++i]); - if (d < 0) - throw new NumberFormatException(""); - set(PRISM_TERM_CRIT_PARAM, d); + set(PRISM_LIN_EQ_METHOD_PARAM, d); } catch (NumberFormatException e) { throw new PrismException("Invalid value for -" + sw + " switch"); } @@ -789,12 +783,21 @@ public class PrismSettings implements Observer throw new PrismException("No value specified for -" + sw + " switch"); } } - // Linear equation solver over-relaxation parameter - else if (sw.equals("omega")) { + // Termination criterion (iterative methods) + else if (sw.equals("relative") || sw.equals("rel")) { + set(PRISM_TERM_CRIT, "Relative"); + } + else if (sw.equals("absolute") || sw.equals("abs")) { + set(PRISM_TERM_CRIT, "Absolute"); + } + // Termination criterion parameter + else if (sw.equals("epsilon") || sw.equals("e")) { if (i < args.length - 1) { try { d = Double.parseDouble(args[++i]); - set(PRISM_LIN_EQ_METHOD_PARAM, d); + if (d < 0) + throw new NumberFormatException(""); + set(PRISM_TERM_CRIT_PARAM, d); } catch (NumberFormatException e) { throw new PrismException("Invalid value for -" + sw + " switch"); }