diff --git a/.gitignore b/.gitignore
index 71c6a896992d914b21bb96b7588241447dee1d73..8af56ece42da5f0a4ce67594d11b3143f8e6c01c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,9 @@
# Generated
/kernelspec/prob2/kernel.json
+
+# Python virtual environment
+/env/
+
+# Jupyter notebook checkpoints
+.ipynb_checkpoints/
diff --git a/notebooks/tests/eval.ipynb b/notebooks/tests/eval.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..44381439659aaddc67677934cc5cd7f2d01d5cd9
--- /dev/null
+++ b/notebooks/tests/eval.ipynb
@@ -0,0 +1,152 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Expressions can be evaluated."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "123"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "123"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "579"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "123 + 456"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "{1,2,5,6}"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{1, 2} \\/ {5, 6}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "{1,2,3,4,5}"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1..5"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "3"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "MAXINT"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Solution variables are displayed."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "TRUE (xx = 3)"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "#xx.(xx : NAT1 & xx mod 3 = 0)"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
diff --git a/notebooks/tests/help.ipynb b/notebooks/tests/help.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..ad210782d8e0d9fa8d7c99b5933dcf8ebf32100c
--- /dev/null
+++ b/notebooks/tests/help.ipynb
@@ -0,0 +1,308 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "`:help` can be used to list all commands, or get help for a specific command. `:?` is equivalent to `:help`."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Type a valid B expression, or one of the following commands:\n",
+ "::echo Echoes the arguments and body back.\n",
+ "::load Load the machine source code from the body.\n",
+ ":? Display help for a specific command, or general help about the REPL.\n",
+ ":help Display help for a specific command, or general help about the REPL.\n"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Type a valid B expression, or one of the following commands:\n",
+ "::echo Echoes the arguments and body back.\n",
+ "::load Load the machine source code from the body.\n",
+ ":? Display help for a specific command, or general help about the REPL.\n",
+ ":help Display help for a specific command, or general help about the REPL.\n"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":?"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ ":? [COMMAND]\n",
+ ":help [COMMAND]\n",
+ "\n",
+ "Display help for a specific command, or general help about the REPL."
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help :help"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ ":? [COMMAND]\n",
+ ":help [COMMAND]\n",
+ "\n",
+ "Display help for a specific command, or general help about the REPL."
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":? :?"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "::load\n",
+ "MACHINE\n",
+ "...\n",
+ "END\n",
+ "\n",
+ "Load the machine source code from the body."
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help ::load"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "When looking up help for a command, the `:` or `::` can be left off of the command name."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ ":? [COMMAND]\n",
+ ":help [COMMAND]\n",
+ "\n",
+ "Display help for a specific command, or general help about the REPL."
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help help"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ ":? [COMMAND]\n",
+ ":help [COMMAND]\n",
+ "\n",
+ "Display help for a specific command, or general help about the REPL."
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help ?"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "::load\n",
+ "MACHINE\n",
+ "...\n",
+ "END\n",
+ "\n",
+ "Load the machine source code from the body."
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help load"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "But it's not possible to use the wrong number of colons."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":help: Cannot display help for unknown command \"::help\"",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:help: Cannot display help for unknown command \"::help\"\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ ":help ::help"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":help: Cannot display help for unknown command \":load\"",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:help: Cannot display help for unknown command \":load\"\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ ":help :load"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Unknown commands cannot be looked up."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":help: Cannot display help for unknown command \"wrong\"",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:help: Cannot display help for unknown command \"wrong\"\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ ":help wrong"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":help: Cannot display help for unknown command \":wrong\"",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:help: Cannot display help for unknown command \":wrong\"\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ ":help :wrong"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
diff --git a/notebooks/tests/load.ipynb b/notebooks/tests/load.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..0578cc3565998c44c260feafb9acb928881e791e
--- /dev/null
+++ b/notebooks/tests/load.ipynb
@@ -0,0 +1,141 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Machines can be loaded from code in the notebook."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "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": [
+ "Loaded machine: things : []\n"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE things\n",
+ "SETS THINGS = {ONE, TWO, THREE, FOUR}\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "{ONE,TWO,THREE,FOUR}"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "THINGS"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Preference values can be specified."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "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": [
+ "Loaded machine: prefs : []\n"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load MININT=-5 MAXINT=5\n",
+ "MACHINE prefs\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "{−5,−4,−3,−2,−1,0,1,2,3,4,5}"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "MININT..MAXINT"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}