diff --git a/CHANGELOG.md b/CHANGELOG.md
index f7ce3363c476d13fac3e399158e6a437903c381b..817b268c70d88567f5470385756b5fe8a11f3733 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,7 @@
* Updated ProB 2 to version 4.0.0-SNAPSHOT.
* Added position information to formula evaluation errors (e. g. type or well-definedness errors).
+* Changed `:exec` and `:init` to automatically set up constants and initialize the machine if necessary. Previously this caused an error "Machine is not initialised".
* Disabled LaTeX formatting inside `:check` tables as well, because of the layout issues mentioned below.
## [1.3.0](https://www3.hhu.de/stups/downloads/prob2-jupyter/prob2-jupyter-kernel-1.3.0-all.jar)
diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index e147d18fd8660e9505c496f798f38232492219a1..41c53bbc0781266010f227b9c99f40c61de0a74a 100644
--- a/notebooks/tests/animate.ipynb
+++ b/notebooks/tests/animate.ipynb
@@ -225,11 +225,11 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: NOT-INITIALISED",
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: NOT-INITIALISED",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: NOT-INITIALISED\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mNOT-INITIALISED\u001b[0m"
]
}
],
@@ -243,11 +243,11 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: NOT-INITIALISED",
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: NOT-INITIALISED",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: NOT-INITIALISED\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mNOT-INITIALISED\u001b[0m"
]
}
],
@@ -351,11 +351,11 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: NOT-INITIALISED",
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: NOT-INITIALISED",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: NOT-INITIALISED\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mNOT-INITIALISED\u001b[0m"
]
}
],
@@ -370,11 +370,11 @@
"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:6:15 to 6:44)",
+ "evalue": "ProB reported Errors\nProB returned error messages:\nError: INITIALISATION FAILS (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:6:15 to 6:44)",
"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:6:15 to 6:44)\u001b[0m",
+ "\u001b[1m\u001b[31mError: INITIALISATION FAILS (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:6:15 to 6:44)\u001b[0m",
"\u001b[1m\u001b[30mINVARIANT value : min_value..max_value\u001b[0m",
"\u001b[1m\u001b[30mINITIALISATION \u001b[0m\u001b[1m\u001b[30m\u001b[41mvalue :: min_value..max_value\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
"\u001b[1m\u001b[30mOPERATIONS\u001b[0m"
@@ -653,6 +653,8 @@
"VARIABLES z\n",
"INVARIANT z : MININT..MAXINT\n",
"INITIALISATION z :: {0, 1}\n",
+ "OPERATIONS\n",
+ " nothing = skip\n",
"END"
]
},
@@ -681,14 +683,14 @@
"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)",
+ "evalue": "ProB reported Errors\nProB returned error messages:\nError: INITIALISATION FAILS (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/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[31mError: INITIALISATION FAILS (/Users/dgelessus/Uni/STUPS/ProB/ProB-2-Überprojekt/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)\u001b[0m",
"\u001b[1m\u001b[30mINVARIANT z : MININT..MAXINT\u001b[0m",
"\u001b[1m\u001b[30mINITIALISATION \u001b[0m\u001b[1m\u001b[30m\u001b[41mz :: {0, 1}\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
- "\u001b[1m\u001b[30mEND\u001b[0m"
+ "\u001b[1m\u001b[30mOPERATIONS\u001b[0m"
]
}
],
@@ -700,7 +702,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
- "`SETUP_CONSTANTS` and `INITIALISATION` can be used as operation names."
+ "Executing an operation in an uninitialised machine automatically initialises the machine."
]
},
{
@@ -711,7 +713,8 @@
{
"data": {
"text/plain": [
- "Loaded machine: Foo"
+ "Machine was not initialised yet. Automatically initialised machine using arbitrary transition: INITIALISATION()\n",
+ "Executed operation: nothing()"
]
},
"execution_count": 30,
@@ -719,6 +722,152 @@
"output_type": "execute_result"
}
],
+ "source": [
+ ":exec nothing"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The same also works if the machine has constants."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: ItHasConstants"
+ ]
+ },
+ "execution_count": 31,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\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": 32,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Executed operation: SETUP_CONSTANTS()"
+ ]
+ },
+ "execution_count": 32,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":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": [
+ "Changed to state with index -1"
+ ]
+ },
+ "execution_count": 34,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":goto -1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 35,
+ "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": 35,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":exec nothing"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "`SETUP_CONSTANTS` and `INITIALISATION` can be used as operation names."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 36,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Foo"
+ ]
+ },
+ "execution_count": 36,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
"source": [
"::load\n",
"MACHINE Foo\n",
@@ -732,7 +881,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 37,
"metadata": {},
"outputs": [
{
@@ -741,7 +890,7 @@
"Executed operation: SETUP_CONSTANTS()"
]
},
- "execution_count": 31,
+ "execution_count": 37,
"metadata": {},
"output_type": "execute_result"
}
@@ -752,7 +901,7 @@
},
{
"cell_type": "code",
- "execution_count": 32,
+ "execution_count": 38,
"metadata": {},
"outputs": [
{
@@ -761,7 +910,7 @@
"Executed operation: INITIALISATION()"
]
},
- "execution_count": 32,
+ "execution_count": 38,
"metadata": {},
"output_type": "execute_result"
}
@@ -772,7 +921,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 39,
"metadata": {},
"outputs": [
{
@@ -784,7 +933,7 @@
"1"
]
},
- "execution_count": 33,
+ "execution_count": 39,
"metadata": {},
"output_type": "execute_result"
}
@@ -795,7 +944,7 @@
},
{
"cell_type": "code",
- "execution_count": 34,
+ "execution_count": 40,
"metadata": {},
"outputs": [
{
@@ -807,7 +956,7 @@
"2"
]
},
- "execution_count": 34,
+ "execution_count": 40,
"metadata": {},
"output_type": "execute_result"
}
@@ -825,7 +974,7 @@
},
{
"cell_type": "code",
- "execution_count": 35,
+ "execution_count": 41,
"metadata": {},
"outputs": [
{
@@ -834,7 +983,7 @@
"Loaded machine: Counter"
]
},
- "execution_count": 35,
+ "execution_count": 41,
"metadata": {},
"output_type": "execute_result"
}
@@ -858,7 +1007,7 @@
},
{
"cell_type": "code",
- "execution_count": 36,
+ "execution_count": 42,
"metadata": {},
"outputs": [
{
@@ -870,7 +1019,7 @@
"1"
]
},
- "execution_count": 36,
+ "execution_count": 42,
"metadata": {},
"output_type": "execute_result"
}
@@ -881,7 +1030,7 @@
},
{
"cell_type": "code",
- "execution_count": 37,
+ "execution_count": 43,
"metadata": {},
"outputs": [
{
@@ -893,7 +1042,7 @@
"2"
]
},
- "execution_count": 37,
+ "execution_count": 43,
"metadata": {},
"output_type": "execute_result"
}
@@ -904,7 +1053,7 @@
},
{
"cell_type": "code",
- "execution_count": 38,
+ "execution_count": 44,
"metadata": {},
"outputs": [
{
@@ -913,7 +1062,7 @@
"Executed operation: SETUP_CONSTANTS()"
]
},
- "execution_count": 38,
+ "execution_count": 44,
"metadata": {},
"output_type": "execute_result"
}
@@ -924,7 +1073,7 @@
},
{
"cell_type": "code",
- "execution_count": 39,
+ "execution_count": 45,
"metadata": {},
"outputs": [
{
@@ -936,7 +1085,7 @@
"{−1,0,1,2}"
]
},
- "execution_count": 39,
+ "execution_count": 45,
"metadata": {},
"output_type": "execute_result"
}
@@ -947,7 +1096,7 @@
},
{
"cell_type": "code",
- "execution_count": 40,
+ "execution_count": 46,
"metadata": {},
"outputs": [
{
@@ -956,7 +1105,7 @@
"Executed operation: INITIALISATION()"
]
},
- "execution_count": 40,
+ "execution_count": 46,
"metadata": {},
"output_type": "execute_result"
}
@@ -967,7 +1116,7 @@
},
{
"cell_type": "code",
- "execution_count": 41,
+ "execution_count": 47,
"metadata": {},
"outputs": [
{
@@ -979,7 +1128,7 @@
"1"
]
},
- "execution_count": 41,
+ "execution_count": 47,
"metadata": {},
"output_type": "execute_result"
}
@@ -990,7 +1139,7 @@
},
{
"cell_type": "code",
- "execution_count": 42,
+ "execution_count": 48,
"metadata": {},
"outputs": [
{
@@ -999,7 +1148,7 @@
"Executed operation: add(-1)"
]
},
- "execution_count": 42,
+ "execution_count": 48,
"metadata": {},
"output_type": "execute_result"
}
@@ -1010,7 +1159,7 @@
},
{
"cell_type": "code",
- "execution_count": 43,
+ "execution_count": 49,
"metadata": {},
"outputs": [
{
@@ -1022,7 +1171,7 @@
"0"
]
},
- "execution_count": 43,
+ "execution_count": 49,
"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 fa3629988276156b3d352bfcd8cd2c16c275e115..8ab0af3cbe01d4cefe2e4cfbcff3463d151f18e6 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -16,6 +16,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.CancellationException;
import java.util.concurrent.ExecutionException;
import java.util.concurrent.ExecutorService;
@@ -34,6 +35,7 @@ import com.google.inject.Injector;
import com.google.inject.Singleton;
import de.prob.animator.ReusableAnimator;
+import de.prob.animator.command.ExecuteOperationException;
import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.ClassicalB;
import de.prob.animator.domainobjects.ErrorItem;
@@ -426,9 +428,7 @@ public final class ProBKernel extends BaseKernel {
}
}
- public @NotNull DisplayData executeOperation(final @NotNull String name, final @Nullable String predicate) {
- final Trace trace = this.animationSelector.getCurrentTrace();
- final String translatedOpName = Transition.unprettifyName(name);
+ private @NotNull Transition singleTransitionFromPredicate(final @Nullable String predicate, final @NotNull Trace trace, final @NotNull String translatedOpName) {
final IEvalElement parsedPredicate;
if (predicate == null) {
parsedPredicate = this.parseFormulaWithoutLetVariables("1=1", FormulaExpand.EXPAND);
@@ -437,11 +437,67 @@ public final class ProBKernel extends BaseKernel {
}
final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), translatedOpName, parsedPredicate, 1);
assert !ops.isEmpty();
- final Transition op = ops.get(0);
+ return ops.get(0);
+ }
+
+ public @NotNull DisplayData executeOperation(final @NotNull String name, final @Nullable String predicate) {
+ Trace trace = this.animationSelector.getCurrentTrace();
+ final String translatedOpName = Transition.unprettifyName(name);
+ final StringBuilder sb = new StringBuilder();
+
+ Transition op;
+ try {
+ op = this.singleTransitionFromPredicate(predicate, trace, translatedOpName);
+ } catch (ExecuteOperationException e) {
+ boolean tryAgain = false;
+ if (
+ !trace.getCurrentState().isConstantsSetUp()
+ && !Arrays.asList(Transition.PARTIAL_SETUP_CONSTANTS_NAME, Transition.SETUP_CONSTANTS_NAME).contains(translatedOpName)
+ ) {
+ LOGGER.debug("Trying to set up constants using arbitrary transition");
+ 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');
+ tryAgain = true;
+ }
+
+ if (
+ !trace.getCurrentState().isInitialised()
+ && !Arrays.asList(Transition.PARTIAL_SETUP_CONSTANTS_NAME, Transition.SETUP_CONSTANTS_NAME, Transition.INITIALISE_MACHINE_NAME).contains(translatedOpName)
+ ) {
+ LOGGER.debug("Trying to initialize machine using arbitrary transition");
+ 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');
+ tryAgain = true;
+ }
+
+ if (tryAgain) {
+ op = this.singleTransitionFromPredicate(predicate, trace, translatedOpName);
+ } else {
+ throw e;
+ }
+ }
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());
}
/**