Skip to content
Snippets Groups Projects
Commit 27ae90fa authored by dgelessus's avatar dgelessus
Browse files

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.
parent 6aaa5dd5
No related branches found
No related tags found
No related merge requests found
Pipeline #123568 passed
...@@ -87,7 +87,7 @@ public final class CliStarter { ...@@ -87,7 +87,7 @@ public final class CliStarter {
List<String> command = new ArrayList<String>(); List<String> command = new ArrayList<String>();
command.add(executable); command.add(executable);
// command.add("-ll"); // 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"); 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 // disable LTL safety model check as the counter examples lead to assertion failures
// in CounterExampleProposition in CounterExample.java // in CounterExampleProposition in CounterExample.java
......
...@@ -21,11 +21,14 @@ import de.prob.core.domainobjects.History; ...@@ -21,11 +21,14 @@ import de.prob.core.domainobjects.History;
import de.prob.core.domainobjects.HistoryItem; import de.prob.core.domainobjects.HistoryItem;
import de.prob.core.domainobjects.MachineDescription; import de.prob.core.domainobjects.MachineDescription;
import de.prob.core.domainobjects.State; 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.exceptions.ProBException;
import de.prob.logging.Logger; import de.prob.logging.Logger;
import de.prob.parser.BindingGenerator; import de.prob.parser.BindingGenerator;
import de.prob.parser.ProBResultParser; import de.prob.parser.PrologTermGenerator;
import de.prob.parser.ResultParserException; import de.prob.parser.ResultParserException;
import de.prob.prolog.output.PrologTermStringOutput; import de.prob.prolog.output.PrologTermStringOutput;
import de.prob.prolog.term.PrologTerm; import de.prob.prolog.term.PrologTerm;
...@@ -74,13 +77,6 @@ public class AnimatorImpl { ...@@ -74,13 +77,6 @@ public class AnimatorImpl {
return item == null ? null : item.getState(); 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() { public History getHistoryImpl() {
return history; return history;
} }
...@@ -153,14 +149,22 @@ public class AnimatorImpl { ...@@ -153,14 +149,22 @@ public class AnimatorImpl {
PrologTermStringOutput pto = new PrologTermStringOutput(); PrologTermStringOutput pto = new PrologTermStringOutput();
command.writeCommand(pto); command.writeCommand(pto);
final String query = pto.fullstop().toString(); final String query = pto.fullstop().toString();
String input;
synchronized (this) {
input = connector.sendCommand(query);
}
Map<String, PrologTerm> bindings; Map<String, PrologTerm> bindings;
try { try {
final Start ast = parseResult(input); PResult topnode;
bindings = BindingGenerator.createBindingMustNotFail(query, ast); 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) { } catch (ResultParserException e) {
Logger.notifyUser(e.getMessage(), e); Logger.notifyUser(e.getMessage(), e);
throw new CommandException(e.getMessage(), e); throw new CommandException(e.getMessage(), e);
......
...@@ -17,8 +17,12 @@ import java.nio.charset.Charset; ...@@ -17,8 +17,12 @@ import java.nio.charset.Charset;
import de.prob.cli.CliException; import de.prob.cli.CliException;
import de.prob.cli.CliStarter; import de.prob.cli.CliStarter;
import de.prob.core.ProblemHandler; 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.exceptions.ProBException;
import de.prob.logging.Logger; import de.prob.logging.Logger;
import de.prob.parser.ProBResultParser;
public class ServerConnection { public class ServerConnection {
private Socket socket = null; private Socket socket = null;
...@@ -54,14 +58,22 @@ public class ServerConnection { ...@@ -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) { if (shutdown) {
final String message = "probcli is currently shutting down"; final String message = "probcli is currently shutting down";
ProblemHandler.raiseCliException(message); ProblemHandler.raiseCliException(message);
} }
checkState(); checkState();
sendQuery(commandString); 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 { private void sendQuery(final String commandString) throws ProBException {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment