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

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
master
Dave Parker 15 years ago
parent
ac4cefbb45
commit
d6673e0458
1 changed files with 26 additions and 18 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. 44
      prism/src/prism/PrismCL.java

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

@ -1776,10 +1776,13 @@ public class PrismCL
mainLog.println();
mainLog.println("-pctl <prop> (or -csl <prop>) .. Model check the PCTL/CSL property <prop>");
mainLog.println("-property <n> (or -prop <n>) ... Only model check property <n> from the properties file");
mainLog.println("-const <vals> .................. Run an experiment using constant values <vals>");
mainLog.println("-const <vals> .................. Define constant values as <vals> (e.g. for experiments)");
mainLog.println("-steadystate (or -ss) .......... Compute steady-state probabilities (D/CTMCs only)");
mainLog.println("-transient <x> (or -tr <x>) .... Compute transient probabilities for time <x> (D/CTMCs only)");
mainLog.println("-simpath <options> <file>....... 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 <file> ............ Import the transition matrix directly from a text file");
mainLog.println("-importstates <file>............ 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 <file> .......... Export the results of model checking to a file");
mainLog.println("-exporttrans <file> ............ Export the transition matrix to a file");
mainLog.println("-exportstaterewards <file> ..... Export the state rewards vector to a file");
@ -1809,12 +1813,14 @@ 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("-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 <name> .............. 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 <x> ..................... Set over-relaxation parameter (for JOR/SOR/...) [default 0.9]");
mainLog.println();
mainLog.println("-omega <x> ..................... 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 <x> (or -e <x>) ....... Set value of epsilon (for convergence check) [default 1e-6]");
mainLog.println("-maxiters <n> .................. Set max number of iterations [default 10000]");
mainLog.println("-epsilon <x> (or -e <x>) ....... Set value of epsilon (for convergence check) [default: 1e-6]");
mainLog.println("-maxiters <n> .................. 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 <name> .............. Specify SCC computation method (xiebeerel, lockstep, sccfind)");
mainLog.println();
mainLog.println("-sbmax <n> ..................... Set memory limit (KB) (for hybrid engine) [default 1024]");
mainLog.println("-sbl <n> ....................... Set number of levels (for hybrid engine) [default -1]");
mainLog.println("-gsmax <n> (or sormax <n>) ..... Set memory limit (KB) for hybrid GS/SOR [default 1024]");
mainLog.println("-gsl <n> (or sorl <n>) ......... 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 <n> ..................... Set memory limit (KB) (for hybrid engine) [default: 1024]");
mainLog.println("-sbl <n> ....................... Set number of levels (for hybrid engine) [default: -1]");
mainLog.println("-gsmax <n> (or sormax <n>) ..... Set memory limit (KB) for hybrid GS/SOR [default: 1024]");
mainLog.println("-gsl <n> (or sorl <n>) ......... Set number of levels for hybrid GS/SOR [default: -1]");
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("-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("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");
mainLog.println("-simconf <x> ................... Set the confidence parameter for the simulator");
mainLog.println("-simsamples <n> ................ Set the number of samples for the simulator");
mainLog.println("-simpathlen <n> ................ Set the maximum path length for the simulator");
mainLog.println("-simpath <options> <file>....... Generate a random path with the simulator");
}
// print version

Write Preview
Loading…
Cancel
Save