Skip to content
Snippets Groups Projects
Commit 04f87a4e authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add external functions tests

parent 808d2322
Branches
Tags
No related merge requests found
%% 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) == ""
END
```
%% Output
[2018-05-11 13:00:45,807, T+140434] "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:00:46,966, T+141593] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 61424
[2018-05-11 13:00:46,967, T+141594] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 40164
[2018-05-11 13:00:46,973, T+141600] "ProB Output Logger for instance 4dadeb3e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-11 13:00:46,997, T+141624] "ProB Output Logger for instance 4dadeb3e" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-11 13:00:47,107, T+141734] "ProB Output Logger for instance 4dadeb3e" 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])
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"
%% Cell type:code id: tags:
``` prob
PROB_INFO_STR("prob-revision")
```
%% Output
"363372b41a2862e778657c124d58da965a3bdaf0"
%% Cell type:code id: tags:
``` prob
PROB_STATISTICS("states")
```
%% Output
Computation not completed: Unknown identifier "PROB_STATISTICS"
%% Cell type:code id: tags:
``` prob
PROB_STATISTICS("prolog-memory-bytes-used")
```
%% 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/
NOT-WELL-DEFINED:
Unexpected error while parsing machine:
Additional information: Error: Could not find or load main class de.prob.cliparser.CliBParser
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
```
...@@ -5,7 +5,10 @@ ...@@ -5,7 +5,10 @@
## version ## version
Print out version of probcli running. Print out version of probcli running.
--> this could be implemented by allowing access to external functions in Jupyter --> this could be implemented by allowing access to external functions in Jupyter
PROB_INFO_STR("prob-version") would then return this information PROB_INFO_STR("prob-version") would then return this information.
To enable this one would need to load a machine
MACHINE Jupyter
DEFINITIONS "LibraryMeta.def"; "LibraryStrings.def" END
## z3/cvc4/kodkod: ## z3/cvc4/kodkod:
Allow predicates to be evaluated with an alternate backend Allow predicates to be evaluated with an alternate backend
...@@ -46,3 +49,27 @@ similar to :exec or -animate Nr probcli REPL commands ...@@ -46,3 +49,27 @@ similar to :exec or -animate Nr probcli REPL commands
### allow to execute other dot commands ### allow to execute other dot commands
i.e., machine hierarchy, ... i.e., machine hierarchy, ...
# Issues
## stdlib contents not available to ProB2 parser
::load
MACHINE Jupyter
DEFINITIONS "LibraryMeta.def"; "LibraryStrings.def"
END
generates
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)
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment