Merge branch 'master' into highprecision

examples/lspplugin/src/main/java/examples/ExamplePluginPR.java

@@ -27,9 +27,7 @@
 import java.io.File;
 import java.io.IOException;
 import java.util.List;
-import java.util.Vector;
 
-import com.fujitsu.vdmj.messages.VDMMessage;
 import com.fujitsu.vdmj.messages.VDMWarning;
 import com.fujitsu.vdmj.tc.definitions.TCClassDefinition;
 import com.fujitsu.vdmj.tc.definitions.TCClassList;
@@ -98,9 +96,7 @@ private void addFirstWarning(CheckCompleteEvent event) throws IOException
 			if (def.name != null)
 			{
 				VDMWarning warning = new VDMWarning(9999, "Example warning from plugin", def.name.getLocation());
-				List<VDMMessage> list = new Vector<VDMMessage>();
-				list.add(warning);
-				MessageHub.getInstance().addPluginMessages(this, list);	// Add the warning to the hub
+				MessageHub.getInstance().addPluginMessage(this, warning);	// Add the warning to the hub
 				break;
 			}
 		}

examples/lspplugin/src/main/java/examples/ExamplePluginSL.java

@@ -27,9 +27,7 @@
 import java.io.File;
 import java.io.IOException;
 import java.util.List;
-import java.util.Vector;
 
-import com.fujitsu.vdmj.messages.VDMMessage;
 import com.fujitsu.vdmj.messages.VDMWarning;
 import com.fujitsu.vdmj.tc.definitions.TCDefinition;
 import com.fujitsu.vdmj.tc.modules.TCModule;
@@ -103,9 +101,7 @@ private void addFirstWarning(CheckCompleteEvent event) throws IOException
 			if (def.name != null)
 			{
 				VDMWarning warning = new VDMWarning(9999, "Example warning from plugin", def.name.getLocation());
-				List<VDMMessage> list = new Vector<VDMMessage>();
-				list.add(warning);
-				MessageHub.getInstance().addPluginMessages(this, list);	// Add the warning to the hub
+				MessageHub.getInstance().addPluginMessage(this, warning);	// Add the warning to the hub
 				break;
 			}
 		}

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

@@ -528,10 +528,22 @@ else if (results.hasAllValues && execCompleted)
 						}
 						else if (po.isExistential())	// Principal exp is "exists..."
 						{
-							infof("PO #%d, MAYBE %s\n", po.number, duration(before, after));
-							po.setStatus(POStatus.MAYBE);
+							if (results.hasAllValues)
+							{
+								infof("PO #%d, FAILED (unsatisfiable) %s\n", po.number, duration(before, after));
+								po.setStatus(POStatus.FAILED);
+								po.setMessage("Unsatisfiable");
+								infoln("----");
+								infoln(po);
+							}
+							else
+							{
+								infof("PO #%d, MAYBE %s\n", po.number, duration(before, after));
+								po.setStatus(POStatus.MAYBE);
+								po.setMessage(null);
+							}
+
 							po.setCounterexample(null);
-							po.setMessage(null);
 							po.setWitness(null);
 						}
 						else

examples/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java

