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.
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).
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).
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
$151477456$
151477456
%% 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
$1582035160$
1582035160
$1582036192$
1582036192
%% Cell type:code id: tags:
``` prob
PROB_STATISTICS("prolog-runtime")
```
%% Output
$1691$
1691
$1658$
1658
%% Cell type:code id: tags:
``` prob
PROB_STATISTICS("prolog-walltime")
```
%% Output
$3040$
3040
$2881$
2881
%% 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"}
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.
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.
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.
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
$\{(1\mapsto\text{"\\"}),(2\mapsto\text{"\""})\}$
{(1↦"\\"),(2↦"\"")}
%% 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.
![](data:image/svg+xml;utf8,<?xml version="1.0" encoding="UTF-8" standalone="no"?><!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN""http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"><!-- Generated by graphviz version 2.40.1 (20161225.0304)--><!-- Title: state Pages: 1 --><svg width="176pt" height="131pt"viewBox="0.00 0.00 176.00 131.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink"><g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 127)"><title>state</title><polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-127 172,-127 172,4 -4,4"/><!-- 4 --><g id="node1" class="node"><title>4</title><polygon fill="#cdba96" stroke="#cdba96" points="54,-123 0,-123 0,-87 54,-87 54,-123"/><text text-anchor="middle" x="27" y="-101.3" font-family="Times,serif" font-size="14.00" fill="#000000">4</text></g><!-- 3 --><g id="node2" class="node"><title>3</title><polygon fill="#cdba96" stroke="#cdba96" points="73,-36 19,-36 19,0 73,0 73,-36"/><text text-anchor="middle" x="46" y="-14.3" font-family="Times,serif" font-size="14.00" fill="#000000">3</text></g><!-- 4->3 --><g id="edge1" class="edge"><title>4->3</title><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"/><polygon fill="#b22222" stroke="#b22222" points="17.6245,-46.1306 21.5364,-36.2844 12.3382,-41.542 17.6245,-46.1306"/><text text-anchor="middle" x="16.5" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">rel</text></g><!-- 3->4 --><g id="edge2" class="edge"><title>3->4</title><path fill="none" stroke="#b22222" d="M42.0682,-36.0034C39.4963,-47.7801 36.0828,-63.4102 33.1552,-76.8156"/><polygon fill="#b22222" stroke="#b22222" points="29.6511,-76.457 30.9368,-86.9735 36.4899,-77.9506 29.6511,-76.457"/><text text-anchor="middle" x="45.5" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">rel</text></g><!-- 2 --><g id="node3" class="node"><title>2</title><polygon fill="#cdba96" stroke="#cdba96" points="149,-123 95,-123 95,-87 149,-87 149,-123"/><text text-anchor="middle" x="122" y="-101.3" font-family="Times,serif" font-size="14.00" fill="#000000">2</text></g><!-- 2->3 --><g id="edge3" class="edge"><title>2->3</title><path fill="none" stroke="#b22222" d="M106.2528,-86.9735C95.3492,-74.4919 80.6716,-57.6899 68.533,-43.7944"/><polygon fill="#b22222" stroke="#b22222" points="70.9419,-41.2319 61.7271,-36.0034 65.6701,-45.8371 70.9419,-41.2319"/><text text-anchor="middle" x="95.5" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">rel</text></g><!-- 1 --><g id="node4" class="node"><title>1</title><polygon fill="#cdba96" stroke="#cdba96" points="168,-36 114,-36 114,0 168,0 168,-36"/><text text-anchor="middle" x="141" y="-14.3" font-family="Times,serif" font-size="14.00" fill="#000000">1</text></g><!-- 2->1 --><g id="edge4" class="edge"><title>2->1</title><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"/><polygon fill="#b22222" stroke="#b22222" points="129.0662,-46.6305 130.0081,-36.0776 122.6909,-43.7398 129.0662,-46.6305"/><text text-anchor="middle" x="130.5" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">rel</text></g><!-- 1->2 --><g id="edge5" class="edge"><title>1->2</title><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"/><polygon fill="#b22222" stroke="#b22222" points="132.1613,-76.1836 131.6235,-86.7648 138.6425,-78.8284 132.1613,-76.1836"/><text text-anchor="middle" x="147.5" y="-57.8" font-family="Times,serif" font-size="14.00" fill="#000000">rel</text></g></g></svg>)