add new external functions

a6b4a72a · Michael Leuschel · e54da55c · a6b4a72a
Commit a6b4a72a authored Jan 9, 2020 by Michael Leuschel
--- a/notebooks/manual/ExternalFunctions.ipynb
+++ b/notebooks/manual/ExternalFunctions.ipynb
@@ -23,7 +23,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 197,
+   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
@@ -32,7 +32,7 @@
       "Loaded machine: Jupyter_LibraryStrings"
      ]
     },
-     "execution_count": 197,
+     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -536,6 +536,154 @@
    "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": 2,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\text{\"ABC\"}$"
+      ],
+      "text/plain": [
+       "\"ABC\""
+      ]
+     },
+     "execution_count": 2,
+     "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": 3,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\text{\"ABC_ABC\"}$"
+      ],
+      "text/plain": [
+       "\"ABC_ABC\""
+      ]
+     },
+     "execution_count": 3,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_TO_UPPER(\"abc_ABC\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\text{\"AZ-AZ-09-AAOU-AO\"}$"
+      ],
+      "text/plain": [
+       "\"AZ-AZ-09-AAOU-AO\""
+      ]
+     },
+     "execution_count": 7,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_TO_UPPER(\"az-AZ-09-äàöù-ÄÖ\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\text{\"\"}$"
+      ],
+      "text/plain": [
+       "\"\""
+      ]
+     },
+     "execution_count": 5,
+     "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": 2,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\text{\"az-az-09-aaou-ao\"}$"
+      ],
+      "text/plain": [
+       "\"az-az-09-aaou-ao\""
+      ]
+     },
+     "execution_count": 2,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "STRING_TO_LOWER(\"az-AZ-09-äàöù-ÄÖ\")"
+   ]
+  },
  {
   "cell_type": "markdown",
   "metadata": {},

 %% Cell type:markdown id: tags:
 # External Functions
 ## LibraryStrings
 In pure B there are only two built-in operators on strings: equality $=$ and inequality $\neq$.
 This library provides several string manipulation functions, and assumes that STRINGS are
 sequences of unicode characters (in UTF-8 encoding).
 You can obtain the definitions below by putting the following into your DEFINITIONS clause:
 `DEFINITIONS "LibraryStrings.def"`
 The file `LibraryStrings.def` is bundled with ProB and can be found in the `stdlib` folder.
 You can also include the machine `LibraryStrings.mch` instead of the definition file;
 the machine defines some of the functions below as proper B functions (i.e., functions
 for which you can compute the domain and use constructs such as
 relational image).
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE Jupyter_LibraryStrings
 DEFINITIONS "LibraryStrings.def"
 END
 ```
 %% Output
    Loaded machine: Jupyter_LibraryStrings
 %% Cell type:markdown id: tags:
 ### STRING_APPEND
 This external function takes two strings and concatenates them.
 Type: $STRING \times STRING \rightarrow STRING $.
 %% Cell type:code id: tags:
 ``` prob
 STRING_APPEND("abc","abc")
 ```
 %% Output
    $\text{"abcabc"}$
    "abcabc"
 %% Cell type:code id: tags:
 ``` prob
 STRING_APPEND("abc","")
 ```
 %% Output
    $\text{"abc"}$
    "abc"
 %% Cell type:markdown id: tags:
 ### STRING_LENGTH
 This external function takes a string and returns the length.
 Type: $STRING \rightarrow INTEGER$.
 %% Cell type:code id: tags:
 ``` prob
 STRING_LENGTH("abc")
 ```
 %% Output
    $3$
    3
 %% Cell type:code id: tags:
 ``` prob
 STRING_LENGTH("")
 ```
 %% Output
    $0$
    0
 %% Cell type:markdown id: tags:
 ### STRING_SPLIT
 This external function takes two strings and separates the first string
 according to the separator specified by the second string.
 Type: $STRING \times STRING \rightarrow \mathit{seq}(STRING) $.
 %% Cell type:code id: tags:
 ``` prob
 STRING_SPLIT("filename.ext",".")
 ```
 %% Output
    $\{(1\mapsto\text{"filename"}),(2\mapsto\text{"ext"})\}$
    {(1↦"filename"),(2↦"ext")}
 %% Cell type:code id: tags:
 ``` prob
 STRING_SPLIT("filename.ext","/")
 ```
 %% Output
    $\{(1\mapsto\text{"filename.ext"})\}$
    {(1↦"filename.ext")}
 %% Cell type:code id: tags:
 ``` prob
 STRING_SPLIT("usr/local/lib","/")
 ```
 %% Output
    $[\text{"usr"},\text{"local"},\text{"lib"}]$
    ["usr","local","lib"]
 %% Cell type:code id: tags:
 ``` prob
 STRING_SPLIT("",".")
 ```
 %% Output
    $\{(1\mapsto\text{""})\}$
    {(1↦"")}
 %% Cell type:markdown id: tags:
 I am not sure the following result makes sense, maybe a sequence of all characters is more appropriate?
 %% Cell type:code id: tags:
 ``` prob
 STRING_SPLIT("usr/local/lib","")
 ```
 %% Output
    $\{(1\mapsto\text{"usr/local/lib"})\}$
    {(1↦"usr/local/lib")}
 %% Cell type:code id: tags:
 ``` prob
 STRING_SPLIT("usr/local/lib","cal")
 ```
 %% Output
    $\{(1\mapsto\text{"usr/lo"}),(2\mapsto\text{"/lib"})\}$
    {(1↦"usr/lo"),(2↦"/lib")}
 %% Cell type:markdown id: tags:
 ### STRING_JOIN
 This external function takes a sequence of strings and a separator string
 and joins the strings together inserting the separators as often as needed.
 It is the inverse of the `STRING_SPLIT` function.
 Type: $\mathit{seq}(STRING) \times STRING \rightarrow STRING $.
 %% Cell type:code id: tags:
 ``` prob
 STRING_JOIN(["usr","local","lib"],"/")
 ```
 %% Output
    $\text{"usr/local/lib"}$
    "usr/local/lib"
 %% Cell type:code id: tags:
 ``` prob
 STRING_JOIN(["usr/lo","/lib"],"cal")
 ```
 %% Output
    $\text{"usr/local/lib"}$
    "usr/local/lib"
 %% Cell type:code id: tags:
 ``` prob
 STRING_JOIN(["usr/local/lib"],"")
 ```
 %% Output
    $\text{"usr/local/lib"}$
    "usr/local/lib"
 %% Cell type:markdown id: tags:
 ### STRING_CHARS
 This external function takes a strings splits it into a sequence
 of the individual characters. Each character is represented by a string.
 Type: $STRING \rightarrow \mathit{seq}(STRING) $.
 %% Cell type:code id: tags:
 ``` prob
 STRING_CHARS("")
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
    ∅
 %% Cell type:code id: tags:
 ``` prob
 STRING_CHARS("abc")
 ```
 %% Output
    $[\text{"a"},\text{"b"},\text{"c"}]$
    ["a","b","c"]
 %% Cell type:code id: tags:
 ``` prob
 STRING_JOIN(STRING_CHARS("abc"),".")
 ```
 %% Output
    $\text{"a.b.c"}$
    "a.b.c"
 %% Cell type:markdown id: tags:
 ### STRING_CODES
 This external function takes a strings splits it into a sequence
 of the individual characters. Each character is represented by a natural number
 (the ASCII or Unicode representation of the character).
 Type: $STRING \rightarrow \mathit{seq}(INTEGER) $.
 %% Cell type:code id: tags:
 ``` prob
 STRING_CODES("")
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
    ∅
 %% Cell type:code id: tags:
 ``` prob
 STRING_CODES("AZ az 09")
 ```
 %% Output
    $[65,90,32,97,122,32,48,57]$
    [65,90,32,97,122,32,48,57]
 %% Cell type:markdown id: tags:
+### CODES_TO_STRING
+This external function is the inverse of the ```STRING_CODES``` function above.
+Type: $\mathit{seq}(INTEGER)\rightarrow  STRING$.
+%% Cell type:code id: tags:
+``` prob
+CODES_TO_STRING([65,66,67])
+```
+%% Output
+    $\text{"ABC"}$
+    "ABC"
+%% Cell type:markdown id: tags:
+### STRING_TO_UPPER
+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).
+Type: $STRING \rightarrow STRING $.
+%% Cell type:code id: tags:
+``` prob
+STRING_TO_UPPER("abc_ABC")
+```
+%% Output
+    $\text{"ABC_ABC"}$
+    "ABC_ABC"
+%% Cell type:code id: tags:
+``` prob
+STRING_TO_UPPER("az-AZ-09-äàöù-ÄÖ")
+```
+%% Output
+    $\text{"AZ-AZ-09-AAOU-AO"}$
+    "AZ-AZ-09-AAOU-AO"
+%% Cell type:code id: tags:
+``` prob
+STRING_TO_UPPER("")
+```
+%% Output
+    $\text{""}$
+    ""
+%% Cell type:markdown id: tags:
+### STRING_TO_LOWER
+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).
+Type: $STRING \rightarrow STRING $.
+%% Cell type:code id: tags:
+``` prob
+STRING_TO_LOWER("az-AZ-09-äàöù-ÄÖ")
+```
+%% Output
+    $\text{"az-az-09-aaou-ao"}$
+    "az-az-09-aaou-ao"
+%% Cell type:markdown id: tags:
 ### SUB_STRING
 This external function takes a strings a position and a sequence and produces a corresponding substring.
 The numbering starts at 1 and the position must be at least 1, but can extend beyond the end of the string.
 Type: $STRING \times INTEGER \times INTEGER \rightarrow STRING $.
 %% Cell type:code id: tags:
 ``` prob
 SUB_STRING("abcdefg",1,3)
 ```
 %% Output
    $\text{"abc"}$
    "abc"
 %% Cell type:code id: tags:
 ``` prob
 SUB_STRING("abcdefg",1,100)
 ```
 %% Output
    $\text{"abcdefg"}$
    "abcdefg"
 %% Cell type:code id: tags:
 ``` prob
 SUB_STRING("abcdefg",4,2)
 ```
 %% Output
    $\text{"de"}$
    "de"
 %% Cell type:code id: tags:
 ``` prob
 SUB_STRING("abcdefg",3,0)
 ```
 %% Output
    $\text{""}$
    ""
 %% Cell type:code id: tags:
 ``` prob
 SUB_STRING("abcdefg",11,3)
 ```
 %% Output
    $\text{""}$
    ""
 %% Cell type:markdown id: tags:
 ### STRING_IS_INT
 %% Cell type:markdown id: tags:
 This external predicate takes a string and is true if the string represents an integer.
 Type: $STRING $.
 %% Cell type:code id: tags:
 ``` prob
 STRING_IS_INT("1204")
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 STRING_IS_INT("-1204")
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 STRING_IS_INT(" - 1204")
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 STRING_IS_INT("1.1")
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:code id: tags:
 ``` prob
 STRING_IS_INT("1.0")
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:code id: tags:
 ``` prob
 STRING_IS_INT("a")
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:code id: tags:
 ``` prob
 STRING_IS_INT("1000000000000000000000000000")
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 STRING_IS_INT("-00001")
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 STRING_IS_INT("00002")
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:markdown id: tags:
 ### STRING_TO_INT
 This external function takes a string and converts it into an integer.
 An error is raised if this cannot be done.
 It is safer to first check with `STRING_IS_INT` whether the conversion can be done.
 Type: $STRING \rightarrow INTEGER$.
 %% Cell type:code id: tags:
 ``` prob
 STRING_TO_INT("1024")
 ```
 %% Output
    $1024$
    1024
 %% Cell type:code id: tags:
 ``` prob
 STRING_TO_INT(" - 00001")
 ```
 %% Output
    $-1$
    −1
 %% Cell type:markdown id: tags:
 ### INT_TO_STRING
 This external function converts an integer to a string representation.
 Type: $INTEGER  \rightarrow STRING $.
 %% Cell type:code id: tags:
 ``` prob
 INT_TO_STRING(1024)
 ```
 %% Output
    $\text{"1024"}$
    "1024"
 %% Cell type:code id: tags:
 ``` prob
 INT_TO_STRING(-1024)
 ```
 %% Output
    $\text{"-1024"}$
    "-1024"
 %% Cell type:code id: tags:
 ``` prob
 INT_TO_STRING(STRING_TO_INT(" - 00001"))
 ```
 %% Output
    $\text{"-1"}$
    "-1"
 %% Cell type:code id: tags:
 ``` prob
 STRING_TO_INT(INT_TO_STRING(-1))=-1
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:markdown id: tags:
 ### DEC_STRING_TO_INT
 This external function takes a decimal string (with optional decimal places) and converts it to an integer with the given precision (rounding if required).
 Type: $STRING \times INTEGER  \rightarrow INTEGER$.
 %% Cell type:code id: tags:
 ``` prob
 DEC_STRING_TO_INT("1024",0)
 ```
 %% Output
    $1024$
    1024
 %% Cell type:code id: tags:
 ``` prob
 DEC_STRING_TO_INT("1024",2)
 ```
 %% Output
    $102400$
    102400
 %% Cell type:code id: tags:
 ``` prob
 DEC_STRING_TO_INT("1024",-1)
 ```
 %% Output
    $102$
    102
 %% Cell type:code id: tags:
 ``` prob
 DEC_STRING_TO_INT("1025",-1)
 ```
 %% Output
    $103$
    103
 %% Cell type:code id: tags:
 ``` prob
 DEC_STRING_TO_INT(" -1025",-1)
 ```
 %% Output
    $-103$
    −103
 %% Cell type:code id: tags:
 ``` prob
 DEC_STRING_TO_INT("1024.234",2)
 ```
 %% Output
    $102423$
    102423
 %% Cell type:code id: tags:
 ``` prob
 DEC_STRING_TO_INT("1024",100)
 ```
 %% Output
    $10240000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000$
    10240000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
 %% Cell type:code id: tags:
 ``` prob
 DEC_STRING_TO_INT("10000000000000000000000000000000000",-32)=100
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:markdown id: tags:
 ### INT_TO_DEC_STRING
 This external function converts an integer to a decimal string representation
 with the precision provided by the second argument.
 Type: $INTEGER  \times INTEGER  \rightarrow STRING $.
 %% Cell type:code id: tags:
 ``` prob
 INT_TO_DEC_STRING(1204,2)
 ```
 %% Output
    $\text{"12.04"}$
    "12.04"
 %% Cell type:code id: tags:
 ``` prob
 INT_TO_DEC_STRING(-1204,3)
 ```
 %% Output
    $\text{"-1.204"}$
    "-1.204"
 %% Cell type:code id: tags:
 ``` prob
 INT_TO_DEC_STRING(0,2)
 ```
 %% Output
    $\text{"0.00"}$
    "0.00"
 %% Cell type:code id: tags:
 ``` prob
 INT_TO_DEC_STRING(1204,-2)
 ```
 %% Output
    $\text{"120400"}$
    "120400"
 %% Cell type:code id: tags:
 ``` prob
 INT_TO_DEC_STRING(-10,3)
 ```
 %% Output
    $\text{"-0.010"}$
    "-0.010"
 %% Cell type:markdown id: tags:
 ### INT_TO_HEX_STRING
 This external function converts an integer to a hexadecimal string representation.
 Type: $INTEGER  \rightarrow STRING $.
 %% Cell type:code id: tags:
 ``` prob
 INT_TO_HEX_STRING(254)
 ```
 %% Output
    $\text{"fe"}$
    "fe"
 %% Cell type:code id: tags:
 ``` prob
 INT_TO_HEX_STRING(0)
 ```
 %% Output
    $\text{"0"}$
    "0"
 %% Cell type:code id: tags:
 ``` prob
 INT_TO_HEX_STRING(-254)
 ```
 %% Output
    $\text{"-fe"}$
    "-fe"
 %% Cell type:code id: tags:
 ``` prob
 INT_TO_HEX_STRING(2**100-1)
 ```
 %% Output
    $\text{"fffffffffffffffffffffffff"}$
    "fffffffffffffffffffffffff"
 %% Cell type:markdown id: tags:
 ### TO_STRING
 This external function converts a B data value to a string representation.
 Type: $\tau \rightarrow STRING$.
 %% Cell type:code id: tags:
 ``` prob
 TO_STRING(1024)
 ```
 %% Output
    $\text{"1024"}$
    "1024"
 %% Cell type:code id: tags:
 ``` prob
 TO_STRING("1024")
 ```
 %% Output
    $\text{"1024"}$
    "1024"
 %% Cell type:code id: tags:
 ``` prob
 TO_STRING({2,3,5})
 ```
 %% Output
    $\text{"{2,3,5}"}$
    "{2,3,5}"
 %% Cell type:code id: tags:
 ``` prob
 TO_STRING((TRUE,3,{11|->rec(a:22,b:33)}))
 ```
 %% Output
    $\text{"(TRUE|->3|->{(11|->rec(a:22,b:33))})"}$
    "(TRUE|->3|->{(11|->rec(a:22,b:33))})"
 %% Cell type:markdown id: tags:
 ### FORMAT_TO_STRING
 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.
 - the length of sequence must correspond to the number of `~w` in the format string.
 - the format string follows the conventions of SICStus Prolog.
    E.g., one can use `~n` for newlines.
 Type: $(STRING*seq(\tau)) \rightarrow STRING$.
 %% Cell type:code id: tags:
 ``` prob
 FORMAT_TO_STRING("two to the power ten = ~w",[2**10])
 ```
 %% Output
    $\text{"two to the power ten = 1024"}$
    "two to the power ten = 1024"
 %% Cell type:code id: tags:
 ``` prob
 FORMAT_TO_STRING("My two sets are ~w and ~w",[1..2,2..1])
 ```
 %% Output
    $\text{"My two sets are {1,2} and {}"}$
    "My two sets are {1,2} and {}"
 %% Cell type:markdown id: tags:
 #### Format Strings
 Various external functions and predicates work with format strings.
 ProB uses the conventions of the SICStus Prolog format string.
 - `~n` inserts a newline into the generated output
 - `~Nn` where N is a number: it inserts $N$ newlines into the output
 - `~w` inserts the next argument into the generated output
 - `~i` consumes the next argument but ignores it; i.e., nothing is inserted into the output
 - `~~` inserts the tilde symbol into the generated output
 - `~N` inserts a newline if not at the beginning of the line
 SICStus Prolog also uses a few other formatting codes, such as `~@`, `~p`,... which should not be used.
 %% Cell type:markdown id: tags:
 ### STRINGIFY
 This external function converts a B expression to a string representation of the expression, not the value.
 It can be used to obtain the name of variables.
 Warning: ProB may simplify and rewrite expressions (you can turn this off by setting the OPTIMIZE_AST preference to false).
 Type: $\tau \rightarrow STRING$.
 %% Cell type:code id: tags:
 ``` prob
 STRINGIFY(dom({1|->2}))
 ```
 %% Output
    $\text{"dom({1 |-> 2})"}$
    "dom({1 |-> 2})"
 %% Cell type:markdown id: tags:
 Compare this with the result of TO_STRING:
 %% Cell type:code id: tags:
 ``` prob
 TO_STRING(dom({1|->2}))
 ```
 %% Output
    $\text{"{1}"}$
    "{1}"
 %% Cell type:code id: tags:
 ``` prob
 :table rec(stringify:STRINGIFY("abc"),tostring:TO_STRING("abc"))
 ```
 %% Output
    |stringify|tostring|
    |---|---|
    |$\text{"\"abc\""}$|$\text{"abc"}$|
    stringify	tostring
    "\"abc\""	"abc"
 %% Cell type:markdown id: tags:
 ## Choose Operators
 You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:
 `DEFINITIONS "CHOOSE.def"`
 ### Choose
 This external function takes a set and returns an element of the set.
 This is a proper mathematical function, i.e., it will always return the same value
 given the same argument.
 It is also known as Hilbert's operator.
 The operator raises an error when it is called with an empty set.
 Also, it is not guaranteed to work for infinite sets.
 Type: $POW(T) \rightarrow T$.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE Jupyter_CHOOSE
 DEFINITIONS "CHOOSE.def"
 END
 ```
 %% Output
    Loaded machine: Jupyter_CHOOSE
 %% Cell type:code id: tags:
 ``` prob
 CHOOSE(1..3)
 ```
 %% Output
    $1$
    1
 %% Cell type:code id: tags:
 ``` prob
 CHOOSE({1,2,3})
 ```
 %% Output
    $1$
    1
 %% Cell type:code id: tags:
 ``` prob
 CHOOSE({"a","b","c"})
 ```
 %% Output
    $\text{"a"}$
    "a"
 %% Cell type:code id: tags:
 ``` prob
 CHOOSE(NATURAL)
 ```
 %% Output
    $0$
    0
 %% Cell type:code id: tags:
 ``` prob
 CHOOSE(INTEGER)
 ```
 %% Output
    $0$
    0
 %% Cell type:markdown id: tags:
 The operator is useful for writing WHILE loops or recursive functions which manipulate sets.
 The following example defines a recursive summation function using the CHOOSE operator.
 ```
 MACHINE RecursiveSigmaCHOOSEv3
 DEFINITIONS
  "Choose.def"
 ABSTRACT_CONSTANTS sigma
 PROPERTIES
  sigma: POW(INTEGER) <-> INTEGER &
  sigma = %x.(x:POW(INTEGER) |
              IF x={} THEN 0 ELSE
                LET c BE c=CHOOSE(x) IN c+sigma(x-{c}) END
              END
              )
 ASSERTIONS
 sigma({3,5,7}) = 15;
 END
 ```
 %% Cell type:markdown id: tags:
 ### MU
 Just like CHOOSE, this external function takes a set and returns an element of the set.
 In contrast to CHOOSE, it is only defined for singleton sets.
 The operator raises an error when it is called with an empty set or a set containing more than one element.
 Type: $POW(T) \rightarrow T$.
 %% Cell type:code id: tags:
 ``` prob
 MU({2})
 ```
 %% Output
    $2$
    2
 %% Cell type:code id: tags:
 ``` prob
 MU({2})+MU({x|x>0 & x<2})
 ```
 %% Output
    $3$
    3
 %% Cell type:markdown id: tags:
 ## Sorting Sets
 You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:
 `DEFINITIONS "SORT.def"`
 Alternatively you can use the following if you use ProB prior to version 1.7.1:
 `
 DEFINITIONS
 SORT(X) == [];
 EXTERNAL_FUNCTION_SORT(T) == (POW(T)-->seq(T));
 `
 This external function SORT takes a set and translates it into a B sequence.
 It uses ProB's internal order for sorting the elements.
 It will not work for infinite sets.
 Type: $POW(\tau) \rightarrow seq(\tau)$.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE Jupyter_SORT
 DEFINITIONS "SORT.def"
 END
 ```
 %% Output
    Loaded machine: Jupyter_SORT
 %% Cell type:code id: tags:
 ``` prob
 SORT(1..3)
 ```
 %% Output
    $[1,2,3]$
    [1,2,3]
 %% Cell type:code id: tags:
 ``` prob
 SORT({3*3,3+3,3**3})
 ```
 %% Output
    $[6,9,27]$
    [6,9,27]
 %% Cell type:code id: tags:
 ``` prob
 SORT({"ab","aa","a","b","10","1","2","11"})
 ```
 %% Output
    $[\text{"1"},\text{"10"},\text{"11"},\text{"2"},\text{"a"},\text{"aa"},\text{"ab"},\text{"b"}]$
    ["1","10","11","2","a","aa","ab","b"]
 %% Cell type:code id: tags:
 ``` prob
 SORT({("a"|->1),("b"|->0),("a"|->0)})
 ```
 %% Output
    $[(\text{"a"}\mapsto 0),(\text{"a"}\mapsto 1),(\text{"b"}\mapsto 0)]$
    [("a"↦0),("a"↦1),("b"↦0)]
 %% Cell type:markdown id: tags:
 A related external function is LEQ_SYM_BREAK which allows one to compare values of arbitrary type.
 Calls to this external function are automatically
 inserted by ProB for symmetry breaking of quantifiers.
 It should currently not be used for sets or sequences.
 %% Cell type:markdown id: tags:
 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 id: tags:
 ``` prob
 SQUASH({0|->"a",100|->"c",1001 |->"d",4|->"b", 44|->"c"})
 ```
 %% Output
    $[\text{"a"},\text{"b"},\text{"c"},\text{"c"},\text{"d"}]$
    ["a","b","c","c","d"]
 %% Cell type:markdown id: tags:
 ## Strongly Connected Components
 You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:
 `DEFINITIONS "SCCS.def"`
 Alternatively you can use the following if you use ProB prior to version 1.9.0:
 `
 DEFINITIONS
  EXTERNAL_FUNCTION_SCCS(T) == (T<->T) --> POW(POW(T));
  SCCS(relation) == {};
 `
 This external function SCCS takes a binary relation and computes the set of strongly connected components.
 Type: $POW(\tau \times \tau) \rightarrow POW(POW(\tau))$.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE Jupyter_SCCS
 DEFINITIONS "SCCS.def"
 END
 ```
 %% Output
    Loaded machine: Jupyter_SCCS
 %% Cell type:code id: tags:
 ``` prob
 SCCS({1|->2,2|->1,2|->3,3|->4,4|->3})
 ```
 %% Output
    $\{\{1,2\},\{3,4\}\}$
    {{1,2},{3,4}}
 %% Cell type:code id: tags:
 ``` prob
 :dot expr_as_graph ("rel",{1|->2,2|->1,2|->3,3|->4,4|->3})
 ```
 %% Output
    <Dot visualization: expr_as_graph [("rel",{(1,2),(2,1),(2,3),(3,4),(4,3)})]>
 %% Cell type:code id: tags:
 ``` prob
 SCCS({x,y|x:2..100 & y:2..100 & (x mod y = 0 or y mod x =0)})
 ```
 %% Output
    $\{\{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\}\}$
    {{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}}
 %% Cell type:markdown id: tags:
 ## LibraryMeta
 This library provides various meta information about ProB and the current model.
 You can obtain the definitions below by putting the following into your DEFINITIONS clause:
 `DEFINITIONS "LibraryMeta.def"`
 The file `LibraryMeta.def` is also bundled with ProB and can be found in the `stdlib` folder.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE Jupyter_LibraryMeta
 DEFINITIONS "LibraryMeta.def"
 END
 ```
 %% Output
    Loaded machine: Jupyter_LibraryMeta
 %% Cell type:markdown id: tags:
 ### PROB_INFO_STR
 This external function provides access to various information strings about ProB.
 Type: $STRING \rightarrow STRING$.
 %% Cell type:code id: tags:
 ``` prob
 PROB_INFO_STR("prob-version")
 ```
 %% Output
    $\text{"1.9.0-beta8"}$
    "1.9.0-beta8"
 %% Cell type:code id: tags:
 ``` prob
 PROB_INFO_STR("prob-revision")
 ```
 %% Output
    $\text{"2a32153ac44523a5f93b0a999f9c42198b9360dc"}$
    "2a32153ac44523a5f93b0a999f9c42198b9360dc"
 %% Cell type:code id: tags:
 ``` prob
 PROB_INFO_STR("prob-last-changed-date")
 ```
 %% Output
    $\text{"Thu Feb 28 13:02:03 2019 +0100"}$
    "Thu Feb 28 13:02:03 2019 +0100"
 %% Cell type:code id: tags:
 ``` prob
 PROB_INFO_STR("java-version")
 ```
 %% Output
    $\text{"1.8.0_202-b08"}$
    "1.8.0_202-b08"
 %% Cell type:code id: tags:
 ``` prob
 PROB_INFO_STR("java-command-path")
 ```
 %% Output
    $\text{"/usr/bin/java"}$
    "/usr/bin/java"
 %% Cell type:code id: tags:
 ``` prob
 PROB_INFO_STR("current-time")
 ```
 %% Output
    $\text{"5/3/2019 - 13h42 41s"}$
    "5/3/2019 - 13h42 41s"
 %% Cell type:markdown id: tags:
 Another command is PROB_INFO_STR("parser-version") which does not work within Jupyter.
 %% Cell type:markdown id: tags:
 ### PROB_STATISTICS
 This external function provides access to various statistics in the form of integers about ProB.
 Type: $STRING \rightarrow INTEGER$.
 %% Cell type:code id: tags:
 ``` prob
 PROB_STATISTICS("prolog-memory-bytes-used")
 ```
 %% Output
    $157096032$
    157096032
 %% Cell type:code id: tags:
 ``` prob
 PROB_STATISTICS("states")
 ```
 %% Output
    $1$
    1
 %% Cell type:code id: tags:
 ``` prob
 PROB_STATISTICS("transitions")
 ```
 %% Output
    $0$
    0
 %% Cell type:code id: tags:
 ``` prob
 PROB_STATISTICS("processed-states")
 ```
 %% Output
    $0$
    0
 %% Cell type:code id: tags:
 ``` prob
 PROB_STATISTICS("current-state-id")
 ```
 %% Output
    $-1$
    −1
 %% Cell type:code id: tags:
 ``` prob
 PROB_STATISTICS("now-timestamp")
 ```
 %% Output
    $1551789761$
    1551789761
 %% Cell type:code id: tags:
 ``` prob
 PROB_STATISTICS("prolog-runtime")
 ```
 %% Output
    $1535$
    1535
 %% Cell type:code id: tags:
 ``` prob
 PROB_STATISTICS("prolog-walltime")
 ```
 %% Output
    $2519$
    2519
 %% Cell type:markdown id: tags:
 Other possible information fields are prolog-memory-bytes-free,
 prolog-global-stack-bytes-used,
 prolog-local-stack-bytes-used,
 prolog-global-stack-bytes-free,
 prolog-local-stack-bytes-free,
 prolog-trail-bytes-used,
 prolog-choice-bytes-used,
 prolog-atoms-bytes-used,
 prolog-atoms-nb-used,
 prolog-gc-count,
 prolog-gc-time.
 %% Cell type:markdown id: tags:
 ### PROJECT_STATISTICS
 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).
 Type: $STRING \rightarrow INTEGER$.
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_STATISTICS("constants")
 ```
 %% Output
    $0$
    0
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_STATISTICS("variables")
 ```
 %% Output
    $0$
    0
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_STATISTICS("properties")
 ```
 %% Output
    $0$
    0
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_STATISTICS("invariants")
 ```
 %% Output
    $0$
    0
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_STATISTICS("operations")
 ```
 %% Output
    $0$
    0
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_STATISTICS("static_assertions")
 ```
 %% Output
    $0$
    0
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_STATISTICS("dynamic_assertions")
 ```
 %% Output
    $0$
    0
 %% Cell type:markdown id: tags:
 ### PROJECT_INFO
 This external function provides access to various information strings about the current specification being processed, with all auxiliary files (i.e., project).
 Type: $STRING \rightarrow POW(STRING)$.
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_INFO("files")
 ```
 %% Output
    $\{\text{"(machine from Jupyter cell).mch"},\text{"LibraryMeta.def"}\}$
    {"(machine from Jupyter cell).mch","LibraryMeta.def"}
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_INFO("main-file")
 ```
 %% Output
    $\{\text{"(machine from Jupyter cell).mch"}\}$
    {"(machine from Jupyter cell).mch"}
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_INFO("variables")
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
    ∅
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_INFO("constants")
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
    ∅
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_INFO("sets")
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
    ∅
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_INFO("operations")
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
    ∅
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_INFO("assertion_labels")
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
    ∅
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_INFO("invariant_labels")
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
    ∅
 %% Cell type:code id: tags:
 ``` prob
 PROJECT_INFO("sha-hash")
 ```
 %% Output
    $\{\text{"5d45f08d7e5cf22716b8fd3dd54a29b4ba4c443c"}\}$
    {"5d45f08d7e5cf22716b8fd3dd54a29b4ba4c443c"}
 %% Cell type:markdown id: tags:
 ### MACHINE_INFO
 This external function provides access to various information strings about B machines being processed.
 Type: $STRING \rightarrow STRING$.
 %% Cell type:code id: tags:
 ``` prob
 MACHINE_INFO("Jupyter_LibraryMeta","TYPE")
 ```
 %% Output
    $\text{"abstract_machine"}$
    "abstract_machine"
 %% Cell type:markdown id: tags:
 ## LibraryIO
 This library provides various input/output facilities.
 It is probably most useful for debugging, but can also be used to write B machines
 which can read and write data.
 You can obtain the definitions below by putting the following into your DEFINITIONS clause:
 `DEFINITIONS "LibraryIO.def"`
 The file `LibraryIO.def` is also bundled with ProB and can be found in the `stdlib` folder.
 %% Cell type:markdown id: tags:
 ## LibraryXML
 This library provides various functions to read and write XML data from file and strings.
 You can obtain the definitions below by putting the following into your DEFINITIONS clause:
 `DEFINITIONS "LibraryXML.def"`
 The file `LibraryXML.def` is also bundled with ProB and can be found in the `stdlib` folder.
 ### Internal Data Type
 An XML document is represented using the type seq(XML_ELement_Type), i.e., a sequence
 of XML elements, whose type is defined by the following (included in the LibraryXML.def file):
 ```
 XML_ELement_Type ==
      struct(
        recId: NATURAL1,
        pId:NATURAL,
        element:STRING,
        attributes: STRING +-> STRING,
        meta: STRING +-> STRING
        );
 ```
 ### Files and Strings
 XML documents can either be stored in a file or in a B string.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE Jupyter_LibraryXML
 DEFINITIONS "LibraryXML.def"
 END
 ```
 %% Output
    Loaded machine: Jupyter_LibraryXML
 %% Cell type:markdown id: tags:
 ### READ_XML_FROM_STRING
 This external function takes an XML document string and converts into into the B format seq(XML_ELement_Type)}.
 Note that all strings in ProB are encoded using UTF-8, so no encoding argument has to be provided.
 %% Cell type:code id: tags:
 ``` prob
 READ_XML_FROM_STRING('''
 <?xml version="1.0" encoding="ASCII"?>
 <Data version= "0.1">
 <Tag1 elemID="ID1" attr1="value1" />
 </Data>
 ''')
 ```
 %% Output
    $\{(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))\}$
    {(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))}
 %% Cell type:markdown id: tags:
 ### READ_XML
 This external function can read in an XML document from file. In contrast to READ_XML_FROM_STRING
 it also takes a second argument specifying the encoding used.
 ProB cannot as of now detect the encoding from the XML header.
 In future this argument may be removed.
 Currently it can take these values:
 "auto","ISO-8859-1","ISO-8859-2","ISO-8859-15",
                    "UTF-8","UTF-16","UTF-16LE","UTF-16BE","UTF-32","UTF-32LE","UTF-32BE",
                    "ANSI\_X3.4-1968", "windows 1252".
 %% Cell type:markdown id: tags:
 ## LibraryHash
 This library provides various facilities to compute hash values for B values.
 You can obtain the definitions below by putting the following into your DEFINITIONS clause:
 `DEFINITIONS "LibraryHash.def"`
 The file `LibraryHash.def` is also bundled with ProB and can be found in the `stdlib` folder.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE Jupyter_LibraryHash
 DEFINITIONS "LibraryHash.def"
 END
 ```
 %% Output
    Loaded machine: Jupyter_LibraryHash
 %% Cell type:markdown id: tags:
 ### HASH
 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.
 Type: $\tau \rightarrow INTEGER$.
 %% Cell type:code id: tags:
 ``` prob
 HASH({1,2,4})
 ```
 %% Output
    $92915201$
    92915201
 %% Cell type:code id: tags:
 ``` prob
 HASH({1,2,5})
 ```
 %% Output
    $191034877$
    191034877
 %% Cell type:code id: tags:
 ``` prob
 i<: 1..7 & j<:1..7 & i /= j & HASH(i)=HASH(j)
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:markdown id: tags:
 ### SHA_HASH
 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.
 Type: $\tau \rightarrow INTEGER$.
 %% Cell type:code id: tags:
 ``` prob
 SHA_HASH({1,2,4})
 ```
 %% Output
    $[37,168,75,91,175,1,8,58,13,207,7,42,222,208,212,29,243,31,27,154]$
    [37,168,75,91,175,1,8,58,13,207,7,42,222,208,212,29,243,31,27,154]
 %% Cell type:code id: tags:
 ``` prob
 SHA_HASH({1,2,5})
 ```
 %% Output
    $[149,81,45,24,177,25,74,30,204,7,143,202,136,116,148,247,6,221,245,52]$
    [149,81,45,24,177,25,74,30,204,7,143,202,136,116,148,247,6,221,245,52]
 %% Cell type:code id: tags:
 ``` prob
 i<: 1..7 & j<:1..7 & i /= j & SHA_HASH(i)=SHA_HASH(j)
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:markdown id: tags:
 ### SHA_HASH_HEX
 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.
 Type: $\tau \rightarrow STRING$.
 %% Cell type:code id: tags:
 ``` prob
 SHA_HASH_HEX({1,2,4})
 ```
 %% Output
    $\text{"25a84b5baf01083a0dcf072aded0d41df31f1b9a"}$
    "25a84b5baf01083a0dcf072aded0d41df31f1b9a"
 %% Cell type:code id: tags:
 ``` prob
 SHA_HASH_HEX({1,2,5})
 ```
 %% Output
    $\text{"95512d18b1194a1ecc078fca887494f706ddf534"}$
    "95512d18b1194a1ecc078fca887494f706ddf534"
 %% Cell type:code id: tags:
 ``` prob
 SHA_HASH_HEX({x|x<:1..8 & card(x)=2})
 ```
 %% Output
    $\text{"6bd1d8beefa14ea131285d11bbf8580c5f31fe78"}$
    "6bd1d8beefa14ea131285d11bbf8580c5f31fe78"
 %% Cell type:code id: tags:
 ``` prob
 SHA_HASH_HEX(0)
 ```
 %% Output
    $\text{"068948b4d423a0db5fd1574edad799005fc456e0"}$
    "068948b4d423a0db5fd1574edad799005fc456e0"
 %% Cell type:code id: tags:
 ``` prob
 SHA_HASH_HEX(SHA_HASH_HEX(0))
 ```
 %% Output
    $\text{"55b9c89f79362578c3641774db978b5455be5bfd"}$
    "55b9c89f79362578c3641774db978b5455be5bfd"
 %% Cell type:markdown id: tags:
 ## LibraryRegex
 This library provides various facilities for pattern matching with regular expressions.
 You can obtain the definitions below by putting the following into your DEFINITIONS clause:
 `DEFINITIONS "LibraryRegex.def"`
 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 id: tags:
 ``` prob
 ::load
 MACHINE Jupyter_LibraryRegex
 DEFINITIONS "LibraryRegex.def"; "LibraryStrings.def"
 END
 ```
 %% Output
    Loaded machine: Jupyter_LibraryRegex
 %% Cell type:markdown id: tags:
 The library works on B strings and regular expression patterns are also written as B strings.
 The syntax used is the ECMAScript syntax: http://www.cplusplus.com/reference/regex/ECMAScript/
 The library is currently implemented using the C++ standard library.
 Below we repeat some information from http://www.cplusplus.com/reference/regex/ECMAScript/ for convenience.
 The library now does support UTF-8 encoded strings and patterns.
 Note that ProB only supports UTF-8 for both B machines and for any strings and Unicode files it processes.
 #### Operators/Quantifiers
 More precisely the library accepts the following operators:
 | Syntax | Descr. | Matches |
 | --- | --- | --- |
 | ```*``` | 0 or more |The preceding atom is matched 0 or more times. |
 | ```+``` |1 or more |The preceding atom is matched 1 or more times. |
 | ```?``` |0 or 1 |The preceding atom is optional (matched either 0 times or once). |
 | ```{int}``` |int |The preceding atom is matched exactly int times. |
 | ```{int,}``` |int or more |The preceding atom is matched int or more times. |
 | ```{min,max}``` |between min and max |The preceding atom is matched at least min times, but not more than max. |
 There is also the ```|``` separator.
 It separates two alternative patterns or subpatterns.
 %% Cell type:markdown id: tags:
 #### Characters
 The library accepts the following special characters:
 | Syntax | Descr. | Matches |
 | --- | --- | --- |
 | ```.```	| not newline	| any character except line terminators (LF, CR, LS, PS).|
 | ```\t```	| tab (HT)	| a horizontal tab character (same as \u0009).|
 | ```\n```	| newline (LF)	| a newline (line feed) character (same as \u000A).|
 | ```\v```	| vertical tab (VT)	| a vertical tab character (same as \u000B).|
 | ```\f```	| form feed (FF)	| a form feed character (same as \u000C).|
 | ```\r```	| carriage return (CR)	| a carriage return character (same as \u000D).|
 | ```\cletter```	| control code	| a control code character whose code unit value is the same as the remainder of dividing the code unit value of letter by 32.|
 For example: ```\ca``` is the same as ```\u0001```, ```\cb``` the same as ```\u0002```, and so on...
 | Syntax | Descr. | Matches |
 | --- | --- | --- |
 | ```\xhh```| ASCII character| a character whose code unit value has an hex value equivalent to the two hex digits hh.|
 For example: ```\x4c``` is the same as L, or ```\x23``` the same as #.
 | Syntax | Descr. | Matches |
 | --- | --- | --- |
 | ```\uhhhh```| unicode character| a character whose code unit value has an hex value equivalent to the four hex digits hhhh.|
 | ```\0```| null| a null character (same as \u0000).|
 | ```\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.|
 | ```\d```| digit| a decimal digit character (same as [[:digit:]]).|
 |  ```\D```| not digit| any character that is not a decimal digit character (same as [^[:digit:]]).|
 |  ```\s```| whitespace| a whitespace character (same as [[:space:]]).|
 | ```\S```| not whitespace| any character that is not a whitespace character (same as [^[:space:]]).|
 |  ```\w```| word| an alphanumeric or underscore character (same as [_[:alnum:]]).|
 |  ```\W```| not word| any character that is not an alphanumeric or underscore character (same as [^_[:alnum:]]).|
 |  ```\character```| character| the character character as it is, without interpreting its special meaning within a regex expression.|
 Any character can be escaped except those which form any of the special character sequences above.
 Needed for: ```^ $ \ . * + ? ( ) [ ] { } |```
 | Syntax | Descr. | Matches |
 | --- | --- | --- |
 | ```[class]```| character class| the target character is part of the class (see character classes below)|
 | ```[^class]```| negated character class| the target character is not part of the class (see character classes below)|
 %% Cell type:markdown id: tags:
 #### Groups
 Groups allow to apply quantifiers to a sequence of characters (instead of a single character). There are two kinds of groups:
 | characters| description| effects|
 | --- | --- | --- |
 | ```(subpattern)```| Group| Creates a backreference.
 | ```(?:subpattern)```| Passive group| Does not create a backreference.
 #### Assertions
 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.
 characters	description	condition for match
 - ```^```	Beginning of line	Either it is the beginning of the target sequence, or follows a line terminator.
 - ```$```	End of line	Either it is the end of the target sequence, or precedes a line terminator.
 - ```\b```	Word boundary	The previous character is a word character and the next is a non-word character (or vice-versa).
 Note: The beginning and the end of the target sequence are considered here as non-word characters.
 - ```\B```	Not a word boundary	The previous and next characters are both word characters or both are non-word characters.
 Note: The beginning and the end of the target sequence are considered here as non-word characters.
 - ```(?=subpattern)```	Positive lookahead	The characters following the assertion must match subpattern, but no characters are consumed.
 - ```(?!subpattern)```	Negative lookahead	The characters following the assertion must not match subpattern, but no characters are consumed.
 #### Character classes
 A character class defines a category of characters. It is introduced by enclosing its descriptors in square brackets ([ and ]).
 The regex object attempts to match the entire character class against a single character in the target sequence (unless a quantifier specifies otherwise).
 The character class can contain any combination of:
 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).
 For example:
 ```[abc]``` matches a, b or c.
 ```[^xyz]``` matches any character except x, y and z.
 Ranges: They can be specified by using the hyphen character (-) between two valid characters.
 For example:
 ```[a-z]``` matches any lowercase letter (a, b, c, ... until z).
 ```[abc1-5]``` matches either a, b or c, or a digit between 1 and 5.
 POSIX-like classes: A whole set of predefined classes can be added to a custom character class. There are three kinds:
 class	description	notes
 - ```[:classname:]```	character class	Uses the regex traits' isctype member with the appropriate type gotten from applying lookup_classname member on classname for the match.
 - ```[.classname.]```	collating sequence	Uses the regex traits' lookup_collatename to interpret classname.
 - ```[=classname=]```	character equivalents	Uses the regex traits' transform_primary of the result of regex_traits::lookup_collatename for classname to check for matches.
 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:
 class	description	equivalent (with regex_traits, default locale)
 - ```[:alnum:]```	alpha-numerical character	isalnum
 - ```[:alpha:]```	alphabetic character	isalpha
 - ```[:blank:]```	blank character	isblank
 - ```[:cntrl:]```	control character	iscntrl
 - ```[:digit:]```	decimal digit character	isdigit
 - ```[:graph:]```	character with graphical representation	isgraph
 - ```[:lower:]```	lowercase letter	islower
 - ```[:print:]```	printable character	isprint
 - ```[:punct:]```	punctuation mark character	ispunct
 - ```[:space:]```	whitespace character	isspace
 - ```[:upper:]```	uppercase letter	isupper
 - ```[:xdigit:]```	hexadecimal digit character	isxdigit
 - ```[:d:]```	decimal digit character	isdigit
 - ```[:w:]```	word character	isalnum
 - ```[:s:]```	whitespace character	isspace
 Please note that the brackets in the class names are additional to those opening and closing the class definition.
 For example:
 ```[[:alpha:]]``` is a character class that matches any alphabetic character.
 ```[abc[:digit:]]``` is a character class that matches a, b, c, or a digit.
 ```[^[:space:]]``` is a character class that matches any character except a whitespace.
 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.
 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 (\).
 %% Cell type:markdown id: tags:
 ### REGEX_MATCH
 This external predicate checks if a string matches a regular expression pattern.
 For example, the following calls check whether the first argument is a non-empty sequenze of lower-case letters:
 %% Cell type:code id: tags:
 ``` prob
 REGEX_MATCH("abc","[a-z]+")
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 REGEX_MATCH("abc1","[a-z]+")
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:markdown id: tags:
 Here we check if we have a non-empty sequence of characters which are not letters:
 %% Cell type:code id: tags:
 ``` prob
 REGEX_MATCH("123.45","[^a-zA-Z]+")
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 REGEX_MATCH("1e9","[^a-zA-Z]+")
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:markdown id: tags:
 Observe that ```REGEX_MATCH``` is a **predicate** not a function returning a boolean value.
 As such you can write:
 %% Cell type:code id: tags:
 ``` prob
 str = "1.9" & (REGEX_MATCH(str,"[0-9]+") or REGEX_MATCH(str,"[0-9]*\.[0-9]+"))
 ```
 %% Output
    $\mathit{TRUE}$
    **Solution:**
    * $\mathit{str} = \text{"1.9"}$
    TRUE
    Solution:
    	str = "1.9"
 %% Cell type:markdown id: tags:
 ### IS_REGEXP
 This external predicate checks if a string is a valid regular expression pattern.
 Again, this is a **predicate**, not a function returning a boolean value.
 %% Cell type:code id: tags:
 ``` prob
 IS_REGEX("ab[0-9]")
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 IS_REGEX("ab[0-9")
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:markdown id: tags:
 ### REGEXP_REPLACE
 This external function replaces all occurences of a pattern in a string by a given replacement string.
 Type: $STRING \times STRING \times STRING \rightarrow STRING$.
 %% Cell type:code id: tags:
 ``` prob
 REGEX_REPLACE("a01b23c4d56","[0-9]+","NUM")
 ```
 %% Output
    $\text{"aNUMbNUMcNUMdNUM"}$
    "aNUMbNUMcNUMdNUM"
 %% Cell type:code id: tags:
 ``` prob
 REGEX_REPLACE("a01b23c4d56","[^0-9]+","X")
 ```
 %% Output
    $\text{"X01X23X4X56"}$
    "X01X23X4X56"
 %% Cell type:markdown id: tags:
 You can use ```$1```, ```$2```, ... to refer to matches subgroups in the replacement string:
 %% Cell type:code id: tags:
 ``` prob
 REGEX_REPLACE("1abd00abc2","([a-z]+).*?([a-z]+)","<<$2$1>>")
 ```
 %% Output
    $\text{"1<<abcabd>>2"}$
    "1<<abcabd>>2"
 %% Cell type:markdown id: tags:
 You can use ```$0``` to refer to the full match:
 %% Cell type:code id: tags:
 ``` prob
 REGEX_REPLACE("ab12cd34","[0-9]+","($0)")
 ```
 %% Output
    $\text{"ab(12)cd(34)"}$
    "ab(12)cd(34)"
 %% Cell type:markdown id: tags:
 ### REGEX_SEARCH_STR
 This external function searches for the **first** occurence of a pattern in a string.
 Type: $STRING \times STRING \rightarrow STRING$.
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH_STR("abcdef000234daf","[1-9][0-9]*")
 ```
 %% Output
    $\text{"234"}$
    "234"
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH_STR("abcdef000234daf","[[:alpha:]]+")
 ```
 %% Output
    $\text{"abcdef"}$
    "abcdef"
 %% Cell type:markdown id: tags:
 In the next example we use the ```$``` operator to force a match at the end:
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH_STR("abcdef000234daf","[[:alpha:]]+$")
 ```
 %% Output
    $\text{"daf"}$
    "daf"
 %% Cell type:markdown id: tags:
 In case there is no match, it returns the empty string:
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH_STR("0123","[[:alpha:]]+")
 ```
 %% Output
    $\text{""}$
    ""
 %% Cell type:markdown id: tags:
 ### REGEX_SEARCH
 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.
 It also expects an index at which to start the search; which can be useful for writing loops to find all matches.
 Type: $STRING \times INTEGER \times STRING \rightarrow struct(position:INTEGER,length:INTEGER,string:STRING,submatches:seq(STRING))$.
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH("abcdef000234daf",1,"[[:alpha:]]+")
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\mathit{rec}(\mathit{length}\in 6,\mathit{position}\in 1,\mathit{string}\in\text{"abcdef"},\mathit{submatches}\in\emptyset)$
    rec(length∈6,position∈1,string∈"abcdef",submatches∈∅)
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH("abcdef000234daf",7,"[[:alpha:]]+")
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\mathit{rec}(\mathit{length}\in 3,\mathit{position}\in 13,\mathit{string}\in\text{"daf"},\mathit{submatches}\in\emptyset)$
    rec(length∈3,position∈13,string∈"daf",submatches∈∅)
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH("abcdef000234daf",1,"([1-9])([0-9]*)")
 ```
 %% Output
    $\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"})\})$
    rec(length∈3,position∈10,string∈"234",submatches∈{(1↦"2"),(2↦"34")})
 %% Cell type:markdown id: tags:
 In case there is no match, the function returns a record with position and length being -1:
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH("0123",1,"[[:alpha:]]+")
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\mathit{rec}(\mathit{length}\in-1,\mathit{position}\in-1,\mathit{string}\in\text{""},\mathit{submatches}\in\emptyset)$
    rec(length∈−1,position∈−1,string∈"",submatches∈∅)
 %% Cell type:markdown id: tags:
 ### REGEX_SEARCH_ALL
 This external function searches for the **all** occurence of a pattern in a string and returns the matched strings as a B sequence.
 It always starts to match at the beginning.
 Type: $STRING \times STRING \rightarrow seq(STRING)$.
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH_ALL("abcdef000234daf567","([1-9])([0-9]*)")
 ```
 %% Output
    $\{(1\mapsto\text{"234"}),(2\mapsto\text{"567"})\}$
    {(1↦"234"),(2↦"567")}
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH_ALL("abcdef000234daf567","([0-9])")
 ```
 %% Output
    $[\text{"0"},\text{"0"},\text{"0"},\text{"2"},\text{"3"},\text{"4"},\text{"5"},\text{"6"},\text{"7"}]$
    ["0","0","0","2","3","4","5","6","7"]
 %% Cell type:markdown id: tags:
 If there is no match the function returns the empty set.
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH_ALL("0123","[[:alpha:]]+")
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$
    ∅
 %% Cell type:markdown id: tags:
 ### Unicode treatment
 The examples below show how ProB deals with Unicode strings and patterns.
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH_ALL("abc-äéà-123","[[:alpha:]]")
 ```
 %% Output
    $[\text{"a"},\text{"b"},\text{"c"},\text{"ä"},\text{"é"},\text{"à"}]$
    ["a","b","c","ä","é","à"]
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH_STR("abc-äéà-123","[äüéèà]+")
 ```
 %% Output
    $\text{"äéà"}$
    "äéà"
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH("abc-äéà-123",1,"[äüéèà]+")
 ```
 %% Output
    $\renewcommand{\emptyset}{\mathord\varnothing}\mathit{rec}(\mathit{length}\in 3,\mathit{position}\in 5,\mathit{string}\in\text{"äéà"},\mathit{submatches}\in\emptyset)$
    rec(length∈3,position∈5,string∈"äéà",submatches∈∅)
 %% Cell type:code id: tags:
 ``` prob
 REGEX_REPLACE("abc-äéà-123","[äüéèà]+"," ça ")
 ```
 %% Output
    $\text{"abc- ça -123"}$
    "abc- ça -123"
 %% Cell type:code id: tags:
 ``` prob
 REGEX_MATCH("äbc","...")
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 REGEX_MATCH("äbc","abc")
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:code id: tags:
 ``` prob
 REGEX_MATCH("äbc","[[:alpha:]]{3}")
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:markdown id: tags:
 ### Useful patterns
 Below we show few examples illustrating useful patterns:
 %% Cell type:markdown id: tags:
 Here we use the ```\w``` word operator:
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH_ALL("The quick fox.","\w+")
 ```
 %% Output
    $[\text{"The"},\text{"quick"},\text{"fox"}]$
    ["The","quick","fox"]
 %% Cell type:markdown id: tags:
 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 id: tags:
 ``` prob
 REGEX_SEARCH("192.69.2.1",1,"(\d+)\.(\d+)\.(\d+)\.(\d+)")
 ```
 %% Output
    $\mathit{rec}(\mathit{length}\in 10,\mathit{position}\in 1,\mathit{string}\in\text{"192.69.2.1"},\mathit{submatches}\in [\text{"192"},\text{"69"},\text{"2"},\text{"1"}])$
    rec(length∈10,position∈1,string∈"192.69.2.1",submatches∈["192","69","2","1"])
 %% Cell type:markdown id: tags:
 This example also uses the non-digit operator ```\D```.
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH("192.69.2.1",1,"(\d+)\D(\d+)\D(\d+)\D(\d+)")
 ```
 %% Output
    $\mathit{rec}(\mathit{length}\in 10,\mathit{position}\in 1,\mathit{string}\in\text{"192.69.2.1"},\mathit{submatches}\in [\text{"192"},\text{"69"},\text{"2"},\text{"1"}])$
    rec(length∈10,position∈1,string∈"192.69.2.1",submatches∈["192","69","2","1"])
 %% Cell type:markdown id: tags:
 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 id: tags:
 ``` prob
 REGEX_SEARCH("192.69.2.1",1,"(\\d+)\\D(\\d+)\\D(\\d+)\\D(\\d+)")'submatches
 ```
 %% Output
    $[\text{"192"},\text{"69"},\text{"2"},\text{"1"}]$
    ["192","69","2","1"]
 %% Cell type:markdown id: tags:
 Here we use the quantifier ```{min,max}``` to find sequences of 1 to 3 digits:
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH_ALL("10234","\d{1,3}")
 ```
 %% Output
    $\{(1\mapsto\text{"102"}),(2\mapsto\text{"34"})\}$
    {(1↦"102"),(2↦"34")}
 %% Cell type:markdown id: tags:
 The next two examples use the ```\s``` whitespace and not-whitespace ```\S``` operators:
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH_ALL("weight is 50 and height is 100","\S+")
 ```
 %% Output
    $[\text{"weight"},\text{"is"},\text{"50"},\text{"and"},\text{"height"},\text{"is"},\text{"100"}]$
    ["weight","is","50","and","height","is","100"]
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH_ALL("weight is 50 and height is 100","\s+\S+")
 ```
 %% Output
    $[\text{" is"},\text{" 50"},\text{" and"},\text{" height"},\text{" is"},\text{" 100"}]$
    [" is"," 50"," and"," height"," is"," 100"]
 %% Cell type:markdown id: tags:
 #### Lookaheads
 These examples use positive lookahead operator ```(?=subpattern)``` and the negative lookahead operator ```(?!subpattern)``` respectively:
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH("abc-defg-hi:jkl",1,"[[:alpha:]]+(?=:)")'string
 ```
 %% Output
    $\text{"hi"}$
    "hi"
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH("abc-defg-hi:jkl",1,"[[:alpha:]]+(?![-a-z])")'string
 ```
 %% Output
    $\text{"hi"}$
    "hi"
 %% Cell type:markdown id: tags:
 Note that lookbehinds (such as ```(?<=:)```) are currently not supported by ProB:
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH("abc-defg-hi:jkl",1,"[[:alpha:]]+(?<=:)")'string
 ```
 %% Output
    :eval: NOT-WELL-DEFINED:
    ### Exception occurred while calling external function:  'REGEX_SEARCH':regex_exception('One of *?+{ was not preceded by a valid regular expression.')
     ### File: /Users/leuschel/git_root/prob_prolog/stdlib/LibraryRegex.def
     ### Line: 28, Column: 1 until 88
     ### within: DEFINITION call of REGEX_SEARCH at Line: 1 Column: 0 until Line: 1 Column: 54
 %% Cell type:markdown id: tags:
 Backreferences ```\int``` are supported, to match the int-th subgroup:
 %% Cell type:code id: tags:
 ``` prob
 REGEX_SEARCH("abc-dede-hi:jkl",1,"([[:alpha:]]+)\1")'string
 ```
 %% Output
    $\text{"dede"}$
    "dede"
 %% Cell type:markdown id: tags:
 #### Escaping in B Strings
 As regular expressions make heavy use of the backslash ```\``` it is important to know how B strings deal with backslashes.
 ProB supports two types of strings:
 - single-line strings delimited using double quotation marks, e.g., ```"abc"```
 - multi-line strings delimited using three single quogtation marks. ```'''abc'''```
 Inside both types of strings the following escape sequences using the backslash are recognised:
 - ```\n``` stands simply for newline
 - ```\t``` stands simply for tab
 - ```\r``` stands for carriage return
 - ```\"``` stands simply for ```"```  (to be able to use quotes in single-line strings)
 - ```\'``` stands simply for ```'``` (to be able to use quotes in multi-line strings)
 - ```\\``` stands simply for ```\``` (to be able to use backslash when preceding any of the above symbols)
 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).
 The following examples illustrate the above.
 %% Cell type:code id: tags:
 ``` prob
 STRING_LENGTH("\"")
 ```
 %% Output
    $1$
    1
 %% Cell type:code id: tags:
 ``` prob
 STRING_LENGTH("\\\"")
 ```
 %% Output
    $2$
    2
 %% Cell type:code id: tags:
 ``` prob
 STRING_LENGTH("\a")
 ```
 %% Output
    $2$
    2
 %% Cell type:code id: tags:
 ``` prob
 STRING_LENGTH("\\a")
 ```
 %% Output
    $2$
    2
 %% Cell type:code id: tags:
 ``` prob
 "\a" = "\\a"
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 "\n" = "\\n"
 ```
 %% Output
    $\mathit{FALSE}$
    FALSE
 %% Cell type:code id: tags:
 ``` prob
 "\\\""
 ```
 %% Output
    $\text{"\\\""}$
    "\\\""
 %% Cell type:markdown id: tags:
 Note that the previous result thus contains two characters:
 %% Cell type:code id: tags:
 ``` prob
 STRING_CHARS("\\\"")
 ```
 %% Output
    :eval: Computation not completed: Unknown identifier "STRING_CHARS"
 %% Cell type:code id: tags:
 ``` prob
 "\a"
 ```
 %% Output
    $\text{"\a"}$
    "\a"
 %% Cell type:code id: tags:
 ``` prob
 "\\"
 ```
 %% Output
    $\text{"\\"}$
    "\\"
 %% Cell type:code id: tags:
 ``` prob
 "(\d+)\D(\d+)\D(\d+)\D(\d+)"
 ```
 %% Output
    $\text{"(\d+)\D(\d+)\D(\d+)\D(\d+)"}$
    "(\d+)\D(\d+)\D(\d+)\D(\d+)"
 %% Cell type:code id: tags:
 ``` prob
 "\b"
 ```
 %% Output
    $\text{"\b"}$
    "\b"
 %% Cell type:markdown id: tags:
 ## LibraryProB
 This library provides various facilities which are very specific to ProB.
 You can obtain the definitions below by putting the following into your DEFINITIONS clause:
 `DEFINITIONS "LibraryProB.def"`
 The file `LibraryProB.def` is bundled with ProB and can be found in the `stdlib` folder.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE Jupyter_LibraryStrings
 DEFINITIONS "LibraryProB.def"
 END
 ```
 %% Output
    Loaded machine: Jupyter_LibraryStrings
 %% Cell type:markdown id: tags:
 With ```ASSERT_EXPR``` you can check assertions within expressions.
 Type: $BOOL \times STRING \times \tau \rightarrow \tau$.
 %% Cell type:code id: tags:
 ``` prob
 1+ASSERT_EXPR(bool(2>1),"err",3)
 ```
 %% Output
    $4$
    4
 %% Cell type:markdown id: tags:
 With ```ASSERT_TRUE``` you can check assertions within predicates.
 Signature: $BOOL \times STRING \times \tau$.
 %% Cell type:code id: tags:
 ``` prob
 ASSERT_TRUE(bool(2>1),"err") & 2>1
 ```
 %% Output
    $\mathit{TRUE}$
    TRUE
 %% Cell type:code id: tags:
 ``` prob
 x=0 & res=ASSERT_EXPR(bool(x>0),"arg not positive",10+x)
 ```
 %% Output
    :eval: UNKNOWN (FALSE with enumeration warning)
 %% Cell type:markdown id: tags:
 The function FORCE forces evaluation of symbolic set representations.
 Type: $POW(\tau) \rightarrow POW(\tau)$.
 %% Cell type:code id: tags:
 ``` prob
 FORCE( /*@symbolic */ { x | x:1..100 & x mod 2 = 0 } )
 ```
 %% Output
    $\{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\}$
    {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}
 %% Cell type:markdown id: tags:
 The function COPY can be used as an "enumeration barrier"; the value is copied only once it is fully known.
 Type: $\tau \rightarrow \tau$
 %% Cell type:code id: tags:
 ``` prob
 x:1..3 & y=COPY(x) & 9/y=3
 ```
 %% Output
    $\mathit{TRUE}$
    **Solution:**
    * $\mathit{x} = 3$
    * $\mathit{y} = 3$
    TRUE
    Solution:
    	x = 3
    	y = 3
 %% Cell type:markdown id: tags:
 ### Version
 This documentation was generated with the following version of ProB:
 %% Cell type:code id: tags:
 ``` prob
 :version
 ```
 %% Output
    ProB CLI: 1.9.0-beta8 (2a32153ac44523a5f93b0a999f9c42198b9360dc)
    ProB 2: 3.2.12-SNAPSHOT (16945773c7a5d9b44c1061db2a89cdd9e1da3cc3)
 %% Cell type:code id: tags:
 ``` prob
 ```