From dab5ba470bb8586d557be19d0b9e95e8c8668c2c Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Tue, 18 Feb 2020 15:07:51 +0100
Subject: [PATCH] Improve a bunch of help texts
---
notebooks/tests/animate.ipynb | 12 ++--
notebooks/tests/assert.ipynb | 12 ++--
notebooks/tests/eval.ipynb | 12 ++--
notebooks/tests/help.ipynb | 68 +++++++++++-------
notebooks/tests/let.ipynb | 8 ++-
notebooks/tests/load_cell.ipynb | 58 +++++++++------
notebooks/tests/load_file.ipynb | 15 ++--
notebooks/tests/pref.ipynb | 70 +++++++++++++++++--
notebooks/tests/time.ipynb | 12 ++--
notebooks/tests/trace.ipynb | 20 +++---
notebooks/tests/type.ipynb | 8 ++-
.../prob2/jupyter/commands/AssertCommand.java | 5 +-
.../prob2/jupyter/commands/BrowseCommand.java | 2 +-
.../prob2/jupyter/commands/BsymbCommand.java | 2 +-
.../prob2/jupyter/commands/EvalCommand.java | 6 +-
.../prob2/jupyter/commands/ExecCommand.java | 3 +-
.../prob2/jupyter/commands/FindCommand.java | 3 +-
.../prob2/jupyter/commands/GotoCommand.java | 3 +-
.../prob2/jupyter/commands/HelpCommand.java | 4 +-
.../de/prob2/jupyter/commands/LetCommand.java | 4 +-
.../jupyter/commands/LoadCellCommand.java | 9 +--
.../jupyter/commands/LoadFileCommand.java | 6 +-
.../prob2/jupyter/commands/PrefCommand.java | 6 +-
.../prob2/jupyter/commands/TimeCommand.java | 2 +-
.../prob2/jupyter/commands/TraceCommand.java | 5 +-
.../prob2/jupyter/commands/TypeCommand.java | 4 +-
26 files changed, 237 insertions(+), 122 deletions(-)
diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb
index 494f156..c6e1ae6 100644
--- a/notebooks/tests/animate.ipynb
+++ b/notebooks/tests/animate.ipynb
@@ -14,13 +14,13 @@
"\n",
"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."
+ "The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of enabled operations (and possible parameter values) in the current state."
],
"text/plain": [
":browse\n",
"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."
+ "The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of enabled operations (and possible parameter values) in the current state."
]
},
"execution_count": 1,
@@ -46,13 +46,17 @@
"\n",
"Execute an operation.\n",
"\n",
- "A transition for the given operation is found and 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."
+ "The predicate is used to select the operation's parameter values. The parameters can be fully specified explicitly (e. g. `:exec op param1 = 123 & param2 = {1, 2}`), or they can be partially constrained (e. g. `:exec op param1 > 100 & card(param2) >= 2`) to let ProB find a valid combination of parameters. If there are multiple valid combinations of parameters that satisfy the predicate, it is undefined which one is selected by ProB.\n",
+ "\n",
+ "If no predicate is specified, the parameters are not constrained, and ProB will select an arbitrary valid combination of parameters."
],
"text/plain": [
":exec OPERATION [PREDICATE]\n",
"Execute an operation.\n",
"\n",
- "A transition for the given operation is found and 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."
+ "The predicate is used to select the operation's parameter values. The parameters can be fully specified explicitly (e. g. `:exec op param1 = 123 & param2 = {1, 2}`), or they can be partially constrained (e. g. `:exec op param1 > 100 & card(param2) >= 2`) to let ProB find a valid combination of parameters. If there are multiple valid combinations of parameters that satisfy the predicate, it is undefined which one is selected by ProB.\n",
+ "\n",
+ "If no predicate is specified, the parameters are not constrained, and ProB will select an arbitrary valid combination of parameters."
]
},
"execution_count": 2,
diff --git a/notebooks/tests/assert.ipynb b/notebooks/tests/assert.ipynb
index f247651..8d6f514 100644
--- a/notebooks/tests/assert.ipynb
+++ b/notebooks/tests/assert.ipynb
@@ -14,17 +14,21 @@
"\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",
+ "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."
+ "Only predicates and $\\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error.\n",
+ "\n",
+ "This command is intended for verifying that a condition holds at a certain point in the notebook. It may also be used in combination with the Jupyter Notebook [nbgrader](https://nbgrader.readthedocs.io/) extension for automatic checking/grading of exercises."
],
"text/plain": [
":assert PREDICATE\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",
+ "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.\n",
"\n",
- "Only predicates and $\\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error."
+ "This command is intended for verifying that a condition holds at a certain point in the notebook. It may also be used in combination with the Jupyter Notebook [nbgrader](https://nbgrader.readthedocs.io/) extension for automatic checking/grading of exercises."
]
},
"execution_count": 1,
diff --git a/notebooks/tests/eval.ipynb b/notebooks/tests/eval.ipynb
index c1b1ac0..6cdfedf 100644
--- a/notebooks/tests/eval.ipynb
+++ b/notebooks/tests/eval.ipynb
@@ -9,22 +9,26 @@
"data": {
"text/markdown": [
"```\n",
+ "FORMULA\n",
+ "// or\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",
+ "Normally you do not need to explicitly call `:eval` to evaluate formulas. If you input a formula without any command before it, it is evaluated automatically (e. g. `:eval 1 + 2` is equivalent to just `1 + 2`).\n",
"\n",
- "If the formula is a $\\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed."
+ "If the formula is a $\\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed. For more control about which solver is used to solve the predicate, use the `:solve` command."
],
"text/plain": [
+ "FORMULA\n",
+ "// or\n",
":eval FORMULA\n",
"Evaluate a formula and display the result.\n",
"\n",
- "This is equivalent to inputting the formula without a command name.\n",
+ "Normally you do not need to explicitly call `:eval` to evaluate formulas. If you input a formula without any command before it, it is evaluated automatically (e. g. `:eval 1 + 2` is equivalent to just `1 + 2`).\n",
"\n",
- "If the formula is a $\\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed."
+ "If the formula is a $\\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed. For more control about which solver is used to solve the predicate, use the `:solve` command."
]
},
"execution_count": 1,
diff --git a/notebooks/tests/help.ipynb b/notebooks/tests/help.ipynb
index cbcb887..fb5e3e3 100644
--- a/notebooks/tests/help.ipynb
+++ b/notebooks/tests/help.ipynb
@@ -15,7 +15,7 @@
{
"data": {
"text/markdown": [
- "Enter a B expression or predicate to evaluate it.\n",
+ "Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use `:load` to load an external machine file.\n",
"\n",
"You can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n",
"\n",
@@ -24,7 +24,7 @@
"* `:eval` - Evaluate a formula and display the result.\n",
"* `:solve` - Solve a predicate with the specified solver.\n",
"* `:table` - Display an expression as a table.\n",
- "* `:type` - Display the type of a formula.\n",
+ "* `:type` - Display the static type of a formula.\n",
"* `:prettyprint` - Pretty-print a predicate.\n",
"* `:let` - Evaluate an expression and store it in a local variable.\n",
"* `:unlet` - Remove a local variable.\n",
@@ -32,13 +32,13 @@
"\n",
"## Animation\n",
"\n",
- "* `::load` - Load the machine source code given in the cell body.\n",
- "* `:load` - Load the machine from the given path.\n",
+ "* `::load` - Load a B machine from the given source code.\n",
+ "* `:load` - Load a machine from a file.\n",
"* `:constants` - Set up the current machine's constants.\n",
"* `:init` - Initialise the current machine with the specified predicate\n",
"* `:exec` - Execute an operation.\n",
"* `:browse` - Show information about the current state.\n",
- "* `:trace` - Display all states and transitions in the current trace.\n",
+ "* `:trace` - Display all states and executed operations in the current trace.\n",
"* `:goto` - Go to the state with the specified index in the current trace.\n",
"* `:find` - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
"\n",
@@ -64,27 +64,27 @@
"* `:version` - Display version info about the ProB CLI and ProB 2.\n"
],
"text/plain": [
- "Enter a B expression or predicate to evaluate it.\n",
+ "Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use :load to load an external machine file.\n",
"You can also use any of the following commands. For more help on a particular command, run :help commandname.\n",
"\n",
"Evaluation:\n",
":eval - Evaluate a formula and display the result.\n",
":solve - Solve a predicate with the specified solver.\n",
":table - Display an expression as a table.\n",
- ":type - Display the type of a formula.\n",
+ ":type - Display the static type of a formula.\n",
":prettyprint - Pretty-print a predicate.\n",
":let - Evaluate an expression and store it in a local variable.\n",
":unlet - Remove a local variable.\n",
":assert - Ensure that the predicate is true, and show an error otherwise.\n",
"\n",
"Animation:\n",
- "::load - Load the machine source code given in the cell body.\n",
- ":load - Load the machine from the given path.\n",
+ "::load - Load a B machine from the given source code.\n",
+ ":load - Load a machine from a file.\n",
":constants - Set up the current machine's constants.\n",
":init - Initialise the current machine with the specified predicate\n",
":exec - Execute an operation.\n",
":browse - Show information about the current state.\n",
- ":trace - Display all states and transitions in the current trace.\n",
+ ":trace - Display all states and executed operations in the current trace.\n",
":goto - Go to the state with the specified index in the current trace.\n",
":find - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
"\n",
@@ -156,19 +156,19 @@
":load FILENAME [PREF=VALUE ...]\n",
"```\n",
"\n",
- "Load the machine from the given path.\n",
+ "Load a machine from a file.\n",
"\n",
- "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
+ "The file 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."
+ "After the file path, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
],
"text/plain": [
":load FILENAME [PREF=VALUE ...]\n",
- "Load the machine from the given path.\n",
+ "Load a machine from a file.\n",
"\n",
- "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
+ "The file 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."
+ "After the file path, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
]
},
"execution_count": 3,
@@ -189,28 +189,44 @@
"data": {
"text/markdown": [
"```\n",
+ "MACHINE\n",
+ "...\n",
+ "END\n",
+ "\n",
+ "// or\n",
+ "\n",
"::load [PREF=VALUE ...]\n",
"MACHINE\n",
"...\n",
"END\n",
"```\n",
"\n",
- "Load the machine source code given in the cell body.\n",
+ "Load a B machine from the given source code.\n",
+ "\n",
+ "Normally you do not need to explicitly call `::load` to load a machine from a cell. If you input the source code for a B machine without any command before it, it is loaded automatically.\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."
+ "If you use an explicit `::load` command, there must be a newline between `::load` and the machine source code. On the same line as `::load`, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
],
"text/plain": [
+ "MACHINE\n",
+ "...\n",
+ "END\n",
+ "\n",
+ "// or\n",
+ "\n",
"::load [PREF=VALUE ...]\n",
"MACHINE\n",
"...\n",
"END\n",
- "Load the machine source code given in the cell body.\n",
+ "Load a B machine from the given source code.\n",
+ "\n",
+ "Normally you do not need to explicitly call `::load` to load a machine from a cell. If you input the source code for a B machine without any command before it, it is loaded automatically.\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."
+ "If you use an explicit `::load` command, there must be a newline between `::load` and the machine source code. On the same line as `::load`, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
]
},
"execution_count": 4,
@@ -269,19 +285,19 @@
":load FILENAME [PREF=VALUE ...]\n",
"```\n",
"\n",
- "Load the machine from the given path.\n",
+ "Load a machine from a file.\n",
"\n",
- "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
+ "The file 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."
+ "After the file path, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
],
"text/plain": [
":load FILENAME [PREF=VALUE ...]\n",
- "Load the machine from the given path.\n",
+ "Load a machine from a file.\n",
"\n",
- "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
+ "The file 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."
+ "After the file path, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, 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/let.ipynb b/notebooks/tests/let.ipynb
index 0896dfd..630ec72 100644
--- a/notebooks/tests/let.ipynb
+++ b/notebooks/tests/let.ipynb
@@ -14,7 +14,9 @@
"\n",
"Evaluate an expression and store it in a local variable.\n",
"\n",
- "The expression is evaluated only once, in the current state, and its value is stored. Once set, variables are available in all states and are not affected by machine loads. A variable created by `:let` shadows any identifier from the machine with the same name.\n",
+ "The expression is evaluated once in the current state, and its value is stored. Once set, variables are available in all states. A variable created by `:let` shadows any identifier with the same name from the machine.\n",
+ "\n",
+ "Variables created by `:let` are retained even when a different machine is loaded. To remove a variable, use `:unlet`.\n",
"\n",
"**Note:** The values of local variables are currently stored in text form. Values must have a syntactically valid text representation, and large values may cause performance issues."
],
@@ -22,7 +24,9 @@
":let NAME EXPR\n",
"Evaluate an expression and store it in a local variable.\n",
"\n",
- "The expression is evaluated only once, in the current state, and its value is stored. Once set, variables are available in all states and are not affected by machine loads. A variable created by `:let` shadows any identifier from the machine with the same name.\n",
+ "The expression is evaluated once in the current state, and its value is stored. Once set, variables are available in all states. A variable created by `:let` shadows any identifier with the same name from the machine.\n",
+ "\n",
+ "Variables created by `:let` are retained even when a different machine is loaded. To remove a variable, use `:unlet`.\n",
"\n",
"**Note:** The values of local variables are currently stored in text form. Values must have a syntactically valid text representation, and large values may cause performance issues."
]
diff --git a/notebooks/tests/load_cell.ipynb b/notebooks/tests/load_cell.ipynb
index f122de4..7d3e416 100644
--- a/notebooks/tests/load_cell.ipynb
+++ b/notebooks/tests/load_cell.ipynb
@@ -9,28 +9,44 @@
"data": {
"text/markdown": [
"```\n",
+ "MACHINE\n",
+ "...\n",
+ "END\n",
+ "\n",
+ "// or\n",
+ "\n",
"::load [PREF=VALUE ...]\n",
"MACHINE\n",
"...\n",
"END\n",
"```\n",
"\n",
- "Load the machine source code given in the cell body.\n",
+ "Load a B machine from the given source code.\n",
+ "\n",
+ "Normally you do not need to explicitly call `::load` to load a machine from a cell. If you input the source code for a B machine without any command before it, it is loaded automatically.\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."
+ "If you use an explicit `::load` command, there must be a newline between `::load` and the machine source code. On the same line as `::load`, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
],
"text/plain": [
+ "MACHINE\n",
+ "...\n",
+ "END\n",
+ "\n",
+ "// or\n",
+ "\n",
"::load [PREF=VALUE ...]\n",
"MACHINE\n",
"...\n",
"END\n",
- "Load the machine source code given in the cell body.\n",
+ "Load a B machine from the given source code.\n",
+ "\n",
+ "Normally you do not need to explicitly call `::load` to load a machine from a cell. If you input the source code for a B machine without any command before it, it is loaded automatically.\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."
+ "If you use an explicit `::load` command, there must be a newline between `::load` and the machine source code. On the same line as `::load`, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
]
},
"execution_count": 1,
@@ -51,7 +67,7 @@
},
{
"cell_type": "code",
- "execution_count": 1,
+ "execution_count": 2,
"metadata": {},
"outputs": [
{
@@ -60,7 +76,7 @@
"Loaded machine: dinge"
]
},
- "execution_count": 1,
+ "execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
@@ -73,7 +89,7 @@
},
{
"cell_type": "code",
- "execution_count": 2,
+ "execution_count": 3,
"metadata": {},
"outputs": [
{
@@ -85,7 +101,7 @@
"{EINS,ZWEI,DREI,VIER}"
]
},
- "execution_count": 2,
+ "execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
@@ -103,7 +119,7 @@
},
{
"cell_type": "code",
- "execution_count": 3,
+ "execution_count": 4,
"metadata": {},
"outputs": [
{
@@ -112,7 +128,7 @@
"Loaded machine: things"
]
},
- "execution_count": 3,
+ "execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
@@ -126,7 +142,7 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": 5,
"metadata": {},
"outputs": [
{
@@ -138,7 +154,7 @@
"{ONE,TWO,THREE,FOUR}"
]
},
- "execution_count": 4,
+ "execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
@@ -156,7 +172,7 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 6,
"metadata": {},
"outputs": [
{
@@ -165,7 +181,7 @@
"Loaded machine: prefs"
]
},
- "execution_count": 5,
+ "execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
@@ -178,7 +194,7 @@
},
{
"cell_type": "code",
- "execution_count": 6,
+ "execution_count": 7,
"metadata": {},
"outputs": [
{
@@ -190,7 +206,7 @@
"{−5,−4,−3,−2,−1,0,1,2,3,4,5}"
]
},
- "execution_count": 6,
+ "execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
@@ -208,7 +224,7 @@
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 8,
"metadata": {},
"outputs": [
{
@@ -229,21 +245,21 @@
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 9,
"metadata": {
"scrolled": true
},
"outputs": [
{
"ename": "WithSourceCodeException",
- "evalue": "de.prob.exception.ProBError: Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\nError: Identifier 'x' declared twice at (Line:Col[:File]) (Line:2 Col:17) and (Line:2 Col:14) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)",
+ "evalue": "de.prob.exception.ProBError: Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\nError: Identifier 'x' (local from duplicate) already declared at (Line:2 Col:14) (local from duplicate) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProlog said no.\u001b[0m",
"\u001b[1m\u001b[30m2 errors:\u001b[0m",
"\u001b[1m\u001b[31mError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\u001b[0m",
"\u001b[1m\u001b[30m CONSTANTS x, \u001b[0m\u001b[1m\u001b[30m\u001b[41mx\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
- "\u001b[1m\u001b[31mError: Identifier 'x' declared twice at (Line:Col[:File]) (Line:2 Col:17) and (Line:2 Col:14) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\u001b[0m",
+ "\u001b[1m\u001b[31mError: Identifier 'x' (local from duplicate) already declared at (Line:2 Col:14) (local from duplicate) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\u001b[0m",
"\u001b[1m\u001b[30m CONSTANTS x, \u001b[0m\u001b[1m\u001b[30m\u001b[41mx\u001b[0m\u001b[1m\u001b[30m\u001b[0m"
]
}
@@ -258,7 +274,7 @@
},
{
"cell_type": "code",
- "execution_count": 9,
+ "execution_count": 10,
"metadata": {},
"outputs": [
{
diff --git a/notebooks/tests/load_file.ipynb b/notebooks/tests/load_file.ipynb
index 1fdbfea..c57db3f 100644
--- a/notebooks/tests/load_file.ipynb
+++ b/notebooks/tests/load_file.ipynb
@@ -12,22 +12,19 @@
":load FILENAME [PREF=VALUE ...]\n",
"```\n",
"\n",
- "Load the machine from the given path.\n",
+ "Load a machine from a file.\n",
"\n",
- "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
+ "The file 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."
+ "After the file path, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, 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",
+ "Load a machine from a file.\n",
"\n",
- "The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n",
+ "The file 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."
+ "After the file path, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
]
},
"execution_count": 1,
diff --git a/notebooks/tests/pref.ipynb b/notebooks/tests/pref.ipynb
index 38d1555..8846808 100644
--- a/notebooks/tests/pref.ipynb
+++ b/notebooks/tests/pref.ipynb
@@ -10,23 +10,25 @@
"text/markdown": [
"```\n",
":pref [NAME ...]\n",
+ "// or\n",
":pref NAME=VALUE [NAME=VALUE ...]\n",
"```\n",
"\n",
"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",
+ "In the first form, the values of the given preferences are displayed (or all preferences, if no preference names are given). In the second form, the values of the given preferences are changed. 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."
+ "Certain preference changes do not take full effect when performed on an already loaded machine. Such preferences must be set when the machine is loaded using the `::load` or `:load` command."
],
"text/plain": [
":pref [NAME ...]\n",
+ "// or\n",
":pref NAME=VALUE [NAME=VALUE ...]\n",
"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",
+ "In the first form, the values of the given preferences are displayed (or all preferences, if no preference names are given). In the second form, the values of the given preferences are changed. 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."
+ "Certain preference changes do not take full effect when performed on an already loaded machine. Such preferences must be set when the machine is loaded using the `::load` or `:load` command."
]
},
"execution_count": 1,
@@ -57,14 +59,21 @@
"ALLOW_INCOMPLETE_SETUP_CONSTANTS = false\n",
"ALLOW_LOCAL_OPERATION_CALLS = false\n",
"ALLOW_NEW_OPERATIONS_IN_REFINEMENT = false\n",
+ "ALLOW_OPERATION_CALLS_IN_EXPRESSIONS = false\n",
+ "ALLOW_OUTPUT_READING = false\n",
"ALLOW_SIMULTANEOUS_ASSIGNMENTS = false\n",
"ALLOW_UNTYPED_IDENTIFIERS = false\n",
+ "ALLOY_SCOPELESS_TRANSLATION = false\n",
+ "ALLOY_STRICT_INTEGERS = true\n",
+ "ALLOY_TRANSLATION_FOR_PROOF = false\n",
+ "ALLOY_USE_IMPLEMENTABLE_INTEGERS = false\n",
"ATELIERB_KRT_PATH = krt\n",
"BBRESULTS = false\n",
"BOOL_AS_PREDICATE = false\n",
"BUGLY = false\n",
"CHR = false\n",
"CLPFD = true\n",
+ "COMPILE_WHILE = true\n",
"COMPRESSION = false\n",
"CSE = false\n",
"CSE_PRED = true\n",
@@ -73,25 +82,59 @@
"CSP_STRIP_SOURCE_LOC = false\n",
"DATA_VALIDATION = false\n",
"DEFAULT_SETSIZE = 2\n",
- "DETECT_LAMBDAS = false\n",
+ "DETECT_LAMBDAS = true\n",
"DISPROVER_MODE = false\n",
"DOT = /opt/local/bin/dot\n",
+ "DOT_ARC_COLORS = true\n",
"DOT_ARGUMENTS = true\n",
"DOT_COLOR_ARC = #006391\n",
"DOT_COLOR_NODE = #99BF38\n",
"DOT_COLOR_NODE_ERROR = #FF3800\n",
"DOT_COLOR_NODE_GOAL = orange\n",
"DOT_COLOR_NODE_OPEN = #F4E3C1\n",
+ "DOT_COLOUR_GOAL = true\n",
+ "DOT_CURRENT_NODE_SHAPE = doubleoctagon\n",
+ "DOT_DECOMPOSE_NODES = true\n",
+ "DOT_DEFINITIONS_SHOW_ALL = false\n",
+ "DOT_DEFINITIONS_USE_SUB_GRAPH = true\n",
+ "DOT_EDGE_FONT_SIZE = 12\n",
"DOT_EDGE_LABELS = true\n",
"DOT_ENGINE = dot\n",
+ "DOT_EVENT_HIERARCHY_EDGE_COL = #806040\n",
+ "DOT_EVENT_HIERARCHY_EXTENDS_COL = gray50\n",
+ "DOT_EVENT_HIERARCHY_GRD_KEEP_COL = #E0C080\n",
+ "DOT_EVENT_HIERARCHY_GRD_STRGTH_COL = gray83\n",
+ "DOT_EVENT_HIERARCHY_HORIZONTAL = true\n",
+ "DOT_EVENT_HIERARCHY_MCH_COL = gray95\n",
+ "DOT_EVENT_HIERARCHY_NEW_COL = #C06040\n",
+ "DOT_EVENT_HIERARCHY_REF_COL = #C0A060\n",
+ "DOT_EVENT_HIERARCHY_RENAME_COL = #E0E0A0\n",
+ "DOT_EVENT_HIERARCHY_RENAME_UNCHG_COL = #E0F0E0\n",
+ "DOT_EVENT_HIERARCHY_UNCHG_COL = gray92\n",
+ "DOT_EXPRESSION_NODE_SHAPE = record\n",
+ "DOT_FILL_NORMAL_NODES = false\n",
"DOT_FUNCTIONS = false\n",
"DOT_IDS = false\n",
"DOT_INFO = true\n",
"DOT_LOOPS = true\n",
+ "DOT_MACHINE_HIERARCHY_MAX_IDS = 0\n",
+ "DOT_NODE_FONT_SIZE = 12\n",
+ "DOT_NORMAL_NODE_SHAPE = box\n",
"DOT_PEN_WIDTH = 2\n",
+ "DOT_PREDICATE_NODE_SHAPE = rect\n",
+ "DOT_PROJECTION_DEF_COL = solid\n",
+ "DOT_PROJECTION_DET_COL = black\n",
+ "DOT_PROJECTION_LABEL_LIMIT = 75\n",
+ "DOT_PROJECTION_NON_DEF_COL = dashed\n",
+ "DOT_PROJECTION_NON_DET_COL = #806040\n",
"DOT_PROP = false\n",
"DOT_ROOT = true\n",
+ "DOT_ROOT_SHAPE = invtriangle\n",
+ "DOT_SCOPE_LIMIT_COL = gray\n",
"DOT_SHOW_OP_READ_WRITES = true\n",
+ "DOT_USE_CONSTANTS = true\n",
+ "DOT_USE_UNICODE = true\n",
+ "DOT_VARIABLE_MODIFICATION_HIDE_ONLY_WRITTEN = false\n",
"DOUBLE_EVALUATION = true\n",
"EDITOR = /usr/local/bin/bbedit\n",
"EDITOR_GUI = /Applications/BBEdit.app\n",
@@ -104,6 +147,8 @@
"INTERNAL_ARGUMENT_PREFIX = $none\n",
"INVARIANT_CHECKING = true\n",
"JAVA_PATH = /usr/bin/java\n",
+ "JVM_PARSER_ARGS = \n",
+ "JVM_PARSER_HEAP_MB = 0\n",
"KODKOD = false\n",
"KODKOD_MAX_NR_SOLS = 22\n",
"KODKOD_ONLY_FULL = true\n",
@@ -112,12 +157,15 @@
"KODKOD_SYMMETRY = 0\n",
"LATEX_ENCODING = auto\n",
"LATEX_GREEK_IDENTIFIERS = false\n",
+ "LIFT_EXISTS = false\n",
"LTSMIN = ./lib/\n",
"MAXINT = 3\n",
"MAX_DISPLAY_SET = 100\n",
"MAX_INITIALISATIONS = 4\n",
"MAX_OPERATIONS = 10\n",
+ "MC_DC_Level = 2\n",
"MEMO = false\n",
+ "MEMOIZE_FUNCTIONS = false\n",
"MINIMAL_TEST_SUITES = true\n",
"MININT = -1\n",
"NDJSON_ERROR_LOG_FILE = \n",
@@ -128,6 +176,7 @@
"PARTITION_PROPERTIES = true\n",
"PARTITION_PROPERTIES_INLINE = true\n",
"PERFORMANCE_INFO = false\n",
+ "PERFORMANCE_INFO_LIMIT = 100\n",
"PGE = off\n",
"PP_CS_STYLE_SEQUENCES = false\n",
"PP_FROZEN_INFOS = false\n",
@@ -136,14 +185,19 @@
"PROB2_TRACE_FILE_UNIQUE = false\n",
"PROOF_INFO = true\n",
"RAISE_ABORT_IMMEDIATELY = false\n",
+ "RANDOMISED_RESTART_INIT = false\n",
"RANDOMISE_ENUMERATION_ORDER = false\n",
"RANDOMISE_OPERATION_ORDER = false\n",
"REMOVE_IMPLIED_CONSTRAINTS = false\n",
"REPL_CACHE_PARSING = false\n",
"REPL_UNICODE = false\n",
"REQUIRE_OUTPUT_ASSIGNMENT = false\n",
+ "SAFETY_MODEL_CHECK = false\n",
+ "SAT_SUPPORTED_INTERPRETER = false\n",
"SHOW_EVENTB_ANY_VALUES = false\n",
"SMT = false\n",
+ "SMTLIB_BOOL_ARRAYS_TO_SETS = false\n",
+ "SMTLIB_PREPROCESS = false\n",
"SMT_SUPPORTED_INTERPRETER = false\n",
"SOLVER_STRENGTH = 0\n",
"STATIC_ORDERING = false\n",
@@ -155,20 +209,24 @@
"SYMBOLIC = false\n",
"SYMBOLIC_MC_TRY_OTHER_SOLVERS = false\n",
"SYMMETRY_MODE = off\n",
+ "SYNTAX_HIGHLIGHT = true\n",
"TIME_OUT = 2500\n",
"TK_CUSTOM_STATE_VIEW_FONT_NAME = \n",
"TK_CUSTOM_STATE_VIEW_FONT_SIZE = 0\n",
"TK_CUSTOM_STATE_VIEW_PADDING = 0\n",
"TK_CUSTOM_STATE_VIEW_STRING_PADDING = 10\n",
+ "TK_CUSTOM_STATE_VIEW_VISIBLE = true\n",
"TLC_WORKERS = 2\n",
"TRACE_INFO = false\n",
"TRACE_UPON_ERROR = false\n",
"TRY_ATELIERB_PROVERS = false\n",
"TRY_FIND_ABORT = false\n",
"TYPE_CHECK_DEFINITIONS = false\n",
+ "USELESS_CODE_ELIMINATION = false\n",
+ "USE_IGNORE_PRAGMAS = false\n",
"USE_RECORD_CONSTRUCTION = true\n",
+ "USE_SCOPE_DEFINITION = true\n",
"WARN_IF_DEFINITION_HIDES_VARIABLE = true\n",
- "WARN_WHEN_EXPANDING_INFINITE_CLOSURES = 5\n",
"XML_ENCODING = auto\n"
]
},
diff --git a/notebooks/tests/time.ipynb b/notebooks/tests/time.ipynb
index ff5eb76..016287b 100644
--- a/notebooks/tests/time.ipynb
+++ b/notebooks/tests/time.ipynb
@@ -14,7 +14,7 @@
"\n",
"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",
+ "The time is internally 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 nanosecond precision, but the actual resolution of the measurement is system-dependent and often much less accurate than nanoseconds.\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."
],
@@ -22,7 +22,7 @@
":time COMMAND [ARGS ...]\n",
"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",
+ "The time is internally 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 nanosecond precision, but the actual resolution of the measurement is system-dependent and often much less accurate than nanoseconds.\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."
]
@@ -51,10 +51,10 @@
{
"data": {
"text/markdown": [
- "Execution time: 1.029510290 seconds"
+ "Execution time: 1.034897011 seconds"
],
"text/plain": [
- "Execution time: 1.029510290 seconds"
+ "Execution time: 1.034897011 seconds"
]
},
"metadata": {},
@@ -90,10 +90,10 @@
{
"data": {
"text/markdown": [
- "Execution time: 1.156164498 seconds"
+ "Execution time: 1.206485155 seconds"
],
"text/plain": [
- "Execution time: 1.156164498 seconds"
+ "Execution time: 1.206485155 seconds"
]
},
"metadata": {},
diff --git a/notebooks/tests/trace.ipynb b/notebooks/tests/trace.ipynb
index 1529644..b395563 100644
--- a/notebooks/tests/trace.ipynb
+++ b/notebooks/tests/trace.ipynb
@@ -12,19 +12,19 @@
":trace\n",
"```\n",
"\n",
- "Display all states and transitions in the current trace.\n",
+ "Display all states and executed operations in the current trace.\n",
"\n",
"Each state has an index, which can be passed to the `:goto` command to go to that state.\n",
"\n",
- "The first state (index -1) is always the root state. All other states are reached from the root state by following (previously executed) transitions."
+ "The first state (index -1) is always the root state. All other states are reached from the root state by following previously executed operations."
],
"text/plain": [
":trace\n",
- "Display all states and transitions in the current trace.\n",
+ "Display all states and executed operations in the current trace.\n",
"\n",
"Each state has an index, which can be passed to the `:goto` command to go to that state.\n",
"\n",
- "The first state (index -1) is always the root state. All other states are reached from the root state by following (previously executed) transitions."
+ "The first state (index -1) is always the root state. All other states are reached from the root state by following previously executed operations."
]
},
"execution_count": 1,
@@ -52,7 +52,7 @@
"\n",
"Use the `:trace` command to view the current trace and the indices of its states. Index -1 refers to the root state and is always available.\n",
"\n",
- "Going backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in a state *will* discard any parts of the trace after that state (and replace them with the destination state of the executed transition)."
+ "Going backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in an older state *will* discard any parts of the trace after that state, and replace them with the new state reached after executing the operation."
],
"text/plain": [
":goto INDEX\n",
@@ -60,7 +60,7 @@
"\n",
"Use the `:trace` command to view the current trace and the indices of its states. Index -1 refers to the root state and is always available.\n",
"\n",
- "Going backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in a state *will* discard any parts of the trace after that state (and replace them with the destination state of the executed transition)."
+ "Going backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in an older state *will* discard any parts of the trace after that state, and replace them with the new state reached after executing the operation."
]
},
"execution_count": 2,
@@ -124,11 +124,11 @@
"data": {
"text/markdown": [
"* -1: Root state\n",
- "* 0: `$initialise_machine` **(current)**"
+ "* 0: `INITIALISATION()` **(current)**"
],
"text/plain": [
"-1: Root state\n",
- "0: $initialise_machine (current)"
+ "0: INITIALISATION() (current)"
]
},
"execution_count": 5,
@@ -169,11 +169,11 @@
"data": {
"text/markdown": [
"* -1: Root state **(current)**\n",
- "* 0: `$initialise_machine`"
+ "* 0: `INITIALISATION()`"
],
"text/plain": [
"-1: Root state (current)\n",
- "0: $initialise_machine"
+ "0: INITIALISATION()"
]
},
"execution_count": 7,
diff --git a/notebooks/tests/type.ipynb b/notebooks/tests/type.ipynb
index 7da9987..9745c40 100644
--- a/notebooks/tests/type.ipynb
+++ b/notebooks/tests/type.ipynb
@@ -12,11 +12,15 @@
":type FORMULA\n",
"```\n",
"\n",
- "Display the type of a formula."
+ "Display the static type of a formula.\n",
+ "\n",
+ "The type is displayed in B syntax. If the formula is a predicate, the type is `predicate`."
],
"text/plain": [
":type FORMULA\n",
- "Display the type of a formula."
+ "Display the static type of a formula.\n",
+ "\n",
+ "The type is displayed in B syntax. If the formula is a predicate, the type is `predicate`."
]
},
"execution_count": 1,
diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index f4fe97d..1268423 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
@@ -46,8 +46,9 @@ public final class AssertCommand implements Command {
@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.";
+ return "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.\n\n"
+ + "This command is intended for verifying that a condition holds at a certain point in the notebook. It may also be used in combination with the Jupyter Notebook [nbgrader](https://nbgrader.readthedocs.io/) extension for automatic checking/grading of exercises.";
}
@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
index f65282f..852ea6f 100644
--- a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
@@ -49,7 +49,7 @@ public final class BrowseCommand implements Command {
@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.";
+ return "The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of enabled operations (and possible parameter values) in the current state.";
}
private static @NotNull String listToString(final List<String> list) {
diff --git a/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java b/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java
index bd961b2..d51a4f4 100644
--- a/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java
@@ -31,7 +31,7 @@ public final class BsymbCommand implements Command {
@Override
public @NotNull String getHelpBody() {
- return "";
+ return "If you want to use bsymb.sty commands in your Markdown cells, you *must* run `:bsymb` first. Otherwise the commands may not be reliably available after reopening the notebook.";
}
@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
index 3e63983..38267a9 100644
--- a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
@@ -32,7 +32,7 @@ public final class EvalCommand implements Command {
@Override
public @NotNull String getSyntax() {
- return ":eval FORMULA";
+ return "FORMULA\n// or\n:eval FORMULA";
}
@Override
@@ -42,8 +42,8 @@ public final class EvalCommand implements Command {
@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.";
+ return "Normally you do not need to explicitly call `:eval` to evaluate formulas. If you input a formula without any command before it, it is evaluated automatically (e. g. `:eval 1 + 2` is equivalent to just `1 + 2`).\n\n"
+ + "If the formula is a $\\mathit{TRUE}$ predicate with free variables, the variable values found while solving are displayed. For more control about which solver is used to solve the predicate, use the `:solve` command.";
}
@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
index e41a07e..43e607d 100644
--- a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
@@ -48,7 +48,8 @@ public final class ExecCommand implements Command {
@Override
public @NotNull String getHelpBody() {
- return "A transition for the given operation is found and 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.";
+ return "The predicate is used to select the operation's parameter values. The parameters can be fully specified explicitly (e. g. `:exec op param1 = 123 & param2 = {1, 2}`), or they can be partially constrained (e. g. `:exec op param1 > 100 & card(param2) >= 2`) to let ProB find a valid combination of parameters. If there are multiple valid combinations of parameters that satisfy the predicate, it is undefined which one is selected by ProB.\n\n"
+ + "If no predicate is specified, the parameters are not constrained, and ProB will select an arbitrary valid combination of parameters.";
}
@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/FindCommand.java b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
index d9ee3c6..ebf0738 100644
--- a/src/main/java/de/prob2/jupyter/commands/FindCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
@@ -44,7 +44,8 @@ public final class FindCommand implements Command {
@Override
public @NotNull String getHelpBody() {
- return "If such a state is found, it is made the current state, otherwise an error is displayed.\n\nNote that this command does not necessarily find a valid *trace* to the found state. Instead, in some cases a single \"fake\" transition is added to the trace, which goes directly to the found state and does not use the machine's operations to reach it.";
+ return "If such a state is found, it is made the current state, otherwise an error is displayed.\n\n"
+ + "Note that this command does not necessarily find a valid *trace* to the found state. Instead, this command may a single \"fake\" transition to the trace, which goes directly to the found state and does not use the machine's operations to reach it. Such a state may or may not be reachable by a sequence of normal operations.";
}
@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/GotoCommand.java b/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
index 497202e..e02ec18 100644
--- a/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
@@ -40,7 +40,8 @@ public final class GotoCommand implements Command {
@Override
public @NotNull String getHelpBody() {
- return "Use the `:trace` command to view the current trace and the indices of its states. Index -1 refers to the root state and is always available.\n\nGoing backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in a state *will* discard any parts of the trace after that state (and replace them with the destination state of the executed transition).";
+ return "Use the `:trace` command to view the current trace and the indices of its states. Index -1 refers to the root state and is always available.\n\n"
+ + "Going backwards in the current trace does *not* discard any parts of the trace, so it is possible to go forward again afterwards. However, executing an operation in an older state *will* discard any parts of the trace after that state, and replace them with the new state reached after executing the operation.";
}
@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
index c8a510a..1ce3f6e 100644
--- a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
@@ -91,8 +91,8 @@ public final class HelpCommand implements Command {
final ProBKernel kernel = this.injector.getInstance(ProBKernel.class);
final List<String> args = CommandUtils.splitArgs(argString);
if (args.isEmpty()) {
- final StringBuilder sb = new StringBuilder("Enter a B expression or predicate to evaluate it.\nYou can also use any of the following commands. For more help on a particular command, run :help commandname.\n");
- final StringBuilder sbMarkdown = new StringBuilder("Enter a B expression or predicate to evaluate it.\n\nYou can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n");
+ final StringBuilder sb = new StringBuilder("Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use :load to load an external machine file.\nYou can also use any of the following commands. For more help on a particular command, run :help commandname.\n");
+ final StringBuilder sbMarkdown = new StringBuilder("Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use `:load` to load an external machine file.\n\nYou can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n");
final Map<Class<? extends Command>, Command> commandsByClass = kernel.getCommands()
.values()
diff --git a/src/main/java/de/prob2/jupyter/commands/LetCommand.java b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
index 35669d3..a8d5eb0 100644
--- a/src/main/java/de/prob2/jupyter/commands/LetCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
@@ -47,7 +47,9 @@ public final class LetCommand implements Command {
@Override
public @NotNull String getHelpBody() {
- return "The expression is evaluated only once, in the current state, and its value is stored. Once set, variables are available in all states and are not affected by machine loads. A variable created by `:let` shadows any identifier from the machine with the same name.\n\n**Note:** The values of local variables are currently stored in text form. Values must have a syntactically valid text representation, and large values may cause performance issues.";
+ return "The expression is evaluated once in the current state, and its value is stored. Once set, variables are available in all states. A variable created by `:let` shadows any identifier with the same name from the machine.\n\n"
+ + "Variables created by `:let` are retained even when a different machine is loaded. To remove a variable, use `:unlet`.\n\n"
+ + "**Note:** The values of local variables are currently stored in text form. Values must have a syntactically valid text representation, and large values may cause performance issues.";
}
@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
index 08ee240..0056fbc 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
@@ -44,18 +44,19 @@ public final class LoadCellCommand implements Command {
@Override
public @NotNull String getSyntax() {
- return "::load [PREF=VALUE ...]\nMACHINE\n...\nEND";
+ return "MACHINE\n...\nEND\n\n// or\n\n::load [PREF=VALUE ...]\nMACHINE\n...\nEND";
}
@Override
public @NotNull String getShortHelp() {
- return "Load the machine source code given in the cell body.";
+ return "Load a B machine from the given source code.";
}
@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.";
+ return "Normally you do not need to explicitly call `::load` to load a machine from a cell. If you input the source code for a B machine without any command before it, it is loaded automatically.\n\n"
+ + "There must be a newline between the `::load` command name and the machine code.\n\n"
+ + "If you use an explicit `::load` command, there must be a newline between `::load` and the machine source code. On the same line as `::load`, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, 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 04fb385..1b4f2c4 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
@@ -61,13 +61,13 @@ public final class LoadFileCommand implements Command {
@Override
public @NotNull String getShortHelp() {
- return "Load the machine from the given path.";
+ return "Load a machine from a file.";
}
@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.";
+ return "The file path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).\n\n"
+ + "After the file path, you can set the values of one or more ProB preferences that should be applied to the newly loaded machine. Preferences can also be changed using the `:pref` command after a machine has been loaded, 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/PrefCommand.java b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
index 28df02a..3672b8b 100644
--- a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
@@ -37,7 +37,7 @@ public final class PrefCommand implements Command {
@Override
public @NotNull String getSyntax() {
- return ":pref [NAME ...]\n:pref NAME=VALUE [NAME=VALUE ...]";
+ return ":pref [NAME ...]\n// or\n:pref NAME=VALUE [NAME=VALUE ...]";
}
@Override
@@ -47,8 +47,8 @@ public final class PrefCommand implements Command {
@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.";
+ return "In the first form, the values of the given preferences are displayed (or all preferences, if no preference names are given). In the second form, the values of the given preferences are changed. 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 an already loaded machine. Such preferences must be set when the machine is loaded using the `::load` or `:load` command.";
}
@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/TimeCommand.java b/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
index c9270d8..ee46d95 100644
--- a/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
@@ -42,7 +42,7 @@ public final class TimeCommand implements Command {
@Override
public @NotNull String getHelpBody() {
- return "The time is internally 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 nanosecond precision, but the actual resolution of the measurement is system-dependent and often much larger than nanoseconds.\n\n"
+ return "The time is internally 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 nanosecond precision, but the actual resolution of the measurement is system-dependent and often much less accurate than nanoseconds.\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.";
}
diff --git a/src/main/java/de/prob2/jupyter/commands/TraceCommand.java b/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
index 773f1bc..c3f97bc 100644
--- a/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
@@ -38,12 +38,13 @@ public final class TraceCommand implements Command {
@Override
public @NotNull String getShortHelp() {
- return "Display all states and transitions in the current trace.";
+ return "Display all states and executed operations in the current trace.";
}
@Override
public @NotNull String getHelpBody() {
- return "Each state has an index, which can be passed to the `:goto` command to go to that state.\n\nThe first state (index -1) is always the root state. All other states are reached from the root state by following (previously executed) transitions.";
+ return "Each state has an index, which can be passed to the `:goto` command to go to that state.\n\n"
+ + "The first state (index -1) is always the root state. All other states are reached from the root state by following previously executed operations.";
}
@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
index 8c0de73..f103035 100644
--- a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
@@ -41,12 +41,12 @@ public final class TypeCommand implements Command {
@Override
public @NotNull String getShortHelp() {
- return "Display the type of a formula.";
+ return "Display the static type of a formula.";
}
@Override
public @NotNull String getHelpBody() {
- return "";
+ return "The type is displayed in B syntax. If the formula is a predicate, the type is `predicate`.";
}
@Override
--
GitLab