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

@@ -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=<n> (or v=<n>) - verbosity level");
+		mainLog.println(" * refine=<where,how> - which states to refine and how");
+		mainLog.println("     <where> = all, allmax, first, firstmax, last, lastmax");
+		mainLog.println("     <how> = all, val");
+		mainLog.println(" * epsilonref=<x> (or eref=<x>) - 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=<x> - epsilon for numerical convergence");
+		mainLog.println(" * maxref=<n> - 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
 
 	/**

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 <file> ............ Export final PRISM model to a file");
 		mainLog.println("-exportprismconst <file> ....... 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 <options> <file>\n");
+			mainLog.println("Generate a random path with the simulator and export it to <file> (or to the screen if <file>=\"stdout\").");
+			mainLog.println("<options> is a comma-separated list of options taken from:");
+			GenerateSimulationPath.printOptions(mainLog);
+		}
 		// -exportresults
 		else if (sw.equals("exportresults")) {
 			mainLog.println("Switch: -exportresults <file[,options]>\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);

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 <x> ............... 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 <string>\n");
+			mainLog.println("<string> 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.

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(" * <n> - generate a path of <n> steps");
+		mainLog.println(" * time=<x> - generate a path of at least <x> time units");
+		mainLog.println(" * deadlock - generate a path until a deadlock is reached");
+		mainLog.println(" * repeat=<n> - try <n> paths until a deadlock is found");
+		
+		mainLog.println(" * sep=<val> - use <val> as column separator (space, tab, comma)");
+		mainLog.println(" * vars=<x1,x2,...> - show values for variables x1,x2,.. only");
+		mainLog.println(" * loopcheck=<true|false> - whether to detect deterministic loops");
+		mainLog.println(" * snapshot=<x> - view states at fixed timepoints of interval <x>");
+		mainLog.println(" * probs=<true|false> - display probability (or rate) of transitions taken");
+		mainLog.println(" * rewards=<true|false> - display state/transition rewards");
+		mainLog.println(" * changes=<true|false> - only display states where displayed variables change");
+	}
+
 	/**
 	 * Create a PathDisplayer object for file export
 	 */