high-level-monitor.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "aff9595e-a7ab-453b-a3ef-529898fd3061",
   "metadata": {},
   "source": [
    "# Set up"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "14c12caa-757a-4678-94e7-6375cd9eb81f",
   "metadata": {
    "tags": []
   },
   "outputs": [],
   "source": [
    "# Let us install timing extensions\n",
    "try:\n",
    "    %load_ext autotime\n",
    "except:\n",
    "    !pip install ipython-autotime\n",
    "    %load_ext autotime"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "18c7d4fb-8349-47af-b979-e5f9957ebe41",
   "metadata": {},
   "source": [
    "### Dependencies: \n",
    "graph_tool, networkx, spot, toytree, toyplot, cvxopt, skunk"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "573dfc69-6b64-41ee-aee2-1e0d05830dff",
   "metadata": {
    "tags": []
   },
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "\n",
      "(ipykernel_launcher.py:44476): Gtk-WARNING **: 13:02:05.200: Locale not supported by C library.\n",
      "\tUsing the fallback 'C' locale.\n"
     ]
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "time: 4.68 s\n"
     ]
    }
   ],
   "source": [
    "from src.workspace import *\n",
    "from src.high_level_monitor import *\n",
    "from src.low_level_monitor import *\n",
    "from src.predictive_intent_tree import *\n",
    "from src.buchi import *\n",
    "from src.himo import *\n",
    "from src.buchi_with_AP import *\n",
    "\n",
    "import numpy as np\n",
    "import skunk\n",
    "import graph_tool.all as gt\n",
    "import time\n",
    "import matplotlib as mpl \n",
    "# mpl.use('cairo') \n",
    "import matplotlib.pyplot as plt\n",
    "import scipy.optimize as sp\n",
    "from collections import deque \n",
    "import toytree\n",
    "import toyplot\n",
    "import networkx as nx"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1aa55f91-ac6b-47c4-9dcc-f10aa5d80e32",
   "metadata": {},
   "source": [
    "### Map setting\n",
    "- In this version, MAP_SIZE 'x' and 'y' should be the same.\n",
    "- Starting position (0,0) is the left bottom of the map."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "474687f2-6bcd-4041-a9ea-b5a39b1086b1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "time: 481 µs\n"
     ]
    }
   ],
   "source": [
    "NUM_REGIONS = 7\n",
    "MAP_SIZE, start_position = {'x': 10, 'y': 10}, (0, 0)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3131e733-9aae-4638-b0bb-751619cba554",
   "metadata": {},
   "source": [
    "### Workspace\n",
    "- Regions are randomly generated."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "9d3ebed6-8518-44a7-ae10-91b1c9f93bb2",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "time: 5.67 ms\n"
     ]
    }
   ],
   "source": [
    "ws = Workspace(MAP_SIZE, NUM_REGIONS, start_position)\n",
    "# ------------------------------------------------------------------\n",
    "# Useful vars\n",
    "#     ws.region: coordinates of regions\n",
    "#     ws.region_idx: cell indices of regions\n",
    "# ------------------------------------------------------------------"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9bc4bd22-b6fd-4770-900c-6aaaeaa9970c",
   "metadata": {},
   "source": [
    "- Or the user can manually define regions: **Workspace(MAP_SIZE, NUM_REGIONS, start_position, region = [(a, b), (c, d), ...])**"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "7ab2799f-f8d5-4214-899c-ea1a40224cb1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "time: 4.54 ms\n"
     ]
    }
   ],
   "source": [
    "# # region = [(4, 1), (4, 3)]\n",
    "# # region = [(1, 4), (4, 4), (4, 0)]\n",
    "# region = [(1, 2), (5, 9), (8, 9)]\n",
    "region = [(1, 6), (2, 9), (5, 6), (8, 3), (9, 8)]\n",
    "NUM_REGIONS = len(region)\n",
    "ws = Workspace(MAP_SIZE, NUM_REGIONS, start_position, region = region)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c1bc3edb-cefb-4e2f-9000-e70f0b983384",
   "metadata": {},
   "source": [
    "### Hypothetical missions\n",
    "- LTL formulas for 'patrol', 'avoid', and 'patrol_while_avoid' missions can be automatically generated using region indices in each list. For example, if **['patrol', 0, 1]** is given to the monitor, **G (F p0 & F p1)** will be added to the intent set."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "cd4b30d2-d01c-452c-80d3-cd9b25a43fda",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "time: 729 µs\n"
     ]
    }
   ],
   "source": [
    "patrol = ['patrol', 0, 1]\n",
    "sequenced_patrol = ['seq_patrol', 1, 0]\n",
    "ordered_patrol = ['ord_patrol', 1, 0]\n",
    "avoid = ['avoid', 2]\n",
    "patrol_while_avoid = ['patrol_while_avoid', patrol, avoid]\n",
    "sequenced_patrol_while_avoid = ['seq_patrol_while_avoid', sequenced_patrol, avoid]\n",
    "ordered_patrol_while_avoid = ['ord_patrol_while_avoid', ordered_patrol, avoid]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "25fcf46c-61f9-4a54-a47a-8badff5356bc",
   "metadata": {
    "tags": []
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "time: 511 µs\n"
     ]
    }
   ],
   "source": [
    "# LTL_formula = ['F p0 & F p1', patrol_while_avoid]\n",
    "# LTL_formula = [ordered_patrol, ['patrol', 2, 0]]\n",
    "LTL_formula = [['patrol_while_avoid', ['patrol', 0, 1, 2], ['avoid', 3, 4]]]\n",
    "# LTL_formula = ['F (p0 & (F p1 & F p2))']\n",
    "# LTL_formula = ['FG p0', 'F p0', 'G!p1', 'G!p2']\n",
    "# LTL_formula = ['G(F p3 & Fp1 & Fp2)']"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "16ca0b23-e466-4399-92db-93b785aca00a",
   "metadata": {
    "tags": []
   },
   "source": [
    "### Monitor"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "96524629-0768-4c53-ba5b-2caf5e74c2b5",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Regions:  [(1, 6), (2, 9), (5, 6), (8, 3), (9, 8)]\n",
      "-------------------------------------------------------------------\n",
      "LTL: probability\n",
      "\n",
      "0- 1: 0.5\n",
      "1- (F p0 & F p1 & F p2) & G ! p3 & G ! p4: 0.5\n",
      "-------------------------------------------------------------------\n",
      "AP(immediate): probability\n",
      "\n",
      "0: 0.39569960478213084\n",
      "1: 0.2533008222219106\n",
      "2: 0.13764201736596107\n",
      "3: 0.08554208466029181\n",
      "4: 0.12781547096970564\n",
      "-------------------------------------------------------------------\n"
     ]
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAxEAAAKvCAYAAAAV0ELXAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjUuMSwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/YYfK9AAAACXBIWXMAAAsTAAALEwEAmpwYAAAoo0lEQVR4nO3df7DldX0f/ueLy/JrL6IjKJEfATLEyBQF3bgqaRs1CaxhNN9Oa8CvJNJYxqm/muk0sU6jaU1bO2l+aLVhGH/HDBSJky+hrLQzJb9IsrLIRgQ04uIXFkShrcquwP7g3T/Obrksu/u5537u3c895zweM2d2P+d87ue+xOvKc1/PzznVWgsAAMBiHTH0AAAAwGQRIgAAgLEIEQAAwFiECAAAYCxCBAAAMBYhAgAAGIsQAQAAU6yqPlFV36mqrxzk9aqqD1fVPVX15ap6adc1hQgAAJhun0py0SFe35Dk7L2PK5L8XtcFhQgAAJhirbU/S/K/DnHKG5J8po38dZJnV9UPHeqaRy7ngPuceOKJ7YwzzliJSzNBnnzyyaFHWBWOOEJWB4D9ffOb38wjjzxSQ8/RV1W1oWdIcmeSxxccX9Vau2qMrz8lyf0Ljrftfe5bB/uCFQkRZ5xxRjZv3rwSl2aCbN++fegRVoX5+fmhRwCAVWfdunVDjzBNHm+t9fkHeqAwd8hw5K9IAQBgtm1LctqC41OTPHioLxAiAACgh6oa9LEMrk/yC3vfpekVSb7XWjtolSlZoToTAACwOlTV1Ul+MsmJVbUtyfuTrEmS1tqVSW5M8rok9yT5QZLLu64pRAAAwBRrrV3a8XpL8vZxrilEAABAD8tUKVqyUQY4vNwTAQAAjMUmAgAAehh6EzEEmwgAAGAsQgQAADAWdSYAAOhBnQkAAKCDTQQAACzRMn5q9ESxiQAAAMYiRAAAAGNRZwIAgB7UmQAAADrYRAAAQA82EQAAAB2ECAAAYCzqTAAA0IM6E0yhb3zjG3nXu96VV77ylTnhhBOyYcOGoUcCAJhoNhFMpC1bfiS7d39nUef+xV8kN9yQnHNOcuqpyaOP/kU2bz7+aecceeTzct5531iJUQGAKTeLmwghgom02ACRJK96VfITPzH6/fvfn3zve/2uBwAw69SZmHpH+CkHAFhWNhEAALBEVTWTdSZ/RwsAAIxFiAAAAMaizgQAAD2oMwEAAHSwiQAAgB5mcRMhRDD1Hn882bRp9PtHHkl27Ej+9E9Hx+vXJ8ccM9xsAACTSIhg6n33u8mv//rTn9t3fPXVycknH+aBAAAmnBDB1Dv55OTmm4eeAgCYVrNYZ3JjNQAAMBabCAAA6MEmAgAAoIMQAQAAjEWdCQAAlqiq1JkAAAC62EQAAEAPNhEAAAAdhAgm0pFHPm9VXw8AYJqpMzGRzjvvG0OPAACQRJ0JAACgk00EAAD0YBMBAADQQYgAAADGos4EAAA9qDMBAAB0sIkAAIAlqiqbCAAAgC5CBAAAMBZ1JgAA6EGdCQAAoIMQAQAAjEWdCQAAelBnAgAA6GATAQAAPdhEAAAAdBAiAACAsagzAQBAD+pMAAAAHWwiAABgiapqJjcRQgQr5rHHHhv0++/7H3RrbdA55ufnB/3+AADLTZ0JAAAYi00EAAD0MIt1JpsIAABgLDYRAADQg00EAABAByECAAAYizoTAAD0oM4EAADQwSYCAAB6sIkAAADoIEQAAABjUWcCAIAlqip1JgAAgC42EQAA0INNBAAAQAchAgAAGIs6EwAA9KDOBAAA0EGIAAAAxqLOBAAAPagzAQAAdBAiAADIAw88kPn5+VRVtm/fPvQ4E2Xfp1YP9RiCOhMAwJS45ZaTs2vXt5f0tR/4QHLUUcmOHcmf//nxOfbYZM2a5+eCCx5a5imZBjYRAABTYqkB4stfTm69Nfn5n1+e6zH9bCIAAGbYnj3Jhz+c/MIvJPPzQ08zeYasFA3JJgIAYIZdf32yc2fycz839CRMEpsIAIAZ9b3vJZ/8ZPLe9yZH+rfCJbOJAABgZnz848mLXpS84hVDT8KkESIAAGbQvfcmGzcmv/iLyfbto8fjj49e2749eeKJYedjdVvU4qqqfjnJW5O0JHckuby19vhKDgYAwMp54IFk9+7k7W9/5mtvfGPyutcl/+JfHP65JtEs1pk6Q0RVnZLkXUnOaa09VlXXJrkkyadWeDYAAFbIuecmv/M7T3/ui19Mrr46+eAHkx/6oWHmYjIs9haaI5McW1W7khyX5MGVG4lpMXQqH/r7A8BqdsIJyXnnPf25h/Z+rtyLX5wce+xhH2lizeK/c3TeE9FaeyDJf0xyX5JvJflea+2/7X9eVV1RVZuravPDDz+8/JMCAACrQmeIqKrnJHlDkjOTvCDJ2qp68/7ntdauaq2ta62tO+mkk5Z/UiZOa82jtaH/awCARbvoouTmm20h6LaYOtNPJbm3tfZwklTV55O8KslnV3IwAACYBOpMB3ZfkldU1XE1+if02iR3r+xYAADAatW5iWitbaqq65J8KcnuJLcnuWqlBwMAgNWuqmZyE7God2dqrb0/yftXeBYAAGAC+MRqAABgLIv9nAgAAOAAZrHOZBMBAACMRYgAAADGos4EADAl1qx5fnbt+vayXo9us1hnEiIAAKbEBRc8NPQIzAghAgAAepjFTYR7IgAAgLEIEQAAwFjUmQAAoAd1JgAAgA42EQAAsERVZRMBAADQRYgAAADGos4EAAA9qDMBAAB0sIkAAIAebCIAAAA6CBEAAMBY1JkAAKAHdSYAAIAONhEAANCDTQQAAEAHIQIAABiLEAEAAEtUVYM/FjHjRVX1taq6p6rec4DXT6iqP66qv6mqO6vq8q5rChEAADClqmouyUeTbEhyTpJLq+qc/U57e5K7WmsvSfKTSX6rqo461HXdWA0AAD2s8hurX57kntba1iSpqmuSvCHJXQvOaUmOr9F/kPkk/yvJ7kNdVIhgxRxzzDFDjwAAMAtOrKrNC46vaq1dtff3pyS5f8Fr25Ks3+/rP5Lk+iQPJjk+yc+31p481DcUIgAAYLI90lpbd5DXDrQmafsdX5hkS5LXJPmRJP+9qv68tfb9g31DIQIAAHpY5XWmbUlOW3B8akYbh4UuT/LB1lpLck9V3Zvkx5J88WAXdWM1AABMr1uTnF1VZ+69WfqSjKpLC92X5LVJUlXPT/LCJFsPdVGbCAAAmFKttd1V9Y4kNyWZS/KJ1tqdVfW2va9fmeQDST5VVXdkVH/61dbaI4e6rhABAAA9rPI6U1prNya5cb/nrlzw+weT/Mw411RnAgAAxmITAQAAPaz2TcRKsIkAAADGIkQAAABjUWcCAIAlqip1JgAAgC42EQAA0INNBAAAQAchAgAAGIs6EwAA9KDOBAAA0MEmAgAAerCJAAAA6CBEAAAAY1FnAgCAHtSZAAAAOthEAADAElWVTQQAAEAXIQIAABiLOhMAAPSgzgQAANDBJgIAAHqwiQAAAOggRAAAAGNRZwIAgB7UmQAAADoIEQAAwFjUmQAAoAd1JgAAgA42EQAAsERVZRMBAADQRYgAAADGos4EAAA9qDMBAAB0sIkAAIAebCIAAAA6CBEAAMBY1JkAAKAHdSYAAIAONhEAANCDTQQAAEAHIQIAABiLOhMAACxRVakzAQAAdLGJAACAHmwiAAAAOggRAADAWNSZAACgB3UmAACADjYRAADQg00EAABAByECAAAYizoTAAD0oM4EAADQQYgAAADGos4EAABLVFXqTAAAAF1sIgAAoAebCAAAgA42EayY3bt3Dz0Cq8T27duHHmFw8/PzQ48AAMtGiAAAgB7UmQAAADrYRAAAQA82EQAAAB2ECAAAYCzqTAAA0IM6EwAAQAebCAAAWKKqsokAAADoIkQAAABjUWcCAIAe1JkAAAA62EQAAEAPNhEAAAAdhAgAAGAs6kwAANCDOhMAAEAHIQIAABiLOhMAACxRVakzAQAAdLGJAACAHmwimDp33XVXXvva1+a4447LC17wgrzvfe/Lnj17hh4LGMDnPve5vP71r88pp5yS+fn5vOxlL8vVV1899FgATCCbiAlzyy0nZ9euby/q3EcfTS6/PPnhH07+zb9JHnzwsfzmb34g9977gfzSL43OWbPm+bnggodWcGJgJY3zZ8Kv/3py8snJW9+anHBCsmnTl/KmN70pf/VXb8o/+Aejc/yZAMBiCBETZrH/spAk11+fPPHEKECsXTt6bseO5NOfTi65ZPTcONcDVp9x/jf87/7dKDzs89KXJo88knzuc/m/IcKfCQDjU2diqnzxi8mP//hTASJJXvOaUbD4m78Zbi5gGAsDxD5nn51897uHfRQAJpwQMcXuuy85/fSnP/f85yfHHDN6DeDOO0eVRwCWbt/bvA71GIIQMcUefTSZn3/m8/Pzo9eA2XbbbckttyQ/93NDTwLApBEiZtQMVveABR56KPm3/za54ILkoouGngaASePG6il2/PGjG6n3t337gTcUwGz4/veTX/3V5HnPS9773qGnAZh8bqw+iKp6dlVdV1Vfraq7q+qVKz0Y/Z1++jPvffjOd5LHH3/mvRLAbHj88VFw2L07+ff/Pjn22KEnAmASLXYT8aEkX2it/cOqOirJcSs4E8vk5S9P/st/SX7wg+S4vf+N3XxzcvTRyUteMuxswOG3Z8/osyK2bUv+039KnvOcoScCmHxD3tw8pM5NRFU9K8nfS/LxJGmt7WytfXeF52IZvP71yZo1yfveN7qB8o//OPnUp5J/9I+e/ravwGz4nd9JNm1KLrts9OYKd9311GPnzqGnA2CSLGYTcVaSh5N8sqpekuS2JO9urT2tbV9VVyS5IklO15VZFY4/Pvmt30o+/OFRfWF+fhQgfvEXh54MGMLmzaNfP/KRZ7529dWjT7MGgMVYTIg4MslLk7yztbapqj6U5D1Jfm3hSa21q5JclSTr1q1ryz0oS3PGGclv//bQUwCrwTXXDD0BwHRSZzqwbUm2tdY27T2+LqNQAQAAzKDOTURr7aGqur+qXtha+1qS1ya5a+VHAwCA1W8WNxGLfXemdyb5g73vzLQ1yeUrNxIAALCaLSpEtNa2JFm3sqMAAACTwCdWAwBAD7NYZ1rUJ1YDAADsYxMBAAA92EQAAAB0ECImzJo1z1/V1wMOL38mADAEdaYJc8EFDw09ArCK+DMBYFhVpc4EAADQRYgAAADGos4EAAA9qDMBAAB0sIkAAIAebCIAAAA6CBEAAMBY1JkAAKAHdSYAAIAONhEAANCDTQQAAEAHIQIAABiLOhMAACxRVakzAQAAdLGJAACAHmwiAAAAOggRAADAWIQIAADoYd/N1UM9FjHfRVX1taq6p6rec5BzfrKqtlTVnVX1p13XdE8EAABMqaqaS/LRJD+dZFuSW6vq+tbaXQvOeXaS/5zkotbafVX1vK7rChEAANDDKr+x+uVJ7mmtbU2SqromyRuS3LXgnDcl+Xxr7b4kaa19p+uiQgQr5jnPec7QI7BKtNaGHgEAptmJVbV5wfFVrbWr9v7+lCT3L3htW5L1+339jyZZU1V/kuT4JB9qrX3mUN9QiAAAgMn2SGtt3UFeO9CaZP+/3TsyycuSvDbJsUn+qqr+urX2twf7hkIEAAD0sMrrTNuSnLbg+NQkDx7gnEdaazuS7KiqP0vykiQHDRHenQkAAKbXrUnOrqozq+qoJJckuX6/c/6/JH+3qo6squMyqjvdfaiL2kQAAMASLfZtVofSWttdVe9IclOSuSSfaK3dWVVv2/v6la21u6vqC0m+nOTJJB9rrX3lUNcVIgAAYIq11m5McuN+z1253/FvJvnNxV5TnQkAABiLTQQAAPSwmutMK8UmAgAAGIsQAQAAjEWdCQAAelBnAgAA6GATAQAAPdhEAAAAdBAiAACAsagzAQBAD+pMAAAAHWwiAABgiarKJgIAAKCLEAEAAIxFnQkAAHpQZwIAAOhgEwEAAD3YRDC57rgj+af/NHnRi5Kjj06qRr++6EWj5++4Y+gJAQCYEjYRk27r1uSyy5ItW5Innkj27HnqtZ07k69+Nfn615NPfzo577zk938/OeusoaYFAGAK2ERMsmuvTc49N9m0KfnBD54eIBbas2f0+qZNo/OvvfbwzgkAMMX2fVbEUI8h2ERMqmuvTd7yluSxxxb/NfvCxFveMjp+4xtXYjIAAKacTcQk2ro1ufzy8QLEQo89Nvr6e+9d3rkAAGbQLG4ihIhJdNllo/sf+njiieTNb16eeQAAmClCxKT58pdHN1Ef7P6HxdqzJ7n9du/aBADA2ISISXPllYfeQhxxRPKzP5v8q381+vWIQ/xXvHPn6HoAACzJ0FUmN1azODfffPAtxBFHJDfdlKxfnxx33FPvyHThhcmTTz7z/D17RtcDAIAx2ERMmq1bD/7ahg2jAHH88cnc3OjX9etHzx/MN76x/DMCADDVhIhJs3PnwV87//zRBmKh444bfcjcwezatSxjAQDMqlmsMwkRk+aoow7+2u23jypMC/3gB6MbsQ9mzZplGQsAgNkhREyas846+GsbN47ugXj00dH9Do8+OjreuPHgX/MjP7L8MwIAzJBZ3ES4sXrSvPrVyde/fuCbq598cnQT9YYNowrTli2jAHGgm6qT0X0Tr371Sk4LAMAUEiImzdvelnz608+sLe3z5JPJf/2vo0eXo44aXQ8AAMagzjRpXvzi0ZZhbq7fdebmRjdin3vusowFADCrZrHOJERMot///f43RB99dPLZzy7PPAAAzBR1pkn0ve+NNglVSWvjf/2xxyaf/GRy5pnLPxsAwIwZahswJJuISXP77clP/VTy3OcmH/rQ6HMgFlttmpsbnf+pTyVvfOOKjgkAwPQSIibJvgAxP5/cfHPyzncmd9wx+lTqY489eJiYmxu9vn598pWvCBAAAPSizjQp9g8Q+z4v4qyzkltuGYWJK68cvfaNb4w+iXrNmtHnQLz61aN3YXITNQDAshry5uYhCRGT4GABYqFzz00++tHDPxsAADNHiFjtFhMgAAAYzCxuItwTsZoJEAAArEJCxGolQAAAsEqpM61GAgQAwMRQZ2J4AgQAAKucTcRqIkAAAEwcmwiGI0AAADAhhIjVQIAAAGCCqDMNTYAAAJho6kwcXgIEAAATyCZiKAIEAMDEqyqbCA4TAQIAgAkmRBxuAgQAABNOnelwEiAAAKaOOhMrR4AAAGBKCBGHgwABAMAUUWdaaQIEAMBUU2dieQkQAABMIZuIlSJAAADMBJsIlocAAQDAFBMilpsAAQDAlFNnWk4CBBzQ8ccfP/QIALBi1JlYOgECAIAZYROxHAQIAICZVFU2ESyBAAEAwIwRIvoQIAAAmEHqTEslQAAAEDdWs1gCBAAAM8wmYlwCBAAAC9hEcGgCBAAACBGLJkAAAEASdabFESAAADgIdSaeSYAAAICnsYk4FAECAIAONhE8RYAAAIADEiIORIAAAICDUmfanwABAMAiVZU608wTIAAAoJNNxD4CBAAAS2ATMasECAAAWDQhQoAAAICxzHadSYAAAKAndaZZIkAAAMCSzGaIECAAAGDJZq/OJEAAALCM1JmmnQABAAC9zc4mQoAAAGAF2ERMKwECAACWzfSHCAECAACW1XTXmQQIAABWUFXNZJ1p0SGiquaSbE7yQGvt4pUbqYc9e5KNG0fh4VnPSv71v06OP16AAACAZTTOJuLdSe5O8qwVmqWfPXuSCy9MNm1KduxIWkuOPnp0LEAAALBCZnETsah7Iqrq1CQ/m+RjKztODxs3jgLD9u2jAJEkc3PJ17427FwAADBlFntj9e8m+ZUkTx7shKq6oqo2V9Xmhx9+eDlmG8/tt482EAs99liyZcvhnwUAAKZYZ4ioqouTfKe1dtuhzmutXdVaW9daW3fSSSct24CLdv75ydq1T39u7drkvPMO/ywAAMyMfTdXD/UYwmI2ERckeX1VfTPJNUleU1WfXdGplmLDhmT9+mTNmtHx/PzoeMOGYecCAIAp0xkiWmv/srV2amvtjCSXJPkfrbU3r/hk45qbS266aRQajj46ufrq0fHc3NCTAQAwxWZxEzFdnxMxNzd6J6ajj04uXp3vQgsAAJNurBDRWvuTJH+yIpMAAAATYbo2EQAAcJj5nAgAAIAONhEAALBEQ97cPCSbCAAAYCxCBAAAMBZ1JgAA6EGdCQAAoIMQAQAAjEWdCQAAelBnAgAA6GATAQAAPdhEAAAAdBAiAACAsagzAQBAD+pMAAAAHWwiAABgiarKJgIAAKCLEAEAAIxFnQkAAHpQZwIAAOhgEwEAAD3YRAAAAHQQIgAAgLGoMwEAQA/qTAAAwFSpqouq6mtVdU9VvecQ5/14Ve2pqn/YdU2bCAAA6GE1byKqai7JR5P8dJJtSW6tqutba3cd4Lz/kOSmxVzXJgIAAKbXy5Pc01rb2lrbmeSaJG84wHnvTPKHSb6zmIsKEQAAMNlOrKrNCx5XLHjtlCT3Lzjetve5/6uqTkny/yS5crHfUJ0JAACWqKpWQ53pkdbauoO8dqDh2n7Hv5vkV1trexb7n0WIAACA6bUtyWkLjk9N8uB+56xLcs3eAHFiktdV1e7W2h8d7KJCBAAA9LAKNhGHcmuSs6vqzCQPJLkkyZsWntBaO3Pf76vqU0luOFSASIQIAACYWq213VX1jozedWkuySdaa3dW1dv2vr7o+yAWEiIAAGCKtdZuTHLjfs8dMDy01t6ymGsKEQAA0MMqrzOtCG/xCgAAjEWIAAAAxqLOBAAAPagzAQAAdLCJAACAHmwiAAAAOggRAADAWNSZAABgiapKnQkAAKCLTQQAAPRgEwEAANBBiAAAAMaizgQAAD2oMwEAAHQQIgCAmXPdddflVa96VZ773OfmmGOOyQtf+ML8xm/8Rnbu3Dn0aEygfW/zOtRjCOpMAMBUuOWWk7Nr17cXde5f/mVy1lnJhg3J/Hzy1a/+bT7wgV/Lbbf9Wt797tE5a9Y8Pxdc8NAKTgyTS4gAAKbCYgNEkrz+9U8/Pv/8ZMeO5I/+KHnXu5Kq8a4Hs0aIAABI8qxnJbt3Dz0Fk2ZWP7FaiAAAZtaePcmuXcnXv558/vOjDcUM/vsgjE2IAABm1oYNoxCRJD/zM8nb3jbsPEwmmwgAgBnykY8kTzyR3H138pnPJB/6UPLLvzz0VLD6CREAwMz60R8d/XruuckJJyQf/GDyxjcmp5wy7Fyw2k3X50Ts2ZNs3Tr6K4UbbhgdAwAswr5A8ZB3dWVMs/g5EdMTIvbsSS68MNm4cRQiLr10dCxIAACLcMcdo19PPnnYOWASTE+daePGZNOmp+6O2r59dLxxY3LxxcPOBgCsKr/yK8nLXpaccUZyxBHJV76SXHtt8upXqzIxPjdWT7Lbbx99SsxCO3YkW7YIEQDA0/zYjyVf+MKoujQ3l7zgBck/+SfP/BA64MCmJ0Scf36ydu1oA7HP2rXJeecNNhIAsDr94388egBLMz33RGzYkKxfn6xZMzqenx8db9gw7FwAAEw1N1ZPsrm55KabRqHh6KOTq68eHc/NDT0ZAABMlempMyWjwHDWWaMQ4T4IAABYEdMVIgAA4DAaslI0pOmpMwEAAIeFTQQAAPRgEwEAANBBiAAAAMaizgQATIU1a56fXbu+vazXg8WYxTqTEAEATIULLnho6BFgZggRAADQwyxuItwTAQAAjEWIAAAAxqLOBAAAPagzAQAAdLCJAACAJaoqmwgAAIAuQgQAADAWdSYAAOhBnQkAAKCDTQQAAPRgEwEAANBBiAAAAMaizgQAAD2oMwEAAHSwiQAAgB5sIgAAADoIEQAAwFjUmQAAYImqSp0JAACgixABAACMRZ0JAAB6UGcCAADoYBMBAAA92EQAAAB0ECIAAICxqDMBAEAP6kwAAAAdbCIAAKAHmwgAAIAOQgQAADAWdSYAAFiiqlJnAgAA6GITAQAAPdhEAAAAdBAiAACAsagzAQBAD+pMAAAAHWwiAACgB5sIAACADkIEAAAwFnUmAADoQZ0JAACggxABAACMRZ0JAACWqKrUmQAAALrYRAAAQA82EQAAAB2ECAAAYCzqTAAA0IM60wFU1WlVdXNV3V1Vd1bVuw/HYAAAwOq0mDrT7iT/vLX2oiSvSPL2qjpnZcdaoj17kq1bkyeeSG64YXQMAAAraN/bvA71GEJniGitfau19qW9v380yd1JTlnpwca2Z09y4YXJxo2jEHHppaNjQQIAAJbVWDdWV9UZSc5PsmlFpulj48Zk06Zk167R8fbto+ONG4edCwAApsyiQ0RVzSf5wyT/rLX2/QO8fkVVba6qzQ8//PByzrg4t9+e7Njx9Od27Ei2bDn8swAAMDPUmQ6iqtZkFCD+oLX2+QOd01q7qrW2rrW27qSTTlrOGRfn/POTtWuf/tzatcl55x3+WQAAYIot5t2ZKsnHk9zdWvvtlR9piTZsSNavT9asGR3Pz4+ON2wYdi4AAKbW0FuI1byJuCDJZUleU1Vb9j5et8JzjW9uLrnpplFoOPro5OqrR8dzc0NPBgAAU6Xzw+Zaa3+RZDI+QWNuLjnrrFGIuPjioacBAICp5BOrAQCgB59YDQAA0MEmAgAAerCJAAAA6CBEAAAAY1FnAgCAHtSZAAAAOthEAABADzYRAAAAHYQIAABgLOpMAACwRFWlzgQAANBFiAAAAMaizgQAAD2oMwEAAHSwiQAAgB5sIgAAADoIEQAAwFjUmQAAoAd1JgAAgA42EQAA0INNBAAAQAchAgAAGIs6EwAALFFVqTMBAADTpaouqqqvVdU9VfWeA7z+/1bVl/c+/rKqXtJ1TZsIAADoYTVvIqpqLslHk/x0km1Jbq2q61trdy047d4kf7+19r+rakOSq5KsP9R1bSIAAGB6vTzJPa21ra21nUmuSfKGhSe01v6ytfa/9x7+dZJTuy4qRAAAwGQ7sao2L3hcseC1U5Lcv+B4297nDuaXkmzs+obqTAAA0MMqqDM90lpbd5DXDjRcO+CJVa/OKET8RNc3FCIAAGB6bUty2oLjU5M8uP9JVfXiJB9LsqG19j+7LipEAABAD6tgE3EotyY5u6rOTPJAkkuSvGnhCVV1epLPJ7mstfa3i7moEAEAAFOqtba7qt6R5KYkc0k+0Vq7s6retvf1K5O8L8lzk/znvYFo9yHqUUmECAAAmGqttRuT3Ljfc1cu+P1bk7x1nGsKEQAA0MMqrzOtCG/xCgAAjMUmAgAAlqiqbCIAAAC6CBEAAMBY1JkAAKAHdSYAAIAOQgQAADAWdSYAAOhBnQkAAKCDTQQAAPRgEwEAANBBiAAAAMaizgQAAD2oMwEAAHSwiQAAgCWqKpsIAACALkIEAAAwFnUmAADoQZ0JAACgg00EAAD0YBMBAADQQYgAAADGos4EAAA9qDNNuj17kq1bkyeeSG64YXQMAAAsq+nZROzZk1x4YfJnf5bs2pVcemmyfn1y003J3NzQ0wEAMKVsIibZxo3Jpk2jAJEk27ePjjduHHYuAACYMtMTIm6/Pdmx4+nP7diRbNkyyDgAADCtpqfOdP75ydq1ow3EPmvXJuedN9hIAABMt6pSZ5poGzaM7oGYn0+qRr+uXz96HgAAWDbTs4mYmxvdRL1x46jCdN55owDhpmoAAFhW0xMiklFguPji0QMAAA4DdSYAAIAO07WJAACAw8wmAgAAoIMQAQAAjEWdCQAAelBnAgAA6GATAQAAPdhEAAAAdBAiAACAsagzAQDAElWVOhMAAEAXmwgAAOjBJgIAAKCDEAEAAIxFnQkAAHpQZwIAAOhgEwEAAD3YRAAAAHQQIgAAgLGoMwEAQA/qTAAAAB1sIgAAYImqyiYCAACgixABAACMRZ0JAAB6UGcCAADoIEQAAABjUWcCAIAe1JkAAAA62EQAAEAPNhEAAAAdhAgAAGAs6kwAANCDOhMAAEAHmwgAAFiiqrKJAAAA6CJEAAAAY1FnAgCAHtSZAAAAOthEAABADzYRAAAAHYQIAABgLOpMAADQgzoTAABAB5sIAADowSYCAACggxABAACMRZ0JAACWqKrUmQAAALrYRAAAQA82EQAAAB2ECAAAYCzqTAAA0IM6EwAAQAchAgAAGIs6EwAA9KDOBAAA0GFRIaKqLqqqr1XVPVX1npUeCgAAJsG+T6we8jGEzhBRVXNJPppkQ5JzklxaVees9GAAAMDqtJhNxMuT3NNa29pa25nkmiRvWNmxAACA1WoxN1afkuT+Bcfbkqzf/6SquiLJFUly+umnL8twAACw2rmx+sAO9E+lPeOJ1q5qra1rra076aST+k8GAACsSovZRGxLctqC41OTPLgy4wAAwGSxiTiwW5OcXVVnVtVRSS5Jcv3KjgUAAKxWnZuI1truqnpHkpuSzCX5RGvtzhWfDAAAWJUW9YnVrbUbk9y4wrMAAMDEUWcCAADosKhNBAAAcGA2EQAAAB2ECAAAYCzqTAAAsERVpc4EAADQxSYCAAB6sIkAAADoIEQAAABjUWcCAIAe1JkAAAA6CBEAAMBY1JkAAKAHdSYAAIAONhEAANCDTQQAAEAHIQIAABiLOhMAACxRVakzAQAAdLGJAACAHmwiAAAAOggRAADAWNSZAACgB3UmAACADkIEAAD0sO9tXod6LGK+i6rqa1V1T1W95wCvV1V9eO/rX66ql3ZdU4gAAIApVVVzST6aZEOSc5JcWlXn7HfahiRn731ckeT3uq4rRAAAwPR6eZJ7WmtbW2s7k1yT5A37nfOGJJ9pI3+d5NlV9UOHuuiK3Fh92223PVJV//9KXHuRTkzyyIDfn9XDzwKJnwOe4meBxM/BavHDQw+wHG677babqurEgcc4pqo2Lzi+qrV21d7fn5Lk/gWvbUuyfr+vP9A5pyT51sG+4YqEiNbaSStx3cWqqs2ttXVDzsDq4GeBxM8BT/GzQOLngOXVWrto6Bk6HOimibaEc55GnQkAAKbXtiSnLTg+NcmDSzjnaYQIAACYXrcmObuqzqyqo5JckuT6/c65Pskv7H2Xplck+V5r7aBVpmR6P2zuqu5TmBF+Fkj8HPAUPwskfg6YIa213VX1jiQ3JZlL8onW2p1V9ba9r1+Z5MYkr0tyT5IfJLm867rV2iHrTgAAAE+jzgQAAIxFiAAAAMYydSGi62O9mX5VdVpV3VxVd1fVnVX17qFnYjhVNVdVt1fVDUPPwnCq6tlVdV1VfXXvnw2vHHomDr+q+uW9/7/wlaq6uqqOGXommFRTFSIW+bHeTL/dSf55a+1FSV6R5O1+Dmbau5PcPfQQDO5DSb7QWvuxJC+Jn4mZU1WnJHlXknWttb+T0Q2mlww7FUyuqQoRWdzHejPlWmvfaq19ae/vH83oXxZOGXYqhlBVpyb52SQfG3oWhlNVz0ry95J8PElaaztba98ddCiGcmSSY6vqyCTHpeN98IGDm7YQcbCP7GZGVdUZSc5PsmngURjG7yb5lSRPDjwHwzorycNJPrm32vaxqlo79FAcXq21B5L8xyT3JflWRu+D/9+GnQom17SFiLE/spvpVVXzSf4wyT9rrX1/6Hk4vKrq4iTfaa3dNvQsDO7IJC9N8nuttfOT7EjinrkZU1XPyaidcGaSFyRZW1VvHnYqmFzTFiLG/shuplNVrckoQPxBa+3zQ8/DIC5I8vqq+mZG1cbXVNVnhx2JgWxLsq21tm8jeV1GoYLZ8lNJ7m2tPdxa25Xk80leNfBMMLGmLUQs5mO9mXJVVRl1n+9urf320PMwjNbav2ytndpaOyOjPwv+R2vN3zrOoNbaQ0nur6oX7n3qtUnuGnAkhnFfkldU1XF7/3/itXGDPSzZkUMPsJwO9rHeA4/F4XdBksuS3FFVW/Y+997W2o3DjQQM7J1J/mDvXzBtTXL5wPNwmLXWNlXVdUm+lNG7+N2e5Kphp4LJVa25ZQAAAFi8aaszAQAAK0yIAAAAxiJEAAAAYxEiAACAsQgRAADAWIQIAABgLEIEAAAwlv8D7KqfW313XUsAAAAASUVORK5CYII=\n",
      "text/plain": [
       "<Figure size 1296x864 with 2 Axes>"
      ]
     },
     "metadata": {
      "needs_background": "light"
     },
     "output_type": "display_data"
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAxkAAADgCAYAAABvlquzAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjUuMSwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy/YYfK9AAAACXBIWXMAAAsTAAALEwEAmpwYAAA0E0lEQVR4nO3deZhU9bXu8e+CBoRAQBkM0iAohHkIs7kcJQMIaFBAUTTHAbyERHPJVYJkMKjHJJjEQFSUq6jgRKtHSHsiEEVQ0IgI2CKiKBEiDSiIogga6GbdP/butrroCXpX19Dv53n6oWpPtXZDvdSq3x7M3REREREREYlKrWQXICIiIiIimUVNhoiIiIiIREpNhoiIiIiIREpNhoiIiIiIREpNhoiIiIiIREpNhoiIiIiIREpNhqQtM9tmZt9Pdh0iUjYzu8LMXkzC6z5vZldV9+uKSPnMbLCZ5SfhdeeZ2S3V/bo1mZoMAcDMrjGztWb2bzObdwzr6YO+SAYxs3pmdp+Z/cvM9pvZa2Y2PNl1iUhqMLOHzWyXmX1mZu+omZeyqMmQIjuBW4D7k12IiCRVFrAdOAtoDNwAPG5mbZNZlIikjN8Dbd3968BI4BYz61PagmaWVa2VSUpRkyEAuPtCd/8rsDd+npk1M7O/mdk+M/vYzFaZWS0zewhoA/yPmX1uZlNL27aZTQ2/9dhpZleZmZtZ+3BeYzN70Mz2hN+c/trMaoXzTjez5Wa218w+MrNHzKxJwn4JIoK7H3D3G919m7sfcfe/AVuBPvDVoQ5mdp2Z7Q7f21cWrW9mTc3sqfBbzjXA6eW9npldFr7395rZDbGjo+GoyqwwO3aGj+uF804Mc2mPmX0SPs5O2C9GRABw9zfd/d9FT8Of06FEPlxvZh8AD5hZ/fBQpU/MbBPQr7ztm9lQM9tsZp+a2V1m9kLRaEn42ePXYWbsDj8/NI5Z9wkz+yBcd6WZdU3IL0EqRU2GVMZ1QD7QHDgZ+CXg7v6fwPvAD9y9obv/IX5FMxsGXAt8H2hP8O1orDsIvi09LZx3GVD0gcUIvjE5BegMtAZujHLHRKR8ZnYy8E3gzZjJ3yB437YCJgCzzezEcN5s4EugJTA+/Clr212Au4BLw+WLtlnkV8BAoBfQE+gP/DqcVwt4ADiV4MuOL4A7j28vReRYhB/+DwJvA7uAxTGzvwGcRPDenAhMJ2hCTgfOBi4vZ7vNgP8GfgE0BTYD345Z5Irw5zsEnxsaUvJ9vwToALQA1gOPHN8eShTUZEhlHCb4AHCqux9291Xu7pVcdyzwQPjNx0HgpqIZZlYbuAj4hbvvd/dtwG3AfwK4+xZ3f9bd/+3ue4A/c3STIiIJYmZ1CP6Tnu/ub8fMOgzcHObBYuBzoGP4nh4D/CYcEdkIzC/nJS4A/sfdX3T3Q8BvCL4VLXJp+Dq7wwy4ia/yYa+7P+nuB919P/BblA8i1cLdfwI0Av4DWAj8O2b2EWB6+H/3FwSfA37r7h+7+3bg9nI2PQJ4Mzy6oiBc9oOY+ZcCf3b399z9c4Jm5OKiw7Lc/f7w88S/Cb6U7Bk70iHVS02GVMYfgS3AM2b2nplNO4Z1TyE4vrtI7ONmQF3gXzHT/kX4TaaZtTCzHDPbYWafAQ+H64hIgoWHLT4EHAKuiZu9N/wAUOQgwTeKzfnqnI4ise/veCXyIfwiYm/c/Ph8OCWsr4GZ/b/wsInPgJVAk7DREZEEc/dCd38RyAZ+HDNrj7t/GfM8/nPAsWSCExxJETs/PhOygJPNrLaZzTCzf4aZsC1cRp8bkkRNhlQo/FbgOnc/DfgBcK2Zfa9odgWr7yIIoCKtYx5/RPCN6Kkx09oAO8LHvw+33yM8weyHBIdQiUgCmZkB9xEcHjnG3Q9XctU9QAEl3+dtylm+RD6YWX2CQySK7OTofNgZPr4O6AgMCPPhzKLNVLJWEYlGFiXPvYr/XLCL488Eo+RniNIyoQD4ELgEOI/g8OzGQNuizVS0A5IYajIECK4AYWYnALWB2mZ2QtHwo5mda2btwzf7Z0Bh+APBG/u0cjb9OHClmXU2swYEh0MAwbcg4fzfmlkjMzuV4PyNh8NFGhEchrHPzFoBP49qf0WkXHcTnAf1g/Bwh0oJ39MLgRvDkYYulHP8NcGx1z8ws2+bWV2Cw6FiPxAsAH5tZs3DY7V/Q8l8+IIgH04iOO5bRBIoPMLgYjNrGI4cnA2MA5aXs9rjwC/CizVkAz8tZ9mnge5mdn74GeRqgnM8iiwA/q+ZtTOzhsDvgMfCkdVGBIdt7QUahPMkidRkSJFfE/yHPY1gxOALvjrBsgOwjOAD/8vAXe7+fDjv9wQfAvaZ2ZT4jbr7EoJjKlcQHHL1cjir6PjNnwIHgPeAF4FH+eoyujcBvYFPCYJnYQT7KSLlCJv9HxGcbP2BBVeO+9zMLq3kJq4hOHTqA2AewcnZpXL3NwkyIIfgG8z9wG6+yodbgLXABuANghM5i26mNQuoTzAiuhpYWsn6ROT4OcGhUfnAJ8CfgJ+5e24569xEcFjTVuAZgsMwS9+4+0fAhcAfCJqFLgQZUJQJ94frrwy39yVfNS0Phq+zA9hEkAuSRFb583dFqs7MOgMbgXpxx3SLSA0XfjO5D+jg7luTXI6IJFl4blg+cKm7r0h2PXJsNJIhCWdmo8ysbniJy1sJriajBkNEMLMfhIdWfY3gW9E3+OqETRGpYczsbDNrEt4T55cEh1BqVCINJazJMLP7wxulbCxjvpnZ7Wa2xcw2mFnvRNUiSfcjghNC/0lwLsePy19cMpVyQUpxHsHJnDsJDs28+BgukS0ZQLkgcc4g+LzwEcHFZs4/lnPDJHUk7HApMzuT4Bj+B929WynzRxAcRzcCGAD8xd0HJKQYEUkJygURiadcEMlMCRvJcPeVwMflLHIeQaC4u68muL55y0TVIyLJp1wQkXjKBZHMlMxzMlpR8uYs+eE0Eam5lAsiEk+5IJKGspL42qXdHKXUY7fMbCIwEeBrX/tan06dOiWyLhEB1q1b95G7N6/ml1UuiKQw5YKIxCsrF5LZZORT8g6Q2Xx1J9cS3P0e4B6Avn37+tq1axNfnUgNZ2b/SsLLKhdEUphyQUTilZULyTxc6ingsvCqEQOBT919VxLrEZHkUy6ISDzlgkgaSthIhpktAAYDzcwsH5gO1AFw9znAYoIrRWwBDgJXJqoWEUkNygURiadcEMlMCWsy3H1cBfMduDpRry8iqUe5ICLxlAsimUl3/BYRERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUipyRARERERkUgltMkws2FmttnMtpjZtFLmNzaz/zGz183sTTO7MpH1iEjyKRdEJJ5yQSTzJKzJMLPawGxgONAFGGdmXeIWuxrY5O49gcHAbWZWN1E1iUhyKRdEJJ5yQSQzJXIkoz+wxd3fc/dDQA5wXtwyDjQyMwMaAh8DBQmsSUSSS7kgIvGUCyIZKJFNRitge8zz/HBarDuBzsBO4A1gsrsfid+QmU00s7VmtnbPnj2JqldEEk+5ICLxlAsiGSiRTYaVMs3jnp8N5AGnAL2AO83s60et5H6Pu/d1977NmzePuk4RqT7KBRGJp1wQyUCJbDLygdYxz7MJvoGIdSWw0ANbgK1ApwTWJCLJpVwQkXjKBZEMlMgm41Wgg5m1C0/Ouhh4Km6Z94HvAZjZyUBH4L0E1iQiyaVcEJF4ygWRDJSVqA27e4GZXQP8HagN3O/ub5rZpHD+HOC/gHlm9gbBcOn17v5RomoSkeRSLohIPOWCSGZKWJMB4O6LgcVx0+bEPN4JDE1kDSKSWpQLIhJPuSCSeXTHbxERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiVSlmgwzO9fM1JCISDHlgojEUy6ISJHKBsHFwLtm9gcz65zIgkQkbSgXRCSeckFEgEo2Ge7+Q+BbwD+BB8zsZTObaGaNElqdiKQs5YKIxFMuiEiRSg9puvtnwJNADtASGAWsN7OfJqg2EUlxygURiadcEBGo/DkZI81sEbAcqAP0d/fhQE9gSjnrDTOzzWa2xcymlbHMYDPLM7M3zeyF49gHEUkC5YKIxFMuiEiRrEoudwEw091Xxk5094NmNr60FcysNjAbGALkA6+a2VPuvilmmSbAXcAwd3/fzFocxz6ISHIoF0QknnJBRIDKHy61Kz4wzOxWAHd/rox1+gNb3P09dz9EMGx6XtwylwAL3f39cFu7K125iCSbckFE4ikXRASofJMxpJRpwytYpxWwPeZ5fjgt1jeBE83seTNbZ2aXVbIeEUk+5YKIxFMuiAhQweFSZvZj4CfA6Wa2IWZWI+ClCrZtpUzzUl6/D/A9oD7wspmtdvd34uqYCEwEaNOmTQUvKyKJpFwQkXjKBRGJV9E5GY8CS4DfA7EnYu13948rWDcfaB3zPBvYWcoyH7n7AeCAma0kODmsRGi4+z3APQB9+/aNDx4RqV7KBRGJp1wQkRIqOlzK3X0bcDWwP+YHMzupgnVfBTqYWTszq0twg56n4pbJBf7DzLLMrAEwAHjr2HZBRKqZckFE4ikXRKSEyoxknAusIxi6jB3SdOC0slZ09wIzuwb4O1AbuN/d3zSzSeH8Oe7+lpktBTYAR4C57r7xuPdGRKqDckFE4ikXRKQEc0+v0cS+ffv62rVrk12GSMYzs3Xu3jfZdVSGckGkeigXRCReWblQ0Ynfvcub7+7rq1qYiKQX5YKIxFMuiEi8ig6Xuq2ceQ58N8JaRCQ9KBdEJJ5yQURKKLfJcPfvVFchIpIelAsiEk+5ICLxKjpc6rvuvtzMRpc2390XJqYsEUlVygURiadcEJF4FR0udRawHPhBKfMcUGiI1DzKBRGJp1wQkRIqOlxqevjnldVTjoikOuWCiMRTLohIvIpuxgeAmTU1s9vNbL2ZrTOzv5hZ00QXJyKpS7kgIvGUCyJSpFJNBpAD7AHGABeEjx9LVFEikhaUCyIST7kgIkDF52QUOcnd/yvm+S1mdn4C6hGR9KFcEJF4ygURASo/krHCzC42s1rhz1jg6UQWJiIpT7kgIvGUCyICVHwJ2/0EV4Uw4Frg4XBWLeBzYHpCqxORlKNcEJF4ygURiVfR1aUaVVchIpIelAsiEk+5ICLxKntOBmZ2ItABOKFomruvTERRIpIelAsiEk+5ICJQySbDzK4CJgPZQB4wEHgZ+G7CKhORlKZcEJF4ygURKVLZE78nA/2Af7n7d4BvEVyWTkRqLuWCiMRTLogIUPkm40t3/xLAzOq5+9tAx8SVJSJpQLkgIvGUCyICVP6cjHwzawL8FXjWzD4BdiaqKBFJC8oFEYmnXBARoJJNhruPCh/eaGYrgMbA0oRVJSIpT7kgIvGUCyJS5FiuLtUbGERwHeyX3P1QwqoSkbSgXBCReMoFEYFKnpNhZr8B5gNNgWbAA2b260QWFrWlS5fSsWNH2rdvz4wZM46an5ubS48ePejVqxd9+/blxRdfLJ73l7/8hW7dutG1a1dmzZpVYr077riDjh070rVrV6ZOnZro3RBJGZmQCyISLeWCiBSp7EjGOOBbMSdzzQDWA7ckqrAoFRYWcvXVV/Pss8+SnZ1Nv379GDlyJF26dCle5nvf+x4jR47EzNiwYQNjx47l7bffZuPGjdx7772sWbOGunXrMmzYMM455xw6dOjAihUryM3NZcOGDdSrV4/du3cncS9Fql1a54KIJIRyQUSAyl9dahsxN9UB6gH/jLyaBFmzZg3t27fntNNOo27dulx88cXk5uaWWKZhw4aYGQAHDhwofvzWW28xcOBAGjRoQFZWFmeddRaLFi0C4O6772batGnUq1cPgBYtWlTjXokk3TbSOBdEJCG2oVwQESpoMszsDjO7Hfg38KaZzTOzB4CNwOfVUWAUduzYQevWrYufZ2dns2PHjqOWW7RoEZ06deKcc87h/vvvB6Bbt26sXLmSvXv3cvDgQRYvXsz27dsBeOedd1i1ahUDBgzgrLPO4tVXX62eHRJJokzJBRGJjnJBROJVdLjU2vDPdcCimOnPJ6SaBHH3o6YVjVTEGjVqFKNGjWLlypXccMMNLFu2jM6dO3P99dczZMgQGjZsSM+ePcnKCn5tBQUFfPLJJ6xevZpXX32VsWPH8t5775W6bZEMkhG5ICKRUi6ISAnlNhnuPr/osZnVBb4ZPt3s7ocr2riZDQP+AtQG5rr70WdcB8v1A1YDF7n7f1ey9krLzs4uHn0AyM/P55RTTilz+TPPPJN//vOffPTRRzRr1owJEyYwYcIEAH75y1+SnZ1dvN3Ro0djZvTv359atWrx0Ucf0bx586h3QSRlZEouiEh0lAsiEq+yV5caDLwLzAbuAt4xszMrWKd2uPxwoAswzsy6lLHcrcDfj6XwY9GvXz/effddtm7dyqFDh8jJyWHkyJElltmyZUvxiMf69es5dOgQTZs2BSg+ofv9999n4cKFjBs3DoDzzz+f5cuXA8GhU4cOHaJZs2aJ2g2RlJLuuSAi0VMuiEiRyl5d6jZgqLtvBjCzbwILgD7lrNMf2OLu74Xr5ADnAZvilvsp8CTQ7xjqPiZZWVnceeednH322RQWFjJ+/Hi6du3KnDlzAJg0aRJPPvkkDz74IHXq1KF+/fo89thjxYc9jRkzhr1791KnTh1mz57NiSeeCMD48eMZP3483bp1o27dusyfP1+HSklNkta5kC6WLl3K5MmTKSws5KqrrmLatGkl5ufm5nLDDTdQq1YtsrKymDVrFoMGDQKgbdu2NGrUiNq1a5OVlcXatcERLR9//DEXXXQR27Zto23btjz++OPFuSZSRcoFEQEq32TUKQoMAHd/x8zqVLBOK2B7zPN8YEDsAmbWChgFfJcEh8aIESMYMWJEiWmTJk0qfnz99ddz/fXXl7ruqlWrSp1et25dHn744eiKFEkvaZ8Lqa4ql98usmLFiqNGWGfMmMH3vvc9pk2bxowZM5gxYwa33nprte2XZDTlgogAlW8y1pnZfcBD4fNLCU7uKk9pX+nHn4E9C7je3QvLGwEws4nARIA2bdpUpl7aTnu6Ussl0rYZ5yS7BJFESrtcSDexl98Gii+/HdtkNGzYsPhx7OW3y5Obm8vzzz8PwOWXX87gwYPVZEhUlAsiAlT+PhmTgDeB/wNMJhjCnFTuGsE3Ea1jnmcDO+OW6QvkmNk24ALgLjM7P35D7n6Pu/d19746qVokZSgXEqwql9+G4Cp6Q4cOpU+fPtxzzz3F0z/88ENatmwJQMuWLXUjUYmSckFEgEqMZJhZLWCdu3cD/nwM234V6GBm7YAdwMXAJbELuHu7mNeZB/zN3f96DK8hIkmgXKgeVbn8NsBLL73EKaecwu7duxkyZAidOnXizDPLPQdX5LgpFyTe8Z5Ttn37di677DI++OADatWqxcSJE5k8eTIAF110EZs3B0fk7du3jyZNmpCXl1fduyaVUGGT4e5HzOx1M2vj7u9XdsPuXmBm1xBcBaI2cL+7v2lmk8L5c467ahFJKuVC9ajq5beLlm3RogWjRo1izZo1nHnmmZx88sns2rWLli1bsmvXLlq0aJHwfZHMp1yQWFU5pywrK4vbbruN3r17s3//fvr06cOQIUPo0qULjz32WPH61113HY0bN07G7kklVPacjJYEd/BcAxwomujuI8teBdx9MbA4blqpYeHuV1SyFhFJDcqFBIu9/HarVq3Iycnh0UcfLbHMli1bOP300zGzEpffPnDgAEeOHKFRo0YcOHCAZ555ht/85jcAjBw5kvnz5zNt2jTmz5/Peeedl4zdk8ykXBCgaueUtWzZsviQzkaNGtG5c2d27NhRYl135/HHHy++lYCknso2GTcltAoRSUfKhQSryuW3P/zwQ0aNGgVAQUEBl1xyCcOGDQNg2rRpjB07lvvuu482bdrwxBNPJG0fJeMoFwQo/ZyyV1555ajlFi1axC9+8Qt2797N008ffdGebdu28dprrzFgQIkLjrFq1SpOPvlkOnToEH3xEolymwwzO4HghK32wBvAfe5eUB2FiUhqUi5Ur+O9/PZpp53G66+/Xuo2mzZtynPPPRdtoVKjKRckXlXPKQP4/PPPGTNmDLNmzeLrX/96ifUWLFhQfHNkSU0VjWTMBw4Dq/jqTpyTE12UiKQ05YKIxFMuSAlVPafs8OHDjBkzhksvvZTRo0eXWLagoICFCxeybl1FV0eWZKqoyeji7t0Bwuter0l8SSKS4pQLCZQK9/gB3edHjplyQUqoyjll7s6ECRPo3Lkz11577VHbXrZsGZ06dSI7O7u6dkeOQ0VNxuGiB+HVHxJcjoikAeWCiMRTLkgJVTmn7MUXX+Shhx6ie/fu9OrVC4Df/e53xYeO5uTk6FCpNFBRk9HTzD4LHxtQP3xugLv718teVUQylHJBROIpF+Qox3tO2aBBg0o9p6PIvHnzIqtREqfcJsPda1dXISKSHpQLIhJPuSAi8Sp7CVsRERERkTKlwjllOp8sddRKdgEiIiIiUnlLly6lY8eOtG/fnhkzZhw1/5FHHqFHjx706NGDb3/72yUuZ922bdvicx369u1bPD0vL4+BAwcWT1+zRufuS9WoyUghiQiNG264gR49etCrVy+GDh3Kzp07q2VfREREJHqFhYVcffXVLFmyhE2bNrFgwQI2bdpUYpl27drxwgsvsGHDBm644QYmTpxYYv6KFSvIy8tj7dq1xdOmTp3K9OnTycvL4+abb2bq1KnVsj+SudRkpIhEhcbPf/5zNmzYQF5eHueeey4333xzteyPiIiIRG/NmjW0b9+e0047jbp163LxxReTm5tbYplvf/vbnHjiiQAMHDiQ/Pz8CrdrZnz2WXDu/qefflruPS1EKkNNRopIVGjE3iHzwIEDpd5tU0Skqo53JPbLL7+kf//+9OzZk65duzJ9+vTidV5//XXOOOMMunfvzg9+8IPiD0AiNdmOHTto3bp18fPs7Gx27NhR5vL33Xcfw4cPL35uZgwdOpQ+ffpwzz33FE+fNWsWP//5z2ndujVTpkzh97//fWJ2QGoMNRkpIlGhAfCrX/2K1q1b88gjj2gkQ0QiV5WR2Hr16rF8+XJef/118vLyWLp0KatXrwbgqquuYsaMGbzxxhuMGjWKP/7xj9W+byKpprRLu5b1BeKKFSu47777uPXWW4unvfTSS6xfv54lS5Ywe/ZsVq5cCcDdd9/NzJkz2b59OzNnzmTChAmJ2QGpMdRkpIhEhQbAb3/7W7Zv386ll17KnXfeGX3xIlKjVWUk1sxo2LAhAIcPH+bw4cPF2bd582bOPPNMAIYMGcKTTz5ZXbskkrKys7PZvn178fP8/PxSD23asGEDV111Fbm5uTRt2rR4etGyLVq0YNSoUcUneM+fP5/Ro0cDcOGFF+rEb6kyNRkpIlGhEeuSSy7Rf9IiErmqjsQWFhbSq1cvWrRowZAhQxgwYAAA3bp146mnngLgiSeeKJGRIjVVv379ePfdd9m6dSuHDh0iJyeHkSNHlljm/fffZ/To0Tz00EN885vfLJ5+4MAB9u/fX/z4mWeeoVu3bkDwOeKFF14AYPny5XTo0KGa9kgylZqMFJGo0Hj33XeLl3vqqafo1KlTNeyNiNQkVR2JrV27Nnl5eeTn57NmzRo2btwIwP3338/s2bPp06cP+/fvp27duonZAZE0kpWVxZ133snZZ59N586dGTt2LF27dmXOnDnMmTMHgJtvvpm9e/fyk5/8pMRVJz/88EMGDRpEz5496d+/P+eccw7Dhg0D4N577+W6666jZ8+e/PKXvzzq0GuRY6Wb8aWI2NAoLCxk/PjxxaEBMGnSpBKhUbTO2rVr+fDDDxk1ahQABQUFXHLJJcWhMW3aNDZv3kytWrU49dRTi7cnIhKVYx2JXbJkSYmR2CJNmjRh8ODBLF26lG7dutGpUyeeeeYZAN555x2efjr5N/oSSQUjRoxgxIgRJaZNmjSp+PHcuXOZO3fuUeuddtppJS5/H2vQoEGsW7cu2kKlRlOTkUISERo6PEpEEi12JLZVq1bk5OTw6KOPllimrJHYPXv2UKdOHZo0acIXX3zBsmXLuP766wHYvXs3LVq04MiRI9xyyy0l8lBERFKbmowkajstNb6V2zbjnGSXICJprCojsbt27eLyyy+nsLCQI0eOMHbsWM4991wAFixYwOzZswEYPXo0V155ZXJ2UCQFpMJnBn1ekGOhJkNERKrseEdie/TowWuvvVbqNidPnszkyZOjLVRERKqFTvwWEREREZFIaSRDRGqspUuXMnnyZAoLC7nqqquYNm1aiflvv/02V155JevXr+e3v/0tU6ZMAYL7N1x00UXFy7333nvcfPPN/OxnP+Oiiy5i8+bNAOzbt48mTZqQl5dXbftUXXTohmSq480FgJkzZzJ37lzMjO7du/PAAw9wwgkn8MQTT3DjjTfy1ltvsWbNmuKrPYlkMjUZIlIjFd2l+tlnnyU7O5t+/foxcuRIunTpUrzMSSedxO23385f//rXEut27NixuHEoLCykVatWxVd4e+yxx4qXu+6662jcuHHC90VEolGVXNixYwe33347mzZton79+owdO5acnByuuOIKunXrxsKFC/nRj35UzXskkjw6XEpEaqTK3KW6RYsW9OvXjzp16pS5neeee47TTz+dU089tcR0d+fxxx9n3LhxCalfRKJX1VwoKCjgiy++oKCggIMHDxZfyrlz58507NixWvZBJFUktMkws2FmttnMtpjZtFLmX2pmG8Kff5hZz0TWIyLJlyq5cKx3qS5LTk5OqY3EqlWrOPnkk3XXXJFKyIRcaNWqFVOmTKFNmza0bNmSxo0bM3To0ESUKZIWEtZkmFltYDYwHOgCjDOzLnGLbQXOcvcewH8Bur2kSAZLpVw4lrtUl+XQoUM89dRTXHjhhUfNW7BggUYxRCohU3Lhk08+ITc3l61bt7Jz504OHDjAww8/HHWJImkjkSMZ/YEt7v6eux8CcoDzYhdw93+4+yfh09VAdgLrEZHkS5lcqOxdqsuzZMkSevfuzcknn1xiekFBAQsXLixxcriIlCkjcmHZsmW0a9eO5s2bU6dOHUaPHs0//vGPRJQpkhYS2WS0ArbHPM8Pp5VlArCktBlmNtHM1prZ2j179kRYoohUs5TJhdi7VB86dIicnBxGjhx5TNsoa7Ri2bJldOrUiexsfW8iUgkZkQtt2rRh9erVHDx4EHfnueeeo3Pnzsdcg0imSGSTUdr44tHjkICZfYcgNK4vbb673+Pufd29b/PmzSMsUY7H0qVL6dixI+3bt2fGjBlHzX/77bc544wzqFevHn/605+Kp3/55Zf079+fnj170rVrV6ZPn148Ly8vj4EDB9KrVy/69u3LmjVrqmVfpNqlTC7E3qW6c+fOjB07tvgu1UV3qv7ggw/Izs7mz3/+M7fccgvZ2dl89tlnABw8eJBnn32W0aNHH7Xtss7TEJFSZUQuDBgwgAsuuIDevXvTvXt3jhw5wsSJEwFYtGgR2dnZvPzyy5xzzjmcffbZx1ybSLpJ5CVs84HWMc+zgZ3xC5lZD2AuMNzd9yawHolAVS7vV69ePZYvX07Dhg05fPgwgwYNYvjw4QwcOJCpU6cyffp0hg8fzuLFi5k6dSrPP/989e5cNTvea7Fv376dyy67jA8++IBatWoxceLE4rsi5+XlMWnSJL788kuysrK466676N+/f7XvWzlSKhcqukv1N77xDfLz80tdt0GDBuzdW3pp8+bNi6xGkRogY3Lhpptu4qabbjpq+qhRo4ovcy1SUySyyXgV6GBm7YAdwMXAJbELmFkbYCHwn+7+TgJrkYjEXt4PKL68X2yT0aJFC1q0aMHTT5e8WZeZ0bBhQwAOHz7M4cOHi0+oM7Pib4g//fTTYz42Pt1UpVnLysritttuo3fv3uzfv58+ffowZMgQunTpkg7NmnJBROIlNRd0Y0mRxEhYk+HuBWZ2DfB3oDZwv7u/aWaTwvlzgN8ATYG7wg+bBe6u22CmsNIu7/fKK69Uev3CwkL69OnDli1buPrqqxkwYAAAs2bN4uyzz2bKlCkcOXIk40+Wq0qz1rJlS1q2bAlAo0aN6Ny5Mzt27KBLly4p36wlOxf0YaJmq8qdnMePH8/f/vY3WrRowcaNG4unR32H93SoMWrJzgWp2dLhPZcONZYmoXf8dvfFwOK4aXNiHl8FXJXIGiRaVb3sZ+3atcnLy2Pfvn2MGjWKjRs30q1bN+6++25mzpzJmDFjePzxx5kwYQLLli2LsvSUUtVmrci2bdt47bXX0qpZUy5IMlRl9BDgiiuu4JprruGyyy4rMT3KO7ynQ42JolyQZEiH91w61FgW3fFbjkkUl/0EaNKkCYMHD2bp0qUAzJ8/v/gE2gsvvDDjT/yO4h4Nn3/+OWPGjGHWrFl8/etfByhu1rZv387MmTOZMGFCJPWKpLuq3sn5zDPP5KSTTipz+1Hc4T0dahTJJOnwnkuHGsuiJkOOSVUu77dnzx727dsHwBdffFF8mU+AU045hRdeeAGA5cuXZ/xdkqvarB0+fJgxY8Zw6aWXlri6UU1r1kQqK6o7vJcliju8p0ONIpkkHd5z6VBjWRJ6uJRkntjL+xUWFjJ+/Pjiy/tBcAWODz74gL59+/LZZ59Rq1YtZs2axaZNm9i1axeXX345hYWFHDlyhLFjx3LuuecCcO+99zJ58mQKCgo44YQTuOeezL75e2yz1qpVK3Jycnj00Ucrta67M2HCBDp37sy1115bYl5RszZ48OAa0ayJVFYUo4flieIO7+lQo0gmSYf3XDrUWBY1GXLMjvfyfj169OC1114rdZuDBg1i3bp1kdVY0UlS7s7kyZNZvHgxDRo0YN68efTu3RuAmTNnMnfuXMyM7t2788ADD3DCCScAcMcdd3DnnXeSlZXFOeecwx/+8Ifjqq8qzdqGDRt46KGH6N69O7169QLgd7/7HSNGjKhxzZpIZUV1qGdpiu7wXtUMS4caRTJJOrzn0qHGsqjJkAql2xV5KnOS1JIlS3j33Xd59913eeWVV/jxj3/MK6+8wo4dO7j99tvZtGkT9evXZ+zYseTk5HDFFVewYsUKcnNz2bBhA/Xq1WP37t1V2qfjbdYGDRpU6jcbRfP0IULkaFUZPaxIVHd4T4caRTJJOrzn0qHGsuicDMk4lTlJKjc3l8suuwwzY+DAgezbt49du3YBQWf/xRdfUFBQwMGDB4u/Mbj77ruZNm0a9erVA4ITrUQkPVT1Du/jxo3jjDPOYPPmzWRnZ3PfffcVbzuqO7ynQ40imSQd3nPpUGOZtSdsyyJJUpnLw5Z1IlXfvn2ZMmUKbdq0oX79+gwdOpShQ4cC8M4777Bq1Sp+9atfccIJJ/CnP/2Jfv36HVNt6TYqJJJJqnIn5wULFpS53Sjv8J4ONYpkknR4z6VDjaXRSIZknMqcJFXWMp988gm5ubls3bqVnTt3cuDAAR5++GEgGOH45JNPWL16NX/84x8ZO3ZsmYctiYiIiNRkGsmQjFOZk6TKWmbZsmW0a9eO5s2bAzB69Gj+8Y9/8MMf/pDs7GxGjx6NmdG/f39q1arFRx99VLysiKSWdBk5TJc6RTJBurzf0qXO8mgkQzJOZe7lMXLkSB588EHcndWrV9O4cWNatmxJmzZtWL16NQcPHsTdee655+jcuTMA559/PsuXLweCQ6cOHTpEs2bNqn3/RERERFKdRjIk41Tm8rAjRoxg8eLFtG/fngYNGvDAAw8AMGDAAC644AJ69+5NVlYW3/rWt5g4cSIA48ePZ/z48XTr1o26desyf/78SK9VLSIiIpIp1GRIRqroJCkzY/bs2aWue9NNN3HTTTcdNb1u3brF52eIiIiISNl0uJSIiIiIiERKIxmSETLhBCkRERGRTKGRDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiZSaDBERERERiVRCmwwzG2Zmm81si5lNK2W+mdnt4fwNZtY7kfWISPIpF0QknnJBJPMkrMkws9rAbGA40AUYZ2Zd4hYbDnQIfyYCdyeqHhFJPuWCiMRTLohkpkSOZPQHtrj7e+5+CMgBzotb5jzgQQ+sBpqYWcsE1iQiyaVcEJF4ygWRDJTIJqMVsD3meX447ViXEZHMoVwQkXjKBZEMlJXAbVsp0/w4lsHMJhIMjwJ8bmabq1hbZTUDPjrele3WCCspW5VqhGqpMx1qBP19xzu1Kq9T1suXMk25EL10eM+lQ42gv+94yoXS6d9JNNKhRtDfd7xScyGRTUY+0DrmeTaw8ziWwd3vAe6JusCKmNlad+9b3a97LFRjdNKhznSosQLKhWqgGqOTDnWmQ40VUC5UA9UYnXSoMxVqTOThUq8CHcysnZnVBS4Gnopb5ingsvCqEQOBT919VwJrEpHkUi6ISDzlgkgGSthIhrsXmNk1wN+B2sD97v6mmU0K588BFgMjgC3AQeDKRNUjIsmnXBCReMoFkcyUyMOlcPfFBMEQO21OzGMHrk5kDVVU7UOux0E1Ricd6kyHGsulXKgWqjE66VBnOtRYLuVCtVCN0UmHOpNeowXvWxERERERkWgk9I7fIiIiIiJS86jJKIWZDTOzzWa2xcymJbue0pjZ/Wa228w2JruWsphZazNbYWZvmdmbZjY52TXFM7MTzGyNmb0e1nhTsmsqi5nVNrPXzOxvya6lJlIuREO5EC3lQnIpF6KhXIhWquSCmow4ZlYbmA0MB7oA48ysS3KrKtU8YFiyi6hAAXCdu3cGBgJXp+Dv8t/Ad929J9ALGBZeuSQVTQbeSnYRNZFyIVLKhWgpF5JEuRAp5UK0UiIX1GQcrT+wxd3fc/dDQA5wXpJrOoq7rwQ+TnYd5XH3Xe6+Pny8n+AffErdodUDn4dP64Q/KXeikpllA+cAc5NdSw2lXIiIciE6yoWkUy5ERLkQnVTKBTUZR2sFbI95nk+K/UNPR2bWFvgW8EqSSzlKOKyYB+wGnnX3lKsRmAVMBY4kuY6aSrmQAMqFKpuFciGZlAsJoFyoslmkSC6oyTialTIt5TrVdGJmDYEngZ+5+2fJrieeuxe6ey+CO8j2N7NuSS6pBDM7F9jt7uuSXUsNplyImHKhapQLKUG5EDHlQtWkWi6oyThaPtA65nk2sDNJtaQ9M6tDEBiPuPvCZNdTHnffBzxP6h27+r+AkWa2jWA4/rtm9nByS6pxlAsRUi5EQrmQfMqFCCkXIpFSuaAm42ivAh3MrJ2Z1QUuBp5Kck1pycwMuA94y93/nOx6SmNmzc2sSfi4PvB94O2kFhXH3X/h7tnu3pbg3+Nyd/9hksuqaZQLEVEuREO5kBKUCxFRLkQj1XJBTUYcdy8ArgH+TnDi0ePu/mZyqzqamS0AXgY6mlm+mU1Idk2l+F/AfxJ00nnhz4hkFxWnJbDCzDYQ/IfxrLvrUpBSgnIhUsoFyQjKhUgpFzKQ7vgtIiIiIiKR0kiGiIiIiIhESk2GiIiIiIhESk2GiIiIiIhESk2GiIiIiIhESk2GiIiIiIhESk1GEpnZKDNzM+sUM61XlJdtM7O5ZtYlqu1VBzO72cy+Hz7+mZk1iJm3uOg61VV8jRvNbEoFy8wzswuOYZttzWxjVWuTmk25UDrlgtRkyoXSKRdSm5qM5BoHvEhww5QivYDIQsPdr3L3TVFtzwIJ/Xfj7r9x92Xh058BDWLmjQjvtCmSqZQLpVAuSA2nXCiFciG1qclIEjNrSHDzmQmEoRHeMfRm4KLwRjQXmdlJZvZXM9tgZqvNrEe47I1mNt/MnjGzbWY22sz+YGZvmNlSM6sTLve8mfUNHw8zs/Vm9rqZPVdKTVeYWW64/mYzmx5Ob2tmb5nZXcB6oLWZ/dHMNoavd1G43GAzW2lmi8xsk5nNKQoYMxsXLrvRzG4Np9UOu/+i7fzfcPo8M7vAzP4PcArBzW9WhPO2mVmz8PG14bobzexncbXea2Zvhr+f+hX8XfxvM3s1/L08GftNCPB9M1tlZu+Y2bkxdf8xXGeDmf3omP7yRcqgXFAuiMRTLigX0pa76ycJP8APgfvCx/8AeoePrwDujFnuDmB6+Pi7QF74+EaCbzXqAD2Bg8DwcN4i4Pzw8fNAX6A5sB1oF04/qZSargB2AU2B+sDGcN22wBFgYLjcGOBZoDZwMvA+wZ0wBwNfAqeF854FLiB4478f1pAFLAfOB/oQ3DGz6PWbhH/OAy4IH28DmsUssw1oFq77BvA1oCHwJvCtsNYCoFe4/OPAD0vZ1xuBKeHjpjHTbwF+GlPHUoJmvAOQD5wATAR+HS5TD1gLtAtfe2Oy/23pJ31/lAvKBf3oJ/5HuaBcSNcfjWQkzzggJ3ycEz4vzSDgIQB3Xw40NbPG4bwl7n6Y4M1Tm+AfOOHztnHbGQisdPet4bY+LuP1nnX3ve7+BbAwfH2Af7n76piaFrh7obt/CLwA9AvnrXH399y9EFgQLtsPeN7d97h7AfAIcCbwHnCamd1hZsOAz8qoqazfyyJ3P+Dun4e1/kc4b6u754WP15Xyu4jXLfz24Q3gUqBrzLzH3f2Iu78b1tsJGApcZmZ5wCsEIdvhGGoXKYtyQbkgEk+5oFxIS1nJLqAmMrOmBN8ydDMzJ3jDu5lNLW3xUqZ5+Oe/Adz9iJkd9rBVJvgWIf7v1mLWK0/8MkXPD1RQU3nrl7q8u39iZj2Bs4GrgbHA+ErUWFEN/455XEjwLUt55hF8k/O6mV1B8A1LcZlxyxbtz0/d/e8lCjJrW8HriJRJuRDOUC6IFFMuhDOUC2lJIxnJcQHwoLuf6u5t3b01sJWg294PNIpZdiVBt4yZDQY+cvdj6eCLvAycZWbtwm2dVMZyQ8LjOusTDFG+VMoyKwmOA61tZs0JvmVYE87rb2btwmMrLyIYon0lfO1mZlab4FuYF8JjJWu5+5PADUDvUl4r/vcRW8P5ZtbAzL4GjAJWVfA7KEsjYFd4XOqlcfMuNLNaZnY6wbDuZuDvwI9jjmP9ZliDSFUoF5QLIvGUC8qFtKWRjOQYB8yIm/YkcAnwK2BaOLT2e4JjAR8wsw0Ex1Fefjwv6O57zGwisDB8Q+8GhpSy6IsEw63tgUfdfW0pHfci4AzgdYJOfaq7f2DBpfVeDvetO8Ebe1H4zckvgBUEXf1id88Nv5V4wL66+sQvSqnnHmCJme1y9+/E7M96M5vHV2E1191fO85vB24gCLZ/EQwdx4bUZoLh3ZOBSe7+pZnNJRhSXW9mBuwhCFiRqlAuKBdE4ikXlAtpy74aMZOaLhz66+vu1xzn+oMJTo46N8KyRCSJlAsiEk+5IJWhw6VERERERCRSGskQEREREZFIaSRDREREREQipSZDREREREQipSZDREREREQipSZDREREREQipSZDREREREQipSZDREREREQi9f8BkEvwVX6bgOoAAAAASUVORK5CYII=\n",
      "text/plain": [
       "<Figure size 1296x216 with 3 Axes>"
      ]
     },
     "metadata": {
      "needs_background": "light"
     },
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<div class=\"toyplot\" id=\"t74bbd33a38174446b8ad2205b62cbd32\" style=\"text-align:center\"><svg class=\"toyplot-canvas-Canvas\" xmlns:toyplot=\"http://www.sandia.gov/toyplot\" xmlns:xlink=\"http://www.w3.org/1999/xlink\" xmlns=\"http://www.w3.org/2000/svg\" width=\"500.0px\" height=\"500.0px\" viewBox=\"0 0 500.0 500.0\" preserveAspectRatio=\"xMidYMid meet\" style=\"background-color:transparent;border-color:#292724;border-style:none;border-width:1.0;fill:rgb(16.1%,15.3%,14.1%);fill-opacity:1.0;font-family:Helvetica;font-size:12px;opacity:1.0;stroke:rgb(16.1%,15.3%,14.1%);stroke-opacity:1.0;stroke-width:1.0\" id=\"t5642e9c475174b57a764aaae5891e6a5\"><g class=\"toyplot-coordinates-Cartesian\" id=\"te021484d03a24439822b8d4fa1ebdf78\"><clipPath id=\"t8632d2a93fe8446bac96d5b1b1d56d07\"><rect x=\"30.0\" y=\"30.0\" width=\"440.0\" height=\"440.0\"></rect></clipPath><g clip-path=\"url(#t8632d2a93fe8446bac96d5b1b1d56d07)\"><g class=\"toytree-mark-Toytree\" id=\"t4bc6ff116c01439daf25cab87c130ce2\"><g class=\"toytree-Edges\" style=\"fill:none;stroke:rgb(14.9%,14.9%,14.9%);stroke-linecap:round;stroke-opacity:1;stroke-width:2\"><path d=\"M 70.8 217.0 L 70.8 390.8 L 163.0 390.8\" id=\"8,7\" style=\"stroke-width:2.978498023910654\"></path><path d=\"M 163.0 390.8 L 163.0 344.5 L 255.2 344.5\" id=\"7,6\" style=\"stroke-width:2.098151367786139\"></path><path d=\"M 163.0 390.8 L 163.0 437.2 L 255.2 437.2\" id=\"7,5\" style=\"stroke-width:1.638978821855166\"></path><path d=\"M 70.8 217.0 L 70.8 66.3 L 163.0 66.3\" id=\"8,4\" style=\"stroke-width:2.266504111109553\"></path><path d=\"M 70.8 217.0 L 70.8 159.0 L 163.0 159.0\" id=\"8,3\" style=\"stroke-width:1.6882100868298053\"></path><path d=\"M 70.8 217.0 L 70.8 251.7 L 163.0 251.7\" id=\"8,2\" style=\"stroke-width:1.639077354848528\"></path><path d=\"M 255.2 344.5 L 255.2 344.5 L 347.4 344.5\" id=\"6,1\" style=\"stroke-width:1.9491421986454887\"></path><path d=\"M 255.2 437.2 L 255.2 437.2 L 347.4 437.2\" id=\"5,0\" style=\"stroke-width:1.5330220473703373\"></path></g><g class=\"toytree-AlignEdges\" style=\"stroke:rgb(66.3%,66.3%,66.3%);stroke-dasharray:2, 4;stroke-linecap:round;stroke-opacity:1.0;stroke-width:2\"><path d=\"M 347.4 437.2 L 347.4 437.2\"></path><path d=\"M 347.4 344.5 L 347.4 344.5\"></path><path d=\"M 347.4 251.7 L 163.0 251.7\"></path><path d=\"M 347.4 159.0 L 163.0 159.0\"></path><path d=\"M 347.4 66.3 L 163.0 66.3\"></path></g><g class=\"toytree-Nodes\" style=\"fill:rgb(40%,76.1%,64.7%);fill-opacity:1.0;stroke:None;stroke-width:1\"><g fill=\"rgb(56.5%,93.3%,56.5%)\" fill-opacity=\"1.0\" id=\"node-0\" transform=\"translate(347.444,437.174)\"><circle r=\"6.599066142111012\"></circle></g><g fill=\"rgb(67.8%,84.7%,90.2%)\" fill-opacity=\"1.0\" id=\"node-1\" transform=\"translate(347.444,344.460)\"><circle r=\"7.847426595936466\"></circle></g><g fill=\"rgb(12.5%,69.8%,66.7%)\" fill-opacity=\"1.0\" id=\"node-2\" transform=\"translate(162.983,251.745)\"><circle r=\"6.917232064545584\"></circle></g><g fill=\"rgb(67.8%,84.7%,90.2%)\" fill-opacity=\"1.0\" id=\"node-3\" transform=\"translate(162.983,159.031)\"><circle r=\"7.064630260489416\"></circle></g><g fill=\"rgb(56.5%,93.3%,56.5%)\" fill-opacity=\"1.0\" id=\"node-4\" transform=\"translate(162.983,66.317)\"><circle r=\"8.799512333328659\"></circle></g><g fill=\"rgb(67.8%,84.7%,90.2%)\" fill-opacity=\"1.0\" id=\"node-5\" transform=\"translate(255.213,437.174)\"><circle r=\"6.916936465565498\"></circle></g><g fill=\"rgb(56.5%,93.3%,56.5%)\" fill-opacity=\"1.0\" id=\"node-6\" transform=\"translate(255.213,344.460)\"><circle r=\"8.294454103358417\"></circle></g><g fill=\"rgb(82.7%,82.7%,82.7%)\" fill-opacity=\"1.0\" id=\"node-7\" transform=\"translate(162.983,390.817)\"><circle r=\"10.935494071731963\"></circle></g><g fill=\"rgb(100%,75.3%,79.6%)\" fill-opacity=\"1.0\" id=\"node-8\" transform=\"translate(70.752,216.978)\"><circle r=\"15.0\"></circle></g></g><g class=\"toytree-NodeLabels\" style=\"fill:rgb(0%,0%,0%);fill-opacity:1.0;font-size:20px;stroke:none\"><g transform=\"translate(341.88,442.28)\"><title>idx: 0\n",
       "dist: 1.0000\n",
       "support: 0.0000\n",
       "height: 0.0000\n",
       "name: 42</title><text>1</text></g><g transform=\"translate(341.88,349.57)\"><title>idx: 1\n",
       "dist: 1.0000\n",
       "support: 0.0000\n",
       "height: 0.0000\n",
       "name: 38</title><text>2</text></g><g transform=\"translate(157.42,256.86)\"><title>idx: 2\n",
       "dist: 1.0000\n",
       "support: 0.0000\n",
       "height: 2.0000\n",
       "name: 5</title><text>4</text></g><g transform=\"translate(157.42,164.14)\"><title>idx: 3\n",
       "dist: 1.0000\n",
       "support: 0.0000\n",
       "height: 2.0000\n",
       "name: 3</title><text>2</text></g><g transform=\"translate(157.42,71.43)\"><title>idx: 4\n",
       "dist: 1.0000\n",
       "support: 0.0000\n",
       "height: 2.0000\n",
       "name: 2</title><text>1</text></g><g transform=\"translate(249.65,442.28)\"><title>idx: 5\n",
       "dist: 1.0000\n",
       "support: 0.0000\n",
       "height: 1.0000\n",
       "name: 8</title><text>2</text></g><g transform=\"translate(249.65,349.57)\"><title>idx: 6\n",
       "dist: 1.0000\n",
       "support: 0.0000\n",
       "height: 1.0000\n",
       "name: 7</title><text>1</text></g><g transform=\"translate(157.42,395.93)\"><title>idx: 7\n",
       "dist: 1.0000\n",
       "support: 0.0000\n",
       "height: 2.0000\n",
       "name: 1</title><text>0</text></g></g><g class=\"toytree-TipLabels\" style=\"fill:rgb(14.9%,14.9%,14.9%);fill-opacity:1.0;font-family:helvetica;font-size:11px;font-weight:normal;stroke:none;white-space:pre\"><g transform=\"translate(347.44,437.17)rotate(0)\"><text x=\"15.00\" y=\"2.81\" style=\"\">(0, 2, 1): 0.1066</text></g><g transform=\"translate(347.44,344.46)rotate(0)\"><text x=\"15.00\" y=\"2.81\" style=\"\">(0, 1, 2): 0.1898</text></g><g transform=\"translate(347.44,251.75)rotate(0)\"><text x=\"15.00\" y=\"2.81\" style=\"\">(4,): 0.1278</text></g><g transform=\"translate(347.44,159.03)rotate(0)\"><text x=\"15.00\" y=\"2.81\" style=\"\">(2,): 0.1376</text></g><g transform=\"translate(347.44,66.32)rotate(0)\"><text x=\"15.00\" y=\"2.81\" style=\"\">(1,): 0.2533</text></g></g></g></g></g></svg><div class=\"toyplot-behavior\"><script>(function()\n",
       "{\n",
       "var modules={};\n",
       "})();</script></div></div>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "time: 1.29 s\n"
     ]
    }
   ],
   "source": [
    "print(\"Regions: \", ws.region)\n",
    "print(\"-------------------------------------------------------------------\")\n",
    "monitor = HIMO(LTL_formula, ws, alpha=1, beta_high=1, beta_low=1, epsilon=0.3, tree_depth=4)\n",
    "monitor.add_observations([(0,1),(1,5)])\n",
    "    \n",
    "monitor.prediction(300, 5)\n",
    "monitor.plot(tree_prob_threshold=0.1, tree_height=500, tree_width=500)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "be9f5e4c-f03a-4dbe-afeb-1f736ed7a86d",
   "metadata": {},
   "source": [
    "---"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "notebook",
   "language": "python",
   "name": "notebook"
  },
  "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.8.0"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}