Merge branch 'master' into highprecision

examples/quickcheck/src/main/java/quickcheck/QuickCheck.java

@@ -442,6 +442,7 @@ else if (results.provedBy != null)
 				IterableContext ictxt = addTypeParams(po, ctxt);
 				Value execResult = new BooleanValue(false);
 				ContextException exception = null;
+				boolean execCompleted = false;
 				long before = System.currentTimeMillis();
 
 				try
@@ -459,6 +460,8 @@ else if (results.provedBy != null)
 						execResult = poexp.eval(ictxt);
 					}
 					while (ictxt.hasNext() && execResult.boolValue(ctxt));
+
+					execCompleted = true;
 				}
 				catch (ContextException e)
 				{
@@ -468,7 +471,8 @@ else if (results.provedBy != null)
 					}
 					else if (e.number == 4024)	// 'not yet specified' expression reached
 					{
-						execResult = new BooleanValue(true);	// MAYBE, in effect
+						// MAYBE, in effect - execCompleted will be false
+						execResult = new BooleanValue(!po.isExistential());
 					}
 					else
 					{
@@ -506,25 +510,32 @@ else if (execResult instanceof BooleanValue)
 					if (execResult.boolValue(ctxt))
 					{
 						POStatus outcome = null;
+						String message = "";
 
 						if (didTimeout)
 						{
 							outcome = POStatus.TIMEOUT;
 						}
-						else if (po.kind.isExistential())
+						else if (po.isExistential())
 						{
 							outcome = POStatus.PROVED;		// An "exists" PO is PROVED, if true.
+							Context path = getWitness(bindings);
+							String w = stringOfContext(path);
+							po.setWitness(w);
+							if (w != null) message = " witness " + w;
 						}
-						else if (results.hasAllValues)
+						else if (results.hasAllValues && execCompleted)
 						{
 							outcome = POStatus.PROVED;		// All values were tested and passed, so PROVED
+							message = " by finite types";
+							po.setProvedBy("finite");
 						}
 						else
 						{
 							outcome = POStatus.MAYBE;
 						}
 
-						infof("PO #%d, %s %s\n", po.number, outcome.toString().toUpperCase(), duration(before, after));
+						infof("PO #%d, %s%s %s\n", po.number, outcome.toString().toUpperCase(), message, duration(before, after));
 						po.setStatus(outcome);
 						po.setCounterexample(null);
 						po.setCounterMessage(null);
@@ -538,7 +549,7 @@ else if (results.hasAllValues)
 							po.setCounterexample(null);
 							po.setCounterMessage(null);
 						}
-						else if (po.kind.isExistential())	// Principal exp is "exists..."
+						else if (po.isExistential())	// Principal exp is "exists..."
 						{
 							infof("PO #%d, MAYBE %s\n", po.number, duration(before, after));
 							po.setStatus(POStatus.MAYBE);
@@ -549,7 +560,8 @@ else if (po.kind.isExistential())	// Principal exp is "exists..."
 						{
 							infof("PO #%d, FAILED %s: ", po.number, duration(before, after));
 							po.setStatus(POStatus.FAILED);
-							po.setCounterexample(printFailPath(bindings));
+							printCounterexample(bindings);
+							po.setCounterexample(getCounterexample(bindings));
 
 							if (exception != null)
 							{
@@ -569,21 +581,22 @@ else if (po.kind.isExistential())	// Principal exp is "exists..."
 				}
 				else
 				{
-					String msg = String.format("Error: PO evaluation returns %s?\n", execResult.kind());
-					infof("PO #%d, %s\n", po.number, msg);
+					String msg = String.format("Error: PO #%d evaluation returns %s?\n", po.number, execResult.kind());
+					infoln(msg);
 					po.setStatus(POStatus.FAILED);
 					po.setCounterexample(null);
 					po.setCounterMessage(msg);
 					infoln("----");
 					printBindings(bindings);
 					infoln("----");
 					infoln(po);
+					errorCount++;
 				}
 			}
 			catch (Exception e)
 			{
-				String msg = String.format("Exception: %s", e.getMessage());
-				infof("PO #%d, %s\n", po.number, msg);
+				String msg = String.format("Exception: PO #%d %s", po.number, e.getMessage());
+				infoln(msg);
 				po.setStatus(POStatus.FAILED);
 				po.setCounterexample(null);
 				po.setCounterMessage(msg);
@@ -681,44 +694,81 @@ private void printBindings(List<INBindingSetter> bindings)
 		}
 	}
 
-	private Context printFailPath(List<INBindingSetter> bindings)
+	private Context getCounterexample(List<INBindingSetter> bindings)
 	{
-		Context path = null;
+		Context ctxt = null;
 
 		for (INBindingSetter setter: bindings)
 		{
-			path = setter.getCounterexample();
+			ctxt = setter.getCounterexample();
 
-			if (path != null)
+			if (ctxt != null)
 			{
 				break;	// Any one will do - see INForAllExpression
 			}
 		}
+
+		return ctxt;
+	}
+
+	private Context getWitness(List<INBindingSetter> bindings)
+	{
+		Context ctxt = null;
 
+		for (INBindingSetter setter: bindings)
+		{
+			ctxt = setter.getWitness();
+
+			if (ctxt != null)
+			{
+				break;	// Any one will do - see INExistsExpression
+			}
+		}
+
+		return ctxt;
+	}
+
+	private void printCounterexample(List<INBindingSetter> bindings)
+	{
+		Context path = getCounterexample(bindings);
+		String cex = stringOfContext(path);
+
+		if (cex == null)
+		{
+			infoln("No counterexample");
+		}
+		else
+		{
+			infoln("Counterexample: " + cex);
+		}
+	}
+
+	private String stringOfContext(Context path)
+	{
 		if (path == null || path.isEmpty())
 		{
-			infof("No counterexample\n");
-			printBindings(bindings);
 			return null;
 		}
 
-		infof("Counterexample: ");
+		StringBuilder result = new StringBuilder();
 		String sep = "";
 		Context ctxt = path;
 
 		while (ctxt.outer != null)
 		{
 			for (TCNameToken name: ctxt.keySet())
 			{
-				infof("%s%s = %s", sep, name, ctxt.get(name));
+				result.append(sep);
+				result.append(name);
+				result.append(" = ");
+				result.append(ctxt.get(name));
 				sep = ", ";
 			}
 
 			ctxt = ctxt.outer;
 		}
 
-		infoln("");
-		return path;
+		return result.toString();
 	}
 
 	private String duration(long time)

lsp/src/main/java/workspace/plugins/POPlugin.java

@@ -233,6 +233,11 @@ else if (file.isDirectory())
 				messages.add(new VDMWarning(9001, po.countermessage, po.location));
 			}
 
