Merge branch 'master' into highprecision

nickbattle · Dec 10, 2023 · 2c3496e · 2c3496e
2 parents 39caa28 + f049654
commit 2c3496e
Show file tree

Hide file tree

Showing 6 changed files with 56 additions and 45 deletions.
diff --git 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
@@ -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,28 +72,26 @@ public FiniteQCStrategy(List<String> argv)
 					default:
 						if (arg.startsWith("-finite:"))
 						{
-							errorln("Unknown finite option: " + arg);
-							errorln(help());
+							println("Unknown finite option: " + arg);
+							println(help());
 							errorCount++;
 							iter.remove();
 						}
 				}
 			}
 			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<INBi
 				{
 					long size = bind.getType().apply(new INTypeSizeVisitor(), ctxt).longValue();
 					product = product * size;	// cumulative for each bind
+					verbose("Size of %s type is %s\n", bind, product);
 
 			   		if (product > 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
@@ -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,29 +155,26 @@ public FixedQCStrategy(List<String> argv)
 					default:
 						if (arg.startsWith("-fixed:"))
 						{
-							errorln("Unknown fixed option: " + arg);
-							errorln(help());
+							println("Unknown fixed option: " + arg);
+							println(help());
 							errorCount++;
 							iter.remove();
 						}
 				}
 			}
 			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<String, ValueList> ranges = new HashMap<String, ValueList>();
 			long before = System.currentTimeMillis();
-			printf("Expanding " + inbinds.size() + " ranges: ");
+			verbose("Expanding %d binds:\n", inbinds.size());
 
 			for (int i=0; i<inbinds.size(); i++)
 			{
@@ -285,7 +281,7 @@ else if (!TypeComparator.compatible(mbset, exptype))
 
 				ctxt.threadState.init();
 				String key = keyFor(inbinds.get(i));
-				printf(".");
+				verbose("%s\n", key);
 				INExpression exp = inexps.get(i);
 				Value value = exp.eval(ctxt);
 
@@ -318,7 +314,7 @@ else if (value instanceof IntegerValue)
 				}
 				else
 				{
-					println("\nRange does not evaluate to a set or integer " + exp.location);
+					println("Range does not evaluate to a set or integer " + exp.location);
 					errorCount++;
 				}
 			}
@@ -329,7 +325,7 @@ else if (value instanceof IntegerValue)
 			}
 
 			long after = System.currentTimeMillis();
-			println("\nRanges expanded " + duration(before, after));
+			verbose("Ranges expanded %s\n", duration(before, after));
 
 			return ranges;
 		}
@@ -496,6 +492,9 @@ public String getName()
 	@Override
 	public boolean init(QuickCheck qc)
 	{
+		verbose("fixed:size = %d\n", expansionLimit);
+		verbose("fixed:file = %s\n", rangesFile);
+
 		if (createFile)
 		{
 			createRangeFile(qc, rangesFile);
@@ -505,7 +504,7 @@ public boolean init(QuickCheck qc)
 		{
 			if (new File(rangesFile).exists())
 			{
-				println("Using ranges file " + rangesFile);
+				verbose("Using ranges file %s\n", rangesFile);
 				allRanges = readRangeFile(qc, rangesFile);
 			}
 			else

diff --git a/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.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;
@@ -84,29 +84,26 @@ public RandomQCStrategy(List<String> argv)
 					default:
 						if (arg.startsWith("-random:"))
 						{
-							errorln("Unknown random option: " + arg);
-							errorln(help());
+							println("Unknown random option: " + arg);
+							println(help());
 							errorCount++;
 							iter.remove();
 						}
 				}
 			}
 			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
@@ -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<String> 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<INBi
 					}
 				}
 			}
+
+			if (nvps.isEmpty())
+			{
+				verbose("No search patterns found\n");
+			}
 		}
 
 		return new StrategyResults(result, false, System.currentTimeMillis() - before);

diff --git a/quickcheck/src/main/java/quickcheck/strategies/TrivialQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/TrivialQCStrategy.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.List;
 import java.util.Stack;
@@ -50,8 +51,8 @@ public TrivialQCStrategy(List<String> 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<INBi
 			{
 				return new StrategyResults(getName(), visitor.getMessage(), null, System.currentTimeMillis() - before);
 			}
+
+			verbose("No trivial patterns found\n");
 		}
 
 		return new StrategyResults();	// Got nothing!