Improve description for EnumerationWarning results

95b79dab · dgelessus · f654fd86 · 95b79dab · 95b79dab
Commit 95b79dab authored 7 years ago by dgelessus
--- 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"
+      "\u001b[1m\u001b[31mUNKNOWN (FALSE with enumeration warning)\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"
     ]
    }
   ],
@@ -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",

 %% Cell type:markdown id: tags:
 Expressions can be evaluated.
 %% Cell type:code id: tags:
 ``` prob
 123
 ```
 %% Output
    123
 %% Cell type:code id: tags:
 ``` prob
 123 + 456
 ```
 %% Output
    579
 %% Cell type:code id: tags:
 ``` prob
 {1, 2} \/ {5, 6}
 ```
 %% Output
    {1,2,5,6}
 %% Cell type:code id: tags:
 ``` prob
 1..5
 ```
 %% Output
    {1,2,3,4,5}
 %% Cell type:code id: tags:
 ``` prob
 MAXINT
 ```
 %% Output
    3
 %% Cell type:markdown id: tags:
 Solution variables are displayed.
 %% Cell type:code id: tags:
 ``` prob
 #xx.(xx : NAT1 & xx mod 3 = 0)
 ```
 %% Output
    TRUE
-    Solutions:
+    Solution:
    	xx = 3
 %% Cell type:code id: tags:
 ``` prob
 #xx, yy.(xx > 2 & yy < 5 & xx < yy)
 ```
 %% Output
    TRUE
-    Solutions:
+    Solution:
    	xx = 3
    	yy = 4
 %% Cell type:markdown id: tags:
 Various kinds of evaluation errors are displayed.
 %% Cell type:code id: tags:
 ``` prob
 unknown
 ```
 %% Output
    Computation not completed: Unknown identifier "unknown"
 %% Cell type:code id: tags:
 ``` prob
 card({x | x > 0 & x mod 2 = 0})
 ```
 %% Output
-    [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[0m
+    [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[0m
+    [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 ***[0m
-    Enumeration warning occurred
+    UNKNOWN (FALSE with enumeration warning)
-    [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 ***[0m
 %% Cell type:code id: tags:
 ``` prob
 2 mod -1
 ```
 %% Output
+    [2018-05-14 14:17:02,617, T+6204] "ProB Output Logger for instance e93f3d5" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] [31m[1m! A well-definedness error occured ![0m
+    [2018-05-14 14:17:02,618, T+6205] "ProB Output Logger for instance e93f3d5" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] [0m[31m[1m! mod not defined for negative numbers: 2 mod-1[0m
+    [2018-05-14 14:17:02,619, T+6206] "ProB Output Logger for instance e93f3d5" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] [0m[31m[1m! Line: 1 Column: 0 until 8[0m
    NOT-WELL-DEFINED:
    mod not defined for negative numbers: 2 mod-1
     ### Line: 1, Column: 0 until 8

--- 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;