s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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
master
Dave Parker 13 years ago
parent
6850de1ab1
commit
47c1a13428
3 changed files with 64 additions and 62 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      prism/src/prism/NondetModelChecker.java
  2. 5
      prism/src/prism/PrismCL.java
  3. 111
      prism/src/prism/PrismSettings.java

10
prism/src/prism/NondetModelChecker.java
View File

@ -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);

5
prism/src/prism/PrismCL.java
View File

@ -1701,11 +1701,6 @@ public class PrismCL implements PrismModelListener
mainLog.println("-exporttransient <file> ........ Export transient probabilities to a file");
mainLog.println("-exportprism <file> ............ Export final PRISM model to a file");
mainLog.println("-exportprismconst <file> ....... 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 <file> ............. When computing Pareto curve, the result is stored to file");
mainLog.println("-paretoepsilon ................. Threshold for Pareto curve approximation");
prism.getSettings().printHelp(mainLog);

111
prism/src/prism/PrismSettings.java
View File

@ -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,38 +862,6 @@ 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:
@ -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 <file> .............. Export an adversary from MDP model checking (as a DTMC)");
mainLog.println("-exportadvmdp <file> ........... Export an adversary from MDP model checking (as an MDP)");
mainLog.println();
mainLog.println("MULTI-OBJECTIVE MODEL CHECKING:");
mainLog.println("-multimaxpoints <n> ............ Maximal number of corner points for (valiter-based) multi-objective");
mainLog.println("-paretoepsilon <x> ............. Threshold for Pareto curve approximation");
mainLog.println("-exportpareto <file> ........... 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");

Write Preview
Loading…
Cancel
Save