"[2018-05-14 10:43:19,119, T+2119526] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 60266\n",
"[2018-05-14 10:43:19,120, T+2119527] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 71649\n",
"This external function takes an XML document string and converts into into the B format seq(XML_ELement_Type)}.\n",
"Note that all strings in ProB are encoded using UTF-8, so no encoding argument has to be provided."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[2018-05-14 10:44:22,117, T+2182524] \"ProB Output Logger for instance 2fda6747\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Walltime 10 ms to parse and convert XML\u001b[0m\n"
[2018-05-13 09:48:03,239, T+5158] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54031
[2018-05-13 09:48:03,239, T+5158] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54031
[2018-05-13 09:48:03,240, T+5159] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 62735
[2018-05-13 09:48:03,240, T+5159] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 62735
This external predicate takes a string and is true if the string represents an integer.
This external predicate takes a string and is true if the string represents an integer.
Type: $STRING $.
Type: $STRING $.
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
STRING_IS_INT("1204")
STRING_IS_INT("1204")
```
```
%% Output
%% Output
TRUE
TRUE
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
STRING_IS_INT("-1204")
STRING_IS_INT("-1204")
```
```
%% Output
%% Output
TRUE
TRUE
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
STRING_IS_INT(" - 1204")
STRING_IS_INT(" - 1204")
```
```
%% Output
%% Output
TRUE
TRUE
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
STRING_IS_INT("1.1")
STRING_IS_INT("1.1")
```
```
%% Output
%% Output
FALSE
FALSE
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
STRING_IS_INT("1.0")
STRING_IS_INT("1.0")
```
```
%% Output
%% Output
FALSE
FALSE
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
STRING_IS_INT("a")
STRING_IS_INT("a")
```
```
%% Output
%% Output
FALSE
FALSE
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
STRING_IS_INT("1000000000000000000000000000")
STRING_IS_INT("1000000000000000000000000000")
```
```
%% Output
%% Output
TRUE
TRUE
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
STRING_IS_INT("-00001")
STRING_IS_INT("-00001")
```
```
%% Output
%% Output
TRUE
TRUE
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
STRING_IS_INT("00002")
STRING_IS_INT("00002")
```
```
%% Output
%% Output
TRUE
TRUE
%% Cell type:markdown id: tags:
%% Cell type:markdown id: tags:
### STRING_TO_INT
### STRING_TO_INT
This external function takes a string and converts it into an integer.
This external function takes a string and converts it into an integer.
An error is raised if this cannot be done.
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.
It is safer to first check with `STRING_IS_INT` whether the conversion can be done.
Type: $STRING \rightarrow INTEGER$.
Type: $STRING \rightarrow INTEGER$.
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
STRING_TO_INT("1024")
STRING_TO_INT("1024")
```
```
%% Output
%% Output
1024
1024
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
STRING_TO_INT(" - 00001")
STRING_TO_INT(" - 00001")
```
```
%% Output
%% Output
−1
−1
%% Cell type:markdown id: tags:
%% Cell type:markdown id: tags:
### INT_TO_STRING
### INT_TO_STRING
This external function converts an integer to a string representation.
This external function converts an integer to a string representation.
Type: $INTEGER \rightarrow STRING $.
Type: $INTEGER \rightarrow STRING $.
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
INT_TO_STRING(1024)
INT_TO_STRING(1024)
```
```
%% Output
%% Output
"1024"
"1024"
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
INT_TO_STRING(-1024)
INT_TO_STRING(-1024)
```
```
%% Output
%% Output
"-1024"
"-1024"
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
INT_TO_STRING(STRING_TO_INT(" - 00001"))
INT_TO_STRING(STRING_TO_INT(" - 00001"))
```
```
%% Output
%% Output
"-1"
"-1"
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
STRING_TO_INT(INT_TO_STRING(-1))=-1
STRING_TO_INT(INT_TO_STRING(-1))=-1
```
```
%% Output
%% Output
TRUE
TRUE
%% Cell type:markdown id: tags:
%% Cell type:markdown id: tags:
### DEC_STRING_TO_INT
### 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 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 a B data value to a string representation.
This external function converts a B data value to a string representation.
Type: $\tau \rightarrow STRING$.
Type: $\tau \rightarrow STRING$.
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
TO_STRING(1024)
TO_STRING(1024)
```
```
%% Output
%% Output
"1024"
"1024"
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
TO_STRING("1024")
TO_STRING("1024")
```
```
%% Output
%% Output
"1024"
"1024"
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
TO_STRING({2,3,5})
TO_STRING({2,3,5})
```
```
%% Output
%% Output
"{2,3,5}"
"{2,3,5}"
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
TO_STRING((TRUE,3,{11|->rec(a:22,b:33)}))
TO_STRING((TRUE,3,{11|->rec(a:22,b:33)}))
```
```
%% Output
%% Output
"((TRUE|->3)|->{(11|->rec(a:22,b:33))})"
"((TRUE|->3)|->{(11|->rec(a:22,b:33))})"
%% Cell type:markdown id: tags:
%% Cell type:markdown id: tags:
### FORMAT_TO_STRING
### 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.
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 length of sequence must correspond to the number of `~w` in the format string.
- the format string follows the conventions of SICStus Prolog.
- the format string follows the conventions of SICStus Prolog.
E.g., one can use `~n` for newlines.
E.g., one can use `~n` for newlines.
Type: $(STRING*seq(\tau)) \rightarrow STRING$.
Type: $(STRING*seq(\tau)) \rightarrow STRING$.
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
FORMAT_TO_STRING("two to the power ten = ~w",[2**10])
FORMAT_TO_STRING("two to the power ten = ~w",[2**10])
```
```
%% Output
%% Output
"two to the power ten = 1024"
"two to the power ten = 1024"
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
FORMAT_TO_STRING("My two sets are ~w and ~w",[1..2,2..1])
FORMAT_TO_STRING("My two sets are ~w and ~w",[1..2,2..1])
```
```
%% Output
%% Output
"My two sets are {1,2} and {}"
"My two sets are {1,2} and {}"
%% Cell type:markdown id: tags:
%% Cell type:markdown id: tags:
#### Format Strings
#### Format Strings
Various external functions and predicates work with format strings.
Various external functions and predicates work with format strings.
ProB uses the conventions of the SICStus Prolog format string.
ProB uses the conventions of the SICStus Prolog format string.
-`~n` inserts a newline into the generated output
-`~n` inserts a newline into the generated output
-`~Nn` where N is a number: it inserts $N$ newlines into the output
-`~Nn` where N is a number: it inserts $N$ newlines into the output
-`~w` inserts the next argument into the generated 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
-`~i` consumes the next argument but ignores it; i.e., nothing is inserted into the output
-`~~` inserts the tilde symbol into the generated output
-`~~` inserts the tilde symbol into the generated output
-`~N` inserts a newline if not at the beginning of the line
-`~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.
SICStus Prolog also uses a few other formatting codes, such as `~@`, `~p`,... which should not be used.
%% Cell type:markdown id: tags:
%% Cell type:markdown id: tags:
## Choose Operator
## Choose Operator
You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:
You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:
`DEFINITIONS "Choose.def"`
`DEFINITIONS "Choose.def"`
### Choose
### Choose
This external function takes a set and returns an element of the set.
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
This is a proper mathematical function, i.e., it will always return the same value
given the same argument.
given the same argument.
It is also known as Hilbert's operator.
It is also known as Hilbert's operator.
The operator raises an error when it is called with an empty set.
The operator raises an error when it is called with an empty set.
Also, it is not guaranteed to work for infinite sets.
Also, it is not guaranteed to work for infinite sets.
[2018-05-13 09:48:08,087, T+10006] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54038
[2018-05-13 09:48:08,087, T+10006] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54038
[2018-05-13 09:48:08,088, T+10007] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 62740
[2018-05-13 09:48:08,088, T+10007] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 62740
[2018-05-13 09:48:09,935, T+11854] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54042
[2018-05-13 09:48:09,935, T+11854] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54042
[2018-05-13 09:48:09,935, T+11854] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 62744
[2018-05-13 09:48:09,935, T+11854] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 62744
[2018-05-13 10:25:49,665, T+2271584] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 56523
[2018-05-13 10:25:49,665, T+2271584] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 56523
[2018-05-13 10:25:49,666, T+2271585] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 63566
[2018-05-13 10:25:49,666, T+2271585] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 63566
This external function provides access to various information strings about ProB.
This external function provides access to various information strings about ProB.
Type: $STRING \rightarrow STRING$.
Type: $STRING \rightarrow STRING$.
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROB_INFO_STR("prob-version")
PROB_INFO_STR("prob-version")
```
```
%% Output
%% Output
"1.8.1-beta4"
"1.8.1-beta4"
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROB_INFO_STR("prob-revision")
PROB_INFO_STR("prob-revision")
```
```
%% Output
%% Output
"d30772a772f686c7972a16ddcb7fe9d79e4af54f"
"d30772a772f686c7972a16ddcb7fe9d79e4af54f"
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROB_INFO_STR("prob-last-changed-date")
PROB_INFO_STR("prob-last-changed-date")
```
```
%% Output
%% Output
"Fri May 11 14:29:42 2018 +0200"
"Fri May 11 14:29:42 2018 +0200"
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROB_INFO_STR("java-version")
PROB_INFO_STR("java-version")
```
```
%% Output
%% Output
"1.8.0_152-b16"
"1.8.0_152-b16"
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROB_INFO_STR("java-command-path")
PROB_INFO_STR("java-command-path")
```
```
%% Output
%% Output
"/usr/bin/java"
"/usr/bin/java"
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROB_INFO_STR("current-time")
PROB_INFO_STR("current-time")
```
```
%% Output
%% Output
"13/5/2018 - 10h18 8s"
"13/5/2018 - 10h18 8s"
%% Cell type:markdown id: tags:
%% Cell type:markdown id: tags:
Another command is PROB_INFO_STR("parser-version") which does not work within Jupyter.
Another command is PROB_INFO_STR("parser-version") which does not work within Jupyter.
%% Cell type:markdown id: tags:
%% Cell type:markdown id: tags:
### PROB_STATISTICS
### PROB_STATISTICS
This external function provides access to various statistics in the form of integers about ProB.
This external function provides access to various statistics in the form of integers about ProB.
Type: $STRING \rightarrow INTEGER$.
Type: $STRING \rightarrow INTEGER$.
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROB_STATISTICS("prolog-memory-bytes-used")
PROB_STATISTICS("prolog-memory-bytes-used")
```
```
%% Output
%% Output
150527440
150527440
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROB_STATISTICS("states")
PROB_STATISTICS("states")
```
```
%% Output
%% Output
1
1
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROB_STATISTICS("transitions")
PROB_STATISTICS("transitions")
```
```
%% Output
%% Output
0
0
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROB_STATISTICS("processed-states")
PROB_STATISTICS("processed-states")
```
```
%% Output
%% Output
0
0
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROB_STATISTICS("current-state-id")
PROB_STATISTICS("current-state-id")
```
```
%% Output
%% Output
−1
−1
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROB_STATISTICS("now-timestamp")
PROB_STATISTICS("now-timestamp")
```
```
%% Output
%% Output
1526199415
1526199415
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROB_STATISTICS("prolog-runtime")
PROB_STATISTICS("prolog-runtime")
```
```
%% Output
%% Output
1320
1320
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROB_STATISTICS("prolog-walltime")
PROB_STATISTICS("prolog-walltime")
```
```
%% Output
%% Output
1054870
1054870
%% Cell type:markdown id: tags:
%% Cell type:markdown id: tags:
Other possible information fields are prolog-memory-bytes-free,
Other possible information fields are prolog-memory-bytes-free,
prolog-global-stack-bytes-used,
prolog-global-stack-bytes-used,
prolog-local-stack-bytes-used,
prolog-local-stack-bytes-used,
prolog-global-stack-bytes-free,
prolog-global-stack-bytes-free,
prolog-local-stack-bytes-free,
prolog-local-stack-bytes-free,
prolog-trail-bytes-used,
prolog-trail-bytes-used,
prolog-choice-bytes-used,
prolog-choice-bytes-used,
prolog-atoms-bytes-used,
prolog-atoms-bytes-used,
prolog-atoms-nb-used,
prolog-atoms-nb-used,
prolog-gc-count,
prolog-gc-count,
prolog-gc-time.
prolog-gc-time.
%% Cell type:markdown id: tags:
%% Cell type:markdown id: tags:
### PROJECT_STATISTICS
### 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).
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$.
Type: $STRING \rightarrow INTEGER$.
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_STATISTICS("constants")
PROJECT_STATISTICS("constants")
```
```
%% Output
%% Output
0
0
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_STATISTICS("variables")
PROJECT_STATISTICS("variables")
```
```
%% Output
%% Output
0
0
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_STATISTICS("properties")
PROJECT_STATISTICS("properties")
```
```
%% Output
%% Output
0
0
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_STATISTICS("invariants")
PROJECT_STATISTICS("invariants")
```
```
%% Output
%% Output
0
0
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_STATISTICS("operations")
PROJECT_STATISTICS("operations")
```
```
%% Output
%% Output
0
0
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_STATISTICS("static_assertions")
PROJECT_STATISTICS("static_assertions")
```
```
%% Output
%% Output
0
0
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_STATISTICS("dynamic_assertions")
PROJECT_STATISTICS("dynamic_assertions")
```
```
%% Output
%% Output
0
0
%% Cell type:markdown id: tags:
%% Cell type:markdown id: tags:
### PROJECT_INFO
### PROJECT_INFO
This external function provides access to various information strings about the current specification being processed, with all auxiliary files (i.e., project).
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)$.
Type: $STRING \rightarrow POW(STRING)$.
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_INFO("files")
PROJECT_INFO("files")
```
```
%% Output
%% Output
{"manual"}
{"manual"}
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_INFO("main-file")
PROJECT_INFO("main-file")
```
```
%% Output
%% Output
{"from_string"}
{"from_string"}
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_INFO("variables")
PROJECT_INFO("variables")
```
```
%% Output
%% Output
∅
∅
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_INFO("constants")
PROJECT_INFO("constants")
```
```
%% Output
%% Output
∅
∅
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_INFO("sets")
PROJECT_INFO("sets")
```
```
%% Output
%% Output
∅
∅
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_INFO("operations")
PROJECT_INFO("operations")
```
```
%% Output
%% Output
∅
∅
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_INFO("assertion_labels")
PROJECT_INFO("assertion_labels")
```
```
%% Output
%% Output
∅
∅
%% Cell type:code id: tags:
%% Cell type:code id: tags:
``` prob
``` prob
PROJECT_INFO("invariant_labels")
PROJECT_INFO("invariant_labels")
```
```
%% Output
%% Output
∅
∅
%% Cell type:markdown id: tags:
%% Cell type:markdown id: tags:
## LibraryIO
## LibraryIO
This library provides various input/output facilities.
This library provides various input/output facilities.
It is probably most useful for debugging, but can also be used to write B machines
It is probably most useful for debugging, but can also be used to write B machines
which can read and write data.
which can read and write data.
You can obtain the definitions below by putting the following into your DEFINITIONS clause:
You can obtain the definitions below by putting the following into your DEFINITIONS clause:
`DEFINITIONS "LibraryIO.def"`
`DEFINITIONS "LibraryIO.def"`
The file `LibraryIO.def` is also bundled with ProB and can be found in the `stdlib` folder.
The file `LibraryIO.def` is also bundled with ProB and can be found in the `stdlib` folder.
%% Cell type:markdown id: tags:
%% Cell type:markdown id: tags:
## LibraryXML
## LibraryXML
This library provides various functions to read and write XML data from file and strings.
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:
You can obtain the definitions below by putting the following into your DEFINITIONS clause:
`DEFINITIONS "LibraryXML.def"`
`DEFINITIONS "LibraryXML.def"`
The file `LibraryXML.def` is also bundled with ProB and can be found in the `stdlib` folder.
The file `LibraryXML.def` is also bundled with ProB and can be found in the `stdlib` folder.
### Internal Data Type
### Internal Data Type
An XML document is represented using the type seq(XML_ELement_Type), i.e., a sequence
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):
of XML elements, whose type is defined by the following (included in the LibraryXML.def file):
`
`
XML_ELement_Type ==
XML_ELement_Type ==
struct(
struct(
recId: NATURAL1,
recId: NATURAL1,
pId:NATURAL,
pId:NATURAL,
element:STRING,
element:STRING,
attributes: STRING +-> STRING,
attributes: STRING +-> STRING,
meta: STRING +-> STRING
meta: STRING +-> STRING
);
);
`
`
### Files and Strings
### Files and Strings
XML documents can either be stored in a file or in a B string.
XML documents can either be stored in a file or in a B string.
[2018-05-14 10:43:19,119, T+2119526] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 60266
[2018-05-14 10:43:19,120, T+2119527] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 71649
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
[2018-05-14 10:44:22,117, T+2182524] "ProB Output Logger for instance 2fda6747" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Walltime 10 ms to parse and convert XML[0m