diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java index afcca2142..67385510d 100644 --- a/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -355,6 +355,7 @@ public StrategyResults getValues(ProofObligation po) if (!union.containsKey(bind.toString())) { // Generate some values for missing bindings, using the fixed method + verbose("Generating fixed values for %s\n", bind); ValueList list = new ValueList(); list.addAll(bind.getType().apply(new FixedRangeCreator(ictxt), 10)); union.put(bind.toString(), list); diff --git a/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java index f1647ac34..02bbaa6e4 100644 --- a/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java +++ b/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java @@ -24,8 +24,8 @@ package quickcheck.strategies; -import static com.fujitsu.vdmj.plugins.PluginConsole.errorln; -import static com.fujitsu.vdmj.plugins.PluginConsole.verbose; +import static quickcheck.commands.QCConsole.println; +import static quickcheck.commands.QCConsole.verbose; import java.util.HashMap; import java.util.Iterator; @@ -72,8 +72,8 @@ public FiniteQCStrategy(List argv) default: if (arg.startsWith("-finite:")) { - errorln("Unknown finite option: " + arg); - errorln(help()); + println("Unknown finite option: " + arg); + println(help()); errorCount++; iter.remove(); } @@ -81,19 +81,17 @@ public FiniteQCStrategy(List argv) } catch (NumberFormatException e) { - errorln("Argument must be numeric"); - errorln(help()); + println("Argument must be numeric"); + println(help()); errorCount++; } catch (ArrayIndexOutOfBoundsException e) { - errorln("Missing argument"); - errorln(help()); + println("Missing argument"); + println(help()); errorCount++; } } - - verbose("finite:size = %d\n", expansionLimit); } @Override @@ -117,6 +115,7 @@ public boolean useByDefault() @Override public boolean init(QuickCheck qc) { + verbose("finite:size = %d\n", expansionLimit); return true; } @@ -136,18 +135,22 @@ public StrategyResults getValues(ProofObligation po, INExpression exp, List expansionLimit) { + verbose("Size is greater than %d limit\n", expansionLimit); return new StrategyResults(); // Too big } } catch (InternalException e) // Infinite { + verbose("Size of bind %s is greater than %d limit\n", bind, expansionLimit); return new StrategyResults(); } catch (ArithmeticException e) // Overflow probably { + verbose("Size of bind %s is greater than %d limit\n", bind, expansionLimit); return new StrategyResults(); } } diff --git a/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java index 8a8223abf..1e1a9561d 100644 --- a/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java +++ b/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java @@ -24,10 +24,9 @@ package quickcheck.strategies; -import static com.fujitsu.vdmj.plugins.PluginConsole.errorln; -import static com.fujitsu.vdmj.plugins.PluginConsole.printf; -import static com.fujitsu.vdmj.plugins.PluginConsole.println; -import static com.fujitsu.vdmj.plugins.PluginConsole.verbose; +import static quickcheck.commands.QCConsole.println; +import static quickcheck.commands.QCConsole.errorln; +import static quickcheck.commands.QCConsole.verbose; import java.io.File; import java.io.FileWriter; @@ -156,8 +155,8 @@ public FixedQCStrategy(List argv) default: if (arg.startsWith("-fixed:")) { - errorln("Unknown fixed option: " + arg); - errorln(help()); + println("Unknown fixed option: " + arg); + println(help()); errorCount++; iter.remove(); } @@ -165,20 +164,17 @@ public FixedQCStrategy(List argv) } catch (NumberFormatException e) { - errorln("Argument must be numeric"); - errorln(help()); + println("Argument must be numeric"); + println(help()); errorCount++; } catch (ArrayIndexOutOfBoundsException e) { - errorln("Missing argument"); - errorln(help()); + println("Missing argument"); + println(help()); errorCount++; } } - - verbose("fixed:size = %d\n", expansionLimit); - verbose("fixed:file = %s\n", rangesFile); } @Override @@ -276,7 +272,7 @@ else if (!TypeComparator.compatible(mbset, exptype)) RootContext ictxt = interpreter.getInitialContext(); Map ranges = new HashMap(); long before = System.currentTimeMillis(); - printf("Expanding " + inbinds.size() + " ranges: "); + verbose("Expanding %d binds:\n", inbinds.size()); for (int i=0; i argv) default: if (arg.startsWith("-random:")) { - errorln("Unknown random option: " + arg); - errorln(help()); + println("Unknown random option: " + arg); + println(help()); errorCount++; iter.remove(); } @@ -93,20 +93,17 @@ public RandomQCStrategy(List argv) } catch (NumberFormatException e) { - errorln("Argument must be numeric"); - errorln(help()); + println("Argument must be numeric"); + println(help()); errorCount++; } catch (ArrayIndexOutOfBoundsException e) { - errorln("Missing argument"); - errorln(help()); + println("Missing argument"); + println(help()); errorCount++; } } - - verbose("random:size = %d\n", expansionLimit); - verbose("random:seed = %d\n", seed); } @Override @@ -124,6 +121,8 @@ public boolean hasErrors() @Override public boolean init(QuickCheck qc) { + verbose("random:size = %d\n", expansionLimit); + verbose("random:seed = %d\n", seed); return true; } diff --git a/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java index 0e39535df..a4eb814b0 100644 --- a/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java +++ b/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java @@ -24,7 +24,8 @@ package quickcheck.strategies; -import static com.fujitsu.vdmj.plugins.PluginConsole.errorln; +import static quickcheck.commands.QCConsole.println; +import static quickcheck.commands.QCConsole.verbose; import java.util.HashMap; import java.util.List; @@ -55,8 +56,8 @@ public SearchQCStrategy(List argv) if (argv.get(i).startsWith("-search:")) { - errorln("Unknown search option: " + argv.get(i)); - errorln(help()); + println("Unknown search option: " + argv.get(i)); + println(help()); errorCount ++; argv.remove(i); } @@ -131,6 +132,11 @@ public StrategyResults getValues(ProofObligation po, INExpression exp, List argv) if (argv.get(i).startsWith("-trivial:")) { - errorln("Unknown trivial option: " + argv.get(i)); - errorln(help()); + println("Unknown trivial option: " + argv.get(i)); + println(help()); errorCount ++; argv.remove(i); } @@ -89,6 +90,8 @@ public StrategyResults getValues(ProofObligation po, INExpression exp, List