{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# ProB2 Jupyter Notebook Overview\n",
    "\n",
    "In this jupyter notebook, we will give you an extended overview of the functionalities that come with the ProB2 jupyter kernel.\n",
    "For this purpose, we will take a look at the simple machine `Lift.mch` taken from the [ProB Public Examples](https://www3.hhu.de/stups/downloads/prob/source/)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## The Help Command\n",
    "\n",
    "If you want to find out more about the commands and how to use them, type in `:help [COMMAND]`. The ProB2 Jupyter Notebook has an autocompletion function which also helps you to find what you need. Simply press `TAB` after the space after `:help`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":help [COMMAND]\n",
       "```\n",
       "\n",
       "Display help for a specific command, or general help about the REPL."
      ],
      "text/plain": [
       ":help [COMMAND]\n",
       "Display help for a specific command, or general help about the REPL."
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :help"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Loading a Machine\n",
    "\n",
    "To start of with the ProB Jupyter Kernel, we have to load a machine. This can be done by typing `::load` in a Code cell before the machine code and pressing `Shift+Enter`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       "::load [PREF=VALUE ...]\n",
       "MACHINE\n",
       "...\n",
       "END\n",
       "```\n",
       "\n",
       "Load the machine source code given in the cell body.\n",
       "\n",
       "There must be a newline between the `::load` command name and the machine code.\n",
       "\n",
       "Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
      ],
      "text/plain": [
       "::load [PREF=VALUE ...]\n",
       "MACHINE\n",
       "...\n",
       "END\n",
       "Load the machine source code given in the cell body.\n",
       "\n",
       "There must be a newline between the `::load` command name and the machine code.\n",
       "\n",
       "Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded."
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help ::load"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: Lift"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load DOT=/usr/bin/dot\n",
    "MODEL Lift\n",
    "DEFINITIONS SET_PREF_SHOW_EVENTB_ANY_VALUES==TRUE;\n",
    "  ASSERT_LTL == \"G( [push_call_button(groundf)] => F {cur_floor=groundf & door_open=TRUE})\";\n",
    "  Rconv == (topf-r+groundf);\n",
    "CONSTANTS groundf,topf\n",
    "PROPERTIES\n",
    "  topf : INTEGER & groundf : INTEGER & (groundf = -1) & (topf = 2) & (groundf < topf)\n",
    "VARIABLES call_buttons,cur_floor,direction_up,door_open\n",
    "INVARIANT\n",
    "       cur_floor : (groundf .. topf) & \n",
    "       door_open : BOOL & \n",
    "       call_buttons : POW(groundf .. topf) &\n",
    "       direction_up : BOOL &\n",
    "       (door_open = TRUE => cur_floor : call_buttons)\n",
    "INITIALISATION cur_floor := (groundf) || door_open := FALSE || call_buttons := ({}) || direction_up := TRUE\n",
    "OPERATIONS\n",
    " move_up = SELECT door_open = FALSE & cur_floor < topf & direction_up = TRUE &\n",
    "             # c.((c : INTEGER) & ((c : INTEGER) & (c > cur_floor) & (c : call_buttons))) &\n",
    "            (cur_floor /: call_buttons) THEN\n",
    "   cur_floor := ((cur_floor)+(1))\n",
    " END ;\n",
    " move_down = SELECT door_open = FALSE & cur_floor > groundf & (direction_up = FALSE) &\n",
    "       # cu.((cu : INTEGER) & ((cu : INTEGER) & (cu < cur_floor) & (cu : call_buttons))) &\n",
    "      (cur_floor /: call_buttons) THEN\n",
    "   cur_floor := ((cur_floor)-(1))\n",
    " END ;\n",
    " reverse_lift_up = SELECT direction_up = FALSE & door_open = FALSE &\n",
    "   # c.((c : INTEGER) & ((c : INTEGER) & (c > cur_floor) & (c : call_buttons))) & \n",
    "   ! l.((l : INTEGER) => (((l : INTEGER) & (l <= cur_floor) & (l >= groundf)) => (l /: call_buttons))) THEN\n",
    "   direction_up := TRUE\n",
    " END ;\n",
    " reverse_lift_down = SELECT direction_up = TRUE & door_open = FALSE & \n",
    "  # cd.(cd : INTEGER & ((cd : INTEGER) & (cd < cur_floor) & (cd : call_buttons))) & \n",
    "  ! u.(u : INTEGER => (((u : INTEGER) & (u >= cur_floor) & (u <= topf)) => (u /: call_buttons))) THEN\n",
    "  direction_up := FALSE\n",
    " END ;\n",
    " open_door = SELECT door_open = FALSE & (cur_floor : call_buttons) THEN\n",
    "    door_open := TRUE\n",
    " END ;\n",
    " close_door = SELECT door_open = TRUE THEN\n",
    "    door_open := FALSE || call_buttons := ((call_buttons)\\({cur_floor}))\n",
    " END ;\n",
    " push_call_button(floor) = SELECT (floor : (groundf .. topf)) & (floor /: call_buttons) THEN \n",
    "     call_buttons := ((call_buttons)\\/({floor}))\n",
    " END \n",
    "END"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Initialising a Machine\n",
    "\n",
    "Now we will set up constants and initialise the machine, to be able to interact with it. You can set up constants with the commant `:constants` and initialise with the command `:init`. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":constants [PREDICATE]\n",
       "```\n",
       "\n",
       "Set up the current machine's constants.\n",
       "\n",
       "This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`."
      ],
      "text/plain": [
       ":constants [PREDICATE]\n",
       "Set up the current machine's constants.\n",
       "\n",
       "This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`."
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :constants"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":constants"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":init [PREDICATE]\n",
       "```\n",
       "\n",
       "Initialise the current machine with the specified predicate\n",
       "\n",
       "This is a shorthand for `:exec INITIALISATION [PREDICATE]`."
      ],
      "text/plain": [
       ":init [PREDICATE]\n",
       "Initialise the current machine with the specified predicate\n",
       "\n",
       "This is a shorthand for `:exec INITIALISATION [PREDICATE]`."
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :init"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine initialised using operation 1: $initialise_machine()"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":init"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Trace and State\n",
    "\n",
    "After loading and initialising the machine, we can explore the state, visualise the machine and state and more. We will start by finding out in which trace we are currently in, to ensure, that we initialised the machine. This can be done with the command `:trace`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "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": [
       ":trace\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": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :trace"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "* -1: Root state\n",
       "* 0: `SETUP_CONSTANTS()`\n",
       "* 1: `INITIALISATION()` **(current)**"
      ],
      "text/plain": [
       "-1: Root state\n",
       "0: SETUP_CONSTANTS()\n",
       "1: INITIALISATION() (current)"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":trace"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Switching to a different trace is possible by typing in `:goto INDEX`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "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": [
       ":goto INDEX\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": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :goto"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Changed to state with index -1"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":goto -1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "* -1: Root state **(current)**\n",
       "* 0: `SETUP_CONSTANTS()`\n",
       "* 1: `INITIALISATION()`"
      ],
      "text/plain": [
       "-1: Root state (current)\n",
       "0: SETUP_CONSTANTS()\n",
       "1: INITIALISATION()"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":trace"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now that we set the current state to -1, we are at out root state again. We did not set up constants or initialise the machine, yet. From here, we have two possibilities to go back to the initialised state. Either by setting up constants and initialising again, or by simply typing `:goto 1`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Changed to state with index 1"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":goto 1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "* -1: Root state\n",
       "* 0: `SETUP_CONSTANTS()`\n",
       "* 1: `INITIALISATION()` **(current)**"
      ],
      "text/plain": [
       "-1: Root state\n",
       "0: SETUP_CONSTANTS()\n",
       "1: INITIALISATION() (current)"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":trace"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Another feature of ProB is, that you can find a state, for which a predicate is true. In the following we will try to use it:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":find PREDICATE\n",
       "```\n",
       "\n",
       "Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
       "\n",
       "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, 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."
      ],
      "text/plain": [
       ":find PREDICATE\n",
       "Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
       "\n",
       "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, 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."
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :find"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {
    "scrolled": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Found a matching state and made it current state"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":find cur_floor=0"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {
    "scrolled": false
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "* -1: Root state\n",
       "* 0: `find_valid_state` **(current)**"
      ],
      "text/plain": [
       "-1: Root state\n",
       "0: find_valid_state (current)"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":trace"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Note that the command leaves us with the root state and the current state, with a valid trace. That means, we lose our previous trace. \n",
    "\n",
    "For the next example we will have to recreate that trace again, with the following three commands:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Changed to state with index -1"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":goto -1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":constants"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine initialised using operation 1: $initialise_machine()"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":init"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Interacting with the Machine\n",
    "\n",
    "If you want to interact with the machine, meaning, that you want to know, which values the variables and constants have, you can simply type in the identifiers of those. e.g. type in `cur_floor` to find out on which floor we are currently at."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$-1$"
      ],
      "text/plain": [
       "−1"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "cur_floor"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If you want to get an overview over the whole machine state and which operations are currently possible, you can use `:browse`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":browse\n",
       "```\n",
       "\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."
      ],
      "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."
      ]
     },
     "execution_count": 23,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :browse"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine: Lift\n",
       "Sets: (none)\n",
       "Constants: groundf, topf\n",
       "Variables: call_buttons, cur_floor, direction_up, door_open\n",
       "Operations: \n",
       "push_call_button(-1)\n",
       "push_call_button(0)\n",
       "push_call_button(1)\n",
       "push_call_button(2)"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":browse"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To use operations, you have to use another command, that is slightly different. Type in the name of any operation, that is currently possible and put `:exec` before:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":exec OPERATION [PREDICATE]\n",
       "```\n",
       "\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."
      ],
      "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."
      ]
     },
     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :exec"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: push_call_button(-1)"
      ]
     },
     "execution_count": 26,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec push_call_button floor=-1"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we check our trace again and browse our actions, we can see, that the call button of the floor -1 is now pushed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "* -1: Root state\n",
       "* 0: `SETUP_CONSTANTS()`\n",
       "* 1: `INITIALISATION()`\n",
       "* 2: `push_call_button(-1)` **(current)**"
      ],
      "text/plain": [
       "-1: Root state\n",
       "0: SETUP_CONSTANTS()\n",
       "1: INITIALISATION()\n",
       "2: push_call_button(-1) (current)"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":trace"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine: Lift\n",
       "Sets: (none)\n",
       "Constants: groundf, topf\n",
       "Variables: call_buttons, cur_floor, direction_up, door_open\n",
       "Operations: \n",
       "open_door()\n",
       "push_call_button(0)\n",
       "push_call_button(1)\n",
       "push_call_button(2)"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":browse"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Of course, we could also type in `call_buttons` to find out, which call buttons are currently pushed."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{-1\\}$"
      ],
      "text/plain": [
       "{−1}"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "call_buttons"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The `:let` command lets you store the value of an expression under a different name. It is evaluated once on the current state. You can use the `:unlet` command if you are not using the local variable anymore."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":let NAME EXPR\n",
       "```\n",
       "\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",
       "\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."
      ],
      "text/plain": [
       ":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",
       "\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."
      ]
     },
     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :let"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{FALSE}$"
      ],
      "text/plain": [
       "FALSE"
      ]
     },
     "execution_count": 31,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":let first_floor_called 1:call_buttons"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: push_call_button(1)"
      ]
     },
     "execution_count": 32,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec push_call_button floor=1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{FALSE}$"
      ],
      "text/plain": [
       "FALSE"
      ]
     },
     "execution_count": 33,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "first_floor_called"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":unlet NAME\n",
       "```\n",
       "\n",
       "Remove a local variable."
      ],
      "text/plain": [
       ":unlet NAME\n",
       "Remove a local variable."
      ]
     },
     "execution_count": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :unlet"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "metadata": {},
   "outputs": [],
   "source": [
    ":unlet first_floor_called"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "metadata": {},
   "outputs": [
    {
     "ename": "CommandExecutionException",
     "evalue": ":eval: Computation not completed: Unknown identifier \"first_floor_called\"",
     "output_type": "error",
     "traceback": [
      "\u001b[1m\u001b[31m:eval: Computation not completed: Unknown identifier \"first_floor_called\"\u001b[0m"
     ]
    }
   ],
   "source": [
    "first_floor_called"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Additionally, you can use the `:table` command to display an expression as a table."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":table EXPRESSION\n",
       "```\n",
       "\n",
       "Display an expression as a table.\n",
       "\n",
       "Although any expression is accepted, this command is most useful for sets of tuples."
      ],
      "text/plain": [
       ":table EXPRESSION\n",
       "Display an expression as a table.\n",
       "\n",
       "Although any expression is accepted, this command is most useful for sets of tuples."
      ]
     },
     "execution_count": 37,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :table"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "|cur_floor|\n",
       "|---|\n",
       "|$-1$|\n"
      ],
      "text/plain": [
       "cur_floor\n",
       "-1\n"
      ]
     },
     "execution_count": 38,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":table cur_floor"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If you are not sure which type an formula has, you can use `:type` to find out."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":type FORMULA\n",
       "```\n",
       "\n",
       "Display the type of a formula.\n",
       "\n",
       "The returned types are *not* standard B types. They are human-readable, but cannot be used in code."
      ],
      "text/plain": [
       ":type FORMULA\n",
       "Display the type of a formula.\n",
       "\n",
       "The returned types are *not* standard B types. They are human-readable, but cannot be used in code."
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :type"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "INTEGER"
      ]
     },
     "execution_count": 40,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":type cur_floor"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "POW(INTEGER)"
      ]
     },
     "execution_count": 41,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":type call_buttons"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Evaluations\n",
    "\n",
    "If you just want to make sure, that a predicate is true, use the `:assert` command instead."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":assert PREDICATE\n",
       "```\n",
       "\n",
       "Ensure that the predicate is true, and show an error otherwise.\n",
       "\n",
       "This command is intended for verifying that a predicate is always true at a certain point in a notebook. Unlike normal evaluation (`:eval`), this command treats a $\\mathit{FALSE}$ result as an error. If the result is $\\mathit{TRUE}$, solutions for free variables (if any) are not displayed.\n",
       "\n",
       "Only predicates and $\\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error."
      ],
      "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",
       "\n",
       "Only predicates and $\\mathit{BOOL}$ expressions are accepted. Expressions of other types cause an error."
      ]
     },
     "execution_count": 42,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :assert"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "metadata": {},
   "outputs": [
    {
     "ename": "CommandExecutionException",
     "evalue": ":assert: Assertion is not true: FALSE",
     "output_type": "error",
     "traceback": [
      "\u001b[1m\u001b[31m:assert: Assertion is not true: FALSE\u001b[0m"
     ]
    }
   ],
   "source": [
    ":assert cur_floor=0"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$"
      ],
      "text/plain": [
       "TRUE"
      ]
     },
     "execution_count": 44,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":assert cur_floor=-1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine: Lift\n",
       "Sets: (none)\n",
       "Constants: groundf, topf\n",
       "Variables: call_buttons, cur_floor, direction_up, door_open\n",
       "Operations: \n",
       "open_door()\n",
       "push_call_button(0)\n",
       "push_call_button(2)"
      ]
     },
     "execution_count": 45,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":browse"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Another notable feature is the following command, with which you can pretty print predicates. Use `:prettyprint` to access it. \n",
    "\n",
    "You also have the option to solve predicates with different solvers. For this you can use the command `:solve`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    ":help :prettyprint"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 47,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\mathit{cur\\_floor} = - 1$"
      ],
      "text/plain": [
       "cur_floor = - 1"
      ]
     },
     "execution_count": 47,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":prettyprint cur_floor=-1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 48,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":solve SOLVER PREDICATE\n",
       "```\n",
       "\n",
       "Solve a predicate with the specified solver.\n",
       "\n",
       "The following solvers are currently available:\n",
       "\n",
       "* `cvc4`\n",
       "* `kodkod`\n",
       "* `prob`\n",
       "* `smt_supported_interpreter`\n",
       "* `z3`\n"
      ],
      "text/plain": [
       ":solve SOLVER PREDICATE\n",
       "Solve a predicate with the specified solver.\n",
       "\n",
       "The following solvers are currently available:\n",
       "\n",
       "* `cvc4`\n",
       "* `kodkod`\n",
       "* `prob`\n",
       "* `smt_supported_interpreter`\n",
       "* `z3`\n"
      ]
     },
     "execution_count": 48,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :solve"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Modifying the Preferences\n",
    "\n",
    "We have seen before, that you can set preferences when loading the machine with the `::load` command. You can modify or change the values of preferences by using the `:pref` command."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 49,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":pref [NAME ...]\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",
       "\n",
       "Certain preference changes do not take full effect when performed on a loaded machine. Such preferences must be assigned when the machine is loaded using the `::load` or `:load` command."
      ],
      "text/plain": [
       ":pref [NAME ...]\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",
       "\n",
       "Certain preference changes do not take full effect when performed on a loaded machine. Such preferences must be assigned when the machine is loaded using the `::load` or `:load` command."
      ]
     },
     "execution_count": 49,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :pref"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Additional Features\n",
    "\n",
    "In addition to the previous commands, you have the possibility to use the `:stats` command to show statistics about the state space. Moreover, you can use the `:time` command to measure the execution time of commands with their arguments. This can be helpful for measuring the solving time for specific machines."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 50,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":stats\n",
       "```\n",
       "\n",
       "Show statistics about the state space."
      ],
      "text/plain": [
       ":stats\n",
       "Show statistics about the state space."
      ]
     },
     "execution_count": 50,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :stats"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 51,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "**Explored States:** 4/15  \n",
       "**Transitions:** 14"
      ],
      "text/plain": [
       "Explored States: 4/15\n",
       "Transitions: 14"
      ]
     },
     "execution_count": 51,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":stats"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 52,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":time COMMAND [ARGS ...]\n",
       "```\n",
       "\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",
       "\n",
       "As with any measurement of execution time, there will likely be small differences between two measurements of the same command. The time is measured by the kernel rather than ProB, so it will include some overhead due to processing of the command by the kernel and communication with ProB."
      ],
      "text/plain": [
       ":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",
       "\n",
       "As with any measurement of execution time, there will likely be small differences between two measurements of the same command. The time is measured by the kernel rather than ProB, so it will include some overhead due to processing of the command by the kernel and communication with ProB."
      ]
     },
     "execution_count": 52,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :time"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 53,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "Execution time: 0.044099194 seconds"
      ],
      "text/plain": [
       "Execution time: 0.044099194 seconds"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/markdown": [
       "**Explored States:** 4/15  \n",
       "**Transitions:** 14"
      ],
      "text/plain": [
       "Explored States: 4/15\n",
       "Transitions: 14"
      ]
     },
     "execution_count": 53,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":time :stats"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To find out your current ProB CLI and ProB2 version, you can use `:version`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 54,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":version\n",
       "```\n",
       "\n",
       "Display version info about the ProB CLI and ProB 2."
      ],
      "text/plain": [
       ":version\n",
       "Display version info about the ProB CLI and ProB 2."
      ]
     },
     "execution_count": 54,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :version"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 55,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "ProB CLI: 1.9.0-nightly (ab12dcd41e1150b19e8c00897fe53f96f76cbd0d)\n",
       "ProB 2: 3.2.12-SNAPSHOT (06e75efe84ffdadf56df45e34acb44ec8e4603dd)"
      ]
     },
     "execution_count": 55,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":version"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Visualisations\n",
    "\n",
    "There are two possible ways of visualising the machine in jupyter notebook. One can be accessed via the `:dot` command. This command allows you to visualise a variety of different things, e.g. the state as graph. You can use autocomplete by clicking `TAB` after the command, as well."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 56,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":dot COMMAND [FORMULA]\n",
       "```\n",
       "\n",
       "Execute and show a dot visualisation.\n",
       "\n",
       "The following dot visualisation commands are available:\n",
       "\n",
       "* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model\n",
       "* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model (**Not available for this machine/state**: only available for Event-B models)\n",
       "* `state_space` - State Space: Show state space\n",
       "* `state_space_sfdp` - State Space (Fast): Show state space (fast)\n",
       "* `current_state` - Current State in State Space: Show current state and successors in state space\n",
       "* `signature_merge` - Signature Merge: Show signature-merged reduced state space\n",
       "* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)\n",
       "* `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram\n",
       "* `enable_graph` - Enable Graph: Show enabling graph of events\n",
       "* `state_as_graph` - Current State as Graph: Show values in current state as a graph\n",
       "* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES (**Not available for this machine/state**: only available when CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine)\n",
       "* `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph\n",
       "* `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree\n",
       "* `invariant` - Invariant Formula Tree: Show invariant as a formula tree\n",
       "* `properties` - Properties Formula Tree: Show properties as a formula tree\n",
       "* `assertions` - Assertions Formula Tree: Show assertions as a formula tree\n",
       "* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree\n",
       "* `goal` - Goal Formula Tree: Show GOAL as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models with a GOAL DEFINITION)\n",
       "* `dependence_graph` - Dependence Graph: Show dependence graph of events\n",
       "* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards\n",
       "* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n",
       "* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate\n",
       "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree (**Not available for this machine/state**: only available when error occured)\n"
      ],
      "text/plain": [
       ":dot COMMAND [FORMULA]\n",
       "Execute and show a dot visualisation.\n",
       "\n",
       "The following dot visualisation commands are available:\n",
       "\n",
       "* `machine_hierarchy` - Machine Hierarchy: Shows the machine hierarchy of a classical B model\n",
       "* `event_hierarchy` - Event Hierarchy: Shows the event hierarchy of an Event-B model (**Not available for this machine/state**: only available for Event-B models)\n",
       "* `state_space` - State Space: Show state space\n",
       "* `state_space_sfdp` - State Space (Fast): Show state space (fast)\n",
       "* `current_state` - Current State in State Space: Show current state and successors in state space\n",
       "* `signature_merge` - Signature Merge: Show signature-merged reduced state space\n",
       "* `dfa_merge` - DFA Merge: Show state space as deterministic automaton (DFA)\n",
       "* `transition_diagram` - State Space Expression Projection...: Project state space onto expression values and show transition diagram\n",
       "* `enable_graph` - Enable Graph: Show enabling graph of events\n",
       "* `state_as_graph` - Current State as Graph: Show values in current state as a graph\n",
       "* `custom_graph` - Customized Current State as Graph: Show values in current state as a graph using CUSTOM_GRAPH_EDGES (**Not available for this machine/state**: only available when CUSTOM_GRAPH_NODES and CUSTOM_GRAPH_EDGES are defined in the DEFINITIONS of a B machine)\n",
       "* `expr_as_graph` - (Relational) Expression as Graph...: Show (relational) expression value as a graph\n",
       "* `formula_tree` - Custom Predicate/Expression Formula Tree...: Show predicate/expressions and sub-formulas as a tree\n",
       "* `invariant` - Invariant Formula Tree: Show invariant as a formula tree\n",
       "* `properties` - Properties Formula Tree: Show properties as a formula tree\n",
       "* `assertions` - Assertions Formula Tree: Show assertions as a formula tree\n",
       "* `deadlock` - Deadlock Formula Tree: Show deadlocking status as a formula tree\n",
       "* `goal` - Goal Formula Tree: Show GOAL as a formula tree (**Not available for this machine/state**: only available for initialised B,Z or Event-B models with a GOAL DEFINITION)\n",
       "* `dependence_graph` - Dependence Graph: Show dependence graph of events\n",
       "* `variable_modification_graph` - Variable Read/Write Graph: Show variable modification by operations and reading in guards\n",
       "* `definitions` - Definitions Graph: Show dependence graph of DEFINITIONS\n",
       "* `predicate_dependency` - Predicate Dependency Graph...: Show dependence graph of conjuncts of a predicate\n",
       "* `last_error` - Last Error Formula Tree: Show last error source as a formula tree (**Not available for this machine/state**: only available when error occured)\n"
      ]
     },
     "execution_count": 56,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :dot"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 57,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.40.1 (20161225.0304)\n",
       " -->\n",
       "<!-- Title: state Pages: 1 -->\n",
       "<svg width=\"574pt\" height=\"131pt\"\n",
       " viewBox=\"0.00 0.00 573.70 131.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 127)\">\n",
       "<title>state</title>\n",
       "<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-127 569.6967,-127 569.6967,4 -4,4\"/>\n",
       "<!-- FALSE -->\n",
       "<g id=\"node1\" class=\"node\">\n",
       "<title>FALSE</title>\n",
       "<ellipse fill=\"#a52a2a\" stroke=\"#a52a2a\" cx=\"37.6967\" cy=\"-105\" rx=\"37.8943\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"37.6967\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">FALSE</text>\n",
       "</g>\n",
       "<!-- ROOT&#45;NODE -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>ROOT&#45;NODE</title>\n",
       "<polygon fill=\"#add8e6\" stroke=\"#add8e6\" points=\"292.6967,-36 205.5564,-18 292.6967,0 379.8369,-18 292.6967,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"292.6967\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">ROOT&#45;NODE</text>\n",
       "</g>\n",
       "<!-- FALSE&#45;&gt;ROOT&#45;NODE -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>FALSE&#45;&gt;ROOT&#45;NODE</title>\n",
       "<path fill=\"none\" stroke=\"#b22222\" d=\"M45.4313,-87.0482C51.2604,-75.7333 60.3678,-61.829 72.6967,-54 96.4841,-38.8946 164.3902,-29.3258 218.5285,-23.8823\"/>\n",
       "<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"219.1954,-27.334 228.8089,-22.8808 218.5167,-20.367 219.1954,-27.334\"/>\n",
       "<text text-anchor=\"middle\" x=\"101.6967\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">door_open</text>\n",
       "</g>\n",
       "<!-- TRUE -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>TRUE</title>\n",
       "<ellipse fill=\"#698b22\" stroke=\"#698b22\" cx=\"126.6967\" cy=\"-105\" rx=\"33.5952\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"126.6967\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">TRUE</text>\n",
       "</g>\n",
       "<!-- TRUE&#45;&gt;ROOT&#45;NODE -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>TRUE&#45;&gt;ROOT&#45;NODE</title>\n",
       "<path fill=\"none\" stroke=\"#a0522d\" d=\"M128.4128,-86.5614C130.3881,-75.6337 134.6244,-62.3348 143.6967,-54 156.5391,-42.2015 195.2856,-33.048 230.0463,-26.9236\"/>\n",
       "<polygon fill=\"#a0522d\" stroke=\"#a0522d\" points=\"230.9228,-30.3249 240.195,-25.1989 229.7499,-23.4239 230.9228,-30.3249\"/>\n",
       "<text text-anchor=\"middle\" x=\"178.1967\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">direction_up</text>\n",
       "</g>\n",
       "<!-- &#45;1 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>&#45;1</title>\n",
       "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"319.6967,-123 265.6967,-123 265.6967,-87 319.6967,-87 319.6967,-123\"/>\n",
       "<text text-anchor=\"middle\" x=\"292.6967\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">&#45;1</text>\n",
       "</g>\n",
       "<!-- &#45;1&#45;&gt;ROOT&#45;NODE -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>&#45;1&#45;&gt;ROOT&#45;NODE</title>\n",
       "<path fill=\"none\" stroke=\"#473c8b\" d=\"M265.574,-99.2206C249.2281,-94.1898 229.6958,-85.08 219.6967,-69 209.7592,-53.0192 225.7758,-40.7054 245.3118,-32.1844\"/>\n",
       "<polygon fill=\"#473c8b\" stroke=\"#473c8b\" points=\"246.7714,-35.3705 254.7693,-28.4218 244.1838,-28.8664 246.7714,-35.3705\"/>\n",
       "<text text-anchor=\"middle\" x=\"245.1967\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">cur_floor</text>\n",
       "</g>\n",
       "<!-- &#45;1&#45;&gt;ROOT&#45;NODE -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>&#45;1&#45;&gt;ROOT&#45;NODE</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M292.6967,-86.9735C292.6967,-75.1918 292.6967,-59.5607 292.6967,-46.1581\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"296.1968,-46.0033 292.6967,-36.0034 289.1968,-46.0034 296.1968,-46.0033\"/>\n",
       "<text text-anchor=\"middle\" x=\"326.1967\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">call_buttons</text>\n",
       "</g>\n",
       "<!-- &#45;1&#45;&gt;ROOT&#45;NODE -->\n",
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>&#45;1&#45;&gt;ROOT&#45;NODE</title>\n",
       "<path fill=\"none\" stroke=\"#bdef6b\" d=\"M319.7358,-98.1105C334.6112,-92.7883 351.8084,-83.7625 360.6967,-69 369.8361,-53.8203 355.4433,-41.6607 337.5823,-33.0275\"/>\n",
       "<polygon fill=\"#bdef6b\" stroke=\"#bdef6b\" points=\"338.5958,-29.6502 328.0322,-28.837 335.7831,-36.0602 338.5958,-29.6502\"/>\n",
       "<text text-anchor=\"middle\" x=\"384.1967\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">groundf</text>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>1</title>\n",
       "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"475.6967,-123 421.6967,-123 421.6967,-87 475.6967,-87 475.6967,-123\"/>\n",
       "<text text-anchor=\"middle\" x=\"448.6967\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;ROOT&#45;NODE -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>1&#45;&gt;ROOT&#45;NODE</title>\n",
       "<path fill=\"none\" stroke=\"#000000\" d=\"M438.6092,-86.6124C431.7628,-75.7039 421.7712,-62.4073 409.6967,-54 392.4638,-42.0011 371.1042,-33.9017 351.3706,-28.479\"/>\n",
       "<polygon fill=\"#000000\" stroke=\"#000000\" points=\"352.0918,-25.0507 341.5356,-25.9538 350.351,-31.8308 352.0918,-25.0507\"/>\n",
       "<text text-anchor=\"middle\" x=\"458.1967\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">call_buttons</text>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g id=\"node6\" class=\"node\">\n",
       "<title>2</title>\n",
       "<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"565.6967,-123 511.6967,-123 511.6967,-87 565.6967,-87 565.6967,-123\"/>\n",
       "<text text-anchor=\"middle\" x=\"538.6967\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;ROOT&#45;NODE -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>2&#45;&gt;ROOT&#45;NODE</title>\n",
       "<path fill=\"none\" stroke=\"#efdf84\" d=\"M528.0369,-86.8227C520.4593,-75.5637 509.2422,-61.808 495.6967,-54 473.2129,-41.0397 411.0663,-31.2111 361.4046,-25.1247\"/>\n",
       "<polygon fill=\"#efdf84\" stroke=\"#efdf84\" points=\"361.6802,-21.6328 351.3353,-23.9202 360.8488,-28.5832 361.6802,-21.6328\"/>\n",
       "<text text-anchor=\"middle\" x=\"524.6967\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">topf</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>"
      ],
      "text/plain": [
       "<Dot visualization: state_as_graph []>"
      ]
     },
     "execution_count": 57,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":dot state_as_graph"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Another option is to use the `ANIMATION_FUNCTION` with the command `:show`. Note, however, that to use this you have to write an `ANIMATION_FUNCTION` for your B model.\n",
    "\n",
    "The following B model contains such an `ANIMATION_FUNCTION` for the visualisation of Lift4. You can use what you have learned before to explore the visualisation."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 58,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: Lift0"
      ]
     },
     "execution_count": 58,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load\n",
    "MODEL Lift0\n",
    "DEFINITIONS SET_PREF_SHOW_EVENTB_ANY_VALUES==TRUE;\n",
    "  ASSERT_LTL == \"G( [push_call_button(groundf)] => F {cur_floor=groundf & door_open=TRUE})\";\n",
    "  Rconv == (topf-r+groundf);\n",
    "  ANIMATION_FUNCTION == ( {r,c,i|r:groundf..topf & ((c=2 & i=0) or (c=1 & i=2))} <+ \n",
    "                            ({r,c,i|r:groundf..topf & Rconv:call_buttons & c=2 & i=1} \\/\n",
    "                             {r,c,i|r:groundf..topf & Rconv=cur_floor & c=1 &\n",
    "                                    ((door_open=TRUE & i=3) or (door_open=FALSE & i=4))}\n",
    "                              ) \\/ {r,c,i| r=topf+1 & c=1 & \n",
    "                                       ((direction_up=TRUE & i=5) or (direction_up=FALSE & i=6)) } );\n",
    "      ANIMATION_IMG0 == \"images/CallButtonOff.gif\";\n",
    "      ANIMATION_IMG1 == \"images/CallButtonOn.gif\";\n",
    "      ANIMATION_IMG2 == \"images/LiftEmpty.gif\";\n",
    "      ANIMATION_IMG3 == \"images/LiftOpen.gif\";\n",
    "      ANIMATION_IMG4 == \"images/LiftClosed.gif\";\n",
    "      ANIMATION_IMG5 == \"images/up_arrow.gif\";\n",
    "      ANIMATION_IMG6 == \"images/down_arrow.gif\";\n",
    "      ANIMATION_RIGHT_CLICK(J,r) ==\n",
    "               IF J=2 THEN\n",
    "                push_call_button(topf-r+groundf)\n",
    "               ELSIF J=1 THEN\n",
    "                 CHOICE open_door OR close_door OR move_up OR move_down OR\n",
    "                        reverse_lift_up OR reverse_lift_down\n",
    "                 END\n",
    "               END;\n",
    "CONSTANTS groundf,topf\n",
    "PROPERTIES\n",
    "  topf : INTEGER & groundf : INTEGER & (groundf = -1) & (topf = 2) & (groundf < topf)\n",
    "VARIABLES call_buttons,cur_floor,direction_up,door_open\n",
    "INVARIANT\n",
    "       cur_floor : (groundf .. topf) & \n",
    "       door_open : BOOL & \n",
    "       call_buttons : POW(groundf .. topf) &\n",
    "       direction_up : BOOL &\n",
    "       (door_open = TRUE => cur_floor : call_buttons)\n",
    "INITIALISATION cur_floor := (groundf) || door_open := FALSE || call_buttons := ({}) || direction_up := TRUE\n",
    "OPERATIONS\n",
    " move_up = SELECT door_open = FALSE & cur_floor < topf & direction_up = TRUE &\n",
    "             # c.((c : INTEGER) & ((c : INTEGER) & (c > cur_floor) & (c : call_buttons))) &\n",
    "            (cur_floor /: call_buttons) THEN\n",
    "   cur_floor := ((cur_floor)+(1))\n",
    " END ;\n",
    " move_down = SELECT door_open = FALSE & cur_floor > groundf & (direction_up = FALSE) &\n",
    "       # cu.((cu : INTEGER) & ((cu : INTEGER) & (cu < cur_floor) & (cu : call_buttons))) &\n",
    "      (cur_floor /: call_buttons) THEN\n",
    "   cur_floor := ((cur_floor)-(1))\n",
    " END ;\n",
    " reverse_lift_up = SELECT direction_up = FALSE & door_open = FALSE &\n",
    "   # c.((c : INTEGER) & ((c : INTEGER) & (c > cur_floor) & (c : call_buttons))) & \n",
    "   ! l.((l : INTEGER) => (((l : INTEGER) & (l <= cur_floor) & (l >= groundf)) => (l /: call_buttons))) THEN\n",
    "   direction_up := TRUE\n",
    " END ;\n",
    " reverse_lift_down = SELECT direction_up = TRUE & door_open = FALSE & \n",
    "  # cd.(cd : INTEGER & ((cd : INTEGER) & (cd < cur_floor) & (cd : call_buttons))) & \n",
    "  ! u.(u : INTEGER => (((u : INTEGER) & (u >= cur_floor) & (u <= topf)) => (u /: call_buttons))) THEN\n",
    "  direction_up := FALSE\n",
    " END ;\n",
    " open_door = SELECT door_open = FALSE & (cur_floor : call_buttons) THEN\n",
    "    door_open := TRUE\n",
    " END ;\n",
    " close_door = SELECT door_open = TRUE THEN\n",
    "    door_open := FALSE || call_buttons := ((call_buttons)\\({cur_floor}))\n",
    " END ;\n",
    " push_call_button(floor) = SELECT (floor : (groundf .. topf)) & (floor /: call_buttons) THEN \n",
    "     call_buttons := ((call_buttons)\\/({floor}))\n",
    " END \n",
    "END"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 59,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "```\n",
       ":show\n",
       "```\n",
       "\n",
       "Show the machine's animation function visualisation for the current state.\n",
       "\n",
       "The visualisation is static, any defined right-click options cannot be viewed or used."
      ],
      "text/plain": [
       ":show\n",
       "Show the machine's animation function visualisation for the current state.\n",
       "\n",
       "The visualisation is static, any defined right-click options cannot be viewed or used."
      ]
     },
     "execution_count": 59,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help :show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 60,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
     "execution_count": 60,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":constants"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 61,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine initialised using operation 1: $initialise_machine()"
      ]
     },
     "execution_count": 61,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":init"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 62,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "<table style=\"font-family:monospace\"><tbody>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/LiftClosed.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/up_arrow.gif\"/></td>\n",
       "<td style=\"padding:0px\"></td>\n",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 62,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 63,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine: Lift0\n",
       "Sets: (none)\n",
       "Constants: groundf, topf\n",
       "Variables: call_buttons, cur_floor, direction_up, door_open\n",
       "Operations: \n",
       "push_call_button(-1)\n",
       "push_call_button(0)\n",
       "push_call_button(1)\n",
       "push_call_button(2)"
      ]
     },
     "execution_count": 63,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":browse"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 64,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: push_call_button(-1)"
      ]
     },
     "execution_count": 64,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec push_call_button floor=-1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 65,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "<table style=\"font-family:monospace\"><tbody>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/LiftClosed.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/CallButtonOn.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/up_arrow.gif\"/></td>\n",
       "<td style=\"padding:0px\"></td>\n",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 65,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 66,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: open_door()"
      ]
     },
     "execution_count": 66,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec open_door"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 67,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "<table style=\"font-family:monospace\"><tbody>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"3\" src=\"images/LiftOpen.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/CallButtonOn.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/up_arrow.gif\"/></td>\n",
       "<td style=\"padding:0px\"></td>\n",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 67,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 68,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: close_door()"
      ]
     },
     "execution_count": 68,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec close_door"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 69,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "<table style=\"font-family:monospace\"><tbody>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/LiftClosed.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/up_arrow.gif\"/></td>\n",
       "<td style=\"padding:0px\"></td>\n",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 69,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 70,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine: Lift0\n",
       "Sets: (none)\n",
       "Constants: groundf, topf\n",
       "Variables: call_buttons, cur_floor, direction_up, door_open\n",
       "Operations: \n",
       "push_call_button(-1)\n",
       "push_call_button(0)\n",
       "push_call_button(1)\n",
       "push_call_button(2)"
      ]
     },
     "execution_count": 70,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":browse"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 71,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: push_call_button(1)"
      ]
     },
     "execution_count": 71,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec push_call_button floor=1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 72,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "<table style=\"font-family:monospace\"><tbody>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/CallButtonOn.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/LiftClosed.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/up_arrow.gif\"/></td>\n",
       "<td style=\"padding:0px\"></td>\n",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 72,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 73,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: move_up()"
      ]
     },
     "execution_count": 73,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":exec move_up"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 74,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "<table style=\"font-family:monospace\"><tbody>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"1\" src=\"images/CallButtonOn.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"4\" src=\"images/LiftClosed.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"2\" src=\"images/LiftEmpty.gif\"/></td>\n",
       "<td style=\"padding:0px\"><img alt=\"0\" src=\"images/CallButtonOff.gif\"/></td>\n",
       "</tr>\n",
       "<tr>\n",
       "<td style=\"padding:0px\"><img alt=\"5\" src=\"images/up_arrow.gif\"/></td>\n",
       "<td style=\"padding:0px\"></td>\n",
       "</tr>\n",
       "</tbody></table>"
      ],
      "text/plain": [
       "<Animation function visualisation>"
      ]
     },
     "execution_count": 74,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":show"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This concludes the overview over the ProB jupyter notebook kernel."
   ]
  }
 ],
 "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
}