From 27ae90fa96b240446a3cddadcbacb7c7698b87b1 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Tue, 10 Oct 2023 18:11:22 +0200
Subject: [PATCH] Add minimal stub handling of probcli progress and callback
 results

This doesn't actually implement them properly. Progress results are
ignored and all callbacks return call_back_not_supported.
---
 de.prob.core/src/de/prob/cli/CliStarter.java  |  2 +-
 .../de/prob/core/internal/AnimatorImpl.java   | 34 +++++++++++--------
 .../prob/core/internal/ServerConnection.java  | 16 +++++++--
 3 files changed, 34 insertions(+), 18 deletions(-)

diff --git a/de.prob.core/src/de/prob/cli/CliStarter.java b/de.prob.core/src/de/prob/cli/CliStarter.java
index a182220c..1c6b9521 100644
--- a/de.prob.core/src/de/prob/cli/CliStarter.java
+++ b/de.prob.core/src/de/prob/cli/CliStarter.java
@@ -87,7 +87,7 @@ public final class CliStarter {
 		List<String> command = new ArrayList<String>();
 		command.add(executable);
 		// command.add("-ll");
-		command.add("-sf_no_callback"); // start socket server on free port; no parser call backs available in ProB1 
+		command.add("-sf");
 		command.add("-p");command.add("use_safety_ltl_model_checker");command.add("false");
 		 // disable LTL safety model check as the counter examples lead to assertion failures 
 		 // in CounterExampleProposition in CounterExample.java
diff --git a/de.prob.core/src/de/prob/core/internal/AnimatorImpl.java b/de.prob.core/src/de/prob/core/internal/AnimatorImpl.java
index 21733a93..3b302ad1 100644
--- a/de.prob.core/src/de/prob/core/internal/AnimatorImpl.java
+++ b/de.prob.core/src/de/prob/core/internal/AnimatorImpl.java
@@ -21,11 +21,14 @@ import de.prob.core.domainobjects.History;
 import de.prob.core.domainobjects.HistoryItem;
 import de.prob.core.domainobjects.MachineDescription;
 import de.prob.core.domainobjects.State;
-import de.prob.core.sablecc.node.Start;
+import de.prob.core.sablecc.node.ACallBackResult;
+import de.prob.core.sablecc.node.AProgressResult;
+import de.prob.core.sablecc.node.AYesResult;
+import de.prob.core.sablecc.node.PResult;
 import de.prob.exceptions.ProBException;
 import de.prob.logging.Logger;
 import de.prob.parser.BindingGenerator;
-import de.prob.parser.ProBResultParser;
+import de.prob.parser.PrologTermGenerator;
 import de.prob.parser.ResultParserException;
 import de.prob.prolog.output.PrologTermStringOutput;
 import de.prob.prolog.term.PrologTerm;
@@ -74,13 +77,6 @@ public class AnimatorImpl {
 		return item == null ? null : item.getState();
 	}
 
-	private Start parseResult(final String input) {
-		if (input == null)
-			return null;
-		else
-			return ProBResultParser.parse(input);
-	}
-
 	public History getHistoryImpl() {
 		return history;
 	}
@@ -153,14 +149,22 @@ public class AnimatorImpl {
 		PrologTermStringOutput pto = new PrologTermStringOutput();
 		command.writeCommand(pto);
 		final String query = pto.fullstop().toString();
-		String input;
-		synchronized (this) {
-			input = connector.sendCommand(query);
-		}
 		Map<String, PrologTerm> bindings;
 		try {
-			final Start ast = parseResult(input);
-			bindings = BindingGenerator.createBindingMustNotFail(query, ast);
+			PResult topnode;
+			synchronized (this) {
+				topnode = connector.sendCommand(query);
+			}
+			// If probcli doesn't return anything, sendCommand throws an exception.
+			assert topnode != null;
+			// Progress and callback results are handled inside sendCommand.
+			assert !(topnode instanceof AProgressResult);
+			assert !(topnode instanceof ACallBackResult);
+
+			if (!(topnode instanceof AYesResult)) {
+				throw new ResultParserException("Prolog query failed - received " + topnode.getClass().getSimpleName() + " in response to query: " + query, null);
+			}
+			bindings = BindingGenerator.createBinding(PrologTermGenerator.toPrologTerm(topnode));
 		} catch (ResultParserException e) {
 			Logger.notifyUser(e.getMessage(), e);
 			throw new CommandException(e.getMessage(), e);
diff --git a/de.prob.core/src/de/prob/core/internal/ServerConnection.java b/de.prob.core/src/de/prob/core/internal/ServerConnection.java
index 8f7db95c..c317ef49 100644
--- a/de.prob.core/src/de/prob/core/internal/ServerConnection.java
+++ b/de.prob.core/src/de/prob/core/internal/ServerConnection.java
@@ -17,8 +17,12 @@ import java.nio.charset.Charset;
 import de.prob.cli.CliException;
 import de.prob.cli.CliStarter;
 import de.prob.core.ProblemHandler;
+import de.prob.core.sablecc.node.ACallBackResult;
+import de.prob.core.sablecc.node.AProgressResult;
+import de.prob.core.sablecc.node.PResult;
 import de.prob.exceptions.ProBException;
 import de.prob.logging.Logger;
+import de.prob.parser.ProBResultParser;
 
 public class ServerConnection {
 	private Socket socket = null;
@@ -54,14 +58,22 @@ public class ServerConnection {
 		}
 	}
 
-	public String sendCommand(final String commandString) throws ProBException {
+	public PResult sendCommand(final String commandString) throws ProBException {
 		if (shutdown) {
 			final String message = "probcli is currently shutting down";
 			ProblemHandler.raiseCliException(message);
 		}
 		checkState();
 		sendQuery(commandString);
-		return getAnswer();
+		PResult topnode = ProBResultParser.parse(getAnswer()).getPResult();
+		// Skip over all progress and callback results, which we don't support here (yet?).
+		while (topnode instanceof AProgressResult || topnode instanceof ACallBackResult) {
+			if (topnode instanceof ACallBackResult) {
+				sendQuery("call_back_not_supported.");
+			}
+			topnode = ProBResultParser.parse(getAnswer()).getPResult();
+		}
+		return topnode;
 	}
 
 	private void sendQuery(final String commandString) throws ProBException {
-- 
GitLab