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

Remove ProBKernel.trace field and use AnimationSelector instead 

This also allows Groovy code to access the current trace.
parent 5310dd2b
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
notebooks/tests/groovy.ipynb
+ 22
− 0
View file @ f654fd86
%% Cell type:code id: tags:
``` prob
:help :groovy
```
%% Output
:groovy EXPRESSION
Evaluate the given Groovy expression.
%% Cell type:code id: tags:
``` prob
:groovy ["one": 1, "two": 2, "three": 3]["two"]
```
%% Output
2
%% Cell type:code id: tags:
``` prob
:groovy print("hello")
```
%% Output
hello
null
%% Cell type:code id: tags:
``` prob
:groovy animations.currentTrace
```
%% Output
Operations:
Possibly not all transitions shown. ProB does not explore states by default
......
src/main/java/de/prob2/jupyter/ProBKernel.java
+ 9
− 13
View file @ f654fd86
......@@ -17,6 +17,7 @@ import de.prob.animator.domainobjects.EvalResult;
import de.prob.animator.domainobjects.EvaluationErrorResult;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.scripting.ClassicalBFactory;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob.unicode.UnicodeTranslator;
......@@ -44,14 +45,17 @@ public final class ProBKernel extends BaseKernel {
private static final Pattern CELL_COMMAND_PATTERN = Pattern.compile("\\s*(\\:\\:[^\\n\\h]*)(?:\\h+([^\\n]*))?(?:\\n(.*))?", Pattern.DOTALL);
private static final Pattern LINE_COMMAND_PATTERN = Pattern.compile("\\s*(\\:[^\\h]*)(?:\\h+(.*))?");
private final @NotNull AnimationSelector animationSelector;
private final @NotNull Map<@NotNull String, @NotNull LineCommand> lineCommands;
private final @NotNull Map<@NotNull String, @NotNull CellCommand> cellCommands;
private @NotNull Trace trace;
@Inject
private ProBKernel(final @NotNull Injector injector, final @NotNull ClassicalBFactory classicalBFactory) {
private ProBKernel(final @NotNull Injector injector, final @NotNull ClassicalBFactory classicalBFactory, final @NotNull AnimationSelector animationSelector) {
super();
this.animationSelector = animationSelector;
this.lineCommands = new HashMap<>();
final LineCommand help = injector.getInstance(HelpCommand.class);
this.lineCommands.put(":?", help);
......@@ -63,7 +67,7 @@ public final class ProBKernel extends BaseKernel {
this.cellCommands = new HashMap<>();
this.cellCommands.put("::load", injector.getInstance(LoadCellCommand.class));
this.trace = new Trace(classicalBFactory.create("MACHINE repl END").load());
this.animationSelector.changeCurrentAnimation(new Trace(classicalBFactory.create("MACHINE repl END").load()));
}
public @NotNull Map<@NotNull String, @NotNull CellCommand> getCellCommands() {
......@@ -74,14 +78,6 @@ public final class ProBKernel extends BaseKernel {
return Collections.unmodifiableMap(this.lineCommands);
}
public @NotNull Trace getTrace() {
return this.trace;
}
public void setTrace(final @NotNull Trace trace) {
this.trace = trace;
}
@Override
public @NotNull String getBanner() {
return "ProB Interactive Expression and Predicate Evaluator (on Jupyter)\nType \":help\" for more information.";
......@@ -177,7 +173,7 @@ public final class ProBKernel extends BaseKernel {
return this.executeLineCommand(name, argString);
}
return this.displayDataForEvalResult(this.trace.evalCurrent(expr, FormulaExpand.EXPAND));
return this.displayDataForEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(expr, FormulaExpand.EXPAND));
}
@Override
......@@ -190,7 +186,7 @@ public final class ProBKernel extends BaseKernel {
@Override
public void onShutdown(final boolean isRestarting) {
this.trace.getStateSpace().kill();
this.animationSelector.getCurrentTrace().getStateSpace().kill();
}
@Override
......
src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
+ 6
− 3
View file @ f654fd86
......@@ -6,6 +6,7 @@ import java.util.Map;
import com.google.inject.Inject;
import de.prob.scripting.ClassicalBFactory;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.ProBKernel;
......@@ -16,12 +17,14 @@ import org.jetbrains.annotations.NotNull;
public final class LoadCellCommand implements CellCommand {
private final @NotNull ClassicalBFactory classicalBFactory;
private final @NotNull AnimationSelector animationSelector;
@Inject
private LoadCellCommand(final @NotNull ClassicalBFactory classicalBFactory) {
private LoadCellCommand(final @NotNull ClassicalBFactory classicalBFactory, final @NotNull AnimationSelector animationSelector) {
super();
this.classicalBFactory = classicalBFactory;
this.animationSelector = animationSelector;
}
@Override
......@@ -39,7 +42,7 @@ public final class LoadCellCommand implements CellCommand {
final List<String> args = CommandUtils.splitArgs(argString);
final Map<String, String> preferences = CommandUtils.parsePreferences(name, args);
kernel.setTrace(new Trace(this.classicalBFactory.create(body).load(preferences)));
return new DisplayData("Loaded machine: " + kernel.getTrace().getModel());
this.animationSelector.changeCurrentAnimation(new Trace(this.classicalBFactory.create(body).load(preferences)));
return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getModel());
}
}
src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
+ 7
− 4
View file @ f654fd86
......@@ -8,6 +8,7 @@ import com.google.inject.Inject;
import de.prob.scripting.ClassicalBFactory;
import de.prob.scripting.ModelTranslationError;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.ProBKernel;
......@@ -17,13 +18,15 @@ import io.github.spencerpark.jupyter.messages.DisplayData;
import org.jetbrains.annotations.NotNull;
public final class LoadFileCommand implements LineCommand {
private final ClassicalBFactory classicalBFactory;
private final @NotNull ClassicalBFactory classicalBFactory;
private final @NotNull AnimationSelector animationSelector;
@Inject
private LoadFileCommand(final ClassicalBFactory classicalBFactory) {
private LoadFileCommand(final @NotNull ClassicalBFactory classicalBFactory, final @NotNull AnimationSelector animationSelector) {
super();
this.classicalBFactory = classicalBFactory;
this.animationSelector = animationSelector;
}
@Override
......@@ -47,10 +50,10 @@ public final class LoadFileCommand implements LineCommand {
final Map<String, String> preferences = CommandUtils.parsePreferences(name, args.subList(1, args.size()));
try {
kernel.setTrace(new Trace(this.classicalBFactory.extract(fileName).load(preferences)));
this.animationSelector.changeCurrentAnimation(new Trace(this.classicalBFactory.extract(fileName).load(preferences)));
} catch (IOException | ModelTranslationError e) {
throw new RuntimeException(e);
}
return new DisplayData("Loaded machine: " + kernel.getTrace().getModel());
return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getModel());
}
}
src/main/java/de/prob2/jupyter/commands/PrefCommand.java
+ 9
− 4
View file @ f654fd86
......@@ -10,6 +10,7 @@ import de.prob.animator.command.ComposedCommand;
import de.prob.animator.command.GetCurrentPreferencesCommand;
import de.prob.animator.command.GetPreferenceCommand;
import de.prob.animator.command.SetPreferenceCommand;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.ProBKernel;
......@@ -18,9 +19,13 @@ import io.github.spencerpark.jupyter.messages.DisplayData;
import org.jetbrains.annotations.NotNull;
public final class PrefCommand implements LineCommand {
private final @NotNull AnimationSelector animationSelector;
@Inject
private PrefCommand() {
private PrefCommand(final @NotNull AnimationSelector animationSelector) {
super();
this.animationSelector = animationSelector;
}
@Override
......@@ -39,7 +44,7 @@ public final class PrefCommand implements LineCommand {
final StringBuilder sb = new StringBuilder();
if (args.isEmpty()) {
final GetCurrentPreferencesCommand cmd = new GetCurrentPreferencesCommand();
kernel.getTrace().getStateSpace().execute(cmd);
this.animationSelector.getCurrentTrace().getStateSpace().execute(cmd);
// TreeMap is used to sort the preferences by name.
new TreeMap<>(cmd.getPreferences()).forEach((k, v) -> {
sb.append(k);
......@@ -57,7 +62,7 @@ public final class PrefCommand implements LineCommand {
sb.append(value);
sb.append('\n');
});
kernel.getTrace().getStateSpace().execute(new ComposedCommand(cmds));
this.animationSelector.getCurrentTrace().getStateSpace().execute(new ComposedCommand(cmds));
} else {
final List<GetPreferenceCommand> cmds = new ArrayList<>();
for (final String arg : args) {
......@@ -66,7 +71,7 @@ public final class PrefCommand implements LineCommand {
}
cmds.add(new GetPreferenceCommand(arg));
}
kernel.getTrace().getStateSpace().execute(new ComposedCommand(cmds));
this.animationSelector.getCurrentTrace().getStateSpace().execute(new ComposedCommand(cmds));
for (final GetPreferenceCommand cmd : cmds) {
sb.append(cmd.getKey());
sb.append(" = ");
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment