diff --git a/00_ProB_Jupyter_Notebook_Overview.ipynb b/manual/00_ProB_Jupyter_Notebook_Overview.ipynb
similarity index 100%
rename from 00_ProB_Jupyter_Notebook_Overview.ipynb
rename to manual/00_ProB_Jupyter_Notebook_Overview.ipynb
diff --git a/manual/ExternalFunctions.ipynb b/manual/ExternalFunctions.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..9030aec066e16edb5ec3abe16ed3740080a35f35
--- /dev/null
+++ b/manual/ExternalFunctions.ipynb
@@ -0,0 +1,5638 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# External Functions\n",
+ "## LibraryStrings\n",
+ "\n",
+ "In pure B there are only two built-in operators on strings: equality $=$ and inequality $\\neq$.\n",
+ "This library provides several string manipulation functions, and assumes that STRINGS are\n",
+ " sequences of unicode characters (in UTF-8 encoding).\n",
+ "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n",
+ "\n",
+ "`DEFINITIONS \"LibraryStrings.def\"`\n",
+ "\n",
+ "The file `LibraryStrings.def` is bundled with ProB and can be found in the `stdlib` folder.\n",
+ "You can also include the machine `LibraryStrings.mch` instead of the definition file;\n",
+ " the machine defines some of the functions below as proper B functions (i.e., functions\n",
+ " for which you can compute the domain and use constructs such as\n",
+ " relational image)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Jupyter_LibraryStrings"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Jupyter_LibraryStrings\n",
+ "DEFINITIONS \"LibraryStrings.def\"\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### STRING_APPEND\n",
+ "\n",
+ "This external function takes two strings and concatenates them.\n",
+ "\n",
+ "Type: $STRING \\times STRING \\rightarrow STRING $."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"abcabc\"}$"
+ ],
+ "text/plain": [
+ "\"abcabc\""
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_APPEND(\"abc\",\"abc\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"abc\"}$"
+ ],
+ "text/plain": [
+ "\"abc\""
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_APPEND(\"abc\",\"\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### STRING_LENGTH\n",
+ "\n",
+ "This external function takes a string and returns the length.\n",
+ "\n",
+ "Type: $STRING \\rightarrow INTEGER$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$3$"
+ ],
+ "text/plain": [
+ "3"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_LENGTH(\"abc\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$0$"
+ ],
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 5,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_LENGTH(\"\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### STRING_SPLIT\n",
+ "\n",
+ "This external function takes two strings and separates the first string\n",
+ " according to the separator specified by the second string.\n",
+ "\n",
+ "Type: $STRING \\times STRING \\rightarrow \\mathit{seq}(STRING) $."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"filename\"}),(2\\mapsto\\text{\"ext\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"filename\"),(2↦\"ext\")}"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_SPLIT(\"filename.ext\",\".\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"filename.ext\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"filename.ext\")}"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_SPLIT(\"filename.ext\",\"/\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"usr\"}),(2\\mapsto\\text{\"local\"}),(3\\mapsto\\text{\"lib\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"usr\"),(2↦\"local\"),(3↦\"lib\")}"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_SPLIT(\"usr/local/lib\",\"/\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"\")}"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_SPLIT(\"\",\".\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "I am not sure the following result makes sense, maybe a sequence of all characters is more appropriate?"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"usr/local/lib\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"usr/local/lib\")}"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_SPLIT(\"usr/local/lib\",\"\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"usr/lo\"}),(2\\mapsto\\text{\"/lib\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"usr/lo\"),(2↦\"/lib\")}"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_SPLIT(\"usr/local/lib\",\"cal\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### STRING_JOIN\n",
+ "This external function takes a sequence of strings and a separator string\n",
+ " and joins the strings together inserting the separators as often as needed.\n",
+ "It is the inverse of the `STRING_SPLIT` function.\n",
+ "\n",
+ "Type: $\\mathit{seq}(STRING) \\times STRING \\rightarrow STRING $."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"usr/local/lib\"}$"
+ ],
+ "text/plain": [
+ "\"usr/local/lib\""
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_JOIN([\"usr\",\"local\",\"lib\"],\"/\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"usr/local/lib\"}$"
+ ],
+ "text/plain": [
+ "\"usr/local/lib\""
+ ]
+ },
+ "execution_count": 13,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_JOIN([\"usr/lo\",\"/lib\"],\"cal\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"usr/local/lib\"}$"
+ ],
+ "text/plain": [
+ "\"usr/local/lib\""
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_JOIN([\"usr/local/lib\"],\"\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### STRING_CHARS\n",
+ "\n",
+ "This external function takes a strings splits it into a sequence\n",
+ "of the individual characters. Each character is represented by a string.\n",
+ "\n",
+ "Type: $STRING \\rightarrow \\mathit{seq}(STRING) $."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ ],
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 15,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_CHARS(\"\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"a\"}),(2\\mapsto\\text{\"b\"}),(3\\mapsto\\text{\"c\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"a\"),(2↦\"b\"),(3↦\"c\")}"
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_CHARS(\"abc\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"a.b.c\"}$"
+ ],
+ "text/plain": [
+ "\"a.b.c\""
+ ]
+ },
+ "execution_count": 17,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_JOIN(STRING_CHARS(\"abc\"),\".\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### STRING_CODES\n",
+ "\n",
+ "This external function takes a strings splits it into a sequence\n",
+ "of the individual characters. Each character is represented by a natural number\n",
+ " (the ASCII or Unicode representation of the character).\n",
+ "\n",
+ "Type: $STRING \\rightarrow \\mathit{seq}(INTEGER) $."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ ],
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_CODES(\"\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 19,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto 65),(2\\mapsto 90),(3\\mapsto 32),(4\\mapsto 97),(5\\mapsto 122),(6\\mapsto 32),(7\\mapsto 48),(8\\mapsto 57)\\}$"
+ ],
+ "text/plain": [
+ "{(1↦65),(2↦90),(3↦32),(4↦97),(5↦122),(6↦32),(7↦48),(8↦57)}"
+ ]
+ },
+ "execution_count": 19,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_CODES(\"AZ az 09\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### CODES_TO_STRING\n",
+ "\n",
+ "This external function is the inverse of the ```STRING_CODES``` function above.\n",
+ "\n",
+ "Type: $\\mathit{seq}(INTEGER)\\rightarrow STRING$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"ABC\"}$"
+ ],
+ "text/plain": [
+ "\"ABC\""
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "CODES_TO_STRING([65,66,67])"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### STRING_TO_UPPER\n",
+ "\n",
+ "This external function converts a string to upper-case letters. It currently converts also diacritical marks (this behaviour may in future be controlled by an additional flag or option).\n",
+ "\n",
+ "Type: $STRING \\rightarrow STRING $."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 21,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"ABC_ABC\"}$"
+ ],
+ "text/plain": [
+ "\"ABC_ABC\""
+ ]
+ },
+ "execution_count": 21,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_TO_UPPER(\"abc_ABC\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"AZ-AZ-09-AAOU-AO\"}$"
+ ],
+ "text/plain": [
+ "\"AZ-AZ-09-AAOU-AO\""
+ ]
+ },
+ "execution_count": 22,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_TO_UPPER(\"az-AZ-09-äàöù-ÄÖ\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"\"}$"
+ ],
+ "text/plain": [
+ "\"\""
+ ]
+ },
+ "execution_count": 23,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_TO_UPPER(\"\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### STRING_TO_LOWER\n",
+ "\n",
+ "This external function converts a string to lower-case letters. It currently converts also diacritical marks (this behaviour may in future be controlled by an additional flag or option).\n",
+ "\n",
+ "Type: $STRING \\rightarrow STRING $."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 24,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"az-az-09-aaou-ao\"}$"
+ ],
+ "text/plain": [
+ "\"az-az-09-aaou-ao\""
+ ]
+ },
+ "execution_count": 24,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_TO_LOWER(\"az-AZ-09-äàöù-ÄÖ\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### SUB_STRING\n",
+ "\n",
+ "This external function takes a strings a position and a sequence and produces a corresponding substring.\n",
+ "The numbering starts at 1 and the position must be at least 1, but can extend beyond the end of the string.\n",
+ "\n",
+ "Type: $STRING \\times INTEGER \\times INTEGER \\rightarrow STRING $."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"abc\"}$"
+ ],
+ "text/plain": [
+ "\"abc\""
+ ]
+ },
+ "execution_count": 25,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SUB_STRING(\"abcdefg\",1,3)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"abcdefg\"}$"
+ ],
+ "text/plain": [
+ "\"abcdefg\""
+ ]
+ },
+ "execution_count": 26,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SUB_STRING(\"abcdefg\",1,100)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"de\"}$"
+ ],
+ "text/plain": [
+ "\"de\""
+ ]
+ },
+ "execution_count": 27,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SUB_STRING(\"abcdefg\",4,2)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 28,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"\"}$"
+ ],
+ "text/plain": [
+ "\"\""
+ ]
+ },
+ "execution_count": 28,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SUB_STRING(\"abcdefg\",3,0)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 29,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"\"}$"
+ ],
+ "text/plain": [
+ "\"\""
+ ]
+ },
+ "execution_count": 29,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SUB_STRING(\"abcdefg\",11,3)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### STRING_IS_INT"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "\n",
+ "This external predicate takes a string and is true if the string represents an integer.\n",
+ "\n",
+ "Type: $STRING $."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 30,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 30,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_IS_INT(\"1204\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 31,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 31,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_IS_INT(\"-1204\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 32,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 32,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_IS_INT(\" - 1204\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 33,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 33,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_IS_INT(\"1.1\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 34,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 34,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_IS_INT(\"1.0\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 35,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 35,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_IS_INT(\"a\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 36,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 36,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_IS_INT(\"1000000000000000000000000000\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 37,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 37,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_IS_INT(\"-00001\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 38,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 38,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_IS_INT(\"00002\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### STRING_TO_INT\n",
+ "\n",
+ "This external function takes a string and converts it into an integer.\n",
+ "An error is raised if this cannot be done.\n",
+ "It is safer to first check with `STRING_IS_INT` whether the conversion can be done.\n",
+ "\n",
+ "Type: $STRING \\rightarrow INTEGER$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 39,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1024$"
+ ],
+ "text/plain": [
+ "1024"
+ ]
+ },
+ "execution_count": 39,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_TO_INT(\"1024\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 40,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$-1$"
+ ],
+ "text/plain": [
+ "−1"
+ ]
+ },
+ "execution_count": 40,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_TO_INT(\" - 00001\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### INT_TO_STRING\n",
+ "\n",
+ "This external function converts an integer to a string representation.\n",
+ "\n",
+ "Type: $INTEGER \\rightarrow STRING $."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 41,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"1024\"}$"
+ ],
+ "text/plain": [
+ "\"1024\""
+ ]
+ },
+ "execution_count": 41,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "INT_TO_STRING(1024)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 42,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"-1024\"}$"
+ ],
+ "text/plain": [
+ "\"-1024\""
+ ]
+ },
+ "execution_count": 42,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "INT_TO_STRING(-1024)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 43,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"-1\"}$"
+ ],
+ "text/plain": [
+ "\"-1\""
+ ]
+ },
+ "execution_count": 43,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "INT_TO_STRING(STRING_TO_INT(\" - 00001\"))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 44,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 44,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_TO_INT(INT_TO_STRING(-1))=-1"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### DEC_STRING_TO_INT\n",
+ "\n",
+ "This external function takes a decimal string (with optional decimal places) and converts it to an integer with the given precision (rounding if required).\n",
+ "\n",
+ "Type: $STRING \\times INTEGER \\rightarrow INTEGER$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 45,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1024$"
+ ],
+ "text/plain": [
+ "1024"
+ ]
+ },
+ "execution_count": 45,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "DEC_STRING_TO_INT(\"1024\",0)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 46,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$102400$"
+ ],
+ "text/plain": [
+ "102400"
+ ]
+ },
+ "execution_count": 46,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "DEC_STRING_TO_INT(\"1024\",2)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 47,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$102$"
+ ],
+ "text/plain": [
+ "102"
+ ]
+ },
+ "execution_count": 47,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "DEC_STRING_TO_INT(\"1024\",-1)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 48,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$103$"
+ ],
+ "text/plain": [
+ "103"
+ ]
+ },
+ "execution_count": 48,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "DEC_STRING_TO_INT(\"1025\",-1)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 49,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$-103$"
+ ],
+ "text/plain": [
+ "−103"
+ ]
+ },
+ "execution_count": 49,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "DEC_STRING_TO_INT(\" -1025\",-1)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 50,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$102423$"
+ ],
+ "text/plain": [
+ "102423"
+ ]
+ },
+ "execution_count": 50,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "DEC_STRING_TO_INT(\"1024.234\",2)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 51,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$10240000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000$"
+ ],
+ "text/plain": [
+ "10240000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+ ]
+ },
+ "execution_count": 51,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "DEC_STRING_TO_INT(\"1024\",100)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 52,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 52,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "DEC_STRING_TO_INT(\"10000000000000000000000000000000000\",-32)=100"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### INT_TO_DEC_STRING\n",
+ "\n",
+ "This external function converts an integer to a decimal string representation\n",
+ " with the precision provided by the second argument.\n",
+ "\n",
+ "Type: $INTEGER \\times INTEGER \\rightarrow STRING $."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 53,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"12.04\"}$"
+ ],
+ "text/plain": [
+ "\"12.04\""
+ ]
+ },
+ "execution_count": 53,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "INT_TO_DEC_STRING(1204,2)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 54,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"-1.204\"}$"
+ ],
+ "text/plain": [
+ "\"-1.204\""
+ ]
+ },
+ "execution_count": 54,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "INT_TO_DEC_STRING(-1204,3)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 55,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"0.00\"}$"
+ ],
+ "text/plain": [
+ "\"0.00\""
+ ]
+ },
+ "execution_count": 55,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "INT_TO_DEC_STRING(0,2)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 56,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"120400\"}$"
+ ],
+ "text/plain": [
+ "\"120400\""
+ ]
+ },
+ "execution_count": 56,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "INT_TO_DEC_STRING(1204,-2)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 57,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"-0.010\"}$"
+ ],
+ "text/plain": [
+ "\"-0.010\""
+ ]
+ },
+ "execution_count": 57,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "INT_TO_DEC_STRING(-10,3)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### INT_TO_HEX_STRING\n",
+ "\n",
+ "This external function converts an integer to a hexadecimal string representation.\n",
+ "\n",
+ "Type: $INTEGER \\rightarrow STRING $."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 58,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"fe\"}$"
+ ],
+ "text/plain": [
+ "\"fe\""
+ ]
+ },
+ "execution_count": 58,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "INT_TO_HEX_STRING(254)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 59,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"0\"}$"
+ ],
+ "text/plain": [
+ "\"0\""
+ ]
+ },
+ "execution_count": 59,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "INT_TO_HEX_STRING(0)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 60,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"-fe\"}$"
+ ],
+ "text/plain": [
+ "\"-fe\""
+ ]
+ },
+ "execution_count": 60,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "INT_TO_HEX_STRING(-254)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 61,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"fffffffffffffffffffffffff\"}$"
+ ],
+ "text/plain": [
+ "\"fffffffffffffffffffffffff\""
+ ]
+ },
+ "execution_count": 61,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "INT_TO_HEX_STRING(2**100-1)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### TO_STRING\n",
+ "\n",
+ "This external function converts a B data value to a string representation.\n",
+ "\n",
+ "Type: $\\tau \\rightarrow STRING$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 62,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"1024\"}$"
+ ],
+ "text/plain": [
+ "\"1024\""
+ ]
+ },
+ "execution_count": 62,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "TO_STRING(1024)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 63,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"1024\"}$"
+ ],
+ "text/plain": [
+ "\"1024\""
+ ]
+ },
+ "execution_count": 63,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "TO_STRING(\"1024\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 64,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"{2,3,5}\"}$"
+ ],
+ "text/plain": [
+ "\"{2,3,5}\""
+ ]
+ },
+ "execution_count": 64,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "TO_STRING({2,3,5})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 65,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"(TRUE|->3|->{(11|->rec(a:22,b:33))})\"}$"
+ ],
+ "text/plain": [
+ "\"(TRUE|->3|->{(11|->rec(a:22,b:33))})\""
+ ]
+ },
+ "execution_count": 65,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "TO_STRING((TRUE,3,{11|->rec(a:22,b:33)}))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### FORMAT_TO_STRING\n",
+ "This external function takes a format string and a B sequence of values and generates an output string, where the values have been inserted into the format string in place of the `~w` placeholders.\n",
+ " - the length of sequence must correspond to the number of `~w` in the format string.\n",
+ " - the format string follows the conventions of SICStus Prolog.\n",
+ " E.g., one can use `~n` for newlines.\n",
+ "\n",
+ "\n",
+ "Type: $(STRING*seq(\\tau)) \\rightarrow STRING$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 66,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"two to the power ten = 1024\"}$"
+ ],
+ "text/plain": [
+ "\"two to the power ten = 1024\""
+ ]
+ },
+ "execution_count": 66,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "FORMAT_TO_STRING(\"two to the power ten = ~w\",[2**10])"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 67,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"My two sets are {1,2} and {}\"}$"
+ ],
+ "text/plain": [
+ "\"My two sets are {1,2} and {}\""
+ ]
+ },
+ "execution_count": 67,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "FORMAT_TO_STRING(\"My two sets are ~w and ~w\",[1..2,2..1])"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "#### Format Strings\n",
+ "\n",
+ "Various external functions and predicates work with format strings.\n",
+ "ProB uses the conventions of the SICStus Prolog format string.\n",
+ " - `~n` inserts a newline into the generated output\n",
+ " - `~Nn` where N is a number: it inserts $N$ newlines into the output\n",
+ " - `~w` inserts the next argument into the generated output\n",
+ " - `~i` consumes the next argument but ignores it; i.e., nothing is inserted into the output\n",
+ " - `~~` inserts the tilde symbol into the generated output\n",
+ " - `~N` inserts a newline if not at the beginning of the line\n",
+ "\n",
+ "SICStus Prolog also uses a few other formatting codes, such as `~@`, `~p`,... which should not be used."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### STRINGIFY\n",
+ "\n",
+ "This external function converts a B expression to a string representation of the expression, not the value.\n",
+ "It can be used to obtain the name of variables.\n",
+ "Warning: ProB may simplify and rewrite expressions (you can turn this off by setting the OPTIMIZE_AST preference to false).\n",
+ "\n",
+ "Type: $\\tau \\rightarrow STRING$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 68,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"dom({1 |-> 2})\"}$"
+ ],
+ "text/plain": [
+ "\"dom({1 |-> 2})\""
+ ]
+ },
+ "execution_count": 68,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRINGIFY(dom({1|->2}))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Compare this with the result of TO_STRING:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 69,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"{1}\"}$"
+ ],
+ "text/plain": [
+ "\"{1}\""
+ ]
+ },
+ "execution_count": 69,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "TO_STRING(dom({1|->2}))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 70,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "|stringify|tostring|\n",
+ "|---|---|\n",
+ "|$\\text{\"\\\"abc\\\"\"}$|$\\text{\"abc\"}$|\n"
+ ],
+ "text/plain": [
+ "stringify\ttostring\n",
+ "\"\\\"abc\\\"\"\t\"abc\"\n"
+ ]
+ },
+ "execution_count": 70,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":table rec(stringify:STRINGIFY(\"abc\"),tostring:TO_STRING(\"abc\"))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Choose Operators\n",
+ "You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:\n",
+ " `DEFINITIONS \"CHOOSE.def\"`\n",
+ "\n",
+ "### Choose\n",
+ "\n",
+ "This external function takes a set and returns an element of the set.\n",
+ "This is a proper mathematical function, i.e., it will always return the same value\n",
+ "given the same argument.\n",
+ "It is also known as Hilbert's operator.\n",
+ "\n",
+ "The operator raises an error when it is called with an empty set.\n",
+ "Also, it is not guaranteed to work for infinite sets.\n",
+ "\n",
+ "Type: $POW(T) \\rightarrow T$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 71,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Jupyter_CHOOSE"
+ ]
+ },
+ "execution_count": 71,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Jupyter_CHOOSE\n",
+ "DEFINITIONS \"CHOOSE.def\"\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 72,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1$"
+ ],
+ "text/plain": [
+ "1"
+ ]
+ },
+ "execution_count": 72,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "CHOOSE(1..3)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 73,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1$"
+ ],
+ "text/plain": [
+ "1"
+ ]
+ },
+ "execution_count": 73,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "CHOOSE({1,2,3})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 74,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"a\"}$"
+ ],
+ "text/plain": [
+ "\"a\""
+ ]
+ },
+ "execution_count": 74,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "CHOOSE({\"a\",\"b\",\"c\"})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 75,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$0$"
+ ],
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 75,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "CHOOSE(NATURAL)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 76,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$0$"
+ ],
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 76,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "CHOOSE(INTEGER)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The operator is useful for writing WHILE loops or recursive functions which manipulate sets.\n",
+ "The following example defines a recursive summation function using the CHOOSE operator.\n",
+ "\n",
+ "```\n",
+ "MACHINE RecursiveSigmaCHOOSEv3\n",
+ "DEFINITIONS\n",
+ " \"Choose.def\"\n",
+ "ABSTRACT_CONSTANTS sigma\n",
+ "PROPERTIES\n",
+ " sigma: POW(INTEGER) <-> INTEGER &\n",
+ " sigma = %x.(x:POW(INTEGER) |\n",
+ " IF x={} THEN 0 ELSE\n",
+ " LET c BE c=CHOOSE(x) IN c+sigma(x-{c}) END\n",
+ " END\n",
+ " )\n",
+ "ASSERTIONS\n",
+ " sigma({3,5,7}) = 15;\n",
+ "END\n",
+ "```"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "\n",
+ "### MU\n",
+ "\n",
+ "Just like CHOOSE, this external function takes a set and returns an element of the set.\n",
+ "In contrast to CHOOSE, it is only defined for singleton sets.\n",
+ "The operator raises an error when it is called with an empty set or a set containing more than one element.\n",
+ "\n",
+ "Type: $POW(T) \\rightarrow T$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 77,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$2$"
+ ],
+ "text/plain": [
+ "2"
+ ]
+ },
+ "execution_count": 77,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "MU({2})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 78,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$3$"
+ ],
+ "text/plain": [
+ "3"
+ ]
+ },
+ "execution_count": 78,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "MU({2})+MU({x|x>0 & x<2})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Sorting Sets\n",
+ "You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:\n",
+ "`DEFINITIONS \"SORT.def\"`\n",
+ "\n",
+ "Alternatively you can use the following if you use ProB prior to version 1.7.1:\n",
+ "`\n",
+ "DEFINITIONS\n",
+ " SORT(X) == [];\n",
+ " EXTERNAL_FUNCTION_SORT(T) == (POW(T)-->seq(T));\n",
+ "`\n",
+ "\n",
+ "This external function SORT takes a set and translates it into a B sequence.\n",
+ "It uses ProB's internal order for sorting the elements.\n",
+ "It will not work for infinite sets.\n",
+ "Type: $POW(\\tau) \\rightarrow seq(\\tau)$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 79,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Jupyter_SORT"
+ ]
+ },
+ "execution_count": 79,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Jupyter_SORT\n",
+ "DEFINITIONS \"SORT.def\"\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 80,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto 1),(2\\mapsto 2),(3\\mapsto 3)\\}$"
+ ],
+ "text/plain": [
+ "{(1↦1),(2↦2),(3↦3)}"
+ ]
+ },
+ "execution_count": 80,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SORT(1..3)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 81,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto 6),(2\\mapsto 9),(3\\mapsto 27)\\}$"
+ ],
+ "text/plain": [
+ "{(1↦6),(2↦9),(3↦27)}"
+ ]
+ },
+ "execution_count": 81,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SORT({3*3,3+3,3**3})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 82,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"1\"}),(2\\mapsto\\text{\"10\"}),(3\\mapsto\\text{\"11\"}),(4\\mapsto\\text{\"2\"}),(5\\mapsto\\text{\"a\"}),(6\\mapsto\\text{\"aa\"}),(7\\mapsto\\text{\"ab\"}),(8\\mapsto\\text{\"b\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"1\"),(2↦\"10\"),(3↦\"11\"),(4↦\"2\"),(5↦\"a\"),(6↦\"aa\"),(7↦\"ab\"),(8↦\"b\")}"
+ ]
+ },
+ "execution_count": 82,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SORT({\"ab\",\"aa\",\"a\",\"b\",\"10\",\"1\",\"2\",\"11\"})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 83,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto(\\text{\"a\"}\\mapsto 0)),(2\\mapsto(\\text{\"a\"}\\mapsto 1)),(3\\mapsto(\\text{\"b\"}\\mapsto 0))\\}$"
+ ],
+ "text/plain": [
+ "{(1↦(\"a\"↦0)),(2↦(\"a\"↦1)),(3↦(\"b\"↦0))}"
+ ]
+ },
+ "execution_count": 83,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SORT({(\"a\"|->1),(\"b\"|->0),(\"a\"|->0)})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "A related external function is LEQ_SYM_BREAK which allows one to compare values of arbitrary type.\n",
+ "Calls to this external function are automatically\n",
+ "inserted by ProB for symmetry breaking of quantifiers.\n",
+ "It should currently not be used for sets or sequences."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The SORT.def file also contains a definition for the SQUASH operator which takes a sequence with gaps and completes it into a proper sequence:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 84,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"a\"}),(2\\mapsto\\text{\"b\"}),(3\\mapsto\\text{\"c\"}),(4\\mapsto\\text{\"c\"}),(5\\mapsto\\text{\"d\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"a\"),(2↦\"b\"),(3↦\"c\"),(4↦\"c\"),(5↦\"d\")}"
+ ]
+ },
+ "execution_count": 84,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SQUASH({0|->\"a\",100|->\"c\",1001 |->\"d\",4|->\"b\", 44|->\"c\"})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## Strongly Connected Components\n",
+ "You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:\n",
+ "`DEFINITIONS \"SCCS.def\"`\n",
+ "\n",
+ "Alternatively you can use the following if you use ProB prior to version 1.9.0:\n",
+ "`\n",
+ "DEFINITIONS\n",
+ " EXTERNAL_FUNCTION_SCCS(T) == (T<->T) --> POW(POW(T));\n",
+ " SCCS(relation) == {};\n",
+ "`\n",
+ "\n",
+ "This external function SCCS takes a binary relation and computes the set of strongly connected components.\n",
+ "Type: $POW(\\tau \\times \\tau) \\rightarrow POW(POW(\\tau))$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 85,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Jupyter_SCCS"
+ ]
+ },
+ "execution_count": 85,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Jupyter_SCCS\n",
+ "DEFINITIONS \"SCCS.def\"\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 86,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\{1,2\\},\\{3,4\\}\\}$"
+ ],
+ "text/plain": [
+ "{{1,2},{3,4}}"
+ ]
+ },
+ "execution_count": 86,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SCCS({1|->2,2|->1,2|->3,3|->4,4|->3})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 87,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "image/svg+xml": [
+ "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+ "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+ " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+ "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
+ " -->\n",
+ "<!-- Title: state Pages: 1 -->\n",
+ "<svg width=\"176pt\" height=\"131pt\"\n",
+ " viewBox=\"0.00 0.00 176.00 131.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+ "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 127)\">\n",
+ "<title>state</title>\n",
+ "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-127 172,-127 172,4 -4,4\"/>\n",
+ "<!-- 4 -->\n",
+ "<g id=\"node1\" class=\"node\">\n",
+ "<title>4</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-123 0,-123 0,-87 54,-87 54,-123\"/>\n",
+ "<text text-anchor=\"middle\" x=\"27\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
+ "</g>\n",
+ "<!-- 3 -->\n",
+ "<g id=\"node2\" class=\"node\">\n",
+ "<title>3</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"73,-36 19,-36 19,0 73,0 73,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"46\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
+ "</g>\n",
+ "<!-- 4->3 -->\n",
+ "<g id=\"edge1\" class=\"edge\">\n",
+ "<title>4->3</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M13.9658,-86.8601C8.5525,-77.0267 4.4709,-64.7259 9,-54 10.4817,-50.491 12.4912,-47.1549 14.8124,-44.0309\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"17.6245,-46.1306 21.5364,-36.2844 12.3382,-41.542 17.6245,-46.1306\"/>\n",
+ "<text text-anchor=\"middle\" x=\"16.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
+ "</g>\n",
+ "<!-- 3->4 -->\n",
+ "<g id=\"edge2\" class=\"edge\">\n",
+ "<title>3->4</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M42.0682,-36.0034C39.4963,-47.7801 36.0828,-63.4102 33.1552,-76.8156\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"29.6511,-76.457 30.9368,-86.9735 36.4899,-77.9506 29.6511,-76.457\"/>\n",
+ "<text text-anchor=\"middle\" x=\"45.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
+ "</g>\n",
+ "<!-- 2 -->\n",
+ "<g id=\"node3\" class=\"node\">\n",
+ "<title>2</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"149,-123 95,-123 95,-87 149,-87 149,-123\"/>\n",
+ "<text text-anchor=\"middle\" x=\"122\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
+ "</g>\n",
+ "<!-- 2->3 -->\n",
+ "<g id=\"edge3\" class=\"edge\">\n",
+ "<title>2->3</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M106.2528,-86.9735C95.3492,-74.4919 80.6716,-57.6899 68.533,-43.7944\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"70.9419,-41.2319 61.7271,-36.0034 65.6701,-45.8371 70.9419,-41.2319\"/>\n",
+ "<text text-anchor=\"middle\" x=\"95.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
+ "</g>\n",
+ "<!-- 1 -->\n",
+ "<g id=\"node4\" class=\"node\">\n",
+ "<title>1</title>\n",
+ "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"168,-36 114,-36 114,0 168,0 168,-36\"/>\n",
+ "<text text-anchor=\"middle\" x=\"141\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
+ "</g>\n",
+ "<!-- 2->1 -->\n",
+ "<g id=\"edge4\" class=\"edge\">\n",
+ "<title>2->1</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M120.4276,-86.8094C120.0556,-76.961 120.3724,-64.6623 123,-54 123.7054,-51.1377 124.6671,-48.2411 125.7816,-45.3993\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"129.0662,-46.6305 130.0081,-36.0776 122.6909,-43.7398 129.0662,-46.6305\"/>\n",
+ "<text text-anchor=\"middle\" x=\"130.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
+ "</g>\n",
+ "<!-- 1->2 -->\n",
+ "<g id=\"edge5\" class=\"edge\">\n",
+ "<title>1->2</title>\n",
+ "<path fill=\"none\" stroke=\"#b22222\" d=\"M141.502,-36.171C141.3832,-46.0136 140.5982,-58.3131 138,-69 137.3184,-71.8037 136.4269,-74.6611 135.4132,-77.4782\"/>\n",
+ "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"132.1613,-76.1836 131.6235,-86.7648 138.6425,-78.8284 132.1613,-76.1836\"/>\n",
+ "<text text-anchor=\"middle\" x=\"147.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
+ "</g>\n",
+ "</g>\n",
+ "</svg>"
+ ],
+ "text/plain": [
+ "<Dot visualization: expr_as_graph [(\"rel\",{(1,2),(2,1),(2,3),(3,4),(4,3)})]>"
+ ]
+ },
+ "execution_count": 87,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":dot expr_as_graph (\"rel\",{1|->2,2|->1,2|->3,3|->4,4|->3})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 88,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\{2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,54,55,56,57,58,60,62,63,64,65,66,68,69,70,72,74,75,76,77,78,80,81,82,84,85,86,87,88,90,91,92,93,94,95,96,98,99,100\\},\\{53\\},\\{59\\},\\{61\\},\\{67\\},\\{71\\},\\{73\\},\\{79\\},\\{83\\},\\{89\\},\\{97\\}\\}$"
+ ],
+ "text/plain": [
+ "{{2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,54,55,56,57,58,60,62,63,64,65,66,68,69,70,72,74,75,76,77,78,80,81,82,84,85,86,87,88,90,91,92,93,94,95,96,98,99,100},{53},{59},{61},{67},{71},{73},{79},{83},{89},{97}}"
+ ]
+ },
+ "execution_count": 88,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SCCS({x,y|x:2..100 & y:2..100 & (x mod y = 0 or y mod x =0)})"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## LibraryMeta\n",
+ "This library provides various meta information about ProB and the current model.\n",
+ "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n",
+ "\n",
+ "`DEFINITIONS \"LibraryMeta.def\"`\n",
+ "\n",
+ "The file `LibraryMeta.def` is also bundled with ProB and can be found in the `stdlib` folder."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 89,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Jupyter_LibraryMeta"
+ ]
+ },
+ "execution_count": 89,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Jupyter_LibraryMeta\n",
+ "DEFINITIONS \"LibraryMeta.def\"\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### PROB_INFO_STR\n",
+ "This external function provides access to various information strings about ProB.\n",
+ "Type: $STRING \\rightarrow STRING$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 90,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"1.9.3-nightly\"}$"
+ ],
+ "text/plain": [
+ "\"1.9.3-nightly\""
+ ]
+ },
+ "execution_count": 90,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROB_INFO_STR(\"prob-version\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 91,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"50333f1779dcae2a9e6d1b2aa95a23678821f851\"}$"
+ ],
+ "text/plain": [
+ "\"50333f1779dcae2a9e6d1b2aa95a23678821f851\""
+ ]
+ },
+ "execution_count": 91,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROB_INFO_STR(\"prob-revision\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 92,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"Mon Feb 17 13:18:47 2020 +0100\"}$"
+ ],
+ "text/plain": [
+ "\"Mon Feb 17 13:18:47 2020 +0100\""
+ ]
+ },
+ "execution_count": 92,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROB_INFO_STR(\"prob-last-changed-date\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 93,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"1.8.0_202-b08\"}$"
+ ],
+ "text/plain": [
+ "\"1.8.0_202-b08\""
+ ]
+ },
+ "execution_count": 93,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROB_INFO_STR(\"java-version\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 94,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"/Library/Java/JavaVirtualMachines/jdk1.8.0_202.jdk/Contents/Home/bin/java\"}$"
+ ],
+ "text/plain": [
+ "\"/Library/Java/JavaVirtualMachines/jdk1.8.0_202.jdk/Contents/Home/bin/java\""
+ ]
+ },
+ "execution_count": 94,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROB_INFO_STR(\"java-command-path\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 95,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"18/2/2020 - 15h29 52s\"}$"
+ ],
+ "text/plain": [
+ "\"18/2/2020 - 15h29 52s\""
+ ]
+ },
+ "execution_count": 95,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROB_INFO_STR(\"current-time\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Another command is PROB_INFO_STR(\"parser-version\") which does not work within Jupyter."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### PROB_STATISTICS\n",
+ "This external function provides access to various statistics in the form of integers about ProB.\n",
+ "Type: $STRING \\rightarrow INTEGER$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 96,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$151477456$"
+ ],
+ "text/plain": [
+ "151477456"
+ ]
+ },
+ "execution_count": 96,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROB_STATISTICS(\"prolog-memory-bytes-used\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 97,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1$"
+ ],
+ "text/plain": [
+ "1"
+ ]
+ },
+ "execution_count": 97,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROB_STATISTICS(\"states\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 98,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$0$"
+ ],
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 98,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROB_STATISTICS(\"transitions\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 99,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$0$"
+ ],
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 99,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROB_STATISTICS(\"processed-states\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 100,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$-1$"
+ ],
+ "text/plain": [
+ "−1"
+ ]
+ },
+ "execution_count": 100,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROB_STATISTICS(\"current-state-id\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 101,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1582036192$"
+ ],
+ "text/plain": [
+ "1582036192"
+ ]
+ },
+ "execution_count": 101,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROB_STATISTICS(\"now-timestamp\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 102,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1658$"
+ ],
+ "text/plain": [
+ "1658"
+ ]
+ },
+ "execution_count": 102,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROB_STATISTICS(\"prolog-runtime\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 103,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$2881$"
+ ],
+ "text/plain": [
+ "2881"
+ ]
+ },
+ "execution_count": 103,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROB_STATISTICS(\"prolog-walltime\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Other possible information fields are prolog-memory-bytes-free,\n",
+ "prolog-global-stack-bytes-used,\n",
+ "prolog-local-stack-bytes-used,\n",
+ "prolog-global-stack-bytes-free,\n",
+ "prolog-local-stack-bytes-free,\n",
+ "prolog-trail-bytes-used,\n",
+ "prolog-choice-bytes-used,\n",
+ "prolog-atoms-bytes-used,\n",
+ "prolog-atoms-nb-used,\n",
+ "prolog-gc-count,\n",
+ "prolog-gc-time."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### PROJECT_STATISTICS\n",
+ "This external function provides access to various statistics in the form of integers about the current specification being processed, with all auxiliary files (i.e., project).\n",
+ "Type: $STRING \\rightarrow INTEGER$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 104,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$0$"
+ ],
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 104,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_STATISTICS(\"constants\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 105,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$0$"
+ ],
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 105,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_STATISTICS(\"variables\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 106,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$0$"
+ ],
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 106,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_STATISTICS(\"properties\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 107,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$0$"
+ ],
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 107,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_STATISTICS(\"invariants\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 108,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$0$"
+ ],
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 108,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_STATISTICS(\"operations\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 109,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$0$"
+ ],
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 109,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_STATISTICS(\"static_assertions\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 110,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$0$"
+ ],
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 110,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_STATISTICS(\"dynamic_assertions\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### PROJECT_INFO\n",
+ "This external function provides access to various information strings about the current specification being processed, with all auxiliary files (i.e., project).\n",
+ "Type: $STRING \\rightarrow POW(STRING)$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 111,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\text{\"(machine from Jupyter cell).mch\"},\\text{\"LibraryMeta.def\"}\\}$"
+ ],
+ "text/plain": [
+ "{\"(machine from Jupyter cell).mch\",\"LibraryMeta.def\"}"
+ ]
+ },
+ "execution_count": 111,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"files\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 112,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\text{\"(machine from Jupyter cell).mch\"}\\}$"
+ ],
+ "text/plain": [
+ "{\"(machine from Jupyter cell).mch\"}"
+ ]
+ },
+ "execution_count": 112,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"main-file\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 113,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ ],
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 113,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"variables\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 114,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ ],
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 114,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"constants\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 115,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ ],
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 115,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"sets\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 116,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ ],
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 116,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"operations\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 117,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ ],
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 117,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"assertion_labels\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 118,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ ],
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 118,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"invariant_labels\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 119,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\text{\"86ff5ffb3ecd6cc4b17b13a797508440fa2faa4c\"}\\}$"
+ ],
+ "text/plain": [
+ "{\"86ff5ffb3ecd6cc4b17b13a797508440fa2faa4c\"}"
+ ]
+ },
+ "execution_count": 119,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"sha-hash\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### MACHINE_INFO\n",
+ "This external function provides access to various information strings about B machines being processed.\n",
+ "Type: $STRING \\rightarrow STRING$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 120,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"abstract_machine\"}$"
+ ],
+ "text/plain": [
+ "\"abstract_machine\""
+ ]
+ },
+ "execution_count": 120,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "MACHINE_INFO(\"Jupyter_LibraryMeta\",\"TYPE\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## LibraryIO\n",
+ "\n",
+ "This library provides various input/output facilities.\n",
+ "It is probably most useful for debugging, but can also be used to write B machines\n",
+ "which can read and write data.\n",
+ "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n",
+ "\n",
+ "`DEFINITIONS \"LibraryIO.def\"`\n",
+ "\n",
+ "The file `LibraryIO.def` is also bundled with ProB and can be found in the `stdlib` folder."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## LibraryXML\n",
+ "\n",
+ "This library provides various functions to read and write XML data from file and strings.\n",
+ "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n",
+ "\n",
+ "`DEFINITIONS \"LibraryXML.def\"`\n",
+ "\n",
+ "The file `LibraryXML.def` is also bundled with ProB and can be found in the `stdlib` folder.\n",
+ "\n",
+ "### Internal Data Type\n",
+ "\n",
+ "An XML document is represented using the type seq(XML_ELement_Type), i.e., a sequence\n",
+ " of XML elements, whose type is defined by the following (included in the LibraryXML.def file):\n",
+ "\n",
+ "```\n",
+ " XML_ELement_Type == \n",
+ " struct(\n",
+ " recId: NATURAL1,\n",
+ " pId:NATURAL,\n",
+ " element:STRING,\n",
+ " attributes: STRING +-> STRING,\n",
+ " meta: STRING +-> STRING\n",
+ " );\n",
+ "```\n",
+ "\n",
+ "### Files and Strings\n",
+ "\n",
+ "XML documents can either be stored in a file or in a B string."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 121,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Jupyter_LibraryXML"
+ ]
+ },
+ "execution_count": 121,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Jupyter_LibraryXML\n",
+ "DEFINITIONS \"LibraryXML.def\"\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### READ_XML_FROM_STRING\n",
+ "This external function takes an XML document string and converts into into the B format seq(XML_ELement_Type)}.\n",
+ "Note that all strings in ProB are encoded using UTF-8, so no encoding argument has to be provided."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 122,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto \\mathit{rec}(\\mathit{attributes}\\in\\{(\\text{\"version\"}\\mapsto\\text{\"0.1\"})\\},\\mathit{element}\\in\\text{\"Data\"},\\mathit{meta}\\in\\{(\\text{\"xmlLineNumber\"}\\mapsto\\text{\"3\"})\\},\\mathit{pId}\\in 0,\\mathit{recId}\\in 1)),(2\\mapsto \\mathit{rec}(\\mathit{attributes}\\in\\{(\\text{\"attr1\"}\\mapsto\\text{\"value1\"}),(\\text{\"elemID\"}\\mapsto\\text{\"ID1\"})\\},\\mathit{element}\\in\\text{\"Tag1\"},\\mathit{meta}\\in\\{(\\text{\"xmlLineNumber\"}\\mapsto\\text{\"4\"})\\},\\mathit{pId}\\in 1,\\mathit{recId}\\in 2))\\}$"
+ ],
+ "text/plain": [
+ "{(1↦rec(attributes∈{(\"version\"↦\"0.1\")},element∈\"Data\",meta∈{(\"xmlLineNumber\"↦\"3\")},pId∈0,recId∈1)),(2↦rec(attributes∈{(\"attr1\"↦\"value1\"),(\"elemID\"↦\"ID1\")},element∈\"Tag1\",meta∈{(\"xmlLineNumber\"↦\"4\")},pId∈1,recId∈2))}"
+ ]
+ },
+ "execution_count": 122,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "READ_XML_FROM_STRING('''\n",
+ "<?xml version=\"1.0\" encoding=\"ASCII\"?>\n",
+ " <Data version= \"0.1\">\n",
+ " <Tag1 elemID=\"ID1\" attr1=\"value1\" />\n",
+ " </Data>\n",
+ "''')"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### READ_XML\n",
+ "\n",
+ "This external function can read in an XML document from file. In contrast to READ_XML_FROM_STRING\n",
+ "it also takes a second argument specifying the encoding used.\n",
+ "ProB cannot as of now detect the encoding from the XML header.\n",
+ "In future this argument may be removed.\n",
+ "Currently it can take these values:\n",
+ "\"auto\",\"ISO-8859-1\",\"ISO-8859-2\",\"ISO-8859-15\",\n",
+ " \"UTF-8\",\"UTF-16\",\"UTF-16LE\",\"UTF-16BE\",\"UTF-32\",\"UTF-32LE\",\"UTF-32BE\",\n",
+ " \"ANSI\\_X3.4-1968\", \"windows 1252\"."
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## LibraryHash\n",
+ "\n",
+ "This library provides various facilities to compute hash values for B values.\n",
+ "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n",
+ "\n",
+ "`DEFINITIONS \"LibraryHash.def\"`\n",
+ "\n",
+ "The file `LibraryHash.def` is also bundled with ProB and can be found in the `stdlib` folder."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 123,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Jupyter_LibraryHash"
+ ]
+ },
+ "execution_count": 123,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Jupyter_LibraryHash\n",
+ "DEFINITIONS \"LibraryHash.def\"\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### HASH\n",
+ "\n",
+ "This external function converts a B data value to an integer hash value. It uses the ```term_hash``` predicate of SICStus Prolog. It will generate an integer that can be efficiently handled by ProB, but may generate collisions.\n",
+ "\n",
+ "Type: $\\tau \\rightarrow INTEGER$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 124,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$92915201$"
+ ],
+ "text/plain": [
+ "92915201"
+ ]
+ },
+ "execution_count": 124,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "HASH({1,2,4})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 125,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$191034877$"
+ ],
+ "text/plain": [
+ "191034877"
+ ]
+ },
+ "execution_count": 125,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "HASH({1,2,5})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 126,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 126,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "i<: 1..7 & j<:1..7 & i /= j & HASH(i)=HASH(j)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### SHA_HASH\n",
+ "\n",
+ "This external function converts a B data value to a SHA hash value represented as a sequence of bytes. It is unlikely to generate a collision.\n",
+ "\n",
+ "Type: $\\tau \\rightarrow INTEGER$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 127,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto 37),(2\\mapsto 168),(3\\mapsto 75),(4\\mapsto 91),(5\\mapsto 175),(6\\mapsto 1),(7\\mapsto 8),(8\\mapsto 58),(9\\mapsto 13),(10\\mapsto 207),(11\\mapsto 7),(12\\mapsto 42),(13\\mapsto 222),(14\\mapsto 208),(15\\mapsto 212),(16\\mapsto 29),(17\\mapsto 243),(18\\mapsto 31),(19\\mapsto 27),(20\\mapsto 154)\\}$"
+ ],
+ "text/plain": [
+ "{(1↦37),(2↦168),(3↦75),(4↦91),(5↦175),(6↦1),(7↦8),(8↦58),(9↦13),(10↦207),(11↦7),(12↦42),(13↦222),(14↦208),(15↦212),(16↦29),(17↦243),(18↦31),(19↦27),(20↦154)}"
+ ]
+ },
+ "execution_count": 127,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SHA_HASH({1,2,4})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 128,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto 149),(2\\mapsto 81),(3\\mapsto 45),(4\\mapsto 24),(5\\mapsto 177),(6\\mapsto 25),(7\\mapsto 74),(8\\mapsto 30),(9\\mapsto 204),(10\\mapsto 7),(11\\mapsto 143),(12\\mapsto 202),(13\\mapsto 136),(14\\mapsto 116),(15\\mapsto 148),(16\\mapsto 247),(17\\mapsto 6),(18\\mapsto 221),(19\\mapsto 245),(20\\mapsto 52)\\}$"
+ ],
+ "text/plain": [
+ "{(1↦149),(2↦81),(3↦45),(4↦24),(5↦177),(6↦25),(7↦74),(8↦30),(9↦204),(10↦7),(11↦143),(12↦202),(13↦136),(14↦116),(15↦148),(16↦247),(17↦6),(18↦221),(19↦245),(20↦52)}"
+ ]
+ },
+ "execution_count": 128,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SHA_HASH({1,2,5})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 129,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 129,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "i<: 1..7 & j<:1..7 & i /= j & SHA_HASH(i)=SHA_HASH(j)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### SHA_HASH_HEX\n",
+ "\n",
+ "This external function converts a B data value to a SHA hash value represented as a hexadecimal string. It is unlikely to generate a collision.\n",
+ "\n",
+ "Type: $\\tau \\rightarrow STRING$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 130,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"25a84b5baf01083a0dcf072aded0d41df31f1b9a\"}$"
+ ],
+ "text/plain": [
+ "\"25a84b5baf01083a0dcf072aded0d41df31f1b9a\""
+ ]
+ },
+ "execution_count": 130,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SHA_HASH_HEX({1,2,4})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 131,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"95512d18b1194a1ecc078fca887494f706ddf534\"}$"
+ ],
+ "text/plain": [
+ "\"95512d18b1194a1ecc078fca887494f706ddf534\""
+ ]
+ },
+ "execution_count": 131,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SHA_HASH_HEX({1,2,5})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 132,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"6bd1d8beefa14ea131285d11bbf8580c5f31fe78\"}$"
+ ],
+ "text/plain": [
+ "\"6bd1d8beefa14ea131285d11bbf8580c5f31fe78\""
+ ]
+ },
+ "execution_count": 132,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SHA_HASH_HEX({x|x<:1..8 & card(x)=2})"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 133,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"068948b4d423a0db5fd1574edad799005fc456e0\"}$"
+ ],
+ "text/plain": [
+ "\"068948b4d423a0db5fd1574edad799005fc456e0\""
+ ]
+ },
+ "execution_count": 133,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SHA_HASH_HEX(0)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 134,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"55b9c89f79362578c3641774db978b5455be5bfd\"}$"
+ ],
+ "text/plain": [
+ "\"55b9c89f79362578c3641774db978b5455be5bfd\""
+ ]
+ },
+ "execution_count": 134,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "SHA_HASH_HEX(SHA_HASH_HEX(0))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## LibraryRegex\n",
+ "\n",
+ "This library provides various facilities for pattern matching with regular expressions.\n",
+ "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n",
+ "\n",
+ "`DEFINITIONS \"LibraryRegex.def\"`\n",
+ "\n",
+ "The file `LibraryRegex.def` is also bundled with ProB and can be found in the `stdlib` folder (as of version 1.8.3-beta4)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 135,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Jupyter_LibraryRegex"
+ ]
+ },
+ "execution_count": 135,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Jupyter_LibraryRegex\n",
+ "DEFINITIONS \"LibraryRegex.def\"; \"LibraryStrings.def\"\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The library works on B strings and regular expression patterns are also written as B strings.\n",
+ "The syntax used is the ECMAScript syntax: http://www.cplusplus.com/reference/regex/ECMAScript/\n",
+ "The library is currently implemented using the C++ standard library.\n",
+ "Below we repeat some information from http://www.cplusplus.com/reference/regex/ECMAScript/ for convenience.\n",
+ "\n",
+ "The library now does support UTF-8 encoded strings and patterns.\n",
+ "Note that ProB only supports UTF-8 for both B machines and for any strings and Unicode files it processes.\n",
+ "\n",
+ "#### Operators/Quantifiers\n",
+ "\n",
+ "More precisely the library accepts the following operators:\n",
+ "\n",
+ "| Syntax | Descr. | Matches |\n",
+ "| --- | --- | --- |\n",
+ "| ```*``` | 0 or more |The preceding atom is matched 0 or more times. |\n",
+ "| ```+``` |1 or more |The preceding atom is matched 1 or more times. |\n",
+ "| ```?``` |0 or 1 |The preceding atom is optional (matched either 0 times or once). |\n",
+ "| ```{int}``` |int |The preceding atom is matched exactly int times. |\n",
+ "| ```{int,}``` |int or more |The preceding atom is matched int or more times. |\n",
+ "| ```{min,max}``` |between min and max |The preceding atom is matched at least min times, but not more than max. |\n",
+ "\n",
+ "\n",
+ "There is also the ```|``` separator.\n",
+ "It separates two alternative patterns or subpatterns.\n",
+ "\n",
+ "\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "#### Characters\n",
+ "The library accepts the following special characters:\n",
+ "\n",
+ "| Syntax | Descr. | Matches |\n",
+ "| --- | --- | --- |\n",
+ "| ```.```\t| not newline\t| any character except line terminators (LF, CR, LS, PS).|\n",
+ "| ```\\t```\t| tab (HT)\t| a horizontal tab character (same as \\u0009).|\n",
+ "| ```\\n```\t| newline (LF)\t| a newline (line feed) character (same as \\u000A).|\n",
+ "| ```\\v```\t| vertical tab (VT)\t| a vertical tab character (same as \\u000B).|\n",
+ "| ```\\f```\t| form feed (FF)\t| a form feed character (same as \\u000C).|\n",
+ "| ```\\r```\t| carriage return (CR)\t| a carriage return character (same as \\u000D).|\n",
+ "| ```\\cletter```\t| control code\t| a control code character whose code unit value is the same as the remainder of dividing the code unit value of letter by 32.|\n",
+ "\n",
+ "For example: ```\\ca``` is the same as ```\\u0001```, ```\\cb``` the same as ```\\u0002```, and so on...\n",
+ "\n",
+ "| Syntax | Descr. | Matches |\n",
+ "| --- | --- | --- |\n",
+ "| ```\\xhh```| ASCII character| a character whose code unit value has an hex value equivalent to the two hex digits hh.|\n",
+ "\n",
+ "For example: ```\\x4c``` is the same as L, or ```\\x23``` the same as #.\n",
+ "\n",
+ "| Syntax | Descr. | Matches |\n",
+ "| --- | --- | --- |\n",
+ "| ```\\uhhhh```| unicode character| a character whose code unit value has an hex value equivalent to the four hex digits hhhh.|\n",
+ "| ```\\0```| null| a null character (same as \\u0000).|\n",
+ "| ```\\int```| backreference| the result of the submatch whose opening parenthesis is the int-th (int shall begin by a digit other than 0). See groups below for more info.|\n",
+ "| ```\\d```| digit| a decimal digit character (same as [[:digit:]]).|\n",
+ "| ```\\D```| not digit| any character that is not a decimal digit character (same as [^[:digit:]]).|\n",
+ "| ```\\s```| whitespace| a whitespace character (same as [[:space:]]).|\n",
+ "| ```\\S```| not whitespace| any character that is not a whitespace character (same as [^[:space:]]).|\n",
+ "| ```\\w```| word| an alphanumeric or underscore character (same as [_[:alnum:]]).|\n",
+ "| ```\\W```| not word| any character that is not an alphanumeric or underscore character (same as [^_[:alnum:]]).|\n",
+ "| ```\\character```| character| the character character as it is, without interpreting its special meaning within a regex expression.|\n",
+ "\n",
+ "Any character can be escaped except those which form any of the special character sequences above.\n",
+ "Needed for: ```^ $ \\ . * + ? ( ) [ ] { } |```\n",
+ "\n",
+ "\n",
+ "| Syntax | Descr. | Matches |\n",
+ "| --- | --- | --- |\n",
+ "| ```[class]```| character class| the target character is part of the class (see character classes below)|\n",
+ "| ```[^class]```| negated character class| the target character is not part of the class (see character classes below)|\n",
+ "\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "\n",
+ "\n",
+ "#### Groups\n",
+ "\n",
+ "Groups allow to apply quantifiers to a sequence of characters (instead of a single character). There are two kinds of groups:\n",
+ "\n",
+ "| characters| description| effects| \n",
+ "| --- | --- | --- |\n",
+ "| ```(subpattern)```| Group| Creates a backreference.\n",
+ "| ```(?:subpattern)```| Passive group| Does not create a backreference.\n",
+ "\n",
+ "#### Assertions\n",
+ "Assertions are conditions that do not consume characters in the target sequence: they do not describe a character, but a condition that must be fulfilled before or after a character.\n",
+ "\n",
+ "characters\tdescription\tcondition for match\n",
+ "\n",
+ "- ```^```\tBeginning of line\tEither it is the beginning of the target sequence, or follows a line terminator.\n",
+ "- ```$```\tEnd of line\tEither it is the end of the target sequence, or precedes a line terminator.\n",
+ "- ```\\b```\tWord boundary\tThe previous character is a word character and the next is a non-word character (or vice-versa).\n",
+ "Note: The beginning and the end of the target sequence are considered here as non-word characters.\n",
+ "- ```\\B```\tNot a word boundary\tThe previous and next characters are both word characters or both are non-word characters.\n",
+ "Note: The beginning and the end of the target sequence are considered here as non-word characters.\n",
+ "- ```(?=subpattern)```\tPositive lookahead\tThe characters following the assertion must match subpattern, but no characters are consumed.\n",
+ "- ```(?!subpattern)```\tNegative lookahead\tThe characters following the assertion must not match subpattern, but no characters are consumed.\n",
+ "\n",
+ "\n",
+ "#### Character classes\n",
+ "A character class defines a category of characters. It is introduced by enclosing its descriptors in square brackets ([ and ]).\n",
+ "The regex object attempts to match the entire character class against a single character in the target sequence (unless a quantifier specifies otherwise).\n",
+ "\n",
+ "The character class can contain any combination of:\n",
+ "Individual characters: Any character specified is considered part of the class (except the characters \\, [, ] and - when they have a special meaning as described in the following paragraphs).\n",
+ "For example:\n",
+ "```[abc]``` matches a, b or c.\n",
+ "```[^xyz]``` matches any character except x, y and z.\n",
+ "Ranges: They can be specified by using the hyphen character (-) between two valid characters.\n",
+ "For example:\n",
+ "```[a-z]``` matches any lowercase letter (a, b, c, ... until z).\n",
+ "```[abc1-5]``` matches either a, b or c, or a digit between 1 and 5.\n",
+ "POSIX-like classes: A whole set of predefined classes can be added to a custom character class. There are three kinds:\n",
+ "\n",
+ "class\tdescription\tnotes\n",
+ "- ```[:classname:]```\tcharacter class\tUses the regex traits' isctype member with the appropriate type gotten from applying lookup_classname member on classname for the match.\n",
+ "- ```[.classname.]```\tcollating sequence\tUses the regex traits' lookup_collatename to interpret classname.\n",
+ "- ```[=classname=]```\tcharacter equivalents\tUses the regex traits' transform_primary of the result of regex_traits::lookup_collatename for classname to check for matches.\n",
+ "\n",
+ "The choice of available classes depend on the regex traits type and on its selected locale. But at least the following character classes shall be recognized by any regex traits type and locale:\n",
+ "\n",
+ "class\tdescription\tequivalent (with regex_traits, default locale)\n",
+ "- ```[:alnum:]```\talpha-numerical character\tisalnum\n",
+ "- ```[:alpha:]```\talphabetic character\tisalpha\n",
+ "- ```[:blank:]```\tblank character\tisblank\n",
+ "- ```[:cntrl:]```\tcontrol character\tiscntrl\n",
+ "- ```[:digit:]```\tdecimal digit character\tisdigit\n",
+ "- ```[:graph:]```\tcharacter with graphical representation\tisgraph\n",
+ "- ```[:lower:]```\tlowercase letter\tislower\n",
+ "- ```[:print:]```\tprintable character\tisprint\n",
+ "- ```[:punct:]```\tpunctuation mark character\tispunct\n",
+ "- ```[:space:]```\twhitespace character\tisspace\n",
+ "- ```[:upper:]```\tuppercase letter\tisupper\n",
+ "- ```[:xdigit:]```\thexadecimal digit character\tisxdigit\n",
+ "- ```[:d:]```\tdecimal digit character\tisdigit\n",
+ "- ```[:w:]```\tword character\tisalnum\n",
+ "- ```[:s:]```\twhitespace character\tisspace\n",
+ "\n",
+ "Please note that the brackets in the class names are additional to those opening and closing the class definition.\n",
+ "For example:\n",
+ "```[[:alpha:]]``` is a character class that matches any alphabetic character.\n",
+ "```[abc[:digit:]]``` is a character class that matches a, b, c, or a digit.\n",
+ "```[^[:space:]]``` is a character class that matches any character except a whitespace.\n",
+ "\n",
+ "Escape characters: All escape characters described above can also be used within a character class specification. The only change is with \\b, that here is interpreted as a backspace character (\\u0008) instead of a word boundary.\n",
+ "Notice that within a class definition, those characters that have a special meaning in the regular expression (such as *, ., $) don't have such a meaning and are interpreted as normal characters (so they do not need to be escaped). Instead, within a class definition, the hyphen (-) and the brackets ([ and ]) do have special meanings under some circumstances, in which case they should be placed within the class in other locations where they do not have such special meaning, or be escaped with a backslash (\\).\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### REGEX_MATCH\n",
+ "\n",
+ "This external predicate checks if a string matches a regular expression pattern.\n",
+ "\n",
+ "For example, the following calls check whether the first argument is a non-empty sequenze of lower-case letters:\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 136,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 136,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_MATCH(\"abc\",\"[a-z]+\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 137,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 137,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_MATCH(\"abc1\",\"[a-z]+\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Here we check if we have a non-empty sequence of characters which are not letters:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 138,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 138,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_MATCH(\"123.45\",\"[^a-zA-Z]+\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 139,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 139,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_MATCH(\"1e9\",\"[^a-zA-Z]+\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Observe that ```REGEX_MATCH``` is a **predicate** not a function returning a boolean value.\n",
+ "As such you can write:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 140,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{str} = \\text{\"1.9\"}$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tstr = \"1.9\""
+ ]
+ },
+ "execution_count": 140,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "str = \"1.9\" & (REGEX_MATCH(str,\"[0-9]+\") or REGEX_MATCH(str,\"[0-9]*\\.[0-9]+\"))"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### IS_REGEXP\n",
+ "This external predicate checks if a string is a valid regular expression pattern.\n",
+ "Again, this is a **predicate**, not a function returning a boolean value."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 141,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 141,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "IS_REGEX(\"ab[0-9]\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 142,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 142,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "IS_REGEX(\"ab[0-9\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### REGEXP_REPLACE\n",
+ "\n",
+ "This external function replaces all occurences of a pattern in a string by a given replacement string.\n",
+ "\n",
+ "Type: $STRING \\times STRING \\times STRING \\rightarrow STRING$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 143,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"aNUMbNUMcNUMdNUM\"}$"
+ ],
+ "text/plain": [
+ "\"aNUMbNUMcNUMdNUM\""
+ ]
+ },
+ "execution_count": 143,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_REPLACE(\"a01b23c4d56\",\"[0-9]+\",\"NUM\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 144,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"X01X23X4X56\"}$"
+ ],
+ "text/plain": [
+ "\"X01X23X4X56\""
+ ]
+ },
+ "execution_count": 144,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_REPLACE(\"a01b23c4d56\",\"[^0-9]+\",\"X\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "You can use ```$1```, ```$2```, ... to refer to matches subgroups in the replacement string:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 145,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"1<<abcabd>>2\"}$"
+ ],
+ "text/plain": [
+ "\"1<<abcabd>>2\""
+ ]
+ },
+ "execution_count": 145,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_REPLACE(\"1abd00abc2\",\"([a-z]+).*?([a-z]+)\",\"<<$2$1>>\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "You can use ```$0``` to refer to the full match:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 146,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"ab(12)cd(34)\"}$"
+ ],
+ "text/plain": [
+ "\"ab(12)cd(34)\""
+ ]
+ },
+ "execution_count": 146,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_REPLACE(\"ab12cd34\",\"[0-9]+\",\"($0)\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### REGEX_SEARCH_STR\n",
+ "This external function searches for the **first** occurence of a pattern in a string.\n",
+ "\n",
+ "Type: $STRING \\times STRING \\rightarrow STRING$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 147,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"234\"}$"
+ ],
+ "text/plain": [
+ "\"234\""
+ ]
+ },
+ "execution_count": 147,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_STR(\"abcdef000234daf\",\"[1-9][0-9]*\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 148,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"abcdef\"}$"
+ ],
+ "text/plain": [
+ "\"abcdef\""
+ ]
+ },
+ "execution_count": 148,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_STR(\"abcdef000234daf\",\"[[:alpha:]]+\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "In the next example we use the ```$``` operator to force a match at the end:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 149,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"daf\"}$"
+ ],
+ "text/plain": [
+ "\"daf\""
+ ]
+ },
+ "execution_count": 149,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_STR(\"abcdef000234daf\",\"[[:alpha:]]+$\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "In case there is no match, it returns the empty string:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 150,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"\"}$"
+ ],
+ "text/plain": [
+ "\"\""
+ ]
+ },
+ "execution_count": 150,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_STR(\"0123\",\"[[:alpha:]]+\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### REGEX_SEARCH\n",
+ "This external function searches for the first occurence of a pattern in a string and returns full information about the match: position, length, match and sub-matches.\n",
+ "It also expects an index at which to start the search; which can be useful for writing loops to find all matches.\n",
+ "\n",
+ "Type: $STRING \\times INTEGER \\times STRING \\rightarrow struct(position:INTEGER,length:INTEGER,string:STRING,submatches:seq(STRING))$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 151,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{rec}(\\mathit{length}\\in 6,\\mathit{position}\\in 1,\\mathit{string}\\in\\text{\"abcdef\"},\\mathit{submatches}\\in\\emptyset)$"
+ ],
+ "text/plain": [
+ "rec(length∈6,position∈1,string∈\"abcdef\",submatches∈∅)"
+ ]
+ },
+ "execution_count": 151,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH(\"abcdef000234daf\",1,\"[[:alpha:]]+\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 152,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{rec}(\\mathit{length}\\in 3,\\mathit{position}\\in 13,\\mathit{string}\\in\\text{\"daf\"},\\mathit{submatches}\\in\\emptyset)$"
+ ],
+ "text/plain": [
+ "rec(length∈3,position∈13,string∈\"daf\",submatches∈∅)"
+ ]
+ },
+ "execution_count": 152,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH(\"abcdef000234daf\",7,\"[[:alpha:]]+\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 153,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{rec}(\\mathit{length}\\in 3,\\mathit{position}\\in 10,\\mathit{string}\\in\\text{\"234\"},\\mathit{submatches}\\in\\{(1\\mapsto\\text{\"2\"}),(2\\mapsto\\text{\"34\"})\\})$"
+ ],
+ "text/plain": [
+ "rec(length∈3,position∈10,string∈\"234\",submatches∈{(1↦\"2\"),(2↦\"34\")})"
+ ]
+ },
+ "execution_count": 153,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH(\"abcdef000234daf\",1,\"([1-9])([0-9]*)\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "In case there is no match, the function returns a record with position and length being -1:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 154,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{rec}(\\mathit{length}\\in-1,\\mathit{position}\\in-1,\\mathit{string}\\in\\text{\"\"},\\mathit{submatches}\\in\\emptyset)$"
+ ],
+ "text/plain": [
+ "rec(length∈−1,position∈−1,string∈\"\",submatches∈∅)"
+ ]
+ },
+ "execution_count": 154,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH(\"0123\",1,\"[[:alpha:]]+\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### REGEX_SEARCH_ALL\n",
+ "This external function searches for the **all** occurence of a pattern in a string and returns the matched strings as a B sequence.\n",
+ "It always starts to match at the beginning.\n",
+ "\n",
+ "Type: $STRING \\times STRING \\rightarrow seq(STRING)$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 155,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"234\"}),(2\\mapsto\\text{\"567\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"234\"),(2↦\"567\")}"
+ ]
+ },
+ "execution_count": 155,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_ALL(\"abcdef000234daf567\",\"([1-9])([0-9]*)\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 156,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"0\"}),(2\\mapsto\\text{\"0\"}),(3\\mapsto\\text{\"0\"}),(4\\mapsto\\text{\"2\"}),(5\\mapsto\\text{\"3\"}),(6\\mapsto\\text{\"4\"}),(7\\mapsto\\text{\"5\"}),(8\\mapsto\\text{\"6\"}),(9\\mapsto\\text{\"7\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"0\"),(2↦\"0\"),(3↦\"0\"),(4↦\"2\"),(5↦\"3\"),(6↦\"4\"),(7↦\"5\"),(8↦\"6\"),(9↦\"7\")}"
+ ]
+ },
+ "execution_count": 156,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_ALL(\"abcdef000234daf567\",\"([0-9])\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "If there is no match the function returns the empty set."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 157,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\emptyset$"
+ ],
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 157,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_ALL(\"0123\",\"[[:alpha:]]+\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### Unicode treatment\n",
+ "\n",
+ "The examples below show how ProB deals with Unicode strings and patterns.\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 158,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"a\"}),(2\\mapsto\\text{\"b\"}),(3\\mapsto\\text{\"c\"}),(4\\mapsto\\text{\"ä\"}),(5\\mapsto\\text{\"é\"}),(6\\mapsto\\text{\"à\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"a\"),(2↦\"b\"),(3↦\"c\"),(4↦\"ä\"),(5↦\"é\"),(6↦\"à\")}"
+ ]
+ },
+ "execution_count": 158,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_ALL(\"abc-äéà-123\",\"[[:alpha:]]\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 159,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"äéà\"}$"
+ ],
+ "text/plain": [
+ "\"äéà\""
+ ]
+ },
+ "execution_count": 159,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_STR(\"abc-äéà-123\",\"[äüéèà]+\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 160,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\renewcommand{\\emptyset}{\\mathord\\varnothing}\\mathit{rec}(\\mathit{length}\\in 3,\\mathit{position}\\in 5,\\mathit{string}\\in\\text{\"äéà\"},\\mathit{submatches}\\in\\emptyset)$"
+ ],
+ "text/plain": [
+ "rec(length∈3,position∈5,string∈\"äéà\",submatches∈∅)"
+ ]
+ },
+ "execution_count": 160,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH(\"abc-äéà-123\",1,\"[äüéèà]+\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 161,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"abc- ça -123\"}$"
+ ],
+ "text/plain": [
+ "\"abc- ça -123\""
+ ]
+ },
+ "execution_count": 161,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_REPLACE(\"abc-äéà-123\",\"[äüéèà]+\",\" ça \")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 162,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 162,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_MATCH(\"äbc\",\"...\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 163,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 163,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_MATCH(\"äbc\",\"abc\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 164,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 164,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_MATCH(\"äbc\",\"[[:alpha:]]{3}\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### Useful patterns\n",
+ "\n",
+ "Below we show few examples illustrating useful patterns:"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Here we use the ```\\w``` word operator:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 165,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"The\"}),(2\\mapsto\\text{\"quick\"}),(3\\mapsto\\text{\"fox\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"The\"),(2↦\"quick\"),(3↦\"fox\")}"
+ ]
+ },
+ "execution_count": 165,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_ALL(\"The quick fox.\",\"\\w+\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The ```\\d``` digit operator is also useful. Note that we have to escape the dot to avoid treating is the operator matching any non-newline character:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 166,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{rec}(\\mathit{length}\\in 10,\\mathit{position}\\in 1,\\mathit{string}\\in\\text{\"192.69.2.1\"},\\mathit{submatches}\\in\\{(1\\mapsto\\text{\"192\"}),(2\\mapsto\\text{\"69\"}),(3\\mapsto\\text{\"2\"}),(4\\mapsto\\text{\"1\"})\\})$"
+ ],
+ "text/plain": [
+ "rec(length∈10,position∈1,string∈\"192.69.2.1\",submatches∈{(1↦\"192\"),(2↦\"69\"),(3↦\"2\"),(4↦\"1\")})"
+ ]
+ },
+ "execution_count": 166,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH(\"192.69.2.1\",1,\"(\\d+)\\.(\\d+)\\.(\\d+)\\.(\\d+)\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "This example also uses the non-digit operator ```\\D```."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 167,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{rec}(\\mathit{length}\\in 10,\\mathit{position}\\in 1,\\mathit{string}\\in\\text{\"192.69.2.1\"},\\mathit{submatches}\\in\\{(1\\mapsto\\text{\"192\"}),(2\\mapsto\\text{\"69\"}),(3\\mapsto\\text{\"2\"}),(4\\mapsto\\text{\"1\"})\\})$"
+ ],
+ "text/plain": [
+ "rec(length∈10,position∈1,string∈\"192.69.2.1\",submatches∈{(1↦\"192\"),(2↦\"69\"),(3↦\"2\"),(4↦\"1\")})"
+ ]
+ },
+ "execution_count": 167,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH(\"192.69.2.1\",1,\"(\\d+)\\D(\\d+)\\D(\\d+)\\D(\\d+)\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Note that we can access the record fields directly and we can escape the ```\\``` if we wish (see section on escaping in B strings below):"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 168,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"192\"}),(2\\mapsto\\text{\"69\"}),(3\\mapsto\\text{\"2\"}),(4\\mapsto\\text{\"1\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"192\"),(2↦\"69\"),(3↦\"2\"),(4↦\"1\")}"
+ ]
+ },
+ "execution_count": 168,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH(\"192.69.2.1\",1,\"(\\\\d+)\\\\D(\\\\d+)\\\\D(\\\\d+)\\\\D(\\\\d+)\")'submatches"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Here we use the quantifier ```{min,max}``` to find sequences of 1 to 3 digits:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 169,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"102\"}),(2\\mapsto\\text{\"34\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"102\"),(2↦\"34\")}"
+ ]
+ },
+ "execution_count": 169,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_ALL(\"10234\",\"\\d{1,3}\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The next two examples use the ```\\s``` whitespace and not-whitespace ```\\S``` operators:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 170,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"weight\"}),(2\\mapsto\\text{\"is\"}),(3\\mapsto\\text{\"50\"}),(4\\mapsto\\text{\"and\"}),(5\\mapsto\\text{\"height\"}),(6\\mapsto\\text{\"is\"}),(7\\mapsto\\text{\"100\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"weight\"),(2↦\"is\"),(3↦\"50\"),(4↦\"and\"),(5↦\"height\"),(6↦\"is\"),(7↦\"100\")}"
+ ]
+ },
+ "execution_count": 170,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_ALL(\"weight is 50 and height is 100\",\"\\S+\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 171,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\" is\"}),(2\\mapsto\\text{\" 50\"}),(3\\mapsto\\text{\" and\"}),(4\\mapsto\\text{\" height\"}),(5\\mapsto\\text{\" is\"}),(6\\mapsto\\text{\" 100\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\" is\"),(2↦\" 50\"),(3↦\" and\"),(4↦\" height\"),(5↦\" is\"),(6↦\" 100\")}"
+ ]
+ },
+ "execution_count": 171,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_ALL(\"weight is 50 and height is 100\",\"\\s+\\S+\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "#### Lookaheads\n",
+ "\n",
+ "These examples use positive lookahead operator ```(?=subpattern)``` and the negative lookahead operator ```(?!subpattern)``` respectively:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 172,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"hi\"}$"
+ ],
+ "text/plain": [
+ "\"hi\""
+ ]
+ },
+ "execution_count": 172,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH(\"abc-defg-hi:jkl\",1,\"[[:alpha:]]+(?=:)\")'string"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 173,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"hi\"}$"
+ ],
+ "text/plain": [
+ "\"hi\""
+ ]
+ },
+ "execution_count": 173,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH(\"abc-defg-hi:jkl\",1,\"[[:alpha:]]+(?![-a-z])\")'string"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Note that lookbehinds (such as ```(?<=:)```) are currently not supported by ProB:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 174,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":eval: NOT-WELL-DEFINED: \n### Exception occurred while calling external function: 'REGEX_SEARCH':regex_exception('One of *?+{ was not preceded by a valid regular expression.')\n ### File: /Users/Shared/Uni/SHK/ProB2/prob_prolog/stdlib/LibraryRegex.def\n ### Line: 28, Column: 1 until 88\n ### within: DEFINITION call of REGEX_SEARCH at Line: 1 Column: 0 until Line: 1 Column: 54\n\n",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:eval: NOT-WELL-DEFINED: \u001b[0m",
+ "\u001b[1m\u001b[31m### Exception occurred while calling external function: 'REGEX_SEARCH':regex_exception('One of *?+{ was not preceded by a valid regular expression.')\u001b[0m",
+ "\u001b[1m\u001b[31m ### File: /Users/Shared/Uni/SHK/ProB2/prob_prolog/stdlib/LibraryRegex.def\u001b[0m",
+ "\u001b[1m\u001b[31m ### Line: 28, Column: 1 until 88\u001b[0m",
+ "\u001b[1m\u001b[31m ### within: DEFINITION call of REGEX_SEARCH at Line: 1 Column: 0 until Line: 1 Column: 54\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH(\"abc-defg-hi:jkl\",1,\"[[:alpha:]]+(?<=:)\")'string"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Backreferences ```\\int``` are supported, to match the int-th subgroup:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 175,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"dede\"}$"
+ ],
+ "text/plain": [
+ "\"dede\""
+ ]
+ },
+ "execution_count": 175,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH(\"abc-dede-hi:jkl\",1,\"([[:alpha:]]+)\\1\")'string"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "#### Escaping in B Strings\n",
+ "\n",
+ "As regular expressions make heavy use of the backslash ```\\``` it is important to know how B strings deal with backslashes.\n",
+ "ProB supports two types of strings:\n",
+ "- single-line strings delimited using double quotation marks, e.g., ```\"abc\"```\n",
+ "- multi-line strings delimited using three single quogtation marks. ```'''abc'''```\n",
+ "\n",
+ "Inside both types of strings the following escape sequences using the backslash are recognised:\n",
+ "\n",
+ "- ```\\n``` stands simply for newline\n",
+ "- ```\\t``` stands simply for tab\n",
+ "- ```\\r``` stands for carriage return\n",
+ "\n",
+ "\n",
+ "- ```\\\"``` stands simply for ```\"``` (to be able to use quotes in single-line strings)\n",
+ "- ```\\'``` stands simply for ```'``` (to be able to use quotes in multi-line strings)\n",
+ "- ```\\\\``` stands simply for ```\\``` (to be able to use backslash when preceding any of the above symbols)\n",
+ "\n",
+ "In all other contexts, i.e., for any value of ```c``` different from ```n,t,r,\",',\\```, the sequence ```\\c``` simply stands for ```\\c``` (i.e., the backslash remains unchanged in the string).\n",
+ "\n",
+ "The following examples illustrate the above."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 176,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$1$"
+ ],
+ "text/plain": [
+ "1"
+ ]
+ },
+ "execution_count": 176,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_LENGTH(\"\\\"\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 177,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$2$"
+ ],
+ "text/plain": [
+ "2"
+ ]
+ },
+ "execution_count": 177,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_LENGTH(\"\\\\\\\"\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 178,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$2$"
+ ],
+ "text/plain": [
+ "2"
+ ]
+ },
+ "execution_count": 178,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_LENGTH(\"\\a\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 179,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$2$"
+ ],
+ "text/plain": [
+ "2"
+ ]
+ },
+ "execution_count": 179,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_LENGTH(\"\\\\a\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 180,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 180,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "\"\\a\" = \"\\\\a\""
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 181,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 181,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "\"\\n\" = \"\\\\n\""
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 182,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"\\\\\\\"\"}$"
+ ],
+ "text/plain": [
+ "\"\\\\\\\"\""
+ ]
+ },
+ "execution_count": 182,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "\"\\\\\\\"\""
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Note that the previous result thus contains two characters:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 183,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"\\\\\"}),(2\\mapsto\\text{\"\\\"\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"\\\\\"),(2↦\"\\\"\")}"
+ ]
+ },
+ "execution_count": 183,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "STRING_CHARS(\"\\\\\\\"\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 184,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"\\a\"}$"
+ ],
+ "text/plain": [
+ "\"\\a\""
+ ]
+ },
+ "execution_count": 184,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "\"\\a\""
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 185,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"\\\\\"}$"
+ ],
+ "text/plain": [
+ "\"\\\\\""
+ ]
+ },
+ "execution_count": 185,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "\"\\\\\""
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 186,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"(\\d+)\\D(\\d+)\\D(\\d+)\\D(\\d+)\"}$"
+ ],
+ "text/plain": [
+ "\"(\\d+)\\D(\\d+)\\D(\\d+)\\D(\\d+)\""
+ ]
+ },
+ "execution_count": 186,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "\"(\\d+)\\D(\\d+)\\D(\\d+)\\D(\\d+)\""
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 187,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"\\b\"}$"
+ ],
+ "text/plain": [
+ "\"\\b\""
+ ]
+ },
+ "execution_count": 187,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "\"\\b\""
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## LibraryProB\n",
+ "\n",
+ "This library provides various facilities which are very specific to ProB.\n",
+ "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n",
+ "\n",
+ "`DEFINITIONS \"LibraryProB.def\"`\n",
+ "\n",
+ "The file `LibraryProB.def` is bundled with ProB and can be found in the `stdlib` folder."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 188,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Jupyter_LibraryStrings"
+ ]
+ },
+ "execution_count": 188,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Jupyter_LibraryStrings\n",
+ "DEFINITIONS \"LibraryProB.def\"\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "With ```ASSERT_EXPR``` you can check assertions within expressions.\n",
+ "\n",
+ "Type: $BOOL \\times STRING \\times \\tau \\rightarrow \\tau$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 189,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$4$"
+ ],
+ "text/plain": [
+ "4"
+ ]
+ },
+ "execution_count": 189,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "1+ASSERT_EXPR(bool(2>1),\"err\",3)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "With ```ASSERT_TRUE``` you can check assertions within predicates.\n",
+ "\n",
+ "Signature: $BOOL \\times STRING \\times \\tau$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 190,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 190,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "ASSERT_TRUE(bool(2>1),\"err\") & 2>1"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 191,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":eval: UNKNOWN (FALSE with enumeration warning)",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:eval: UNKNOWN (FALSE with enumeration warning)\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ "x=0 & res=ASSERT_EXPR(bool(x>0),\"arg not positive\",10+x)"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The function FORCE forces evaluation of symbolic set representations.\n",
+ "\n",
+ "Type: $POW(\\tau) \\rightarrow POW(\\tau)$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 192,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56,58,60,62,64,66,68,70,72,74,76,78,80,82,84,86,88,90,92,94,96,98,100\\}$"
+ ],
+ "text/plain": [
+ "{2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56,58,60,62,64,66,68,70,72,74,76,78,80,82,84,86,88,90,92,94,96,98,100}"
+ ]
+ },
+ "execution_count": 192,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "FORCE( /*@symbolic */ { x | x:1..100 & x mod 2 = 0 } )"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The function COPY can be used as an \"enumeration barrier\"; the value is copied only once it is fully known.\n",
+ "\n",
+ "Type: $\\tau \\rightarrow \\tau$"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 193,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$\n",
+ "\n",
+ "**Solution:**\n",
+ "* $\\mathit{x} = 3$\n",
+ "* $\\mathit{y} = 3$"
+ ],
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tx = 3\n",
+ "\ty = 3"
+ ]
+ },
+ "execution_count": 193,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "x:1..3 & y=COPY(x) & 9/y=3"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### Version\n",
+ "This documentation was generated with the following version of ProB:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 194,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "ProB CLI: 1.9.3-nightly (50333f1779dcae2a9e6d1b2aa95a23678821f851)\n",
+ "ProB 2: 4.0.0-SNAPSHOT (1d61b6ea7ef1b2e38a6b6045dbb0e81bcb6d8423)"
+ ]
+ },
+ "execution_count": 194,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":version"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
diff --git a/images/B_CallButtonDown_Off.gif b/manual/images/B_CallButtonDown_Off.gif
similarity index 100%
rename from images/B_CallButtonDown_Off.gif
rename to manual/images/B_CallButtonDown_Off.gif
diff --git a/images/B_CallButtonDown_On.gif b/manual/images/B_CallButtonDown_On.gif
similarity index 100%
rename from images/B_CallButtonDown_On.gif
rename to manual/images/B_CallButtonDown_On.gif
diff --git a/images/B_CallButtonOff.gif b/manual/images/B_CallButtonOff.gif
similarity index 100%
rename from images/B_CallButtonOff.gif
rename to manual/images/B_CallButtonOff.gif
diff --git a/images/B_CallButtonOn.gif b/manual/images/B_CallButtonOn.gif
similarity index 100%
rename from images/B_CallButtonOn.gif
rename to manual/images/B_CallButtonOn.gif
diff --git a/images/B_CallButtonUp_Off.gif b/manual/images/B_CallButtonUp_Off.gif
similarity index 100%
rename from images/B_CallButtonUp_Off.gif
rename to manual/images/B_CallButtonUp_Off.gif
diff --git a/images/B_CallButtonUp_On.gif b/manual/images/B_CallButtonUp_On.gif
similarity index 100%
rename from images/B_CallButtonUp_On.gif
rename to manual/images/B_CallButtonUp_On.gif
diff --git a/images/B_CallButton_DownArrow_On.gif b/manual/images/B_CallButton_DownArrow_On.gif
similarity index 100%
rename from images/B_CallButton_DownArrow_On.gif
rename to manual/images/B_CallButton_DownArrow_On.gif
diff --git a/images/B_CallButton_UpArrow_On.gif b/manual/images/B_CallButton_UpArrow_On.gif
similarity index 100%
rename from images/B_CallButton_UpArrow_On.gif
rename to manual/images/B_CallButton_UpArrow_On.gif
diff --git a/images/B_CallButton_UpDownArrows_Off.gif b/manual/images/B_CallButton_UpDownArrows_Off.gif
similarity index 100%
rename from images/B_CallButton_UpDownArrows_Off.gif
rename to manual/images/B_CallButton_UpDownArrows_Off.gif
diff --git a/images/B_DownButton_On.gif b/manual/images/B_DownButton_On.gif
similarity index 100%
rename from images/B_DownButton_On.gif
rename to manual/images/B_DownButton_On.gif
diff --git a/images/B_LiftClosed.gif b/manual/images/B_LiftClosed.gif
similarity index 100%
rename from images/B_LiftClosed.gif
rename to manual/images/B_LiftClosed.gif
diff --git a/images/B_LiftOpen.gif b/manual/images/B_LiftOpen.gif
similarity index 100%
rename from images/B_LiftOpen.gif
rename to manual/images/B_LiftOpen.gif
diff --git a/images/B_UpButton_On.gif b/manual/images/B_UpButton_On.gif
similarity index 100%
rename from images/B_UpButton_On.gif
rename to manual/images/B_UpButton_On.gif
diff --git a/images/B_UpDownButtons_Off.gif b/manual/images/B_UpDownButtons_Off.gif
similarity index 100%
rename from images/B_UpDownButtons_Off.gif
rename to manual/images/B_UpDownButtons_Off.gif
diff --git a/images/B_UpDownButtons_On.gif b/manual/images/B_UpDownButtons_On.gif
similarity index 100%
rename from images/B_UpDownButtons_On.gif
rename to manual/images/B_UpDownButtons_On.gif
diff --git a/images/B_down_arrow.gif b/manual/images/B_down_arrow.gif
similarity index 100%
rename from images/B_down_arrow.gif
rename to manual/images/B_down_arrow.gif
diff --git a/images/B_down_arrow_off.gif b/manual/images/B_down_arrow_off.gif
similarity index 100%
rename from images/B_down_arrow_off.gif
rename to manual/images/B_down_arrow_off.gif
diff --git a/images/B_floor_1_off.gif b/manual/images/B_floor_1_off.gif
similarity index 100%
rename from images/B_floor_1_off.gif
rename to manual/images/B_floor_1_off.gif
diff --git a/images/B_floor_1_on.gif b/manual/images/B_floor_1_on.gif
similarity index 100%
rename from images/B_floor_1_on.gif
rename to manual/images/B_floor_1_on.gif
diff --git a/images/B_floor_2_off.gif b/manual/images/B_floor_2_off.gif
similarity index 100%
rename from images/B_floor_2_off.gif
rename to manual/images/B_floor_2_off.gif
diff --git a/images/B_floor_2_on.gif b/manual/images/B_floor_2_on.gif
similarity index 100%
rename from images/B_floor_2_on.gif
rename to manual/images/B_floor_2_on.gif
diff --git a/images/B_floor_3_off.gif b/manual/images/B_floor_3_off.gif
similarity index 100%
rename from images/B_floor_3_off.gif
rename to manual/images/B_floor_3_off.gif
diff --git a/images/B_floor_3_on.gif b/manual/images/B_floor_3_on.gif
similarity index 100%
rename from images/B_floor_3_on.gif
rename to manual/images/B_floor_3_on.gif
diff --git a/images/B_floor_E_off.gif b/manual/images/B_floor_E_off.gif
similarity index 100%
rename from images/B_floor_E_off.gif
rename to manual/images/B_floor_E_off.gif
diff --git a/images/B_floor_E_on.gif b/manual/images/B_floor_E_on.gif
similarity index 100%
rename from images/B_floor_E_on.gif
rename to manual/images/B_floor_E_on.gif
diff --git a/images/B_up_arrow.gif b/manual/images/B_up_arrow.gif
similarity index 100%
rename from images/B_up_arrow.gif
rename to manual/images/B_up_arrow.gif
diff --git a/images/B_up_arrow_off.gif b/manual/images/B_up_arrow_off.gif
similarity index 100%
rename from images/B_up_arrow_off.gif
rename to manual/images/B_up_arrow_off.gif
diff --git a/images/CallButtonOff.gif b/manual/images/CallButtonOff.gif
similarity index 100%
rename from images/CallButtonOff.gif
rename to manual/images/CallButtonOff.gif
diff --git a/images/CallButtonOn.gif b/manual/images/CallButtonOn.gif
similarity index 100%
rename from images/CallButtonOn.gif
rename to manual/images/CallButtonOn.gif
diff --git a/images/LiftClosed.gif b/manual/images/LiftClosed.gif
similarity index 100%
rename from images/LiftClosed.gif
rename to manual/images/LiftClosed.gif
diff --git a/images/LiftEmpty.gif b/manual/images/LiftEmpty.gif
similarity index 100%
rename from images/LiftEmpty.gif
rename to manual/images/LiftEmpty.gif
diff --git a/images/LiftOpen.gif b/manual/images/LiftOpen.gif
similarity index 100%
rename from images/LiftOpen.gif
rename to manual/images/LiftOpen.gif
diff --git a/images/down_arrow.gif b/manual/images/down_arrow.gif
similarity index 100%
rename from images/down_arrow.gif
rename to manual/images/down_arrow.gif
diff --git a/images/up_arrow.gif b/manual/images/up_arrow.gif
similarity index 100%
rename from images/up_arrow.gif
rename to manual/images/up_arrow.gif
diff --git a/Argumentation_Theory.ipynb b/mathematical/Argumentation_Theory.ipynb
similarity index 100%
rename from Argumentation_Theory.ipynb
rename to mathematical/Argumentation_Theory.ipynb
diff --git a/Euler_Problem.ipynb b/mathematical/Euler_Problem.ipynb
similarity index 100%
rename from Euler_Problem.ipynb
rename to mathematical/Euler_Problem.ipynb
diff --git a/Fibonacci_Numbers.ipynb b/mathematical/Fibonacci_Numbers.ipynb
similarity index 100%
rename from Fibonacci_Numbers.ipynb
rename to mathematical/Fibonacci_Numbers.ipynb
diff --git a/images/ProBRodinArgumentationState.png b/mathematical/images/ProBRodinArgumentationState.png
similarity index 100%
rename from images/ProBRodinArgumentationState.png
rename to mathematical/images/ProBRodinArgumentationState.png
diff --git a/resources/triangle_Euler67.def b/mathematical/resources/triangle_Euler67.def
similarity index 100%
rename from resources/triangle_Euler67.def
rename to mathematical/resources/triangle_Euler67.def
diff --git a/resources/triangle_Euler67.txt b/mathematical/resources/triangle_Euler67.txt
similarity index 100%
rename from resources/triangle_Euler67.txt
rename to mathematical/resources/triangle_Euler67.txt
diff --git a/Apples_and_Oranges.ipynb b/puzzles/Apples_and_Oranges.ipynb
similarity index 100%
rename from Apples_and_Oranges.ipynb
rename to puzzles/Apples_and_Oranges.ipynb
diff --git a/Bridges_Puzzle.ipynb b/puzzles/Bridges_Puzzle.ipynb
similarity index 100%
rename from Bridges_Puzzle.ipynb
rename to puzzles/Bridges_Puzzle.ipynb
diff --git a/Cheryls_Birthday.ipynb b/puzzles/Cheryls_Birthday.ipynb
similarity index 100%
rename from Cheryls_Birthday.ipynb
rename to puzzles/Cheryls_Birthday.ipynb
diff --git a/Die_Hard_Jugs.ipynb b/puzzles/Die_Hard_Jugs.ipynb
similarity index 100%
rename from Die_Hard_Jugs.ipynb
rename to puzzles/Die_Hard_Jugs.ipynb
diff --git a/Game_of_Life.ipynb b/puzzles/Game_of_Life.ipynb
similarity index 100%
rename from Game_of_Life.ipynb
rename to puzzles/Game_of_Life.ipynb
diff --git a/Gilbreath_Card_Trick.ipynb b/puzzles/Gilbreath_Card_Trick.ipynb
similarity index 100%
rename from Gilbreath_Card_Trick.ipynb
rename to puzzles/Gilbreath_Card_Trick.ipynb
diff --git a/N-Bishops.ipynb b/puzzles/N-Bishops.ipynb
similarity index 100%
rename from N-Bishops.ipynb
rename to puzzles/N-Bishops.ipynb
diff --git a/N-Queens.ipynb b/puzzles/N-Queens.ipynb
similarity index 100%
rename from N-Queens.ipynb
rename to puzzles/N-Queens.ipynb
diff --git a/Peaceable_Armies_of_Queens.ipynb b/puzzles/Peaceable_Armies_of_Queens.ipynb
similarity index 100%
rename from Peaceable_Armies_of_Queens.ipynb
rename to puzzles/Peaceable_Armies_of_Queens.ipynb
diff --git a/SEND-MORE-MONEY.ipynb b/puzzles/SEND-MORE-MONEY.ipynb
similarity index 100%
rename from SEND-MORE-MONEY.ipynb
rename to puzzles/SEND-MORE-MONEY.ipynb
diff --git a/images/ChessPieces/Chess_bdd45.gif b/puzzles/images/ChessPieces/Chess_bdd45.gif
similarity index 100%
rename from images/ChessPieces/Chess_bdd45.gif
rename to puzzles/images/ChessPieces/Chess_bdd45.gif
diff --git a/images/ChessPieces/Chess_bdl45.gif b/puzzles/images/ChessPieces/Chess_bdl45.gif
similarity index 100%
rename from images/ChessPieces/Chess_bdl45.gif
rename to puzzles/images/ChessPieces/Chess_bdl45.gif
diff --git a/images/ChessPieces/Chess_bld45.gif b/puzzles/images/ChessPieces/Chess_bld45.gif
similarity index 100%
rename from images/ChessPieces/Chess_bld45.gif
rename to puzzles/images/ChessPieces/Chess_bld45.gif
diff --git a/images/ChessPieces/Chess_bll45.gif b/puzzles/images/ChessPieces/Chess_bll45.gif
similarity index 100%
rename from images/ChessPieces/Chess_bll45.gif
rename to puzzles/images/ChessPieces/Chess_bll45.gif
diff --git a/images/ChessPieces/Chess_emptyXg45.gif b/puzzles/images/ChessPieces/Chess_emptyXg45.gif
similarity index 100%
rename from images/ChessPieces/Chess_emptyXg45.gif
rename to puzzles/images/ChessPieces/Chess_emptyXg45.gif
diff --git a/images/ChessPieces/Chess_emptyd45.gif b/puzzles/images/ChessPieces/Chess_emptyd45.gif
similarity index 100%
rename from images/ChessPieces/Chess_emptyd45.gif
rename to puzzles/images/ChessPieces/Chess_emptyd45.gif
diff --git a/images/ChessPieces/Chess_emptyg45.gif b/puzzles/images/ChessPieces/Chess_emptyg45.gif
similarity index 100%
rename from images/ChessPieces/Chess_emptyg45.gif
rename to puzzles/images/ChessPieces/Chess_emptyg45.gif
diff --git a/images/ChessPieces/Chess_emptyl45.gif b/puzzles/images/ChessPieces/Chess_emptyl45.gif
similarity index 100%
rename from images/ChessPieces/Chess_emptyl45.gif
rename to puzzles/images/ChessPieces/Chess_emptyl45.gif
diff --git a/images/ChessPieces/Chess_kdd45.gif b/puzzles/images/ChessPieces/Chess_kdd45.gif
similarity index 100%
rename from images/ChessPieces/Chess_kdd45.gif
rename to puzzles/images/ChessPieces/Chess_kdd45.gif
diff --git a/images/ChessPieces/Chess_kdl45.gif b/puzzles/images/ChessPieces/Chess_kdl45.gif
similarity index 100%
rename from images/ChessPieces/Chess_kdl45.gif
rename to puzzles/images/ChessPieces/Chess_kdl45.gif
diff --git a/images/ChessPieces/Chess_kld45.gif b/puzzles/images/ChessPieces/Chess_kld45.gif
similarity index 100%
rename from images/ChessPieces/Chess_kld45.gif
rename to puzzles/images/ChessPieces/Chess_kld45.gif
diff --git a/images/ChessPieces/Chess_kll45.gif b/puzzles/images/ChessPieces/Chess_kll45.gif
similarity index 100%
rename from images/ChessPieces/Chess_kll45.gif
rename to puzzles/images/ChessPieces/Chess_kll45.gif
diff --git a/images/ChessPieces/Chess_krd45.gif b/puzzles/images/ChessPieces/Chess_krd45.gif
similarity index 100%
rename from images/ChessPieces/Chess_krd45.gif
rename to puzzles/images/ChessPieces/Chess_krd45.gif
diff --git a/images/ChessPieces/Chess_krl45.gif b/puzzles/images/ChessPieces/Chess_krl45.gif
similarity index 100%
rename from images/ChessPieces/Chess_krl45.gif
rename to puzzles/images/ChessPieces/Chess_krl45.gif
diff --git a/images/ChessPieces/Chess_krt45.gif b/puzzles/images/ChessPieces/Chess_krt45.gif
similarity index 100%
rename from images/ChessPieces/Chess_krt45.gif
rename to puzzles/images/ChessPieces/Chess_krt45.gif
diff --git a/images/ChessPieces/Chess_ndd45.gif b/puzzles/images/ChessPieces/Chess_ndd45.gif
similarity index 100%
rename from images/ChessPieces/Chess_ndd45.gif
rename to puzzles/images/ChessPieces/Chess_ndd45.gif
diff --git a/images/ChessPieces/Chess_ndl45.gif b/puzzles/images/ChessPieces/Chess_ndl45.gif
similarity index 100%
rename from images/ChessPieces/Chess_ndl45.gif
rename to puzzles/images/ChessPieces/Chess_ndl45.gif
diff --git a/images/ChessPieces/Chess_nld45.gif b/puzzles/images/ChessPieces/Chess_nld45.gif
similarity index 100%
rename from images/ChessPieces/Chess_nld45.gif
rename to puzzles/images/ChessPieces/Chess_nld45.gif
diff --git a/images/ChessPieces/Chess_nll45.gif b/puzzles/images/ChessPieces/Chess_nll45.gif
similarity index 100%
rename from images/ChessPieces/Chess_nll45.gif
rename to puzzles/images/ChessPieces/Chess_nll45.gif
diff --git a/images/ChessPieces/Chess_pdd45.gif b/puzzles/images/ChessPieces/Chess_pdd45.gif
similarity index 100%
rename from images/ChessPieces/Chess_pdd45.gif
rename to puzzles/images/ChessPieces/Chess_pdd45.gif
diff --git a/images/ChessPieces/Chess_pdl45.gif b/puzzles/images/ChessPieces/Chess_pdl45.gif
similarity index 100%
rename from images/ChessPieces/Chess_pdl45.gif
rename to puzzles/images/ChessPieces/Chess_pdl45.gif
diff --git a/images/ChessPieces/Chess_pld45.gif b/puzzles/images/ChessPieces/Chess_pld45.gif
similarity index 100%
rename from images/ChessPieces/Chess_pld45.gif
rename to puzzles/images/ChessPieces/Chess_pld45.gif
diff --git a/images/ChessPieces/Chess_pll45.gif b/puzzles/images/ChessPieces/Chess_pll45.gif
similarity index 100%
rename from images/ChessPieces/Chess_pll45.gif
rename to puzzles/images/ChessPieces/Chess_pll45.gif
diff --git a/images/ChessPieces/Chess_qdd45.gif b/puzzles/images/ChessPieces/Chess_qdd45.gif
similarity index 100%
rename from images/ChessPieces/Chess_qdd45.gif
rename to puzzles/images/ChessPieces/Chess_qdd45.gif
diff --git a/images/ChessPieces/Chess_qdl45.gif b/puzzles/images/ChessPieces/Chess_qdl45.gif
similarity index 100%
rename from images/ChessPieces/Chess_qdl45.gif
rename to puzzles/images/ChessPieces/Chess_qdl45.gif
diff --git a/images/ChessPieces/Chess_qgg45.gif b/puzzles/images/ChessPieces/Chess_qgg45.gif
similarity index 100%
rename from images/ChessPieces/Chess_qgg45.gif
rename to puzzles/images/ChessPieces/Chess_qgg45.gif
diff --git a/images/ChessPieces/Chess_qgt45.gif b/puzzles/images/ChessPieces/Chess_qgt45.gif
similarity index 100%
rename from images/ChessPieces/Chess_qgt45.gif
rename to puzzles/images/ChessPieces/Chess_qgt45.gif
diff --git a/images/ChessPieces/Chess_qld45.gif b/puzzles/images/ChessPieces/Chess_qld45.gif
similarity index 100%
rename from images/ChessPieces/Chess_qld45.gif
rename to puzzles/images/ChessPieces/Chess_qld45.gif
diff --git a/images/ChessPieces/Chess_qll45.gif b/puzzles/images/ChessPieces/Chess_qll45.gif
similarity index 100%
rename from images/ChessPieces/Chess_qll45.gif
rename to puzzles/images/ChessPieces/Chess_qll45.gif
diff --git a/images/ChessPieces/Chess_qrg45.gif b/puzzles/images/ChessPieces/Chess_qrg45.gif
similarity index 100%
rename from images/ChessPieces/Chess_qrg45.gif
rename to puzzles/images/ChessPieces/Chess_qrg45.gif
diff --git a/images/ChessPieces/Chess_qrt45.gif b/puzzles/images/ChessPieces/Chess_qrt45.gif
similarity index 100%
rename from images/ChessPieces/Chess_qrt45.gif
rename to puzzles/images/ChessPieces/Chess_qrt45.gif
diff --git a/images/ChessPieces/Chess_qyt45.gif b/puzzles/images/ChessPieces/Chess_qyt45.gif
similarity index 100%
rename from images/ChessPieces/Chess_qyt45.gif
rename to puzzles/images/ChessPieces/Chess_qyt45.gif
diff --git a/images/ChessPieces/Chess_rdd45.gif b/puzzles/images/ChessPieces/Chess_rdd45.gif
similarity index 100%
rename from images/ChessPieces/Chess_rdd45.gif
rename to puzzles/images/ChessPieces/Chess_rdd45.gif
diff --git a/images/ChessPieces/Chess_rdl45.gif b/puzzles/images/ChessPieces/Chess_rdl45.gif
similarity index 100%
rename from images/ChessPieces/Chess_rdl45.gif
rename to puzzles/images/ChessPieces/Chess_rdl45.gif
diff --git a/images/ChessPieces/Chess_rld45.gif b/puzzles/images/ChessPieces/Chess_rld45.gif
similarity index 100%
rename from images/ChessPieces/Chess_rld45.gif
rename to puzzles/images/ChessPieces/Chess_rld45.gif
diff --git a/images/ChessPieces/Chess_rll45.gif b/puzzles/images/ChessPieces/Chess_rll45.gif
similarity index 100%
rename from images/ChessPieces/Chess_rll45.gif
rename to puzzles/images/ChessPieces/Chess_rll45.gif
diff --git a/images/ChessPieces/Licence.txt b/puzzles/images/ChessPieces/Licence.txt
similarity index 100%
rename from images/ChessPieces/Licence.txt
rename to puzzles/images/ChessPieces/Licence.txt
diff --git a/images/Empty.gif b/puzzles/images/Empty.gif
similarity index 100%
rename from images/Empty.gif
rename to puzzles/images/Empty.gif
diff --git a/images/Filled.gif b/puzzles/images/Filled.gif
similarity index 100%
rename from images/Filled.gif
rename to puzzles/images/Filled.gif
diff --git a/images/French_suits_Club.gif b/puzzles/images/French_suits_Club.gif
similarity index 100%
rename from images/French_suits_Club.gif
rename to puzzles/images/French_suits_Club.gif
diff --git a/images/French_suits_Diamond.gif b/puzzles/images/French_suits_Diamond.gif
similarity index 100%
rename from images/French_suits_Diamond.gif
rename to puzzles/images/French_suits_Diamond.gif
diff --git a/images/French_suits_Heart.gif b/puzzles/images/French_suits_Heart.gif
similarity index 100%
rename from images/French_suits_Heart.gif
rename to puzzles/images/French_suits_Heart.gif
diff --git a/images/French_suits_Spade.gif b/puzzles/images/French_suits_Spade.gif
similarity index 100%
rename from images/French_suits_Spade.gif
rename to puzzles/images/French_suits_Spade.gif
diff --git a/images/ProB_ApplesOranges_Sol.png b/puzzles/images/ProB_ApplesOranges_Sol.png
similarity index 100%
rename from images/ProB_ApplesOranges_Sol.png
rename to puzzles/images/ProB_ApplesOranges_Sol.png
diff --git a/images/ProB_ApplesOranges_Table.png b/puzzles/images/ProB_ApplesOranges_Table.png
similarity index 100%
rename from images/ProB_ApplesOranges_Table.png
rename to puzzles/images/ProB_ApplesOranges_Table.png
diff --git a/images/Void.gif b/puzzles/images/Void.gif
similarity index 100%
rename from images/Void.gif
rename to puzzles/images/Void.gif
diff --git a/images/sm_empty_box.gif b/puzzles/images/sm_empty_box.gif
similarity index 100%
rename from images/sm_empty_box.gif
rename to puzzles/images/sm_empty_box.gif
diff --git a/images/sm_gray_box.gif b/puzzles/images/sm_gray_box.gif
similarity index 100%
rename from images/sm_gray_box.gif
rename to puzzles/images/sm_gray_box.gif
diff --git a/images/sm_queen_black.gif b/puzzles/images/sm_queen_black.gif
similarity index 100%
rename from images/sm_queen_black.gif
rename to puzzles/images/sm_queen_black.gif
diff --git a/images/sm_queen_white.gif b/puzzles/images/sm_queen_white.gif
similarity index 100%
rename from images/sm_queen_white.gif
rename to puzzles/images/sm_queen_white.gif