From d6673e0458c30073e29636e628ed5280dee861d1 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 15 Dec 2010 10:14:11 +0000 Subject: [PATCH] Added ptamethod to -help; and re-arranged -help output. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2331 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/PrismCL.java | 44 +++++++++++++++++++++--------------- 1 file changed, 26 insertions(+), 18 deletions(-) diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 9c18eb9e..6c60eb26 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -1776,10 +1776,13 @@ public class PrismCL mainLog.println(); mainLog.println("-pctl (or -csl ) .. Model check the PCTL/CSL property "); mainLog.println("-property (or -prop ) ... Only model check property from the properties file"); - mainLog.println("-const .................. Run an experiment using constant values "); + mainLog.println("-const .................. Define constant values as (e.g. for experiments)"); mainLog.println("-steadystate (or -ss) .......... Compute steady-state probabilities (D/CTMCs only)"); mainLog.println("-transient (or -tr ) .... Compute transient probabilities for time (D/CTMCs only)"); + mainLog.println("-simpath ....... Generate a random path with the simulator"); + mainLog.println("-nobuild ....................... Skip model construction (just do parse/export)"); mainLog.println(); + mainLog.println("IMPORT OPTIONS:"); mainLog.println("-importpepa .................... Model description is in PEPA, not the PRISM language"); mainLog.println("-importtrans ............ Import the transition matrix directly from a text file"); mainLog.println("-importstates ............ Import the list of states directly from a text file"); @@ -1790,6 +1793,7 @@ public class PrismCL mainLog.println("-ctmc .......................... Force imported/built model to be a CTMC"); mainLog.println("-mdp ........................... Force imported/built model to be an MDP"); mainLog.println(); + mainLog.println("EXPORT OPTIONS:"); mainLog.println("-exportresults .......... Export the results of model checking to a file"); mainLog.println("-exporttrans ............ Export the transition matrix to a file"); mainLog.println("-exportstaterewards ..... Export the state rewards vector to a file"); @@ -1809,12 +1813,14 @@ 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("-nobuild ....................... Skip model construction (just parse/export)"); 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"); @@ -1826,40 +1832,42 @@ public class PrismCL 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(); + 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("-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("-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("-nopre ......................... Skip precomputation algorithms"); + mainLog.println("MODEL CHECKING OPTIONS:"); + mainLog.println("-nopre ......................... Skip (optional) precomputation algorithms"); mainLog.println("-fair .......................... Use fairness (for probabilistic reachability in MDPs)"); mainLog.println("-nofair ........................ Don't use fairness (for probabilistic reachability in MDPs) [default]"); mainLog.println("-fixdl ......................... Automatically put self-loops in deadlock states"); - mainLog.println("-nocompact ..................... Switch off \"compact\" sparse storage schemes"); mainLog.println("-noprobchecks .................. Disable checks on model probabilities/rates"); mainLog.println("-zerorewardchecks .............. 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(); - 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("-gsl (or sorl ) ......... Set number of levels for hybrid GS/SOR [default -1]"); + 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("-gsl (or sorl ) ......... Set number of levels for hybrid GS/SOR [default: -1]"); + 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(); - 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("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 ................. Set the approximation parameter for the simulator"); mainLog.println("-simconf ................... Set the confidence parameter for the simulator"); mainLog.println("-simsamples ................ Set the number of samples for the simulator"); mainLog.println("-simpathlen ................ Set the maximum path length for the simulator"); - mainLog.println("-simpath ....... Generate a random path with the simulator"); } // print version