"Type a valid B expression, or one of the following commands:\n",
"Enter a B expression or predicate to evaluate it.\n",
"\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",
"* `:check` Check the machine's properties, invariant, or assertions in 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.\n",
"* `:find` Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
"* `:goto` Go to the state with the specified index in the current trace.\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",
"* `:show` Show the machine's animation function visualisation for the current state.\n",
"* `:solve` Solve a predicate with the specified solver.\n",
"* `:stats` Show statistics about the state space.\n",
"* `:table` Display an expression as a table.\n",
"* `:time` Execute the given command and measure how long it takes to execute.\n",
"* `:trace` Display all states and transitions in the current trace.\n",
"* `:type` Display the type of a formula.\n",
"* `:version` Display version info about the ProB CLI and ProB 2.\n"
"You can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n",
"\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",
"* `:bsymb` - Load all bsymb.sty command definitions, so that they can be used in $\\LaTeX$ formulas in Markdown cells.\n",
"* `:check` - Check the machine's properties, invariant, or assertions in 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.\n",
"* `:find` - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
"* `:goto` - Go to the state with the specified index in the current trace.\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",
"* `:let` - Evaluate an expression and store it in a local variable.\n",
"* `:load` - Load the machine from the given path.\n",
"* `:modelcheck` - Run the ProB model checker on the current model.\n",
"* `:pref` - View or change the value of one or more preferences.\n",
"* `:prettyprint` - Pretty-print a predicate.\n",
"* `:show` - Show the machine's animation function visualisation for the current state.\n",
"* `:solve` - Solve a predicate with the specified solver.\n",
"* `:stats` - Show statistics about the state space.\n",
"* `:table` - Display an expression as a table.\n",
"* `:time` - Execute the given command and measure how long it takes to execute.\n",
"* `:trace` - Display all states and transitions in the current trace.\n",
"* `:type` - Display the type of a formula.\n",
"* `:unlet` - Remove a local variable.\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 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",
":check Check the machine's properties, invariant, or assertions in 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.\n",
":find Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
":goto Go to the state with the specified index in the current trace.\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",
":show Show the machine's animation function visualisation for the current state.\n",
":solve Solve a predicate with the specified solver.\n",
":stats Show statistics about the state space.\n",
":table Display an expression as a table.\n",
":time Execute the given command and measure how long it takes to execute.\n",
":trace Display all states and transitions in the current trace.\n",
":type Display the type of a formula.\n",
":version Display version info about the ProB CLI and ProB 2.\n"
"Enter a B expression or predicate to evaluate it.\n",
"You can also use any of the following commands. For more help on a particular command, run :help commandname.\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",
":bsymb - Load all bsymb.sty command definitions, so that they can be used in $\\LaTeX$ formulas in Markdown cells.\n",
":check - Check the machine's properties, invariant, or assertions in 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.\n",
":find - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
":goto - Go to the state with the specified index in the current trace.\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",
":let - Evaluate an expression and store it in a local variable.\n",
":load - Load the machine from the given path.\n",
":modelcheck - Run the ProB model checker on the current model.\n",
":pref - View or change the value of one or more preferences.\n",
":prettyprint - Pretty-print a predicate.\n",
":show - Show the machine's animation function visualisation for the current state.\n",
":solve - Solve a predicate with the specified solver.\n",
":stats - Show statistics about the state space.\n",
":table - Display an expression as a table.\n",
":time - Execute the given command and measure how long it takes to execute.\n",
":trace - Display all states and transitions in the current trace.\n",
":type - Display the type of a formula.\n",
":unlet - Remove a local variable.\n",
":version - Display version info about the ProB CLI and ProB 2.\n"
]
},
"execution_count": 1,
...
...
%% Cell type:markdown id: tags:
`:help` can be used to list all commands, or get help for a specific command.
%% Cell type:code id: tags:
``` prob
:help
```
%% Output
Type a valid B expression, or one of the following commands:
Enter a B expression or predicate to evaluate it.
* `::load` Load the machine source code given in the cell body.
* `::render` Render some content with the specified MIME type.
* `:assert` Ensure that the predicate is true, and show an error otherwise.
* `:browse` Show information about the current state.
* `:check` Check the machine's properties, invariant, or assertions in the current state.
* `:constants` Set up the current machine's constants.
* `:dot` Execute and show a dot visualisation.
* `:eval` Evaluate a formula and display the result.
* `:exec` Execute an operation.
* `:find` Try to find a state for which the given predicate is true (in addition to the machine's invariant).
* `:goto` Go to the state with the specified index in the current trace.
* `:groovy` Evaluate the given Groovy expression.
* `:help` Display help for a specific command, or general help about the REPL.
* `:init` Initialise the current machine with the specified predicate
* `:load` Load the machine from the given path.
* `:pref` View or change the value of one or more preferences.
* `:prettyprint` Pretty-print a predicate.
* `:show` Show the machine's animation function visualisation for the current state.
* `:solve` Solve a predicate with the specified solver.
* `:stats` Show statistics about the state space.
* `:table` Display an expression as a table.
* `:time` Execute the given command and measure how long it takes to execute.
* `:trace` Display all states and transitions in the current trace.
* `:type` Display the type of a formula.
* `:version` Display version info about the ProB CLI and ProB 2.
Type a valid B expression, or one of the following commands:
::load Load the machine source code given in the cell body.
::render Render some content with the specified MIME type.
:assert Ensure that the predicate is true, and show an error otherwise.
:browse Show information about the current state.
:check Check the machine's properties, invariant, or assertions in the current state.
:constants Set up the current machine's constants.
:dot Execute and show a dot visualisation.
:eval Evaluate a formula and display the result.
:exec Execute an operation.
:find Try to find a state for which the given predicate is true (in addition to the machine's invariant).
:goto Go to the state with the specified index in the current trace.
:groovy Evaluate the given Groovy expression.
:help Display help for a specific command, or general help about the REPL.
:init Initialise the current machine with the specified predicate
:load Load the machine from the given path.
:pref View or change the value of one or more preferences.
:prettyprint Pretty-print a predicate.
:show Show the machine's animation function visualisation for the current state.
:solve Solve a predicate with the specified solver.
:stats Show statistics about the state space.
:table Display an expression as a table.
:time Execute the given command and measure how long it takes to execute.
:trace Display all states and transitions in the current trace.
:type Display the type of a formula.
:version Display version info about the ProB CLI and ProB 2.
You can also use any of the following commands. For more help on a particular command, run `:help commandname`.
* `::load` - Load the machine source code given in the cell body.
* `::render` - Render some content with the specified MIME type.
* `:assert` - Ensure that the predicate is true, and show an error otherwise.
* `:browse` - Show information about the current state.
* `:bsymb` - Load all bsymb.sty command definitions, so that they can be used in $\LaTeX$ formulas in Markdown cells.
* `:check` - Check the machine's properties, invariant, or assertions in the current state.
* `:constants` - Set up the current machine's constants.
* `:dot` - Execute and show a dot visualisation.
* `:eval` - Evaluate a formula and display the result.
* `:exec` - Execute an operation.
* `:find` - Try to find a state for which the given predicate is true (in addition to the machine's invariant).
* `:goto` - Go to the state with the specified index in the current trace.
* `:groovy` - Evaluate the given Groovy expression.
* `:help` - Display help for a specific command, or general help about the REPL.
* `:init` - Initialise the current machine with the specified predicate
* `:let` - Evaluate an expression and store it in a local variable.
* `:load` - Load the machine from the given path.
* `:modelcheck` - Run the ProB model checker on the current model.
* `:pref` - View or change the value of one or more preferences.
* `:prettyprint` - Pretty-print a predicate.
* `:show` - Show the machine's animation function visualisation for the current state.
* `:solve` - Solve a predicate with the specified solver.
* `:stats` - Show statistics about the state space.
* `:table` - Display an expression as a table.
* `:time` - Execute the given command and measure how long it takes to execute.
* `:trace` - Display all states and transitions in the current trace.
* `:type` - Display the type of a formula.
* `:unlet` - Remove a local variable.
* `:version` - Display version info about the ProB CLI and ProB 2.
Enter a B expression or predicate to evaluate it.
You can also use any of the following commands. For more help on a particular command, run :help commandname.
::load - Load the machine source code given in the cell body.
::render - Render some content with the specified MIME type.
:assert - Ensure that the predicate is true, and show an error otherwise.
:browse - Show information about the current state.
:bsymb - Load all bsymb.sty command definitions, so that they can be used in $\LaTeX$ formulas in Markdown cells.
:check - Check the machine's properties, invariant, or assertions in the current state.
:constants - Set up the current machine's constants.
:dot - Execute and show a dot visualisation.
:eval - Evaluate a formula and display the result.
:exec - Execute an operation.
:find - Try to find a state for which the given predicate is true (in addition to the machine's invariant).
:goto - Go to the state with the specified index in the current trace.
:groovy - Evaluate the given Groovy expression.
:help - Display help for a specific command, or general help about the REPL.
:init - Initialise the current machine with the specified predicate
:let - Evaluate an expression and store it in a local variable.
:load - Load the machine from the given path.
:modelcheck - Run the ProB model checker on the current model.
:pref - View or change the value of one or more preferences.
:prettyprint - Pretty-print a predicate.
:show - Show the machine's animation function visualisation for the current state.
:solve - Solve a predicate with the specified solver.
:stats - Show statistics about the state space.
:table - Display an expression as a table.
:time - Execute the given command and measure how long it takes to execute.
:trace - Display all states and transitions in the current trace.
:type - Display the type of a formula.
:unlet - Remove a local variable.
:version - Display version info about the ProB CLI and ProB 2.
%% Cell type:code id: tags:
``` prob
:help :help
```
%% Output
```
:help [COMMAND]
```
Display help for a specific command, or general help about the REPL.
:help [COMMAND]
Display help for a specific command, or general help about the REPL.
%% Cell type:code id: tags:
``` prob
:help :load
```
%% Output
```
:load FILENAME [PREF=VALUE ...]
```
Load the machine from the given path.
The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).
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.
:load FILENAME [PREF=VALUE ...]
Load the machine from the given path.
The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).
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.
%% Cell type:code id: tags:
``` prob
:help ::load
```
%% Output
```
::load [PREF=VALUE ...]
MACHINE
...
END
```
Load the machine source code given in the cell body.
There must be a newline between the `::load` command name and the machine code.
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.
::load [PREF=VALUE ...]
MACHINE
...
END
Load the machine source code given in the cell body.
There must be a newline between the `::load` command name and the machine code.
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.
%% Cell type:markdown id: tags:
When looking up help for a command, the `:` or `::` can be left off of the command name.
%% Cell type:code id: tags:
``` prob
:help help
```
%% Output
```
:help [COMMAND]
```
Display help for a specific command, or general help about the REPL.
:help [COMMAND]
Display help for a specific command, or general help about the REPL.
%% Cell type:code id: tags:
``` prob
:help load
```
%% Output
```
:load FILENAME [PREF=VALUE ...]
```
Load the machine from the given path.
The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).
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.
:load FILENAME [PREF=VALUE ...]
Load the machine from the given path.
The path is relative to the kernel's current directory (i. e. the directory in which the notebook is located).
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.
%% Cell type:markdown id: tags:
But it's not possible to use the wrong number of colons.
%% Cell type:code id: tags:
``` prob
:help ::help
```
%% Output
:help: Cannot display help for unknown command "::help"
%% Cell type:markdown id: tags:
Unknown commands cannot be looked up.
%% Cell type:code id: tags:
``` prob
:help wrong
```
%% Output
:help: Cannot display help for unknown command "wrong"
%% Cell type:code id: tags:
``` prob
:help :wrong
```
%% Output
:help: Cannot display help for unknown command ":wrong"
finalStringBuildersb=newStringBuilder("Type a valid B expression, or one of the following commands:\n");
finalStringBuildersbMarkdown=newStringBuilder("Type a valid B expression, or one of the following commands:\n\n");
finalStringBuildersb=newStringBuilder("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");
finalStringBuildersbMarkdown=newStringBuilder("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\n");
