diff --git a/notebooks/manual/ExternalFunctions.ipynb b/notebooks/manual/ExternalFunctions.ipynb
index 4aa67b97547e6135319ecfbadb7e4a916cdc3387..42260be5e612f232c912b5b55f90b1315bc961c3 100644
--- a/notebooks/manual/ExternalFunctions.ipynb
+++ b/notebooks/manual/ExternalFunctions.ipynb
@@ -1700,19 +1700,19 @@
},
{
"cell_type": "code",
- "execution_count": 66,
+ "execution_count": 84,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
- "[2018-05-13 10:01:46,422, T+828341] \"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:01:47,612, T+829531] \"Shell-0\" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 54965\n",
- "[2018-05-13 10:01:47,612, T+829531] \"Shell-0\" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 63092\n",
- "[2018-05-13 10:01:47,615, T+829534] \"ProB Output Logger for instance 75f6d09c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --\u001b[0m\n",
- "[2018-05-13 10:01:47,634, T+829553] \"ProB Output Logger for instance 75f6d09c\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1\u001b[0m\n",
- "[2018-05-13 10:01:47,750, T+829669] \"ProB Output Logger for instance 75f6d09c\" 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-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"
]
},
{
@@ -1721,7 +1721,7 @@
"Loaded machine: Jupyter : []\n"
]
},
- "execution_count": 66,
+ "execution_count": 84,
"metadata": {},
"output_type": "execute_result"
}
@@ -1730,10 +1730,16 @@
"::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_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",
"END"
]
},
@@ -2059,6 +2065,324 @@
"prolog-gc-time."
]
},
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### PROJECT_STATISTICS\n",
+ "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).\n",
+ "Type: $STRING \\rightarrow INTEGER$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 86,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 86,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_STATISTICS(\"constants\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 87,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 87,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_STATISTICS(\"variables\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 88,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 88,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_STATISTICS(\"properties\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 89,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 89,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_STATISTICS(\"invariants\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 90,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 90,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_STATISTICS(\"operations\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 91,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 91,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_STATISTICS(\"static_assertions\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 92,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "0"
+ ]
+ },
+ "execution_count": 92,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_STATISTICS(\"dynamic_assertions\")"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "### PROJECT_INFO\n",
+ "This external function provides access to various information strings about the current specification being processed, with all auxiliary files (i.e., project).\n",
+ "Type: $STRING \\rightarrow POW(STRING)$."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 93,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "{\"manual\"}"
+ ]
+ },
+ "execution_count": 93,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"files\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 100,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "{\"from_string\"}"
+ ]
+ },
+ "execution_count": 100,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"main-file\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 94,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 94,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"variables\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 95,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 95,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"constants\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 96,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 96,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"sets\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 97,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 97,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"operations\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 98,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 98,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"assertion_labels\")"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 99,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "∅"
+ ]
+ },
+ "execution_count": 99,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "PROJECT_INFO(\"invariant_labels\")"
+ ]
+ },
{
"cell_type": "markdown",
"metadata": {},