Added QC -n option

nickbattle · Nov 11, 2024 · 38e0eb7 · 38e0eb7
1 parent 00e8ca7
commit 38e0eb7
Show file tree

Hide file tree

Showing 5 changed files with 51 additions and 6 deletions.
diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java
@@ -955,7 +955,7 @@ public void printHelp(String USAGE)
 		println(USAGE);
 		println("");
 		println("  -?|-help           - show command help");
-		println("  -q|-v              - run with minimal or verbose output");
+		println("  -q|-v|-n           - run with minimal, verbose, basic output");
 		println("  -t <msecs>         - timeout in millisecs");
 		println("  -i <status>        - only show this result status");
 		println("  -s <strategy>      - enable this strategy (below)");

diff --git a/quickcheck/src/main/java/quickcheck/commands/QCConsole.java b/quickcheck/src/main/java/quickcheck/commands/QCConsole.java
@@ -59,10 +59,20 @@ public static void setIncludes(List<POStatus> includes)
 		QCConsole.includes = includes;
 	}
 
+	public static List<POStatus> getIncludes()
+	{
+		return includes;
+	}
+
 	public static void setVerbose(boolean verbose)
 	{
 		QCConsole.verbose = verbose;
 	}
+
+	public boolean getVerbose()
+	{
+		return verbose;
+	}
 
 	public static void info(POStatus status, String m)
 	{

diff --git a/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java b/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java
@@ -36,6 +36,7 @@
 import com.fujitsu.vdmj.debug.ConsoleDebugReader;
 import com.fujitsu.vdmj.debug.ConsoleExecTimer;
 import com.fujitsu.vdmj.lex.Dialect;
+import com.fujitsu.vdmj.messages.Console;
 import com.fujitsu.vdmj.plugins.AnalysisCommand;
 import com.fujitsu.vdmj.plugins.PluginRegistry;
 import com.fujitsu.vdmj.plugins.analyses.POPlugin;
@@ -48,7 +49,7 @@
 
 public class QuickCheckCommand extends AnalysisCommand
 {
-	private final static String CMD = "quickcheck [-?|-help][-q|-v][-t <secs>][-i <status>]*[-s <strategy>]* [-<strategy:option>]* [<PO numbers/ranges/patterns>]";
+	private final static String CMD = "quickcheck [-?|-help][-q|-v|-n][-t <secs>][-i <status>]*[-s <strategy>]* [-<strategy:option>]* [<PO numbers/ranges/patterns>]";
 	private final static String SHORT = "quickcheck [-help][<options>][<POs>]";
 	private final static String USAGE = "Usage: " + CMD;
 	public  final static String HELP = SHORT + " - lightweight PO verification";
@@ -70,6 +71,7 @@ public String run(String line)
 		List<String> poNames = new Vector<String>();
 		List<POStatus> includes = new Vector<POStatus>();
 		long timeout = -1;
+		boolean numbersOnly = false;
 
 		QuickCheck qc = new QuickCheck();
 
@@ -122,6 +124,11 @@ public String run(String line)
 							return USAGE;
 						}
 						break;
+
+					case "-n":
+						numbersOnly = true;
+						QCConsole.setQuiet(true);
+						break;
 
 					case "-":
 						i++;
@@ -208,6 +215,14 @@ public String run(String line)
 						execTimer.start();
 
 						qc.checkObligation(po, results);
+
+						if (numbersOnly)
+						{
+							if (includes.isEmpty() || includes.contains(po.status))
+							{
+								Console.out.printf("PO #%d: %s\n", po.number, po.status.toString().toUpperCase());
+							}
+						}
 					}
 					catch (Exception e)
 					{

diff --git a/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java b/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java
@@ -30,6 +30,8 @@
 import com.fujitsu.vdmj.Settings;
 import com.fujitsu.vdmj.debug.ConsoleExecTimer;
 import com.fujitsu.vdmj.lex.Dialect;
+import com.fujitsu.vdmj.messages.Console;
+import com.fujitsu.vdmj.pog.POStatus;
 import com.fujitsu.vdmj.pog.ProofObligation;
 import com.fujitsu.vdmj.pog.ProofObligationList;
 
@@ -50,15 +52,18 @@ public class QuickCheckExecutor extends AsyncExecutor
 	private final long timeout;
 	private final List<Integer> poList;
 	private final List<String> poNames;
+	private final boolean numbersOnly;
 	private String answer;
 
-	public QuickCheckExecutor(DAPRequest request, QuickCheck qc, long timeout, List<Integer> poList, List<String> poNames)
+	public QuickCheckExecutor(DAPRequest request, QuickCheck qc,
+			long timeout, List<Integer> poList, List<String> poNames, boolean numbersOnly)
 	{
 		super("qc", request);
 		this.qc = qc;
 		this.timeout = timeout;
 		this.poList = poList;
 		this.poNames = poNames;
+		this.numbersOnly = numbersOnly;
 	}
 
 	@Override
@@ -73,6 +78,7 @@ protected void exec() throws Exception
 		POPlugin pog = PluginRegistry.getInstance().getPlugin("PO");
 		ProofObligationList all = pog.getProofObligations();
 		ProofObligationList chosen = qc.getPOs(all, poList, poNames);
+		List<POStatus> includes = QCConsole.getIncludes();
 
 		if (qc.hasErrors())
 		{
@@ -102,6 +108,14 @@ protected void exec() throws Exception
 						execTimer.start();
 
 						qc.checkObligation(po, results);
+
+						if (numbersOnly)
+						{
+							if (includes.isEmpty() || includes.contains(po.status))
+							{
+								Console.out.printf("PO #%d: %s\n", po.number, po.status.toString().toUpperCase());
+							}
+						}
 					}
 					finally
 					{

diff --git a/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java b/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java
@@ -43,14 +43,15 @@
 
 public class QuickCheckLSPCommand extends AnalysisCommand implements InitRunnable, ScriptRunnable
 {
-	public final static String CMD = "quickcheck [-?|-help][-q|-v][-t <secs>][-i <status>]*[-s <strategy>]* [-<strategy:option>]* [<PO numbers/ranges/patterns>]";
+	public final static String CMD = "quickcheck [-?|-help][-q|-v|-n][-t <secs>][-i <status>]*[-s <strategy>]* [-<strategy:option>]* [<PO numbers/ranges/patterns>]";
 	public final static String SHORT = "quickcheck [-help][<options>][<POs>]";
 	private final static String USAGE = "Usage: " + CMD;
 
 	private List<Integer> poList = new Vector<Integer>();
 	private List<String> poNames = new Vector<String>();
 	private List<POStatus> includes = new Vector<POStatus>();
 	private long timeout = -1;
+	private boolean numbersOnly = false;
 	private QuickCheck qc = new QuickCheck();
 
 	public QuickCheckLSPCommand(String line)
@@ -125,6 +126,11 @@ private DAPMessageList setup(DAPRequest request)
 							return result(request, USAGE);
 						}
 						break;
+
+					case "-n":
+						QCConsole.setQuiet(true);
+						numbersOnly = true;
+						break;
 
 					case "-":
 						i++;
@@ -184,7 +190,7 @@ public DAPMessageList run(DAPRequest request)
 
 		if (errs == null)
 		{
-			QuickCheckExecutor executor = new QuickCheckExecutor(request, qc, timeout, poList, poNames);
+			QuickCheckExecutor executor = new QuickCheckExecutor(request, qc, timeout, poList, poNames, numbersOnly);
 			executor.start();
 		}
 
@@ -200,7 +206,7 @@ public String initRun(DAPRequest request)
 		{
 			try
 			{
-				QuickCheckExecutor executor = new QuickCheckExecutor(request, qc, timeout, poList, poNames);
+				QuickCheckExecutor executor = new QuickCheckExecutor(request, qc, timeout, poList, poNames, numbersOnly);
 				executor.exec();	// Note, not start!
 				executor.clean();	// Send POG updated notification
 				return executor.getAnswer();