multiagent_scaling.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "3b359025",
   "metadata": {},
   "source": [
    "# Trajectory planning for multi-agent systems"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5cf987f5",
   "metadata": {},
   "source": [
    "This notebook contains a scalable version of the multi-agent navigation case study with a simplified layout.\n",
    "\n",
    "This case study uses _merging_ of _PolyhedralContractCompounds_ and model checking by calling _contains_behavior_ for each possible next position.\n",
    "\n",
    "Some info on the number of operations:\n",
    "\n",
    "This happens once at the start:\n",
    "\n",
    "1. Swapping contract and collision contract -> merged\n",
    "\n",
    "This happens for each timestep:\n",
    "\n",
    "2. Each robot has a dynamics contract, they are merged by adding one at a time\n",
    "3. The resuting dynamics contract is merged again with the contract from 1.\n",
    "4. Then each possible next position (combination of all robots' positions) is checked using the contains_behavior function (I expect this to be the cause for the long run time as the number of possible next positions explodes when adding another robot - I would suggest sticking with 1 or 2 robots and increasing the length of the corridor $l_{corridor}$)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "eb50b037",
   "metadata": {},
   "outputs": [],
   "source": [
    "%matplotlib inline\n",
    "import numpy as np\n",
    "from utils.multiagent_utils import (\n",
    "    Coord,\n",
    "    Robot,\n",
    "    distance,\n",
    "    get_collision_contract,\n",
    "    get_swapping_contract,\n",
    "    strategy_multiple_simple,\n",
    "    find_move_candidates_general\n",
    ")\n",
    "from utils.plotting_utils import plot_grid_world\n",
    "\n",
    "from pacti.iocontract import Var\n",
    "from pacti.contracts import PolyhedralIoContractCompound"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5b4d753e",
   "metadata": {},
   "source": [
    "### Create gridworld and robots"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "104e7504",
   "metadata": {},
   "source": [
    "We will set up the grid world such that all robots start in the same lane as their respective goal such that the grid world is set up as a corridor, with the scaling parameters the number of robots $n_{robots}$ and the corridor length $l_{corridor}$.\n",
    "\n",
    "To visualize the setup:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "e93e21a9",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAPEAAAGbCAYAAAAV03aBAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjcuMSwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/bCgiHAAAACXBIWXMAAA9hAAAPYQGoP6dpAAAw7ElEQVR4nO3deXQfV33//+d85rNLH+2LJdmS7Xi3kzirEyckJjiQyDhJf9B+gUAdoKHJj5aW/g4cyq/f7yGn362055sW0gAtNPBNS3/ltCy/GgolCSnYDrEtZ3csx6tsa7f25bPN3O8f11K8yLEszXw013o/ztHR8pFmRp+5r5k7d+69YymlFEIIY4XmegOEELMjIRbCcBJiIQwnIRbCcBJiIQwnIRbCcBJiIQwnIRbCcBJiIQwnIQ6Ihx56iMWLF1/y944dO4ZlWXz729/2fZtma9OmTWzatOmSv/f8889jWRbPP/+879t0JZIQz9LRo0f5vd/7PVasWEEymSSZTLJmzRo+/elP8+qrr87JNu3evRvLsnj88ccveO3+++/HsiyeeuqpC1674447aGhoKMQmCg9JiGdh+/btrFu3jqeffprNmzfz+OOP81d/9Vfce++9/OQnP2H9+vUcP358Wsv627/9W1pbWz3Zruuvv55kMsmOHTsueG3Xrl2Ew2F27tx5zs+z2Sx79uzhtttu82QbROGE53oDTHX48GE+9KEP0dTUxLPPPktdXd05r//Zn/0ZTz75JKHQOx8nR0dHKSoqIhKJeLZt4XCYDRs2XBDU1tZWent7+chHPnJBwFtaWkin09x+++2zXv/Y2BjJZHLWyxHTI2fiGfryl7/M6OgoTz311AUBBh2kz3zmMyxatGjyZw899BDFxcUcPnyY5uZmUqkUDz744ORr518TDwwM8NBDD1FaWkpZWRnbtm1jYGBgWtt3++2309XVxaFDhyZ/tnPnTkpKSvjUpz41GeizX5v4uwlPPvkka9euJRaLUV9fz6c//ekL1r9p0ybWrVtHS0sLd9xxB8lkki9+8YsX3a6TJ0/ywAMPUFRURE1NDZ/97GfJZDLT+p/E1ORMPEPbt29n2bJlbNiw4bL+Lp/P8773vY/bb7+dv/iLv7joGUspxf3338+OHTt45JFHWL16NT/4wQ/Ytm3btNYzEcYdO3awbNkyQAf1lltuYcOGDUQiEXbt2sV99903+VoqleLaa68F4Etf+hKPPfYYmzdv5tFHH6W1tZWvfe1r7Nmzh507d55Tczh9+jT33nsvH/rQh/joRz9KbW3tlNs0Pj7Oe97zHtra2vjMZz5DfX09Tz/9NM8999z03jwxNSUu2+DgoALUAw88cMFr/f39qqenZ/JjbGxs8rVt27YpQH3hC1+44O+2bdummpqaJr//4Q9/qAD15S9/efJn+Xxevetd71KAeuqpp95xG4eGhpRt2+qTn/zk5M9WrlypHnvsMaWUUjfffLP63Oc+N/ladXW1uvvuu5VSSnV3d6toNKre+973KsdxJn/niSeeUID6u7/7u8mf3XnnnQpQX//61y/YhjvvvFPdeeedk9//5V/+pQLU9773vcmfjY6OqmXLlilA/eIXv3jH/0lMTarTMzA0NARAcXHxBa9t2rSJ6urqyY+//uu/vuB3Hn300Uuu4yc/+QnhcPic37Vtm9///d+f1jamUimuueaayWvf3t5eWltb2bhxIwC33XbbZBX64MGD9PT0TJ69n3nmGbLZLH/4h394zjX9ww8/TElJCT/+8Y/PWVcsFuPjH//4tP6nuro6PvjBD07+LJlM8qlPfWpa/5OYmoR4BlKpFAAjIyMXvPaNb3yDn//85/z93//9lH8bDodZuHDhJddx/Phx6urqLjhQrFy5ctrbefvtt09e++7atQvbtrnlllsA2LhxIy0tLWQymQuuhyda1M9fVzQaZenSpRe0uDc0NBCNRqf1Py1btgzLsmb8P4kLSYhnoLS0lLq6Ol5//fULXtuwYQObN2++6K2aWCx2yRZrr0yEcufOnezcuZOrr7568qCwceNGMpkMe/bsYceOHYTD4cmAX65EIuHZNovLJyGeoS1btnDo0CF2797ty/Kbmpro6Oi44Gx/OfeSz27c2rlz5zkHlvr6epqamiYDft111002sjU1NU25rmw2y9GjRydfn8n/dPjwYdR507p5dX98vpIQz9DnP/95kskkn/jEJ+jq6rrg9fML6uVqbm4mn8/zta99bfJnjuPw1a9+ddrLqK+vZ8mSJTz77LPs3bt38np4wsaNG/nhD39Ia2vrObeWNm/eTDQa5Stf+co5/8e3vvUtBgcH2bJly4z/p/b2dv75n/958mdjY2P8zd/8zYyWJzS5xTRDy5cv57vf/S4f/vCHWblyJQ8++CDXXnstSimOHj3Kd7/7XUKh0LSuf6eydetWbrvtNr7whS9w7Ngx1qxZw/e//30GBwcvazm33347Tz/9NMAFVfyNGzfyj//4j5O/N6G6upo//uM/5rHHHuOee+7hvvvuo7W1lSeffJKbbrqJj370ozP6nx5++GGeeOIJfvu3f5uWlhbq6up4+umnpWPIbM1t47j5Dh06pB599FG1bNkyFY/HVSKRUKtWrVKPPPKIevnll8/53W3btqmioqIpl3P+LSallDp9+rT62Mc+pkpKSlRpaan62Mc+pl566aVp3WKa8I1vfEMBqqGh4YLX9u3bpwAFqK6urgtef+KJJ9SqVatUJBJRtbW16tFHH1X9/f3n/M6dd96p1q5dO+W6z7/FpJRSx48fV/fdd59KJpOqqqpK/cEf/IH66U9/KreYZsFSSuadFsJkck0shOEkxEIYTkIshOEkxEIYTkIshOGmdZ/YdV3a29tJpVIX9HsVQvhDKcXw8DD19fXv2FV3WiFub28/Z3C7EKJwTpw48Y6dhqYV4olROydOnKCkpMSbLRNCvKOhoSEWLVo0mb+LmVaIJ6rQJSUlEmIhCuxSl7DSsCWE4STEQhhOQiyE4STEQhhOQiyE4STEQhhOQiyE4STEQhhOQiyE4STEQhhOQiyE4STEQhjO03mns9ksoB/8Nd85jgPIewHyXpxv4v2YzvOrpsOzEGezWf70T/8UVJ4bbrwOu0DPGwoix3Vp2bsPsLjhxg3zuvA6jkNLS4uUizPOLhv/+b885kmQvX0ChMqD2wPOSZjPT011XXB7z3yTB+ZviAEpF2c7u2yoLBCgENu2zQ03rAfnFM33bJz3Zx/OTMnffO9m7PA7D+q+kun3IiPl4oyzy4Zte/PcBk/PxHoHhbBte97vLNsOnfks74WUi3NNlA2vzPO6jRDmkxALYTgJsRCGkxALYTgJsRCGkxALYTgJsRCGkxALYTgJsRCGkxALYTgJsRCGkxALYTgJsRCGkxALYTgJsRCGkxALYThvp+eZQ0pBb2+Yzs4wubxFyIKyMoeGhiyRyFxvnZhLuRwMDdlksxYA4TCUlDjEYt7MrDHXjA6x68JrryV4/pfFvPxKgp7eMGOjNq4CC4jFXEpKXFauSPOu20fYeOsoxcXuXG+2KIDR0RDHjkU51halpzvM6FiIfN5CKQjbimTSpaIyT1NjjiWLs5SVOXO9yTNmZIiVgt17kvz9dyt480Cc8XGLkhKX4iKHqso8tq1wXYtMxmJ4xOaXO4r5j18VU1+X476tg/xfDwwQj18ZR2FxrrExi5dfSXDgQJy+/jCxmNLloipPJKywLMjnLUbHQrS3Rzl4ME5ZmcOyqzJcf924kWE2LsTDwyG+/b8r2P7jUtLpEA0NWVKpqc6uimhUkUq51NflyOWgozPK175exe49SR55uJdVqzIF337hn2PHorzwYpITJ6JUV+VZvizDVDPkhsOKeNyhssJBKRgYtGnZp/9uw82jrFgx9d8FlVEh7u21+e//cwG/3l1E3YIcixdnp/23kQg0LsqSTlvsbUny/56s53N/1MUtG8Z83GJRCErBa6/H+dWOYlzXYsXyDNOdj8+yoLzMobTEobMzwk//vYS+/lE23Dw27WXMNWOONwMDNv/tTICXL0tTVZWf0XLiccWa1Wn6+2z+558vYG9L0uMtFYX2xv44zz+fIhFXLG7Kzih8oRDU1+eoqszzwq+LeXF3EteQ5hMjQqwUfPOpSl48E+DZXs9aFixblqG/3+avvlpNb68hh1xxgY6OMDt3FpEscqmuntmB/WylpS61NTl27y3i8OGYB1voPyNCvGNnET/9WQkN9VnPGqQsC5ZdlebwkRjfeqoKJe1cxslmLV54sYjRsRC1NbMP8ITSUpdYRPHi7iRDQ8GPSOC3MJu1+Pb/rsRxoKLC25bDcBgWLczyzHMpXn454emyhf/eeivGkSNRFjdNv21kuurrc7R3RHjt9bjny/Za4EO8tyXJkSMxGhd5v6NAdwgZHw/xzHPz91ErJnIcfS1clFS+dOYJhaC6Kk9ra5zR0WDHJNhbB/z8mRR5B1/v61ZX5fjVzmK6u41qrJ/XTp2K0N4R8eQ6+GIqKhxO94U5ftybR5D6JdAhzmQsXns9QUW5fzsKoLIyz0C/zcG3zGjIEHD6dJh83vK162QoBJGIoqMz2Af3QIf4xIkoQ8Mh37tK2ja4isAfccXbOrvCBen7XFTk0tkVCfTtpkCHuL0jwthYiGTS/3fQtuF4m4TYBBODXZIJ/8tFMukyMhJibCy4UQnulqFbpi0oSBc421aBb8AQmuOA41iePd/3ndghPdAmn7d8X9dMBbrUWhYoCvTmKe8e+iz8ZVlQqGIxsT7LCm7ZCHSIS0ocbFuRy/m/rlzeoqLSvBEs85FtQyLuksn6n+Rs1iISJtBjjwMd4sZFWVLFLiMj/naLVAqUsljiQ6cB4Y+6+lxBrlNHx0KUl+cDPXQ10CGuqclTWZlnaNjfEKfTFtGoS1OjhNgUleXO5CB/P42OhqirK0BVcBYCHWLLgjveNczwsO3rzurqitC4KMvq1Wn/ViI8VVeXoyTl+Nq3OZOxCIcVDfUS4lm5a9MIpaUOfX3+nI1dF0ZGbd733uFAX/eIc1VUOCy9Kkt3j38dMbq6wzQ05GhokBDPyuLFWTbeOkJ7R9SXG+5tbVEa6nPctWnY+4ULX61emSYWVQwMeH+AHx/X0ztdvXY88JMDBD7ElgWffOg0jYuyHDvmbWeM4eEQmWyIh377NLW1/nbtFN5buDDH+vVjdHSGyXu4+5SCthNR1qxOs3x58KdwCnyIAerq8nziodMoZdHpUT/WdNri2PEYm+4Y5n3vHfJkmaLwrr9unKVLsxw+EsPx4A6hUnqururqPDffZMYUPUaEGODuzcM8tO00wyNhTp2KzKqha2Q0xFuH4my8dZQ/+sNuI3aUmFoiobhr0zANDVkOHY7Nqk+B48DRYxGKUw6b7xr2fPy6X4wJsWXBgx/u59Hf7UFh8eaBOOn05d3sd11dTTpxIspd7x7mP3+xg5KSAPdsF9NSUeHwvruHWbI4w6HDsRk1gg4Phzj4VoyqKr2soDdmnS3YY6zOY1nwmx8YYPXKNF//2ypeeTVBJKyoq89RXHTxMOZy+jbSwECY2tocn/pkL1vfP0jYqP9evJOKCof3bxni5VcS7HspQc/BGFWVecrLnYv2vVcKBgdtenptwjbcfNMoN94wbtwDBowsxuvWpfny/zjFc79I8W8/K6G1Nc7xjIVl6VEntq1QyiKdtsjlQoRCivq6HL/xwGned/cQixaZc5QV0xeLKTbcPEZTY5a3Dsc42BrnrcMxUBCPKSIRfQ2Wd2B8PIRlKYqLXa6+Os3K5WkWLcrpftmGMTLEAMmk4v1bhrj3niHeeCPBocMxDh+JcuRobPImfU11npUrMjQ1Zblu/dhFJpkXV5oFC/IsWJDnumvH6eoKMzBo09Wth7Wi9ON9amvzlJU6VFfrs7XJjA3xBNuGa64Z55prxud6U0TAFBe7FBdPdKW9csuHMQ1bQoipSYiFMJyEWAjDSYiFMJyEWAjDSYiFMJyEWAjDSYiFMJyEWAjDSYiFMJyEWAjDSYiFMJyEWAjDSYiFMJyEWAjDSYiFMJynkwI4jgOOqz/PY47j4Dju5NdY8/f90O+FlIsJZ5cNr3gWYsdxaGl5CdxesMAuxJPBA8pxXVr27dff2Nux7fjcbtAcclyXlr17QA3M+3IB55aN5q0OtgcJ9Hh6HgNnGfOb2828vmpxXR1gMQVv4udZiG3b5oYbN4DK0dx8N/Y8npFdV6G3g9tN8z0b5b04M9F/85aPYIeL5naD5pjjOBD6GRDCDic8WaanZ2JdWG3scGpeF1wsBzscByeEbdvz+70AbFvXROxwEXY4NcdbM8csBzuc9HSR87ieJ8SVQUIshOEkxEIYTkIshOEkxEIYTkIshOEkxEIYTkIshOEkxEIYTkIshOEkxEIYTkIshOEkxEIYTkIshOEkxEIYTkIshOE8np5njikFw8OQzYJtQ3ExRCJzvVUiCPJ5yOV0GYlErqhyYX6IT5+GXbvgwAHYv19/77pgWZBIwIoVsHIl3HST/mzJPGDzgutCezt0dkJXF/T06CCDPsCXl0N9PVRXw8KFRofa3BCfPAnf/z48/zx0d+twFhdDMql3klIwPg47d8IvfgH/8A9wzTXwwANw660S5iuV48ChQ/DGG7qMZLP6YJ5MQvzMrKP5vA74oUO6rCxYAGvXwqpVEI3O7fbPgHkhdhz46U/hO9+BEyf0kXTVKr0zLkYpGByEF1+Effvg3nvh4x+HiorCbbfwX18f7N6ta2SxmA5n4iKT0VVW6s/ZrD5L/+xnOtS33gp1dYXbZg+YFeJMBr7yFfjxj/VOWrcOpjOPsWVBWZn+6OuDf/kXePNN+JM/gcWLfd5oURBtbbrG1dMDjY0XD+/5olFoaNDXy8eP67+/4w5Yvdrf7fWQOa3TuRw8/jj86EdQW6vDN5OJyCsq9A46cAC+9CW944TZ2trg3/8dhoZ0G8h0A3y2SASWLdNl6tln9dncEOaE+J/+SZ+BFy3SZ9TZCId1I9dbb8Gf/zmMjXmyiWIODAzoM/D4uD6wz7atY8ECXcv75S/h1CkvttB3ZoT4zTd1iMvKoKTEm2WGw/rI+9JLetnCPK6rr4G7u6GpybvlLlgA6TS88IK+hAu44IfYdeGb34T+fu8bHOJxqKrS18iHD3u7bOG/I0d0K3Rjo/d3Gxob4ehRI6rVwQ/x66/Dq6/6s6NAX1/39enrIGEOpXTAbFvfPvJaJAKlpfogkc16v3wPBT/Ezz2nr3dSPj3+w7J0Y9czz+iGEWGGri59i7Gmxr91VFXpqnpbm3/r8ECwQ5zPw69/PfuGrEuprtY768ABf9cjvNPdrRski3x8QNtEL672dv/W4YFgh7i9XXfS8OssPCEa1QcMud1kju7uwvSuKiqCjg5dfQ+oYIf45EkYHfX3aDshFIJjx/xfj5g9pXSI/bgWPl9Rkb7MCvBtyGCHeHxc77BCPBo0HNZnfRF8rqsbmwoxaCEc1rW0icETARTsEAshLinYIU4kdOux4/i/rnxe31IQwRcK6evhXM7/deXz+mwcDu4wg2CHeOFCfU0yOur/ulxXBkOYwrL0raVCXKeOjupegoW4/p6hYIe4vl6fHYeH/V1PNquPtF523RP+qqkpTCeM0VHdUzDA48+DHeJwGG65RXdy91NPjy4Uq1b5ux7hnZoafXb0s5Y2UV2vr/dvHR4IdogB7rpLXxv7dTZWSvfL3rzZu8EVwn+1tborbne3f+vo7dUHi8ZG/9bhgeCHeN06Pa1OW5s/N9y7uvR8S+95j/fLFv6xLD0u3HH8uTbO5fQtx7VrAz9lT/BDHArB7/yODlpHh7fLTqf1xHof+ABcdZW3yxb+W7pUh6ytTTdMeqmtTS9/zRpvl+uD4IcY9BH3P/0nfW3sVYeMfF7PqbR+vV62ME8oBDffrKu8XnaZ7ezUw1RvuUVPEBBwZoQYdNC2bNFdMWfb0JXPQ2srLF8On/tcoG8fiEsoK4N3v1vvw2PHZn/J1dmpJwK44w4995YBzAlxJAKf/ayecrarS++wmVSh+vr0TCGrVuk5tuS2kvkaG+G979UNkwcP6u66lyuX0zUz19XtIwZUoycEtxvKVGIxHeQ1a+Db39YTBlRX6+rUdKas7ezUjRQf+IBMWXulaWyErVvPnbK2uvrSk+ZNTFk7PKzbRWTK2gKwbWhu1i3WE5PHHzgw9eTx6TSMjOgdlUrpa5z775fJ469UFRVw992wZMm5k8fH47rn38SAiXxet2iPjb09efxtt+nJEwPeEj0V80I8YeFC+Mxn4MEHz32MS1+fvqaZeIzLtdfqqvNNN+npTCW8Vzbb1mFcvvzCx7ik02//Tn29/qip0de+8hiXOVRZqatRW7fKA9XE20IhfaBfuFB/Lw9UM4RlSa8rMbWAj0SaDXNap4UQU5IQC2E4CbEQhpMQC2E4CbEQhpMQC2E4CbEQhpMQC2E4CbEQhpMQC2E4CbEQhpMQC2E4CbEQhpMQC2E4CbEQhpMQC2E4T0dJO2ceQeoU4lGkAeY4jn4PHFfeC8fBcdzJr7Hk/fC6THgWYsdxaGlpAZUHstih+XuSd1yXlr17QA2AhbwX+/brb+zt2HZ8bjdojumysQ+waG5uxn6nWVqnydv5SlQe3B5wToKavwUX19UBFudyu5n3V3CuC26v/lplgdnPrulZiG3b5oYb1oNziuZ7NnpyhDGV4zhw5kEEzVs+gh0umtsNmkO6Cr0d3O55Xy7g3LJh2948INDTM7HeQSFs2573O8u29RnHDhdhh1NzvDVzyHKww3FwpFxMmCgbXpnndRshzCchFsJwEmIhDCchFsJwEmIhDCchFsJwEmIhDCchFsJwEmIhDCchFsJwEmIhDCchFsJwEmIhDCchFsJwEmIhDCchFsJw3k7PMxeUA4OHYeQEjJyE0VPg5sAKQawCUk1QVA9lKyEyf2fYmJfyY5A+DdlhyPSBk9Y/D0V12YimIFYO0ZK53c5ZMjfE+XHo3gOdu2D4ODhZsAA7DpYNKB3snhYd6Hgl1N4CC26F5IK53nrhp3QvDLfpj9yw/lkoCqEzxV05uswAhJNQ1AAlTZBYAJY1N9s8C2aGePAQHP5nGHhL75hEld4ZF+PmId0HR38EHTugaQvU3/H2ThVXBicLA60wcADyaYiWQvEifRCfilKQG4GhQzB8FEqXQcXady5LAWRWKVYKTj4Dx/4VcqNQvBDsacwWGApDsgYS1TDeBW99F/oPwKqPQWQez391JckO6prZSDvEyyFRe+m/sSxdpY6mdHnq2w/jvVBzAyRq/N9mj5jTsKUUtP2bPgNbFpQsmV6Az2ZZuiqdrIWe3bD/m/pILMyWHYTOF2C0Qx/Yo6WXv4xIkW4/yfTrZY13e7+dPjEnxF2/1mfgSJE+Ss7m2iWchOJGOP0KHPwHfY0kzOSkoWsPjPfoqvNsLpGskL4+zo9B1259cDCAGSEe74Fj/7/+Ol7pzTLtGCTrdcNX5wveLFMUXv8BfUeiaOHFr30vh2XpcpHug9OvG3GAD36IldINUmOd+laRlyJFEIroM3z6tLfLFv4b64L+VohXQcjD+awtC4rqYOiIbuEOuOCHeKwdTr8K8WpvjrTnSy7QZ/ruPd4vW/hr6CionG6Y8pod0x+DhwN/Ng5+iLv36Ht9ft2Qt0IQTugqtZP1Zx3Ce9lBXY2OVfi3jliFbuAKeCNXsEOsFPS8BOEif2/Cxyt1dX34qH/rEN4a79V3Fvx8zpUd1Q8JHOvxbx0eCHaIM32QGfC/u2Qoqrtqjnb4ux7hneygbon2u4eVndQ9wAIs2CEe69TN/X73oLEs/THa7u96hHfGe3QXW7+F45AdAifj/7pmKNghzo2CcgvTPdIKG3NfcN5TDrhZfWfBb6HImeduB7e9JNghxpvnt05/dW5h1ydmRikKWzZUwYvi5Qh2iCeOtKoA76ByddVJBJ+ln4NdkIOucvW6vLwP7bFghzhRDeEYOOP+r0s5kKzzfz1i9ixLjwOeGB/sJyet22QKcf09QwEPca2+hZD3OcTKOdNvVkJsjHhlYa5T8+N6XX50NPJIcLcM9H260uX+NzhlBvWQxOImf9cjvBMr1dVqPzvoKFePRU9U+bcODwQ7xAC1G87sLB+b+DP9ULUe4j72/hHeSpwZH57p928d2SGIlQT+Miv4Ia5Yo8eIjnX5s/zssO4jW7vBn+ULf1g2lFylZ/Bw894vX7n6AJFarLvlBljwQxyKQNNWfU3idbXadfRMH7Ub9ER6wiypRihu8KeTzniPrkaXLvN+2R4LfohBV3UX3AZj3d5Vq9WZifSKFsKS+42cIG3eC0Wg8mp9pkz3ebfc3IjuhltxNUSKvVuuT8wIsWXB0vv1Dhtum32QJwIcLYEVH9G3K4SZEtX6IO+Me3N9nBvRY8srr9aXcQYwI8SgW49Xf+JMkE/MfIc5GT3YO1oCqx6C8tWebqaYAyVLofpGvW9H22c2/le5ugqdHYDKa3RbTIBvK53NrNkuY+Ww9hE4th06fqlHOCVqITKNARJuXo9GyY3pHXTVB3WjhTCfZUHZcj3a7fSrurY2MSn8pYI4MW1t5rT+m+rr9YR5hgQYTAsx6B217Legci0c/4me3WGsQwc5nAQ7cWYHKH0PMT+mB1KgdNWraQs0vFu3SIsrS1G9DuLAQT02fKRNDzOd6HF19uTx+bSugufH9XVv+WooW+XPLCE+My/EoI+8FeugfI2eSL6nRU8anhnQHTeUq38nFNWhL1upr5uq1gf+doGYpXACqq6FshW6aj3WocelZwf0aCSFvj0VjuuDerJOz3BpYHgnmBniCVZI76yyFbpalB3QVWY3r3dUpFjvqEIMWRPBEk5A6VX6w82dGdaa1+UkFNbdeS933vKAMjvEZ5voFC8tzeJ8oQjEyuZ6K3xjztW7EGJKEmIhDCchFsJwEmIhDCchFsJwEmIhDCchFsJwEmIhDCchFsJwEmIhDCchFsJwEmIhDCchFsJwEmIhDCchFsJwEmIhDOfppACO44Dj6s/zmOM4OI47+TXW/H0/9Hsh5WLC2WXDK56F2HEcWlpeArcXLLBD8/ck77guLfv262/s7dgBfiym3xzXpWXvHlAD875cwLllo3mrg+1BAj2enkeeonABt5t5fdXiujrAYgrexM+zENu2zQ03bgCVo7n5bmw7uE9W95uuQm8Ht5vmezbKe6H0181bPoIdLprbDZpjjuNA6GdACNujmVc9PRPrwmpjh1PzuuBiOdjhODghbNue3+8FYNu6JmKHi7DD5k4N6wnLwQ5P42EHl2Ee1/OEuDJIiIUwnIRYCMNJiIUwnIRYCMNJiIUwnIRYCMNJiIUwnIRYCMNJiIUwnIRYCMNJiIUwnIRYCMNJiIUwnIRYCMNJiIUwnMfT88yVfuAwcBzoBNJABCgDms76kOmD5hcHXTYGz3ykz/w8CpQApUAFuqyYy+AQK+A14DngP9A7K3/mNeus37GAYmAtcA+wEfB2ZgURNGPAMWA/0AWMn/n5RMXTRZeLKFAFrAaWoENtHkND3At8C3gWGEXviCXonXI+FxgC9gK70Tvsd4HrC7KlopBcdI3sRXSNLIEuGwmmroWlgT7g5+gz8o3og71ZsTBrawG9g55A76yF6PC+kxC6Wl0GZIA3gS8CHwQewsi3QEwhDexE185iwDLgUnObxYF6oA7oRof5BPAuTDorG1aCfwn8BfrMuprL3/wYsAroAb4DDAB/gOnXRGIcXSvbDyxCXz5dDguoRR/oD6Cr43cD5d5too8Map1+Bfhf6OrzCmZ+/LGAGvQR+EfoarnyYgPFnMij20T2A1dx+QE+28QZvA19UBib9dYVgiEhHgaeRF+/XIU3rcxlQDXwA/T1sjDTG8DrXLxN5HLZ6DJ2FF0ugn+ANyTE/4jeUV4FeEI1+lrqG+gDhTBLL7AHfUD28lE5YXRN7RX0WTnYDAhxN/AToBJvjrTnuwpoRV9vC7O0ots1anxYdgn6PvNrBP1sbECIf4k+4tb6tPzImY9/Q9+iEGYYQYe4Ev868dSiOxB1+7R8bwQ8xAp4Bl1V8nNTFwAHz3wIM5xCd/Cp8HEdxejGrRM+rmP2Ah7iAaAdfc3jp4mddczn9Qjv9KHPwH4X4STQ4fM6ZifgIT6OrjbN5rbBdExUx476vB7hnXZ0Tyy/FaEv57IFWNfMBDzE/eg3z48GrfNF0F31RPC56LsJhXh4ewzd0y99qV+cMwEPsYM+SxZi9FGItwdQiGCbaIAsVLlQBLnRM+AhDqPfwEI08Tvoo64IvhA6wIUIlntmfcGNSnC3DND3/+IUpiqTRw+oEMEXQvdrHr/UL3pgHH3tXVSAdc1MwEPchG7U8rs31cT40sU+r0d4p47ChHgUfTK51IiouRPwEBehO6T3+7yeQSAFLPV5PcI7FegDr5/tGAp9oKjzcR2zF/AQgx4S5gA5H9fRCVyHPvMLMyxE96jq9XEdg+hxxY0+rmP2DAjxRqABfV/QD2Pot+F9yBxcJomhx5T3ow/yfuhC960P9rhiA0KcAn4LHbZRj5etgCPATcCtHi9b+G8lerTRKR+W3YMeBHGND8v2lgEhBrgPfUY+grdH3Tb0cMRHkNk9TFSMPvjm0bO9eGVi7q2b8WeElLcMCXEY+DS6kesA3gS5Hb3zP4muMgkzLUVPcNeBN3cx0ujut1ejJ80LPkNCDHrupD9B77T9zHzqFBd9Rs8AnwLe78nWibliAbegz5qd6GrwTA2gB8FcA9yJKbUzg0IMem6tPwVuQ7/ZbUz/FoNCN4K8gR6D+nngN5HGrCuBjS4Td6HLw0Eu7yCfQR/Yh9CXbe+mMP2yvWHYbJegbwP9d/TcWN9DDwyPoe8bFnPuYAkX3Rg2iA5wCXAv8DB6DLG4ctjAenRD14voKnEWXS6KuHDu6Qx6hFwf+ly2EH02D/btpKkYGGLQ1ZzfQt9D3oGeleMEuip1/vVyEXo88v3oI+wy5Ox7JasBtqCr1m+hw9zLhV13o+iycTW6hteAqXEwc6snlQNb0de1p9HjjzvQHUNs3n4Wk7k7SMxECH1GrkdXjwfRVeWJMcFh3n4Wk/mDXq6Qkm2hH9dRNdcbIgInwpVeNgxr2BJCnE9CLIThJMRCGE5CLIThJMRCGE5CLIThJMRCGE5CLIThJMRCGE5CLIThJMRCGE5CLIThJMRCGE5CLIThJMRCGE5CLIThPJ0UwHGccz7PV47j6PfAceW9cBwcx538GkveD6/LhGchdhyHlpYWUHkgix2avyd5x3Vp2bsH1ABYyHuxb7/+xt6ObZszi6QfdNnYB1g0Nzdj27N/2qK30/OoPLg94JwENX8LLq6rAyzO5XYz76/gXBfcMw+BU1nOnZ11ZjwLsW3b3HDDenBO0XzPRk+OMKZyHEdPcw00b/kIdji4D6j2m65Cbwe3e96XCzi3bNi28mSZnp6J9Q4KYdv2vN9Ztq3POHa4CDucmuOtmUOWgx2OgyPlYsJE2fDKPK/bCGE+CbEQhpMQC2E4CbEQhpMQC2E4CbEQhpMQC2E4CbEQhpMQC2E4CbEQhpMQC2E4CbEQhpMQC2E4CbEQhpMQC2E4CbEQhvN2ep45opSid2yA40MddI70knPzhKwQZbEUTaV1NKSqidiRud5MMQdyTo7BzAiDmRFyTh6AcChMSayI0lgxsfDsp8eZa0aHuH98iF+deImfHtlF21AnI9kxHFfPrIgFKCiKJiiLFfPuxTdxV9NNLCtfhGVZc7rdwl+ucukY6eVQXxtHB9sZzY4zns8yudsVRO0IRZE4i0oWsLyikYUlNYRDZsbByK3OOjl+2Po833vz53SNniZqR6iIl1JdWk70rDOuq1xGs+MMZkf4zqvb+UHrL7ht4bU8vP43WFBcNYf/gfBL92gfL556naOD7eScHOWJEqqLKojb0XMO3pl8lpHcOK/1HOKN3iMsTNVwc/1aGkvr5nDrZ8a4EB8f7OCre/+JF0+9RiqaZEVFE+HQ1PM2hawQqVgRqVgRDcU1DGSG+bfDu3ij5wi/s/4B3rP4ZjkrXyEc1+HV7rfY0/EGw9kxFqZqSUYuPj1uLBwlFo5SmSgl42Q5NdzDv771S9bXruTGujVGVbONCvHB08f5rzu/yaH+k1xVtvAdd9L5LMuiPF5CaayYY4PtfPmF79A3PsRvrt4sQTZc3s2z6+Sr7O3YT1k8xYqKpsv6+5gdZWlZAwPpYXadepXh7Cibmm4kHo75tMXeMibEJ4Y6+a87v8WRgVOsqVyCfZGz76WErBBLyxbSPtzD37z8fRLhGFtX3OHx1opCUUrx4qnX2d3+BvWpKlLRmU8PXBZPkQjHeLX7EBYWdy2+yYgGUSNuMeWcHH+993sc6j/BqorFMw7w2epT1YQtm2+9+iMO95/wYCvFXDgycJK9nfupK66cVYAnxMJRlpTV62vlniMebKH/jAjxv771K3adepWlZQ2eBHhCY8kCekb7+fq+fyHn5DxbriiMkewYL5x87cwto2LPlhsPx6hIlLK743W6R/s8W65fAh/i4cwo33vz5yTDcYoiCU+XbVkWS8sa2NP+Bi+ces3TZQv/tZ4+TvtIDw2pGs+XXZ0sZygzyitdBz1fttcCH+Jdp17h1HA39cXVviw/GYnjovjZkV0o5c1jNYT/Mvksb/YeoTyewrb8Kca1RZUcGThF//iQL8v3SuBD/PMjL2KHbCK2f21wC4oqeamzleODHb6tQ3jr5HAXXWN9VCXLfVtHaayYwcwIbUOdvq3DC4EO8Wh2nEMDJymP+/sso9JYMcPZUY4MnPR1PcI7feNDKMVF+wh4wbIsEpEYHSM9vq3DC4EO8fHBDkayY6QiSV/XE7JCKOCYnImN0THSSyLi/33cokiC7rF+HDe4D0cPdIi7x/pI5zMFueketsKcHOr2fT1i9lzl0p8eIlGAcpEIxxjPZRjNjfu+rpkKdIjzroOFVZAeVXYoRMbJ+r4eMXuuclEoQgUoFyErhKtc3AA3egY6xLYVQqEK0mrsKtfX6yvhnZAVAiwKkStXKSysghwwZirQIS5PlBANRcgWoCNGzs3LyCZDhKwQqWiSdAFqThknQywcDXQ/6kCHuKmkjuJokpHcmK/r0Wd6iyWl9b6uR3invria8QJcp47m0lQlys4Z4ho0gQ5xWTxFfaqagfSIr+sZyY2TDMdYbOBY0vmqIlGCUvoyyE9j2TR1Aa+hBTrElmWxefHNpPMZX3dW50gvKyqbWFF5eUPYxNxpSNVQHk/R52NvqpHsOMlIjEUltb6twwuBDjHAHY3XU5Uso8unjuhZJ0fOzXPvVRvPNJgIExRHk6ysXMzp8QHfGj67Rk/TVFpHTVGFL8v3SuBLbU1RBc3LbuP0+IAvDVxHBk6xsrKJOxZd7/myhb9WVS6mLJ6ie6zf82UPZUawrRBX1ywP/KQRgQ8xwIfX3MO66mUcHjjp6VG3Z6yfeDjK7173AVKx2Y9FFYVVmSzjprq1DKSHSeczni037zqcGu5h/YKVNJYs8Gy5fjEixKlYEf/3Db9JRbzEsyAPpIfpGevnN1a+mxvr1niwlWIurK1eyrrqpRwdaPekpua4Dof7T7K0rIEbFqwK/FkYDAkxwLW1K/ijDR+lKBLnYH8b+Rn2ZVVK0T3aR/tID/evuJNPXnu/ETtKTC0cCnNn4w2sqVrC4f6TjGRnftspk89yqP8EjSULeM/im0l6PH7dL8bMsQW6kSsejvLVPf8fb54+ysJUDWWx1LRDmMlnOTJ4iqJInG1Xv5+Hrt1q7FzD4m2JSJzNSzaQiMR5rfsQA+kIdanqaY8zVkrRPdbPQHqYVZWLedei6yj1eeScl4wrwTfXr+Pxu/8fvvXyj3j22G7aR3qojJdRkSiZ8oa8q1yGMqN0jp5GoVhduYRHrv8A1y1YNQdbL/wSD8d4d9ONNJYs4MVTr3Go7wSJcJSqZDmJcGzKA306n6FvfIjBzAiViVLeu+QW1lQvMe7AbtbWnlGVLOfzt26jedltPHtsN//Rto+jg6fIuy6g+7oC6H5Y+nbETfVruGfpRjYuvMaYapK4PCErxPKKRhpS1Rwb6GB/7xG6RvsYP9PoNdH/2VUuFhZRO0JVoowN9etYUlZv1Nn3bEaGGHRHkKtrlnN1zXK2Xb2VwwMnaRvspGOkl3Q+Q8QOUx4voam0jqbSOhpLFsi17zyRjCRYU72UlZVN9KeHJp/FlMnnUCiidoSSaBFl8RTl8ZQR09K+E2NDfLbyRAk3JtZIK7M4hx2yqUqW+zqFTxAY0zothJiahFgIw0mIhTCchFgIw0mIhTCchFgIw0mIhTCchFgIw0mIhTCchFgIw0mIhTCchFgIw0mIhTCchFgIw0mIhTCchFgIw3k6KYDjOOC4+vM85jgOjuNOfo01f98P/V5IuZhwdtnwimchdhyHlpaXwO0FSz+0e75yXJeWffv1N+F/x7bn75xeUi7OdXbZaN7qYHuQQI/fUZnD6kLzu9BqUi6m5s051FLTeJzC0NAQpaWlDA4OUlJSctHfy2azoLLYdgEe4R5wuuoYxg7P37PwBMdxpFycZaJsRGPF7/h7082dp9fE0WgUiHq5SGN5UU26Uti2jZSLt3ldNqSuJ4ThJMRCGE5CLIThJMRCGE5CLIThJMRCGE5CLIThJMRCGE5CLIThJMRCGE5CLIThJMRCGE5CLIThpjWeYmK04tDQkK8bI4R420TeLjVaeFohHh4eBmDRokWz3CwhxOUaHh6mtLT0oq9Pa1IA13Vpb28nlUphWTJLgxCFoJRieHiY+vp6Qu8wrdG0QiyECC5p2BLCcBJiIQwnIRbCcBJiIQwnIRbCcBJiIQwnIRbCcP8HIF6qYsJSZ4UAAAAASUVORK5CYII=",
      "text/plain": [
       "<Figure size 640x480 with 1 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "# Define the grid world dimensions\n",
    "n_robots = 5\n",
    "l_corridor = 3\n",
    "\n",
    "# Initialize the robots\n",
    "robots = []\n",
    "for i in range(n_robots):\n",
    "    robots.append(Robot(\"r\"+str(i), (0, i), (l_corridor-1, i)))\n",
    "\n",
    "plot_grid_world(l_corridor, n_robots, robots)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2bc27790",
   "metadata": {},
   "source": [
    "### Define dynamics contracts for each robot per timestep\n",
    "The contracts are explained in detail in the multiagent.ipynb notebook."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "8c4afdae",
   "metadata": {},
   "outputs": [],
   "source": [
    "def get_dynamics_contract_robot(name: str, init_pos: Coord, timestep: int, grid_n: int, grid_m: int\n",
    ") -> PolyhedralIoContractCompound:  # noqa: WPS210\n",
    "    \"\"\"\n",
    "    Function to set up the contract encoding the dynamics for a single robot for the next timestep.\n",
    "\n",
    "    Args:\n",
    "        name: name of the robot\n",
    "        init_pos: current coordinates of the robot\n",
    "        timestep: current timestep\n",
    "\n",
    "    Returns:\n",
    "        Resulting contract compound that encodes the dynamics for the robot.\n",
    "    \"\"\"\n",
    "    x_str_0 = 'x_{0}_0'.format(name)\n",
    "    y_str_0 = 'y_{0}_0'.format(name)\n",
    "    x_str_1 = 'x_{0}_1'.format(name)\n",
    "    y_str_1 = 'y_{0}_1'.format(name)\n",
    "    t_0 = 't_0'\n",
    "    t_1 = 't_1'\n",
    "\n",
    "    contract = PolyhedralIoContractCompound.from_strings(\n",
    "        input_vars=[x_str_0, y_str_0, t_0],\n",
    "        output_vars=[x_str_1, y_str_1, t_1],\n",
    "        assumptions=[\n",
    "            [\n",
    "                \"{0} = {1}\".format(x_str_0, init_pos.x),\n",
    "                \"{0} = {1}\".format(y_str_0, init_pos.y),\n",
    "                \"{0} = {1}\".format(t_0, timestep),\n",
    "            ]\n",
    "        ],\n",
    "        guarantees=[\n",
    "            [\n",
    "                \"{0} - {1} = 1\".format(t_1, t_0),\n",
    "                \"{0} - {1} + {2} - {3} <= 1\".format(x_str_1, x_str_0, y_str_1, y_str_0),\n",
    "                \"{0} - {1} - {2} + {3} <= 1\".format(x_str_1, x_str_0, y_str_1, y_str_0),\n",
    "                \"-{0} + {1} + {2} - {3} <= 1\".format(x_str_1, x_str_0, y_str_1, y_str_0),\n",
    "                \"-{0} + {1} - {2} + {3} <= 1\".format(x_str_1, x_str_0, y_str_1, y_str_0),\n",
    "                \"{0} <= {1}\".format(x_str_1, grid_n - 1),\n",
    "                \"{0} <= {1}\".format(y_str_1, grid_m - 1),\n",
    "                \"-{0} <= 0\".format(x_str_1),\n",
    "                \"-{0} <= 0\".format(y_str_1),\n",
    "            ]\n",
    "        ],\n",
    "    )\n",
    "    return contract"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "959e8914",
   "metadata": {},
   "source": [
    "### Extension to N robots and a grid length of L\n",
    "\n",
    "Choose the number of robots in $n_{robots}$ and the grid length in $l_{corridor}$. The maximum number of timesteps is set to be 3 times the grid length (as upper bound). The robots will be placed as shown in the visualization above. The function below does not produce any animation or save the trace of the simulation."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "f82c9beb",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAgMAAADwCAYAAACdQmfJAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjcuMSwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/bCgiHAAAACXBIWXMAAA9hAAAPYQGoP6dpAAAhL0lEQVR4nO3de3hU5aHv8d+aNZkkkysJSUggRJA7KOINROrGLSqXR3T31NZ6qdSn3h4vR8957Kndp+fR02fXXZ+63a1WW9pq98babdtdW4/1VmnZCtSKaYsiGm7hIpgQAiGT68ysWeePt0m5EyAza8z7/TxPCMmEWe8Mb9b6rffq+L7vCwAAWCsUdAEAAECwCAMAAFiOMAAAgOUIAwAAWI4wAACA5QgDAABYjjAAAIDlCAMAAFiOMAAAgOUIA8AnxJIlS3Taaacd9+e2bt0qx3H04x//OO1lOlVz587V3Llzj/tzK1askOM4WrFiRdrLBNiIMACkWWNjo+68805NmDBB0WhU0WhUU6ZM0R133KF33303kDK9/fbbchxHjz766GGPXXnllXIcR08//fRhj1100UUaOXJkJooIIIMIA0Aavfjii5o2bZqWLVumefPm6dFHH9W3v/1tLViwQC+99JLOOussbdu2bUDP9YMf/EANDQ2DUq6zzz5b0WhUK1euPOyx1atXKxwOa9WqVQd9Px6Pa82aNbrwwgsHpQwAskc46AIAQ9XmzZt1zTXXqK6uTsuXL1d1dfVBj3/zm9/UE088oVDo2Jm8s7NTBQUFysnJGbSyhcNhzZw587ALfkNDg/bs2aNrr732sKBQX1+vnp4ezZkz55SP39XVpWg0esrPA2Bw0DIApMnDDz+szs5OPf3004cFAclckO+++27V1tb2f2/JkiUqLCzU5s2btXDhQhUVFem6667rf+zQMQNtbW1asmSJSkpKVFpaqhtvvFFtbW0DKt+cOXPU3NysTZs29X9v1apVKi4u1i233NIfDA58rO/f9XniiSc0depU5ebmqqamRnfcccdhx587d66mTZum+vp6XXTRRYpGo/rqV7961HJ99NFHuuqqq1RQUKDKykrde++96u3tHdBrAnByaBkA0uTFF1/UuHHjNHPmzBP6d8lkUpdffrnmzJmjb33rW0e9g/Z9X1deeaVWrlyp2267TZMnT9bzzz+vG2+8cUDH6buor1y5UuPGjZNkLvizZs3SzJkzlZOTo9WrV2vx4sX9jxUVFWn69OmSpAceeEAPPvig5s2bp9tvv10NDQ168skntWbNGq1ateqglozW1lYtWLBA11xzja6//npVVVUdsUzd3d265JJLtH37dt19992qqanRsmXL9Lvf/W5gbx6Ak0IYANKgvb1du3bt0lVXXXXYY21tbUomk/1fFxQUKD8/v//r3t5eXX311XrooYeOeYwXXnhBb7zxhh5++GHdd999kqTbb79dF1988YDKeMEFF8h1Xa1cuVJLliyRZC741157rfLy8jRjxgytXLnyoDAwa9Ysua6rlpYWPfTQQ7rsssv08ssv93d1TJo0SXfeeaeeeeYZffGLX+w/VlNTk773ve/p1ltvPWaZli5dqg0bNuhnP/uZrr76aknSzTff3B9AAKQH3QRAGrS3t0uSCgsLD3ts7ty5qqio6P/47ne/e9jP3H777cc9xksvvaRwOHzQz7quq7vuumtAZSwqKtKZZ57ZPzZgz549amho0OzZsyVJF154YX/XwIYNG9TS0tLfmvD6668rHo/rnnvuOWjMw80336zi4mL95je/OehYubm5B4WDY72m6upqfeYzn+n/XjQa1S233DKg1wTg5BAGgDQoKiqSJHV0dBz22Pe//3399re/1TPPPHPEfxsOhzVq1KjjHmPbtm2qrq4+LHBMnDhxwOWcM2dO/9iA1atXy3VdzZo1S5I0e/Zs1dfXq7e397DxAn0zIA49ViQS0dixYw+bITFy5EhFIpEBvaZx48bJcZyTfk0AThxhAEiDkpISVVdXa926dYc9NnPmTM2bN++oU/Ryc3OPO8NgsPRd3FetWqVVq1bpjDPO6A8Xs2fPVm9vr9asWaOVK1cqHA73B4UTdWA3CIDsQxgA0mTRokXatGmT3n777bQ8f11dnT7++OPDWh9OZC2CAwcRrlq16qCAUlNTo7q6uv6gMGPGjP7BjHV1dUc8VjweV2NjY//jJ/OaNm/eLN/3T/o1AThxhAEgTb785S8rGo3qpptuUnNz82GPH3rBO1ELFy5UMpnUk08+2f89z/P02GOPDfg5ampqNGbMGC1fvlzvvPNO/3iBPrNnz9avfvUrNTQ0HDSlcN68eYpEIvrOd75z0Ov40Y9+pP3792vRokUn/Zp27dqlX/ziF/3f6+rq0tKlS0/q+QAMDLMJgDQZP368nn32WX3+85/XxIkTdd1112n69OnyfV+NjY169tlnFQqFBjQ+4EiuuOIKXXjhhfrKV76irVu3asqUKfrlL3+p/fv3n9DzzJkzR8uWLZOkw7ouZs+erZ/+9Kf9P9enoqJC999/vx588EHNnz9fixcvVkNDg5544gmdd955uv7660/qNd188816/PHH9YUvfEH19fWqrq7WsmXLWKAISDPCAJBGV155pd577z098sgjeu211/TUU0/JcRzV1dVp0aJFuu2220562lwoFNILL7yge+65R88884wcx9HixYv1yCOPaMaMGQN+nr4wMHLkyMOa9w8MB4euPPjAAw+ooqJCjz/+uO69916VlZXplltu0Te+8Y2TXi0xGo1q+fLluuuuu/TYY48pGo3quuuu04IFCzR//vyTek4Ax+f4p9pWCQAAPtEYMwAAgOUIAwAAWI4wAACA5QgDAABYjjAAAIDlCAMAAFhuQOsMpFIp7dq1S0VFRYdtIAIAALKT7/uKxWKqqak55p4nAwoDu3btUm1t7aAVDgAAZM6OHTuOudrpgMJA33asO3bsUHFx8eCUDAAApFV7e7tqa2v7r+NHM6Aw0Nc1UFxcTBgAAOAT5nhd/AwgBADAcoQBAAAsRxgAAMByhAEAACw3oAGE6RSPxyVJrusGXJKhzfM8SbzP6cb7nBm8z5nB+5wZfe9zJBIJrAyBhoF4PK6vf/3rkp/UOefOkHuMBRFw8rxUSvXv/EmSo3POnckvdpp4nqf6+nrqc5pRnzOD+pwZB9bnr/2fBwMLBIG3DMhPSqkWyftI8qlsaZFKSak9f/0iKYmTZ9pQn9OP+pw51Of0O7A++3FJFoYB13V1zjlnSd5OLZw/m4SfJp7nSb75+8IF8+SGj734BE6OeZ97qc9pRn3ODOpzZhxYn13XD6wcgbcMmAoWkuu6VLY0ct3QXz/zPqcT9TkzqM+ZQX3OjL76HKTgSwAAAAJFGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoSBE+T7UiplPgMAsg/n5xMXDroA2SyRkNavz9fWbRE1bovog/V52tfmyvMcOY5UUJDS+PE9Gn96XHV1vZo8qUclJamgiw0AVujpcbRnT1htba5a97pqaspRPO4o5UuhkFRYkNKIEQkNK/VUWuqpoiIp1w261NmJMHAEu3eHteKNQr36WrG2bo2oNx6S4/iKRlPKjfhyQr5831FXi6vGrcV69VUp5EoVFUldekm7Lv67Do0f3yvHCfqVAMDQ09rqaktjRB98mKe9e8PyPHPxj0ZTyglLcnwlE46aYq4at0bk+44ikZSqq5OaMqlHdXVxFRRw43YgwsABOjtD+ulzw/T/flOi1j1h5Uc91dTElZ/vH+PCnjB/JqTdLTn6t2Xlev7XpZp5fqduvqlVo0YlMlZ+ABjK2ttDWvNOVBs35SoWc1Va6ml0bVw5Ocf/tz09jpqbw2psLFZ5WVLTp3frjGk9ikToU5AIA/3+8pd8ff+Hw/Xue/kqL09q8uRuhU5gREVOjjSyJqGa6oTa2lz99vVivb8+X0tuaNWC+e00TQHASUqlpE2bcvXW21E1N+eopjqhkTXJE3qOvDxfo2sT8jyptTWs3/2+SDs+imjW+Z0aMeLEnmsosj4M+L703M+H6d+XlamzM6QJ408tKTqONGyYp5KSbm3fEdG3/qVKf16br//x31tolgKAE5RISKtWF+gva6PKjfiaML73hG7UDuW6UmVlUqWlnrZsiai5KazZszs1bWqP1V27VocB35ee/rcyLftJuQoLPE2cOHiVIRSSTquLqz0W0iuvlKi7K6SvfqVZhYUEAgAYiHjc0Yo3CrV2bb5GjUwM6vkzEvE1flxczbtNK0Ey6eis6d3WBgJrpxb6vvTT54Zp2U/KVVqSVE1NIi2VoLgopbFje7XijSJ9618q1dNjaU0DgBOQTEpvrizQ2rX5qhsdT9uNVFVlUiXFnt54s1DvrctLyzE+CawNA/V/iurfnylTUaGnysr09hdFoymNGdOr139XpOd+PiytxwKAoWDd+/n689qoRteaQdzpVF7uqbAgpdV/KNCuXQMYjTgEWRkGYrGQlv6wXN1dIY0YkZnR/oUFKZWVefr5L4Zp/Xp70ycAHE9LS1hr1kQ1rMRTNJqZ0f6VlUl1d4f01ttR9fba14JrZRhY9pMyvf9+vsaOzexaACOqEtq/P6Qnlw6nuwAAjiCZlN76Y1TtsVDaW20PVTc6rs2bc7X23fyMHjcbWBcGPvooRy+/UqyKykTG55c6jjR2bK/WvpuvlasKM3psAPgk2LYtoo2bc1U3OvNrtOTkSMPLk3r3vXy1t9t1ebTr1Upa8Uah9u4Lq2J4MPNK8/J8hRzp5VeKWT8bAA7g+1LDhlyFJOXmBnOCLCvztG+fq61bcwM5flCsCgPd3Y5efa1YRUXeKc1TPVXV1XGtez+PsQMAcICWlrC2bs1VVVVwiwCFQlJhYUrrP8xV0qK1iKwKA2vfzdeOHRGNqAp2ieCiopQ6Ol39cU000HIAQDbZuTNHnV2hwNdjqaxIqqkpR01N9swssCoMbN2aq6QXXPNTH8eR8vJS+uADWgYAoE9Tc1h5ecH3n0YivjxPamuzZx15q8LApi0RuVnyigsLPDVuzWVWAQDIzCJo3p2jggIv6KJIMt0FrXsJA0NOKiV9+GGeCguzo6IVFqXUHgtpx45I0EUBgMC1t7vq6gypIJodS7YXFKS06+McawZ6WxMG4nFHHZ2hwLsI+uTlphSPhxTrsOa/AACOqrfXUTzhZM2WwpGIr56ekLzsuH9MO2uuRImEIz/lKBTKjooWCpnWikSCbgIA8DxHvq+s2Sgo5Eh+ypTLBtaEgVDIVDLfz47/2FTKlMe1p0sKAI7KcbInCEhmzQM5ypobyHSzJgzk5qbkun7WzBv1PEeu6ys3kh39YwAQpHDYVyiUPXfifedoW27YrAkD4bBUVxdXZ2d2/M92dIRUUJBSTU2wax4AQDYoKvIUjabU2ZUdl6WurpCGDw92gbpMsuRlGpMn9ainNzteckenq8qKpMrKLBmdAgDHEI36Kinx1JUlYaA37qg6Q7vaZoPseNczpG50XJLprw9aZ0dIU6d0Z1UfGQAEqaY6rq7O4E+KfdeIkmJ7btasCgNTJveotDSpvXvDgZYjHnfkhKQzpvUEWg4AyCYjqpJSSEoEfEPe1uaqpNhTRUWWDDLLAKvCwKhRCc2a2andLcGGgebmsEbWJDT7gs5AywEA2aS2NqGqyqRa9gR7jt7TGtb48T0qLs6CZuQMsSoMSNJl82LKCSuwfinfl/bvD+vyy9pVUGBPRQOA44lEfE2Z3KP9+93AVv7r6naUk+Nr3OnxYAoQEOvCwNkzujR1are2bo0EUtl27sxRRWVSl1wcy/zBASDLjR3Tq+HDk2pqDqZ14KOPcjTmtF5VV9szeFCyMAyEw9KtX9qjkpKUmjNc2bq6HLXHXF17zV7V1tpV0QBgIEpKUpp5XpdisZC6uzM7mLClJaziopRmnt9lzZTCPpa9XGPatB79t0/vU2trTsZ2DUylpC2NeZo1s1P/cGVbRo4JAJ9Ekyb1aMrkHm3fEcnY7K/eXkd721ydd16XKivtGTjYx8owIEmfu3qfzj+vUxs35SkeT28g8H1pw8Y8jRoZ1+237FFOTloPBwCfaK4rzZrZpRFVCTVmoEs3kZC2NEY0eVK3pk7pTu/BspS1YSAa9XX//2rW9DO71bAhT7296QkEqZQJAuVlSX3lvmaNHWvXoBQAOBnDhnm65O9jGlbqaUtj+loI4nFHmzbnatLEHl38dx3W3qxZGwYkqaIiqQe+9rHOObtLGzbmae++wV2quLvb0Qcf5qmyIqn//dUmzZhhZ+IEgJNRXZ3UZZe2a3h5Uhs35Q56t+7+/SFt3hLRlMk9uuTvOxSN2rEp0ZFYHQYkqaoqqa8/8LE+/Q9t2rcvrI0bc095MyPfl3buytGWxjydf26X/un/7tLZBAEAOGHV1UktXNCuyZO7tX1HRE3N4VPuNkgmpcbGiPbvd3Xh7A7NuyRm/VTvYFd2yBKlpZ7+5z27NfO8Tv3wqeFqaMhXftRT9YiE8vMHXuuSSal5d4727Q2rvDypO25v0aevalNurr1pEwBOVVmZp8svjWn0qITeXlOghg25Ki31NLw8qfAJXMV6ehztbgmruzuk0bVxzZrZqdGjmdklEQb6OY70qTmdmja1R79dXqRXXyvWlsZcJRKOCgs9FRZ4KipKKSfH799PIJmUOjtdxTpC6oi5SvmOqqoSuuH6Vl02L8b4AAAYJOGwdMYZPRo1KqFNmyP64MM8bWnMlRvyVVCQUrQgpYJo6qAth+NxR51dIXV1hdTREVJOjq+RIxOaPLFHY8f2ntDN3lBHGDjEsGGePvuZNl21eL/eqY/qrT9G9f76fO1uCat1a44SCUf6axgIhXwVFqQ0rNTTrPO7NOOsLn1qTodKSuxubgKAdBk2zNN553brjGk92r49op27cvTxxzmKxULavTv814GGjnxfyskxQaG8PKkzpsU1ujahmprEQYEBBmHgKCIRX7Mv6NTsCzrl+9Leva62b48o1uEqkXAUDvvKy0tpZI2pXLYtUAEAQcrL8zVhQq8mTOiV70uxWEjt7a6SSUeplJmeGImkVFLiWT0wcKAIAwPgOFJ5uafycgYBAkC2cRypuDhl1cZCg437WQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAsRxgAAMByhAEAACwXDroAnudJXsp8Rlp4nifPS/X/XQ7vdTqY95n6nG7U58ygPmfGgfU5SIGGAc/zVF//Zym1R3IkN0RDRTp4qZTq/7TefOG+KNfNC7ZAQ5SXSqn+nTWS30Z9TiPqc2ZQnzPjwPq88ApPbkBX5cBbBiQn6ALYJbVb9A6lSSplTpzIHOpz+lCfAxDcJTnQMOC6rs45d6bkJ7Rw4aVyXTfI4gxZpin1RSm1Wwvnz+Z9ThPP8yTf/H3homvlhguCLdAQRX3ODOpzZnieJ4VelRSSG84PrByBtwyYX2RXbriIX+p0cTy54TzJC8l1Xd7nNHJdc5fqhgvkhosCLs0QRX3OGOpzBjie3HA06FLQvgYAgO0IAwAAWI4wAACA5QgDAABYjjAAAIDlCAMAAFiOMAAAgOUIAwAAWI4wAACA5QgDAABYjjAAAIDlCAMAAFiOMAAAgOUIAwAAWI4wAACA5QgDAABYjjAAAIDlCAMAAFiOMAAAgOUIAwAAWI4wAACA5QgDAABYjjAAAIDlwkEXIOu1tkrbtpmPxkbzdTwu5eRIhYXSmDHS6NFSXZ1UUyOFyFcAkBG+L8ViUlubtH+/tHev1NsreZ45R+fnS2VlUmmpVFIiRaNBlzhrEQaOJJGQ6uulV181n2Mx8z3HkSIR89n3pWRSSqXM14WF0umnSwsWSHPmSMXFQb8KABiaenul7dulhgZp506ps9Oci8NhyXXNTVkqZc7bvm++33eOHjeOG7cjIAwcKJWSXn9d+tnPpM2bzcW+slI67TQTAo7G80xgWLdO+stfpOpqEwo++1mpoCBTpQeAoS0el95/33zs3m0u8uXlUlWVCQFHk0iYc3R9vbR2rTRqlHTWWdLYseZmDoSBfh9/LC1dKq1YYRJjba1pYhoI1zXNUKWlJkA0NUk//KH09tvSbbdJ06enseAAYIGmJumtt6SNG825dswYEwYGIifHdBeUlUk9PdKuXdJHH5lz87nnmlYDyxEGJGnlSunxx02zU13dqTXxh8MmdVZWmvR6//2mheCGG46dXAEAh0ulpHfflf74R9MdMHbssVtqjycvz7T2dnRIa9aYUHDRRWbsl8XoNHntNemf/9k0OU2dOnh9/ZGINGmSSaRPPSV997um1QAAMDCplGlh/f3vzbl0/PhTCwIHKiw0z7d3rxkftnnz4DzvJ5TdYWDFCulf/9X0J40bN/gDShxHGjHC9Gf9/OemGyKVGtxjAMBQ5PvSO+9Iq1dLw4dLFRWDfwzXNd0NyaS0fLm0devgH+MTwt4wsHmz9J3vmAEpdXXpHURSVva3QPDKK+k7DgAMFZs2SX/4gwkCpaXpPdaoUeamcMUK01JgITvDQCIhfe97UnNz5kaTlpeb5q0f/9hMhQEAHFl7uxksGIlIw4Zl5pi1tdKePaZbwvMyc8wsYmcYeP55U9EyPa1k9GgzWGXpUisrGwAcVyplBvY1NZn1ADLFccw5ev16s36BZewLA3v3Ss89JxUVZX41qlDIjGJ9802TPgEAB9u508zEGjUq8wsD5eebtWHWrJG6uzN77IDZFwbeeMN0D2QycR6oqMh0U7z2WjDHB4BstnGjGdAX1Nz/qiqppcUsQW8Ru8JAMim9/LKUmxvsnP+qKtMyYFllA4BjamszAweHDw+uDK5rrhEffGDV7C+7wsC6daaiBdUq0KeszFT61auDLQcAZJMdO8yGQ+mePXA8lZVmfNfu3cGWI4PsCgNbtpgNLoLeuapvw6P164MtBwBkk+Zmc1ce9H4B0aiZdr5vX7DlyCD7wkDQlaxPYaG0YQOrEgKAZJrkm5qCv1nr4zhWrTlgTxjwfXMnni0bUhQWmuYw1hwAALO2QEdH9uz0Go2aDY0sYU8Y6O01TT55eUGXxMjPN7tnWZQ8AeCourvNOTFbztF5eWZjJEtab+0JA4mEaYbKlp0DQyFTnng86JIAQPBSKdOCmy1duX3naEtmFNgTBvoqmO8HW44DOU7mF9UAAOAQ9lyJIhHTKpAtywB7ngkCg7UdJwB8krmu+ciWO/G+c3S2tCanmV1hoLpa6uoKuiRGV5cZoFJVFXRJACB4hYWmnz5blgHu7jabJBEGhqApU7KnosViZidDwgAAmFkERUVm0F426O42N5CWsCsMnHaaGTOQDeMGOjqkyZOzZ7AMAATJcczqsNkSBqTMbZ+cBewKAxMm/G1+f5A8z3xMmRJsOQAgm1RVmTEDQY/tam833bhlZcGWI4PsCgPjxklnnmlWuQrS7t2m0s+ZE2w5ACCbjB5tLsBBr7+ye7c0dqzpyrWEXWHAcaQFC0w3QW9vMGXwfam1VZo716qKBgDHFY2a7tPW1uDK0Lf2y4QJwZUhAHaFAUmaNcskvqC2D96zRyoulubNC+b4AJDNTj/dDCQMKhDs3CmNHCmNGhXM8QNiXxjIz5duuslMF8n0jlTxuNmV64orTPoFABysokI6+2yppcWsHJtJ+/ebtQVmzpRycjJ77IDZFwYk6VOfki6/3OxXnal1p33f7Jo4dap0ww3MIgCAo5k+3bQQbN+euWMmk2ZjohkzpLq6zB03S9gZBhzHtA5MmCA1NGRmxavt281MhltvNU1gAIAjy801XbrRaGZ2dk2lzM3aaaeZVgkL2RkGJDN47x//0Yxe/fDD9E1l8X0TBHxfuvNO6Zxz0nMcABhKamqkiy825850biXsedLmzWaBoUsuMV3JFrI3DEjS+PHS175mmoQ++GDwVyf0PGnTJtMSceed0vz5g/v8ADCUjR9vLtCS1Ng4+DdtPT3mHF1dLV16qdUzvOwOA5IZyPf1r5sBI1u2mCapwVihsK1NWr/epNv77zeDBhknAAAnZsIEMyW8okLasMEsCHSqfN+sN7N9u7kGzJ9vnt9i4aALkBXGjJEeekj6z/+U/uM/pHXrzKJAw4ef2BbDvm9GozY1SeGwCQBf+pL1lQwATsno0eauvb5eWrvWLApUWWmmaZ+IVMosaNTaKpWWSpddZsJAmEsh70Cf3Fzp2mulc8+Vfv1r6c03zZ19NGoqXFGR2fnw0Lv7ZNLsMxCLmdaA4mLp/POlxYvNCoO0BgDAqSsoMDPB+rp1GxvNWILiYjM4Oxo98kW9t9fsEhuLmc/l5WZw4uTJVncLHIowcKgJE6T77jPT//7rv6Tf/95UuO3bzZxXxzEtAH2fQyFTEcvLpUWLTP/WxImEAAAYbI5jwkBdnVnAbcsWM/gvFjPrEhw6psD3zU1cQYHpsp0wwfzbwsJgyp/FCANHM2KE9LnPSZ/9rGn637bNBIKODhMKXNfsvT1qlGnCqqo6sS4FAMDJGz7cfJx3ntnpsK3NjCdIJv92oxaJSCUlpksgLy/oEmc1wsDxOI6pSKWlZiEMAED2cBxzp8/d/inhVhYAAMsRBgAAsBxhAAAAyxEGAACwHGEAAADLEQYAALAcYQAAAMsRBgAAsBxhAAAAyxEGAACwHGEAAADLEQYAALAcYQAAAMsRBgAAsBxhAAAAyxEGAACwHGEAAADLEQYAALAcYQAAAMsRBgAAsBxhAAAAyxEGAACwHGEAAADLhYMugOd5B33G4PM8z7y/Xor3OY3M+5zq/7sc3ut0oD5nBvU5M/rrc8ACDQOe56m+vr7/a9d1AyzN0GXe5z9LqT2SI7khGoTSwUulVP+n9eaL8Gty3fxgCzREUZ8zg/qcGQdeBxcuXBjYdZDfIms4QRfAMvxqpRf1ObOoz0Od4/u+f7wfam9vV0lJifbv36/i4uJBLUA8HpdEq0C6eZ4n+XG57nH/u3EKTHNfWG6Yu6h0oj5nBvU5M/q6CSKRyKA/90Cv34GPGUjHi8fhTNjivU43N/DfKDtQnzOD+pwZ2XAzTNsPAACWIwwAAGA5wgAAAJYjDAAAYDnCAAAAlhvQWNG+2Yft7e1pLQwAABg8fdft460iMKAwEIvFJEm1tbWnWCwAAJBpsVhMJSUlR318QIsOpVIp7dq1S0VFRXIcVv4CAOCTwPd9xWIx1dTUKHSMpbsHFAYAAMDQxQBCAAAsRxgAAMByhAEAACxHGAAAwHKEAQAALEcYAADAcoQBAAAs9/8B1TGhS1Omy9EAAAAASUVORK5CYII=",
      "text/plain": [
       "<Figure size 640x480 with 1 Axes>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[(4, 0), (4, 1)]\n",
      "Taking move: [(1, 0), (1, 1)]\n",
      "[(4, 0), (4, 1)]\n",
      "Taking move: [(2, 0), (2, 1)]\n",
      "[(4, 0), (4, 1)]\n",
      "Taking move: [(3, 0), (3, 1)]\n",
      "[(4, 0), (4, 1)]\n",
      "Taking move: [(4, 0), (4, 1)]\n",
      "All robots reached their goal.\n"
     ]
    }
   ],
   "source": [
    "def run_sim(n_robots,l_corridor):\n",
    "    grid_n = l_corridor\n",
    "    grid_m = n_robots\n",
    "\n",
    "    # Initialize the robots\n",
    "    robots = []\n",
    "    for i in range(n_robots):\n",
    "        robots.append(Robot(\"r\"+str(i), (0, i), (l_corridor-1, i)))\n",
    "\n",
    "    plot_grid_world(l_corridor, n_robots, robots)\n",
    "\n",
    "    num_iter = l_corridor * 3 # estimated maximum time steps that it might take\n",
    "\n",
    "    # Get the contracts ensuring no conflicts\n",
    "    if n_robots > 1:\n",
    "        c_collision = get_collision_contract(robots)\n",
    "        c_swapping = get_swapping_contract(robots)\n",
    "        c_no_conflicts = c_collision.merge(c_swapping)\n",
    "\n",
    "    t_0 = 0\n",
    "\n",
    "    for _j in range(0, num_iter):  # noqa: WPS122\n",
    "        # merge the dynamics contracts\n",
    "\n",
    "        dynamics_contract = get_dynamics_contract_robot(robots[0].name, robots[0].pos, t_0, grid_n, grid_m)\n",
    "        for robot in robots[1:]:\n",
    "            contract = get_dynamics_contract_robot(robot.name, robot.pos, t_0, grid_n, grid_m)\n",
    "            dynamics_contract.merge(contract)\n",
    "\n",
    "        # merge dynamics with the no conflict contracts\n",
    "        if n_robots > 1:\n",
    "            multiagent_contract = dynamics_contract.merge(c_no_conflicts)\n",
    "        else:\n",
    "            multiagent_contract = dynamics_contract\n",
    "\n",
    "        moves_list, t_1 = find_move_candidates_general(grid_n, grid_m, robots, t_0, multiagent_contract)\n",
    "        goals = [robot.goal for robot in robots]\n",
    "        print([(goal.x, goal.y) for goal in goals])\n",
    "\n",
    "        move = strategy_multiple_simple(moves_list, goals)\n",
    "        print('Taking move: {}'.format(move))\n",
    "\n",
    "        for i,robot in enumerate(robots):\n",
    "            robot.move(move[i])\n",
    "\n",
    "        if distance([[robot.pos.x, robot.pos.y] for robot in robots], [robot.goal for robot in robots]) == 0:\n",
    "            print('All robots reached their goal.')\n",
    "            break\n",
    "            \n",
    "# Define the number of robots and grid size\n",
    "n_robots = 2\n",
    "l_corridor = 5\n",
    "run_sim(n_robots,l_corridor)"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.9.13"
  },
  "vscode": {
   "interpreter": {
    "hash": "b282b3e35ff361393169c4f355db145ffcb63e574f57c9818c827b7c99ca9fc3"
   }
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}