diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index c6e1ae6f7cbb1ad503bd335f9d2b0fca239e536d..68fef0da1fc1ef0b10f20cb1a89690e5fc595944 100644
--- a/notebooks/tests/animate.ipynb
+++ b/notebooks/tests/animate.ipynb
@@ -281,7 +281,7 @@
{
"data": {
"text/plain": [
- "Machine constants set up using operation 2: $setup_constants()"
+ "Executed operation: $setup_constants()"
]
},
"execution_count": 11,
@@ -391,7 +391,7 @@
{
"data": {
"text/plain": [
- "Machine initialised using operation 7: $initialise_machine()"
+ "Executed operation: $initialise_machine()"
]
},
"execution_count": 16,
@@ -906,7 +906,7 @@
{
"data": {
"text/plain": [
- "Machine constants set up using operation 0: $setup_constants()"
+ "Executed operation: $setup_constants()"
]
},
"execution_count": 38,
@@ -949,7 +949,7 @@
{
"data": {
"text/plain": [
- "Machine initialised using operation 3: $initialise_machine()"
+ "Executed operation: $initialise_machine()"
]
},
"execution_count": 40,
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 8513b96debc84b0cdcd582cac9b53defc2139afe..3d3f24a994b979755a9ffb181c1f8242a32f89a4 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -28,11 +28,13 @@ import com.google.inject.Singleton;
import de.prob.animator.ReusableAnimator;
import de.prob.animator.domainobjects.ErrorItem;
+import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.exception.ProBError;
import de.prob.scripting.ClassicalBFactory;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.StateSpace;
import de.prob.statespace.Trace;
+import de.prob.statespace.Transition;
import de.prob2.jupyter.commands.AssertCommand;
import de.prob2.jupyter.commands.BrowseCommand;
import de.prob2.jupyter.commands.BsymbCommand;
@@ -302,6 +304,24 @@ public final class ProBKernel extends BaseKernel {
this.setCurrentMachineDirectory(machineDirectory);
}
+ public @NotNull DisplayData executeOperation(final @NotNull String name, final @Nullable String predicate) {
+ final Trace trace = this.animationSelector.getCurrentTrace();
+ final String translatedOpName = Transition.unprettifyName(name);
+ final String modifiedPredicate;
+ if (predicate == null) {
+ modifiedPredicate = "1=1";
+ } else {
+ modifiedPredicate = this.insertLetVariables(predicate);
+ }
+ final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), translatedOpName, modifiedPredicate, 1);
+ assert !ops.isEmpty();
+ final Transition op = ops.get(0);
+
+ this.animationSelector.changeCurrentAnimation(trace.add(op));
+ trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
+ return new DisplayData(String.format("Executed operation: %s", op.getRep()));
+ }
+
@Override
public @NotNull String getBanner() {
return "ProB Interactive Expression and Predicate Evaluator (on Jupyter)\nType \":help\" for more information.";
diff --git a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
index 5bb95a3152d71f319753efa565c6e8b76da352d3..06833835b2a6acf956d1dc1a45466847a203b373 100644
--- a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
@@ -64,19 +64,7 @@ public final class ConstantsCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
- final Trace trace = this.animationSelector.getCurrentTrace();
- final String predicate;
- if (!args.get(PREDICATE_PARAM).isPresent()) {
- predicate = "1=1";
- } else {
- predicate = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM).get());
- }
- final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), "$setup_constants", predicate, 1);
- assert !ops.isEmpty();
- final Transition op = ops.get(0);
- this.animationSelector.changeCurrentAnimation(trace.add(op));
- trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
- return new DisplayData(String.format("Machine constants set up using operation %s: %s", op.getId(), op.getRep()));
+ return this.kernelProvider.get().executeOperation(Transition.SETUP_CONSTANTS_NAME, args.get(PREDICATE_PARAM).orElse(null));
}
@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
index 2d3d73c177836730645583cbb472921ca84d8307..38aa66a34f959071ee2b741495b6f5b634bc979c 100644
--- a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
@@ -70,21 +70,7 @@ public final class ExecCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
- final Trace trace = this.animationSelector.getCurrentTrace();
- final String translatedOpName = Transition.unprettifyName(args.get(OPERATION_PARAM));
- final String predicate;
- if (!args.get(PREDICATE_PARAM).isPresent()) {
- predicate = "1=1";
- } else {
- predicate = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM).get());
- }
- final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), translatedOpName, predicate, 1);
- assert !ops.isEmpty();
- final Transition op = ops.get(0);
-
- this.animationSelector.changeCurrentAnimation(trace.add(op));
- trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
- return new DisplayData(String.format("Executed operation: %s", op.getRep()));
+ return this.kernelProvider.get().executeOperation(args.get(OPERATION_PARAM), args.get(PREDICATE_PARAM).orElse(null));
}
@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
index 27d64266e6c1de1cad5af3f5f021d16f0f637d1e..eb08d94f56f586d13bf329e8e869069f6fbbdaf8 100644
--- a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
@@ -64,19 +64,7 @@ public final class InitialiseCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
- final Trace trace = this.animationSelector.getCurrentTrace();
- final String predicate;
- if (!args.get(PREDICATE_PARAM).isPresent()) {
- predicate = "1=1";
- } else {
- predicate = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM).get());
- }
- final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), "$initialise_machine", predicate, 1);
- assert !ops.isEmpty();
- final Transition op = ops.get(0);
- this.animationSelector.changeCurrentAnimation(trace.add(op));
- trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
- return new DisplayData(String.format("Machine initialised using operation %s: %s", op.getId(), op.getRep()));
+ return this.kernelProvider.get().executeOperation(Transition.INITIALISE_MACHINE_NAME, args.get(PREDICATE_PARAM).orElse(null));
}
@Override