@@ -0,0 +1,110 @@
+/*******************************************************************************
+ *
+ *	Copyright (c) 2023 Nick Battle.
+ *
+ *	Author: Nick Battle
+ *
+ *	This file is part of VDMJ.
+ *
+ *	VDMJ is free software: you can redistribute it and/or modify
+ *	it under the terms of the GNU General Public License as published by
+ *	the Free Software Foundation, either version 3 of the License, or
+ *	(at your option) any later version.
+ *
+ *	VDMJ is distributed in the hope that it will be useful,
+ *	but WITHOUT ANY WARRANTY; without even the implied warranty of
+ *	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ *	GNU General Public License for more details.
+ *
+ *	You should have received a copy of the GNU General Public License
+ *	along with VDMJ.  If not, see <http://www.gnu.org/licenses/>.
+ *	SPDX-License-Identifier: GPL-3.0-or-later
+ *
+ ******************************************************************************/
+
+package quickcheck.commands;
+
+import static com.fujitsu.vdmj.plugins.PluginConsole.println;
+
+import com.fujitsu.vdmj.plugins.AnalysisCommand;
+import com.fujitsu.vdmj.plugins.analyses.POPlugin;
+import com.fujitsu.vdmj.plugins.commands.PrintCommand;
+import com.fujitsu.vdmj.pog.ProofObligation;
+import com.fujitsu.vdmj.pog.ProofObligationList;
+
+/**
+ * Launch a "print" command for a PO counterexample or witness.
+ */
+public class QCRunCommand extends AnalysisCommand
+{
+	private final static String CMD = "qcrun <PO number>";
+	private final static String USAGE = "Usage: " + CMD;
+
+	public QCRunCommand(String line)
+	{
+		super(line);
+
+		if (!argv[0].equals("qcrun"))
+		{
+			throw new IllegalArgumentException(USAGE);
+		}
+	}
+
+	@Override
+	public String run(String line)
+	{
+		POPlugin po = registry.getPlugin("PO");
+		ProofObligationList all = po.getProofObligations();
+
+		if (argv.length == 2)
+		{
+    		int number = 0;
+
+			try
+			{
+				number = Integer.parseInt(argv[1]);
+			}
+			catch (NumberFormatException e)
+			{
+				return USAGE;
+			}
+
+			for (ProofObligation obligation: all)
+			{
+				if (obligation.number == number)
+				{
+					String launch = null;
+
+					if (!obligation.counterexample.isEmpty())
+					{
+						launch = obligation.getCexLaunch();
+					}
+					else if (!obligation.witness.isEmpty())
+					{
+						launch = obligation.getWitnessLaunch();
+					}
+					else
+					{
+						return "Obligation does not have a counterexample/witness. Run qc?";
+					}
+
+					String pline = "print " + launch;
+					println("> " + pline);
+					PrintCommand cmd = new PrintCommand(pline);
+					return cmd.run(pline);
+				}
+			}
+
+			return "No such obligation: " + number;
+		}
+		else
+		{
+			return USAGE;
+		}
+	}
+
+	public static void help()
+	{
+		println(CMD + " - execute counterexample/witness");
+	}
+}

examples/quickcheck/src/main/java/quickcheck/commands/QCRunLSPCommand.java

@@ -0,0 +1,109 @@
+/*******************************************************************************
+ *
+ *	Copyright (c) 2023 Nick Battle.
+ *
+ *	Author: Nick Battle
+ *
+ *	This file is part of VDMJ.
+ *
+ *	VDMJ is free software: you can redistribute it and/or modify
+ *	it under the terms of the GNU General Public License as published by
+ *	the Free Software Foundation, either version 3 of the License, or
+ *	(at your option) any later version.
+ *
+ *	VDMJ is distributed in the hope that it will be useful,
+ *	but WITHOUT ANY WARRANTY; without even the implied warranty of
+ *	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ *	GNU General Public License for more details.
+ *
+ *	You should have received a copy of the GNU General Public License
+ *	along with VDMJ.  If not, see <http://www.gnu.org/licenses/>.
+ *	SPDX-License-Identifier: GPL-3.0-or-later
+ *
+ ******************************************************************************/
+package quickcheck.commands;
+
+import static com.fujitsu.vdmj.plugins.PluginConsole.println;
+
+import com.fujitsu.vdmj.pog.ProofObligation;
+import com.fujitsu.vdmj.pog.ProofObligationList;
+
+import dap.DAPMessageList;
+import dap.DAPRequest;
+import dap.ExpressionExecutor;
+import vdmj.commands.AnalysisCommand;
+import workspace.PluginRegistry;
+import workspace.plugins.POPlugin;
+
+/**
+ * Launch a "print" command for a PO counterexample or witness.
+ */
+public class QCRunLSPCommand extends AnalysisCommand
+{
+	public static final String USAGE = "Usage: qcrun <PO number>";
+	public static final String HELP = "qcrun <PO number> - execute counterexample/witness";
+
+	private final int number;
+
+	public QCRunLSPCommand(String line)
+	{
+		super(line);
+		String[] parts = line.split("\\s+", 2);
+
+		if (parts.length != 2)
+		{
+			throw new IllegalArgumentException(USAGE);
+		}
+
+		try
+		{
+			number = Integer.parseInt(argv[1]);
+		}
+		catch (NumberFormatException e)
+		{
+			throw new IllegalArgumentException(USAGE);
+		}
+	}
+
+	@Override
+	public DAPMessageList run(DAPRequest request)
+	{
+		POPlugin po = PluginRegistry.getInstance().getPlugin("PO");
+		ProofObligationList all = po.getProofObligations();
+
+		for (ProofObligation obligation: all)
+		{
+			if (obligation.number == number)
+			{
+				String launch = null;
+
+				if (!obligation.counterexample.isEmpty())
+				{
+					launch = obligation.getCexLaunch();
+				}
+				else if (!obligation.witness.isEmpty())
+				{
+					launch = obligation.getWitnessLaunch();
+				}
+				else
+				{
+					return new DAPMessageList(request, false,
+						"Obligation does not have a counterexample/witness. Run qc?", null);
+				}
+
+				println("print " + launch);
+				ExpressionExecutor executor = new ExpressionExecutor("print", request, launch);
+				executor.start();
+				return null;
+			}
+		}
+
+		return new DAPMessageList(request, false, "No such obligation: " + number, null);
+	}
+
+	@Override
+	public boolean notWhenRunning()
+	{
+		return true;
+	}
+}

examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java

@@ -95,10 +95,15 @@ protected void exec() throws Exception
 				{
 					qc.checkObligation(po, results);
 				}
+
+				if (cancelled)
+				{
+					break;
+				}
 			}
 		}
 
-		answer = qc.hasErrors() ? "Failed" : "OK";
+		answer = qc.hasErrors() ? "Failed" : cancelled ? "Cancelled" : "OK";
 	}
 
 	@Override

examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java

@@ -28,6 +28,7 @@
 import com.fujitsu.vdmj.util.Utils;
 
 import json.JSONObject;
+import quickcheck.commands.QCRunLSPCommand;
 import quickcheck.commands.QuickCheckLSPCommand;
 import vdmj.commands.AnalysisCommand;
 import vdmj.commands.HelpList;
@@ -68,9 +69,14 @@ public AnalysisCommand getCommand(String line)
 	{
 		String[] argv = Utils.toArgv(line);
 
-		if (argv[0].equals("quickcheck") || argv[0].equals("qc"))
+		switch (argv[0])
 		{
-			return new QuickCheckLSPCommand(line);
+			case "quickcheck":
+			case "qc":
+				return new QuickCheckLSPCommand(line);
+
+			case "qcrun":
+				return new QCRunLSPCommand(line);
 		}
 
 		return null;
@@ -79,6 +85,8 @@ public AnalysisCommand getCommand(String line)
 	@Override
 	public HelpList getCommandHelp()
 	{
-		return new HelpList(QuickCheckLSPCommand.SHORT + " - lightweight PO verification");
+		return new HelpList(
+			QuickCheckLSPCommand.SHORT + " - lightweight PO verification",
+			QCRunLSPCommand.HELP);
 	}
 }

examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckPlugin.java

@@ -29,6 +29,7 @@
 import com.fujitsu.vdmj.plugins.AnalysisPlugin;
 import com.fujitsu.vdmj.util.Utils;
 
+import quickcheck.commands.QCRunCommand;
 import quickcheck.commands.QuickCheckCommand;
 
 public class QuickCheckPlugin extends AnalysisPlugin
@@ -55,9 +56,14 @@ public AnalysisCommand getCommand(String line)
 	{
 		String[] argv = Utils.toArgv(line);
 
-		if (argv[0].equals("quickcheck") || argv[0].equals("qc"))
+		switch (argv[0])
 		{
-			return new QuickCheckCommand(line);
+			case "quickcheck":
+			case "qc":
+				return new QuickCheckCommand(line);
+
+			case "qcrun":
+				return new QCRunCommand(line);
 		}
 
 		return null;
@@ -67,5 +73,6 @@ public AnalysisCommand getCommand(String line)
 	public void help()
 	{
 		QuickCheckCommand.help();
+		QCRunCommand.help();
 	}
 }

lsp/src/main/java/workspace/EventListener.java

@@ -34,11 +34,12 @@
  */
 public interface EventListener
 {
-	public final static int AST_PRIORITY = Integer.getInteger("lspx.plugins.priority.ast", 100);
-	public final static int TC_PRIORITY  = Integer.getInteger("lspx.plugins.priority.tc", 200);
-	public final static int IN_PRIORITY  = Integer.getInteger("lspx.plugins.priority.in", 300);
-	public final static int PO_PRIORITY  = Integer.getInteger("lspx.plugins.priority.po", 400);
-	public final static int CT_PRIORITY  = Integer.getInteger("lspx.plugins.priority.co", 500);
+	public final static int WS_PRIORITY  = Integer.getInteger("lspx.plugins.priority.ws", 100);
+	public final static int AST_PRIORITY = Integer.getInteger("lspx.plugins.priority.ast", 200);
+	public final static int TC_PRIORITY  = Integer.getInteger("lspx.plugins.priority.tc", 300);
+	public final static int IN_PRIORITY  = Integer.getInteger("lspx.plugins.priority.in", 400);
+	public final static int PO_PRIORITY  = Integer.getInteger("lspx.plugins.priority.po", 500);
+	public final static int CT_PRIORITY  = Integer.getInteger("lspx.plugins.priority.co", 600);
 
 	public final static int USER_PRIORITY = Integer.getInteger("lspx.plugins.priority.user", 1000);