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

Removed bisim from PTA options, tidied PrismSettings + -help (to match), added missing -help switches. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2334 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
b81b80e877
commit
062beb5709
2 changed files with 66 additions and 31 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. 12
      prism/src/prism/PrismCL.java
  2. 85
      prism/src/prism/PrismSettings.java

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

@ -1820,6 +1820,8 @@ public class PrismCL
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("-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("ENGINES/METHODS:");
mainLog.println("-mtbdd (or -m) ................. Use the MTBDD engine");
@ -1855,6 +1857,11 @@ public class PrismCL
mainLog.println("-nossdetect .................... Disable steady-state detection for CTMC transient computations");
mainLog.println("-sccmethod <name> .............. Specify SCC computation method (xiebeerel, lockstep, sccfind)");
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");
mainLog.println("-extrareachinfo ................ Display extra info about progress of reachability");
mainLog.println();
mainLog.println("SPARSE/HYBRID/MTBDD OPTIONS:");
mainLog.println("-nocompact ..................... Switch off \"compact\" sparse storage schemes");
mainLog.println("-sbmax <n> ..................... Set memory limit (KB) (for hybrid engine) [default: 1024]");
@ -1864,11 +1871,6 @@ public class PrismCL
mainLog.println("-cuddmaxmem <n> ................ Set max memory for CUDD package (KB) [default: 200x1024]");
mainLog.println("-cuddepsilon <x> ............... Set epsilon value for CUDD package [default: 1e-15]");
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");
mainLog.println("-extrareachinfo ................ Display extra info about progress of reachability");
mainLog.println();
mainLog.println("SIMULATION OPTIONS:");
mainLog.println("-sim ........................... Use the PRISM simulator to approximate results of model checking");
mainLog.println("-simapprox <x> ................. Set the approximation parameter for the simulator");

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

@ -179,32 +179,65 @@ public class PrismSettings implements Observer
{
{ //Datatype: Key: Display name: Version: Default: Constraints: Comment:
//====================================================================================================================================================================================================================================================================================================================================
{ CHOICE_TYPE, PRISM_ENGINE, "Engine", "2.1", "Hybrid", "MTBDD,Sparse,Hybrid", "Which engine (hybrid, sparse or MTBDD) should be used for model checking." },
{ BOOLEAN_TYPE, PRISM_VERBOSE, "Verbose output", "2.1", new Boolean(false), "", "Display verbose output to log." },
{ BOOLEAN_TYPE, PRISM_FAIRNESS, "Use fairness", "2.1", new Boolean(false), "", "Constrain to fair adversaries when model checking probabilistic reachability properties of MDPs." },
{ BOOLEAN_TYPE, PRISM_PRECOMPUTATION, "Use precomputation", "2.1", new Boolean(true), "", "Use model checking precomputation algorithms (Prob0, Prob1, etc.)." },
{ 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." },
{ BOOLEAN_TYPE, PRISM_COMPACT, "Use compact schemes", "2.1", new Boolean(true), "", "Use additional optimisations for compressing sparse matrices and vectors with repeated values." },
{ CHOICE_TYPE, PRISM_LIN_EQ_METHOD, "Iterative 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_TERM_CRIT, "Termination criteria", "2.1", "Relative", "Absolute,Relative", "Criteria to use for checking termination of iterative numerical methods." },
{ DOUBLE_TYPE, PRISM_TERM_CRIT_PARAM, "Termination epsilon", "2.1", new Double(1.0E-6), "0.0,", "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_CUDD_MAX_MEM, "CUDD max. memory (KB)", "2.1", new Integer(204800), "0,", "Maximum memory available to CUDD (underlying BDD/MTBDD library) in KB (Note: Restart PRISM after changing this.)" },
{ DOUBLE_TYPE, PRISM_CUDD_EPSILON, "CUDD epsilon", "2.1", new Double(1.0E-15), "0.0,", "Epsilon value used by CUDD (underlying BDD/MTBDD library) for terminal cache comparisons." },
{ INTEGER_TYPE, PRISM_NUM_SB_LEVELS, "Hybrid sparse levels", "2.1", new Integer(-1), "-1,", "Number of MTBDD levels ascended when adding sparse matrices to hybrid engine data structures (-1 means use default)." },
{ INTEGER_TYPE, PRISM_SB_MAX_MEM, "Hybrid sparse memory (KB)", "2.1", new Integer(1024), "0,", "Maximum memory usage when adding sparse matrices to hybrid engine data structures (KB)." },
{ INTEGER_TYPE, PRISM_NUM_SOR_LEVELS, "Hybrid GS levels", "2.1", new Integer(-1), "-1,", "Number of MTBDD levels descended for hybrid engine data structures block division with GS/SOR." },
{ INTEGER_TYPE, PRISM_SOR_MAX_MEM, "Hybrid GS memory (KB)", "2.1", new Integer(1024), "0,", "Maximum memory usage for hybrid engine data structures block division with GS/SOR (KB)." },
{ 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." },
{ 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." },
{ BOOLEAN_TYPE, PRISM_EXTRA_REACH_INFO, "Extra reachability information", "3.1.1", new Boolean(false), "0,", "Display extra information about progress of reachability during model construction." },
{ CHOICE_TYPE, PRISM_SCC_METHOD, "SCC decomposition method", "3.2", "Lockstep", "Xie-Beerel,Lockstep,SCC-Find", "Which algorithm to use for decomposing a graph into strongly connected components (SCCs)." },
{ STRING_TYPE, PRISM_SYMM_RED_PARAMS, "Symmetry reduction parameters", "3.2", "", "", "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)." },
{ CHOICE_TYPE, PRISM_PTA_METHOD, "PTA model checking method", "3.3", "Stochastic games", "Digital clocks,Stochastic games,Bisimulation minimisation", "Which method to use for model checking of PTAs." },
{ STRING_TYPE, PRISM_AR_OPTIONS, "Abstraction refinement options", "3.3", "", "", "Various options passed to the asbtraction-refinement engine (e.g. for PTA model checking)." },
{ CHOICE_TYPE, PRISM_EXPORT_ADV, "Adversary export", "3.3", "None", "None,DTMC,MDP", "Type of adversary to generate and export during MDP model checking" },
{ STRING_TYPE, PRISM_EXPORT_ADV_FILENAME, "Adversary export filename", "3.3", "adv.tra", "", "Name of file for MDP adversary export (if enabled)" },
// ENGINES/METHODS:
{ CHOICE_TYPE, PRISM_ENGINE, "Engine", "2.1", "Hybrid", "MTBDD,Sparse,Hybrid",
"Which engine (hybrid, sparse or MTBDD) should be used for model checking." },
{ CHOICE_TYPE, PRISM_PTA_METHOD, "PTA model checking method", "3.3", "Stochastic games", "Digital clocks,Stochastic games",
"Which method to use for model checking of PTAs." },
// 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." },
{ CHOICE_TYPE, PRISM_TERM_CRIT, "Termination criteria", "2.1", "Relative", "Absolute,Relative",
"Criteria to use for checking termination of iterative numerical methods." },
{ DOUBLE_TYPE, PRISM_TERM_CRIT_PARAM, "Termination epsilon", "2.1", new Double(1.0E-6), "0.0,",
"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." },
{ BOOLEAN_TYPE, PRISM_FAIRNESS, "Use fairness", "2.1", new Boolean(false), "",
"Constrain to fair adversaries when model checking probabilistic reachability properties of MDPs." },
{ 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." },
{ 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",
"Which algorithm to use for decomposing a graph into strongly connected components (SCCs)." },
{ STRING_TYPE, PRISM_SYMM_RED_PARAMS, "Symmetry reduction parameters", "3.2", "", "",
"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)." },
// OUTPUT OPTIONS:
{ 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." },
{ BOOLEAN_TYPE, PRISM_EXTRA_REACH_INFO, "Extra reachability information", "3.1.1", new Boolean(false), "0,",
"Display extra information about progress of reachability during model construction." },
// SPARSE/HYBRID/MTBDD OPTIONS:
{ BOOLEAN_TYPE, PRISM_COMPACT, "Use compact schemes", "2.1", new Boolean(true), "",
"Use additional optimisations for compressing sparse matrices and vectors with repeated values." },
{ INTEGER_TYPE, PRISM_NUM_SB_LEVELS, "Hybrid sparse levels", "2.1", new Integer(-1), "-1,",
"Number of MTBDD levels ascended when adding sparse matrices to hybrid engine data structures (-1 means use default)." },
{ INTEGER_TYPE, PRISM_SB_MAX_MEM, "Hybrid sparse memory (KB)", "2.1", new Integer(1024), "0,",
"Maximum memory usage when adding sparse matrices to hybrid engine data structures (KB)." },
{ INTEGER_TYPE, PRISM_NUM_SOR_LEVELS, "Hybrid GS levels", "2.1", new Integer(-1), "-1,",
"Number of MTBDD levels descended for hybrid engine data structures block division with GS/SOR." },
{ INTEGER_TYPE, PRISM_SOR_MAX_MEM, "Hybrid GS memory (KB)", "2.1", new Integer(1024), "0,",
"Maximum memory usage for hybrid engine data structures block division with GS/SOR (KB)." },
{ INTEGER_TYPE, PRISM_CUDD_MAX_MEM, "CUDD max. memory (KB)", "2.1", new Integer(204800), "0,",
"Maximum memory available to CUDD (underlying BDD/MTBDD library) in KB (Note: Restart PRISM after changing this.)" },
{ DOUBLE_TYPE, PRISM_CUDD_EPSILON, "CUDD epsilon", "2.1", new Double(1.0E-15), "0.0,",
"Epsilon value used by CUDD (underlying BDD/MTBDD library) for terminal cache comparisons." },
// ADVERSARIES/COUNTEREXAMPLES
{ CHOICE_TYPE, PRISM_EXPORT_ADV, "Adversary export", "3.3", "None", "None,DTMC,MDP",
"Type of adversary to generate and export during MDP model checking" },
{ STRING_TYPE, PRISM_EXPORT_ADV_FILENAME, "Adversary export filename", "3.3", "adv.tra", "",
"Name of file for MDP adversary export (if enabled)" },
},
{
{ BOOLEAN_TYPE, MODEL_AUTO_PARSE, "Auto parse", "2.1", new Boolean(true), "", "Parse PRISM models automatically as they are loaded/edited in the text editor." },

Write Preview
Loading…
Cancel
Save