diff --git a/manual/ExternalFunctions.ipynb b/manual/ExternalFunctions.ipynb
index 2df761098c987f7da69cd75be058056578db364c..638e130093e6d1398c774b397b24305cc65b02f2 100644
--- a/manual/ExternalFunctions.ipynb
+++ b/manual/ExternalFunctions.ipynb
@@ -4116,7 +4116,7 @@
},
{
"cell_type": "code",
- "execution_count": 121,
+ "execution_count": 1,
"metadata": {},
"outputs": [
{
@@ -4125,7 +4125,7 @@
"Loaded machine: Jupyter_LibraryXML"
]
},
- "execution_count": 121,
+ "execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
@@ -4148,19 +4148,19 @@
},
{
"cell_type": "code",
- "execution_count": 122,
+ "execution_count": 2,
"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))\\}$"
+ "$\\{(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,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
@@ -5396,6 +5396,275 @@
"REGEX_SEARCH_ALL(\"0123\",\"[[:alpha:]]+\")"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### Ignoring case \n",
+ "\n",
+ "As of ProB 1.12.0 the above functions also have counterparts which ignore the case. The names of the functions have and additional I (for Ignore case). Here are a few examples to illustrate their behaviour."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{FALSE}$"
+ ],
+ "text/plain": [
+ "FALSE"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_MATCH(\"abC\",\"(a|b|c)+\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\mathit{TRUE}$"
+ ],
+ "text/plain": [
+ "TRUE"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_IMATCH(\"abC\",\"(a|b|c)+\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"ab\"}$"
+ ],
+ "text/plain": [
+ "\"ab\""
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH(\"abCabCdABC\",1,\"(a|b|c)+\")'string"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"abCabC\"}$"
+ ],
+ "text/plain": [
+ "\"abCabC\""
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_ISEARCH(\"abCabCdABC\",1,\"(a|b|c)+\")'string"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"ab\"}$"
+ ],
+ "text/plain": [
+ "\"ab\""
+ ]
+ },
+ "execution_count": 16,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_STR(\"abCabCdABC\",\"(a|b|c)+\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"abCabC\"}$"
+ ],
+ "text/plain": [
+ "\"abCabC\""
+ ]
+ },
+ "execution_count": 17,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_ISEARCH_STR(\"abCabCdABC\",\"(a|b|c)+\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"ab\"}),(2\\mapsto\\text{\"ab\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"ab\"),(2↦\"ab\")}"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_SEARCH_ALL(\"abCabCdABC\",\"(a|b|c)+\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"abCabC\"}),(2\\mapsto\\text{\"ABC\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"abCabC\"),(2↦\"ABC\")}"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_ISEARCH_ALL(\"abCabCdABC\",\"(a|b|c)+\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"*C*CdABC\"}$"
+ ],
+ "text/plain": [
+ "\"*C*CdABC\""
+ ]
+ },
+ "execution_count": 13,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_REPLACE(\"abCabCdABC\",\"(a|b|c)+\",\"*\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\text{\"*d*\"}$"
+ ],
+ "text/plain": [
+ "\"*d*\""
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_IREPLACE(\"abCabCdABC\",\"(a|b|c)+\",\"*\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Note that there was a bug in the C++ regular expression library used by ProB in GCC prior to version 8.1. If ProB was built using GCC (on Linux) with an older version the next call may behave differently. The bug means that in a range only the first character (here a) is treated in a case insensitive fashion (and not the entire range)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 18,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(1\\mapsto\\text{\"aBC\"}),(2\\mapsto\\text{\"abZ\"}),(3\\mapsto\\text{\"AA\"})\\}$"
+ ],
+ "text/plain": [
+ "{(1↦\"aBC\"),(2↦\"abZ\"),(3↦\"AA\")}"
+ ]
+ },
+ "execution_count": 18,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "REGEX_ISEARCH_ALL(\"aBC abZ AA\",\"[a-z]+\")"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {},
@@ -6234,7 +6503,7 @@
],
"source": [
"::load\n",
- "MACHINE Jupyter_LibraryStrings\n",
+ "MACHINE Jupyter_LibraryProB\n",
"DEFINITIONS \"LibraryProB.def\"\n",
"END"
]
@@ -6393,6 +6662,268 @@
"x:1..3 & y=COPY(x) & 9/y=3"
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "## LibraryBits\n",
+ "You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:\n",
+ " `DEFINITIONS \"LibraryBits.def\"`"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 20,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: Jupyter_LibraryBits"
+ ]
+ },
+ "execution_count": 20,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "::load\n",
+ "MACHINE Jupyter_LibraryBits\n",
+ "DEFINITIONS \"LibraryBits.def\"\n",
+ "END"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 21,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$6$"
+ ],
+ "text/plain": [
+ "6"
+ ]
+ },
+ "execution_count": 21,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "BOR(2,4)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 22,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$6$"
+ ],
+ "text/plain": [
+ "6"
+ ]
+ },
+ "execution_count": 22,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "BOR(2,6)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 23,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$2$"
+ ],
+ "text/plain": [
+ "2"
+ ]
+ },
+ "execution_count": 23,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "BAND(2,6)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 24,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$4$"
+ ],
+ "text/plain": [
+ "4"
+ ]
+ },
+ "execution_count": 24,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "BXOR(2,6)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 25,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$14$"
+ ],
+ "text/plain": [
+ "14"
+ ]
+ },
+ "execution_count": 25,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "BXOR(0xf,1)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 26,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$16$"
+ ],
+ "text/plain": [
+ "16"
+ ]
+ },
+ "execution_count": 26,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "BLSHIFT(8,1)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 27,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$64$"
+ ],
+ "text/plain": [
+ "64"
+ ]
+ },
+ "execution_count": 27,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "BLSHIFT(16,2)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 32,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$8$"
+ ],
+ "text/plain": [
+ "8"
+ ]
+ },
+ "execution_count": 32,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "BRSHIFT(16,1)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 33,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$32$"
+ ],
+ "text/plain": [
+ "32"
+ ]
+ },
+ "execution_count": 33,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "BRSHIFT(16,-1)"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 36,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$-15$"
+ ],
+ "text/plain": [
+ "−15"
+ ]
+ },
+ "execution_count": 36,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "BNOT(14)"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {},