From 062beb5709b5fae6ae652e02a68e1b8d9af30785 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 15 Dec 2010 23:43:43 +0000 Subject: [PATCH] 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 --- prism/src/prism/PrismCL.java | 12 +++-- prism/src/prism/PrismSettings.java | 85 +++++++++++++++++++++--------- 2 files changed, 66 insertions(+), 31 deletions(-) diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 41cd8861..ec84f6d5 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -1820,6 +1820,8 @@ 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("-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("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 .............. 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 ..................... Set memory limit (KB) (for hybrid engine) [default: 1024]"); @@ -1864,11 +1871,6 @@ public class PrismCL 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("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"); diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index cf71c9df..bf119c79 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -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." },