Skip to content
Snippets Groups Projects
Commit 8ad235f6 authored by dgelessus's avatar dgelessus
Browse files

Remove inline stdlib definitions 

Now that ClassicalBFactory.loadString has been fixed in the ProB 2
kernel, the stdlib can be used in ::load machines.
parent ffc69ec4
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
notebooks/manual/ExternalFunctions.ipynb
+ 126
− 241
View file @ 8ad235f6
%% 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
DEFINITIONS // "LibraryStrings.def"
STRING_LENGTH(xxx) == length(xxx);
EXTERNAL_FUNCTION_STRING_LENGTH == STRING --> INTEGER;
/* This external function takes two strings and concatenates them. */
STRING_APPEND(xxx,yyy) == append(xxx,yyy);
EXTERNAL_FUNCTION_STRING_APPEND == (STRING*STRING) --> STRING;
/* This external function takes a sequence of strings and concatenates them. */
STRING_CONC(string_conc_list) == "";
EXTERNAL_FUNCTION_STRING_CONC == seq(STRING) --> STRING;
/* This external function takes two strings and separates the first string
according to the separator specified by the second string. */
STRING_SPLIT(xxx,yyy) == split(xxx,yyy);
EXTERNAL_FUNCTION_STRING_SPLIT == ((STRING*STRING) --> (INTEGER<->STRING));
/* 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. */
STRING_JOIN(xxx,yyy) == join(xxx,yyy);
EXTERNAL_FUNCTION_STRING_JOIN == (((INTEGER<->STRING)*STRING) --> STRING);
STRING_CHARS(xxx) == chars(xxx);
EXTERNAL_FUNCTION_STRING_CHARS == (STRING --> (INTEGER<->STRING));
STRING_CODES(xxx) == codes(xxx);
EXTERNAL_FUNCTION_STRING_CODES == (STRING --> (INTEGER<->INTEGER));
/* 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 {\tt STRING\_IS\_INT} whether the conversion can be done. */
STRING_TO_INT(sss) == 0;
EXTERNAL_FUNCTION_STRING_TO_INT == (STRING --> INTEGER);
/* This external predicate takes a string and is true if the string represents an integer. */
STRING_IS_INT(sss) == (1=1);
EXTERNAL_PREDICATE_STRING_IS_INT == (STRING);
/* This external function takes a decimal string (with optional decimal places)
and converts it to an integer with the given precision. */
EXTERNAL_FUNCTION_DEC_STRING_TO_INT == STRING * INTEGER --> INTEGER;
DEC_STRING_TO_INT(decimal_string,precision) == 0;
/* parametric function; cannot be represented as constant function : */
STRING_TO_ENUM(sss) ==({}(1)); /* Note: you have to include the DEFINITION into your B file */
EXTERNAL_FUNCTION_STRING_TO_ENUM(STRING_TO_ENUM_TYPE) == (STRING --> STRING_TO_ENUM_TYPE);
TYPED_STRING_TO_ENUM(t,sss) ==({}(1));
EXTERNAL_FUNCTION_TYPED_STRING_TO_ENUM(STRING_TO_ENUM_TYPE) ==
(POW(STRING_TO_ENUM_TYPE)*STRING --> STRING_TO_ENUM_TYPE);
/* This external function converts an integer to a string representation. */
INT_TO_STRING(sss) == "0";
EXTERNAL_FUNCTION_INT_TO_STRING == (INTEGER --> STRING);
/* This external function converts an integer to a decimal string representation
with the precision provided by the second argument. */
INT_TO_DEC_STRING(integer,precision) == "0.0";
EXTERNAL_FUNCTION_INT_TO_DEC_STRING == (INTEGER*INTEGER --> STRING);
/* This external function converts a B data value to a string representation. */
TO_STRING(sss) == "0";
EXTERNAL_FUNCTION_TO_STRING(TO_STRING_TYPE) == (TO_STRING_TYPE --> 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.
*/
FORMAT_TO_STRING(MyFormatString,ListOfValues) == "0";
EXTERNAL_FUNCTION_FORMAT_TO_STRING(FORMAT_TO_STRING_TYPE) == ((STRING*seq(FORMAT_TO_STRING_TYPE)) --> STRING);
/* This external function checks whether the second string occurs contiguously within the first string. */
EXTERNAL_FUNCTION_STRING_CONTAINS_STRING == (STRING*STRING)--> BOOL;
STRING_CONTAINS_STRING(arg1,arg2)==FALSE; // TRUE when arg2 occurs as contiguous substring in arg1
MACHINE Jupyter_LibraryStrings
DEFINITIONS "LibraryStrings.def"
END
```
%% Output
[2018-05-13 09:48:02,007, T+3926] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[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,243, T+5162] "ProB Output Logger for instance 4f9c1863" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-13 09:48:03,263, T+5182] "ProB Output Logger for instance 4f9c1863" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-13 09:48:03,386, T+5305] "ProB Output Logger for instance 4f9c1863" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),Jupyter,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/manual])
[2018-05-16 13:20:12,877, T+5592] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-05-16 13:20:14,476, T+7191] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57016
[2018-05-16 13:20:14,478, T+7193] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1950
[2018-05-16 13:20:14,481, T+7196] "ProB Output Logger for instance 5406bd9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-16 13:20:14,504, T+7219] "ProB Output Logger for instance 5406bd9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-16 13:20:14,685, T+7400] "ProB Output Logger for instance 5406bd9a" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 12:58:57.712),Jupyter_LibraryStrings,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/manual,/Users/david/.prob/prob2-3.2.10-SNAPSHOT/stdlib/LibraryStrings.def])
Loaded machine: Jupyter : []
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
"abcabc"
%% Cell type:code id: tags:
``` prob
STRING_APPEND("abc","")
```
%% Output
"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
%% Cell type:code id: tags:
``` prob
STRING_LENGTH("")
```
%% Output
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↦"filename"),(2↦"ext")}
%% Cell type:code id: tags:
``` prob
STRING_SPLIT("filename.ext","/")
```
%% Output
{(1↦"filename.ext")}
%% Cell type:code id: tags:
``` prob
STRING_SPLIT("usr/local/lib","/")
```
%% Output
["usr","local","lib"]
%% Cell type:code id: tags:
``` prob
STRING_SPLIT("",".")
```
%% Output
{(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↦"usr/local/lib")}
%% Cell type:code id: tags:
``` prob
STRING_SPLIT("usr/local/lib","cal")
```
%% Output
{(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
"usr/local/lib"
%% Cell type:code id: tags:
``` prob
STRING_JOIN(["usr/lo","/lib"],"cal")
```
%% Output
"usr/local/lib"
%% Cell type:code id: tags:
``` prob
STRING_JOIN(["usr/local/lib"],"")
```
%% Output
"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
∅
%% Cell type:code id: tags:
``` prob
STRING_CHARS("abc")
```
%% Output
["a","b","c"]
%% Cell type:code id: tags:
``` prob
STRING_JOIN(STRING_CHARS("abc"),".")
```
%% Output
"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
∅
%% Cell type:code id: tags:
``` prob
STRING_CODES("AZ az 09")
```
%% Output
[65,90,32,97,122,32,48,57]
%% 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
TRUE
%% Cell type:code id: tags:
``` prob
STRING_IS_INT("-1204")
```
%% Output
TRUE
%% Cell type:code id: tags:
``` prob
STRING_IS_INT(" - 1204")
```
%% Output
TRUE
%% Cell type:code id: tags:
``` prob
STRING_IS_INT("1.1")
```
%% Output
FALSE
%% Cell type:code id: tags:
``` prob
STRING_IS_INT("1.0")
```
%% Output
FALSE
%% Cell type:code id: tags:
``` prob
STRING_IS_INT("a")
```
%% Output
FALSE
%% Cell type:code id: tags:
``` prob
STRING_IS_INT("1000000000000000000000000000")
```
%% Output
TRUE
%% Cell type:code id: tags:
``` prob
STRING_IS_INT("-00001")
```
%% Output
TRUE
%% Cell type:code id: tags:
``` prob
STRING_IS_INT("00002")
```
%% Output
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
%% Cell type:code id: tags:
``` prob
STRING_TO_INT(" - 00001")
```
%% Output
−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
"1024"
%% Cell type:code id: tags:
``` prob
INT_TO_STRING(-1024)
```
%% Output
"-1024"
%% Cell type:code id: tags:
``` prob
INT_TO_STRING(STRING_TO_INT(" - 00001"))
```
%% Output
"-1"
%% Cell type:code id: tags:
``` prob
STRING_TO_INT(INT_TO_STRING(-1))=-1
```
%% Output
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
%% Cell type:code id: tags:
``` prob
DEC_STRING_TO_INT("1024",2)
```
%% Output
102400
%% Cell type:code id: tags:
``` prob
DEC_STRING_TO_INT("1024",-1)
```
%% Output
102
%% Cell type:code id: tags:
``` prob
DEC_STRING_TO_INT("1025",-1)
```
%% Output
103
%% Cell type:code id: tags:
``` prob
DEC_STRING_TO_INT(" -1025",-1)
```
%% Output
−103
%% Cell type:code id: tags:
``` prob
DEC_STRING_TO_INT("1024.234",2)
```
%% Output
102423
%% Cell type:code id: tags:
``` prob
DEC_STRING_TO_INT("1024",100)
```
%% Output
10240000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
%% Cell type:code id: tags:
``` prob
DEC_STRING_TO_INT("10000000000000000000000000000000000",-32)=100
```
%% Output
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
"12.04"
%% Cell type:code id: tags:
``` prob
INT_TO_DEC_STRING(-1204,3)
```
%% Output
"-1.204"
%% Cell type:code id: tags:
``` prob
INT_TO_DEC_STRING(0,2)
```
%% Output
"0.00"
%% Cell type:code id: tags:
``` prob
INT_TO_DEC_STRING(1204,-2)
```
%% Output
"120400"
%% Cell type:code id: tags:
``` prob
INT_TO_DEC_STRING(-10,3)
```
%% Output
"-0.010"
%% 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
"1024"
%% Cell type:code id: tags:
``` prob
TO_STRING("1024")
```
%% Output
"1024"
%% Cell type:code id: tags:
``` prob
TO_STRING({2,3,5})
```
%% Output
"{2,3,5}"
%% Cell type:code id: tags:
``` prob
TO_STRING((TRUE,3,{11|->rec(a:22,b:33)}))
```
%% Output
"((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
"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
"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:
## Choose Operator
You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:
`DEFINITIONS "Choose.def"`
`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(XXX) == "a member of XXX";
EXTERNAL_FUNCTION_CHOOSE(CHOOSE_TYPE) == (POW(CHOOSE_TYPE)-->CHOOSE_TYPE)
END
DEFINITIONS "CHOOSE.def"
END
```
%% Output
[2018-05-13 09:48:06,965, T+8884] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[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,090, T+10009] "ProB Output Logger for instance 2f1db1bc" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-13 09:48:08,107, T+10026] "ProB Output Logger for instance 2f1db1bc" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-13 09:48:08,207, T+10126] "ProB Output Logger for instance 2f1db1bc" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),Jupyter_CHOOSE,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/manual])
[2018-05-16 13:20:18,426, T+11141] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-05-16 13:20:19,769, T+12484] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57053
[2018-05-16 13:20:19,770, T+12485] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1954
[2018-05-16 13:20:19,772, T+12487] "ProB Output Logger for instance 28964c5" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-16 13:20:19,796, T+12511] "ProB Output Logger for instance 28964c5" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-16 13:20:19,946, T+12661] "ProB Output Logger for instance 28964c5" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 12:58:57.712),Jupyter_CHOOSE,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/manual,/Users/david/.prob/prob2-3.2.10-SNAPSHOT/stdlib/CHOOSE.def])
Loaded machine: Jupyter_CHOOSE : []
%% Cell type:code id: tags:
``` prob
CHOOSE(1..3)
```
%% Output
1
%% Cell type:code id: tags:
``` prob
CHOOSE({1,2,3})
```
%% Output
1
%% Cell type:code id: tags:
``` prob
CHOOSE({"a","b","c"})
```
%% Output
"a"
%% Cell type:code id: tags:
``` prob
CHOOSE(NATURAL)
```
%% Output
0
%% Cell type:code id: tags:
``` prob
CHOOSE(INTEGER)
```
%% Output
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:
## 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_CHOOSE
DEFINITIONS
SORT(X) == [];
EXTERNAL_FUNCTION_SORT(T) == (POW(T)-->seq(T))
END
MACHINE Jupyter_SORT
DEFINITIONS "SORT.def"
END
```
%% Output
[2018-05-13 09:48:08,755, T+10674] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[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,937, T+11856] "ProB Output Logger for instance f4b34d8" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-13 09:48:09,963, T+11882] "ProB Output Logger for instance f4b34d8" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-13 09:48:10,084, T+12003] "ProB Output Logger for instance f4b34d8" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),Jupyter_CHOOSE,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/manual])
[2018-05-16 13:20:20,560, T+13275] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-05-16 13:20:22,110, T+14825] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57070
[2018-05-16 13:20:22,111, T+14826] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1958
[2018-05-16 13:20:22,114, T+14829] "ProB Output Logger for instance 1c63edfa" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-16 13:20:22,137, T+14852] "ProB Output Logger for instance 1c63edfa" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-16 13:20:22,280, T+14995] "ProB Output Logger for instance 1c63edfa" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 12:58:57.712),Jupyter_SORT,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/manual,/Users/david/.prob/prob2-3.2.10-SNAPSHOT/stdlib/SORT.def])
Loaded machine: Jupyter_CHOOSE : []
Loaded machine: Jupyter_SORT : []
%% Cell type:code id: tags:
``` prob
SORT(1..3)
```
%% Output
[1,2,3]
%% Cell type:code id: tags:
``` prob
SORT({3*3,3+3,3**3})
```
%% Output
[6,9,27]
%% Cell type:code id: tags:
``` prob
SORT({"ab","aa","a","b","10","1","2","11"})
```
%% Output
["1","10","11","2","a","aa","ab","b"]
%% Cell type:code id: tags:
``` prob
SORT({("a"|->1),("b"|->0),("a"|->0)})
```
%% Output
[("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:
## 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
DEFINITIONS
EXTERNAL_FUNCTION_PROB_INFO_STR == STRING --> STRING;
PROB_INFO_STR(info_field_name) == "";
EXTERNAL_FUNCTION_PROB_STATISTICS == STRING --> INTEGER;
PROB_STATISTICS(info_field_name) == 0;
EXTERNAL_FUNCTION_PROJECT_INFO == STRING --> POW(STRING);
PROJECT_INFO(info_field_name) == {};
EXTERNAL_FUNCTION_PROJECT_STATISTICS == STRING --> INTEGER;
PROJECT_STATISTICS(info_field_name) == 0;
EXTERNAL_FUNCTION_MACHINE_INFO == STRING * STRING --> STRING;
MACHINE_INFO(info_field_name,machine) == ""
MACHINE Jupyter_LibraryMeta
DEFINITIONS "LibraryMeta.def"
END
```
%% Output
[2018-05-13 10:25:48,398, T+2270317] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[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,670, T+2271589] "ProB Output Logger for instance 26a501d7" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-13 10:25:49,687, T+2271606] "ProB Output Logger for instance 26a501d7" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-13 10:25:49,803, T+2271722] "ProB Output Logger for instance 26a501d7" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),Jupyter,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/manual])
[2018-05-16 13:20:22,869, T+15584] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-05-16 13:20:24,234, T+16949] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57087
[2018-05-16 13:20:24,235, T+16950] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1962
[2018-05-16 13:20:24,237, T+16952] "ProB Output Logger for instance 742efc90" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-16 13:20:24,255, T+16970] "ProB Output Logger for instance 742efc90" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-16 13:20:24,405, T+17120] "ProB Output Logger for instance 742efc90" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 12:58:57.712),Jupyter_LibraryMeta,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/manual,/Users/david/.prob/prob2-3.2.10-SNAPSHOT/stdlib/LibraryMeta.def])
Loaded machine: Jupyter : []
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
"1.8.1-beta4"
%% Cell type:code id: tags:
``` prob
PROB_INFO_STR("prob-revision")
```
%% Output
"d30772a772f686c7972a16ddcb7fe9d79e4af54f"
"60150095a9bbe8cd7e75d9ef85686d632beb8840"
%% Cell type:code id: tags:
``` prob
PROB_INFO_STR("prob-last-changed-date")
```
%% Output
"Fri May 11 14:29:42 2018 +0200"
"Wed May 16 07:45:07 2018 +0200"
%% Cell type:code id: tags:
``` prob
PROB_INFO_STR("java-version")
```
%% Output
"1.8.0_152-b16"
"1.8.0_172-b11"
%% Cell type:code id: tags:
``` prob
PROB_INFO_STR("java-command-path")
```
%% Output
"/usr/bin/java"
"/Library/Java/JavaVirtualMachines/jdk1.8.0_172.jdk/Contents/Home/bin/java"
%% Cell type:code id: tags:
``` prob
PROB_INFO_STR("current-time")
```
%% Output
"13/5/2018 - 10h18 8s"
"16/5/2018 - 13h20 25s"
%% 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
150527440
150571952
%% Cell type:code id: tags:
``` prob
PROB_STATISTICS("states")
```
%% Output
1
%% Cell type:code id: tags:
``` prob
PROB_STATISTICS("transitions")
```
%% Output
0
%% Cell type:code id: tags:
``` prob
PROB_STATISTICS("processed-states")
```
%% Output
0
%% Cell type:code id: tags:
``` prob
PROB_STATISTICS("current-state-id")
```
%% Output
−1
%% Cell type:code id: tags:
``` prob
PROB_STATISTICS("now-timestamp")
```
%% Output
1526199415
1526469625
%% Cell type:code id: tags:
``` prob
PROB_STATISTICS("prolog-runtime")
```
%% Output
1320
1600
%% Cell type:code id: tags:
``` prob
PROB_STATISTICS("prolog-walltime")
```
%% Output
1054870
2600
%% 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
%% Cell type:code id: tags:
``` prob
PROJECT_STATISTICS("variables")
```
%% Output
0
%% Cell type:code id: tags:
``` prob
PROJECT_STATISTICS("properties")
```
%% Output
0
%% Cell type:code id: tags:
``` prob
PROJECT_STATISTICS("invariants")
```
%% Output
0
%% Cell type:code id: tags:
``` prob
PROJECT_STATISTICS("operations")
```
%% Output
0
%% Cell type:code id: tags:
``` prob
PROJECT_STATISTICS("static_assertions")
```
%% Output
0
%% Cell type:code id: tags:
``` prob
PROJECT_STATISTICS("dynamic_assertions")
```
%% Output
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
{"manual"}
{"LibraryMeta.def","manual"}
%% Cell type:code id: tags:
``` prob
PROJECT_INFO("main-file")
```
%% Output
{"from_string"}
%% Cell type:code id: tags:
``` prob
PROJECT_INFO("variables")
```
%% Output
∅
%% Cell type:code id: tags:
``` prob
PROJECT_INFO("constants")
```
%% Output
∅
%% Cell type:code id: tags:
``` prob
PROJECT_INFO("sets")
```
%% Output
∅
%% Cell type:code id: tags:
``` prob
PROJECT_INFO("operations")
```
%% Output
∅
%% Cell type:code id: tags:
``` prob
PROJECT_INFO("assertion_labels")
```
%% Output
∅
%% Cell type:code id: tags:
``` prob
PROJECT_INFO("invariant_labels")
```
%% Output
∅
%% 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 JupyterLibraryXML
DEFINITIONS
XML_ELement_Type ==
struct(
recId: NATURAL1,
pId:NATURAL,
element:STRING,
attributes: STRING +-> STRING,
meta: STRING +-> STRING
);
EXTERNAL_FUNCTION_READ_XML == (STRING * STRING) --> seq(XML_ELement_Type);
READ_XML(file,encoding) == {};
// encoding can be "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"
EXTERNAL_FUNCTION_READ_XML_FROM_STRING == STRING --> seq(XML_ELement_Type);
READ_XML_FROM_STRING(contents) == {};
EXTERNAL_FUNCTION_WRITE_XML_TO_STRING == seq(XML_ELement_Type) --> STRING;
WRITE_XML_TO_STRING(contents) == "<?xml ...?>";
EXTERNAL_PREDICATE_WRITE_XML == seq(XML_ELement_Type) * STRING;
WRITE_XML(contents,file) == (1=1)
END
MACHINE Jupyter_LibraryXML
DEFINITIONS "LibraryXML.def"
END
```
%% Output
[2018-05-14 10:43:17,767, T+2118174] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[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
[2018-05-14 10:43:19,132, T+2119539] "ProB Output Logger for instance 2fda6747" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-14 10:43:19,145, T+2119552] "ProB Output Logger for instance 2fda6747" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-14 10:43:19,271, T+2119678] "ProB Output Logger for instance 2fda6747" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),JupyterLibraryXML,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/manual])
[2018-05-16 13:20:26,472, T+19187] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-05-16 13:20:27,833, T+20548] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 57112
[2018-05-16 13:20:27,834, T+20549] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1967
[2018-05-16 13:20:27,836, T+20551] "ProB Output Logger for instance 136352e6" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-16 13:20:27,853, T+20568] "ProB Output Logger for instance 136352e6" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-16 13:20:27,989, T+20704] "ProB Output Logger for instance 136352e6" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 12:58:57.712),Jupyter_LibraryXML,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/manual,/Users/david/.prob/prob2-3.2.10-SNAPSHOT/stdlib/LibraryXML.def])
Loaded machine: JupyterLibraryXML : []
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
[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
[2018-05-16 13:20:28,298, T+21013] "ProB Output Logger for instance 136352e6" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Walltime 20 ms to parse and convert XML
{(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:code id: tags:
``` prob
```
......
notebooks/tests/external_functions.ipynb
+ 35
− 92
View file @ 8ad235f6
%% Cell type:markdown id: tags:
The following fails:
%% Cell type:code id: tags:
``` prob
::load
MACHINE Jupyter
DEFINITIONS "LibraryMeta.def"; "LibraryStrings.def"
END
```
%% Output
---------------------------------------------------------------------------
de.prob.exception.ProBError: ProB returned error messages:
Error: Definition file cannot be read: Loading of file content not supported.
at de.prob.scripting.ClassicalBFactory.parseString(ClassicalBFactory.java:137)
at de.prob.scripting.ClassicalBFactory.create(ClassicalBFactory.java:55)
at de.prob2.jupyter.commands.LoadCellCommand.run(LoadCellCommand.java:49)
at de.prob2.jupyter.ProBKernel.executeCellCommand(ProBKernel.java:98)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:168)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:282)
at io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$0(ShellChannel.java:50)
at java.lang.Thread.run(Thread.java:748)
at io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:39)
%% Cell type:markdown id: tags:
The following works:
%% Cell type:code id: tags:
``` prob
::load
MACHINE Jupyter
DEFINITIONS
EXTERNAL_FUNCTION_PROB_INFO_STR == STRING --> STRING;
PROB_INFO_STR(info_field_name) == "";
EXTERNAL_FUNCTION_PROB_STATISTICS == STRING --> INTEGER;
PROB_STATISTICS(info_field_name) == 0
END
```
%% Output
[2018-05-11 13:05:25,769, T+420396] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-05-11 13:05:26,896, T+421523] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 61716
[2018-05-11 13:05:26,896, T+421523] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 40215
[2018-05-11 13:05:26,898, T+421525] "ProB Output Logger for instance 502f39a7" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-11 13:05:26,922, T+421549] "ProB Output Logger for instance 502f39a7" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-11 13:05:27,034, T+421661] "ProB Output Logger for instance 502f39a7" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-04-11 12:07:37.302),Jupyter,[/Users/leuschel/git_root/JAVAPROB/prob2-jupyter-kernel/notebooks/tests])
[2018-05-16 13:05:41,328, T+7460] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-05-16 13:05:42,778, T+8910] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 50359
[2018-05-16 13:05:42,779, T+8911] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1835
[2018-05-16 13:05:42,783, T+8915] "ProB Output Logger for instance 62d429fd" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-16 13:05:42,801, T+8933] "ProB Output Logger for instance 62d429fd" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-16 13:05:42,973, T+9105] "ProB Output Logger for instance 62d429fd" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 12:58:57.712),Jupyter,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests,/Users/david/.prob/prob2-3.2.10-SNAPSHOT/stdlib/LibraryMeta.def,/Users/david/.prob/prob2-3.2.10-SNAPSHOT/stdlib/LibraryStrings.def])
Loaded machine: Jupyter : []
%% Cell type:code id: tags:
``` prob
PROB_INFO_STR("prob-version")
```
%% Output
"1.8.1-beta4"
%% Cell type:code id: tags:
``` prob
PROB_INFO_STR("java-version")
```
%% Output
"1.8.0_152-b16"
"1.8.0_172-b11"
%% Cell type:code id: tags:
``` prob
PROB_INFO_STR("prob-revision")
```
%% Output
"363372b41a2862e778657c124d58da965a3bdaf0"
"60150095a9bbe8cd7e75d9ef85686d632beb8840"
%% Cell type:code id: tags:
``` prob
PROB_STATISTICS("states")
```
%% Output
1
%% Cell type:code id: tags:
``` prob
PROB_STATISTICS("prolog-memory-bytes-used")
```
%% Output
150458528
150586816
%% Cell type:markdown id: tags:
The following fails because Java parser not available from within probcli:
%% Cell type:code id: tags:
``` prob
PROB_INFO_STR("parser-version")
```
%% Output
[2018-05-11 13:01:48,465, T+203092] "ProB Output Logger for instance 4dadeb3e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! An error occurred !
[2018-05-11 13:01:48,466, T+203093] "ProB Output Logger for instance 4dadeb3e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! source(parsercall)
[2018-05-11 13:01:48,466, T+203093] "ProB Output Logger for instance 4dadeb3e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! Unexpected error while parsing machine: 
[2018-05-11 13:01:48,467, T+203094] "ProB Output Logger for instance 4dadeb3e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! An error occurred !
[2018-05-11 13:01:48,467, T+203094] "ProB Output Logger for instance 4dadeb3e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! source(parsercall)
[2018-05-11 13:01:48,468, T+203095] "ProB Output Logger for instance 4dadeb3e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! Additional information: Error: Could not find or load main class de.prob.cliparser.CliBParser
[2018-05-11 13:01:48,469, T+203096] "ProB Output Logger for instance 4dadeb3e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! An error occurred !
[2018-05-11 13:01:48,469, T+203096] "ProB Output Logger for instance 4dadeb3e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! source(internal_error(parsercall))
[2018-05-11 13:01:48,470, T+203097] "ProB Output Logger for instance 4dadeb3e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! Java B parser (probcliparser.jar) is missing from lib directory in: /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/
[2018-05-16 13:06:07,175, T+33307] "ProB Output Logger for instance 62d429fd" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! An error occurred !
[2018-05-16 13:06:07,176, T+33308] "ProB Output Logger for instance 62d429fd" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! source(parsercall)
[2018-05-16 13:06:07,176, T+33308] "ProB Output Logger for instance 62d429fd" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! Unexpected error while parsing machine: 
[2018-05-16 13:06:07,177, T+33309] "ProB Output Logger for instance 62d429fd" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! An error occurred !
[2018-05-16 13:06:07,177, T+33309] "ProB Output Logger for instance 62d429fd" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! source(parsercall)
[2018-05-16 13:06:07,178, T+33310] "ProB Output Logger for instance 62d429fd" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! Additional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden
[2018-05-16 13:06:07,179, T+33311] "ProB Output Logger for instance 62d429fd" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! An error occurred !
[2018-05-16 13:06:07,179, T+33311] "ProB Output Logger for instance 62d429fd" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! source(internal_error(parsercall))
[2018-05-16 13:06:07,180, T+33312] "ProB Output Logger for instance 62d429fd" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! Java B parser (probcliparser.jar) is missing from lib directory in: /Users/david/.prob/prob2-3.2.10-SNAPSHOT/
NOT-WELL-DEFINED:
Unexpected error while parsing machine:
Additional information: Error: Could not find or load main class de.prob.cliparser.CliBParser
Additional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden
Java B parser (probcliparser.jar) is missing from lib directory in: /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/
%% Cell type:code id: tags:
``` prob
```
Java B parser (probcliparser.jar) is missing from lib directory in: /Users/david/.prob/prob2-3.2.10-SNAPSHOT/
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment