From 38e0eb78568201a2d46605ba4a65576040f81379 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Mon, 11 Nov 2024 14:39:36 +0000 Subject: [PATCH] Added QC -n option --- .../src/main/java/quickcheck/QuickCheck.java | 2 +- .../java/quickcheck/commands/QCConsole.java | 10 ++++++++++ .../quickcheck/commands/QuickCheckCommand.java | 17 ++++++++++++++++- .../quickcheck/commands/QuickCheckExecutor.java | 16 +++++++++++++++- .../commands/QuickCheckLSPCommand.java | 12 +++++++++--- 5 files changed, 51 insertions(+), 6 deletions(-) diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java index fac8004f6..43baa40f3 100644 --- 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 - timeout in millisecs"); println(" -i - only show this result status"); println(" -s - enable this strategy (below)"); diff --git a/quickcheck/src/main/java/quickcheck/commands/QCConsole.java b/quickcheck/src/main/java/quickcheck/commands/QCConsole.java index 68520c799..f1c8c8da3 100644 --- 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 includes) QCConsole.includes = includes; } + public static List 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 index 98190c5c0..04a20d3a6 100644 --- 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 ][-i ]*[-s ]* [-]* []"; + private final static String CMD = "quickcheck [-?|-help][-q|-v|-n][-t ][-i ]*[-s ]* [-]* []"; private final static String SHORT = "quickcheck [-help][][]"; 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 poNames = new Vector(); List includes = new Vector(); 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 index 726e87c30..d0e85bfdb 100644 --- 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 poList; private final List poNames; + private final boolean numbersOnly; private String answer; - public QuickCheckExecutor(DAPRequest request, QuickCheck qc, long timeout, List poList, List poNames) + public QuickCheckExecutor(DAPRequest request, QuickCheck qc, + long timeout, List poList, List 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 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 index 75a12dee7..b46a86219 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java +++ b/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java @@ -43,7 +43,7 @@ public class QuickCheckLSPCommand extends AnalysisCommand implements InitRunnable, ScriptRunnable { - public final static String CMD = "quickcheck [-?|-help][-q|-v][-t ][-i ]*[-s ]* [-]* []"; + public final static String CMD = "quickcheck [-?|-help][-q|-v|-n][-t ][-i ]*[-s ]* [-]* []"; public final static String SHORT = "quickcheck [-help][][]"; private final static String USAGE = "Usage: " + CMD; @@ -51,6 +51,7 @@ public class QuickCheckLSPCommand extends AnalysisCommand implements InitRunnabl private List poNames = new Vector(); private List includes = new Vector(); 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();