From 3c030656a461e9d73aa2c0c8c17f262acbff9f94 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Wed, 22 Jul 2020 16:08:23 +0200
Subject: [PATCH] Make :exec/:init/:constants automatically move in trace as
needed
---
CHANGELOG.md | 3 +
notebooks/tests/animate.ipynb | 300 ++++++++++++++----
.../java/de/prob2/jupyter/ProBKernel.java | 71 ++++-
3 files changed, 309 insertions(+), 65 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 525292e..35ff115 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,9 @@
* Updated ProB 2 to version 4.0.0-SNAPSHOT.
* Improved the performance of loading machines by reusing the existing instance of ProB instead of starting a new one for each machine.
+* Changed the `:exec`, `:init` and `:constants` commands to automatically move forward or backward in the trace to allow the command to execute successfully.
+ * Executing `:init` in an already initialised state will return to the last uninitialised state to re-initialise the machine (possibly with different initial values). The same works for `:constants`. Previously this caused an error "Machine is already initialised" or "Machine constants are already set up".
+ * Executing an operation in an uninitialised state will automatically initialise the machine with an arbitrary valid initialisation transition. If the machine has constants, they are also set up automatically in a similar way. This is useful if the machine's constants/initial variables are unambiguous or the exact values are not important. Previously this caused an error "Machine is not initialised".
* Significantly refactored the logic for parsing commands and their arguments.
* This is an internal change and should not affect any user-visible behavior. That is, all inputs that were accepted by previous versions should still be accepted - if any previously valid inputs are no longer accepted, this is a bug.
* As a side effect, the inspection and code completion features now work better in a few edge cases.
diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index 15c0a4c..997fb31 100644
--- a/notebooks/tests/animate.ipynb
+++ b/notebooks/tests/animate.ipynb
@@ -564,15 +564,15 @@
"outputs": [
{
"ename": "IllegalArgumentException",
- "evalue": "Executing operation $setup_constants with predicate 1=1 produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS",
+ "evalue": "Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS\u001b[0m"
+ "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope\u001b[0m"
]
}
],
"source": [
- ":constants"
+ ":exec nope"
]
},
{
@@ -582,114 +582,294 @@
"outputs": [
{
"ename": "IllegalArgumentException",
- "evalue": "Executing operation $initialise_machine with predicate 1=1 produced errors: Machine is already initialised, cannot execute INITIALISATION",
+ "evalue": "Executing operation add with predicate 1=0 produced errors: Could not execute operation add in state 6 with additional predicate (but a transition for operation exists)",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $initialise_machine with predicate 1=1 produced errors: Machine is already initialised, cannot execute INITIALISATION\u001b[0m"
+ "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation add with predicate 1=0 produced errors: Could not execute operation add in state 6 with additional predicate (but a transition for operation exists)\u001b[0m"
]
}
],
"source": [
- ":init"
+ ":exec add 1=0"
]
},
{
"cell_type": "code",
"execution_count": 25,
"metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: NoConstants"
+ ]
+ },
+ "execution_count": 25,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE NoConstants\n",
+ "VARIABLES z\n",
+ "INVARIANT z : MININT..MAXINT\n",
+ "INITIALISATION z :: {0, 1}\n",
+ "OPERATIONS\n",
+ " nothing = skip\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "metadata": {},
"outputs": [
{
"ename": "IllegalArgumentException",
- "evalue": "Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope",
+ "evalue": "Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS in state root",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope\u001b[0m"
+ "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS in state root\u001b[0m"
]
}
],
"source": [
- ":exec nope"
+ ":constants"
]
},
{
"cell_type": "code",
- "execution_count": 26,
+ "execution_count": 27,
"metadata": {},
"outputs": [
{
- "ename": "IllegalArgumentException",
- "evalue": "Executing operation add with predicate 1=0 produced errors: Could not execute operation add in state 6 with additional predicate (but a transition for operation exists)",
+ "ename": "ProBError",
+ "evalue": "ProB reported Errors\nProB returned error messages:\nError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation add with predicate 1=0 produced errors: Could not execute operation add in state 6 with additional predicate (but a transition for operation exists)\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m",
+ "\u001b[1m\u001b[31mError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)\u001b[0m",
+ "\u001b[1m\u001b[30m// Source code not known\u001b[0m"
]
}
],
"source": [
- ":exec add 1=0"
+ ":init z = -1"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Executing an operation in an uninitialised machine automatically initialises the machine."
]
},
{
"cell_type": "code",
- "execution_count": 27,
+ "execution_count": 28,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "Loaded machine: NoConstants"
+ "Machine was not initialised yet. Automatically initialised machine using arbitrary transition: INITIALISATION()\n",
+ "Executed operation: nothing()"
+ ]
+ },
+ "execution_count": 28,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec nothing"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "An already initialised machine can be reinitialised."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine was already initialised. Returned to uninitialised state to re-initialise the machine.\n",
+ "Executed operation: INITIALISATION()"
+ ]
+ },
+ "execution_count": 29,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init z = 1"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The same also works if the machine has constants."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: ItHasConstants"
]
},
- "execution_count": 27,
+ "execution_count": 30,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"::load\n",
- "MACHINE NoConstants\n",
+ "MACHINE ItHasConstants\n",
+ "CONSTANTS c\n",
+ "PROPERTIES c : MININT..MAXINT\n",
"VARIABLES z\n",
"INVARIANT z : MININT..MAXINT\n",
"INITIALISATION z :: {0, 1}\n",
+ "OPERATIONS\n",
+ " nothing = skip\n",
"END"
]
},
{
"cell_type": "code",
- "execution_count": 28,
+ "execution_count": 31,
"metadata": {},
"outputs": [
{
"ename": "IllegalArgumentException",
- "evalue": "Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS in state root",
+ "evalue": "Executing operation $initialise_machine with predicate z = 0 produced errors: Could not execute operation INITIALISATION in state root with additional predicate",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS in state root\u001b[0m"
+ "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $initialise_machine with predicate z = 0 produced errors: Could not execute operation INITIALISATION in state root with additional predicate\u001b[0m"
]
}
],
"source": [
- ":constants"
+ ":init z = 0"
]
},
{
"cell_type": "code",
- "execution_count": 29,
+ "execution_count": 32,
"metadata": {},
"outputs": [
{
- "ename": "ProBError",
- "evalue": "ProB reported Errors\nProB returned error messages:\nError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m",
- "\u001b[1m\u001b[31mError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)\u001b[0m",
- "\u001b[1m\u001b[30m// Source code not known\u001b[0m"
- ]
+ "data": {
+ "text/plain": [
+ "Executed operation: SETUP_CONSTANTS()"
+ ]
+ },
+ "execution_count": 32,
+ "metadata": {},
+ "output_type": "execute_result"
}
],
"source": [
- ":init z = -1"
+ ":constants c = 2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 33,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine was not initialised yet. Automatically initialised machine using arbitrary transition: INITIALISATION()\n",
+ "Executed operation: nothing()"
+ ]
+ },
+ "execution_count": 33,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec nothing"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 34,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine was already initialised. Returned to uninitialised state to re-initialise the machine.\n",
+ "Executed operation: INITIALISATION()"
+ ]
+ },
+ "execution_count": 34,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":init z = 1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 35,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Changed to state with index -1"
+ ]
+ },
+ "execution_count": 35,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":goto -1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 36,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Machine constants were not set up yet. Automatically set up constants using arbitrary transition: SETUP_CONSTANTS()\n",
+ "Machine was not initialised yet. Automatically initialised machine using arbitrary transition: INITIALISATION()\n",
+ "Executed operation: nothing()"
+ ]
+ },
+ "execution_count": 36,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec nothing"
]
},
{
@@ -701,7 +881,7 @@
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 37,
"metadata": {},
"outputs": [
{
@@ -710,7 +890,7 @@
"Loaded machine: Foo"
]
},
- "execution_count": 30,
+ "execution_count": 37,
"metadata": {},
"output_type": "execute_result"
}
@@ -728,7 +908,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 38,
"metadata": {},
"outputs": [
{
@@ -737,7 +917,7 @@
"Executed operation: SETUP_CONSTANTS()"
]
},
- "execution_count": 31,
+ "execution_count": 38,
"metadata": {},
"output_type": "execute_result"
}
@@ -748,7 +928,7 @@
},
{
"cell_type": "code",
- "execution_count": 32,
+ "execution_count": 39,
"metadata": {},
"outputs": [
{
@@ -757,7 +937,7 @@
"Executed operation: INITIALISATION()"
]
},
- "execution_count": 32,
+ "execution_count": 39,
"metadata": {},
"output_type": "execute_result"
}
@@ -768,7 +948,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 40,
"metadata": {},
"outputs": [
{
@@ -780,7 +960,7 @@
"1"
]
},
- "execution_count": 33,
+ "execution_count": 40,
"metadata": {},
"output_type": "execute_result"
}
@@ -791,7 +971,7 @@
},
{
"cell_type": "code",
- "execution_count": 34,
+ "execution_count": 41,
"metadata": {},
"outputs": [
{
@@ -803,7 +983,7 @@
"2"
]
},
- "execution_count": 34,
+ "execution_count": 41,
"metadata": {},
"output_type": "execute_result"
}
@@ -821,7 +1001,7 @@
},
{
"cell_type": "code",
- "execution_count": 35,
+ "execution_count": 42,
"metadata": {},
"outputs": [
{
@@ -830,7 +1010,7 @@
"Loaded machine: Counter"
]
},
- "execution_count": 35,
+ "execution_count": 42,
"metadata": {},
"output_type": "execute_result"
}
@@ -854,7 +1034,7 @@
},
{
"cell_type": "code",
- "execution_count": 36,
+ "execution_count": 43,
"metadata": {},
"outputs": [
{
@@ -866,7 +1046,7 @@
"1"
]
},
- "execution_count": 36,
+ "execution_count": 43,
"metadata": {},
"output_type": "execute_result"
}
@@ -877,7 +1057,7 @@
},
{
"cell_type": "code",
- "execution_count": 37,
+ "execution_count": 44,
"metadata": {},
"outputs": [
{
@@ -889,7 +1069,7 @@
"2"
]
},
- "execution_count": 37,
+ "execution_count": 44,
"metadata": {},
"output_type": "execute_result"
}
@@ -900,7 +1080,7 @@
},
{
"cell_type": "code",
- "execution_count": 38,
+ "execution_count": 45,
"metadata": {},
"outputs": [
{
@@ -909,7 +1089,7 @@
"Executed operation: SETUP_CONSTANTS()"
]
},
- "execution_count": 38,
+ "execution_count": 45,
"metadata": {},
"output_type": "execute_result"
}
@@ -920,7 +1100,7 @@
},
{
"cell_type": "code",
- "execution_count": 39,
+ "execution_count": 46,
"metadata": {},
"outputs": [
{
@@ -932,7 +1112,7 @@
"{−1,0,1,2}"
]
},
- "execution_count": 39,
+ "execution_count": 46,
"metadata": {},
"output_type": "execute_result"
}
@@ -943,7 +1123,7 @@
},
{
"cell_type": "code",
- "execution_count": 40,
+ "execution_count": 47,
"metadata": {},
"outputs": [
{
@@ -952,7 +1132,7 @@
"Executed operation: INITIALISATION()"
]
},
- "execution_count": 40,
+ "execution_count": 47,
"metadata": {},
"output_type": "execute_result"
}
@@ -963,7 +1143,7 @@
},
{
"cell_type": "code",
- "execution_count": 41,
+ "execution_count": 48,
"metadata": {},
"outputs": [
{
@@ -975,7 +1155,7 @@
"1"
]
},
- "execution_count": 41,
+ "execution_count": 48,
"metadata": {},
"output_type": "execute_result"
}
@@ -986,7 +1166,7 @@
},
{
"cell_type": "code",
- "execution_count": 42,
+ "execution_count": 49,
"metadata": {},
"outputs": [
{
@@ -995,7 +1175,7 @@
"Executed operation: add(-1)"
]
},
- "execution_count": 42,
+ "execution_count": 49,
"metadata": {},
"output_type": "execute_result"
}
@@ -1006,7 +1186,7 @@
},
{
"cell_type": "code",
- "execution_count": 43,
+ "execution_count": 50,
"metadata": {},
"outputs": [
{
@@ -1018,7 +1198,7 @@
"0"
]
},
- "execution_count": 43,
+ "execution_count": 50,
"metadata": {},
"output_type": "execute_result"
}
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 9f852d1..8bb100c 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -15,6 +15,7 @@ import java.util.List;
import java.util.Map;
import java.util.Optional;
import java.util.Properties;
+import java.util.Set;
import java.util.concurrent.atomic.AtomicReference;
import java.util.function.Function;
import java.util.regex.Matcher;
@@ -32,6 +33,7 @@ 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.State;
import de.prob.statespace.StateSpace;
import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
@@ -304,22 +306,81 @@ public final class ProBKernel extends BaseKernel {
this.setCurrentMachineDirectory(machineDirectory);
}
+ private static @NotNull Transition singleTransitionFromPredicate(final State state, final String opName, final String predicate) {
+ final List<Transition> ops = state.getStateSpace().transitionFromPredicate(state, opName, predicate, 1);
+ assert !ops.isEmpty();
+ return ops.get(0);
+ }
+
public @NotNull DisplayData executeOperation(final @NotNull String name, final @Nullable String predicate) {
- final Trace trace = this.animationSelector.getCurrentTrace();
+ Trace trace = this.animationSelector.getCurrentTrace();
final String translatedOpName = Transition.unprettifyName(name);
+ final StringBuilder sb = new StringBuilder();
+
+ if (Transition.SETUP_CONSTANTS_NAME.equals(translatedOpName) && trace.getCurrentState().isConstantsSetUp()) {
+ trace = trace.gotoPosition(-1);
+ sb.append("Machine constants were already set up. Returned to root state to set up machine constants again.\n");
+ } else if (Transition.INITIALISE_MACHINE_NAME.equals(translatedOpName) && trace.getCurrentState().isInitialised()) {
+ // The last uninitialised state may be at index 0 (if SETUP_CONSTANTS exists) or at index -1 (if not).
+ trace = trace.gotoPosition(0);
+ if (trace.getCurrentState().isInitialised()) {
+ trace = trace.gotoPosition(-1);
+ }
+ sb.append("Machine was already initialised. Returned to uninitialised state to re-initialise the machine.\n");
+ }
+
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);
+ Transition op;
+ try {
+ op = singleTransitionFromPredicate(trace.getCurrentState(), translatedOpName, modifiedPredicate);
+ } catch (IllegalArgumentException e) {
+ if (!trace.getCurrentState().isConstantsSetUp()) {
+ if (Transition.PARTIAL_SETUP_CONSTANTS_NAME.equals(translatedOpName) || Transition.SETUP_CONSTANTS_NAME.equals(translatedOpName)) {
+ throw e;
+ } else {
+ final Set<Transition> setupConstantsTransitions = trace.getNextTransitions();
+ if (setupConstantsTransitions.isEmpty()) {
+ throw new UserErrorException("Machine constants are not set up and no valid constant values were found automatically - cannot execute operation " + name, e);
+ }
+ final Transition setupConstants = setupConstantsTransitions.iterator().next();
+ trace = trace.add(setupConstants);
+ trace.getStateSpace().evaluateTransitions(Collections.singleton(setupConstants), FormulaExpand.TRUNCATE);
+ sb.append("Machine constants were not set up yet. Automatically set up constants using arbitrary transition: ");
+ sb.append(setupConstants.getPrettyRep());
+ sb.append('\n');
+ }
+ }
+
+ if (!trace.getCurrentState().isInitialised()) {
+ if (Transition.PARTIAL_SETUP_CONSTANTS_NAME.equals(translatedOpName) || Transition.SETUP_CONSTANTS_NAME.equals(translatedOpName) || Transition.INITIALISE_MACHINE_NAME.equals(translatedOpName)) {
+ throw e;
+ } else {
+ final Set<Transition> initialisationTransitions = trace.getNextTransitions();
+ if (initialisationTransitions.isEmpty()) {
+ throw new UserErrorException("Machine is not initialised and no valid initialisation was found automatically - cannot execute operation " + name, e);
+ }
+ final Transition initialisation = initialisationTransitions.iterator().next();
+ trace = trace.add(initialisation);
+ trace.getStateSpace().evaluateTransitions(Collections.singleton(initialisation), FormulaExpand.TRUNCATE);
+ sb.append("Machine was not initialised yet. Automatically initialised machine using arbitrary transition: ");
+ sb.append(initialisation.getPrettyRep());
+ sb.append('\n');
+ }
+ }
+
+ op = singleTransitionFromPredicate(trace.getCurrentState(), translatedOpName, modifiedPredicate);
+ }
this.animationSelector.changeCurrentAnimation(trace.add(op));
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
- return new DisplayData(String.format("Executed operation: %s", op.getPrettyRep()));
+ sb.append("Executed operation: ");
+ sb.append(op.getPrettyRep());
+ return new DisplayData(sb.toString());
}
@Override
--
GitLab