From 24839b334a4a6d6a4c197eb66249488ea2cc5576 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Thu, 2 Jul 2020 19:24:37 +0200
Subject: [PATCH] Merge implementations of :constants, :init and :exec
---
notebooks/tests/animate.ipynb | 8 ++++----
.../java/de/prob2/jupyter/ProBKernel.java | 20 +++++++++++++++++++
.../jupyter/commands/ConstantsCommand.java | 14 +------------
.../prob2/jupyter/commands/ExecCommand.java | 16 +--------------
.../jupyter/commands/InitialiseCommand.java | 14 +------------
5 files changed, 27 insertions(+), 45 deletions(-)
diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index c6e1ae6..68fef0d 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 8513b96..3d3f24a 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 5bb95a3..0683383 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 2d3d73c..38aa66a 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 27d6426..eb08d94 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
--
GitLab