{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Rush Hour Puzzle\n",
    "\n",
    "The [rush hour puzzle](https://en.wikipedia.org/wiki/Rush_Hour_(puzzle)) was invented in 1970 by Nob Yoshigahara. Even though the puzzle is one of the older puzzles, it is very interesting to model. \n",
    "In this notebook we are going to look at one encoding for the rush hour board game in which cars are packed on a 6-by-6 grid and can either move horizontally or vertically. The goal is to move the red car to the exit.\n",
    "In this particular instance we try to solve the [hardest puzzle of the original game Nr. 40](www.puzzles.com/products/RushHour/RHfromMarkRiedel/Jam.html?40).\n",
    "\n",
    "Inspired by discussions with Neng-Fa Zhou at ICLP'14 in Vienna, we now have a new version of the B model for this puzzle.\n",
    "\n",
    "The old version can still be found in the our [modelling examples](https://www3.hhu.de/stups/handbook/prob2/modelling_examples.html#rush-hour-puzzle)\n",
    "\n",
    "Let us take a look at the B model of the Rush Hour Puzzle. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: RushHour"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load\n",
    "MACHINE RushHour\n",
    "/* a more elegant encoding of the Rush Hour puzzle */\n",
    "/* Michael Leuschel, July 2014 */\n",
    "/* ProB finds solution in about 10.5 secs (turning invariant checking off) */\n",
    "/* This version has been slightly adapted for TLC by adding the c:1..red guards:\n",
    "    it finds a solution in 3 seconds\n",
    "   (most of this time is spent replaying the counter ; the model checking seems less than a\n",
    "    second) */\n",
    "SETS DIR = {h,v}\n",
    "CONSTANTS sze, dir, red, dim, free_initial\n",
    "PROPERTIES\n",
    " sze = [2,2,2,2,2,  2,2,2,2,  3,3,3,  2] & /* the sizes of the cars */\n",
    " dir = [v,v,v,v,v,  h,h,h,h,  v,v,h,  h] & /* indicating whether the cars move vertically or horizontally */\n",
    " red = size(sze) & /* the last car is the red one */\n",
    " dim = 5 & /* the grid goes from 0..dim */\n",
    " free_initial = {(0,3),(1,3), (0,5), (3,4),(4,0),(4,1),(5,5)}\n",
    "DEFINITIONS\n",
    "  GOAL == (col(red) = 4); /* The target : move red car to the right */\n",
    "  ANIMATION_STR_JUSTIFY_RIGHT == TRUE;\n",
    "  ANIMATION_FUNCTION_DEFAULT == (0..dim)*(0..dim)*{-1};\n",
    "  ANIMATION_FUNCTION ==\n",
    "    {r,c,i| i:1..red & dir(i)=h & row(i)=r & c:col(i)..col(i)+sze(i)-1} \\/\n",
    "    {r,c,i| i:1..red & dir(i)=v & col(i)=c & r:row(i)..row(i)+sze(i)-1}  \\/\n",
    "    free * {0}\n",
    "VARIABLES free, row, col\n",
    "INVARIANT\n",
    "  free <: (0..dim)*(0..dim) &                /* the currently free blocks */\n",
    "  card(free) = card(free_initial) &\n",
    "  row : 1..red --> 0..dim &                  /* the row of each car */\n",
    "  col : 1..red --> 0..dim                    /* the column for each car */\n",
    "INITIALISATION\n",
    " free :=  free_initial\n",
    " ||\n",
    "  col := [(1),(2),(2),(3),(4),                    /* vertical 2-size cars */\n",
    "          (0),(1),(3),(4),                        /* horiz. 2-size cars */\n",
    "          (0),(5),                                /* vertical 3-size cars */\n",
    "          (0),                                    /* horiz. 3-size cars */\n",
    "          (3)]                                    /* red car */\n",
    " ||\n",
    "  row := [(1),(1),(4),(3),(0),\n",
    "          (5),(0),(5),(4),\n",
    "          (0),(1),\n",
    "          (3),\n",
    "          (2)]                                    /* red car */\n",
    "OPERATIONS\n",
    "  mv_down(c,F) = PRE c:1..red & c |-> v : dir & F = row(c)+sze(c)|->col(c) &\n",
    "                F : free THEN\n",
    "            free := free - {F} \\/ {row(c)|->col(c)} ||\n",
    "            row(c) := row(c)+1\n",
    "    END;\n",
    "  mv_up(c,F) = PRE c:1..red & c |-> v : dir & F = row(c)-1|->col(c) &\n",
    "                  F : free THEN\n",
    "            free := free - {F} \\/ {row(c)+sze(c)-1|->col(c)} ||\n",
    "            row(c) := row(c)-1\n",
    "    END;\n",
    "  mv_right(c,F) = PRE c:1..red & c |-> h : dir & F = row(c)|->col(c)+sze(c) &\n",
    "                F : free THEN\n",
    "            free := free - {F} \\/ {row(c)|->col(c)} ||\n",
    "            col(c) := col(c)+1\n",
    "    END;\n",
    "  mv_left(c,F) = PRE c:1..red & c |-> h : dir & F = row(c)|->col(c)-1 &\n",
    "                  F : free THEN\n",
    "            free := free - {F} \\/ {row(c)|->col(c)+sze(c)-1} ||\n",
    "            col(c) := col(c)-1\n",
    "    END\n",
    "END"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Finding a Solution\n",
    "\n",
    "Since jupyter notebook does not "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":constants"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine initialised using operation 1: $initialise_machine()"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":init"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use `:load` to load an external machine file.\n",
       "\n",
       "You can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n",
       "\n",
       "## Evaluation\n",
       "\n",
       "* `:eval` - Evaluate a formula and display the result.\n",
       "* `:solve` - Solve a predicate with the specified solver.\n",
       "* `:table` - Display an expression as a table.\n",
       "* `:type` - Display the static type of a formula.\n",
       "* `:prettyprint` - Pretty-print a predicate.\n",
       "* `:let` - Evaluate an expression and store it in a local variable.\n",
       "* `:unlet` - Remove a local variable.\n",
       "* `:assert` - Ensure that the predicate is true, and show an error otherwise.\n",
       "\n",
       "## Animation\n",
       "\n",
       "* `::load` - Load a B machine from the given source code.\n",
       "* `:load` - Load a machine from a file.\n",
       "* `:constants` - Set up the current machine's constants.\n",
       "* `:init` - Initialise the current machine with the specified predicate\n",
       "* `:exec` - Execute an operation.\n",
       "* `:browse` - Show information about the current state.\n",
       "* `:trace` - Display all states and executed operations in the current trace.\n",
       "* `:goto` - Go to the state with the specified index in the current trace.\n",
       "* `:find` - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
       "\n",
       "## Visualisation\n",
       "\n",
       "* `:show` - Show the machine's animation function visualisation for the current state.\n",
       "* `:dot` - Execute and show a dot visualisation.\n",
       "\n",
       "## Verification\n",
       "\n",
       "* `:check` - Check the machine's properties, invariant, or assertions in the current state.\n",
       "* `:modelcheck` - Run the ProB model checker on the current model.\n",
       "\n",
       "## Other\n",
       "\n",
       "* `::render` - Render some content with the specified MIME type.\n",
       "* `:bsymb` - Load all bsymb.sty command definitions, so that they can be used in $\\LaTeX$ formulas in Markdown cells.\n",
       "* `:groovy` - Evaluate the given Groovy expression.\n",
       "* `:help` - Display help for a specific command, or general help about the REPL.\n",
       "* `:pref` - View or change the value of one or more preferences.\n",
       "* `:stats` - Show statistics about the state space.\n",
       "* `:time` - Execute the given command and measure how long it takes to execute.\n",
       "* `:version` - Display version info about the ProB 2 Jupyter kernel, ProB 2, and the underlying ProB CLI.\n"
      ],
      "text/plain": [
       "Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use :load to load an external machine file.\n",
       "You can also use any of the following commands. For more help on a particular command, run :help commandname.\n",
       "\n",
       "Evaluation:\n",
       ":eval - Evaluate a formula and display the result.\n",
       ":solve - Solve a predicate with the specified solver.\n",
       ":table - Display an expression as a table.\n",
       ":type - Display the static type of a formula.\n",
       ":prettyprint - Pretty-print a predicate.\n",
       ":let - Evaluate an expression and store it in a local variable.\n",
       ":unlet - Remove a local variable.\n",
       ":assert - Ensure that the predicate is true, and show an error otherwise.\n",
       "\n",
       "Animation:\n",
       "::load - Load a B machine from the given source code.\n",
       ":load - Load a machine from a file.\n",
       ":constants - Set up the current machine's constants.\n",
       ":init - Initialise the current machine with the specified predicate\n",
       ":exec - Execute an operation.\n",
       ":browse - Show information about the current state.\n",
       ":trace - Display all states and executed operations in the current trace.\n",
       ":goto - Go to the state with the specified index in the current trace.\n",
       ":find - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
       "\n",
       "Visualisation:\n",
       ":show - Show the machine's animation function visualisation for the current state.\n",
       ":dot - Execute and show a dot visualisation.\n",
       "\n",
       "Verification:\n",
       ":check - Check the machine's properties, invariant, or assertions in the current state.\n",
       ":modelcheck - Run the ProB model checker on the current model.\n",
       "\n",
       "Other:\n",
       "::render - Render some content with the specified MIME type.\n",
       ":bsymb - Load all bsymb.sty command definitions, so that they can be used in $\\LaTeX$ formulas in Markdown cells.\n",
       ":groovy - Evaluate the given Groovy expression.\n",
       ":help - Display help for a specific command, or general help about the REPL.\n",
       ":pref - View or change the value of one or more preferences.\n",
       ":stats - Show statistics about the state space.\n",
       ":time - Execute the given command and measure how long it takes to execute.\n",
       ":version - Display version info about the ProB 2 Jupyter kernel, ProB 2, and the underlying ProB CLI.\n"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":help"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "14.355 sec, 4782 of 4782 states processed, 29890 transitions"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "Model Checking complete. No error nodes found."
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":modelcheck"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "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": 4
}