Skip to content
Snippets Groups Projects
Commit 33e39917 authored by dgelessus's avatar dgelessus
Browse files

Add :load command to load a machine from a file

parent eeadf0a0
No related branches found
No related tags found
No related merge requests found
File moved
%% Cell type:markdown id: tags:
Machines can be loaded from files in the current directory.
%% Cell type:code id: tags:
``` prob
:load things.mch
```
%% Output
[2018-05-14 10:45:48,930, T+45662] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-05-14 10:45:50,431, T+47163] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 51537
[2018-05-14 10:45:50,432, T+47164] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 878
[2018-05-14 10:45:50,436, T+47168] "ProB Output Logger for instance cda6f00" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-14 10:45:50,460, T+47192] "ProB Output Logger for instance cda6f00" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-14 10:45:50,604, T+47336] "ProB Output Logger for instance cda6f00" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),things,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/things.mch])
Loaded machine: things : []
%% Cell type:code id: tags:
``` prob
THINGS
```
%% Output
{ONE,TWO,THREE,FOUR}
%% Cell type:markdown id: tags:
Preference values can be specified.
%% Cell type:code id: tags:
``` prob
:load things.mch MININT=-5 MAXINT=5
```
%% Output
[2018-05-14 10:46:02,661, T+59393] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-05-14 10:46:04,150, T+60882] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 51630
[2018-05-14 10:46:04,152, T+60884] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 882
[2018-05-14 10:46:04,154, T+60886] "ProB Output Logger for instance 4d195f75" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-14 10:46:04,188, T+60920] "ProB Output Logger for instance 4d195f75" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-14 10:46:04,315, T+61047] "ProB Output Logger for instance 4d195f75" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),things,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/things.mch])
Loaded machine: things : []
%% Cell type:code id: tags:
``` prob
MININT..MAXINT
```
%% Output
{−5,−4,−3,−2,−1,0,1,2,3,4,5}
MACHINE things
SETS THINGS = {ONE, TWO, THREE, FOUR}
END
......@@ -26,6 +26,7 @@ import de.prob2.jupyter.commands.CellCommand;
import de.prob2.jupyter.commands.HelpCommand;
import de.prob2.jupyter.commands.LineCommand;
import de.prob2.jupyter.commands.LoadCellCommand;
import de.prob2.jupyter.commands.LoadFileCommand;
import de.prob2.jupyter.commands.NoSuchCommandException;
import de.prob2.jupyter.commands.PrefCommand;
......@@ -56,6 +57,7 @@ public final class ProBKernel extends BaseKernel {
final LineCommand help = injector.getInstance(HelpCommand.class);
this.lineCommands.put(":?", help);
this.lineCommands.put(":help", help);
this.lineCommands.put(":load", injector.getInstance(LoadFileCommand.class));
this.lineCommands.put(":pref", injector.getInstance(PrefCommand.class));
this.cellCommands = new HashMap<>();
......
package de.prob2.jupyter.commands;
import java.io.IOException;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import com.google.inject.Inject;
import de.prob.scripting.ClassicalBFactory;
import de.prob.scripting.ModelTranslationError;
import de.prob.statespace.Trace;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.messages.DisplayData;
import org.jetbrains.annotations.NotNull;
public final class LoadFileCommand implements LineCommand {
private final ClassicalBFactory classicalBFactory;
@Inject
private LoadFileCommand(final ClassicalBFactory classicalBFactory) {
super();
this.classicalBFactory = classicalBFactory;
}
@Override
public @NotNull String getSyntax() {
return ":load FILENAME [PREF=VALUE ...]";
}
@Override
public @NotNull String getShortHelp() {
return "Load the machine from the given path.";
}
@Override
public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String name, final @NotNull List<@NotNull String> args) {
if (args.isEmpty()) {
throw new CommandExecutionException(name, "Missing machine file name");
}
final String fileName = args.get(0);
final List<String> prefArgs = args.subList(1, args.size());
final Map<String, String> preferences = new HashMap<>();
for (final String arg : prefArgs) {
final String[] split = arg.split("=", 2);
if (split.length == 1) {
throw new CommandExecutionException(name, "Missing value for preference " + split[0]);
}
preferences.put(split[0], split[1]);
}
try {
kernel.setTrace(new Trace(this.classicalBFactory.extract(fileName).load(preferences)));
} catch (IOException | ModelTranslationError e) {
throw new RuntimeException(e);
}
return new DisplayData("Loaded machine: " + kernel.getTrace().getModel());
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment