From f522d4448f82d8270e7980c73cd31626136cde7d Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Wed, 20 Jun 2018 15:32:31 +0200
Subject: [PATCH] Show better error messages when :constants or :init are not
possible
---
notebooks/tests/animate.ipynb | 102 ++++++++++++------
.../jupyter/commands/ConstantsCommand.java | 8 +-
.../jupyter/commands/InitialiseCommand.java | 8 +-
3 files changed, 86 insertions(+), 32 deletions(-)
diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index a470eae..30c76d6 100644
--- a/notebooks/tests/animate.ipynb
+++ b/notebooks/tests/animate.ipynb
@@ -317,6 +317,9 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$\\{-1,0,1,2\\}$"
+ ],
"text/plain": [
"{−1,0,1,2}"
]
@@ -422,6 +425,9 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$2$"
+ ],
"text/plain": [
"2"
]
@@ -490,6 +496,9 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$1$"
+ ],
"text/plain": [
"1"
]
@@ -583,10 +592,10 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":constants: Could not setup constants",
+ "evalue": ":constants: Machine constants are already set up",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:constants: Could not setup constants\u001b[0m"
+ "\u001b[1m\u001b[31m:constants: Machine constants are already set up\u001b[0m"
]
}
],
@@ -601,15 +610,15 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":constants: Could not setup constants with the specified predicate",
+ "evalue": ":init: Machine is already initialised",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:constants: Could not setup constants with the specified predicate\u001b[0m"
+ "\u001b[1m\u001b[31m:init: Machine is already initialised\u001b[0m"
]
}
],
"source": [
- ":constants 1=1"
+ ":init"
]
},
{
@@ -619,15 +628,15 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":init: Could not initialise machine",
+ "evalue": ":exec: Could not execute operation nope",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:init: Could not initialise machine\u001b[0m"
+ "\u001b[1m\u001b[31m:exec: Could not execute operation nope\u001b[0m"
]
}
],
"source": [
- ":init"
+ ":exec nope"
]
},
{
@@ -637,51 +646,77 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":init: Could not initialise machine with the specified predicate",
+ "evalue": ":exec: Could not execute operation add with the given predicate",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:init: Could not initialise machine with the specified predicate\u001b[0m"
+ "\u001b[1m\u001b[31m:exec: Could not execute operation add with the given predicate\u001b[0m"
]
}
],
"source": [
- ":init 1=1"
+ ":exec add 1=0"
]
},
{
"cell_type": "code",
"execution_count": 29,
"metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: NoConstants : []\n"
+ ]
+ },
+ "execution_count": 29,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE NoConstants\n",
+ "VARIABLES z\n",
+ "INVARIANT z : MININT..MAXINT\n",
+ "INITIALISATION z :: {0, 1}\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "metadata": {},
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":exec: Could not execute operation nope",
+ "evalue": ":constants: Machine has no constants, use :init instead",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:exec: Could not execute operation nope\u001b[0m"
+ "\u001b[1m\u001b[31m:constants: Machine has no constants, use :init instead\u001b[0m"
]
}
],
"source": [
- ":exec nope"
+ ":constants"
]
},
{
"cell_type": "code",
- "execution_count": 30,
+ "execution_count": 31,
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":exec: Could not execute operation add with the given predicate",
+ "ename": "ProBError",
+ "evalue": "ProB reported Errors\nProB returned error messages:\nError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests:4:15 to 4:26)",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:exec: Could not execute operation add with the given predicate\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:4:15 to 4:26)\u001b[0m"
]
}
],
"source": [
- ":exec add 1=0"
+ ":init z = -1"
]
},
{
@@ -693,7 +728,7 @@
},
{
"cell_type": "code",
- "execution_count": 31,
+ "execution_count": 32,
"metadata": {},
"outputs": [
{
@@ -702,7 +737,7 @@
"Loaded machine: Foo : []\n"
]
},
- "execution_count": 31,
+ "execution_count": 32,
"metadata": {},
"output_type": "execute_result"
}
@@ -720,7 +755,7 @@
},
{
"cell_type": "code",
- "execution_count": 32,
+ "execution_count": 33,
"metadata": {},
"outputs": [
{
@@ -729,7 +764,7 @@
"Executed operation 2: $setup_constants()"
]
},
- "execution_count": 32,
+ "execution_count": 33,
"metadata": {},
"output_type": "execute_result"
}
@@ -740,7 +775,7 @@
},
{
"cell_type": "code",
- "execution_count": 33,
+ "execution_count": 34,
"metadata": {},
"outputs": [
{
@@ -749,7 +784,7 @@
"Executed operation 7: $initialise_machine()"
]
},
- "execution_count": 33,
+ "execution_count": 34,
"metadata": {},
"output_type": "execute_result"
}
@@ -760,16 +795,19 @@
},
{
"cell_type": "code",
- "execution_count": 34,
+ "execution_count": 35,
"metadata": {},
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$1$"
+ ],
"text/plain": [
"1"
]
},
- "execution_count": 34,
+ "execution_count": 35,
"metadata": {},
"output_type": "execute_result"
}
@@ -780,16 +818,19 @@
},
{
"cell_type": "code",
- "execution_count": 35,
+ "execution_count": 36,
"metadata": {},
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$2$"
+ ],
"text/plain": [
"2"
]
},
- "execution_count": 35,
+ "execution_count": 36,
"metadata": {},
"output_type": "execute_result"
}
@@ -806,8 +847,9 @@
"name": "prob2"
},
"language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
"file_extension": ".prob",
- "mimetype": "text/x-prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
"name": "prob"
}
},
diff --git a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
index 9dad437..d12caae 100644
--- a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
@@ -43,7 +43,13 @@ public final class ConstantsCommand implements Command {
final List<String> predicates = argString.isEmpty() ? Collections.emptyList() : Collections.singletonList(argString);
final Transition op = trace.getCurrentState().findTransition("$setup_constants", predicates);
if (op == null) {
- throw new UserErrorException("Could not setup constants" + (argString.isEmpty() ? "" : " with the specified predicate"));
+ if (trace.gotoPosition(-1).canExecuteEvent("$initialise_machine")) {
+ throw new UserErrorException("Machine has no constants, use :init instead");
+ } else if (trace.getCurrent().getIndex() > -1) {
+ throw new UserErrorException("Machine constants are already set up");
+ } else {
+ throw new UserErrorException("Could not setup constants" + (argString.isEmpty() ? "" : " with the specified predicate"));
+ }
}
this.animationSelector.changeCurrentAnimation(trace.add(op));
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
diff --git a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
index 704793b..52fe6e7 100644
--- a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
@@ -43,7 +43,13 @@ public final class InitialiseCommand implements Command {
final List<String> predicates = argString.isEmpty() ? Collections.emptyList() : Collections.singletonList(argString);
final Transition op = trace.getCurrentState().findTransition("$initialise_machine", predicates);
if (op == null) {
- throw new UserErrorException("Could not initialise machine" + (argString.isEmpty() ? "" : " with the specified predicate"));
+ if (trace.getCurrentState().isInitialised()) {
+ throw new UserErrorException("Machine is already initialised");
+ } else if (trace.getHead().getPrevious() == null && trace.canExecuteEvent("$setup_constants")) {
+ throw new UserErrorException("Machine constants are not yet set up, use :constants first");
+ } else {
+ throw new UserErrorException("Could not initialise machine" + (argString.isEmpty() ? "" : " with the specified predicate"));
+ }
}
this.animationSelector.changeCurrentAnimation(trace.add(op));
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
--
GitLab