From 47c1a134281a164eed6ad29d8a1dfa3100efb3c7 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 17 Dec 2012 13:40:41 +0000 Subject: [PATCH] Tidy/tweak multi-objective settings, align with others. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6216 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModelChecker.java | 10 +-- prism/src/prism/PrismCL.java | 5 -- prism/src/prism/PrismSettings.java | 111 +++++++++++++----------- 3 files changed, 64 insertions(+), 62 deletions(-) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 7171f5fd..ece1ad2b 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -2436,7 +2436,7 @@ public class NondetModelChecker extends NonProbModelChecker } double tolerance = prism.getSettings().getDouble(PrismSettings.PRISM_PARETO_EPSILON); - int maxIters = prism.getSettings().getInteger(PrismSettings.PRISM_MAX_ITERS_MULTI); + int maxIters = prism.getSettings().getInteger(PrismSettings.PRISM_MULTI_MAX_POINTS); NativeIntArray adversary = new NativeIntArray((int) modelProduct.getNumStates()); int dimProb = targets.length; @@ -2632,9 +2632,9 @@ public class NondetModelChecker extends NonProbModelChecker if (!decided) throw new PrismException("The computation did not finish in " + maxIters - + " target point iterations, try increasing this number using the -maxiterspareto switch."); + + " target point iterations, try increasing this number using the -multimaxpoints switch."); else { - String paretoFile = prism.getSettings().getString(PrismSettings.PRISM_PARETO_FILENAME); + String paretoFile = prism.getSettings().getString(PrismSettings.PRISM_EXPORT_PARETO_FILENAME); //export to file if required if (paretoFile != null && !paretoFile.equals("")) { @@ -2686,7 +2686,7 @@ public class NondetModelChecker extends NonProbModelChecker boolean maximizingReward = (opsAndBounds.rewardSize() > 0 && (opsAndBounds.getRewardOperator(0) == Operator.R_MAX || opsAndBounds.getRewardOperator(0) == Operator.R_MIN)); boolean maximizingNegated = (maximizingProb && opsAndBounds.getProbOperator(0) == Operator.P_MIN) || (maximizingReward && opsAndBounds.getRewardOperator(0) == Operator.R_MIN); - int maxIters = prism.getSettings().getInteger(PrismSettings.PRISM_MAX_ITERS_MULTI); + int maxIters = prism.getSettings().getInteger(PrismSettings.PRISM_MULTI_MAX_POINTS); NativeIntArray adversary = new NativeIntArray((int) modelProduct.getNumStates()); int dimProb = targets.length; @@ -2884,7 +2884,7 @@ public class NondetModelChecker extends NonProbModelChecker if (!decided) throw new PrismException("The computation did not finish in " + maxIters - + " target point iterations, try increasing this number using the -maxiterspareto switch."); + + " target point iterations, try increasing this number using the -multimaxpoints switch."); if (maximizingProb || maximizingReward) { int maximizingCoord = (maximizingProb) ? 0 : dimProb; return (maximizingNegated) ? -targetPoint.getCoord(maximizingCoord) : targetPoint.getCoord(maximizingCoord); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index c8deb41c..a8ec1ccc 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -1701,11 +1701,6 @@ public class PrismCL implements PrismModelListener mainLog.println("-exporttransient ........ Export transient probabilities to a file"); mainLog.println("-exportprism ............ Export final PRISM model to a file"); mainLog.println("-exportprismconst ....... Export final PRISM model with expanded constants to a file"); - mainLog.println(); - mainLog.println("MULTI-OBJECTIVE VERIFICATION:"); - mainLog.println("-maxiterspareto ................ Maximal number of weights to be used"); - mainLog.println("-paretofile ............. When computing Pareto curve, the result is stored to file"); - mainLog.println("-paretoepsilon ................. Threshold for Pareto curve approximation"); prism.getSettings().printHelp(mainLog); diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 2a428275..7e2d49b6 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -83,9 +83,6 @@ 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_PARETO_EPSILON = "prism.paretoEpsilon";//"prism.terminationEpsilon"; - public static final String PRISM_MAX_ITERS_MULTI = "prism.maxItersMulti";//"prism.maxIterations" - public static final String PRISM_PARETO_FILENAME = "prism.paretoFileName"; public static final String PRISM_CUDD_MAX_MEM = "prism.cuddMaxMem"; public static final String PRISM_CUDD_EPSILON = "prism.cuddEpsilon"; @@ -103,6 +100,10 @@ public class PrismSettings implements Observer public static final String PRISM_EXPORT_ADV = "prism.exportAdv"; public static final String PRISM_EXPORT_ADV_FILENAME = "prism.exportAdvFilename"; + public static final String PRISM_MULTI_MAX_POINTS = "prism.multiMaxIters"; + public static final String PRISM_PARETO_EPSILON = "prism.paretoEpsilon"; + public static final String PRISM_EXPORT_PARETO_FILENAME = "prism.exportParetoFileName"; + //Simulator public static final String SIMULATOR_DEFAULT_NUM_SAMPLES = "simulator.defaultNumSamples"; public static final String SIMULATOR_DEFAULT_CONFIDENCE = "simulator.defaultConfidence"; @@ -209,15 +210,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." }, - { DOUBLE_TYPE, PRISM_PARETO_EPSILON, "Pareto approx. threshold", "4.1", new Double(1.0E-2), "0.0,", - "Determines to what precision the Pareto curve will be approximated." }, - - { INTEGER_TYPE, PRISM_MAX_ITERS_MULTI, "Termination max. corner points in multi-objective", "2.1", new Integer(50), "0,", - "Maximum number of corner points to explore if multi-objective value iteration does not converge." }, - { STRING_TYPE, PRISM_PARETO_FILENAME, "File to store Pareto curve", "4.1", "", "0,", - "The name of the file in which the Pareto curve will be stored." }, - - // MODEL CHECKING OPTIONS: + // MODEL CHECKING OPTIONS: { BOOLEAN_TYPE, PRISM_PRECOMPUTATION, "Use precomputation", "2.1", new Boolean(true), "", "Whether to use model checking precomputation algorithms (Prob0, Prob1, etc.), where optional." }, { BOOLEAN_TYPE, PRISM_PROB0, "Use Prob0 precomputation", "4.0.2", new Boolean(true), "", @@ -238,8 +231,15 @@ public class PrismSettings implements Observer "Parameters for symmetry reduction (format: \"i j\" where i and j are the number of modules before and after the symmetric ones; empty string means symmetry reduction disabled)." }, { STRING_TYPE, PRISM_AR_OPTIONS, "Abstraction refinement options", "3.3", "", "", "Various options passed to the asbtraction-refinement engine (e.g. for PTA model checking)." }, + // MULTI-OBJECTIVE MODEL CHECKING OPTIONS: + { INTEGER_TYPE, PRISM_MULTI_MAX_POINTS, "Max. multi-objective corner points", "4.0.3", new Integer(50), "0,", + "Maximum number of corner points to explore if (value iteration based) multi-objective model checking does not converge." }, + { DOUBLE_TYPE, PRISM_PARETO_EPSILON, "Pareto approximation threshold", "4.0.3", new Double(1.0E-2), "0.0,", + "Determines to what precision the Pareto curve will be approximated." }, + { STRING_TYPE, PRISM_EXPORT_PARETO_FILENAME, "Pareto curve export filename", "4.0.3", "", "0,", + "If non-empty, any Pareto curve generated will be exported to this file." }, // OUTPUT OPTIONS: - { BOOLEAN_TYPE, PRISM_VERBOSE, "Verbose output", "2.1", new Boolean(false), "", + { BOOLEAN_TYPE, PRISM_VERBOSE, "Verbose output", "2.1", new Boolean(false), "", "Display verbose output to log." }, { BOOLEAN_TYPE, PRISM_EXTRA_DD_INFO, "Extra MTBDD information", "3.1.1", new Boolean(false), "0,", "Display extra information about (MT)BDDs used during and after model construction." }, @@ -862,39 +862,7 @@ public class PrismSettings implements Observer throw new PrismException("No value specified for -" + sw + " switch"); } } - // Max different corner points that will be generated when performing - // target driven multi-obj verification. - else if (sw.equals("maxiterspareto")) { - if (i < args.length - 1) { - try { - j = Integer.parseInt(args[++i]); - if (j < 0) - throw new NumberFormatException(""); - set(PRISM_MAX_ITERS_MULTI, j); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - // Termination criterion for Pareto curve generation - else if (sw.equals("paretoepsilon")) { - if (i < args.length - 1) { - try { - d = Double.parseDouble(args[++i]); - if (d < 0) - throw new NumberFormatException("The argument for -paretoepsilon switch must be nonnegative"); - set(PRISM_PARETO_EPSILON, d); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value for -" + sw + " switch"); - } - } else { - throw new PrismException("No value specified for -" + sw + " switch"); - } - } - // MODEL CHECKING OPTIONS: // Precomputation algs off @@ -967,6 +935,47 @@ public class PrismSettings implements Observer } } + // MULTI-OBJECTIVE MODEL CHECKING OPTIONS: + + // Max different corner points that will be generated when performing + // target driven multi-obj verification. + else if (sw.equals("multimaxpoints")) { + if (i < args.length - 1) { + try { + j = Integer.parseInt(args[++i]); + if (j < 0) + throw new NumberFormatException(""); + set(PRISM_MULTI_MAX_POINTS, j); + } catch (NumberFormatException e) { + throw new PrismException("Invalid value for -" + sw + " switch"); + } + } else { + throw new PrismException("No value specified for -" + sw + " switch"); + } + } + // Threshold for approximate Pareto curve generation + else if (sw.equals("paretoepsilon")) { + if (i < args.length - 1) { + try { + d = Double.parseDouble(args[++i]); + if (d < 0) + throw new PrismException("Value for -" + sw + " switch must be non-negative"); + set(PRISM_PARETO_EPSILON, d); + } catch (NumberFormatException e) { + throw new PrismException("Invalid value for -" + sw + " switch"); + } + } else { + throw new PrismException("No value specified for -" + sw + " switch"); + } + } + else if (sw.equals("exportpareto")) { + if (i < args.length - 1) { + set(PRISM_EXPORT_PARETO_FILENAME, args[++i]); + } else { + throw new PrismException("No file specified for -" + sw + " switch"); + } + } + // OUTPUT OPTIONS: // Verbosity @@ -1096,13 +1105,6 @@ public class PrismSettings implements Observer throw new PrismException("No file specified for -" + sw + " switch"); } } - else if (sw.equals("paretofile")) { - if (i < args.length - 1) { - set(PRISM_PARETO_FILENAME, args[++i]); - } else { - throw new PrismException("No file specified for -" + sw + " switch"); - } - } // unknown switch - error else { @@ -1163,6 +1165,11 @@ public class PrismSettings implements Observer mainLog.println("-exportadv .............. Export an adversary from MDP model checking (as a DTMC)"); mainLog.println("-exportadvmdp ........... Export an adversary from MDP model checking (as an MDP)"); mainLog.println(); + mainLog.println("MULTI-OBJECTIVE MODEL CHECKING:"); + mainLog.println("-multimaxpoints ............ Maximal number of corner points for (valiter-based) multi-objective"); + mainLog.println("-paretoepsilon ............. Threshold for Pareto curve approximation"); + mainLog.println("-exportpareto ........... When computing Pareto curves, export points to a file"); + mainLog.println(); mainLog.println("OUTPUT OPTIONS:"); mainLog.println("-verbose (or -v) ............... Verbose mode: print out state lists and probability vectors"); mainLog.println("-extraddinfo ................... Display extra info about some (MT)BDDs");