"Display all states and transitions 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."
],
"text/plain": [
"```\n",
":trace\n",
"```\n",
"\n",
"Display all states and transitions 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."
]
},
"execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":help :trace"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"```\n",
":goto INDEX\n",
"```\n",
"\n",
"Go to the state with the specified index in the current trace.\n",
"\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)."
],
"text/plain": [
"```\n",
":goto INDEX\n",
"```\n",
"\n",
"Go to the state with the specified index in the current trace.\n",
"\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)."
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":help :goto"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"* -1: Root state **(current)**"
],
"text/plain": [
"-1: Root state (current)"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":trace"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Machine initialised using operation 0: $initialise_machine()"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":init"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"* -1: Root state\n",
"* 0: $initialise_machine **(current)**"
],
"text/plain": [
"-1: Root state\n",
"0: $initialise_machine (current)"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":trace"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"Changed to state with index -1"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":goto -1"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"text/markdown": [
"* -1: Root state **(current)**\n",
"* 0: $initialise_machine"
],
"text/plain": [
"-1: Root state (current)\n",
"0: $initialise_machine"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
":trace"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Indices out of bounds are not accepted."
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"ename": "CommandExecutionException",
"evalue": ":goto: Invalid trace index -2, must be in -1..0",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[31m:goto: Invalid trace index -2, must be in -1..0\u001b[0m"
]
}
],
"source": [
":goto -2"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"ename": "CommandExecutionException",
"evalue": ":goto: Invalid trace index 1, must be in -1..0",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[31m:goto: Invalid trace index 1, must be in -1..0\u001b[0m"
]
}
],
"source": [
":goto 1"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "ProB 2",
"language": "prob",
"name": "prob2"
},
"language_info": {
"codemirror_mode": "prob2_jupyter_repl",
"file_extension": ".prob",
"mimetype": "text/x-prob2-jupyter-repl",
"name": "prob"
}
},
"nbformat": 4,
"nbformat_minor": 2
}
%% Cell type:code id: tags:
``` prob
:help :trace
```
%% Output
```
:trace
```
Display all states and transitions in the current trace.
Each state has an index, which can be passed to the `:goto` command to go to that state.
The first state (index -1) is always the root state. All other states are reached from the root state by following (previously executed) transitions.
```
:trace
```
Display all states and transitions in the current trace.
Each state has an index, which can be passed to the `:goto` command to go to that state.
The first state (index -1) is always the root state. All other states are reached from the root state by following (previously executed) transitions.
%% Cell type:code id: tags:
``` prob
:help :goto
```
%% Output
```
:goto INDEX
```
Go to the state with the specified index in the current trace.
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.
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).
```
:goto INDEX
```
Go to the state with the specified index in the current trace.
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.
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).
%% Cell type:code id: tags:
``` prob
:trace
```
%% Output
* -1: Root state **(current)**
-1: Root state (current)
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 0: $initialise_machine()