+			if (po.witness != null)
+			{
+				json.put("witness", "PO #" + po.number + ": " + po.witness);
+			}
+
 			poList.add(json);
 		}
 

stdlib/src/main/java/VDMUtil.java

@@ -68,7 +68,7 @@ public static Value val2seq_of_char(Value arg)
 	}
 
 	@VDMFunction
-	public static Value seq_of_char2val(Value arg)
+	public static Value seq_of_char2val_(Value arg)		// Note, with underscore - see VDM
 	{
 		ValueList result = new ValueList();
 
@@ -93,7 +93,7 @@ public static Value seq_of_char2val(Value arg)
 			INExpression inexp = ClassMapper.getInstance(INNode.MAPPINGS).convert(tcexp);
 
 			result.add(new BooleanValue(true));
-			Context ctxt = new Context(null, "seq_of_char2val", null);
+			Context ctxt = new Context(null, "seq_of_char2val_", null);
 			ctxt.setThreadState(null);
 			result.add(inexp.eval(ctxt));
 		}
@@ -123,7 +123,7 @@ public static Value classname(Value arg)
 		}
 	}
 
-	public Value get_file_pos(Context ctxt)
+	public static Value get_file_pos(Context ctxt)
 	{
 		try
 		{

stdlib/src/main/resources/VDMUtil.vdmpp

@@ -29,8 +29,12 @@ val2seq_of_char(x) == is not yet specified;
 -- RESULT.#1 = false implies a conversion failure
 static public seq_of_char2val[@p]:seq1 of char -> bool * [@p]
 seq_of_char2val(s) ==
-  is not yet specified
-  post let mk_(b,t) = RESULT in not b => t = nil;
+let mk_(b, v) = seq_of_char2val_(s) in
+    if is_(v, @p) then mk_(b, v) else mk_(false, nil)
+post let mk_(b,t) = RESULT in not b => t = nil;
+
+static seq_of_char2val_:seq1 of char -> bool * ?
+seq_of_char2val_(s) == is not yet specified
 
 static public classname[@T] : @T -> [seq1 of char]
 	classname(s) == is not yet specified;

stdlib/src/main/resources/VDMUtil.vdmrt

@@ -29,8 +29,12 @@ val2seq_of_char(x) == is not yet specified;
 -- RESULT.#1 = false implies a conversion failure
 static public seq_of_char2val[@p]:seq1 of char -> bool * [@p]
 seq_of_char2val(s) ==
-  is not yet specified
-  post let mk_(b,t) = RESULT in not b => t = nil;
+let mk_(b, v) = seq_of_char2val_(s) in
+    if is_(v, @p) then mk_(b, v) else mk_(false, nil)
+post let mk_(b,t) = RESULT in not b => t = nil;
+
+static seq_of_char2val_:seq1 of char -> bool * ?
+seq_of_char2val_(s) == is not yet specified
 
 static public classname[@T] : @T -> [seq1 of char]
 	classname(s) == is not yet specified;

vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java

@@ -109,6 +109,7 @@ public Value eval(Context ctxt)
 					{
 						if (!v.equals(nvp.value))
 						{
+							setWitness(evalContext);
 							matches = false;
 							break;	// This quantifier set does not match
 						}
@@ -119,6 +120,7 @@ public Value eval(Context ctxt)
 				{
 					if (matches && predicate.eval(evalContext).boolValue(ctxt))
 					{
+						setWitness(evalContext);
 						return new BooleanValue(true);
 					}
 				}
@@ -177,6 +179,26 @@ private void setCounterexample(Context ctxt, boolean didTimeout)
 			}
 		}
 	}
