From 43d027f21e97f7864529caa13e71bf93514bbd88 Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Wed, 6 Jun 2018 12:18:23 +0200 Subject: [PATCH] Rerun all notebooks --- notebooks/manual/ExternalFunctions.ipynb | 81 +---------- notebooks/models/scheduler.ipynb | 43 ------ notebooks/tests/animate.ipynb | 98 +------------ notebooks/tests/chr_tests.ipynb | 30 ++-- notebooks/tests/eval.ipynb | 31 +---- notebooks/tests/external_functions.ipynb | 37 +---- notebooks/tests/groovy.ipynb | 7 + notebooks/tests/help.ipynb | 130 +++++++++++++++++- notebooks/tests/load_cell.ipynb | 24 ---- notebooks/tests/load_file.ipynb | 24 ---- notebooks/tests/pref.ipynb | 8 ++ notebooks/tests/solve.ipynb | 98 ++----------- notebooks/tests/table.ipynb | 34 ----- notebooks/tests/time.ipynb | 8 +- notebooks/tests/version.ipynb | 11 +- .../Functional_Programming_in_B.ipynb | 46 +++---- notebooks/tutorials/prob_solver_intro.ipynb | 19 +-- 17 files changed, 219 insertions(+), 510 deletions(-) diff --git a/notebooks/manual/ExternalFunctions.ipynb b/notebooks/manual/ExternalFunctions.ipynb index 17f9e92..d2dd2ec 100644 --- a/notebooks/manual/ExternalFunctions.ipynb +++ b/notebooks/manual/ExternalFunctions.ipynb @@ -26,18 +26,6 @@ "execution_count": 1, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-16 13:20:12,877, T+5592] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n", - "[2018-05-16 13:20:14,476, T+7191] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57016\n", - "[2018-05-16 13:20:14,478, T+7193] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1950\n", - "[2018-05-16 13:20:14,481, T+7196] \"ProB Output Logger for instance 5406bd9a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-05-16 13:20:14,504, T+7219] \"ProB Output Logger for instance 5406bd9a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", - "[2018-05-16 13:20:14,685, T+7400] \"ProB Output Logger for instance 5406bd9a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 12:58:57.712),Jupyter_LibraryStrings,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/manual,/Users/david/.prob/prob2-3.2.10-SNAPSHOT/stdlib/LibraryStrings.def])\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -1307,18 +1295,6 @@ "execution_count": 54, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-16 13:20:18,426, T+11141] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n", - "[2018-05-16 13:20:19,769, T+12484] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57053\n", - "[2018-05-16 13:20:19,770, T+12485] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1954\n", - "[2018-05-16 13:20:19,772, T+12487] \"ProB Output Logger for instance 28964c5\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-05-16 13:20:19,796, T+12511] \"ProB Output Logger for instance 28964c5\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", - "[2018-05-16 13:20:19,946, T+12661] \"ProB Output Logger for instance 28964c5\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 12:58:57.712),Jupyter_CHOOSE,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/manual,/Users/david/.prob/prob2-3.2.10-SNAPSHOT/stdlib/CHOOSE.def])\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -1488,18 +1464,6 @@ "execution_count": 60, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-16 13:20:20,560, T+13275] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n", - "[2018-05-16 13:20:22,110, T+14825] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57070\n", - "[2018-05-16 13:20:22,111, T+14826] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1958\n", - "[2018-05-16 13:20:22,114, T+14829] \"ProB Output Logger for instance 1c63edfa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-05-16 13:20:22,137, T+14852] \"ProB Output Logger for instance 1c63edfa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", - "[2018-05-16 13:20:22,280, T+14995] \"ProB Output Logger for instance 1c63edfa\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 12:58:57.712),Jupyter_SORT,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/manual,/Users/david/.prob/prob2-3.2.10-SNAPSHOT/stdlib/SORT.def])\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -1626,18 +1590,6 @@ "execution_count": 65, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-16 13:20:22,869, T+15584] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n", - "[2018-05-16 13:20:24,234, T+16949] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57087\n", - "[2018-05-16 13:20:24,235, T+16950] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1962\n", - "[2018-05-16 13:20:24,237, T+16952] \"ProB Output Logger for instance 742efc90\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-05-16 13:20:24,255, T+16970] \"ProB Output Logger for instance 742efc90\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", - "[2018-05-16 13:20:24,405, T+17120] \"ProB Output Logger for instance 742efc90\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 12:58:57.712),Jupyter_LibraryMeta,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/manual,/Users/david/.prob/prob2-3.2.10-SNAPSHOT/stdlib/LibraryMeta.def])\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -1693,7 +1645,7 @@ { "data": { "text/plain": [ - "\"60150095a9bbe8cd7e75d9ef85686d632beb8840\"" + "\"c6264c505a07e8df7a9f0a7631c9d503c125bd8e\"" ] }, "execution_count": 67, @@ -1713,7 +1665,7 @@ { "data": { "text/plain": [ - "\"Wed May 16 07:45:07 2018 +0200\"" + "\"Tue Jun 5 12:14:24 2018 +0100\"" ] }, "execution_count": 68, @@ -1773,7 +1725,7 @@ { "data": { "text/plain": [ - "\"16/5/2018 - 13h20 25s\"" + "\"6/6/2018 - 11h59 26s\"" ] }, "execution_count": 71, @@ -1809,7 +1761,7 @@ { "data": { "text/plain": [ - "150571952" + "150612400" ] }, "execution_count": 72, @@ -1909,7 +1861,7 @@ { "data": { "text/plain": [ - "1526469625" + "1528279167" ] }, "execution_count": 77, @@ -1929,7 +1881,7 @@ { "data": { "text/plain": [ - "1600" + "1820" ] }, "execution_count": 78, @@ -1949,7 +1901,7 @@ { "data": { "text/plain": [ - "2600" + "2960" ] }, "execution_count": 79, @@ -2351,18 +2303,6 @@ "execution_count": 95, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-16 13:20:26,472, T+19187] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n", - "[2018-05-16 13:20:27,833, T+20548] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57112\n", - "[2018-05-16 13:20:27,834, T+20549] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1967\n", - "[2018-05-16 13:20:27,836, T+20551] \"ProB Output Logger for instance 136352e6\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-05-16 13:20:27,853, T+20568] \"ProB Output Logger for instance 136352e6\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", - "[2018-05-16 13:20:27,989, T+20704] \"ProB Output Logger for instance 136352e6\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 12:58:57.712),Jupyter_LibraryXML,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/manual,/Users/david/.prob/prob2-3.2.10-SNAPSHOT/stdlib/LibraryXML.def])\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -2395,13 +2335,6 @@ "execution_count": 96, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-16 13:20:28,298, T+21013] \"ProB Output Logger for instance 136352e6\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Walltime 20 ms to parse and convert XML\u001b[0m\n" - ] - }, { "data": { "text/plain": [ diff --git a/notebooks/models/scheduler.ipynb b/notebooks/models/scheduler.ipynb index 8223d42..6f23b2a 100644 --- a/notebooks/models/scheduler.ipynb +++ b/notebooks/models/scheduler.ipynb @@ -7,17 +7,6 @@ "scrolled": false }, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-06 08:57:28,567, T+7800] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/git_root/prob_prolog/probcli.sh\n", - "[2018-06-06 08:57:29,600, T+8833] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 53579\n", - "[2018-06-06 08:57:29,601, T+8834] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 65646\n", - "[2018-06-06 08:57:29,603, T+8836] \"ProB Output Logger for instance 56018fb8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-06-06 08:57:29,619, T+8852] \"ProB Output Logger for instance 56018fb8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -161,15 +150,6 @@ "execution_count": 8, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-06 08:57:52,255, T+31488] \"ProB Output Logger for instance 56018fb8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\n", - "[2018-06-06 08:57:52,256, T+31489] \"ProB Output Logger for instance 56018fb8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ALL OPERATIONS COVERED\u001b[0m\n", - "[2018-06-06 08:57:52,257, T+31490] \"ProB Output Logger for instance 56018fb8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -230,14 +210,6 @@ "execution_count": 11, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-06 08:58:13,114, T+52347] \"ProB Output Logger for instance 56018fb8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] finding_trace_from_to(root)\u001b[0m\n", - "[2018-06-06 08:58:13,119, T+52352] \"ProB Output Logger for instance 56018fb8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] .\u001b[0m\n" - ] - }, { "data": { "text/markdown": [ @@ -324,14 +296,6 @@ "execution_count": 15, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-06 09:14:55,680, T+1054913] \"ProB Output Logger for instance 56018fb8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] finding_trace_from_to(root)\u001b[0m\n", - "[2018-06-06 09:14:55,681, T+1054914] \"ProB Output Logger for instance 56018fb8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] .\u001b[0m\n" - ] - }, { "data": { "text/markdown": [ @@ -354,13 +318,6 @@ "source": [ ":table waiting" ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb index 8de4aae..a470eae 100644 --- a/notebooks/tests/animate.ipynb +++ b/notebooks/tests/animate.ipynb @@ -150,17 +150,6 @@ "execution_count": 6, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 12:13:17,947, T+13580] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n", - "[2018-06-04 12:13:19,470, T+15103] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 52560\n", - "[2018-06-04 12:13:19,472, T+15105] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1092\n", - "[2018-06-04 12:13:19,480, T+15113] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-06-04 12:13:19,507, T+15140] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -194,16 +183,6 @@ "execution_count": 7, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 12:13:20,152, T+15785] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 100 ms (walltime: 100 ms)\u001b[0m\n", - "[2018-06-04 12:13:20,153, T+15786] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)\u001b[0m\n", - "[2018-06-04 12:13:20,153, T+15786] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)\u001b[0m\n", - "[2018-06-04 12:13:20,154, T+15787] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -269,13 +248,6 @@ "execution_count": 10, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 12:13:20,510, T+16143] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime to FINALISE SETUP_CONSTANTS: 20 ms (walltime: 20 ms)\u001b[0m\n" - ] - }, { "ename": "CommandExecutionException", "evalue": ":constants: Could not setup constants with the specified predicate", @@ -294,13 +266,6 @@ "execution_count": 11, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 12:13:20,595, T+16228] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -388,40 +353,13 @@ "execution_count": 15, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 12:13:21,030, T+16663] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[31m\u001b[1m! An error occurred !\u001b[0m\n", - "[2018-06-04 12:13:21,031, T+16664] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! source(initialisation_fails)\u001b[0m\n", - "[2018-06-04 12:13:21,032, T+16665] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! INITIALISATION FAILS\u001b[0m\n", - "[2018-06-04 12:13:21,045, T+16678] \"Shell-0\" de.prob.animator.AnimatorImpl.getErrorItems(AnimatorImpl.java:105): [ERROR] ProB raised exception(s):\n", - "[2018-06-04 12:13:21,049, T+16682] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Line: 6 Column: 15 until 44 in file: /Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests\u001b[0m\n", - "[2018-06-04 12:13:21,047, T+16680] \"Shell-0\" de.prob.animator.AnimatorImpl.getErrorItems(AnimatorImpl.java:107): [ERROR] Error: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests:6:15 to 6:44)\n" - ] - }, { "ename": "ProBError", "evalue": "ProB reported Errors\nProB returned error messages:\nError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests:6:15 to 6:44)", "output_type": "error", "traceback": [ - "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m", - "\u001b[1m\u001b[31mde.prob.exception.ProBError: ProB reported Errors\u001b[0m", - "\u001b[1m\u001b[31mProB returned error messages:\u001b[0m", - "\u001b[1m\u001b[31mError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests:6:15 to 6:44)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob.animator.command.AbstractCommand.processErrorResult(AbstractCommand.java:137)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:81)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.execute(StateSpace.java:549)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:277)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob.statespace.State.findTransitions(State.java:153)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob.statespace.State.findTransition(State.java:136)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.InitialiseCommand.run(InitialiseCommand.java:44)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:98)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:113)\u001b[0m", - "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:307)\u001b[0m", - "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$0(ShellChannel.java:50)\u001b[0m", - "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m", - "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:39)\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:6:15 to 6:44)\u001b[0m" ] } ], @@ -434,15 +372,6 @@ "execution_count": 16, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 12:13:21,224, T+16857] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[0m\n", - "[2018-06-04 12:13:21,226, T+16859] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ALL OPERATIONS COVERED\u001b[0m\n", - "[2018-06-04 12:13:21,226, T+16859] \"ProB Output Logger for instance 27a0802c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -767,18 +696,6 @@ "execution_count": 31, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 12:13:22,299, T+17932] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n", - "[2018-06-04 12:13:23,889, T+19522] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 52592\n", - "[2018-06-04 12:13:23,890, T+19523] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1096\n", - "[2018-06-04 12:13:23,909, T+19542] \"ProB Output Logger for instance 2120e79e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-06-04 12:13:23,922, T+19555] \"ProB Output Logger for instance 2120e79e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", - "[2018-06-04 12:13:24,268, T+19901] \"ProB Output Logger for instance 2120e79e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % unused_constants(1,[x])\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -806,17 +723,6 @@ "execution_count": 32, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 12:13:24,473, T+20106] \"ProB Output Logger for instance 2120e79e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 80 ms (walltime: 90 ms)\u001b[0m\n", - "[2018-06-04 12:13:24,474, T+20107] \"ProB Output Logger for instance 2120e79e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)\u001b[0m\n", - "[2018-06-04 12:13:24,474, T+20107] \"ProB Output Logger for instance 2120e79e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)\u001b[0m\n", - "[2018-06-04 12:13:24,475, T+20108] \"ProB Output Logger for instance 2120e79e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)\u001b[0m\n", - "[2018-06-04 12:13:24,537, T+20170] \"ProB Output Logger for instance 2120e79e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 20 ms (walltime: 30 ms)\u001b[0m\n" - ] - }, { "data": { "text/plain": [ diff --git a/notebooks/tests/chr_tests.ipynb b/notebooks/tests/chr_tests.ipynb index 0421395..65f3abc 100644 --- a/notebooks/tests/chr_tests.ipynb +++ b/notebooks/tests/chr_tests.ipynb @@ -82,7 +82,7 @@ }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 5, "metadata": {}, "outputs": [ { @@ -91,7 +91,7 @@ "Preference changed: CHR = FALSE\n" ] }, - "execution_count": 6, + "execution_count": 5, "metadata": {}, "output_type": "execute_result" } @@ -102,35 +102,23 @@ }, { "cell_type": "code", - "execution_count": 7, - "metadata": {}, + "execution_count": 6, + "metadata": { + "scrolled": true + }, "outputs": [ { - "ename": "UserErrorException", - "evalue": "Enumeration warning occurred", + "ename": "CommandExecutionException", + "evalue": ":eval: 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 18:43:12,008, T+9454167] \"ProB Output Logger for instance 127e70c5\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Timeout when posting constraint:\u001b[0m\n" + "\u001b[1m\u001b[31m:eval: UNKNOWN (FALSE with enumeration warning)\u001b[0m" ] } ], "source": [ "x>y & y>x" ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { diff --git a/notebooks/tests/eval.ipynb b/notebooks/tests/eval.ipynb index 186403a..630157d 100644 --- a/notebooks/tests/eval.ipynb +++ b/notebooks/tests/eval.ipynb @@ -7,6 +7,13 @@ "outputs": [ { "data": { + "text/markdown": [ + "```\n", + ":eval EXPRESSION\n", + "```\n", + "\n", + "Evaluate an expression." + ], "text/plain": [ ":eval EXPRESSION\n", "\n", @@ -141,13 +148,6 @@ "execution_count": 7, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-28 14:55:02,886, T+6383] \"ProB Output Logger for instance 4d6ccc97\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Rewrite NAT1 to: 1 .. MAXINT\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -220,14 +220,6 @@ "execution_count": 10, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-28 14:55:03,150, T+6647] \"ProB Output Logger for instance 4d6ccc97\" 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-28 14:55:03,151, T+6648] \"ProB Output Logger for instance 4d6ccc97\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** exiting multiple error blocks (2 -> 0) for catch_enumeration_warning_exceptions ***\u001b[0m\n" - ] - }, { "ename": "CommandExecutionException", "evalue": ":eval: UNKNOWN (FALSE with enumeration warning)", @@ -246,15 +238,6 @@ "execution_count": 11, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-28 14:55:03,236, T+6733] \"ProB Output Logger for instance 4d6ccc97\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[31m\u001b[1m! A well-definedness error occured !\u001b[0m\n", - "[2018-05-28 14:55:03,237, T+6734] \"ProB Output Logger for instance 4d6ccc97\" 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-28 14:55:03,238, T+6735] \"ProB Output Logger for instance 4d6ccc97\" 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": "CommandExecutionException", "evalue": ":eval: NOT-WELL-DEFINED: \nmod not defined for negative numbers: 2 mod-1\n ### Line: 1, Column: 0 until 8\n\n", diff --git a/notebooks/tests/external_functions.ipynb b/notebooks/tests/external_functions.ipynb index 00ed34a..f2b1c01 100644 --- a/notebooks/tests/external_functions.ipynb +++ b/notebooks/tests/external_functions.ipynb @@ -5,18 +5,6 @@ "execution_count": 1, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-16 13:05:41,328, T+7460] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n", - "[2018-05-16 13:05:42,778, T+8910] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 50359\n", - "[2018-05-16 13:05:42,779, T+8911] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1835\n", - "[2018-05-16 13:05:42,783, T+8915] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-05-16 13:05:42,801, T+8933] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", - "[2018-05-16 13:05:42,973, T+9105] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 12:58:57.712),Jupyter,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests,/Users/david/.prob/prob2-3.2.10-SNAPSHOT/stdlib/LibraryMeta.def,/Users/david/.prob/prob2-3.2.10-SNAPSHOT/stdlib/LibraryStrings.def])\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -83,7 +71,7 @@ { "data": { "text/plain": [ - "\"60150095a9bbe8cd7e75d9ef85686d632beb8840\"" + "\"c6264c505a07e8df7a9f0a7631c9d503c125bd8e\"" ] }, "execution_count": 4, @@ -123,7 +111,7 @@ { "data": { "text/plain": [ - "150586816" + "150627280" ] }, "execution_count": 6, @@ -148,26 +136,11 @@ "metadata": {}, "outputs": [ { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-16 13:06:07,175, T+33307] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[31m\u001b[1m! An error occurred !\u001b[0m\n", - "[2018-05-16 13:06:07,176, T+33308] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! source(parsercall)\u001b[0m\n", - "[2018-05-16 13:06:07,176, T+33308] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Unexpected error while parsing machine: \u001b[0m\n", - "[2018-05-16 13:06:07,177, T+33309] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! An error occurred !\u001b[0m\n", - "[2018-05-16 13:06:07,177, T+33309] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! source(parsercall)\u001b[0m\n", - "[2018-05-16 13:06:07,178, T+33310] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Additional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\u001b[0m\n", - "[2018-05-16 13:06:07,179, T+33311] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! An error occurred !\u001b[0m\n", - "[2018-05-16 13:06:07,179, T+33311] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! source(internal_error(parsercall))\u001b[0m\n", - "[2018-05-16 13:06:07,180, T+33312] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Java B parser (probcliparser.jar) is missing from lib directory in: /Users/david/.prob/prob2-3.2.10-SNAPSHOT/\u001b[0m\n" - ] - }, - { - "ename": "UserErrorException", - "evalue": "NOT-WELL-DEFINED: \nUnexpected error while parsing machine: \n\n\nAdditional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\n\n\nJava B parser (probcliparser.jar) is missing from lib directory in: /Users/david/.prob/prob2-3.2.10-SNAPSHOT/\n\n", + "ename": "CommandExecutionException", + "evalue": ":eval: NOT-WELL-DEFINED: \nUnexpected error while parsing machine: \n\n\nAdditional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\n\n\nJava B parser (probcliparser.jar) is missing from lib directory in: /Users/david/.prob/prob2-3.2.10-SNAPSHOT/\n\n", "output_type": "error", "traceback": [ - "\u001b[1m\u001b[31mNOT-WELL-DEFINED: \u001b[0m", + "\u001b[1m\u001b[31m:eval: NOT-WELL-DEFINED: \u001b[0m", "\u001b[1m\u001b[31mUnexpected error while parsing machine: \u001b[0m", "\u001b[1m\u001b[31m\u001b[0m", "\u001b[1m\u001b[31m\u001b[0m", diff --git a/notebooks/tests/groovy.ipynb b/notebooks/tests/groovy.ipynb index 00426ea..0943f9d 100644 --- a/notebooks/tests/groovy.ipynb +++ b/notebooks/tests/groovy.ipynb @@ -7,6 +7,13 @@ "outputs": [ { "data": { + "text/markdown": [ + "```\n", + ":groovy EXPRESSION\n", + "```\n", + "\n", + "Evaluate the given Groovy expression." + ], "text/plain": [ ":groovy EXPRESSION\n", "\n", diff --git a/notebooks/tests/help.ipynb b/notebooks/tests/help.ipynb index a921ecd..60ae957 100644 --- a/notebooks/tests/help.ipynb +++ b/notebooks/tests/help.ipynb @@ -14,13 +14,48 @@ "outputs": [ { "data": { + "text/markdown": [ + "Type a valid B expression, or one of the following commands:\n", + "\n", + "* `::load` Load the machine source code from the body.\n", + "* `::render` Render some content with the specified MIME type.\n", + "* `:?` Display help for a specific command, or general help about the REPL.\n", + "* `:browse` Show information about the current state\n", + "* `:constants` Set up the current machine's constants with the specified predicate\n", + "* `:eval` Evaluate an expression.\n", + "* `:exec` Execute an operation with the specified predicate, or by its ID\n", + "* `:groovy` Evaluate the given Groovy expression.\n", + "* `:help` Display help for a specific command, or general help about the REPL.\n", + "* `:init` Initialise the current machine with the specified predicate\n", + "* `:initialise` Initialise the current machine with the specified predicate\n", + "* `:load` Load the machine from the given path.\n", + "* `:pref` View or change the value of one or more preferences.\n", + "* `:prettyprint` Pretty-print a predicate.\n", + "* `:solve` Solve a predicate with the specified solver\n", + "* `:table` Display an expression as a table.\n", + "* `:time` Execute the given command and measure how long it takes to execute.\n", + "* `:version` Display version info about the ProB CLI and ProB 2\n" + ], "text/plain": [ "Type a valid B expression, or one of the following commands:\n", "::load Load the machine source code from the body.\n", + "::render Render some content with the specified MIME type.\n", ":? Display help for a specific command, or general help about the REPL.\n", + ":browse Show information about the current state\n", + ":constants Set up the current machine's constants with the specified predicate\n", + ":eval Evaluate an expression.\n", + ":exec Execute an operation with the specified predicate, or by its ID\n", + ":groovy Evaluate the given Groovy expression.\n", ":help Display help for a specific command, or general help about the REPL.\n", + ":init Initialise the current machine with the specified predicate\n", + ":initialise Initialise the current machine with the specified predicate\n", ":load Load the machine from the given path.\n", - ":pref View or change the value of one or more preferences.\n" + ":pref View or change the value of one or more preferences.\n", + ":prettyprint Pretty-print a predicate.\n", + ":solve Solve a predicate with the specified solver\n", + ":table Display an expression as a table.\n", + ":time Execute the given command and measure how long it takes to execute.\n", + ":version Display version info about the ProB CLI and ProB 2\n" ] }, "execution_count": 1, @@ -39,13 +74,48 @@ "outputs": [ { "data": { + "text/markdown": [ + "Type a valid B expression, or one of the following commands:\n", + "\n", + "* `::load` Load the machine source code from the body.\n", + "* `::render` Render some content with the specified MIME type.\n", + "* `:?` Display help for a specific command, or general help about the REPL.\n", + "* `:browse` Show information about the current state\n", + "* `:constants` Set up the current machine's constants with the specified predicate\n", + "* `:eval` Evaluate an expression.\n", + "* `:exec` Execute an operation with the specified predicate, or by its ID\n", + "* `:groovy` Evaluate the given Groovy expression.\n", + "* `:help` Display help for a specific command, or general help about the REPL.\n", + "* `:init` Initialise the current machine with the specified predicate\n", + "* `:initialise` Initialise the current machine with the specified predicate\n", + "* `:load` Load the machine from the given path.\n", + "* `:pref` View or change the value of one or more preferences.\n", + "* `:prettyprint` Pretty-print a predicate.\n", + "* `:solve` Solve a predicate with the specified solver\n", + "* `:table` Display an expression as a table.\n", + "* `:time` Execute the given command and measure how long it takes to execute.\n", + "* `:version` Display version info about the ProB CLI and ProB 2\n" + ], "text/plain": [ "Type a valid B expression, or one of the following commands:\n", "::load Load the machine source code from the body.\n", + "::render Render some content with the specified MIME type.\n", ":? Display help for a specific command, or general help about the REPL.\n", + ":browse Show information about the current state\n", + ":constants Set up the current machine's constants with the specified predicate\n", + ":eval Evaluate an expression.\n", + ":exec Execute an operation with the specified predicate, or by its ID\n", + ":groovy Evaluate the given Groovy expression.\n", ":help Display help for a specific command, or general help about the REPL.\n", + ":init Initialise the current machine with the specified predicate\n", + ":initialise Initialise the current machine with the specified predicate\n", ":load Load the machine from the given path.\n", - ":pref View or change the value of one or more preferences.\n" + ":pref View or change the value of one or more preferences.\n", + ":prettyprint Pretty-print a predicate.\n", + ":solve Solve a predicate with the specified solver\n", + ":table Display an expression as a table.\n", + ":time Execute the given command and measure how long it takes to execute.\n", + ":version Display version info about the ProB CLI and ProB 2\n" ] }, "execution_count": 2, @@ -64,6 +134,14 @@ "outputs": [ { "data": { + "text/markdown": [ + "```\n", + ":? [COMMAND]\n", + ":help [COMMAND]\n", + "```\n", + "\n", + "Display help for a specific command, or general help about the REPL." + ], "text/plain": [ ":? [COMMAND]\n", ":help [COMMAND]\n", @@ -87,6 +165,14 @@ "outputs": [ { "data": { + "text/markdown": [ + "```\n", + ":? [COMMAND]\n", + ":help [COMMAND]\n", + "```\n", + "\n", + "Display help for a specific command, or general help about the REPL." + ], "text/plain": [ ":? [COMMAND]\n", ":help [COMMAND]\n", @@ -110,6 +196,13 @@ "outputs": [ { "data": { + "text/markdown": [ + "```\n", + ":load FILENAME [PREF=VALUE ...]\n", + "```\n", + "\n", + "Load the machine from the given path." + ], "text/plain": [ ":load FILENAME [PREF=VALUE ...]\n", "\n", @@ -132,6 +225,16 @@ "outputs": [ { "data": { + "text/markdown": [ + "```\n", + "::load [PREF=VALUE ...]\n", + "MACHINE\n", + "...\n", + "END\n", + "```\n", + "\n", + "Load the machine source code from the body." + ], "text/plain": [ "::load [PREF=VALUE ...]\n", "MACHINE\n", @@ -164,6 +267,14 @@ "outputs": [ { "data": { + "text/markdown": [ + "```\n", + ":? [COMMAND]\n", + ":help [COMMAND]\n", + "```\n", + "\n", + "Display help for a specific command, or general help about the REPL." + ], "text/plain": [ ":? [COMMAND]\n", ":help [COMMAND]\n", @@ -187,6 +298,14 @@ "outputs": [ { "data": { + "text/markdown": [ + "```\n", + ":? [COMMAND]\n", + ":help [COMMAND]\n", + "```\n", + "\n", + "Display help for a specific command, or general help about the REPL." + ], "text/plain": [ ":? [COMMAND]\n", ":help [COMMAND]\n", @@ -210,6 +329,13 @@ "outputs": [ { "data": { + "text/markdown": [ + "```\n", + ":load FILENAME [PREF=VALUE ...]\n", + "```\n", + "\n", + "Load the machine from the given path." + ], "text/plain": [ ":load FILENAME [PREF=VALUE ...]\n", "\n", diff --git a/notebooks/tests/load_cell.ipynb b/notebooks/tests/load_cell.ipynb index 0578cc3..ed36c15 100644 --- a/notebooks/tests/load_cell.ipynb +++ b/notebooks/tests/load_cell.ipynb @@ -12,18 +12,6 @@ "execution_count": 1, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-10 19:11:33,924, T+6623] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n", - "[2018-05-10 19:11:36,660, T+9359] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54371\n", - "[2018-05-10 19:11:36,661, T+9360] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 2398\n", - "[2018-05-10 19:11:36,664, T+9363] \"ProB Output Logger for instance 4540b804\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-05-10 19:11:36,691, T+9390] \"ProB Output Logger for instance 4540b804\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", - "[2018-05-10 19:11:36,829, T+9528] \"ProB Output Logger for instance 4540b804\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),things,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests])\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -74,18 +62,6 @@ "execution_count": 3, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-10 19:11:37,170, T+9869] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n", - "[2018-05-10 19:11:39,169, T+11868] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54475\n", - "[2018-05-10 19:11:39,171, T+11870] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 2406\n", - "[2018-05-10 19:11:39,178, T+11877] \"ProB Output Logger for instance 4905453a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-05-10 19:11:39,229, T+11928] \"ProB Output Logger for instance 4905453a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", - "[2018-05-10 19:11:39,370, T+12069] \"ProB Output Logger for instance 4905453a\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),prefs,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests])\u001b[0m\n" - ] - }, { "data": { "text/plain": [ diff --git a/notebooks/tests/load_file.ipynb b/notebooks/tests/load_file.ipynb index e23f4ca..d4c6d42 100644 --- a/notebooks/tests/load_file.ipynb +++ b/notebooks/tests/load_file.ipynb @@ -12,18 +12,6 @@ "execution_count": 1, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-14 10:45:48,930, T+45662] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n", - "[2018-05-14 10:45:50,431, T+47163] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 51537\n", - "[2018-05-14 10:45:50,432, T+47164] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 878\n", - "[2018-05-14 10:45:50,436, T+47168] \"ProB Output Logger for instance cda6f00\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-05-14 10:45:50,460, T+47192] \"ProB Output Logger for instance cda6f00\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", - "[2018-05-14 10:45:50,604, T+47336] \"ProB Output Logger for instance cda6f00\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),things,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/things.mch])\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -71,18 +59,6 @@ "execution_count": 3, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-14 10:46:02,661, T+59393] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n", - "[2018-05-14 10:46:04,150, T+60882] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 51630\n", - "[2018-05-14 10:46:04,152, T+60884] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 882\n", - "[2018-05-14 10:46:04,154, T+60886] \"ProB Output Logger for instance 4d195f75\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-05-14 10:46:04,188, T+60920] \"ProB Output Logger for instance 4d195f75\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n", - "[2018-05-14 10:46:04,315, T+61047] \"ProB Output Logger for instance 4d195f75\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),things,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/things.mch])\u001b[0m\n" - ] - }, { "data": { "text/plain": [ diff --git a/notebooks/tests/pref.ipynb b/notebooks/tests/pref.ipynb index 4f3bf97..0b3818f 100644 --- a/notebooks/tests/pref.ipynb +++ b/notebooks/tests/pref.ipynb @@ -7,6 +7,14 @@ "outputs": [ { "data": { + "text/markdown": [ + "```\n", + ":pref [NAME ...]\n", + ":pref NAME=VALUE [NAME=VALUE ...]\n", + "```\n", + "\n", + "View or change the value of one or more preferences." + ], "text/plain": [ ":pref [NAME ...]\n", ":pref NAME=VALUE [NAME=VALUE ...]\n", diff --git a/notebooks/tests/solve.ipynb b/notebooks/tests/solve.ipynb index dfe63d9..54d96d6 100644 --- a/notebooks/tests/solve.ipynb +++ b/notebooks/tests/solve.ipynb @@ -7,6 +7,13 @@ "outputs": [ { "data": { + "text/markdown": [ + "```\n", + ":solve SOLVER PREDICATE\n", + "```\n", + "\n", + "Solve a predicate with the specified solver" + ], "text/plain": [ ":solve SOLVER PREDICATE\n", "\n", @@ -58,15 +65,6 @@ "execution_count": 3, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-28 12:47:47,491, T+10065] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: xx > 2 & yy < 5 & xx < yy ints: irange(2,5), intatoms: none\u001b[0m\n", - "[2018-05-28 12:47:47,494, T+10068] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n", - "[2018-05-28 12:47:47,495, T+10069] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [3]\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -88,48 +86,9 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": null, "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-28 12:47:47,576, T+10150] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** LOADING Z3 library failed\u001b[0m\n", - "[2018-05-28 12:47:47,577, T+10151] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** error(system_error,system_error(dlopen(\"/Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle\") failed in load_foreign_resource/1: dlopen(/Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle, 2): Library not loaded: libz3.dylib\u001b[0m\n", - "[2018-05-28 12:47:47,577, T+10151] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Referenced from: /Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle\u001b[0m\n", - "[2018-05-28 12:47:47,578, T+10152] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Reason: image not found))\u001b[0m\n", - "[2018-05-28 12:47:47,579, T+10153] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[31m\u001b[1m! An error occurred !\u001b[0m\n", - "[2018-05-28 12:47:47,580, T+10154] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! source(internal_error(smt_solvers_interface))\u001b[0m\n", - "[2018-05-28 12:47:47,580, T+10154] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Call for event start_solving failed. init_interface(z3)\u001b[0m\n", - "[2018-05-28 12:47:47,588, T+10162] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0mexception(make_call/3, error(existence_error(procedure,z3interface:pop_frame/0),existence_error($@(z3interface:pop_frame,4462428732),0,procedure,z3interface:pop_frame/0,0))).\u001b[0m\n", - "[2018-05-28 12:47:47,591, T+10165] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** LOADING Z3 library failed\u001b[0m\n", - "[2018-05-28 12:47:47,592, T+10166] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** error(system_error,system_error(dlopen(\"/Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle\") failed in load_foreign_resource/1: dlopen(/Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle, 2): Library not loaded: libz3.dylib\u001b[0m\n", - "[2018-05-28 12:47:47,593, T+10167] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Referenced from: /Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle\u001b[0m\n", - "[2018-05-28 12:47:47,594, T+10168] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Reason: image not found))\u001b[0m\n" - ] - }, - { - "ename": "ProBError", - "evalue": "(error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4462428732),0,procedure,:(z3interface,/(pop_frame,0)),0)))", - "output_type": "error", - "traceback": [ - "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m", - "\u001b[1m\u001b[31mde.prob.exception.ProBError: (error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4462428732),0,procedure,:(z3interface,/(pop_frame,0)),0)))\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob.animator.CommandProcessor.extractResult(CommandProcessor.java:70)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob.animator.CommandProcessor.sendCommand(CommandProcessor.java:51)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:68)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.execute(StateSpace.java:549)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.SolveCommand.run(SolveCommand.java:70)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeLineCommand(ProBKernel.java:118)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:142)\u001b[0m", - "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:282)\u001b[0m", - "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$0(ShellChannel.java:50)\u001b[0m", - "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m", - "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:39)\u001b[0m" - ] - } - ], + "outputs": [], "source": [ ":solve smt_supported_interpreter xx > 2 & yy < 5 & xx < yy" ] @@ -139,37 +98,13 @@ "execution_count": 5, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-28 12:47:47,745, T+10319] \"Shell-0\" de.prob.animator.AnimatorImpl.getErrorItems(AnimatorImpl.java:105): [ERROR] ProB raised exception(s):\n", - "[2018-05-28 12:47:47,746, T+10320] \"Shell-0\" de.prob.animator.AnimatorImpl.getErrorItems(AnimatorImpl.java:107): [ERROR] Internal error: Call for event start_solving failed. init_interface(z3)\n", - "[2018-05-28 12:47:47,748, T+10322] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** LOADING Z3 library failed\u001b[0m\n", - "[2018-05-28 12:47:47,751, T+10325] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** error(system_error,system_error(dlopen(\"/Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle\") failed in load_foreign_resource/1: dlopen(/Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle, 2): Library not loaded: libz3.dylib\u001b[0m\n", - "[2018-05-28 12:47:47,752, T+10326] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Referenced from: /Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle\u001b[0m\n", - "[2018-05-28 12:47:47,753, T+10327] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Reason: image not found))\u001b[0m\n" - ] - }, { "ename": "ProBError", "evalue": "ProB reported Errors\nProB returned error messages:\nInternal error: Call for event start_solving failed. init_interface(z3)", "output_type": "error", "traceback": [ - "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m", - "\u001b[1m\u001b[31mde.prob.exception.ProBError: ProB reported Errors\u001b[0m", - "\u001b[1m\u001b[31mProB returned error messages:\u001b[0m", - "\u001b[1m\u001b[31mInternal error: Call for event start_solving failed. init_interface(z3)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob.animator.command.AbstractCommand.processErrorResult(AbstractCommand.java:137)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:81)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.execute(StateSpace.java:549)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.SolveCommand.run(SolveCommand.java:70)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeLineCommand(ProBKernel.java:118)\u001b[0m", - "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:142)\u001b[0m", - "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:282)\u001b[0m", - "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$0(ShellChannel.java:50)\u001b[0m", - "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m", - "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:39)\u001b[0m" + "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m", + "\u001b[1m\u001b[31mInternal error: Call for event start_solving failed. init_interface(z3)\u001b[0m" ] } ], @@ -189,17 +124,6 @@ "execution_count": 6, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-05-28 12:47:47,872, T+10446] \"Shell-0\" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh\n", - "[2018-05-28 12:47:49,327, T+11901] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 49601\n", - "[2018-05-28 12:47:49,328, T+11902] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 982\n", - "[2018-05-28 12:47:49,342, T+11916] \"ProB Output Logger for instance 6ee25e74\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n", - "[2018-05-28 12:47:49,384, T+11958] \"ProB Output Logger for instance 6ee25e74\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n" - ] - }, { "data": { "text/plain": [ diff --git a/notebooks/tests/table.ipynb b/notebooks/tests/table.ipynb index 8ae8fb8..7ee5fda 100644 --- a/notebooks/tests/table.ipynb +++ b/notebooks/tests/table.ipynb @@ -54,16 +54,6 @@ "execution_count": 3, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:38:09,730, T+6763] \"ProB Output Logger for instance 37c36608\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] finding_trace_from_to(root)\u001b[0m\n", - "[2018-06-04 14:38:09,734, T+6767] \"ProB Output Logger for instance 37c36608\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\n", - "[2018-06-04 14:38:09,843, T+6876] \"ProB Output Logger for instance 37c36608\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] call_command(table,expr_as_table,_85889,[set_extension(pos(2,-1,1,1,1,13),[integer(pos(3,-1,1,2,1,3),1),integer(pos(4,-1,1,5,1,6),2),integer(pos(5,-1,1,8,1,9),3),integer(pos(6,-1,1,11,1,12),4)]),_84193],[])\u001b[0m\n", - "[2018-06-04 14:38:09,844, T+6877] \"ProB Output Logger for instance 37c36608\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] result(list([list([Nr,Elements]),list([1,1]),list([2,2]),list([3,3]),list([4,4])]))\u001b[0m\n" - ] - }, { "data": { "text/markdown": [ @@ -96,14 +86,6 @@ "execution_count": 4, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:38:09,968, T+7001] \"ProB Output Logger for instance 37c36608\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] call_command(table,expr_as_table,_98723,[sequence_extension(pos(2,-1,1,1,1,13),[integer(pos(3,-1,1,2,1,3),1),integer(pos(4,-1,1,5,1,6),2),integer(pos(5,-1,1,8,1,9),3),integer(pos(6,-1,1,11,1,12),4)]),_97041],[])\u001b[0m\n", - "[2018-06-04 14:38:09,970, T+7003] \"ProB Output Logger for instance 37c36608\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] result(list([list([Nr,prj1,prj2]),list([1,1,1]),list([2,2,2]),list([3,3,3]),list([4,4,4])]))\u001b[0m\n" - ] - }, { "data": { "text/markdown": [ @@ -136,14 +118,6 @@ "execution_count": 5, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:38:10,074, T+7107] \"ProB Output Logger for instance 37c36608\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] call_command(table,expr_as_table,_116255,[set_extension(pos(2,-1,1,1,1,34),[couple(pos(3,-1,1,2,1,11),[integer(pos(4,-1,1,3,1,4),1),integer(pos(5,-1,1,6,1,7),2),integer(pos(6,-1,1,9,1,10),3)]),couple(pos(7,-1,1,13,1,22),[integer(pos(8,-1,1,14,1,15),4),integer(pos(9,-1,1,17,1,18),5),integer(pos(10,-1,1,20,1,21),6)]),couple(pos(11,-1,1,24,1,33),[integer(pos(12,-1,1,25,1,26),7),integer(pos(13,-1,1,28,1,29),8),integer(pos(14,-1,1,31,1,32),9)])]),_112973],[])\u001b[0m\n", - "[2018-06-04 14:38:10,075, T+7108] \"ProB Output Logger for instance 37c36608\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] result(list([list([Nr,prj11,prj12,prj2]),list([1,1,2,3]),list([2,4,5,6]),list([3,7,8,9])]))\u001b[0m\n" - ] - }, { "data": { "text/markdown": [ @@ -174,14 +148,6 @@ "execution_count": 6, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-04 14:38:10,310, T+7343] \"ProB Output Logger for instance 37c36608\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] call_command(table,expr_as_table,_129729,[set_extension(pos(2,-1,1,1,1,11),[couple(pos(3,-1,1,2,1,10),[empty_set(pos(4,-1,1,3,1,5)),empty_set(pos(5,-1,1,7,1,9))])]),_128283],[])\u001b[0m\n", - "[2018-06-04 14:38:10,312, T+7345] \"ProB Output Logger for instance 37c36608\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] result(list([list([Nr,prj1,prj2]),list([1,{},{}])]))\u001b[0m\n" - ] - }, { "data": { "text/markdown": [ diff --git a/notebooks/tests/time.ipynb b/notebooks/tests/time.ipynb index 1ddfa7d..deaa13a 100644 --- a/notebooks/tests/time.ipynb +++ b/notebooks/tests/time.ipynb @@ -44,10 +44,10 @@ { "data": { "text/markdown": [ - "Execution time: 1.046329981 seconds" + "Execution time: 1.037496364 seconds" ], "text/plain": [ - "Execution time: 1.046329981 seconds" + "Execution time: 1.037496364 seconds" ] }, "metadata": {}, @@ -83,10 +83,10 @@ { "data": { "text/markdown": [ - "Execution time: 1.079991277 seconds" + "Execution time: 1.074667161 seconds" ], "text/plain": [ - "Execution time: 1.079991277 seconds" + "Execution time: 1.074667161 seconds" ] }, "metadata": {}, diff --git a/notebooks/tests/version.ipynb b/notebooks/tests/version.ipynb index 5d879b6..29683b1 100644 --- a/notebooks/tests/version.ipynb +++ b/notebooks/tests/version.ipynb @@ -7,6 +7,13 @@ "outputs": [ { "data": { + "text/markdown": [ + "```\n", + ":version\n", + "```\n", + "\n", + "Display version info about the ProB CLI and ProB 2" + ], "text/plain": [ ":version\n", "\n", @@ -30,8 +37,8 @@ { "data": { "text/plain": [ - "ProB CLI: 1.8.1-beta4 (96831f0a148fe73b4a5d86278d07c91c4131a9cd)\n", - "ProB 2: 3.2.10-SNAPSHOT (92eeabb16aad9af19f0c175f6f29ee9fe0478e9e)" + "ProB CLI: 1.8.1-beta4 (c6264c505a07e8df7a9f0a7631c9d503c125bd8e)\n", + "ProB 2: 3.2.10-SNAPSHOT (8108b7526c431b4d51d23676edf00973f0ec1c96)" ] }, "execution_count": 2, diff --git a/notebooks/tutorials/Functional_Programming_in_B.ipynb b/notebooks/tutorials/Functional_Programming_in_B.ipynb index 9d48341..c225131 100644 --- a/notebooks/tutorials/Functional_Programming_in_B.ipynb +++ b/notebooks/tutorials/Functional_Programming_in_B.ipynb @@ -17,7 +17,7 @@ }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 1, "metadata": {}, "outputs": [ { @@ -31,7 +31,7 @@ "\tr1 = 10000000000" ] }, - "execution_count": 6, + "execution_count": 1, "metadata": {}, "output_type": "execute_result" } @@ -51,7 +51,7 @@ }, { "cell_type": "code", - "execution_count": 7, + "execution_count": 2, "metadata": {}, "outputs": [ { @@ -64,7 +64,7 @@ "\tf = λx·(x ∈ INTEGER∣x ∗ x)" ] }, - "execution_count": 7, + "execution_count": 2, "metadata": {}, "output_type": "execute_result" } @@ -83,7 +83,7 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 3, "metadata": {}, "outputs": [ { @@ -96,7 +96,7 @@ "\tf = λx·(x ∈ INTEGER∣x ∗ x)" ] }, - "execution_count": 8, + "execution_count": 3, "metadata": {}, "output_type": "execute_result" } @@ -115,7 +115,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 4, "metadata": {}, "outputs": [ { @@ -128,7 +128,7 @@ "\tf = λx·(x ∈ INTEGER∣x ∗ x)" ] }, - "execution_count": 9, + "execution_count": 4, "metadata": {}, "output_type": "execute_result" } @@ -147,16 +147,9 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 5, "metadata": {}, "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "[2018-06-06 09:48:30,643, T+626136] \"ProB Output Logger for instance 23eee4b8\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] VIRTUAL TIME-OUT caused by: ### Warning: enumerating NATURAL(1) : NATURAL(1) : 1:sup ---> 1:3\u001b[0m\n" - ] - }, { "data": { "text/plain": [ @@ -167,7 +160,7 @@ "\tr1 = 317" ] }, - "execution_count": 10, + "execution_count": 5, "metadata": {}, "output_type": "execute_result" } @@ -186,7 +179,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 6, "metadata": {}, "outputs": [ { @@ -203,7 +196,7 @@ "\tr1 = 317" ] }, - "execution_count": 13, + "execution_count": 6, "metadata": {}, "output_type": "execute_result" } @@ -226,7 +219,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 7, "metadata": {}, "outputs": [ { @@ -239,7 +232,7 @@ "\tf = {x,y∣x ∈ NATURAL ∧ y × 2 ≥ x ∧ (y − 1) × 2 < x}" ] }, - "execution_count": 12, + "execution_count": 7, "metadata": {}, "output_type": "execute_result" } @@ -258,7 +251,7 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 8, "metadata": {}, "outputs": [ { @@ -303,7 +296,7 @@ "16\t16\t4\n" ] }, - "execution_count": 5, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } @@ -311,13 +304,6 @@ "source": [ ":table {x,isqrt|x:1..16 & isqrt**2 >= x & (isqrt-1)**2 <x }" ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { diff --git a/notebooks/tutorials/prob_solver_intro.ipynb b/notebooks/tutorials/prob_solver_intro.ipynb index 7752c94..59d5ab5 100644 --- a/notebooks/tutorials/prob_solver_intro.ipynb +++ b/notebooks/tutorials/prob_solver_intro.ipynb @@ -13,7 +13,7 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 1, "metadata": {}, "outputs": [ { @@ -22,7 +22,7 @@ "1024" ] }, - "execution_count": 2, + "execution_count": 1, "metadata": {}, "output_type": "execute_result" } @@ -599,7 +599,7 @@ }, { "cell_type": "code", - "execution_count": 1, + "execution_count": 17, "metadata": {}, "outputs": [ { @@ -613,7 +613,7 @@ "\tn = 7" ] }, - "execution_count": 1, + "execution_count": 17, "metadata": {}, "output_type": "execute_result" } @@ -634,7 +634,7 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 18, "metadata": {}, "outputs": [ { @@ -656,7 +656,7 @@ "\tN = {\"a\",\"b\",\"c\"}" ] }, - "execution_count": 5, + "execution_count": 18, "metadata": {}, "output_type": "execute_result" } @@ -671,13 +671,6 @@ "iso: V >->> N & !v.(v:V => iso[g1[{v}]] = g2[iso[{v}]])\n", "END" ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { -- GitLab