Skip to content

Commit

Permalink
Merge branch 'master' into highprecision
Browse files Browse the repository at this point in the history
  • Loading branch information
@nickbattle
nickbattle committed Dec 9, 2023
2 parents 4898562 + 9c88600 commit 39caa28
Show file tree
Hide file tree
Showing 4 changed files with 58 additions and 14 deletions.
34 changes: 22 additions & 12 deletions quickcheck/src/main/java/quickcheck/QuickCheck.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,12 +25,10 @@
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;
import static quickcheck.commands.QCConsole.verbose;

import java.lang.reflect.Constructor;
import java.util.HashMap;
Expand Down Expand Up @@ -316,24 +314,36 @@ public StrategyResults getValues(ProofObligation po)

for (QCStrategy strategy: strategies)
{
verbose("Invoking %s strategy\n", strategy.getName());
StrategyResults sresults = strategy.getValues(po, exp, binds, ictxt);
Map<String, ValueList> cexamples = sresults.counterexamples;

if (sresults.provedBy != null) // No need to go further
{
verbose("Obligation proved by %s\n", strategy.getName());
sresults.setDuration(System.currentTimeMillis() - before);
return sresults;
}

for (String bind: cexamples.keySet())
if (cexamples.isEmpty())
{
if (union.containsKey(bind))
{
union.get(bind).addAll(cexamples.get(bind));
}
else
verbose("No bindings returned by %s\n", strategy.getName());
}
else
{
for (String bind: cexamples.keySet())
{
union.put(bind, cexamples.get(bind));
ValueList values = cexamples.get(bind);
verbose("%s returned %d values for %s\n", strategy.getName(), values.size(), bind);

if (union.containsKey(bind))
{
union.get(bind).addAll(values);
}
else
{
union.put(bind, values);
}
}
}

Expand Down Expand Up @@ -421,7 +431,7 @@ else if (results.provedBy != null)

try
{
verbose("PO #%d, starting...\n", po.number);
verbose("PO #%d, starting evaluation...\n", po.number);

// Suspend annotation execution by the interpreter, because the
// expressions and statements in the PO can invoke them.
Expand Down Expand Up @@ -811,7 +821,7 @@ public void printHelp(String USAGE)
println(USAGE);
println("");
println(" -?|-help - show command help");
println(" -q - run with minimal output (quiet)");
println(" -q|-v - run with minimal or verbose output");
println(" -t <secs> - timeout in secs");
println(" -i <status> - only show this result status");
println(" -s <strategy> - enable this strategy (below)");
Expand Down
22 changes: 22 additions & 0 deletions quickcheck/src/main/java/quickcheck/commands/QCConsole.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@
public class QCConsole extends PluginConsole
{
private static boolean quiet = false;
private static boolean verbose = false;
private static List<POStatus> includes = new Vector<POStatus>();

public static void setQuiet(boolean quiet)
Expand All @@ -57,6 +58,11 @@ public static void setIncludes(List<POStatus> includes)
{
QCConsole.includes = includes;
}

public static void setVerbose(boolean verbose)
{
QCConsole.verbose = verbose;
}

public static void info(POStatus status, String m)
{
Expand All @@ -81,4 +87,20 @@ public static void infoln(POStatus status, Object m)
Console.out.println(m.toString());
}
}

public static void verbose(String format, Object... args)
{
if (!quiet && verbose)
{
Console.out.printf(format, args);
}
}

public static void verboseln(String m)
{
if (!quiet && verbose)
{
Console.out.println(m);
}
}
}
9 changes: 8 additions & 1 deletion quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@

import static com.fujitsu.vdmj.plugins.PluginConsole.errorln;
import static com.fujitsu.vdmj.plugins.PluginConsole.println;
import static quickcheck.commands.QCConsole.verbose;

import java.util.Arrays;
import java.util.List;
Expand All @@ -47,7 +48,7 @@

public class QuickCheckCommand extends AnalysisCommand
{
private final static String CMD = "quickcheck [-?|-help][-q][-t <secs>][-i <status>]*[-s <strategy>]* [-<strategy:option>]* [<PO numbers/ranges/patterns>]";
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 SHORT = "quickcheck [-help][<options>][<POs>]";
private final static String USAGE = "Usage: " + CMD;
public final static String HELP = SHORT + " - lightweight PO verification";
Expand Down Expand Up @@ -83,6 +84,7 @@ public String run(String line)
}

QCConsole.setQuiet(false);
QCConsole.setVerbose(false);

for (int i=0; i < arglist.size(); i++) // Should just be POs, or -? -help
{
Expand All @@ -99,6 +101,10 @@ public String run(String line)
QCConsole.setQuiet(true);
break;

case "-v":
QCConsole.setVerbose(true);
break;

case "-t":
i++;
timeout = Integer.parseInt(arglist.get(i));
Expand Down Expand Up @@ -184,6 +190,7 @@ public String run(String line)
{
for (ProofObligation po: chosen)
{
verbose("Processing PO #%s\n", po.number);
StrategyResults results = qc.getValues(po);

if (!qc.hasErrors())
Expand Down
7 changes: 6 additions & 1 deletion quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@

public class QuickCheckLSPCommand extends AnalysisCommand implements InitRunnable, ScriptRunnable
{
public final static String CMD = "quickcheck [-?|-help][-q][-t <secs>][-i <status>]*[-s <strategy>]* [-<strategy:option>]* [<PO numbers/ranges/patterns>]";
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 SHORT = "quickcheck [-help][<options>][<POs>]";
private final static String USAGE = "Usage: " + CMD;

Expand Down Expand Up @@ -87,6 +87,7 @@ private DAPMessageList setup(DAPRequest request)
}

QCConsole.setQuiet(false);
QCConsole.setVerbose(false);

for (int i=0; i < arglist.size(); i++) // Should just be POs, or -? -help
{
Expand All @@ -103,6 +104,10 @@ private DAPMessageList setup(DAPRequest request)
QCConsole.setQuiet(true);
break;

case "-v":
QCConsole.setVerbose(true);
break;

case "-t":
i++;
timeout = Integer.parseInt(arglist.get(i));
Expand Down

0 comments on commit 39caa28

Please sign in to comment.