+
+	/**
+	 * This is used by the QuickCheck plugin to report which values succeeded.
+	 */
+	private void setWitness(Context ctxt)
+	{
+		for (INMultipleBind bind: bindList)
+		{
+			if (bind instanceof INBindingSetter)			// Type and multitype binds
+			{
+				INBindingSetter setter = (INBindingSetter)bind;
+
+				if (setter.getBindValues() != null)			// One we care about (set QC values for)
+				{
+					setter.setWitness(ctxt);
+					break;									// Just one will do - see QC printFailPath
+				}
+			}
+		}
+	}
 
 	@Override
 	public <R, S> R apply(INExpressionVisitor<R, S> visitor, S arg)

vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingSetter.java

@@ -37,4 +37,6 @@ public interface INBindingSetter
 	public TCType getType();
 	public void setCounterexample(Context ctxt, boolean didTimeout);
 	public Context getCounterexample();
+	public void setWitness(Context ctxt);
+	public Context getWitness();
 }

vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java

@@ -44,6 +44,7 @@ public class INMultipleTypeBind extends INMultipleBind implements INBindingSette
 
 	private ValueList bindValues = null;
 	private Context bindCounterexample = null;
+	private Context bindWitness = null;
 	private boolean bindPermuted = false;
 	private boolean bindOverride = false;
 	private long bindTimeout = 0;
@@ -80,6 +81,8 @@ public void setBindValues(ValueList values, long timeout)
 		}
 
 		didTimeout = false;
+		bindCounterexample = null;
+		bindWitness = null;
 	}
 
 	@Override
@@ -121,6 +124,25 @@ public Context getCounterexample()
 		return bindCounterexample;
 	}
 
+	@Override
+	public void setWitness(Context ctxt)
+	{
+		if (ctxt == null)
+		{
+			bindWitness = null;
+		}
+		else if (bindWitness == null)	// Catch first witness, don't overwrite
+		{
+			bindWitness = ctxt;
+		}
+	}
+
+	@Override
+	public Context getWitness()
+	{
+		return bindWitness;
+	}
+
 	@Override
 	public TCType getType()
 	{