diff --git a/notebooks/tests/trace.ipynb b/notebooks/tests/trace.ipynb new file mode 100644 index 0000000000000000000000000000000000000000..fe26a11fb91e23c0cb0918ae842845ec63d2a686 --- /dev/null +++ b/notebooks/tests/trace.ipynb @@ -0,0 +1,253 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "```\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." + ], + "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 +}