diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index bc367a0d81e4b599bebaf9c3ef2f47b64e10216c..4c62bf7ea8f45d0798d160cd25bf4c7ea64f5895 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 8e79a0f80931212a5a72e40652df7187f685c82f..6ae6b79e5f3e81f33d3b062247810e87d33bbf4d 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 5f54acbe074cbb0799c563d7d4a543325e9de65c..c0bd454c846441d18440a4fe7f143bf99d1db30f 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 c1ff1ec89935487719ca77c6fede58e38c464980..d3bc3854db27001ea9223f51170e9024a3b39c83 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 0943f9d394bae583274928e4bbf97631d4f08ad2..d4838cdce7ea9d15daaa1589e2220a1b73a763a8 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 d601de4515851122069ccad1bf066999421edabb..8489fd0acd55e39a7e764800c7019d6ab79ad2d2 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 ed36c155dfe42d5001a3afb3b2a76c0eff4499f4..6f2d327cdab4d72d93f969426bd641fb4f842eef 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 d4c6d42297c10957821dc0678799551321461bcd..83549e1ccf53d880b0fb9597af491daa743e0bff 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 0b3818fd65f3dc66f6f4dfa60e75beef86d19d33..692439ad151b92fd37b64ee18ebdb704caf83d44 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 76c55bd3712c8db352d5fbe3a4a00ed19b66457c..4cdc1fc28a186cf9b28e2c7f592dd4447b05cbfd 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 6f973067119f4311f63d84db4888d5901587f269..b7853e991697b2ade37fd7830ee3793799f74c6b 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 062485cc6fafeabdcd050a640c28ab48856b6068..de67d5392128eeeb723931c41ae102d31829d17f 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 cdf2fea830c89f7fa9071a43458e2bd4714e7ec0..6831829d419a04cd3845420c83b826101208f5d2 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 7ee5fdab5cc0dd140f395c6b750a2bf8f99dca48..f435c72bfba6c2d072dedd7c3099f03ffb079a0a 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 deaa13a8494f39e2e53c47b944f8432b6b161d62..a0e147634d93d339dfa74d8482cbbc7f99afa287 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 1a1396325cf023c5ac3b9a36a6a9c2b1d0c75041..2173cc3699f69e865e5d929166011bd1c21bc726 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 29683b1842d9185fb3daec8abef075f533b34b3e..e33dd0f6b79c315f89dbb3b09ee882f714c35fc4 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 ab8cfc086698cc05a21726cea0dea14d99dfcae2..40c2699214afab64c2d13c079a2c3804f374e496 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 df7eeec4d25afd17e4ce444d433633f294bdf152..d7b7448d45b3aa85569ab87dda81742fc361ba46 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 7c7f5a35da20394f55fd2a85a208fab6fd24c55a..b9be2eb10d65686f4dfe13136e85f014aa7db5b4 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 ca2550221f97916c3924a0db4323a8065b27f20d..1b0a6c948425ebc6325d68805abb8ba91c6e9395 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 54fc9e5b26f8691cad6dde8cf8b9a8d5d33d872f..c57d9c7bf327ad99ddacca2219b0af3a05d6522e 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 87d426b8578cc411f0e69b0733f1e0d2d239d7f8..ab8965903d702c2572e0d687a3c60660d5371292 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 c74e114594b3a4158a5558d46f333fc27de355e4..66a19399484522beec5e8611d030d434d2b16f07 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 b66513276adcba55ead84460488cc4a1a2067e45..6eb9988fe9216c59c656ab409ce8bb81da774a15 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 149044a83652c0ab3bdd127f4e4c839f099784f1..42fb94339885e8f9e7511bed80b4311663c1fa57 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 5b69cb1de03cc7bfbbe989f66f44132bb658261f..e26e3547f5c75ccc43f40dbca7dcd66080bad195 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 9ed0fe3a485aa047e8cdda5d2906c1c896ebe31b..c9ceb7e3cbdce7bd3bdbd8c3a4580f1a5abc8389 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 5552b8799373b3ef488e3c6958a3bccfa77ea460..6efaf70d5dab73fcce4a1fb28eaa2b97cb164105 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 7c77569b0b974dffc808e0b500849b08c5ab3e1a..3d02abf31ab1bedb6947536bbc9e221989307c55 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 4d532050266098b17bcb68c2032e822fcd12d267..61e5065abdb8ebc323fcd32d945a7bf1c6ed2c4e 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 149bb8373153ed6501c1853cc73278929ca422fb..ebb2a0e3bc2e56677745c84a7778a114dc193882 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 f9df36fb0e04fc70f270330be14829c6b3539b98..66539e007ac1011965999a41f7ea4cfdb763bbbd 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 02ab8f52977c3b333ea4b855c9340e64083dbf8e..77b2970ebdbddb264f523336fc51a829573c9ca5 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 d79fc154308ed14f79c165c6d21fa0086c5a5980..7d8c53b741a2e76d368e59a203d2e59e8bbd7714 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 5a89edd1208d46786c32f9849bea5e2beba8a254..7ce190214037788c65fd4ecf43ba97594a6fd0f9 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 df66411a63d29f3b0ca2563d897288e684ba2880..96a6b1455f775771d001a50be0dae73a0edf6806 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 83b11d749e339bc05827aba5ddbf872c68c72596..4c71ae0cf2cbf1aaaadbb4739cf9d6be7ec2da70 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