diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java index 1b4890929..82913b1bc 100644 --- a/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -25,6 +25,9 @@ package quickcheck; import static com.fujitsu.vdmj.plugins.PluginConsole.errorln; +import static com.fujitsu.vdmj.plugins.PluginConsole.infof; +import static com.fujitsu.vdmj.plugins.PluginConsole.infoln; +import static com.fujitsu.vdmj.plugins.PluginConsole.println; import static com.fujitsu.vdmj.plugins.PluginConsole.verbose; import static quickcheck.commands.QCConsole.infof; import static quickcheck.commands.QCConsole.infoln; @@ -362,7 +365,7 @@ public void checkObligation(ProofObligation po, StrategyResults results) if (!po.isCheckable) { - infof("PO #%d, UNCHECKED\n", po.number); + infof(POStatus.UNCHECKED, "PO #%d, UNCHECKED\n", po.number); return; } else if (results.provedBy != null) @@ -372,7 +375,7 @@ else if (results.provedBy != null) po.setMessage(results.message); po.setWitness(results.witness); po.setCounterexample(null); - infof("PO #%d, PROVED by %s %s %s\n", po.number, results.provedBy, results.message, duration(results.duration)); + infof(POStatus.PROVED, "PO #%d, PROVED by %s %s %s\n", po.number, results.provedBy, results.message, duration(results.duration)); return; } @@ -511,7 +514,7 @@ else if (results.hasAllValues && execCompleted) outcome = POStatus.MAYBE; } - infof("PO #%d, %s%s %s\n", po.number, outcome.toString().toUpperCase(), desc, duration(before, after)); + infof(outcome, "PO #%d, %s%s %s\n", po.number, outcome.toString().toUpperCase(), desc, duration(before, after)); po.setStatus(outcome); po.setCounterexample(null); po.setMessage(null); @@ -520,7 +523,7 @@ else if (results.hasAllValues && execCompleted) { if (didTimeout) // Result would have been true (above), but... { - infof("PO #%d, TIMEOUT %s\n", po.number, duration(before, after)); + infof(POStatus.TIMEOUT, "PO #%d, TIMEOUT %s\n", po.number, duration(before, after)); po.setStatus(POStatus.TIMEOUT); po.setCounterexample(null); po.setMessage(null); @@ -530,15 +533,15 @@ else if (po.isExistential()) // Principal exp is "exists..." { if (results.hasAllValues) { - infof("PO #%d, FAILED (unsatisfiable) %s\n", po.number, duration(before, after)); + infof(POStatus.FAILED, "PO #%d, FAILED (unsatisfiable) %s\n", po.number, duration(before, after)); po.setStatus(POStatus.FAILED); po.setMessage("Unsatisfiable"); - infoln("----"); - infoln(po); + infoln(POStatus.FAILED, "----"); + infoln(POStatus.FAILED, po.toString()); } else { - infof("PO #%d, MAYBE %s\n", po.number, duration(before, after)); + infof(POStatus.MAYBE, "PO #%d, MAYBE %s\n", po.number, duration(before, after)); po.setStatus(POStatus.MAYBE); po.setMessage(null); } @@ -548,7 +551,7 @@ else if (po.isExistential()) // Principal exp is "exists..." } else { - infof("PO #%d, FAILED %s: ", po.number, duration(before, after)); + infof(POStatus.FAILED, "PO #%d, FAILED %s: ", po.number, duration(before, after)); po.setStatus(POStatus.FAILED); printCounterexample(bindings); po.setCounterexample(findCounterexample(bindings)); @@ -557,7 +560,7 @@ else if (po.isExistential()) // Principal exp is "exists..." if (execException != null) { String msg = "Causes " + execException.getMessage(); - infoln(msg); + infoln(POStatus.FAILED, msg); po.setMessage(msg); } else @@ -565,8 +568,8 @@ else if (po.isExistential()) // Principal exp is "exists..." po.setMessage(null); } - infoln("----"); - infoln(po); + infoln(POStatus.FAILED, "----"); + infoln(POStatus.FAILED, po.toString()); } } } @@ -755,11 +758,11 @@ private void printCounterexample(List bindings) if (cex == null) { - infoln("No counterexample"); + infoln(POStatus.FAILED, "No counterexample"); } else { - infoln("Counterexample: " + cex); + infoln(POStatus.FAILED, "Counterexample: " + cex); } } @@ -802,4 +805,37 @@ private String duration(long before, long after) double duration = (double)(after - before)/1000; return "in " + duration + "s"; } + + public void printHelp(String USAGE) + { + println(USAGE); + println(""); + println(" -?|-help - show command help"); + println(" -q - run with minimal output (quiet)"); + println(" -t - timeout in secs"); + println(" -i - only show this result status"); + println(" -s - enable this strategy (below)"); + println(" - - pass option to strategy"); + println(" PO# numbers - only process these POs"); + println(" PO# - PO# - process a range of POs"); + println(" - process PO names or modules matching"); + println(""); + println("Enabled strategies:"); + + for (QCStrategy strategy: getEnabledStrategies()) + { + println(" " + strategy.help()); + } + + if (!getDisabledStrategies().isEmpty()) + { + println(""); + println("Disabled strategies (add with -s ):"); + + for (QCStrategy strategy: getDisabledStrategies()) + { + println(" " + strategy.help()); + } + } + } } diff --git a/quickcheck/src/main/java/quickcheck/commands/QCConsole.java b/quickcheck/src/main/java/quickcheck/commands/QCConsole.java index 50c237ce5..77c2b6923 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QCConsole.java +++ b/quickcheck/src/main/java/quickcheck/commands/QCConsole.java @@ -24,8 +24,12 @@ package quickcheck.commands; +import java.util.List; +import java.util.Vector; + import com.fujitsu.vdmj.messages.Console; import com.fujitsu.vdmj.plugins.PluginConsole; +import com.fujitsu.vdmj.pog.POStatus; /** * This extends the PluginConsole from VDMJ to allow us to have "global" quiet @@ -37,6 +41,7 @@ public class QCConsole extends PluginConsole { private static boolean quiet = false; + private static List includes = new Vector(); public static void setQuiet(boolean quiet) { @@ -47,26 +52,31 @@ public static boolean getQuiet() { return quiet; } + + public static void setIncludes(List includes) + { + QCConsole.includes = includes; + } - public static void info(String m) + public static void info(POStatus status, String m) { - if (!quiet) + if (!quiet && (includes.isEmpty() || includes.contains(status))) { Console.out.print(m); } } - public static void infof(String format, Object... args) + public static void infof(POStatus status, String format, Object... args) { - if (!quiet) + if (!quiet && (includes.isEmpty() || includes.contains(status))) { Console.out.printf(format, args); } } - public static void infoln(Object m) + public static void infoln(POStatus status, Object m) { - if (!quiet) + if (!quiet && (includes.isEmpty() || includes.contains(status))) { Console.out.println(m.toString()); } diff --git a/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java b/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java index 317a1073e..a90175297 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java +++ b/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java @@ -24,8 +24,8 @@ package quickcheck.commands; -import static quickcheck.commands.QCConsole.errorln; -import static quickcheck.commands.QCConsole.println; +import static com.fujitsu.vdmj.plugins.PluginConsole.errorln; +import static com.fujitsu.vdmj.plugins.PluginConsole.println; import java.util.Arrays; import java.util.List; @@ -38,16 +38,16 @@ import com.fujitsu.vdmj.plugins.AnalysisCommand; import com.fujitsu.vdmj.plugins.PluginRegistry; import com.fujitsu.vdmj.plugins.analyses.POPlugin; +import com.fujitsu.vdmj.pog.POStatus; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import quickcheck.QuickCheck; -import quickcheck.strategies.QCStrategy; import quickcheck.strategies.StrategyResults; public class QuickCheckCommand extends AnalysisCommand { - private final static String CMD = "quickcheck [-?|-help][-q][-t ][-s ]* [-]* []"; + private final static String CMD = "quickcheck [-?|-help][-q][-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"; @@ -67,6 +67,7 @@ public String run(String line) { List poList = new Vector(); List poNames = new Vector(); + List includes = new Vector(); long timeout = 0; QuickCheck qc = new QuickCheck(); @@ -91,24 +92,7 @@ public String run(String line) { case "-?": case "-help": - println(USAGE); - println("Enabled strategies:"); - - for (QCStrategy strategy: qc.getEnabledStrategies()) - { - println(" " + strategy.help()); - } - - if (!qc.getDisabledStrategies().isEmpty()) - { - println("Disabled strategies (add with -s ):"); - - for (QCStrategy strategy: qc.getDisabledStrategies()) - { - println(" " + strategy.help()); - } - } - + qc.printHelp(USAGE); return null; case "-q": @@ -119,6 +103,19 @@ public String run(String line) i++; timeout = Integer.parseInt(arglist.get(i)); break; + + case "-i": + try + { + i++; + includes.add(POStatus.valueOf(arglist.get(i).toUpperCase())); + } + catch (IllegalArgumentException e) + { + println("Not a valid PO status: " + arglist.get(i)); + return USAGE; + } + break; case "-": i++; @@ -143,7 +140,7 @@ public String run(String line) { if (arg.startsWith("-")) { - errorln("Unexpected argument: " + arg); + println("Unexpected argument: " + arg); return USAGE; } @@ -155,29 +152,31 @@ public String run(String line) } catch (IndexOutOfBoundsException e) { - errorln("Malformed arguments"); + println("Malformed arguments"); return USAGE; } catch (NumberFormatException e) { - errorln("Malformed argument: " + e.getMessage()); + println("Malformed argument: " + e.getMessage()); return USAGE; } } - + + QCConsole.setIncludes(includes); + POPlugin pog = PluginRegistry.getInstance().getPlugin("PO"); ProofObligationList all = pog.getProofObligations(); ProofObligationList chosen = qc.getPOs(all, poList, poNames); if (qc.hasErrors()) { - errorln("Failed to find POs"); + println("Failed to find POs"); return null; } if (chosen.isEmpty()) { - errorln("No POs in current " + (Settings.dialect == Dialect.VDM_SL ? "module" : "class")); + println("No POs in current " + (Settings.dialect == Dialect.VDM_SL ? "module" : "class")); return null; } diff --git a/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java b/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java index 03d917e0d..26c343f6b 100644 --- a/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java +++ b/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java @@ -24,31 +24,32 @@ package quickcheck.commands; -import static quickcheck.commands.QCConsole.errorln; -import static quickcheck.commands.QCConsole.println; +import static com.fujitsu.vdmj.plugins.PluginConsole.errorln; import java.io.IOException; import java.util.Arrays; import java.util.List; import java.util.Vector; +import com.fujitsu.vdmj.pog.POStatus; + import dap.DAPMessageList; import dap.DAPRequest; import json.JSONObject; import quickcheck.QuickCheck; -import quickcheck.strategies.QCStrategy; import vdmj.commands.AnalysisCommand; import vdmj.commands.InitRunnable; import vdmj.commands.ScriptRunnable; public class QuickCheckLSPCommand extends AnalysisCommand implements InitRunnable, ScriptRunnable { - public final static String CMD = "quickcheck [-?|-help][-q][-t ][-s ]* [-]* []"; + public final static String CMD = "quickcheck [-?|-help][-q][-t ][-i ]*[-s ]* [-]* []"; public final static String SHORT = "quickcheck [-help][][]"; private final static String USAGE = "Usage: " + CMD; private List poList = new Vector(); private List poNames = new Vector(); + private List includes = new Vector(); private long timeout = 0; private QuickCheck qc = new QuickCheck(); @@ -95,24 +96,7 @@ private DAPMessageList setup(DAPRequest request) { case "-?": case "-help": - println(USAGE); - println("Enabled strategies:"); - - for (QCStrategy strategy: qc.getEnabledStrategies()) - { - println(" " + strategy.help()); - } - - if (!qc.getDisabledStrategies().isEmpty()) - { - println("Disabled strategies (add with -s ):"); - - for (QCStrategy strategy: qc.getDisabledStrategies()) - { - println(" " + strategy.help()); - } - } - + qc.printHelp(USAGE); return result(request, null); case "-q": @@ -124,6 +108,19 @@ private DAPMessageList setup(DAPRequest request) timeout = Integer.parseInt(arglist.get(i)); break; + case "-i": + try + { + i++; + includes.add(POStatus.valueOf(arglist.get(i).toUpperCase())); + } + catch (IllegalArgumentException e) + { + errorln("Not a valid PO status: " + arglist.get(i)); + return result(request, USAGE); + } + break; + case "-": i++; int from = poList.get(poList.size() - 1); @@ -169,6 +166,8 @@ private DAPMessageList setup(DAPRequest request) } } + QCConsole.setIncludes(includes); + return null; }