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 3, 2023
2 parents 524056e + 4be9e80 commit 4fb7fb9
Show file tree
Hide file tree
Showing 4 changed files with 114 additions and 70 deletions.
64 changes: 50 additions & 14 deletions quickcheck/src/main/java/quickcheck/QuickCheck.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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)
Expand All @@ -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;
}

Expand Down Expand Up @@ -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);
Expand All @@ -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);
Expand All @@ -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);
}
Expand All @@ -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));
Expand All @@ -557,16 +560,16 @@ 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
{
po.setMessage(null);
}

infoln("----");
infoln(po);
infoln(POStatus.FAILED, "----");
infoln(POStatus.FAILED, po.toString());
}
}
}
Expand Down Expand Up @@ -755,11 +758,11 @@ private void printCounterexample(List<INBindingSetter> bindings)

if (cex == null)
{
infoln("No counterexample");
infoln(POStatus.FAILED, "No counterexample");
}
else
{
infoln("Counterexample: " + cex);
infoln(POStatus.FAILED, "Counterexample: " + cex);
}
}

Expand Down Expand Up @@ -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 <secs> - timeout in secs");
println(" -i <status> - only show this result status");
println(" -s <strategy> - enable this strategy (below)");
println(" -<strategy:option> - pass option to strategy");
println(" PO# numbers - only process these POs");
println(" PO# - PO# - process a range of POs");
println(" <pattern> - 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 <name>):");

for (QCStrategy strategy: getDisabledStrategies())
{
println(" " + strategy.help());
}
}
}
}
22 changes: 16 additions & 6 deletions quickcheck/src/main/java/quickcheck/commands/QCConsole.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -37,6 +41,7 @@
public class QCConsole extends PluginConsole
{
private static boolean quiet = false;
private static List<POStatus> includes = new Vector<POStatus>();

public static void setQuiet(boolean quiet)
{
Expand All @@ -47,26 +52,31 @@ public static boolean getQuiet()
{
return quiet;
}

public static void setIncludes(List<POStatus> 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());
}
Expand Down
55 changes: 27 additions & 28 deletions quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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 <secs>][-s <strategy>]* [-<strategy:option>]* [<PO numbers/ranges/patterns>]";
private final static String CMD = "quickcheck [-?|-help][-q][-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 All @@ -67,6 +67,7 @@ public String run(String line)
{
List<Integer> poList = new Vector<Integer>();
List<String> poNames = new Vector<String>();
List<POStatus> includes = new Vector<POStatus>();
long timeout = 0;

QuickCheck qc = new QuickCheck();
Expand All @@ -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 <name>):");

for (QCStrategy strategy: qc.getDisabledStrategies())
{
println(" " + strategy.help());
}
}

qc.printHelp(USAGE);
return null;

case "-q":
Expand All @@ -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++;
Expand All @@ -143,7 +140,7 @@ public String run(String line)
{
if (arg.startsWith("-"))
{
errorln("Unexpected argument: " + arg);
println("Unexpected argument: " + arg);
return USAGE;
}

Expand All @@ -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;
}

Expand Down
Loading

0 comments on commit 4fb7fb9

Please sign in to comment.