diff --git a/notebooks/manual/ExternalFunctions.ipynb b/notebooks/manual/ExternalFunctions.ipynb index f1e110b24c91eaa004bdc7ec5e9c5a10b11c76ca..4aa67b97547e6135319ecfbadb7e4a916cdc3387 100644 --- a/notebooks/manual/ExternalFunctions.ipynb +++ b/notebooks/manual/ExternalFunctions.ipynb @@ -1685,6 +1685,380 @@ "It should currently not be used for sets or sequences." ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## LibraryMeta\n", + "This library provides various meta information about ProB and the current model.\n", + "You can obtain the definitions below by putting the following into your DEFINITIONS clause:\n", + "\n", + "`DEFINITIONS \"LibraryMeta.def\"`\n", + "\n", + "The file `LibraryMeta.def` is also bundled with ProB and can be found in the `stdlib` folder." + ] + }, + { + "cell_type": "code", + "execution_count": 66, + "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" + ] + }, + { + "data": { + "text/plain": [ + "Loaded machine: Jupyter : []\n" + ] + }, + "execution_count": 66, + "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", + "END" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### PROB_INFO_STR\n", + "This external function provides access to various information strings about ProB.\n", + "Type: $STRING \\rightarrow STRING$." + ] + }, + { + "cell_type": "code", + "execution_count": 68, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "\"1.8.1-beta4\"" + ] + }, + "execution_count": 68, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PROB_INFO_STR(\"prob-version\")" + ] + }, + { + "cell_type": "code", + "execution_count": 70, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "\"d30772a772f686c7972a16ddcb7fe9d79e4af54f\"" + ] + }, + "execution_count": 70, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PROB_INFO_STR(\"prob-revision\")" + ] + }, + { + "cell_type": "code", + "execution_count": 82, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "\"Fri May 11 14:29:42 2018 +0200\"" + ] + }, + "execution_count": 82, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PROB_INFO_STR(\"prob-last-changed-date\")" + ] + }, + { + "cell_type": "code", + "execution_count": 71, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "\"1.8.0_152-b16\"" + ] + }, + "execution_count": 71, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PROB_INFO_STR(\"java-version\")" + ] + }, + { + "cell_type": "code", + "execution_count": 80, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "\"/usr/bin/java\"" + ] + }, + "execution_count": 80, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PROB_INFO_STR(\"java-command-path\")" + ] + }, + { + "cell_type": "code", + "execution_count": 81, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "\"13/5/2018 - 10h18 8s\"" + ] + }, + "execution_count": 81, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PROB_INFO_STR(\"current-time\")" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Another command is PROB_INFO_STR(\"parser-version\") which does not work within Jupyter." + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### PROB_STATISTICS\n", + "This external function provides access to various statistics in the form of integers about ProB.\n", + "Type: $STRING \\rightarrow INTEGER$." + ] + }, + { + "cell_type": "code", + "execution_count": 73, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "150527440" + ] + }, + "execution_count": 73, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PROB_STATISTICS(\"prolog-memory-bytes-used\")" + ] + }, + { + "cell_type": "code", + "execution_count": 74, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "1" + ] + }, + "execution_count": 74, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PROB_STATISTICS(\"states\")" + ] + }, + { + "cell_type": "code", + "execution_count": 75, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "0" + ] + }, + "execution_count": 75, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PROB_STATISTICS(\"transitions\")" + ] + }, + { + "cell_type": "code", + "execution_count": 76, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "0" + ] + }, + "execution_count": 76, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PROB_STATISTICS(\"processed-states\")" + ] + }, + { + "cell_type": "code", + "execution_count": 77, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "−1" + ] + }, + "execution_count": 77, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PROB_STATISTICS(\"current-state-id\")" + ] + }, + { + "cell_type": "code", + "execution_count": 78, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "1526199415" + ] + }, + "execution_count": 78, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PROB_STATISTICS(\"now-timestamp\")" + ] + }, + { + "cell_type": "code", + "execution_count": 79, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "1320" + ] + }, + "execution_count": 79, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PROB_STATISTICS(\"prolog-runtime\")" + ] + }, + { + "cell_type": "code", + "execution_count": 83, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "1054870" + ] + }, + "execution_count": 83, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "PROB_STATISTICS(\"prolog-walltime\")" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Other possible information fields are prolog-memory-bytes-free,\n", + "prolog-global-stack-bytes-used,\n", + "prolog-local-stack-bytes-used,\n", + "prolog-global-stack-bytes-free,\n", + "prolog-local-stack-bytes-free,\n", + "prolog-trail-bytes-used,\n", + "prolog-choice-bytes-used,\n", + "prolog-atoms-bytes-used,\n", + "prolog-atoms-nb-used,\n", + "prolog-gc-count,\n", + "prolog-gc-time." + ] + }, { "cell_type": "markdown", "metadata": {},