From 95b79dab7e72e85086c31ea16677505912dc78a1 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 14 May 2018 14:18:32 +0200
Subject: [PATCH] Improve description for EnumerationWarning results

---
 notebooks/tests/eval.ipynb                    | 27 ++++++++++---------
 .../java/de/prob2/jupyter/ProBKernel.java     |  2 +-
 2 files changed, 16 insertions(+), 13 deletions(-)

diff --git a/notebooks/tests/eval.ipynb b/notebooks/tests/eval.ipynb
index 6613a9c..882ac54 100644
--- a/notebooks/tests/eval.ipynb
+++ b/notebooks/tests/eval.ipynb
@@ -124,7 +124,7 @@
       "text/plain": [
        "TRUE\n",
        "\n",
-       "Solutions:\n",
+       "Solution:\n",
        "\txx = 3"
       ]
      },
@@ -147,7 +147,7 @@
       "text/plain": [
        "TRUE\n",
        "\n",
-       "Solutions:\n",
+       "Solution:\n",
        "\txx = 3\n",
        "\tyy = 4"
       ]
@@ -195,22 +195,16 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "[2018-05-11 12:12:54,581, T+4960] \"ProB Output Logger for instance 411341bd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] VIRTUAL TIME-OUT caused by: ### Warning: enumerating x : (all_solutions) : INTEGER : 2:sup ---> 2:3\u001b[0m\n"
+      "[2018-05-14 14:17:02,521, T+6108] \"ProB Output Logger for instance e93f3d5\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] VIRTUAL TIME-OUT caused by: ### Warning: enumerating x : (all_solutions) : INTEGER : 2:sup ---> 2:3\u001b[0m\n",
+      "[2018-05-14 14:17:02,524, T+6111] \"ProB Output Logger for instance e93f3d5\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** exiting multiple error blocks (2 -> 0) for catch_enumeration_warning_exceptions ***\u001b[0m\n"
      ]
     },
     {
      "ename": "UserErrorException",
-     "evalue": "Enumeration warning occurred",
+     "evalue": "UNKNOWN (FALSE with enumeration warning)",
      "output_type": "error",
      "traceback": [
-      "\u001b[1m\u001b[31mEnumeration warning occurred\u001b[0m"
-     ]
-    },
-    {
-     "name": "stdout",
-     "output_type": "stream",
-     "text": [
-      "[2018-05-11 12:12:54,584, T+4963] \"ProB Output Logger for instance 411341bd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** exiting multiple error blocks (2 -> 0) for catch_enumeration_warning_exceptions ***\u001b[0m\n"
+      "\u001b[1m\u001b[31mUNKNOWN (FALSE with enumeration warning)\u001b[0m"
      ]
     }
    ],
@@ -223,6 +217,15 @@
    "execution_count": 10,
    "metadata": {},
    "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "[2018-05-14 14:17:02,617, T+6204] \"ProB Output Logger for instance e93f3d5\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[31m\u001b[1m! A well-definedness error occured !\u001b[0m\n",
+      "[2018-05-14 14:17:02,618, T+6205] \"ProB Output Logger for instance e93f3d5\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! mod not defined for negative numbers: 2 mod-1\u001b[0m\n",
+      "[2018-05-14 14:17:02,619, T+6206] \"ProB Output Logger for instance e93f3d5\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Line: 1 Column: 0 until 8\u001b[0m\n"
+     ]
+    },
     {
      "ename": "UserErrorException",
      "evalue": "NOT-WELL-DEFINED: \nmod not defined for negative numbers: 2 mod-1\n ### Line: 1, Column: 0 until 8\n\n",
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 8a1d750..6b4fded 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -126,7 +126,7 @@ public final class ProBKernel extends BaseKernel {
 			sb.append(result.getReason());
 			error = true;
 		} else if (aer instanceof EnumerationWarning) {
-			sb.append("Enumeration warning occurred");
+			sb.append("UNKNOWN (FALSE with enumeration warning)");
 			error = true;
 		} else if (aer instanceof EvaluationErrorResult) {
 			final EvaluationErrorResult result = (EvaluationErrorResult)aer;
-- 
GitLab