From 8ad235f6a699935b8b721caa152482ed6136dcef Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Wed, 16 May 2018 13:25:31 +0200
Subject: [PATCH] Remove inline stdlib definitions
Now that ClassicalBFactory.loadString has been fixed in the ProB 2
kernel, the stdlib can be used in ::load machines.
---
notebooks/manual/ExternalFunctions.ipynb | 367 ++++++++---------------
notebooks/tests/external_functions.ipynb | 127 +++-----
2 files changed, 161 insertions(+), 333 deletions(-)
diff --git a/notebooks/manual/ExternalFunctions.ipynb b/notebooks/manual/ExternalFunctions.ipynb
index 670463d..17f9e92 100644
--- a/notebooks/manual/ExternalFunctions.ipynb
+++ b/notebooks/manual/ExternalFunctions.ipynb
@@ -30,18 +30,18 @@
"name": "stdout",
"output_type": "stream",
"text": [
- "[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\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\n",
- "[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\n",
- "[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 --\u001b[0m\n",
- "[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\u001b[0m\n",
- "[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])\u001b[0m\n"
+ "[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\n",
+ "[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\n",
+ "[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\n",
+ "[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 --\u001b[0m\n",
+ "[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\u001b[0m\n",
+ "[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])\u001b[0m\n"
]
},
{
"data": {
"text/plain": [
- "Loaded machine: Jupyter : []\n"
+ "Loaded machine: Jupyter_LibraryStrings : []\n"
]
},
"execution_count": 1,
@@ -51,81 +51,8 @@
],
"source": [
"::load\n",
- "MACHINE Jupyter\n",
- "DEFINITIONS // \"LibraryStrings.def\"\n",
- " STRING_LENGTH(xxx) == length(xxx);\n",
- " EXTERNAL_FUNCTION_STRING_LENGTH == STRING --> INTEGER;\n",
- " \n",
- " /* This external function takes two strings and concatenates them. */\n",
- " STRING_APPEND(xxx,yyy) == append(xxx,yyy);\n",
- " EXTERNAL_FUNCTION_STRING_APPEND == (STRING*STRING) --> STRING;\n",
- "\n",
- " /* This external function takes a sequence of strings and concatenates them. */\n",
- " STRING_CONC(string_conc_list) == \"\";\n",
- " EXTERNAL_FUNCTION_STRING_CONC == seq(STRING) --> STRING;\n",
- " \n",
- " /* This external function takes two strings and separates the first string\n",
- " according to the separator specified by the second string. */\n",
- " STRING_SPLIT(xxx,yyy) == split(xxx,yyy);\n",
- " EXTERNAL_FUNCTION_STRING_SPLIT == ((STRING*STRING) --> (INTEGER<->STRING));\n",
- " \n",
- " /* This external function takes a sequence of strings and a separator string\n",
- " and joins the strings together inserting the separators as often as needed.\n",
- " It is the inverse of the STRING_SPLIT function. */\n",
- " STRING_JOIN(xxx,yyy) == join(xxx,yyy);\n",
- " EXTERNAL_FUNCTION_STRING_JOIN == (((INTEGER<->STRING)*STRING) --> STRING);\n",
- " \n",
- " STRING_CHARS(xxx) == chars(xxx);\n",
- " EXTERNAL_FUNCTION_STRING_CHARS == (STRING --> (INTEGER<->STRING));\n",
- " \n",
- " STRING_CODES(xxx) == codes(xxx);\n",
- " EXTERNAL_FUNCTION_STRING_CODES == (STRING --> (INTEGER<->INTEGER));\n",
- " \n",
- " /* This external function takes a string and converts it into an integer.\n",
- " An error is raised if this cannot be done.\n",
- " It is safer to first check with {\\tt STRING\\_IS\\_INT} whether the conversion can be done. */\n",
- " STRING_TO_INT(sss) == 0;\n",
- " EXTERNAL_FUNCTION_STRING_TO_INT == (STRING --> INTEGER);\n",
- " \n",
- " /* This external predicate takes a string and is true if the string represents an integer. */\n",
- " STRING_IS_INT(sss) == (1=1);\n",
- " EXTERNAL_PREDICATE_STRING_IS_INT == (STRING);\n",
- " \n",
- " /* This external function takes a decimal string (with optional decimal places)\n",
- " and converts it to an integer with the given precision. */\n",
- " EXTERNAL_FUNCTION_DEC_STRING_TO_INT == STRING * INTEGER --> INTEGER;\n",
- " DEC_STRING_TO_INT(decimal_string,precision) == 0;\n",
- " \n",
- " /* parametric function; cannot be represented as constant function : */\n",
- " STRING_TO_ENUM(sss) ==({}(1)); /* Note: you have to include the DEFINITION into your B file */\n",
- " EXTERNAL_FUNCTION_STRING_TO_ENUM(STRING_TO_ENUM_TYPE) == (STRING --> STRING_TO_ENUM_TYPE);\n",
- " TYPED_STRING_TO_ENUM(t,sss) ==({}(1));\n",
- " EXTERNAL_FUNCTION_TYPED_STRING_TO_ENUM(STRING_TO_ENUM_TYPE) == \n",
- " (POW(STRING_TO_ENUM_TYPE)*STRING --> STRING_TO_ENUM_TYPE);\n",
- " \n",
- " /* This external function converts an integer to a string representation. */\n",
- " INT_TO_STRING(sss) == \"0\";\n",
- " EXTERNAL_FUNCTION_INT_TO_STRING == (INTEGER --> STRING);\n",
- " \n",
- " /* This external function converts an integer to a decimal string representation\n",
- " with the precision provided by the second argument. */\n",
- " INT_TO_DEC_STRING(integer,precision) == \"0.0\";\n",
- " EXTERNAL_FUNCTION_INT_TO_DEC_STRING == (INTEGER*INTEGER --> STRING);\n",
- " \n",
- " /* This external function converts a B data value to a string representation. */\n",
- " TO_STRING(sss) == \"0\";\n",
- " EXTERNAL_FUNCTION_TO_STRING(TO_STRING_TYPE) == (TO_STRING_TYPE --> STRING);\n",
- " \n",
- " /* This external function takes a format string and a B sequence of values and generates an output\n",
- " string, where the values have been inserted into the format string in place of the ~w placeholders.\n",
- " */\n",
- " FORMAT_TO_STRING(MyFormatString,ListOfValues) == \"0\";\n",
- " EXTERNAL_FUNCTION_FORMAT_TO_STRING(FORMAT_TO_STRING_TYPE) == ((STRING*seq(FORMAT_TO_STRING_TYPE)) --> STRING);\n",
- " \n",
- " /* This external function checks whether the second string occurs contiguously within the first string. */\n",
- " EXTERNAL_FUNCTION_STRING_CONTAINS_STRING == (STRING*STRING)--> BOOL;\n",
- " STRING_CONTAINS_STRING(arg1,arg2)==FALSE; // TRUE when arg2 occurs as contiguous substring in arg1\n",
- "\n",
+ "MACHINE Jupyter_LibraryStrings\n",
+ "DEFINITIONS \"LibraryStrings.def\"\n",
"END"
]
},
@@ -1360,7 +1287,7 @@
"source": [
"## Choose Operator\n",
"You can obtain access to the definitions below by putting the following into your DEFINITIONS clause:\n",
- " `DEFINITIONS \"Choose.def\"`\n",
+ " `DEFINITIONS \"CHOOSE.def\"`\n",
"\n",
"### Choose\n",
"\n",
@@ -1384,12 +1311,12 @@
"name": "stdout",
"output_type": "stream",
"text": [
- "[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\n",
- "[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\n",
- "[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\n",
- "[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 --\u001b[0m\n",
- "[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\u001b[0m\n",
- "[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])\u001b[0m\n"
+ "[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\n",
+ "[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\n",
+ "[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\n",
+ "[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 --\u001b[0m\n",
+ "[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\u001b[0m\n",
+ "[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])\u001b[0m\n"
]
},
{
@@ -1406,10 +1333,8 @@
"source": [
"::load\n",
"MACHINE Jupyter_CHOOSE\n",
- "DEFINITIONS\n",
- " CHOOSE(XXX) == \"a member of XXX\";\n",
- " EXTERNAL_FUNCTION_CHOOSE(CHOOSE_TYPE) == (POW(CHOOSE_TYPE)-->CHOOSE_TYPE)\n",
- " END"
+ "DEFINITIONS \"CHOOSE.def\"\n",
+ "END"
]
},
{
@@ -1519,7 +1444,7 @@
"The operator is useful for writing WHILE loops or recursive functions which manipulate sets.\n",
"The following example defines a recursive summation function using the CHOOSE operator.\n",
"\n",
- "`\n",
+ "```\n",
"MACHINE RecursiveSigmaCHOOSEv3\n",
"DEFINITIONS\n",
" \"Choose.def\"\n",
@@ -1534,7 +1459,7 @@
"ASSERTIONS\n",
" sigma({3,5,7}) = 15;\n",
"END\n",
- "`"
+ "```"
]
},
{
@@ -1567,18 +1492,18 @@
"name": "stdout",
"output_type": "stream",
"text": [
- "[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\n",
- "[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\n",
- "[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\n",
- "[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 --\u001b[0m\n",
- "[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\u001b[0m\n",
- "[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])\u001b[0m\n"
+ "[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\n",
+ "[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\n",
+ "[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\n",
+ "[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 --\u001b[0m\n",
+ "[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\u001b[0m\n",
+ "[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])\u001b[0m\n"
]
},
{
"data": {
"text/plain": [
- "Loaded machine: Jupyter_CHOOSE : []\n"
+ "Loaded machine: Jupyter_SORT : []\n"
]
},
"execution_count": 60,
@@ -1588,11 +1513,9 @@
],
"source": [
"::load\n",
- "MACHINE Jupyter_CHOOSE\n",
- "DEFINITIONS\n",
- " SORT(X) == [];\n",
- " EXTERNAL_FUNCTION_SORT(T) == (POW(T)-->seq(T))\n",
- " END"
+ "MACHINE Jupyter_SORT\n",
+ "DEFINITIONS \"SORT.def\"\n",
+ "END"
]
},
{
@@ -1700,46 +1623,36 @@
},
{
"cell_type": "code",
- "execution_count": 84,
+ "execution_count": 65,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[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\n",
- "[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\n",
- "[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\n",
- "[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 --\u001b[0m\n",
- "[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\u001b[0m\n",
- "[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])\u001b[0m\n"
+ "[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\n",
+ "[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\n",
+ "[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\n",
+ "[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 --\u001b[0m\n",
+ "[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\u001b[0m\n",
+ "[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])\u001b[0m\n"
]
},
{
"data": {
"text/plain": [
- "Loaded machine: Jupyter : []\n"
+ "Loaded machine: Jupyter_LibraryMeta : []\n"
]
},
- "execution_count": 84,
+ "execution_count": 65,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"::load\n",
- "MACHINE Jupyter\n",
- "DEFINITIONS\n",
- " EXTERNAL_FUNCTION_PROB_INFO_STR == STRING --> STRING;\n",
- " PROB_INFO_STR(info_field_name) == \"\";\n",
- " EXTERNAL_FUNCTION_PROB_STATISTICS == STRING --> INTEGER;\n",
- " PROB_STATISTICS(info_field_name) == 0;\n",
- " EXTERNAL_FUNCTION_PROJECT_INFO == STRING --> POW(STRING);\n",
- " PROJECT_INFO(info_field_name) == {};\n",
- " EXTERNAL_FUNCTION_PROJECT_STATISTICS == STRING --> INTEGER;\n",
- " PROJECT_STATISTICS(info_field_name) == 0;\n",
- " EXTERNAL_FUNCTION_MACHINE_INFO == STRING * STRING --> STRING;\n",
- " MACHINE_INFO(info_field_name,machine) == \"\"\n",
+ "MACHINE Jupyter_LibraryMeta\n",
+ "DEFINITIONS \"LibraryMeta.def\"\n",
"END"
]
},
@@ -1754,7 +1667,7 @@
},
{
"cell_type": "code",
- "execution_count": 68,
+ "execution_count": 66,
"metadata": {},
"outputs": [
{
@@ -1763,7 +1676,7 @@
"\"1.8.1-beta4\""
]
},
- "execution_count": 68,
+ "execution_count": 66,
"metadata": {},
"output_type": "execute_result"
}
@@ -1774,16 +1687,16 @@
},
{
"cell_type": "code",
- "execution_count": 70,
+ "execution_count": 67,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "\"d30772a772f686c7972a16ddcb7fe9d79e4af54f\""
+ "\"60150095a9bbe8cd7e75d9ef85686d632beb8840\""
]
},
- "execution_count": 70,
+ "execution_count": 67,
"metadata": {},
"output_type": "execute_result"
}
@@ -1794,16 +1707,16 @@
},
{
"cell_type": "code",
- "execution_count": 82,
+ "execution_count": 68,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "\"Fri May 11 14:29:42 2018 +0200\""
+ "\"Wed May 16 07:45:07 2018 +0200\""
]
},
- "execution_count": 82,
+ "execution_count": 68,
"metadata": {},
"output_type": "execute_result"
}
@@ -1814,16 +1727,16 @@
},
{
"cell_type": "code",
- "execution_count": 71,
+ "execution_count": 69,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "\"1.8.0_152-b16\""
+ "\"1.8.0_172-b11\""
]
},
- "execution_count": 71,
+ "execution_count": 69,
"metadata": {},
"output_type": "execute_result"
}
@@ -1834,16 +1747,16 @@
},
{
"cell_type": "code",
- "execution_count": 80,
+ "execution_count": 70,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "\"/usr/bin/java\""
+ "\"/Library/Java/JavaVirtualMachines/jdk1.8.0_172.jdk/Contents/Home/bin/java\""
]
},
- "execution_count": 80,
+ "execution_count": 70,
"metadata": {},
"output_type": "execute_result"
}
@@ -1854,16 +1767,16 @@
},
{
"cell_type": "code",
- "execution_count": 81,
+ "execution_count": 71,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "\"13/5/2018 - 10h18 8s\""
+ "\"16/5/2018 - 13h20 25s\""
]
},
- "execution_count": 81,
+ "execution_count": 71,
"metadata": {},
"output_type": "execute_result"
}
@@ -1890,16 +1803,16 @@
},
{
"cell_type": "code",
- "execution_count": 73,
+ "execution_count": 72,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "150527440"
+ "150571952"
]
},
- "execution_count": 73,
+ "execution_count": 72,
"metadata": {},
"output_type": "execute_result"
}
@@ -1910,7 +1823,7 @@
},
{
"cell_type": "code",
- "execution_count": 74,
+ "execution_count": 73,
"metadata": {},
"outputs": [
{
@@ -1919,7 +1832,7 @@
"1"
]
},
- "execution_count": 74,
+ "execution_count": 73,
"metadata": {},
"output_type": "execute_result"
}
@@ -1930,7 +1843,7 @@
},
{
"cell_type": "code",
- "execution_count": 75,
+ "execution_count": 74,
"metadata": {},
"outputs": [
{
@@ -1939,7 +1852,7 @@
"0"
]
},
- "execution_count": 75,
+ "execution_count": 74,
"metadata": {},
"output_type": "execute_result"
}
@@ -1950,7 +1863,7 @@
},
{
"cell_type": "code",
- "execution_count": 76,
+ "execution_count": 75,
"metadata": {},
"outputs": [
{
@@ -1959,7 +1872,7 @@
"0"
]
},
- "execution_count": 76,
+ "execution_count": 75,
"metadata": {},
"output_type": "execute_result"
}
@@ -1970,7 +1883,7 @@
},
{
"cell_type": "code",
- "execution_count": 77,
+ "execution_count": 76,
"metadata": {},
"outputs": [
{
@@ -1979,7 +1892,7 @@
"−1"
]
},
- "execution_count": 77,
+ "execution_count": 76,
"metadata": {},
"output_type": "execute_result"
}
@@ -1990,16 +1903,16 @@
},
{
"cell_type": "code",
- "execution_count": 78,
+ "execution_count": 77,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "1526199415"
+ "1526469625"
]
},
- "execution_count": 78,
+ "execution_count": 77,
"metadata": {},
"output_type": "execute_result"
}
@@ -2010,16 +1923,16 @@
},
{
"cell_type": "code",
- "execution_count": 79,
+ "execution_count": 78,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "1320"
+ "1600"
]
},
- "execution_count": 79,
+ "execution_count": 78,
"metadata": {},
"output_type": "execute_result"
}
@@ -2030,16 +1943,16 @@
},
{
"cell_type": "code",
- "execution_count": 83,
+ "execution_count": 79,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "1054870"
+ "2600"
]
},
- "execution_count": 83,
+ "execution_count": 79,
"metadata": {},
"output_type": "execute_result"
}
@@ -2076,7 +1989,7 @@
},
{
"cell_type": "code",
- "execution_count": 86,
+ "execution_count": 80,
"metadata": {},
"outputs": [
{
@@ -2085,7 +1998,7 @@
"0"
]
},
- "execution_count": 86,
+ "execution_count": 80,
"metadata": {},
"output_type": "execute_result"
}
@@ -2096,7 +2009,7 @@
},
{
"cell_type": "code",
- "execution_count": 87,
+ "execution_count": 81,
"metadata": {},
"outputs": [
{
@@ -2105,7 +2018,7 @@
"0"
]
},
- "execution_count": 87,
+ "execution_count": 81,
"metadata": {},
"output_type": "execute_result"
}
@@ -2116,7 +2029,7 @@
},
{
"cell_type": "code",
- "execution_count": 88,
+ "execution_count": 82,
"metadata": {},
"outputs": [
{
@@ -2125,7 +2038,7 @@
"0"
]
},
- "execution_count": 88,
+ "execution_count": 82,
"metadata": {},
"output_type": "execute_result"
}
@@ -2136,7 +2049,7 @@
},
{
"cell_type": "code",
- "execution_count": 89,
+ "execution_count": 83,
"metadata": {},
"outputs": [
{
@@ -2145,7 +2058,7 @@
"0"
]
},
- "execution_count": 89,
+ "execution_count": 83,
"metadata": {},
"output_type": "execute_result"
}
@@ -2156,7 +2069,7 @@
},
{
"cell_type": "code",
- "execution_count": 90,
+ "execution_count": 84,
"metadata": {},
"outputs": [
{
@@ -2165,7 +2078,7 @@
"0"
]
},
- "execution_count": 90,
+ "execution_count": 84,
"metadata": {},
"output_type": "execute_result"
}
@@ -2176,7 +2089,7 @@
},
{
"cell_type": "code",
- "execution_count": 91,
+ "execution_count": 85,
"metadata": {},
"outputs": [
{
@@ -2185,7 +2098,7 @@
"0"
]
},
- "execution_count": 91,
+ "execution_count": 85,
"metadata": {},
"output_type": "execute_result"
}
@@ -2196,7 +2109,7 @@
},
{
"cell_type": "code",
- "execution_count": 92,
+ "execution_count": 86,
"metadata": {},
"outputs": [
{
@@ -2205,7 +2118,7 @@
"0"
]
},
- "execution_count": 92,
+ "execution_count": 86,
"metadata": {},
"output_type": "execute_result"
}
@@ -2225,16 +2138,16 @@
},
{
"cell_type": "code",
- "execution_count": 93,
+ "execution_count": 87,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "{\"manual\"}"
+ "{\"LibraryMeta.def\",\"manual\"}"
]
},
- "execution_count": 93,
+ "execution_count": 87,
"metadata": {},
"output_type": "execute_result"
}
@@ -2245,7 +2158,7 @@
},
{
"cell_type": "code",
- "execution_count": 100,
+ "execution_count": 88,
"metadata": {},
"outputs": [
{
@@ -2254,7 +2167,7 @@
"{\"from_string\"}"
]
},
- "execution_count": 100,
+ "execution_count": 88,
"metadata": {},
"output_type": "execute_result"
}
@@ -2265,7 +2178,7 @@
},
{
"cell_type": "code",
- "execution_count": 94,
+ "execution_count": 89,
"metadata": {},
"outputs": [
{
@@ -2274,7 +2187,7 @@
"∅"
]
},
- "execution_count": 94,
+ "execution_count": 89,
"metadata": {},
"output_type": "execute_result"
}
@@ -2285,7 +2198,7 @@
},
{
"cell_type": "code",
- "execution_count": 95,
+ "execution_count": 90,
"metadata": {},
"outputs": [
{
@@ -2294,7 +2207,7 @@
"∅"
]
},
- "execution_count": 95,
+ "execution_count": 90,
"metadata": {},
"output_type": "execute_result"
}
@@ -2305,7 +2218,7 @@
},
{
"cell_type": "code",
- "execution_count": 96,
+ "execution_count": 91,
"metadata": {},
"outputs": [
{
@@ -2314,7 +2227,7 @@
"∅"
]
},
- "execution_count": 96,
+ "execution_count": 91,
"metadata": {},
"output_type": "execute_result"
}
@@ -2325,7 +2238,7 @@
},
{
"cell_type": "code",
- "execution_count": 97,
+ "execution_count": 92,
"metadata": {},
"outputs": [
{
@@ -2334,7 +2247,7 @@
"∅"
]
},
- "execution_count": 97,
+ "execution_count": 92,
"metadata": {},
"output_type": "execute_result"
}
@@ -2345,7 +2258,7 @@
},
{
"cell_type": "code",
- "execution_count": 98,
+ "execution_count": 93,
"metadata": {},
"outputs": [
{
@@ -2354,7 +2267,7 @@
"∅"
]
},
- "execution_count": 98,
+ "execution_count": 93,
"metadata": {},
"output_type": "execute_result"
}
@@ -2365,7 +2278,7 @@
},
{
"cell_type": "code",
- "execution_count": 99,
+ "execution_count": 94,
"metadata": {},
"outputs": [
{
@@ -2374,7 +2287,7 @@
"∅"
]
},
- "execution_count": 99,
+ "execution_count": 94,
"metadata": {},
"output_type": "execute_result"
}
@@ -2417,7 +2330,7 @@
"An XML document is represented using the type seq(XML_ELement_Type), i.e., a sequence\n",
" of XML elements, whose type is defined by the following (included in the LibraryXML.def file):\n",
"\n",
- "`\n",
+ "```\n",
" XML_ELement_Type == \n",
" struct(\n",
" recId: NATURAL1,\n",
@@ -2426,7 +2339,7 @@
" attributes: STRING +-> STRING,\n",
" meta: STRING +-> STRING\n",
" );\n",
- "`\n",
+ "```\n",
"\n",
"### Files and Strings\n",
"\n",
@@ -2435,58 +2348,37 @@
},
{
"cell_type": "code",
- "execution_count": 1,
+ "execution_count": 95,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[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\n",
- "[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",
- "[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 --\u001b[0m\n",
- "[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\u001b[0m\n",
- "[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])\u001b[0m\n"
+ "[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\n",
+ "[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\n",
+ "[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\n",
+ "[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 --\u001b[0m\n",
+ "[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\u001b[0m\n",
+ "[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])\u001b[0m\n"
]
},
{
"data": {
"text/plain": [
- "Loaded machine: JupyterLibraryXML : []\n"
+ "Loaded machine: Jupyter_LibraryXML : []\n"
]
},
- "execution_count": 1,
+ "execution_count": 95,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"::load\n",
- "MACHINE JupyterLibraryXML\n",
- "DEFINITIONS\n",
- " XML_ELement_Type == \n",
- " struct(\n",
- " recId: NATURAL1,\n",
- " pId:NATURAL,\n",
- " element:STRING,\n",
- " attributes: STRING +-> STRING,\n",
- " meta: STRING +-> STRING\n",
- " );\n",
- " EXTERNAL_FUNCTION_READ_XML == (STRING * STRING) --> seq(XML_ELement_Type);\n",
- " READ_XML(file,encoding) == {}; \n",
- " // encoding can be \"auto\", \"ISO-8859-1\", \"ISO-8859-2\", \"ISO-8859-15\", \"UTF-8\", \"UTF-16\",\n",
- " // \"UTF-16LE\",\"UTF-16BE\",\"UTF-32\",\"UTF-32LE\",\"UTF-32BE\", \"ANSI_X3.4-1968\", \"windows 1252\"\n",
- " \n",
- " EXTERNAL_FUNCTION_READ_XML_FROM_STRING == STRING --> seq(XML_ELement_Type);\n",
- " READ_XML_FROM_STRING(contents) == {};\n",
- " \n",
- " EXTERNAL_FUNCTION_WRITE_XML_TO_STRING == seq(XML_ELement_Type) --> STRING;\n",
- " WRITE_XML_TO_STRING(contents) == \"<?xml ...?>\";\n",
- " \n",
- " EXTERNAL_PREDICATE_WRITE_XML == seq(XML_ELement_Type) * STRING;\n",
- " WRITE_XML(contents,file) == (1=1)\n",
- " END"
+ "MACHINE Jupyter_LibraryXML\n",
+ "DEFINITIONS \"LibraryXML.def\"\n",
+ "END"
]
},
{
@@ -2500,14 +2392,14 @@
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": 96,
"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-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\u001b[0m\n"
]
},
{
@@ -2516,7 +2408,7 @@
"{(1↦rec(attributes∈{(\"version\"↦\"0.1\")},element∈\"Data\",meta∈{(\"xmlLineNumber\"↦\"3\")},pId∈0,recId∈1)),(2↦rec(attributes∈{(\"attr1\"↦\"value1\"),(\"elemID\"↦\"ID1\")},element∈\"Tag1\",meta∈{(\"xmlLineNumber\"↦\"4\")},pId∈1,recId∈2))}"
]
},
- "execution_count": 2,
+ "execution_count": 96,
"metadata": {},
"output_type": "execute_result"
}
@@ -2545,13 +2437,6 @@
" \"UTF-8\",\"UTF-16\",\"UTF-16LE\",\"UTF-16BE\",\"UTF-32\",\"UTF-32LE\",\"UTF-32BE\",\n",
" \"ANSI\\_X3.4-1968\", \"windows 1252\"."
]
- },
- {
- "cell_type": "code",
- "execution_count": null,
- "metadata": {},
- "outputs": [],
- "source": []
}
],
"metadata": {
diff --git a/notebooks/tests/external_functions.ipynb b/notebooks/tests/external_functions.ipynb
index ed9bab2..00ed34a 100644
--- a/notebooks/tests/external_functions.ipynb
+++ b/notebooks/tests/external_functions.ipynb
@@ -1,66 +1,20 @@
{
"cells": [
- {
- "cell_type": "markdown",
- "metadata": {},
- "source": [
- "The following fails:"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 11,
- "metadata": {},
- "outputs": [
- {
- "ename": "ProBError",
- "evalue": "ProB returned error messages:\nError: Definition file cannot be read: Loading of file content not supported.",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m",
- "\u001b[1m\u001b[31mde.prob.exception.ProBError: ProB returned error messages:\u001b[0m",
- "\u001b[1m\u001b[31mError: Definition file cannot be read: Loading of file content not supported.\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob.scripting.ClassicalBFactory.parseString(ClassicalBFactory.java:137)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob.scripting.ClassicalBFactory.create(ClassicalBFactory.java:55)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.LoadCellCommand.run(LoadCellCommand.java:49)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCellCommand(ProBKernel.java:98)\u001b[0m",
- "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:168)\u001b[0m",
- "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:282)\u001b[0m",
- "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$0(ShellChannel.java:50)\u001b[0m",
- "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
- "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:39)\u001b[0m"
- ]
- }
- ],
- "source": [
- "::load\n",
- "MACHINE Jupyter\n",
- " DEFINITIONS \"LibraryMeta.def\"; \"LibraryStrings.def\"\n",
- "END"
- ]
- },
- {
- "cell_type": "markdown",
- "metadata": {},
- "source": [
- "The following works:"
- ]
- },
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 1,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[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\n",
- "[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\n",
- "[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\n",
- "[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 --\u001b[0m\n",
- "[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\u001b[0m\n",
- "[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])\u001b[0m\n"
+ "[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\n",
+ "[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\n",
+ "[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\n",
+ "[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 --\u001b[0m\n",
+ "[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\u001b[0m\n",
+ "[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])\u001b[0m\n"
]
},
{
@@ -69,7 +23,7 @@
"Loaded machine: Jupyter : []\n"
]
},
- "execution_count": 8,
+ "execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
@@ -77,17 +31,13 @@
"source": [
"::load\n",
"MACHINE Jupyter\n",
- "DEFINITIONS\n",
- " EXTERNAL_FUNCTION_PROB_INFO_STR == STRING --> STRING;\n",
- " PROB_INFO_STR(info_field_name) == \"\";\n",
- " EXTERNAL_FUNCTION_PROB_STATISTICS == STRING --> INTEGER;\n",
- " PROB_STATISTICS(info_field_name) == 0\n",
+ " DEFINITIONS \"LibraryMeta.def\"; \"LibraryStrings.def\"\n",
"END"
]
},
{
"cell_type": "code",
- "execution_count": 3,
+ "execution_count": 2,
"metadata": {},
"outputs": [
{
@@ -96,7 +46,7 @@
"\"1.8.1-beta4\""
]
},
- "execution_count": 3,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
@@ -107,16 +57,16 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "\"1.8.0_152-b16\""
+ "\"1.8.0_172-b11\""
]
},
- "execution_count": 4,
+ "execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
@@ -127,16 +77,16 @@
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "\"363372b41a2862e778657c124d58da965a3bdaf0\""
+ "\"60150095a9bbe8cd7e75d9ef85686d632beb8840\""
]
},
- "execution_count": 7,
+ "execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
@@ -147,7 +97,7 @@
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 5,
"metadata": {},
"outputs": [
{
@@ -156,7 +106,7 @@
"1"
]
},
- "execution_count": 9,
+ "execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
@@ -167,16 +117,16 @@
},
{
"cell_type": "code",
- "execution_count": 10,
+ "execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
- "150458528"
+ "150586816"
]
},
- "execution_count": 10,
+ "execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
@@ -194,50 +144,43 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 7,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-05-11 13:01:48,465, T+203092] \"ProB Output Logger for instance 4dadeb3e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[31m\u001b[1m! An error occurred !\u001b[0m\n",
- "[2018-05-11 13:01:48,466, T+203093] \"ProB Output Logger for instance 4dadeb3e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! source(parsercall)\u001b[0m\n",
- "[2018-05-11 13:01:48,466, T+203093] \"ProB Output Logger for instance 4dadeb3e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Unexpected error while parsing machine: \u001b[0m\n",
- "[2018-05-11 13:01:48,467, T+203094] \"ProB Output Logger for instance 4dadeb3e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! An error occurred !\u001b[0m\n",
- "[2018-05-11 13:01:48,467, T+203094] \"ProB Output Logger for instance 4dadeb3e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! source(parsercall)\u001b[0m\n",
- "[2018-05-11 13:01:48,468, T+203095] \"ProB Output Logger for instance 4dadeb3e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Additional information: Error: Could not find or load main class de.prob.cliparser.CliBParser\u001b[0m\n",
- "[2018-05-11 13:01:48,469, T+203096] \"ProB Output Logger for instance 4dadeb3e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! An error occurred !\u001b[0m\n",
- "[2018-05-11 13:01:48,469, T+203096] \"ProB Output Logger for instance 4dadeb3e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! source(internal_error(parsercall))\u001b[0m\n",
- "[2018-05-11 13:01:48,470, T+203097] \"ProB Output Logger for instance 4dadeb3e\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Java B parser (probcliparser.jar) is missing from lib directory in: /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/\u001b[0m\n"
+ "[2018-05-16 13:06:07,175, T+33307] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[31m\u001b[1m! An error occurred !\u001b[0m\n",
+ "[2018-05-16 13:06:07,176, T+33308] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! source(parsercall)\u001b[0m\n",
+ "[2018-05-16 13:06:07,176, T+33308] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Unexpected error while parsing machine: \u001b[0m\n",
+ "[2018-05-16 13:06:07,177, T+33309] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! An error occurred !\u001b[0m\n",
+ "[2018-05-16 13:06:07,177, T+33309] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! source(parsercall)\u001b[0m\n",
+ "[2018-05-16 13:06:07,178, T+33310] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Additional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\u001b[0m\n",
+ "[2018-05-16 13:06:07,179, T+33311] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! An error occurred !\u001b[0m\n",
+ "[2018-05-16 13:06:07,179, T+33311] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! source(internal_error(parsercall))\u001b[0m\n",
+ "[2018-05-16 13:06:07,180, T+33312] \"ProB Output Logger for instance 62d429fd\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Java B parser (probcliparser.jar) is missing from lib directory in: /Users/david/.prob/prob2-3.2.10-SNAPSHOT/\u001b[0m\n"
]
},
{
"ename": "UserErrorException",
- "evalue": "NOT-WELL-DEFINED: \nUnexpected error while parsing machine: \n\n\nAdditional information: Error: Could not find or load main class de.prob.cliparser.CliBParser\n\n\nJava B parser (probcliparser.jar) is missing from lib directory in: /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/\n\n",
+ "evalue": "NOT-WELL-DEFINED: \nUnexpected error while parsing machine: \n\n\nAdditional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\n\n\nJava B parser (probcliparser.jar) is missing from lib directory in: /Users/david/.prob/prob2-3.2.10-SNAPSHOT/\n\n",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[31mNOT-WELL-DEFINED: \u001b[0m",
"\u001b[1m\u001b[31mUnexpected error while parsing machine: \u001b[0m",
"\u001b[1m\u001b[31m\u001b[0m",
"\u001b[1m\u001b[31m\u001b[0m",
- "\u001b[1m\u001b[31mAdditional information: Error: Could not find or load main class de.prob.cliparser.CliBParser\u001b[0m",
+ "\u001b[1m\u001b[31mAdditional information: Fehler: Hauptklasse de.prob.cliparser.CliBParser konnte nicht gefunden oder geladen werden\u001b[0m",
"\u001b[1m\u001b[31m\u001b[0m",
"\u001b[1m\u001b[31m\u001b[0m",
- "\u001b[1m\u001b[31mJava B parser (probcliparser.jar) is missing from lib directory in: /Users/leuschel/.prob/prob2-3.2.10-SNAPSHOT/\u001b[0m"
+ "\u001b[1m\u001b[31mJava B parser (probcliparser.jar) is missing from lib directory in: /Users/david/.prob/prob2-3.2.10-SNAPSHOT/\u001b[0m"
]
}
],
"source": [
"PROB_INFO_STR(\"parser-version\")"
]
- },
- {
- "cell_type": "code",
- "execution_count": null,
- "metadata": {},
- "outputs": [],
- "source": []
}
],
"metadata": {
--
GitLab