From 9a658794b1c0fa0e7a90160c14eb40d5cae287d9 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 7 Jun 2013 21:36:15 +0000 Subject: [PATCH] Additional -help xxx messages. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6833 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/QuantAbstractRefine.java | 23 +++++++++++++++++++ prism/src/prism/PrismCL.java | 14 ++++++++++- prism/src/prism/PrismSettings.java | 21 ++++++++++++++++- .../src/simulator/GenerateSimulationPath.java | 19 +++++++++++++++ 4 files changed, 75 insertions(+), 2 deletions(-) diff --git a/prism/src/explicit/QuantAbstractRefine.java b/prism/src/explicit/QuantAbstractRefine.java index 26836f5f..09a858be 100644 --- a/prism/src/explicit/QuantAbstractRefine.java +++ b/prism/src/explicit/QuantAbstractRefine.java @@ -371,6 +371,29 @@ public abstract class QuantAbstractRefine parseOption(opt); } + /** + * Print bulleted list of options to a log (used by -help switch). + */ + public static void printOptions(PrismLog mainLog) + { + mainLog.println(" * verbose= (or v=) - verbosity level"); + mainLog.println(" * refine= - which states to refine and how"); + mainLog.println(" = all, allmax, first, firstmax, last, lastmax"); + mainLog.println(" = all, val"); + mainLog.println(" * epsilonref= (or eref=) - epsilon for refinement"); + mainLog.println(" * nopre - disable precomputation"); + mainLog.println(" * pre - use precomputation"); + mainLog.println(" * noprob0 - disable prob0 precomputation"); + mainLog.println(" * noprob1 - disable prob1 precomputation"); + mainLog.println(" * epsilon= - epsilon for numerical convergence"); + mainLog.println(" * maxref= - maximum number of refinements"); + mainLog.println(" * opt - use optimisations"); + mainLog.println(" * noopt - disable optimisations"); + mainLog.println(" * exportdot - export dot files for each refinement"); + mainLog.println(" * above - start numerical soluton from above"); + mainLog.println(" * below - start numerical soluton from below"); + } + // Abstract methods that must be implemented for abstraction-refinement loop /** diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 0b36158a..8d811e48 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -38,6 +38,7 @@ import parser.ast.ExpressionReward; import parser.ast.ModulesFile; import parser.ast.PropertiesFile; import parser.ast.Property; +import simulator.GenerateSimulationPath; import simulator.method.ACIconfidence; import simulator.method.ACIiterations; import simulator.method.ACIwidth; @@ -1927,7 +1928,7 @@ public class PrismCL implements PrismModelListener mainLog.println("-exportprism ............ Export final PRISM model to a file"); mainLog.println("-exportprismconst ....... Export final PRISM model with expanded constants to a file"); - prism.getSettings().printHelp(mainLog); + PrismSettings.printHelp(mainLog); mainLog.println(); mainLog.println("SIMULATION OPTIONS:"); @@ -1964,6 +1965,13 @@ public class PrismCL implements PrismModelListener mainLog.println(" -const a=1:2:50,b=5.6"); mainLog.println(" -const a=1:2:50 -const b=5.6"); } + // -simpath + else if (sw.equals("simpath")) { + mainLog.println("Switch: -simpath \n"); + mainLog.println("Generate a random path with the simulator and export it to (or to the screen if =\"stdout\")."); + mainLog.println(" is a comma-separated list of options taken from:"); + GenerateSimulationPath.printOptions(mainLog); + } // -exportresults else if (sw.equals("exportresults")) { mainLog.println("Switch: -exportresults \n"); @@ -1973,6 +1981,10 @@ public class PrismCL implements PrismModelListener mainLog.println(" * csv - Export results as comma-separated values"); mainLog.println(" * matrix - Export results as one or more 2D matrices (e.g. for surface plots)"); } + // Try PrismSettings + else if (PrismSettings.printHelpSwitch(mainLog, sw)) { + return; + } // Unknown else { mainLog.println("Sorry - no help available for switch -" + sw); diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index e6661747..0daf2ca1 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -32,6 +32,9 @@ import java.util.*; import java.io.*; import java.awt.*; import javax.swing.*; + +import explicit.QuantAbstractRefine; + import java.util.regex.*; import parser.ast.*; @@ -1311,7 +1314,7 @@ public class PrismSettings implements Observer * 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) + public static void printHelp(PrismLog mainLog) { mainLog.println(); mainLog.println("ENGINES/METHODS:"); @@ -1403,6 +1406,22 @@ public class PrismSettings implements Observer mainLog.println("-fauinitival ............... Set length of additional initial time interval [default: 1.0]"); } + /** + * Print a -help xxx message, i.e. display help on a specific switch {@code sw}. + * Return true iff help was available for this switch. + */ + public static boolean printHelpSwitch(PrismLog mainLog, String sw) + { + // -aroptions + if (sw.equals("aroptions")) { + mainLog.println("Switch: -aroptions \n"); + mainLog.println(" is a comma-separated list of options regarding abstraction-refinement:"); + QuantAbstractRefine.printOptions(mainLog); + return true; + } + return false; + } + /** * 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. diff --git a/prism/src/simulator/GenerateSimulationPath.java b/prism/src/simulator/GenerateSimulationPath.java index 843b8190..4c2870c6 100644 --- a/prism/src/simulator/GenerateSimulationPath.java +++ b/prism/src/simulator/GenerateSimulationPath.java @@ -315,6 +315,25 @@ public class GenerateSimulationPath } } + /** + * Print bulleted list of options to a log (used by -help switch). + */ + public static void printOptions(PrismLog mainLog) + { + mainLog.println(" * - generate a path of steps"); + mainLog.println(" * time= - generate a path of at least time units"); + mainLog.println(" * deadlock - generate a path until a deadlock is reached"); + mainLog.println(" * repeat= - try paths until a deadlock is found"); + + mainLog.println(" * sep= - use as column separator (space, tab, comma)"); + mainLog.println(" * vars= - show values for variables x1,x2,.. only"); + mainLog.println(" * loopcheck= - whether to detect deterministic loops"); + mainLog.println(" * snapshot= - view states at fixed timepoints of interval "); + mainLog.println(" * probs= - display probability (or rate) of transitions taken"); + mainLog.println(" * rewards= - display state/transition rewards"); + mainLog.println(" * changes= - only display states where displayed variables change"); + } + /** * Create a PathDisplayer object for file export */