From 1f9ec3ac6ea6362fcc92639c128b186e89d901e5 Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Mon, 25 Jun 2018 17:26:17 +0200 Subject: [PATCH] Add full help messages for all commands --- notebooks/tests/animate.ipynb | 44 +++++++++-- notebooks/tests/assert.ipynb | 14 +++- notebooks/tests/dot.ipynb | 74 +++++++++++++++++- notebooks/tests/eval.ipynb | 37 +++++---- notebooks/tests/groovy.ipynb | 13 +++- notebooks/tests/help.ipynb | 78 ++++++++++++++----- notebooks/tests/load_cell.ipynb | 70 ++++++++++++++--- notebooks/tests/load_file.ipynb | 64 ++++++++++++--- notebooks/tests/pref.ipynb | 24 +++++- notebooks/tests/prettyprint.ipynb | 17 +++- notebooks/tests/render.ipynb | 17 +++- notebooks/tests/show.ipynb | 10 ++- notebooks/tests/solve.ipynb | 49 ++++++++---- notebooks/tests/table.ipynb | 13 +++- notebooks/tests/time.ipynb | 28 +++++-- notebooks/tests/type.ipynb | 13 +++- notebooks/tests/version.ipynb | 13 ++-- .../prob2/jupyter/commands/AssertCommand.java | 6 ++ .../prob2/jupyter/commands/BrowseCommand.java | 7 +- .../de/prob2/jupyter/commands/Command.java | 2 + .../jupyter/commands/ConstantsCommand.java | 7 +- .../de/prob2/jupyter/commands/DotCommand.java | 25 +++++- .../prob2/jupyter/commands/EvalCommand.java | 10 ++- .../prob2/jupyter/commands/ExecCommand.java | 8 +- .../prob2/jupyter/commands/GroovyCommand.java | 5 ++ .../prob2/jupyter/commands/HelpCommand.java | 19 ++++- .../jupyter/commands/InitialiseCommand.java | 5 ++ .../jupyter/commands/LoadCellCommand.java | 8 +- .../jupyter/commands/LoadFileCommand.java | 6 ++ .../prob2/jupyter/commands/PrefCommand.java | 6 ++ .../jupyter/commands/PrettyPrintCommand.java | 6 ++ .../prob2/jupyter/commands/RenderCommand.java | 6 ++ .../prob2/jupyter/commands/ShowCommand.java | 5 ++ .../prob2/jupyter/commands/SolveCommand.java | 48 +++++------- .../prob2/jupyter/commands/TableCommand.java | 5 ++ .../prob2/jupyter/commands/TimeCommand.java | 6 ++ .../prob2/jupyter/commands/TypeCommand.java | 5 ++ .../jupyter/commands/VersionCommand.java | 7 +- 38 files changed, 633 insertions(+), 147 deletions(-) diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb index bc367a0..4c62bf7 100644 --- a/notebooks/tests/animate.ipynb +++ b/notebooks/tests/animate.ipynb @@ -12,12 +12,18 @@ ":browse\n", "```\n", "\n", - "Show information about the current state" + "Show information about the current state.\n", + "\n", + "The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of transitions that are available in the current state. Each transition has a numeric ID, which can be passed to `:exec` to execute that transition." ], "text/plain": [ + "```\n", ":browse\n", + "```\n", "\n", - "Show information about the current state" + "Show information about the current state.\n", + "\n", + "The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of transitions that are available in the current state. Each transition has a numeric ID, which can be passed to `:exec` to execute that transition." ] }, "execution_count": 1, @@ -42,13 +48,23 @@ ":exec OPERATION_ID\n", "```\n", "\n", - "Execute an operation with the specified predicate, or by its ID" + "Execute an operation with the specified predicate, or by its ID.\n", + "\n", + "In the first form, the given operation is executed. If the optional predicate is specified, a transition is found for which the predicate is $\\mathit{TRUE}$. The predicate can be used to restrict what values the operation's parameters or the variables in the next state may have.\n", + "\n", + "In the second form, a known transition with the given numeric ID is executed. A list of the current state's available transitions and their IDs can be viewed using `:browse`. Only transition IDs from the current state can be executed." ], "text/plain": [ + "```\n", ":exec OPERATION [PREDICATE]\n", ":exec OPERATION_ID\n", + "```\n", + "\n", + "Execute an operation with the specified predicate, or by its ID.\n", "\n", - "Execute an operation with the specified predicate, or by its ID" + "In the first form, the given operation is executed. If the optional predicate is specified, a transition is found for which the predicate is $\\mathit{TRUE}$. The predicate can be used to restrict what values the operation's parameters or the variables in the next state may have.\n", + "\n", + "In the second form, a known transition with the given numeric ID is executed. A list of the current state's available transitions and their IDs can be viewed using `:browse`. Only transition IDs from the current state can be executed." ] }, "execution_count": 2, @@ -72,12 +88,18 @@ ":constants [PREDICATE]\n", "```\n", "\n", - "Set up the current machine's constants with the specified predicate" + "Set up the current machine's constants.\n", + "\n", + "This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`." ], "text/plain": [ + "```\n", ":constants [PREDICATE]\n", + "```\n", + "\n", + "Set up the current machine's constants.\n", "\n", - "Set up the current machine's constants with the specified predicate" + "This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`." ] }, "execution_count": 3, @@ -101,12 +123,18 @@ ":init [PREDICATE]\n", "```\n", "\n", - "Initialise the current machine with the specified predicate" + "Initialise the current machine with the specified predicate\n", + "\n", + "This is a shorthand for `:exec INITIALISATION [PREDICATE]`." ], "text/plain": [ + "```\n", ":init [PREDICATE]\n", + "```\n", + "\n", + "Initialise the current machine with the specified predicate\n", "\n", - "Initialise the current machine with the specified predicate" + "This is a shorthand for `:exec INITIALISATION [PREDICATE]`." ] }, "execution_count": 4, diff --git a/notebooks/tests/assert.ipynb b/notebooks/tests/assert.ipynb index 8e79a0f..6ae6b79 100644 --- a/notebooks/tests/assert.ipynb +++ b/notebooks/tests/assert.ipynb @@ -12,12 +12,22 @@ ":assert PREDICATE\n", "```\n", "\n", - "Ensure that the predicate is true, and show an error otherwise." + "Ensure that the predicate is true, and show an error otherwise.\n", + "\n", + "This command is intended for verifying that a predicate is always true at a certain point in a notebook. Unlike normal evaluation (`:eval`), this command treats a $\\mathit{FALSE}$ result as an error. If the result is $\\mathit{TRUE}$, solutions for free variables (if any) are not displayed.\n", + "\n", + "Only predicates and $\\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error." ], "text/plain": [ + "```\n", ":assert PREDICATE\n", + "```\n", + "\n", + "Ensure that the predicate is true, and show an error otherwise.\n", + "\n", + "This command is intended for verifying that a predicate is always true at a certain point in a notebook. Unlike normal evaluation (`:eval`), this command treats a $\\mathit{FALSE}$ result as an error. If the result is $\\mathit{TRUE}$, solutions for free variables (if any) are not displayed.\n", "\n", - "Ensure that the predicate is true, and show an error otherwise." + "Only predicates and $\\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error." ] }, "execution_count": 1, diff --git a/notebooks/tests/dot.ipynb b/notebooks/tests/dot.ipynb index 5f54acb..c0bd454 100644 --- a/notebooks/tests/dot.ipynb +++ b/notebooks/tests/dot.ipynb @@ -12,12 +12,62 @@ ":dot COMMAND [FORMULA]\n", "```\n", "\n", - "Execute and show a dot visualization." + "Execute and show a dot visualisation.\n", + "\n", + "The following dot visualisation commands are available:\n", + "\n", + "* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model\n", + "* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model (**Not available for this machine/state**: only available for Event-B models)\n", + "* `state_space` - State Space: Show state space\n", + "* `state_space_sfdp` - State Space (Fast): Show state space (fast)\n", + "* `signature_merge` - Signature Merge: Show signature-merged reduced state space\n", + "* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)\n", + "* `state_as_graph` - State Graph: Show values in current state as a graph\n", + "* `custom_graph` - Customized State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES (**Not available for this machine/state**: only available when CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine)\n", + "* `invariant` - Invariant Formula Tree: Show invariant as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n", + "* `properties` - Properties Formula Tree: Show properties as a formula tree\n", + "* `assertions` - Assertions Formula Tree: Show assertions as a formula tree\n", + "* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n", + "* `goal` - Goal Formula Tree: Show GOAL as a formula tree\n", + "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree (**Not available for this machine/state**: only available when error occured)\n", + "* `enable_graph` - Enable Graph: Show enabling graph of events\n", + "* `dependence_graph` - Dependence Graph: Show dependence graph of events\n", + "* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n", + "* `expr_as_graph` - Expression Graph: Show expression value as a graph (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n", + "* `formula_tree` - Formula Tree: Show predicate and sub-expressions as a tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n", + "* `transition_diagram` - Transition Diagram Projection: Project state space onto expression values\n", + "* `predicate_dependency` - Predicate Dependency Graph: Show dependence graph of conjuncts of a predicate\n" ], "text/plain": [ + "```\n", ":dot COMMAND [FORMULA]\n", + "```\n", + "\n", + "Execute and show a dot visualisation.\n", + "\n", + "The following dot visualisation commands are available:\n", "\n", - "Execute and show a dot visualization." + "* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model\n", + "* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model (**Not available for this machine/state**: only available for Event-B models)\n", + "* `state_space` - State Space: Show state space\n", + "* `state_space_sfdp` - State Space (Fast): Show state space (fast)\n", + "* `signature_merge` - Signature Merge: Show signature-merged reduced state space\n", + "* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)\n", + "* `state_as_graph` - State Graph: Show values in current state as a graph\n", + "* `custom_graph` - Customized State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES (**Not available for this machine/state**: only available when CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine)\n", + "* `invariant` - Invariant Formula Tree: Show invariant as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n", + "* `properties` - Properties Formula Tree: Show properties as a formula tree\n", + "* `assertions` - Assertions Formula Tree: Show assertions as a formula tree\n", + "* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n", + "* `goal` - Goal Formula Tree: Show GOAL as a formula tree\n", + "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree (**Not available for this machine/state**: only available when error occured)\n", + "* `enable_graph` - Enable Graph: Show enabling graph of events\n", + "* `dependence_graph` - Dependence Graph: Show dependence graph of events\n", + "* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n", + "* `expr_as_graph` - Expression Graph: Show expression value as a graph (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n", + "* `formula_tree` - Formula Tree: Show predicate and sub-expressions as a tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models)\n", + "* `transition_diagram` - Transition Diagram Projection: Project state space onto expression values\n", + "* `predicate_dependency` - Predicate Dependency Graph: Show dependence graph of conjuncts of a predicate\n" ] }, "execution_count": 1, @@ -29,6 +79,26 @@ ":help :dot" ] }, + { + "cell_type": "code", + "execution_count": 2, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Preference changed: DOT = /opt/local/bin/dot\n" + ] + }, + "execution_count": 2, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":pref DOT=/opt/local/bin/dot" + ] + }, { "cell_type": "code", "execution_count": 3, diff --git a/notebooks/tests/eval.ipynb b/notebooks/tests/eval.ipynb index c1ff1ec..d3bc385 100644 --- a/notebooks/tests/eval.ipynb +++ b/notebooks/tests/eval.ipynb @@ -9,15 +9,25 @@ "data": { "text/markdown": [ "```\n", - ":eval EXPRESSION\n", + ":eval FORMULA\n", "```\n", "\n", - "Evaluate an expression." + "Evaluate a formula and display the result.\n", + "\n", + "This is equivalent to inputting the formula without a command name.\n", + "\n", + "If the formula is a $\\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed." ], "text/plain": [ - ":eval EXPRESSION\n", + "```\n", + ":eval FORMULA\n", + "```\n", + "\n", + "Evaluate a formula and display the result.\n", + "\n", + "This is equivalent to inputting the formula without a command name.\n", "\n", - "Evaluate an expression." + "If the formula is a $\\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed." ] }, "execution_count": 1, @@ -166,10 +176,10 @@ { "data": { "text/markdown": [ - "$TRUE$\n", + "$\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $xx = 3$" + "* $\\mathit{xx} = 3$" ], "text/plain": [ "TRUE\n", @@ -195,11 +205,11 @@ { "data": { "text/markdown": [ - "$TRUE$\n", + "$\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $xx = 3$\n", - "* $yy = 4$" + "* $\\mathit{xx} = 3$\n", + "* $\\mathit{yy} = 4$" ], "text/plain": [ "TRUE\n", @@ -330,11 +340,11 @@ { "data": { "text/markdown": [ - "$TRUE$\n", + "$\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $xx = 3$\n", - "* $yy = 4$" + "* $\\mathit{xx} = 3$\n", + "* $\\mathit{yy} = 4$" ], "text/plain": [ "TRUE\n", @@ -388,8 +398,9 @@ "name": "prob2" }, "language_info": { + "codemirror_mode": "prob2_jupyter_repl", "file_extension": ".prob", - "mimetype": "text/x-prob", + "mimetype": "text/x-prob2-jupyter-repl", "name": "prob" } }, diff --git a/notebooks/tests/groovy.ipynb b/notebooks/tests/groovy.ipynb index 0943f9d..d4838cd 100644 --- a/notebooks/tests/groovy.ipynb +++ b/notebooks/tests/groovy.ipynb @@ -12,12 +12,18 @@ ":groovy EXPRESSION\n", "```\n", "\n", - "Evaluate the given Groovy expression." + "Evaluate the given Groovy expression.\n", + "\n", + "The standard ProB 2 Groovy environment is used to evaluate the expression, so ProB 2's global `api` and `animations` objects may be used to load machines and manipulate traces." ], "text/plain": [ + "```\n", ":groovy EXPRESSION\n", + "```\n", + "\n", + "Evaluate the given Groovy expression.\n", "\n", - "Evaluate the given Groovy expression." + "The standard ProB 2 Groovy environment is used to evaluate the expression, so ProB 2's global `api` and `animations` objects may be used to load machines and manipulate traces." ] }, "execution_count": 1, @@ -106,8 +112,9 @@ "name": "prob2" }, "language_info": { + "codemirror_mode": "prob2_jupyter_repl", "file_extension": ".prob", - "mimetype": "text/x-prob", + "mimetype": "text/x-prob2-jupyter-repl", "name": "prob" } }, diff --git a/notebooks/tests/help.ipynb b/notebooks/tests/help.ipynb index d601de4..8489fd0 100644 --- a/notebooks/tests/help.ipynb +++ b/notebooks/tests/help.ipynb @@ -17,45 +17,49 @@ "text/markdown": [ "Type a valid B expression, or one of the following commands:\n", "\n", - "* `::load` Load the machine source code from the body.\n", + "* `::load` Load the machine source code given in the cell body.\n", "* `::render` Render some content with the specified MIME type.\n", "* `:assert` Ensure that the predicate is true, and show an error otherwise.\n", - "* `:browse` Show information about the current state\n", - "* `:constants` Set up the current machine's constants with the specified predicate\n", - "* `:eval` Evaluate an expression.\n", - "* `:exec` Execute an operation with the specified predicate, or by its ID\n", + "* `:browse` Show information about the current state.\n", + "* `:constants` Set up the current machine's constants.\n", + "* `:dot` Execute and show a dot visualisation.\n", + "* `:eval` Evaluate a formula and display the result.\n", + "* `:exec` Execute an operation with the specified predicate, or by its ID.\n", "* `:groovy` Evaluate the given Groovy expression.\n", "* `:help` Display help for a specific command, or general help about the REPL.\n", "* `:init` Initialise the current machine with the specified predicate\n", "* `:load` Load the machine from the given path.\n", "* `:pref` View or change the value of one or more preferences.\n", "* `:prettyprint` Pretty-print a predicate.\n", - "* `:solve` Solve a predicate with the specified solver\n", + "* `:show` Show the machine's animation function visualisation for the current state.\n", + "* `:solve` Solve a predicate with the specified solver.\n", "* `:table` Display an expression as a table.\n", "* `:time` Execute the given command and measure how long it takes to execute.\n", "* `:type` Display the type of a formula.\n", - "* `:version` Display version info about the ProB CLI and ProB 2\n" + "* `:version` Display version info about the ProB CLI and ProB 2.\n" ], "text/plain": [ "Type a valid B expression, or one of the following commands:\n", - "::load Load the machine source code from the body.\n", + "::load Load the machine source code given in the cell body.\n", "::render Render some content with the specified MIME type.\n", ":assert Ensure that the predicate is true, and show an error otherwise.\n", - ":browse Show information about the current state\n", - ":constants Set up the current machine's constants with the specified predicate\n", - ":eval Evaluate an expression.\n", - ":exec Execute an operation with the specified predicate, or by its ID\n", + ":browse Show information about the current state.\n", + ":constants Set up the current machine's constants.\n", + ":dot Execute and show a dot visualisation.\n", + ":eval Evaluate a formula and display the result.\n", + ":exec Execute an operation with the specified predicate, or by its ID.\n", ":groovy Evaluate the given Groovy expression.\n", ":help Display help for a specific command, or general help about the REPL.\n", ":init Initialise the current machine with the specified predicate\n", ":load Load the machine from the given path.\n", ":pref View or change the value of one or more preferences.\n", ":prettyprint Pretty-print a predicate.\n", - ":solve Solve a predicate with the specified solver\n", + ":show Show the machine's animation function visualisation for the current state.\n", + ":solve Solve a predicate with the specified solver.\n", ":table Display an expression as a table.\n", ":time Execute the given command and measure how long it takes to execute.\n", ":type Display the type of a formula.\n", - ":version Display version info about the ProB CLI and ProB 2\n" + ":version Display version info about the ProB CLI and ProB 2.\n" ] }, "execution_count": 1, @@ -82,7 +86,9 @@ "Display help for a specific command, or general help about the REPL." ], "text/plain": [ + "```\n", ":help [COMMAND]\n", + "```\n", "\n", "Display help for a specific command, or general help about the REPL." ] @@ -108,12 +114,22 @@ ":load FILENAME [PREF=VALUE ...]\n", "```\n", "\n", - "Load the machine from the given path." + "Load the machine from the given path.\n", + "\n", + "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n", + "\n", + "Any number of preference assignments may be included after the file path. Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded." ], "text/plain": [ + "```\n", ":load FILENAME [PREF=VALUE ...]\n", + "```\n", "\n", - "Load the machine from the given path." + "Load the machine from the given path.\n", + "\n", + "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n", + "\n", + "Any number of preference assignments may be included after the file path. Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded." ] }, "execution_count": 3, @@ -140,15 +156,25 @@ "END\n", "```\n", "\n", - "Load the machine source code from the body." + "Load the machine source code given in the cell body.\n", + "\n", + "There must be a newline between the `::load` command name and the machine code.\n", + "\n", + "Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded." ], "text/plain": [ + "```\n", "::load [PREF=VALUE ...]\n", "MACHINE\n", "...\n", "END\n", + "```\n", + "\n", + "Load the machine source code given in the cell body.\n", + "\n", + "There must be a newline between the `::load` command name and the machine code.\n", "\n", - "Load the machine source code from the body." + "Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded." ] }, "execution_count": 4, @@ -182,7 +208,9 @@ "Display help for a specific command, or general help about the REPL." ], "text/plain": [ + "```\n", ":help [COMMAND]\n", + "```\n", "\n", "Display help for a specific command, or general help about the REPL." ] @@ -208,12 +236,22 @@ ":load FILENAME [PREF=VALUE ...]\n", "```\n", "\n", - "Load the machine from the given path." + "Load the machine from the given path.\n", + "\n", + "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n", + "\n", + "Any number of preference assignments may be included after the file path. Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded." ], "text/plain": [ + "```\n", ":load FILENAME [PREF=VALUE ...]\n", + "```\n", + "\n", + "Load the machine from the given path.\n", + "\n", + "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n", "\n", - "Load the machine from the given path." + "Any number of preference assignments may be included after the file path. Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded." ] }, "execution_count": 6, diff --git a/notebooks/tests/load_cell.ipynb b/notebooks/tests/load_cell.ipynb index ed36c15..6f2d327 100644 --- a/notebooks/tests/load_cell.ipynb +++ b/notebooks/tests/load_cell.ipynb @@ -1,5 +1,50 @@ { "cells": [ + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "```\n", + "::load [PREF=VALUE ...]\n", + "MACHINE\n", + "...\n", + "END\n", + "```\n", + "\n", + "Load the machine source code given in the cell body.\n", + "\n", + "There must be a newline between the `::load` command name and the machine code.\n", + "\n", + "Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded." + ], + "text/plain": [ + "```\n", + "::load [PREF=VALUE ...]\n", + "MACHINE\n", + "...\n", + "END\n", + "```\n", + "\n", + "Load the machine source code given in the cell body.\n", + "\n", + "There must be a newline between the `::load` command name and the machine code.\n", + "\n", + "Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded." + ] + }, + "execution_count": 1, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":help ::load" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -9,7 +54,7 @@ }, { "cell_type": "code", - "execution_count": 1, + "execution_count": 2, "metadata": {}, "outputs": [ { @@ -18,7 +63,7 @@ "Loaded machine: things : []\n" ] }, - "execution_count": 1, + "execution_count": 2, "metadata": {}, "output_type": "execute_result" } @@ -32,16 +77,19 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 3, "metadata": {}, "outputs": [ { "data": { + "text/markdown": [ + "$\\{\\mathit{ONE},\\mathit{TWO},\\mathit{THREE},\\mathit{FOUR}\\}$" + ], "text/plain": [ "{ONE,TWO,THREE,FOUR}" ] }, - "execution_count": 2, + "execution_count": 3, "metadata": {}, "output_type": "execute_result" } @@ -59,7 +107,7 @@ }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 4, "metadata": {}, "outputs": [ { @@ -68,7 +116,7 @@ "Loaded machine: prefs : []\n" ] }, - "execution_count": 3, + "execution_count": 4, "metadata": {}, "output_type": "execute_result" } @@ -81,16 +129,19 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 5, "metadata": {}, "outputs": [ { "data": { + "text/markdown": [ + "$\\{-5,-4,-3,-2,-1,0,1,2,3,4,5\\}$" + ], "text/plain": [ "{−5,−4,−3,−2,−1,0,1,2,3,4,5}" ] }, - "execution_count": 4, + "execution_count": 5, "metadata": {}, "output_type": "execute_result" } @@ -107,8 +158,9 @@ "name": "prob2" }, "language_info": { + "codemirror_mode": "prob2_jupyter_repl", "file_extension": ".prob", - "mimetype": "text/x-prob", + "mimetype": "text/x-prob2-jupyter-repl", "name": "prob" } }, diff --git a/notebooks/tests/load_file.ipynb b/notebooks/tests/load_file.ipynb index d4c6d42..83549e1 100644 --- a/notebooks/tests/load_file.ipynb +++ b/notebooks/tests/load_file.ipynb @@ -1,5 +1,44 @@ { "cells": [ + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "```\n", + ":load FILENAME [PREF=VALUE ...]\n", + "```\n", + "\n", + "Load the machine from the given path.\n", + "\n", + "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n", + "\n", + "Any number of preference assignments may be included after the file path. Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded." + ], + "text/plain": [ + "```\n", + ":load FILENAME [PREF=VALUE ...]\n", + "```\n", + "\n", + "Load the machine from the given path.\n", + "\n", + "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n", + "\n", + "Any number of preference assignments may be included after the file path. Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded." + ] + }, + "execution_count": 1, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":help :load" + ] + }, { "cell_type": "markdown", "metadata": {}, @@ -9,7 +48,7 @@ }, { "cell_type": "code", - "execution_count": 1, + "execution_count": 2, "metadata": {}, "outputs": [ { @@ -18,7 +57,7 @@ "Loaded machine: things : []\n" ] }, - "execution_count": 1, + "execution_count": 2, "metadata": {}, "output_type": "execute_result" } @@ -29,16 +68,19 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 3, "metadata": {}, "outputs": [ { "data": { + "text/markdown": [ + "$\\{\\mathit{ONE},\\mathit{TWO},\\mathit{THREE},\\mathit{FOUR}\\}$" + ], "text/plain": [ "{ONE,TWO,THREE,FOUR}" ] }, - "execution_count": 2, + "execution_count": 3, "metadata": {}, "output_type": "execute_result" } @@ -56,7 +98,7 @@ }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 4, "metadata": {}, "outputs": [ { @@ -65,7 +107,7 @@ "Loaded machine: things : []\n" ] }, - "execution_count": 3, + "execution_count": 4, "metadata": {}, "output_type": "execute_result" } @@ -76,16 +118,19 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 5, "metadata": {}, "outputs": [ { "data": { + "text/markdown": [ + "$\\{-5,-4,-3,-2,-1,0,1,2,3,4,5\\}$" + ], "text/plain": [ "{−5,−4,−3,−2,−1,0,1,2,3,4,5}" ] }, - "execution_count": 4, + "execution_count": 5, "metadata": {}, "output_type": "execute_result" } @@ -102,8 +147,9 @@ "name": "prob2" }, "language_info": { + "codemirror_mode": "prob2_jupyter_repl", "file_extension": ".prob", - "mimetype": "text/x-prob", + "mimetype": "text/x-prob2-jupyter-repl", "name": "prob" } }, diff --git a/notebooks/tests/pref.ipynb b/notebooks/tests/pref.ipynb index 0b3818f..692439a 100644 --- a/notebooks/tests/pref.ipynb +++ b/notebooks/tests/pref.ipynb @@ -13,13 +13,23 @@ ":pref NAME=VALUE [NAME=VALUE ...]\n", "```\n", "\n", - "View or change the value of one or more preferences." + "View or change the value of one or more preferences.\n", + "\n", + "In the first form, the values of all given preferences are displayed (or all preferences, if none are given). In the second form, the given preference assignments are performed. The two forms cannot be mixed; it is not possible to view and change preferences in a single command.\n", + "\n", + "Certain preference changes do not take full effect when performed on a loaded machine. Such preferences must be assigned when the machine is loaded using the `::load` or `:load` command." ], "text/plain": [ + "```\n", ":pref [NAME ...]\n", ":pref NAME=VALUE [NAME=VALUE ...]\n", + "```\n", + "\n", + "View or change the value of one or more preferences.\n", "\n", - "View or change the value of one or more preferences." + "In the first form, the values of all given preferences are displayed (or all preferences, if none are given). In the second form, the given preference assignments are performed. The two forms cannot be mixed; it is not possible to view and change preferences in a single command.\n", + "\n", + "Certain preference changes do not take full effect when performed on a loaded machine. Such preferences must be assigned when the machine is loaded using the `::load` or `:load` command." ] }, "execution_count": 1, @@ -151,6 +161,7 @@ "SYMMETRY_MODE = off\n", "TIME_OUT = 2500\n", "TK_CUSTOM_STATE_VIEW_PADDING = 0\n", + "TK_CUSTOM_STATE_VIEW_STRING_PADDING = 10\n", "TLC_WORKERS = 2\n", "TRACE_INFO = false\n", "TRACE_UPON_ERROR = false\n", @@ -207,6 +218,9 @@ "outputs": [ { "data": { + "text/markdown": [ + "$\\{-1,0,1,2,3\\}$" + ], "text/plain": [ "{−1,0,1,2,3}" ] @@ -276,6 +290,9 @@ "outputs": [ { "data": { + "text/markdown": [ + "$\\{-5,-4,-3,-2,-1,0,1,2,3,4,5\\}$" + ], "text/plain": [ "{−5,−4,−3,−2,−1,0,1,2,3,4,5}" ] @@ -340,8 +357,9 @@ "name": "prob2" }, "language_info": { + "codemirror_mode": "prob2_jupyter_repl", "file_extension": ".prob", - "mimetype": "text/x-prob", + "mimetype": "text/x-prob2-jupyter-repl", "name": "prob" } }, diff --git a/notebooks/tests/prettyprint.ipynb b/notebooks/tests/prettyprint.ipynb index 76c55bd..4cdc1fc 100644 --- a/notebooks/tests/prettyprint.ipynb +++ b/notebooks/tests/prettyprint.ipynb @@ -12,12 +12,22 @@ ":prettyprint PREDICATE\n", "```\n", "\n", - "Pretty-print a predicate." + "Pretty-print a predicate.\n", + "\n", + "The predicate is not evaluated or simplified, it is only reformatted and converted to Unicode/$\\LaTeX$ form.\n", + "\n", + "Expressions cannot be pretty-printed, only predicates." ], "text/plain": [ + "```\n", ":prettyprint PREDICATE\n", + "```\n", + "\n", + "Pretty-print a predicate.\n", + "\n", + "The predicate is not evaluated or simplified, it is only reformatted and converted to Unicode/$\\LaTeX$ form.\n", "\n", - "Pretty-print a predicate." + "Expressions cannot be pretty-printed, only predicates." ] }, "execution_count": 1, @@ -83,8 +93,9 @@ "name": "prob2" }, "language_info": { + "codemirror_mode": "prob2_jupyter_repl", "file_extension": ".prob", - "mimetype": "text/x-prob", + "mimetype": "text/x-prob2-jupyter-repl", "name": "prob" } }, diff --git a/notebooks/tests/render.ipynb b/notebooks/tests/render.ipynb index 6f97306..b7853e9 100644 --- a/notebooks/tests/render.ipynb +++ b/notebooks/tests/render.ipynb @@ -13,13 +13,23 @@ "CONTENT\n", "```\n", "\n", - "Render some content with the specified MIME type." + "Render some content with the specified MIME type.\n", + "\n", + "This command is intended for debugging the rendering behavior of Jupyter and the kernel, it should not be used in regular notebooks. To include text or images in a notebook, Markdown cells should be used instead.\n", + "\n", + "The command does not place any restrictions on the MIME type or content. A plain text fallback with the raw content is always included, and will be displayed if the frontend does not support the given MIME type." ], "text/plain": [ + "```\n", "::render MIMETYPE\n", "CONTENT\n", + "```\n", + "\n", + "Render some content with the specified MIME type.\n", + "\n", + "This command is intended for debugging the rendering behavior of Jupyter and the kernel, it should not be used in regular notebooks. To include text or images in a notebook, Markdown cells should be used instead.\n", "\n", - "Render some content with the specified MIME type." + "The command does not place any restrictions on the MIME type or content. A plain text fallback with the raw content is always included, and will be displayed if the frontend does not support the given MIME type." ] }, "execution_count": 1, @@ -241,8 +251,9 @@ "name": "prob2" }, "language_info": { + "codemirror_mode": "prob2_jupyter_repl", "file_extension": ".prob", - "mimetype": "text/x-prob", + "mimetype": "text/x-prob2-jupyter-repl", "name": "prob" } }, diff --git a/notebooks/tests/show.ipynb b/notebooks/tests/show.ipynb index 062485c..de67d53 100644 --- a/notebooks/tests/show.ipynb +++ b/notebooks/tests/show.ipynb @@ -12,12 +12,18 @@ ":show\n", "```\n", "\n", - "Show the machine's animation function visualisation for the current state." + "Show the machine's animation function visualisation for the current state.\n", + "\n", + "The visualisation is static, any defined right-click options cannot be viewed or used." ], "text/plain": [ + "```\n", ":show\n", + "```\n", + "\n", + "Show the machine's animation function visualisation for the current state.\n", "\n", - "Show the machine's animation function visualisation for the current state." + "The visualisation is static, any defined right-click options cannot be viewed or used." ] }, "execution_count": 1, diff --git a/notebooks/tests/solve.ipynb b/notebooks/tests/solve.ipynb index cdf2fea..6831829 100644 --- a/notebooks/tests/solve.ipynb +++ b/notebooks/tests/solve.ipynb @@ -12,12 +12,30 @@ ":solve SOLVER PREDICATE\n", "```\n", "\n", - "Solve a predicate with the specified solver" + "Solve a predicate with the specified solver.\n", + "\n", + "The following solvers are currently available:\n", + "\n", + "* `cvc4`\n", + "* `kodkod`\n", + "* `prob`\n", + "* `smt_supported_interpreter`\n", + "* `z3`\n" ], "text/plain": [ + "```\n", ":solve SOLVER PREDICATE\n", + "```\n", + "\n", + "Solve a predicate with the specified solver.\n", + "\n", + "The following solvers are currently available:\n", "\n", - "Solve a predicate with the specified solver" + "* `cvc4`\n", + "* `kodkod`\n", + "* `prob`\n", + "* `smt_supported_interpreter`\n", + "* `z3`\n" ] }, "execution_count": 1, @@ -44,11 +62,11 @@ { "data": { "text/markdown": [ - "$TRUE$\n", + "$\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $xx = 3$\n", - "* $yy = 4$" + "* $\\mathit{xx} = 3$\n", + "* $\\mathit{yy} = 4$" ], "text/plain": [ "TRUE\n", @@ -75,11 +93,11 @@ { "data": { "text/markdown": [ - "$TRUE$\n", + "$\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $xx = 3$\n", - "* $yy = 4$" + "* $\\mathit{xx} = 3$\n", + "* $\\mathit{yy} = 4$" ], "text/plain": [ "TRUE\n", @@ -105,10 +123,10 @@ "outputs": [ { "ename": "ProBError", - "evalue": "(error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4498957308),0,procedure,:(z3interface,/(pop_frame,0)),0)))", + "evalue": "(error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4375289388),0,procedure,:(z3interface,/(pop_frame,0)),0)))", "output_type": "error", "traceback": [ - "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31m(error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4498957308),0,procedure,:(z3interface,/(pop_frame,0)),0)))\u001b[0m" + "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31m(error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4375289388),0,procedure,:(z3interface,/(pop_frame,0)),0)))\u001b[0m" ] } ], @@ -236,11 +254,11 @@ { "data": { "text/markdown": [ - "$TRUE$\n", + "$\\mathit{TRUE}$\n", "\n", "**Solution:**\n", - "* $x = 2$\n", - "* $z = 2$" + "* $\\mathit{x} = 2$\n", + "* $\\mathit{z} = 2$" ], "text/plain": [ "TRUE\n", @@ -267,7 +285,7 @@ { "data": { "text/markdown": [ - "$FALSE$" + "$\\mathit{FALSE}$" ], "text/plain": [ "FALSE" @@ -290,8 +308,9 @@ "name": "prob2" }, "language_info": { + "codemirror_mode": "prob2_jupyter_repl", "file_extension": ".prob", - "mimetype": "text/x-prob", + "mimetype": "text/x-prob2-jupyter-repl", "name": "prob" } }, diff --git a/notebooks/tests/table.ipynb b/notebooks/tests/table.ipynb index 7ee5fda..f435c72 100644 --- a/notebooks/tests/table.ipynb +++ b/notebooks/tests/table.ipynb @@ -12,12 +12,18 @@ ":table EXPRESSION\n", "```\n", "\n", - "Display an expression as a table." + "Display an expression as a table.\n", + "\n", + "Although any expression is accepted, this command is most useful for sets of tuples." ], "text/plain": [ + "```\n", ":table EXPRESSION\n", + "```\n", + "\n", + "Display an expression as a table.\n", "\n", - "Display an expression as a table." + "Although any expression is accepted, this command is most useful for sets of tuples." ] }, "execution_count": 1, @@ -177,8 +183,9 @@ "name": "prob2" }, "language_info": { + "codemirror_mode": "prob2_jupyter_repl", "file_extension": ".prob", - "mimetype": "text/x-prob", + "mimetype": "text/x-prob2-jupyter-repl", "name": "prob" } }, diff --git a/notebooks/tests/time.ipynb b/notebooks/tests/time.ipynb index deaa13a..a0e1476 100644 --- a/notebooks/tests/time.ipynb +++ b/notebooks/tests/time.ipynb @@ -12,12 +12,22 @@ ":time COMMAND [ARGS ...]\n", "```\n", "\n", - "Execute the given command and measure how long it takes to execute." + "Execute the given command and measure how long it takes to execute.\n", + "\n", + "The time is measured using Java's [`System.nanoTime()`](https://docs.oracle.com/javase/8/docs/api/java/lang/System.html#nanoTime--) method. The measured time is displayed with the full number of decimal places, but no guarantees are made about the actual resolution of the time measurement.\n", + "\n", + "As with any measurement of execution time, there will likely be small differences between two measurements of the same command. The time is measured by the kernel rather than ProB, so it will include some overhead due to processing of the command by the kernel and communication with ProB." ], "text/plain": [ + "```\n", ":time COMMAND [ARGS ...]\n", + "```\n", "\n", - "Execute the given command and measure how long it takes to execute." + "Execute the given command and measure how long it takes to execute.\n", + "\n", + "The time is measured using Java's [`System.nanoTime()`](https://docs.oracle.com/javase/8/docs/api/java/lang/System.html#nanoTime--) method. The measured time is displayed with the full number of decimal places, but no guarantees are made about the actual resolution of the time measurement.\n", + "\n", + "As with any measurement of execution time, there will likely be small differences between two measurements of the same command. The time is measured by the kernel rather than ProB, so it will include some overhead due to processing of the command by the kernel and communication with ProB." ] }, "execution_count": 1, @@ -44,10 +54,10 @@ { "data": { "text/markdown": [ - "Execution time: 1.037496364 seconds" + "Execution time: 1.054965314 seconds" ], "text/plain": [ - "Execution time: 1.037496364 seconds" + "Execution time: 1.054965314 seconds" ] }, "metadata": {}, @@ -83,10 +93,10 @@ { "data": { "text/markdown": [ - "Execution time: 1.074667161 seconds" + "Execution time: 1.105035884 seconds" ], "text/plain": [ - "Execution time: 1.074667161 seconds" + "Execution time: 1.105035884 seconds" ] }, "metadata": {}, @@ -94,6 +104,9 @@ }, { "data": { + "text/markdown": [ + "$\\{12345,24690,37035,49380,61725,74070,86415,98760\\}$" + ], "text/plain": [ "{12345,24690,37035,49380,61725,74070,86415,98760}" ] @@ -115,8 +128,9 @@ "name": "prob2" }, "language_info": { + "codemirror_mode": "prob2_jupyter_repl", "file_extension": ".prob", - "mimetype": "text/x-prob", + "mimetype": "text/x-prob2-jupyter-repl", "name": "prob" } }, diff --git a/notebooks/tests/type.ipynb b/notebooks/tests/type.ipynb index 1a13963..2173cc3 100644 --- a/notebooks/tests/type.ipynb +++ b/notebooks/tests/type.ipynb @@ -12,12 +12,18 @@ ":type FORMULA\n", "```\n", "\n", - "Display the type of a formula." + "Display the type of a formula.\n", + "\n", + "The returned types are *not* standard B types. They are human-readable, but cannot be used in code." ], "text/plain": [ + "```\n", ":type FORMULA\n", + "```\n", + "\n", + "Display the type of a formula.\n", "\n", - "Display the type of a formula." + "The returned types are *not* standard B types. They are human-readable, but cannot be used in code." ] }, "execution_count": 1, @@ -259,8 +265,9 @@ "name": "prob2" }, "language_info": { + "codemirror_mode": "prob2_jupyter_repl", "file_extension": ".prob", - "mimetype": "text/x-prob", + "mimetype": "text/x-prob2-jupyter-repl", "name": "prob" } }, diff --git a/notebooks/tests/version.ipynb b/notebooks/tests/version.ipynb index 29683b1..e33dd0f 100644 --- a/notebooks/tests/version.ipynb +++ b/notebooks/tests/version.ipynb @@ -12,12 +12,14 @@ ":version\n", "```\n", "\n", - "Display version info about the ProB CLI and ProB 2" + "Display version info about the ProB CLI and ProB 2." ], "text/plain": [ + "```\n", ":version\n", + "```\n", "\n", - "Display version info about the ProB CLI and ProB 2" + "Display version info about the ProB CLI and ProB 2." ] }, "execution_count": 1, @@ -37,8 +39,8 @@ { "data": { "text/plain": [ - "ProB CLI: 1.8.1-beta4 (c6264c505a07e8df7a9f0a7631c9d503c125bd8e)\n", - "ProB 2: 3.2.10-SNAPSHOT (8108b7526c431b4d51d23676edf00973f0ec1c96)" + "ProB CLI: 1.8.1-beta5 (c72b1a169223d7a37e2bc4313a57da091c8e23e7)\n", + "ProB 2: 3.2.10-SNAPSHOT (01c9043ddb8ad69e4e9063a98f0ce132faf030a2)" ] }, "execution_count": 2, @@ -58,8 +60,9 @@ "name": "prob2" }, "language_info": { + "codemirror_mode": "prob2_jupyter_repl", "file_extension": ".prob", - "mimetype": "text/x-prob", + "mimetype": "text/x-prob2-jupyter-repl", "name": "prob" } }, diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java index ab8cfc0..40c2699 100644 --- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java @@ -35,6 +35,12 @@ public final class AssertCommand implements Command { return "Ensure that the predicate is true, and show an error otherwise."; } + @Override + public @NotNull String getHelpBody() { + return "This command is intended for verifying that a predicate is always true at a certain point in a notebook. Unlike normal evaluation (`:eval`), this command treats a $\\mathit{FALSE}$ result as an error. If the result is $\\mathit{TRUE}$, solutions for free variables (if any) are not displayed.\n\n" + + "Only predicates and $\\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error."; + } + @Override public @NotNull DisplayData run(final @NotNull String argString) { final AbstractEvalResult result = this.animationSelector.getCurrentTrace().evalCurrent(argString, FormulaExpand.TRUNCATE); diff --git a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java index df7eeec..d7b7448 100644 --- a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java @@ -44,7 +44,12 @@ public final class BrowseCommand implements Command { @Override public @NotNull String getShortHelp() { - return "Show information about the current state"; + return "Show information about the current state."; + } + + @Override + public @NotNull String getHelpBody() { + return "The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of transitions that are available in the current state. Each transition has a numeric ID, which can be passed to `:exec` to execute that transition."; } private static <T extends AbstractElement> @NotNull String elementsToString( diff --git a/src/main/java/de/prob2/jupyter/commands/Command.java b/src/main/java/de/prob2/jupyter/commands/Command.java index 7c7f5a3..b9be2eb 100644 --- a/src/main/java/de/prob2/jupyter/commands/Command.java +++ b/src/main/java/de/prob2/jupyter/commands/Command.java @@ -11,6 +11,8 @@ public interface Command { public abstract @NotNull String getShortHelp(); + public abstract @NotNull String getHelpBody(); + public abstract @Nullable DisplayData run(final @NotNull String argString); public abstract @Nullable ReplacementOptions complete(final @NotNull String argString, final int at); diff --git a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java index ca25502..1b0a6c9 100644 --- a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java @@ -34,7 +34,12 @@ public final class ConstantsCommand implements Command { @Override public @NotNull String getShortHelp() { - return "Set up the current machine's constants with the specified predicate"; + return "Set up the current machine's constants."; + } + + @Override + public @NotNull String getHelpBody() { + return "This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`."; } @Override diff --git a/src/main/java/de/prob2/jupyter/commands/DotCommand.java b/src/main/java/de/prob2/jupyter/commands/DotCommand.java index 54fc9e5..c57d9c7 100644 --- a/src/main/java/de/prob2/jupyter/commands/DotCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/DotCommand.java @@ -44,7 +44,30 @@ public final class DotCommand implements Command { @Override public @NotNull String getShortHelp() { - return "Execute and show a dot visualization."; + return "Execute and show a dot visualisation."; + } + + @Override + public @NotNull String getHelpBody() { + final StringBuilder sb = new StringBuilder("The following dot visualisation commands are available:\n\n"); + final Trace trace = this.animationSelector.getCurrentTrace(); + final GetAllDotCommands cmd = new GetAllDotCommands(trace.getCurrentState()); + trace.getStateSpace().execute(cmd); + for (final DynamicCommandItem item : cmd.getCommands()) { + sb.append("* `"); + sb.append(item.getCommand()); + sb.append("` - "); + sb.append(item.getName()); + sb.append(": "); + sb.append(item.getDescription()); + if (!item.isAvailable()) { + sb.append(" (**Not available for this machine/state**: "); + sb.append(item.getAvailable()); + sb.append(')'); + } + sb.append('\n'); + } + return sb.toString(); } @Override diff --git a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java index 87d426b..ab89659 100644 --- a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java @@ -22,12 +22,18 @@ public final class EvalCommand implements Command { @Override public @NotNull String getSyntax() { - return ":eval EXPRESSION"; + return ":eval FORMULA"; } @Override public @NotNull String getShortHelp() { - return "Evaluate an expression."; + return "Evaluate a formula and display the result."; + } + + @Override + public @NotNull String getHelpBody() { + return "This is equivalent to inputting the formula without a command name.\n\n" + + "If the formula is a $\\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed."; } @Override diff --git a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java index c74e114..66a1939 100644 --- a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java @@ -38,7 +38,13 @@ public final class ExecCommand implements Command { @Override public @NotNull String getShortHelp() { - return "Execute an operation with the specified predicate, or by its ID"; + return "Execute an operation with the specified predicate, or by its ID."; + } + + @Override + public @NotNull String getHelpBody() { + return "In the first form, the given operation is executed. If the optional predicate is specified, a transition is found for which the predicate is $\\mathit{TRUE}$. The predicate can be used to restrict what values the operation's parameters or the variables in the next state may have.\n\n" + + "In the second form, a known transition with the given numeric ID is executed. A list of the current state's available transitions and their IDs can be viewed using `:browse`. Only transition IDs from the current state can be executed."; } @Override diff --git a/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java b/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java index b665132..6eb9988 100644 --- a/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java @@ -40,6 +40,11 @@ public final class GroovyCommand implements Command { return "Evaluate the given Groovy expression."; } + @Override + public @NotNull String getHelpBody() { + return "The standard ProB 2 Groovy environment is used to evaluate the expression, so ProB 2's global `api` and `animations` objects may be used to load machines and manipulate traces."; + } + @Override public @NotNull DisplayData run(final @NotNull String argString) { this.groovyScriptEngine.put("__console", this.injector.getInstance(ProBKernel.class).getIO().out); diff --git a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java index 149044a..42fb943 100644 --- a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java @@ -35,6 +35,11 @@ public final class HelpCommand implements Command { return "Display help for a specific command, or general help about the REPL."; } + @Override + public @NotNull String getHelpBody() { + return ""; + } + @Override public @NotNull DisplayData run(final @NotNull String argString) { final ProBKernel kernel = this.injector.getInstance(ProBKernel.class); @@ -72,8 +77,18 @@ public final class HelpCommand implements Command { if (command == null) { throw new UserErrorException(String.format("Cannot display help for unknown command \"%s\"", commandName)); } - final DisplayData result = new DisplayData(command.getSyntax() + "\n\n" + command.getShortHelp()); - result.putMarkdown("```\n" + command.getSyntax() + "\n```\n\n" + command.getShortHelp()); + final StringBuilder sb = new StringBuilder(); + sb.append("```\n"); + sb.append(command.getSyntax()); + sb.append("\n```\n\n"); + sb.append(command.getShortHelp()); + final String helpBody = command.getHelpBody(); + if (!helpBody.isEmpty()) { + sb.append("\n\n"); + sb.append(helpBody); + } + final DisplayData result = new DisplayData(sb.toString()); + result.putMarkdown(sb.toString()); return result; } else { throw new UserErrorException("Expected at most 1 argument, got " + args.size()); diff --git a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java index 5b69cb1..e26e354 100644 --- a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java @@ -37,6 +37,11 @@ public final class InitialiseCommand implements Command { return "Initialise the current machine with the specified predicate"; } + @Override + public @NotNull String getHelpBody() { + return "This is a shorthand for `:exec INITIALISATION [PREDICATE]`."; + } + @Override public @NotNull DisplayData run(final @NotNull String argString) { final Trace trace = this.animationSelector.getCurrentTrace(); diff --git a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java index 9ed0fe3..c9ceb7e 100644 --- a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java @@ -36,7 +36,13 @@ public final class LoadCellCommand implements Command { @Override public @NotNull String getShortHelp() { - return "Load the machine source code from the body."; + return "Load the machine source code given in the cell body."; + } + + @Override + public @NotNull String getHelpBody() { + return "There must be a newline between the `::load` command name and the machine code.\n\n" + + "Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."; } @Override diff --git a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java index 5552b87..6efaf70 100644 --- a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java @@ -52,6 +52,12 @@ public final class LoadFileCommand implements Command { return "Load the machine from the given path."; } + @Override + public @NotNull String getHelpBody() { + return "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n\n" + + "Any number of preference assignments may be included after the file path. Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."; + } + @Override public @NotNull DisplayData run(final @NotNull String argString) { final List<String> args = CommandUtils.splitArgs(argString); diff --git a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java index 7c77569..3d02abf 100644 --- a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java @@ -40,6 +40,12 @@ public final class PrefCommand implements Command { return "View or change the value of one or more preferences."; } + @Override + public @NotNull String getHelpBody() { + return "In the first form, the values of all given preferences are displayed (or all preferences, if none are given). In the second form, the given preference assignments are performed. The two forms cannot be mixed; it is not possible to view and change preferences in a single command.\n\n" + + "Certain preference changes do not take full effect when performed on a loaded machine. Such preferences must be assigned when the machine is loaded using the `::load` or `:load` command."; + } + @Override public @NotNull DisplayData run(final @NotNull String argString) { final List<String> args = CommandUtils.splitArgs(argString); diff --git a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java index 4d53205..61e5065 100644 --- a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java @@ -32,6 +32,12 @@ public final class PrettyPrintCommand implements Command { return "Pretty-print a predicate."; } + @Override + public @NotNull String getHelpBody() { + return "The predicate is not evaluated or simplified, it is only reformatted and converted to Unicode/$\\LaTeX$ form.\n\n" + + "Expressions cannot be pretty-printed, only predicates."; + } + @Override public @NotNull DisplayData run(final @NotNull String argString) { final IEvalElement formula = this.animationSelector.getCurrentTrace().getModel().parseFormula(argString, FormulaExpand.EXPAND); diff --git a/src/main/java/de/prob2/jupyter/commands/RenderCommand.java b/src/main/java/de/prob2/jupyter/commands/RenderCommand.java index 149bb83..ebb2a0e 100644 --- a/src/main/java/de/prob2/jupyter/commands/RenderCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/RenderCommand.java @@ -26,6 +26,12 @@ public final class RenderCommand implements Command { return "Render some content with the specified MIME type."; } + @Override + public @NotNull String getHelpBody() { + return "This command is intended for debugging the rendering behavior of Jupyter and the kernel, it should not be used in regular notebooks. To include text or images in a notebook, Markdown cells should be used instead.\n\n" + + "The command does not place any restrictions on the MIME type or content. A plain text fallback with the raw content is always included, and will be displayed if the frontend does not support the given MIME type."; + } + @Override public @NotNull DisplayData run(final @NotNull String argString) { final String[] split = argString.split("\n", 2); diff --git a/src/main/java/de/prob2/jupyter/commands/ShowCommand.java b/src/main/java/de/prob2/jupyter/commands/ShowCommand.java index f9df36f..66539e0 100644 --- a/src/main/java/de/prob2/jupyter/commands/ShowCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/ShowCommand.java @@ -37,6 +37,11 @@ public final class ShowCommand implements Command { return "Show the machine's animation function visualisation for the current state."; } + @Override + public @NotNull String getHelpBody() { + return "The visualisation is static, any defined right-click options cannot be viewed or used."; + } + @Override public @NotNull DisplayData run(final @NotNull String argString) { if (!argString.isEmpty()) { diff --git a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java index 02ab8f5..77b2970 100644 --- a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java @@ -1,9 +1,10 @@ package de.prob2.jupyter.commands; +import java.util.Arrays; import java.util.List; +import java.util.Map; import java.util.regex.Matcher; import java.util.stream.Collectors; -import java.util.stream.Stream; import com.google.inject.Inject; @@ -21,6 +22,9 @@ import io.github.spencerpark.jupyter.kernel.display.DisplayData; import org.jetbrains.annotations.NotNull; public final class SolveCommand implements Command { + private static final @NotNull Map<@NotNull String, CbcSolveCommand.@NotNull Solvers> SOLVERS = Arrays.stream(CbcSolveCommand.Solvers.values()) + .collect(Collectors.toMap(s -> s.name().toLowerCase(), s -> s)); + private final @NotNull AnimationSelector animationSelector; @Inject @@ -37,7 +41,18 @@ public final class SolveCommand implements Command { @Override public @NotNull String getShortHelp() { - return "Solve a predicate with the specified solver"; + return "Solve a predicate with the specified solver."; + } + + @Override + public @NotNull String getHelpBody() { + final StringBuilder sb = new StringBuilder("The following solvers are currently available:\n\n"); + SOLVERS.keySet().stream().sorted().forEach(solver -> { + sb.append("* `"); + sb.append(solver); + sb.append("`\n"); + }); + return sb.toString(); } @Override @@ -48,30 +63,9 @@ public final class SolveCommand implements Command { } final Trace trace = this.animationSelector.getCurrentTrace(); - final CbcSolveCommand.Solvers solver; - switch (split.get(0)) { - case "prob": - solver = CbcSolveCommand.Solvers.PROB; - break; - - case "kodkod": - solver = CbcSolveCommand.Solvers.KODKOD; - break; - - case "smt_supported_interpreter": - solver = CbcSolveCommand.Solvers.SMT_SUPPORTED_INTERPRETER; - break; - - case "z3": - solver = CbcSolveCommand.Solvers.Z3; - break; - - case "cvc4": - solver = CbcSolveCommand.Solvers.CVC4; - break; - - default: - throw new UserErrorException("Unknown solver: " + split.get(0)); + final CbcSolveCommand.Solvers solver = SOLVERS.get(split.get(0)); + if (solver == null) { + throw new UserErrorException("Unknown solver: " + split.get(0)); } final IEvalElement predicate = trace.getModel().parseFormula(split.get(1), FormulaExpand.EXPAND); @@ -97,7 +91,7 @@ public final class SolveCommand implements Command { } else { // Cursor is in the solver name. final String prefix = argString.substring(0, at); - final List<String> solverNames = Stream.of("prob", "kodkod", "smt_supported_interpreter", "z3", "cvc4") + final List<String> solverNames = SOLVERS.keySet().stream() .filter(s -> s.startsWith(prefix)) .sorted() .collect(Collectors.toList()); diff --git a/src/main/java/de/prob2/jupyter/commands/TableCommand.java b/src/main/java/de/prob2/jupyter/commands/TableCommand.java index d79fc15..7d8c53b 100644 --- a/src/main/java/de/prob2/jupyter/commands/TableCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/TableCommand.java @@ -39,6 +39,11 @@ public final class TableCommand implements Command { return "Display an expression as a table."; } + @Override + public @NotNull String getHelpBody() { + return "Although any expression is accepted, this command is most useful for sets of tuples."; + } + @Override public @NotNull DisplayData run(final @NotNull String argString) { final Trace trace = this.animationSelector.getCurrentTrace(); diff --git a/src/main/java/de/prob2/jupyter/commands/TimeCommand.java b/src/main/java/de/prob2/jupyter/commands/TimeCommand.java index 5a89edd..7ce1902 100644 --- a/src/main/java/de/prob2/jupyter/commands/TimeCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/TimeCommand.java @@ -33,6 +33,12 @@ public final class TimeCommand implements Command { return "Execute the given command and measure how long it takes to execute."; } + @Override + public @NotNull String getHelpBody() { + return "The time is measured using Java's [`System.nanoTime()`](https://docs.oracle.com/javase/8/docs/api/java/lang/System.html#nanoTime--) method. The measured time is displayed with the full number of decimal places, but no guarantees are made about the actual resolution of the time measurement.\n\n" + + "As with any measurement of execution time, there will likely be small differences between two measurements of the same command. The time is measured by the kernel rather than ProB, so it will include some overhead due to processing of the command by the kernel and communication with ProB."; + } + @Override public @Nullable DisplayData run(final @NotNull String argString) { final ProBKernel kernel = this.injector.getInstance(ProBKernel.class); diff --git a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java index df66411..96a6b14 100644 --- a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java @@ -34,6 +34,11 @@ public final class TypeCommand implements Command { return "Display the type of a formula."; } + @Override + public @NotNull String getHelpBody() { + return "The returned types are *not* standard B types. They are human-readable, but cannot be used in code."; + } + @Override public @NotNull DisplayData run(final @NotNull String argString) { final Trace trace = this.animationSelector.getCurrentTrace(); diff --git a/src/main/java/de/prob2/jupyter/commands/VersionCommand.java b/src/main/java/de/prob2/jupyter/commands/VersionCommand.java index 83b11d7..4c71ae0 100644 --- a/src/main/java/de/prob2/jupyter/commands/VersionCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/VersionCommand.java @@ -29,7 +29,12 @@ public final class VersionCommand implements Command { @Override public @NotNull String getShortHelp() { - return "Display version info about the ProB CLI and ProB 2"; + return "Display version info about the ProB CLI and ProB 2."; + } + + @Override + public @NotNull String getHelpBody() { + return ""; } @Override -- GitLab