diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 3be5838b..7bc196b0 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -1734,8 +1734,9 @@ public class PrismCL return aSimMethod; } - // print help message - + /** + * Print a -help message, i.e. a list of the command-line switches. + */ private void printHelp() { mainLog.println("Usage: prism [] [options]"); @@ -1785,58 +1786,9 @@ public class PrismCL 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("ENGINES/METHODS:"); - mainLog.println("-mtbdd (or -m) ................. Use the MTBDD engine"); - mainLog.println("-sparse (or -s) ................ Use the Sparse engine"); - mainLog.println("-hybrid (or -h) ................ Use the Hybrid engine [default]"); - mainLog.println("-ptamethod .............. Specify PTA engine (games, digital) [default: games]"); - mainLog.println(); - mainLog.println("NUMERICAL SOLUTION OPTIONS:"); - mainLog.println("-power (or -pow, -pwr) ......... Use the Power method for numerical computation"); - mainLog.println("-jacobi (or -jac) .............. Use Jacobi for numerical computation [default]"); - mainLog.println("-gaussseidel (or -gs) .......... Use Gauss-Seidel for numerical computation"); - mainLog.println("-bgaussseidel (or -bgs) ........ Use Backwards Gauss-Seidel for numerical computation"); - mainLog.println("-pgaussseidel (or -pgs) ........ Use Pseudo Gauss-Seidel for numerical computation"); - mainLog.println("-bpgaussseidel (or -bpgs) ...... Use Backwards Pseudo Gauss-Seidel for numerical computation"); - mainLog.println("-jor ........................... Use JOR for numerical computation"); - mainLog.println("-sor ........................... Use SOR for numerical computation"); - mainLog.println("-bsor .......................... Use Backwards SOR for numerical computation"); - mainLog.println("-psor .......................... Use Pseudo SOR for numerical computation"); - mainLog.println("-bpsor ......................... Use Backwards Pseudo SOR for numerical computation"); - mainLog.println("-omega ..................... Set over-relaxation parameter (for JOR/SOR/...) [default: 0.9]"); - mainLog.println("-relative (or -rel) ............ Use relative error for detecting convergence [default]"); - mainLog.println("-absolute (or -abs) ............ Use absolute error for detecting convergence"); - mainLog.println("-epsilon (or -e ) ....... Set value of epsilon (for convergence check) [default: 1e-6]"); - mainLog.println("-maxiters .................. Set max number of iterations [default: 10000]"); - mainLog.println(); - mainLog.println("MODEL CHECKING OPTIONS:"); - mainLog.println("-nopre ......................... Skip (optional) precomputation algorithms"); - mainLog.println("-fair .......................... Use fairness (for model checking of MDPs)"); - mainLog.println("-nofair ........................ Don't use fairness (for model checking of MDPs) [default]"); - mainLog.println("-fixdl ......................... Automatically put self-loops in deadlock states"); - mainLog.println("-noprobchecks .................. Disable checks on model probabilities/rates"); - 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 SCC computation method (xiebeerel, lockstep, sccfind)"); - mainLog.println("-symm ................. Symmetry reduction options string"); - mainLog.println("-aroptions ............ Abstraction-refinement engine options string"); - 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("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("-sbl ....................... Set number of levels (for hybrid engine) [default: -1]"); - 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]"); + + prism.getSettings().printHelp(mainLog); + mainLog.println(); mainLog.println("SIMULATION OPTIONS:"); mainLog.println("-sim ........................... Use the PRISM simulator to approximate results of model checking"); diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 9a7499bf..6a4677d3 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -1018,6 +1018,66 @@ public class PrismSettings implements Observer return i + 1; } + /** + * Print a fragment of the -help message, + * i.e. a list of the command-line switches handled by this class. + */ + public void printHelp(PrismLog mainLog) + { + mainLog.println(); + mainLog.println("ENGINES/METHODS:"); + mainLog.println("-mtbdd (or -m) ................. Use the MTBDD engine"); + mainLog.println("-sparse (or -s) ................ Use the Sparse engine"); + mainLog.println("-hybrid (or -h) ................ Use the Hybrid engine [default]"); + mainLog.println("-ptamethod .............. Specify PTA engine (games, digital) [default: games]"); + mainLog.println(); + mainLog.println("NUMERICAL SOLUTION OPTIONS:"); + mainLog.println("-power (or -pow, -pwr) ......... Use the Power method for numerical computation"); + mainLog.println("-jacobi (or -jac) .............. Use Jacobi for numerical computation [default]"); + mainLog.println("-gaussseidel (or -gs) .......... Use Gauss-Seidel for numerical computation"); + mainLog.println("-bgaussseidel (or -bgs) ........ Use Backwards Gauss-Seidel for numerical computation"); + mainLog.println("-pgaussseidel (or -pgs) ........ Use Pseudo Gauss-Seidel for numerical computation"); + mainLog.println("-bpgaussseidel (or -bpgs) ...... Use Backwards Pseudo Gauss-Seidel for numerical computation"); + mainLog.println("-jor ........................... Use JOR for numerical computation"); + mainLog.println("-sor ........................... Use SOR for numerical computation"); + mainLog.println("-bsor .......................... Use Backwards SOR for numerical computation"); + mainLog.println("-psor .......................... Use Pseudo SOR for numerical computation"); + mainLog.println("-bpsor ......................... Use Backwards Pseudo SOR for numerical computation"); + mainLog.println("-omega ..................... Set over-relaxation parameter (for JOR/SOR/...) [default: 0.9]"); + mainLog.println("-relative (or -rel) ............ Use relative error for detecting convergence [default]"); + mainLog.println("-absolute (or -abs) ............ Use absolute error for detecting convergence"); + mainLog.println("-epsilon (or -e ) ....... Set value of epsilon (for convergence check) [default: 1e-6]"); + mainLog.println("-maxiters .................. Set max number of iterations [default: 10000]"); + mainLog.println(); + mainLog.println("MODEL CHECKING OPTIONS:"); + mainLog.println("-nopre ......................... Skip (optional) precomputation algorithms"); + mainLog.println("-fair .......................... Use fairness (for model checking of MDPs)"); + mainLog.println("-nofair ........................ Don't use fairness (for model checking of MDPs) [default]"); + mainLog.println("-fixdl ......................... Automatically put self-loops in deadlock states"); + mainLog.println("-noprobchecks .................. Disable checks on model probabilities/rates"); + 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 SCC computation method (xiebeerel, lockstep, sccfind)"); + mainLog.println("-symm ................. Symmetry reduction options string"); + mainLog.println("-aroptions ............ Abstraction-refinement engine options string"); + 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("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("-sbl ....................... Set number of levels (for hybrid engine) [default: -1]"); + 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]"); + } + /** * Set the value for an option, with the option key given as a String, * and the value as an Object of appropriate type or a String to be parsed.