Last active
April 15, 2020 04:34
-
-
Save mvcisback/f62056f5257691160f3a0e99c6539394 to your computer and use it in GitHub Desktop.
CAV2020 Artifact Evaluation for Learning from Demos
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # Start from a core stack version | |
| FROM jupyter/scipy-notebook:dc9744740e12 | |
| USER root | |
| RUN apt-get update && apt-get install -y \ | |
| zlib1g-dev \ | |
| graphviz | |
| USER jovyan | |
| # Install from requirements.txt file | |
| COPY requirements.txt /tmp/ | |
| COPY experiment.ipynb /home/jovyan/ | |
| RUN pip install wheel | |
| RUN pip install --requirement /tmp/requirements.txt |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "cells": [ | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "# CAV 2020 Artifact\n", | |
| "\n", | |
| "- paper: **Learning Task Specifications from Demonstrations via the Principle of Maximum Causal Entropy**\n", | |
| "- authors: Marcell Vazquez-Chanlatte, Sanjit A. Seshia\n", | |
| "\n", | |
| "\n", | |
| "This notebook is designed to be run sequentially; however the majority of the notebook is setup for the final section on actually performing inference. As such, we have provided the following TOC to get an overview of the notebook.\n", | |
| "\n", | |
| "## TOC:\n", | |
| "1. [Dynamical System](#1.-Create-Dynamical-System)\n", | |
| "2. [Sensor and Visualizing the Map](#2.-Create-Sensor-+-Visualize-Map)\n", | |
| "3. [Demonstrations](#3.-Describe-demonstrations)\n", | |
| "4. [Concept Class](#4.-Define-Specification-Circuits)\n", | |
| "5. [Specification Inference](#5.-Run-Maximum-Casual-Entropy-Specification-Inference)" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": null, | |
| "metadata": {}, | |
| "outputs": [], | |
| "source": [ | |
| "import aiger as A\n", | |
| "import aiger_bv as BV\n", | |
| "import aiger_coins as C\n", | |
| "import aiger_gridworld as GW\n", | |
| "import aiger_ptltl as LTL\n", | |
| "import funcy as fn\n", | |
| "import matplotlib.pyplot as plt\n", | |
| "import seaborn as sns\n", | |
| "from bidict import bidict" | |
| ] | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "# 1. Create Dynamical System\n", | |
| "\n", | |
| "Here we create a BitVector sequential circuit, `DYN`, using `py-aiger`, the models a gridworld (line 4).\n", | |
| "\n", | |
| "Afterwords, lines 6-8 describe introducing a slip probability of `1/32` (modeled by a biased coin with bias `31/32`). \n", | |
| "\n", | |
| "**Note that states are 1-hot encoded**" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 2, | |
| "metadata": {}, | |
| "outputs": [], | |
| "source": [ | |
| "X = BV.atom(8, 'x', signed=False)\n", | |
| "Y = BV.atom(8, 'y', signed=False)\n", | |
| "\n", | |
| "DYN = GW.gridworld(8, start=(3, 5), compressed_inputs=True)\n", | |
| "\n", | |
| "SLIP = BV.atom(1, 'c', signed=False).repeat(2) & BV.atom(2, 'a', signed=False)\n", | |
| "SLIP = SLIP.with_output('a').aigbv\n", | |
| "DYN2 = C.coin((31, 32), 'c') >> C.circ2mdp(DYN << SLIP)\n", | |
| "\n", | |
| "def encode_state(x, y):\n", | |
| " x, y = [BV.encode_int(8, 1 << (v - 1), signed=False) for v in (x, y)]\n", | |
| " return {'x': tuple(x), 'y': tuple(y)}" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 3, | |
| "metadata": {}, | |
| "outputs": [ | |
| { | |
| "data": { | |
| "text/plain": [ | |
| "{'x': (False, True, False, False, False, False, False, False),\n", | |
| " 'y': (False, False, True, False, False, False, False, False)}" | |
| ] | |
| }, | |
| "execution_count": 3, | |
| "metadata": {}, | |
| "output_type": "execute_result" | |
| } | |
| ], | |
| "source": [ | |
| "encode_state(2, 3)" | |
| ] | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "# 2. Create Sensor / Feature overlay\n", | |
| "\n", | |
| "Next, we define the mapping from concrete states to sensor values / atomic predicates.\n", | |
| "We use simple coordinate wise bitvector masks to encode the color overlays." | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 4, | |
| "metadata": {}, | |
| "outputs": [], | |
| "source": [ | |
| "def mask_test(xmask, ymask):\n", | |
| " return ((X & xmask) !=0) & ((Y & ymask) != 0)\n", | |
| "\n", | |
| "\n", | |
| "APS = { # x-axis y-axis\n", | |
| " 'yellow': mask_test(0b1000_0001, 0b1000_0001),\n", | |
| " 'blue': mask_test(0b0001_1000, 0b0011100),\n", | |
| " 'brown': mask_test(0b0011_1100, 0b1000_0001),\n", | |
| " 'red': mask_test(0b1000_0001, 0b0100_1100) \\\n", | |
| " | mask_test(0b0100_0010, 0b1100_1100),\n", | |
| "}\n", | |
| "\n", | |
| "def create_sensor(aps):\n", | |
| " sensor = BV.aig2aigbv(A.empty())\n", | |
| " for name, ap in APS.items():\n", | |
| " sensor |= ap.with_output(name).aigbv\n", | |
| " return sensor\n", | |
| "\n", | |
| "\n", | |
| "SENSOR = create_sensor(APS)" | |
| ] | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "## Visualizing Overlay\n", | |
| "\n", | |
| "This can all seem pretty abstract, so let's visualize the way the sensor sees the board." | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 5, | |
| "metadata": {}, | |
| "outputs": [ | |
| { | |
| "data": { | |
| "text/html": [ | |
| "<text style='border: solid 1px;background-color:#ffff8c'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:#ffb081'> </text> <text style='border: solid 1px;background-color:#ffb081'> </text> <text style='border: solid 1px;background-color:#ffb081'> </text> <text style='border: solid 1px;background-color:#ffb081'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:#ffff8c'> </text>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| }, | |
| { | |
| "data": { | |
| "text/html": [ | |
| "<text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| }, | |
| { | |
| "data": { | |
| "text/html": [ | |
| "<text style='border: solid 1px;background-color:#ff5454'> </text> <text style='border: solid 1px;background-color:#ff5454'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:#9595ff'> </text> <text style='border: solid 1px;background-color:#9595ff'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:#ff5454'> </text> <text style='border: solid 1px;background-color:#ff5454'> </text>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| }, | |
| { | |
| "data": { | |
| "text/html": [ | |
| "<text style='border: solid 1px;background-color:#ff5454'> </text> <text style='border: solid 1px;background-color:#ff5454'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:#9595ff'> </text> <text style='border: solid 1px;background-color:#9595ff'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:#ff5454'> </text> <text style='border: solid 1px;background-color:#ff5454'> </text>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| }, | |
| { | |
| "data": { | |
| "text/html": [ | |
| "<text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:#9595ff'> </text> <text style='border: solid 1px;background-color:#9595ff'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| }, | |
| { | |
| "data": { | |
| "text/html": [ | |
| "<text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| }, | |
| { | |
| "data": { | |
| "text/html": [ | |
| "<text style='border: solid 1px;background-color:#ff5454'> </text> <text style='border: solid 1px;background-color:#ff5454'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:white'> </text> <text style='border: solid 1px;background-color:#ff5454'> </text> <text style='border: solid 1px;background-color:#ff5454'> </text>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| }, | |
| { | |
| "data": { | |
| "text/html": [ | |
| "<text style='border: solid 1px;background-color:#ffff8c'> </text> <text style='border: solid 1px;background-color:#ff5454'> </text> <text style='border: solid 1px;background-color:#ffb081'> </text> <text style='border: solid 1px;background-color:#ffb081'> </text> <text style='border: solid 1px;background-color:#ffb081'> </text> <text style='border: solid 1px;background-color:#ffb081'> </text> <text style='border: solid 1px;background-color:#ff5454'> </text> <text style='border: solid 1px;background-color:#ffff8c'> </text>" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| } | |
| ], | |
| "source": [ | |
| "from IPython.display import HTML as html_print\n", | |
| "\n", | |
| "\n", | |
| "COLOR_ALIAS = {\n", | |
| " 'yellow': '#ffff8c', 'brown': '#ffb081',\n", | |
| " 'red': '#ff5454', 'blue': '#9595ff'\n", | |
| "}\n", | |
| "\n", | |
| "\n", | |
| "def tile(color='black'):\n", | |
| " color = COLOR_ALIAS.get(color, color)\n", | |
| " s = ' '*4\n", | |
| " return f\"<text style='border: solid 1px;background-color:{color}'>{s}</text>\"\n", | |
| "\n", | |
| "\n", | |
| "def ap_at_state(x, y, in_ascii=False):\n", | |
| " \"\"\"Use sensor to create colored tile.\"\"\"\n", | |
| " state = encode_state(x, y)\n", | |
| " obs = SENSOR(state)[0] # <---------- \n", | |
| "\n", | |
| " for k in COLOR_ALIAS.keys():\n", | |
| " if obs[k][0]:\n", | |
| " return tile(k)\n", | |
| " return tile('white')\n", | |
| "\n", | |
| "def print_map():\n", | |
| " \"\"\"Scan the board row by row and print colored tiles.\"\"\"\n", | |
| " order = range(1, 9)\n", | |
| " for y in order:\n", | |
| " chars = (ap_at_state(x, y, in_ascii=True) for x in order)\n", | |
| " display(html_print(' '.join(chars)))\n", | |
| " \n", | |
| "print_map()" | |
| ] | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "# 3. Describe demonstrations\n", | |
| "\n", | |
| "We now encode a collection of demonstrations from an agent attempting to:\n", | |
| "\n", | |
| "1. Avoid the red tiles (lava).\n", | |
| "2. Reach the yellow tiles (recharge).\n", | |
| "3. If the agent touches a blue tile (water), then it must dry off (brown tile) before recharging.\n", | |
| "\n", | |
| "**Note** Trace 5 corresponds to a very unlikely demonstration where the agent enters the water, but is unable to dry off due to wind." | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 21, | |
| "metadata": {}, | |
| "outputs": [ | |
| { | |
| "data": { | |
| "text/html": [ | |
| "trc 0: →<text style='border: solid 1px;background-color:#9595ff'> </text>→<text style='border: solid 1px;background-color:#9595ff'> </text>↑<text style='border: solid 1px;background-color:#9595ff'> </text>↑<text style='border: solid 1px;background-color:#9595ff'> </text>↑<text style='border: solid 1px;background-color:white'> </text>↑<text style='border: solid 1px;background-color:#ffb081'> </text>→<text style='border: solid 1px;background-color:#ffb081'> </text>→<text style='border: solid 1px;background-color:white'> </text>→<text style='border: solid 1px;background-color:#ffff8c'> </text>\n" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| }, | |
| { | |
| "data": { | |
| "text/html": [ | |
| "trc 1: ↑<text style='border: solid 1px;background-color:white'> </text>↑<text style='border: solid 1px;background-color:white'> </text>↑<text style='border: solid 1px;background-color:white'> </text>↑<text style='border: solid 1px;background-color:#ffb081'> </text>←<text style='border: solid 1px;background-color:white'> </text>←<text style='border: solid 1px;background-color:#ffff8c'> </text>←<text style='border: solid 1px;background-color:#ffff8c'> </text>←<text style='border: solid 1px;background-color:#ffff8c'> </text>←<text style='border: solid 1px;background-color:#ffff8c'> </text>\n" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| }, | |
| { | |
| "data": { | |
| "text/html": [ | |
| "trc 2: ←<text style='border: solid 1px;background-color:white'> </text>→<text style='border: solid 1px;background-color:white'> </text>↑<text style='border: solid 1px;background-color:white'> </text>↑<text style='border: solid 1px;background-color:white'> </text>↑<text style='border: solid 1px;background-color:white'> </text>←<text style='border: solid 1px;background-color:white'> </text>↑<text style='border: solid 1px;background-color:white'> </text>←<text style='border: solid 1px;background-color:#ffff8c'> </text>←<text style='border: solid 1px;background-color:#ffff8c'> </text>\n" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| }, | |
| { | |
| "data": { | |
| "text/html": [ | |
| "trc 3: ↑<text style='border: solid 1px;background-color:white'> </text>↑<text style='border: solid 1px;background-color:white'> </text>→<text style='border: solid 1px;background-color:#9595ff'> </text>←<text style='border: solid 1px;background-color:white'> </text>↑<text style='border: solid 1px;background-color:white'> </text>↑<text style='border: solid 1px;background-color:#ffb081'> </text>←<text style='border: solid 1px;background-color:white'> </text>←<text style='border: solid 1px;background-color:#ffff8c'> </text>←<text style='border: solid 1px;background-color:#ffff8c'> </text>\n" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| }, | |
| { | |
| "data": { | |
| "text/html": [ | |
| "trc 4: ↑<text style='border: solid 1px;background-color:white'> </text>→<text style='border: solid 1px;background-color:#9595ff'> </text>↑<text style='border: solid 1px;background-color:#9595ff'> </text>↑<text style='border: solid 1px;background-color:white'> </text>↑<text style='border: solid 1px;background-color:#ffb081'> </text>←<text style='border: solid 1px;background-color:#ffb081'> </text>←<text style='border: solid 1px;background-color:white'> </text>←<text style='border: solid 1px;background-color:#ffff8c'> </text>←<text style='border: solid 1px;background-color:#ffff8c'> </text>\n" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| }, | |
| { | |
| "data": { | |
| "text/html": [ | |
| "trc 5: ↑<text style='border: solid 1px;background-color:white'> </text>→<text style='border: solid 1px;background-color:#9595ff'> </text>↑<text style='border: solid 1px;background-color:#9595ff'> </text>↑<text style='border: solid 1px;background-color:white'> </text>←<text style='border: solid 1px;background-color:white'> </text>←<text style='border: solid 1px;background-color:white'> </text>←<text style='border: solid 1px;background-color:white'> </text>↑<text style='border: solid 1px;background-color:#ffff8c'> </text>↑<text style='border: solid 1px;background-color:#ffff8c'> </text>\n" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| } | |
| ], | |
| "source": [ | |
| "def print_trc(trc, idx=0):\n", | |
| " actions, states = trc\n", | |
| " obs = (ap_at_state(*pos, in_ascii=True) for pos in states)\n", | |
| " display(\n", | |
| " html_print(f'trc {idx}: ' + ''.join(''.join(x) for x in zip(actions, obs)) + '\\n')\n", | |
| " )\n", | |
| "\n", | |
| "ACTIONS0 = \"→→↑↑↑↑→→→\"\n", | |
| "STATES0 = ((4, 5), (5, 5), (5, 4), (5, 3),(5, 2), (5, 1), (6, 1), (7, 1), (8, 1))\n", | |
| "TRC0 = (ACTIONS0, STATES0)\n", | |
| "print_trc(TRC0, 0)\n", | |
| "\n", | |
| "ACTIONS1 = \"↑↑↑↑←←←←←\"\n", | |
| "STATES1 = ((3, 4), (3, 3), (3, 2), (3, 1), (2, 1), (1, 1), (1, 1), (1, 1), (1, 1),)\n", | |
| "TRC1 = (ACTIONS1, STATES1)\n", | |
| "print_trc(TRC1, 1)\n", | |
| "\n", | |
| "ACTIONS2 = \"←→↑↑↑←↑←←\"\n", | |
| "STATES2 = ((2, 5), (3, 5), (3, 4), (3, 3), (3, 2), (2, 2), (2, 1), (1, 1), (1, 1))\n", | |
| "TRC2 = (ACTIONS2, STATES2)\n", | |
| "print_trc(TRC2, 2)\n", | |
| "\n", | |
| "ACTIONS3 = \"↑↑→←↑↑←←←\"\n", | |
| "STATES3 = ((3, 4), (3, 3), (4, 3), (3, 3), (3, 2), (3, 1), (2, 1), (1, 1), (1, 1))\n", | |
| "TRC3 = (ACTIONS3, STATES3)\n", | |
| "print_trc(TRC3, 3)\n", | |
| "\n", | |
| "ACTIONS4 = \"↑→↑↑↑←←←←\"\n", | |
| "STATES4 = ((3, 4), (4, 4), (4, 3), (4, 2), (4, 1), (3, 1), (2, 1), (1, 1), (1, 1))\n", | |
| "TRC4 = (ACTIONS4, STATES4)\n", | |
| "print_trc(TRC4, 4)\n", | |
| "\n", | |
| "ACTIONS5 = \"↑→↑↑←←←↑↑\"\n", | |
| "STATES5 = ((3, 4), (4, 4), (4, 3), (4, 2), (3, 2), (2, 2), (1, 2), (1, 1), (1, 1))\n", | |
| "TRC5 = (ACTIONS5, STATES5)\n", | |
| "print_trc(TRC5, 5)\n", | |
| "\n", | |
| "TRACES = [TRC0, TRC1, TRC2, TRC3, TRC4] # Variety of positive demos.\n", | |
| "TRACES += [TRC5] # Unlucky, Negative Demonstration.\n", | |
| "TRACES += 4 * [TRC4] # Additional \"Safe\" Demonstrations." | |
| ] | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "## Convert \"human readable\" demos to bitvectors.\n", | |
| "\n", | |
| "We need to put the traces in a form that the dynamcs understands (namely Tuples of `bool`s (or `0, 1`).\n", | |
| "\n", | |
| "As before, the positions, `x, y` are 1-hot encoded. The actions bitvectors are simply mapped to the corresponding action in the `aiger_gridworld` module." | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 22, | |
| "metadata": {}, | |
| "outputs": [ | |
| { | |
| "data": { | |
| "text/plain": [ | |
| "([{'a': (1, 0)},\n", | |
| " {'a': (1, 0)},\n", | |
| " {'a': (0, 1)},\n", | |
| " {'a': (0, 1)},\n", | |
| " {'a': (0, 1)},\n", | |
| " {'a': (0, 1)},\n", | |
| " {'a': (1, 0)},\n", | |
| " {'a': (1, 0)},\n", | |
| " {'a': (1, 0)}],\n", | |
| " [{'x': (False, False, False, True, False, False, False, False),\n", | |
| " 'y': (False, False, False, False, True, False, False, False)},\n", | |
| " {'x': (False, False, False, False, True, False, False, False),\n", | |
| " 'y': (False, False, False, False, True, False, False, False)},\n", | |
| " {'x': (False, False, False, False, True, False, False, False),\n", | |
| " 'y': (False, False, False, True, False, False, False, False)},\n", | |
| " {'x': (False, False, False, False, True, False, False, False),\n", | |
| " 'y': (False, False, True, False, False, False, False, False)},\n", | |
| " {'x': (False, False, False, False, True, False, False, False),\n", | |
| " 'y': (False, True, False, False, False, False, False, False)},\n", | |
| " {'x': (False, False, False, False, True, False, False, False),\n", | |
| " 'y': (True, False, False, False, False, False, False, False)},\n", | |
| " {'x': (False, False, False, False, False, True, False, False),\n", | |
| " 'y': (True, False, False, False, False, False, False, False)},\n", | |
| " {'x': (False, False, False, False, False, False, True, False),\n", | |
| " 'y': (True, False, False, False, False, False, False, False)},\n", | |
| " {'x': (False, False, False, False, False, False, False, True),\n", | |
| " 'y': (True, False, False, False, False, False, False, False)}])" | |
| ] | |
| }, | |
| "execution_count": 22, | |
| "metadata": {}, | |
| "output_type": "execute_result" | |
| } | |
| ], | |
| "source": [ | |
| "ACTION2ARROW = bidict({\n", | |
| " GW.NORTH_C: '↑',\n", | |
| " GW.SOUTH_C: '↓',\n", | |
| " GW.WEST_C: '←',\n", | |
| " GW.EAST_C: '→',\n", | |
| "})\n", | |
| "\n", | |
| "def str2actions(vals):\n", | |
| " return [ACTION2ARROW.inv[c] for c in vals]\n", | |
| "\n", | |
| "def encode_trace(trc):\n", | |
| " actions, states = trc\n", | |
| " actions = str2actions(actions)\n", | |
| " actions = [{'a': a} for a in actions]\n", | |
| " states = [encode_state(*s) for s in states]\n", | |
| " return actions, states\n", | |
| "\n", | |
| "encode_trace(TRC0)" | |
| ] | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "# 4. Define Specification Circuits / Concept Class\n", | |
| "\n", | |
| "First, we describe the properties over colors of the map. This is done in past tense temporal logic using `py-aiger-ptltl`." | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 23, | |
| "metadata": {}, | |
| "outputs": [], | |
| "source": [ | |
| "LAVA, RECHARGE, WATER, DRY = map(LTL.atom, ['red', 'yellow', 'blue', 'brown'])\n", | |
| "\n", | |
| "EVENTUALLY_RECHARGE = RECHARGE.once()\n", | |
| "AVOID_LAVA = (~LAVA).historically()\n", | |
| "\n", | |
| "RECHARGED_AND_ONCE_WET = RECHARGE & WATER.once()\n", | |
| "DRIED_OFF = (~WATER).since(DRY)\n", | |
| "\n", | |
| "DIDNT_RECHARGE_WHILE_WET = (RECHARGED_AND_ONCE_WET).implies(DRIED_OFF)\n", | |
| "DONT_RECHARGE_WHILE_WET = DIDNT_RECHARGE_WHILE_WET.historically()\n", | |
| "\n", | |
| "CONST_TRUE = LTL.atom(True)\n", | |
| "\n", | |
| "\n", | |
| "SPECS = [\n", | |
| " CONST_TRUE, AVOID_LAVA, EVENTUALLY_RECHARGE, DONT_RECHARGE_WHILE_WET,\n", | |
| " AVOID_LAVA & EVENTUALLY_RECHARGE & DONT_RECHARGE_WHILE_WET,\n", | |
| " AVOID_LAVA & EVENTUALLY_RECHARGE,\n", | |
| " AVOID_LAVA & DONT_RECHARGE_WHILE_WET,\n", | |
| " EVENTUALLY_RECHARGE & DONT_RECHARGE_WHILE_WET,\n", | |
| "]\n", | |
| "\n", | |
| "SPEC_NAMES = [\n", | |
| " \"CONST_TRUE\", \"AVOID_LAVA\", \"EVENTUALLY_RECHARGE\", \"DONT_RECHARGE_WHILE_WET\",\n", | |
| " \"AVOID_LAVA & EVENTUALLY_RECHARGE & DONT_RECHARGE_WHILE_WET\",\n", | |
| " \"AVOID_LAVA & EVENTUALLY_RECHARGE\",\n", | |
| " \"AVOID_LAVA & DONT_RECHARGE_WHILE_WET\",\n", | |
| " \"EVENTUALLY_RECHARGE & DONT_RECHARGE_WHILE_WET\",\n", | |
| "]" | |
| ] | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "## Convert specifications to monitor circuits\n", | |
| "\n", | |
| "Next we preprend the sensor circuit to make these specifications over sequences of positions. The `py-aiger` ecosystem makes this fairly painless." | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 24, | |
| "metadata": {}, | |
| "outputs": [], | |
| "source": [ | |
| "def spec2monitor(spec):\n", | |
| " monitor = spec.aig | A.sink(['red', 'yellow', 'brown', 'blue'])\n", | |
| " monitor = BV.aig2aigbv(monitor)\n", | |
| " return SENSOR >> monitor\n", | |
| " \n", | |
| "SPEC2MONITORS = { spec: spec2monitor(spec) for spec in SPECS }" | |
| ] | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "# 5. Run Maximum Casual Entropy Specification Inference\n", | |
| "\n", | |
| "Finally, we use our maximum causal entropy inference algorithm which computes a BDD representation of the composition of each spec and MDP circuit.\n", | |
| "\n", | |
| "**Note:** Several performance bugs were fixed between this version and the submitted version, resulting in improved BDD construction times.\n", | |
| "\n", | |
| "Package `mce-spec-inference` package available here: https://pypi.org/project/mce-spec-inference/" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 25, | |
| "metadata": { | |
| "scrolled": true | |
| }, | |
| "outputs": [ | |
| { | |
| "name": "stdout", | |
| "output_type": "stream", | |
| "text": [ | |
| "encoding traces\n", | |
| "done encoding traces\n", | |
| "concretizing spec\n", | |
| "concretizing spec\n", | |
| "concretizing spec\n", | |
| "concretizing spec\n", | |
| "done spec\n", | |
| "fitting policy\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 1\n", | |
| "Controller Size: 0\n", | |
| "log_prob: -436.68272375276655\n", | |
| "build spec: 1.0s\n", | |
| "fit: 0.0037s\n", | |
| "surprise: 0.018s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 1.0323832035064697, 'fit': 0.003675222396850586, 'surprise': 0.018192052841186523}\n", | |
| "concretizing spec\n", | |
| "done spec\n", | |
| "fitting policy\n", | |
| "done spec\n", | |
| "done spec\n", | |
| "fitting policy\n", | |
| "fitting policy\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 1628\n", | |
| "Controller Size: 328\n", | |
| "log_prob: -416.140363638969\n", | |
| "build spec: 1.2s\n", | |
| "fit: 0.75s\n", | |
| "surprise: 0.016s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 1.226585865020752, 'fit': 0.7500314712524414, 'surprise': 0.01633596420288086}\n", | |
| "concretizing spec\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 1797\n", | |
| "Controller Size: 348\n", | |
| "log_prob: -464.52300675667044\n", | |
| "build spec: 1.6s\n", | |
| "fit: 0.84s\n", | |
| "surprise: 0.017s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 1.5723936557769775, 'fit': 0.8362810611724854, 'surprise': 0.01737356185913086}\n", | |
| "concretizing spec\n", | |
| "done spec\n", | |
| "fitting policy\n", | |
| "done spec\n", | |
| "fitting policy\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 523\n", | |
| "Controller Size: 118\n", | |
| "log_prob: -406.3010404427357\n", | |
| "build spec: 1.7s\n", | |
| "fit: 0.25s\n", | |
| "surprise: 0.018s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 1.6993613243103027, 'fit': 0.24697279930114746, 'surprise': 0.018005847930908203}\n", | |
| "concretizing spec\n", | |
| "done spec\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "fitting policy\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 850\n", | |
| "Controller Size: 195\n", | |
| "log_prob: -468.3600156772926\n", | |
| "build spec: 1.8s\n", | |
| "fit: 3.1s\n", | |
| "surprise: 0.018s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 1.807154893875122, 'fit': 3.123621940612793, 'surprise': 0.018232107162475586}\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 577\n", | |
| "Controller Size: 132\n", | |
| "log_prob: -384.2062931371331\n", | |
| "build spec: 2.3s\n", | |
| "fit: 2.1s\n", | |
| "surprise: 0.018s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 2.2858481407165527, 'fit': 2.1305387020111084, 'surprise': 0.017897367477416992}\n", | |
| "done spec\n", | |
| "fitting policy\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 1913\n", | |
| "Controller Size: 374\n", | |
| "log_prob: -434.06910537400285\n", | |
| "build spec: 2.2s\n", | |
| "fit: 6.7s\n", | |
| "surprise: 0.021s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 2.1837480068206787, 'fit': 6.7344560623168945, 'surprise': 0.021210193634033203}\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 1842\n", | |
| "Controller Size: 372\n", | |
| "log_prob: -407.4691572492924\n", | |
| "build spec: 1.8s\n", | |
| "fit: 6.3s\n", | |
| "surprise: 0.02s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 1.7971274852752686, 'fit': 6.251629590988159, 'surprise': 0.019525766372680664}\n" | |
| ] | |
| } | |
| ], | |
| "source": [ | |
| "from mce.infer import spec_mle\n", | |
| "\n", | |
| "\n", | |
| "def evaluate_demos(trcs, dynamics=DYN2):\n", | |
| " demos = [encode_trace(trc) for trc in trcs]\n", | |
| " best, spec2score = spec_mle(\n", | |
| " dynamics, demos, SPEC2MONITORS.values(), parallel=True\n", | |
| " )\n", | |
| " \n", | |
| " def normalize(score):\n", | |
| " return score - spec2score[SPEC2MONITORS[CONST_TRUE]]\n", | |
| "\n", | |
| " return fn.lmap(normalize, spec2score.values())\n", | |
| " \n", | |
| "scores1 = evaluate_demos(TRACES)" | |
| ] | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "## Plotting Results\n", | |
| "\n", | |
| "**Remark**: Based on the reviews, we have slightly changed how we present our likelihood results. Namely:\n", | |
| "\n", | |
| "1. Because of the sheer number of possible traces, the log likelihoods are typically **very** small.\n", | |
| "2. As a base line, we compare against the likelihood of generating the demonstrations under uniformly random actions.\n", | |
| "3. **Note** that this is equivilent to the likelihood of the demos under the `CONST_TRUE` specification.\n" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 26, | |
| "metadata": {}, | |
| "outputs": [ | |
| { | |
| "data": { | |
| "image/png": "iVBORw0KGgoAAAANSUhEUgAAAtIAAAEXCAYAAACAp6MwAAAABHNCSVQICAgIfAhkiAAAAAlwSFlzAAALEgAACxIB0t1+/AAAADh0RVh0U29mdHdhcmUAbWF0cGxvdGxpYiB2ZXJzaW9uMy4yLjEsIGh0dHA6Ly9tYXRwbG90bGliLm9yZy+j8jraAAAgAElEQVR4nOzde7zc073/8dcbdau7pNG4JEXcVcjuoSHu50hPKSokQUlvqsfl1K3aRlVPKS3q3oMqKa2Ie4X+KCUuEWWHkLglIq6tNkGp49r4/P5Ya5JvvpnZM3uyd3ay834+HvMw813r+12f9f3OyGfWfGa2IgIzMzMzM2ufpbo6ADMzMzOzxZETaTMzMzOzJjiRNjMzMzNrghNpMzMzM7MmOJE2MzMzM2uCE2kzMzMzsyY4kTYzs25H0jhJ32hy3/UkvSNp6Q6OaYSkBwqP35G0fr4/StKpTRxzzn6SBkl6ttD2gqTdOyL2OjGcIum3Tey3saRJkv4p6ejOiG1BSeorKSQt09WxVCPp/0k6tPD4VEmzJL3WWc/jPM6c5+6SbpF8YpiZmUl6AegFzAbeAW4HjoyIdzphnG9ExF0AEfESsFJHjlFNRHToGBFxP7BxRx6zk30XuCci+nd1IIuriPhC5b6k9YDjgD4R8fe8eYGfY5LGAb+NiMsK43b662Nx4RVpMzNblO2V/9HuD2wNfL+L47GO0wd4spkdF9UV4i62HvB6IYm2hcCJtJmZLfIi4jXgDlJCDYCk7SQ9KOkfkh6XtHO1fSVtIOluSa/nj71/J2m13HYVKQEZmz+u/m7x43xJQyW1lo53jKRb8v3lJJ0l6SVJf5N0saQVGplTHmPDKttXlnSPpPOVbCLpTklvSHpW0gE1jrezpFdKm/tLekLSW5LGSFq+0P+bkp7Lx71FUu9C20BJj+T9HpE0sND2GUn35pKMO4EehbblJf02n+t/5H17VYn1bmAX4MJ83jeStKqkKyXNlPSipJMkLZX7j5A0XtI5kl4HTqlyzKUkfU/S9Dz+tZLWKLRfl0se3pJ0n6TNC20rSDo7j/uWpAdK1/GgfI1nSRpZ7fzn4/ynpKfyuXlV0vHFayPpB/kYL0g6qLBfm88jSXsrlcG8nec3OG8fJ+kbSiU8dwK98/kcpVJZiqQ1JF0h6S+S3pR0c96+uqRb83l/M99fJ7edBgwqXKcL8/Y5z90GrtsDeW5vSpohac4qenfgRNrMzBZ5+R/2LwDP5cdrA7cBpwJrAMcDN0jqWW134HSgN7ApsC45EYuIrwAvkVe+I+LnpX3HAhtL6lfYdiBwdb5/BrARKcHfEFgbOHkB5rkm8CdgfEQcDaxISpCuBj4FDAN+KWmzBg95ADAY+AzwWWBEHmdX0jk5APg08CJwTW5bg3RuzwfWBH4B3JZjI8cykZRA/wSYU6Ob769KOsdrAocD75WDiohdgftJpTorRcRU4IK87/rATsAhwFcLu20LPE8q9zmtylyPAvbJ+/YG3gQuKrT/P6Af6Tw+Cvyu0HYWMAAYSHo+fRf4uNC+A6lsZjfgZEmbVhkf4NfAtyJiZWAL4O5C21qkc7Y26TxdKqlSilPzeSTp34ArgROA1YAdgReKg+aypC8Af8nnc0SV2K4iPZ82z+fgnLx9KeAK0icE65Gu14X5uCOZ9zodWeW4jVy3Z/Pcfw78WpKqHGfxFBG++eabb775tsjdSMnCO8A/gSAlmKvlthOBq0r97wAOzffHkeqeqx13H+Cx0ji7Fx73zeMtkx//Fjg53++X41mRlKD/H7BBYd/PAzNqjDsCeKDwOIAN8/1RwOXAFOCEQp+hwP2l41wC/Kiw36n5/s7AK6V5HVx4/HPg4nz/18DPC20rAR/luX8FeLg05oQc/3rAv4BPFtquJtXQAnwNeBD4bAPXd841ApYGPgQ2K7R/CxhXOHcv1Tne08BuhcefznNapkrf1fL5X5WUSL4HbFWlX+W5sE5h28PAsBoxvJTjXqW0fecq5+1a4If1nkf5ep/TwDksX/9K7Mvkc/ExsHoD16U/8Ga1McrP3Qav23OFthXzvmvVi2NxuXlF2szMFmX7RFrd2xnYhLllBH2A/XP5wD8k/YO0avjp8gEk9ZJ0Tf6o/W1SYtyj3K8NVwPD8/0DgZsj4l2gJykxmFiI4fa8vRlfBFYALi5s6wNsW5rnQaTVzUa8Vrj/LnO/fNabtAoNQKQvcL5OWgmdpy17sdD2ZkT8X6mt4irSG5prcgnBzyV9ooE4ewCfKB2rMmbFy3WO0Qe4qXCeniZ9UbWXpKUlnZHLIt5m7opuj3xbHpjexrFrncey/YD/BF5UKn/5fKGt2nnrTf3n0bp1YmvEusAbEfFmuUHSipIuyWUZbwP3AaupsV/7aOS6zTl3+XUDC+HLvAuLE2kzM1vkRcS9pNXXs/Kml0kr0qsVbp+MiDOq7P5T0irYlhGxCnAwaRVwzuHrDH8n0FNSf1JCXSnrmEVaydy8EMOq0fwvGvyKlED9QdIn87aXgXtL81wpIr7d5BgVfyElngDk8dYEXi23Zevltr8Cqxfiq7QBEBEfRcSPI2IzUpnEnqSP+uuZRVo9Lo5bGXPO4esc42XgC6VztXxEvEp6A7Q3sDtpFbpv3kd57PeBDRqIs00R8UhE7E0qnbiZtOpcUe28/YX6z6OXOyC2l4E1lL8bUHIcqWxl2/z62DFvr7xG2jrvjVy3bs2JtJmZLS7OBf5d0lakVeW9JO2RVxuXz1/oWqfKfiuTSkTeyrXVJ5Ta/0aq76wqIj4CrgPOJNXP3pm3f0xKfs+R9ClItduS9liAOR5Jqicdm79sdiuwkaSvSPpEvn2ujRrdRo0Gviqpv6TlSG82/hwRLwB/yGMeqPyFS2Az4NaIeBFoBX4saVlJOwB7VQ4qaRdJW+bVzLdJSdbH1BERs0lJ52lKX7bsAxxLus6Nujjv3yfH0lPS3rltZeAD0qr7inm+lbE/JpXV/EJS7/x8+nw+Lw3L5+MgSavm58zbzD/3ynkbRHqTcV0Dz6Nfk67VbkpfqFxb0ibtiS0i/kqqEf+l0pcLPyGpkjCvTErk/5Hr439U2r3m66ODrttizYm0mZktFiJiJulLVydHxMukFcYfADNJK24nUP3ftR8D2wBvkb5Ed2Op/XTgpPyx+vE1hr+atJp5XUT8q7D9RNIXIB/KH4vfxQL8lnOkQtLDgFeA35MS0f8gfcnwL6SPyX8GtCvJqzLOXaT63BtIq8wb5DGIiNdJSd5xpMTzu8CeETEr734g6Qtkb5CSrisLh14LuJ6URD4N3Esq92jEUaRa4eeBB0jn/PJ2TOs84Bbgj5L+CTyU4yTH+CJppfSp3FZ0PDAZeCTP62c0lyN9BXghPxcOJ5XhVLxG+gLkX0hfdDw8Ip7JbTWfRxHxMOnLe+eQnsP3Mv8nBo3G9hHwDPB34Dt5+7mkkqJZpPNye2m/84Ah+Vc3zq9y3AW9bos15eJvMzMzM+sESj/N+NuIqPaJiS3GvCJtZmZmZtYEJ9JmZmZmZk1waYeZmZmZWRO8Im1mZmZm1gQn0mZmZmZmTVimqwMwM7OFo0ePHtG3b9+uDsPMbLEyceLEWRFR9S+WOpE2M1tC9O3bl9bW1q4Ow8xssSLpxVptLu0wMzMzM2uCE2kzMzMzsyY4kTYzMzMza4ITaTMzMzOzJjiRNjMzMzNrghNpMzMzM7MmOJE2MzMzM2uCE2kzMzMzsyY4kTYzMzMza4ITaTPrViStJekaSdMlTZT0B0kbSdpc0t2SnpU0TdIPJSnvM0LSx5I+WzjOFEl98/2vSZos6Ym8fW9JF0maJOkpSe/l+5MkDakSU82+kkZJmpEfPy5pt8J+L0jqUXi8s6RbCzHPLBxrkqTNOu/MmplZmf9EuJl1Gzkxvgn4TUQMy9u2AnoBo4BvR8QfJa0I3AD8F3BR3v0VYCQwtHTMdfL2bSLiLUkrAT0j4ve5vS9wa0T0rxVXRBxRq6+kPYETIuJ6SbsAlwL9GpzymIg4ssG+ZmbWwbwibWbdyS7ARxFxcWVDRDwObASMj4g/5m3vAkcC3yvseyuwuaSNS8f8FPBP4J287zsRMaOT4p8ArN2RB5R0mKRWSa0zZ87syEObmS3xnEibWXeyBTCxyvbNy9sjYjqwkqRV8qaPgZ8DPyjt+zjwN2CGpCsk7dWxIc9jMHBzO/oPLZV2rFDuEBGXRkRLRLT07Nmz4yI1MzMn0mZmBVcD20n6TGVDRMwmJbhDgKnAOZJO6eBxz5Q0NY//s8L2qNK3uG1MRPQv3N7r4LjMzKwNTqTNrDt5EhhQZftT5e2S1gfeiYi3K9si4l/A2cCJxb6RPBwRpwPDgP06OO4TImKjPO7lhe2vA6sXHq8BzOrgsc3MrElOpM2sO7kbWE7SYZUN+Zc4ngV2kLR73rYCcD6plKNsFLA70DP37S1pm0J7f+DFTokeLgSWkrRHfjwO+EqOY2ngYOCeThrbzMzayYm0mXUbERHAvsDu+efvngROB14D9gZOkvQsMBl4hJS4lo/xISnJ/lTe9AngLEnPSJpE+lWP/+7E+E8Fvps3/QTYUNLjwGPAc8BvC7uUa6QHdkZcZmZWndL/t83MrLtraWmJ1tbWrg7DzGyxImliRLRUa/OKtJmZmZlZE/wHWczMOpCki4DtS5vPi4gruiIeMzPrPE6kzcw6UOWvGJqZWffn0g4zMzMzsyY4kTYzMzMza4ITaTMzMzOzJjiRNjMzMzNrghNpMzMzM7MmOJE2MzMzM2uCE2kzMzMzsyb4d6TNzKzTvPQ/W3Z1CFay3smTuzoEs27DK9JmZmZmZk1wIm1mZmZm1gQn0mZmZmZmTXAibWZmZmbWBCfSZmZmZmZNcCJtZmZmZtYEJ9JmZmZmZk1wIm1m3Z6kfSSFpE0k/UjS6aX2/pKezvfXkfR7SdMkTZd0nqRlc9vOkm7N90dIminpsdz3DkkD68QxStKQGm39c4yD8+NDJY0u9emRx1wuP75Z0kPNnhczM1swTqTNbEkwHHgg/3c0MLTUPgwYLUnAjcDNEdEP2AhYCTitxnHHRMTWue8ZwI2SNu2AGAFuAv5d0oqFPkOAsRHxgaTVgAHAqpLWb3JMMzNbAE6kzaxbk7QSsAPwdWBYREwF3pS0baHbAaQEe1fg/Yi4AiAiZgPHAF8rJbTziYh7gEuBw5qIUcD+wAhS8rx8RLwN3AvsVeg6LMcJ8GVgLHBN3m5mZguZE2kz6+72Bm7PCfTrkgaQktFhAJK2A96IiGnA5sDE4s45oX0J2LCBsR4FNmkixoHAjIiYDowDvpi3F+PsTVohvzu3VVbXRzN3FXs+kg6T1CqpdebMmU2EZmZmtTiRNrPubjhp1Zb83+HAGGCIpKWYd5V3QanJ/arFCHAbsL2kVUir5jdExGxJvYB+wAP5DcJHkraoduCIuDQiWiKipWfPnk2GZ2Zm1SzT1QGYmXUWSWuQyjW2lBTA0kAAJwAzgJ2A/YDP512eItUhF4+xCrAe8Bzwb3WG3Bp4up0xLp1j2FvSSFIyvqaklSPin5JuB/YlJfzH5t0OAFYHZqSqEFYhJd8j2zO2mZktGK9Im1l3NgS4KiL6RETfiFiXlEAPIq1CnwM8HxGv5P5/AlaUdAjMSXLPBkZFxLttDSRpJ1J99K/aGeNuwBMRsW6OsQ9wAyl5Jsd5LNALmJC3DQcG5/59SV86dJ20mdlC5kTazLqz4aRfvyi6IW+/jlQTPaesIyKClMDuL2kaMBV4H/hBjeMPlTRJ0tTcZ7+IqLcifYmkV/JtQp0YAe4EepN+ISQk9QX6AHN+9i4iZgBvlb5AaWZmnUzp3w0zM+vuWlpaorW1daGO+dL/bLlQx7P61jt5cleHYLZYkTQxIlqqtXlF2szMzMysCf6yoZlZB5N0EbB9afN5ld+nNjOz7sGJtJlZB4uII7o6BjMz63wu7TAzMzMza4ITaTMzMzOzJri0w8zMOo1/IcLMujOvSJuZmZmZNcGJtJmZmZlZE5xIm5mZmZk1wYm0mZmZmVkT/GVDMzOzJcj2F5T/VpBVM/6o8V0dgi0GvCJtZmZmZtYEJ9JmZmZmZk1wIm1mZmZm1gQn0mZmZmZmTXAibWZmZmbWBCfSZmZmZmZNcCJtZmZmZtYEJ9JmSwhJsyVNKty+J+lHkk4v9esv6el8/wVJkwv7nJ+3j5L0qqTl8uMeue+Whb5vSJqR798laWdJt5bGGiVpSOFxD0kfSTq81O8FST1K20ZIujDf/1Tus1ah/SJJ369xLnaW9FaO7RlJZ5WOO7N0rjbLbRtJ+oOkaZIelXStpF4dMLfJkp6QdK+kPoW2XpKulvS8pImSJkjat8ocKrfdq83XzMw6h/8gi9mS472I6F/cIGkj4HagmHAOA0YXHu8SEbOqHG828DXgfysbImIy0D8fexRwa0Rcnx/v3ECM+wMPAcOBixvoXxn375LOAM4CDpa0DTAIGNDGbvdHxJ6SVgAek3RTRFT+AsOYiDiy2FnS8sBtwLERMbYwp54NhtnW3HaJiFmSfgycBHxTkoCbgd9ExIF5vD7Al8pzaHB8MzPrYF6RNluCRcRU4E1J2xY2H8C8iXQt5wLHSOrIN+TDgeOAtSWt0859LwU2kLQLcBFwZER8VG+niHgPmASsXafrgcCEShKd9x0XEVMajK+RuU0oxLEr8GFEzEm6I+LFiLigwfHMzKyTOZE2W3KsUCoDGJq3jyatQiNpO+CNiJhW2O+ewj7HFLa/BDwAfKUjgpO0LvDpiHgYuBYYWmeXeUTEx8C3gRuAZyPivgbHXR3oBxT7Dy2dqxWALYCJbRxqUHEfCivH7ZjbYNIqNMDmwKN1wh9UinODKvM7TFKrpNaZM2fWOZyZmbWHSzvMlhzzlXZkY4AHJR3H/GUdULu0A+B04Pekkod6os72oaQkE+Aa4HLg7AaOO/dAEZMkTQF+2UD3QZIeJyXR50bEa4W2aqUd9Y43T5lFLm2pqDe3eyStAbwD/LDawSVdBOxAWqX+XLUxq4mIS0mr9bS0tNS6BmZm1gSvSJst4SLiZWAGsBOwHymxbnTfaaSyiAMa6P46sHpp2xpAJUkfDoyQ9AJwC/BZSf0ajaXg43yr5/6I2Iq08vt1SdXeZBQ9Sds1122pN7ddgD6kc/njwnjbVDpExBHAbjRek21mZp3MibSZQVqFPgd4PiJeaee+pwHHN9BvGtBb0qYw54tzWwGT8pceV4qItSOib0T0Ja12D29nLO0WETOAM4AT63S9Ghgo6YuVDZJ2lLRFWzs1OreI+BfwHeCQvDp9N7C8pG8Xuq3Y4LTMzGwhcCJttuQo10ifUWi7jrQyW+1LhsUa6SvLjRHxJPVreYmID4CDgStyDfH1wDci4i1SUnlTaZcbmDfZfELSK/n2i7xtRGHbK018QbHiYmBHSX3z43KN9MD8pcQ9gaPyz989BfwXUK/wuJG5ARARfyVdgyMiIoB9gJ2UfkbwYeA3zJvwl2ukh5SPaWZmnUfp/9VmZtbdtbS0RGtra1eHYV1s+wu27+oQFgvjjxpfv5MtESRNjIiWam1ekTYzMzMza4J/tcPMui1JewA/K22eERH7dkU8ZmbWvTiRNrNuKyLuAO7o6jjMzKx7cmmHmZmZmVkTnEibmZmZmTXBpR1mZmZLEP8ahVnH8Yq0mZmZmVkTnEibmZmZmTXBibSZmZmZWROcSJuZmZmZNcFfNjQzs4bcu+NOXR2CdYCd7ru3q0Mw6za8Im1mZmZm1gQn0mZmZmZmTXAibWZmZmbWBCfSZmZmZmZNcCJtZmZmZtYEJ9JmZmZmZk1wIm1mZmZm1gQn0mYLmaTZkiZJelLS45KOk7RUoX0HSQ9LeibfDiu0nSLpXUmfKmx7R9Ka+ZiTJL0m6dXC42XrxDFF0lhJq+XtfSW9V9h/kqRDcttKki6RNF3SREnjJG1biaN0/BGSLixtmyTpmtK2UZJm5LbHJe1WaFtG0k8lTSvEMrLKHCq379WY696Sbi48/r6k5wqP95J0S77/gqQehbadJd1anlO+Fse3cV47OqbJhWOeL+mifP+p0vUaUm08MzPreP6DLGYL33sR0R8gJ8RXA6sAP5K0Vn68T0Q8mhO6OyS9GhG35f1nAccBJ1YOGBGvA5VjngK8ExFntSOO3wBHAKfltumVtpLLgBlAv4j4WNJngM0ambSkTYGlgUGSPhkR/1doPiEirpe0C3Ap0C9vPxVYC9gyIt6XtHKe+3xzqONB4JLC488Db0v6VET8HRiY+3SEzoppl4iYVT6IpL7ArQ2OaWZmHcgr0mZdKCdMhwFHShIpmR0VEY/m9lnAd4HiqublwFBJa3RgKBOAtdvqIGkDYFvgpIj4OMc3o5Dg1zMcuAr4I7B3vTgkrQh8EzgqIt7P4/0zIk5pcLw5ImImKUndMG9aG7iBlKyS/zu+vcddEItiTGZm1j5OpM26WEQ8T1qp/RSwOTCx1KU1b694h5RM/3dHjC9paWA34JbC5g1K5QmDcgyTImJ2jUOtUNwH+J9S+1DgGmA0KamuZjBQKXfYEHgpIv7ZRvgrlOIc2kbf8cBASRsD04CH8uNlgK2ARwp97ynM47I2jtklMUk6ptFgJB0mqVVS68yZM9s5FTMza4tLO8wWT+cDkyTVK99oywo5UVwbeBq4s9A2X2mHpC/VOd48JQ2SRgAt+X4LMCsiXpL0KnC5pDUi4o3c/UxJPwXWIZU4zEfSV0lvHtYEBkbEy+Ux63iQtMq7NGnl+2HgZGBr4JnKqnc2p4xC0s7AfLXQbej0mNojIi4llcvQ0tIS7d3fzMxq84q0WReTtD4wG/g78BQwoNRlAPBkcUNE/INUS33EAgxdSfj6AJWykrY8CWyVV7DbaziwiaQXgOmkmvD9Cu0nRMRGpLrvy/O254D1cl00EXFFjvctUuLZXuNJSetAYEJe6V4e2JmOq4/uDjGZmVmDnEibdSFJPYGLgQsjIoCLgBGSKl8CXBP4GfDzKrv/AvgWC/jJUkS8CxwNHJdLCmr1m04qM/lxrueu/MLHF9s6vtIvkhxA+sJg34joS6qRrlbecSGwlKQ9cly/Bi6UtHw+1tJA1V8hacDTQG9gB+CxvG0ScDhdV4u8KMZkZmYNciJttvBVamifBO4iffnuxwAR8VfgYOBXkp4hrUpeHhFjywfJH/PfBCy3oAFFxGPAE8xNbss10kfn7d8AegHPSZoCjCKtpLdlEPBqRPylsO0+YDNJny7FEaRf6vhu3jQS+CswRdJjwP3Ab4DKscr1yGe0MccA/gy8HhEf5c0TgPVpfvX3JEmvVG6dHFOxRvrKJuM1M7MOpPT/cTMz6+5aWlqitbW16f3v3XGnDozGuspO993b1SGYLVYkTYyIlmptXpE2MzMzM2uCf7XDrBvLNdZ/qtK0W/4jLt2OpJuAz5Q2nxgRd3RFPLBoxmRmZgvOibRZN1b8i4dLiojYt6tjKFsUYzIzswXn0g4zMzMzsyY4kTYzMzMza4JLO8zMrCH+tQczs3l5RdrMzMzMrAlOpM3MzMzMmuBE2szMzMysCU6kzczMzMya4C8bmpmZLUEuPG5sV4dgttAdefZenXJcr0ibmZmZmTXBibSZmZmZWROcSJuZmZmZNcGJtJmZmZlZE5xIm5mZmZk1wYm0mZmZmVkTnEibmZmZmTWhoURa0j6SQtIm+fGPJJ1e6tNf0tP5/jqSfi9pmqTpks6TtGxu21nSrfn+CEkzJT2W+94haWCdWEZJGlKjrX+Oc3B+fKik0aU+PfKYy+XHN0t6qM6Ye0l6StIUSae10a8yn0mF22aSnpe0canvuZJOzOfjrdI+u+c+Ienswj7HSzpF0shC39mF+0dXOz+S3ik9/o6k9yWtWtg257qU+o6T1JLvf1PSmELbKvn6rl/jfIySNCPH9rik3UrHfbYQ+/WFtkPyuZ6cnxvHF47X7Nwq5/gZSWeV9hks6eHcNknSGEnrVZnDJEkP1pjrdnmOkyX9plqfUiyP5fnfJ2nPUp/DcizP5Lh2KJ231sLjlrxtj0KM7xTO7ZV14pjvnNR6Hue2jST9Qen1+qikayX1qvb8KV8vpdfeR5IOL/V7IZ+3JyTdK6lPoa2XpKuVXkMTJU2QtG+VOczz2qky33Mkfafw+A5JlxUeny3pWEl9JU0p7XtKtedg8bVR47x2ZEzvlY55iKQ/5/svla5X32rjmZlZx2t0RXo48ED+L8BoYGipzzBgtCQBNwI3R0Q/YCNgJaBWAjomIrbOfc8AbpS0aTvm0FacNwH/LmnFQp8hwNiI+EDSasAAYFXVSAazc4EvRsQWwGVt9IM0n/6F21PANaTzA4CkpXIc1+RN95f2uStv/wD4sqQexQEi4rRKX+C9wn7n14mtYjjwCPDlBvtXXAasW0gM/ge4PCKeb2OfE3Kc3wEuLrUdVIi9kpx8Iff9j4jYEtgOeKsdMdaa2/05jq2BPSVtn8fbArgAODQiNsl9fgf0Lc8h32q90TsN+E6O+ZQ6Md6fn/MbA0cDFyq/ychJ9beAHSJiE+Bw4GpJaxX2/1Q+T3NExB2F50Qrc8/tIXXimO+cZPM9jyUtD9wG/G9E9IuIbYBfAj3rzLdif+Ah5r4+i3aJiM8C44CT8rkQcDNwX0SsHxEDSK+jdcpzqPLaKRsPDMzHXQroAWxeaB8IVH2T1ITOiGl66ZhXRsS2+fqdzLzX64UOmoeZmdVRN5GWtBKwA/B1cjIYEVOBNyVtW+h6ACnB3hV4PyKuyH1nA8cAXysltPOJiHuAS4HD2juR/I/u/sAIUvK8fES8DdwLFP+czbAcJ6RkayylRLeKD8n/eEfEjPbGxvxvPHYEXoyIF+vs9y/S+TimiTGrkrQB6Y3NSVRPaGqKiCAldufmlbjdgDMb3H0CsHYD/b4PHB8Rf8ljfhARv2pkgEbmFhHvAZMKsZwI/DQini70uSUi7mtkzIKmniMRMYn0huTIQjwnRMSs3P4o8BvgiMJuZwIj2xlfWzGUz0ktBwITImLOn0WLiHERMaWNfYqGA8cBa0tap0af4vNkV+DDiJjzBiwiXoyICxocr+hB4PP5/ubAFOCfklZX+nRqU+DRJtECYsMAACAASURBVI67IBbFmMzMrB0aWZHeG7g9J8+vSxqQt48mJ5+StgPeiIhppH8QJhYPkBPal4ANGxjvUWCTxsKfx0BgRkRMJ61qfbFKnL1JK+R357bhuX00NRKvvFL0FHB5gx+ZDi19BLtCREwGPpa0Ve5TTOYBBpX22aDQdhFwkAqlCgtoGOmNw/3AxpJ6tWfniHgCuAP4E3BURHzY4K6DSauLRb8rzLmSkG9B6flTcmbxXJXa6s5N0upAP6CSKG9O/WSlOObvavSZDvy0/FF/g4rP+fleP6QV5uJK5QTgQ0m7NDHWfKqcE6jyPKb+tRlUujZfKoyxLvDpiHgYuJb5P9GqKD5PGrk2bb125shvzP6lVLIzkHQO/0xKZFuAyYXn8galeRxe7ZhdGZOkQY0Go1Qq1CqpdebMme2cipmZtaWRRHo4c0sQrmFuwjkGGJITzXJiuCDU5H614rwN2F7SKqRV8xsiYnZOsvoBD+Q3CR/lj/nLjgIeB74NjJXUU9LnVKjpLSl/JP5e3j4aGCZpGWAf4LrCPuWPgqdXGvKbkCtJJQCNiDrbhgPXRMTHwA2kVfz2ugh4NSLGNdD3TElTgauBn5XaiqUdJzQ4drHMon+pra25DZL0OPAqcEdEvFY+sKQ1c5IyVbkmtsqYB1XZb29gReA/SWUY/fLzpLXct4ZmnvOnkksgFkBb56TW87gt95euzS2FtqGkBBrmfX1W3CPpVeAL1Ph/iaSLlOrQH6k1ZvG1U8WDpIS1krROKDweX+g3vTSPcklSPZ0eU0Tc32gwEXFpRLREREvPno1W4ZiZWSPaTKQlrUH6ePUySS8AJwAHSFJEvAzMAHYC9iMl1pBWbweUjrMKsB7wXAMxbQ08XbfXvMdfOsdwco7zAmCwpJVzAnA7sC/zJvwHAKsDM/I+fam+Kr0HqUbzLuAnpMT8UOYm7Y26Jo+5O/BERPytHfueSyqt+WQDfV8nzQuYcw1n5ftbkt483JnnPIx2lndkH+dbI06IiI1IJQuXN9D/SUrPn0Y0MLf7I2Ir0irn1yVVkvAngW0AIuL1nDhdSioRaVTlOTKZdJ1+TyrVaPQ5UnzOz/f6yY+fLG6IiLuBFUg15M2qdU5qaeraZMOBEfna3AJ8VlK/QvsuQB9SicmPC+NtU+kQEUeQyomazQYrNclbksooHiKt/nZkfXR3iMnMzBpUb0V6CHBVRPSJiL4RsS4pea58rDgaOAd4PiJeydv+BKwo6RCYk+SeDYyKiHfbGkzSTqT66IZqYgt2IyWn6+Y4+5BWJPctxHks0Iu04gPpH/bBuX9fUoJQrU76MeBgSUtFxLXANFKt6G3tCTCvSs0ifaGyXav3EfEGaTXv6w10H0f6WH7Z/HgEcE++Pxw4pTLniOgN9FbhVxI60YXAUpL2qNPvdNIq9loAkpaV9I0Gjt/Q3HL98hmkxB7g58BIzfsF1zZr+at4jHTOl8srhTeRapjrXmdJnwV+SFrlr8TzM0lr5vb+pGv4yyq7nwp8t52xzqfKOanlamCgpErZFJJ2rPFJDoU+GwErRcTahdfb6ZTexEXEv0hfND0kvwG8G1he0rcL3dp7bYoeBPYklaHNzq+r1UiJa1clrYtiTGZm1qB6ifRwUlJQdANz/wG8jrSaNSdhyF9I2xfYX9I0YCrwPvCDGmNUajGn5j77Fb/4VcMlkl7JtwkNxHkn0Jv0cXXkWuc+pNWfStwzgLc07xcoIf0ag4ApkiYCfwMuIX2EX+38lWtLi7/yMJpUC3tjaZ9yTWW1n/c7m/St/jZFxK2kGuGJub5ze+YmSMOY/zzdxNw3ELsVzusrkipfhLqtsO06mpCfF+XEr1gjfVfu9wdS0n2XpCdJNbKrNDBEvbkVXQzsKKlvXkX+b+BKpZ+MG0/6ktfVhf5nlq7PsqXj/RqYDDyeyzk+DRwPXK/qX7AdpPzzd6QE+uiI+FOe/y2klfsHJT1DelN5cET8tXyQfK46quh1zjnJj+d7HudPd/YEjlL6+bungP9qIIZ6r8858jxHA0fk58w+wE5KP0H4MOmLl8WEv5HXTsVk0mvoodK2tyJ/ubMJ1V4bnRFTuUa60VIvMzPrREr/VpmZWXfX0tISra2Nlu5bd3XhcWPrdzLrZo48e6/6nWqQNDEiqv6YgP+yoZmZmZlZE5bp6gBqkXQRqSyh6LzIv09tiw5fq0VXrkkv/1rKjIjYt1r/xV2uLf9TlabdIuL1hR0PLJoxmZlZx1hkE+n8DX1bDPhaLboi4g7S734vEXJiWu/XRxaqRTEmMzPrGC7tMDMzMzNrghNpMzMzM7MmLLKlHWZmZtbxFuTXC8xsXl6RNjMzMzNrghNpMzMzM7MmOJE2MzMzM2uCE2kzMzMzsyb4y4ZmZmZLkNMOHtLVIVgTRv72+q4OwarwirSZmZmZWROcSJuZmZmZNcGJtJmZmZlZE5xIm5mZmZk1wYm0mZmZmVkTnEibmZmZmTXBibSZmZmZWROcSJuZmZmZNcGJtC32JO0jKSRtkh//SNLppT79JT2d768j6feSpkmaLuk8Scvmtp0l3Zrvj5A0U9Jjue8dkgbWiWWUpKp/7SDHEJIG58eHShpd6tMjj7lcfnyzpIfqjLmXpKckTZF0Whv9KvOZVLhtJul5SRuX+p4r6cR8Pt4q7bN77hOSzi7sc7ykUySNLPSdXbh/dLXzI+md0uPvSHpf0qqFbXOuS6nvOEkt+f43JY0ptK2Sr+/6Nc7HKEkzcmyPS9qtdNxnC7FfX2g7JJ/ryfm5cXzheM3OrXKOn5F0VmmfwZIezm2TJI2RtF6VOUyS9GC1uZqZWedwIm3dwXDggfxfgNHA0FKfYcBoSQJuBG6OiH7ARsBKQK0EdExEbJ37ngHcKGnTDorzJuDfJa1Y6DMEGBsRH0haDRgArForGczOBb4YEVsAl9WJYUxE9C/cngKuIZ0fACQtleO4Jm+6v7TPXXn7B8CXJfUoDhARp1X6Au8V9ju/TmwVw4FHgC832L/iMmDdSqIP/A9weUQ838Y+J+Q4vwNcXGo7qBD7EABJX8h9/yMitgS2A95qR4y15nZ/jmNrYE9J2+fxtgAuAA6NiE1yn98BfctzyLc23+iZmVnHciJtizVJKwE7AF8nJ4MRMRV4U9K2ha4HkBLsXYH3I+KK3Hc2cAzwtVJCO5+IuAe4FDisiTgF7A+MICXPy0fE28C9wF6FrsNynJCSrbGUEt0qPgTWyTHOaG9szP/GY0fgxYh4sc5+/yKdj2OaGLMqSRuQ3ticxNw3HA2JiAAOB87Nq9S7AWc2uPsEYO0G+n0fOD4i/pLH/CAiftXIAI3MLSLeAyYVYjkR+GlEPF3oc0tE3NfImHncwyS1SmqdOXNmo7uZmVkDnEjb4m5v4PacPL8uaUDePpqcfEraDngjIqYBmwMTiwfICe1LwIYNjPcosEkTcQ4EZkTEdGAc8MUqcfYmrZDfnduG5/bR1Ei88urxU8Dlkvo2EMfQUpnGChExGfhY0la5TzGZBxhU2meDQttFwEHFUoUFNIz0xuF+YGNJvdqzc0Q8AdwB/Ak4KiI+bHDXwcDNpW2/K8y5kpBvQen5U3Jm8VyV2urOTdLqQD+gkihvTnrOtaU45u/KjRFxaUS0RERLz5496xzKzMzaw4m0Le6GM7cE4RrmJpxjgCE50SwnhgtCTe5XK87bgO0lrUJaNb8hImbnJKsf8EB+k/BR/pi/7CjgceDbwFhJPSV9rljTW1Iu7Xgvbx8NDJO0DLAPcF1hn3Jpx/RKQ34TciVwdIPnIepsGw5cExEfAzeQVvHb6yLg1YgY10DfMyVNBa4GflZqK5Z2nNDg2MUyi/6ltrbmNkjS48CrwB0R8Vr5wJLWzMny1EpddpUxD2owTjMz6wBOpG2xJWkNUqnGZZJeAE4ADpCkiHgZmAHsBOxHSqwhrd4OKB1nFWA94LkGht0aeLpur3mPv3SO4eQc5wXAYEkr50T2dmBf5k34DwBWB2bkffpSfVV6D+C+XLf8E1Jifihzk/ZGXZPH3B14IiL+1o59zyWV1nyygb6vk+YFzLmGs/L9LUlvHu7Mcx5GO8s7so/zrREnRMRGpBKKyxvo/ySl508jGpjb/RGxFWkF+uuSKkn4k8A2ABHxek7OLyWViJiZWRdzIm2LsyHAVRHRJyL6RsS6pOR5UG4fDZwDPB8Rr+RtfwJWlHQIzElyzwZGRcS7bQ0maSdSfXRDNbEFu5GS03VznH1IK5L7FuI8FuhFqtWFlGQNzv37kpK3anXSjwEHS1oqIq4FpgEHkhLqhuVV5lmkL1S2a/U+It4AriUl0/WMI5WXLJsfjwDuyfeHA6dU5hwRvYHekvq0J54mXQgsJWmPOv1OJ61irwUgaVlJ32jg+A3NLde4n0FK7AF+DowsfcG1zVp+MzNbeJxI2+JsOOmXL4puYO5K33WkFb45iWH+Qtq+wP6SpgFTgfeBH9QYo1JTPDX32a/4xa8aLpH0Sr5NaCDOO4HepLKLyLXOfYA5P3uXE6y3Sl+ghPRrIwKmSJoI/A24BLg6l7XUmk/lVvyVh9Gk+u8bS/uUa6Sr/bzf2UCPKtvnERG3kmqEJ+Ya4u2ZmzQOY/7zdBNz30DsVjivr0j6fN5+W2HbdTQhPy9OBb5b2Fyskb4r9/sDKem+S9KTpPrlVRoYot7cii4GdpTUN9ev/zdwpdLP8Y0HNiWVolScWbo+y1Y5ppmZdQKlfz/MzKy7a2lpidbW1q4Ow7rYaQdX/al7W8SN/G2tr75YZ5M0MSJaqrV5RdrMzMzMrAnLdHUAZosjSReRyhKKzqv8PrUtOnytzMyssziRNmtCRBzR1TFYY3ytzMyss7i0w8zMzMysCV6RNjMzW4L4S2tmHccr0mZmZmZmTXAibWZmZmbWBCfSZmZmZmZNcCJtZmZmZtYEJ9JmZmZmZk3wr3aYmZktQZ4+7e6G+m06ctdOjsRs8ecVaTMzMzOzJjiRNjMzMzNrghNpMzMzM7MmOJE2MzMzM2uCE2kzMzMzsyY4kTYzMzMza4ITaTMzMzOzJjiRtg4haR9JIWmT/PhHkk4v9ekv6el8fx1Jv5c0TdJ0SedJWja37Szp1nx/hKSZkh7Lfe+QNLBOLKMkDanR1j/HOTg/PlTS6FKfHnnM5fLjmyU9VGfMvSQ9JWmKpNPa6NfmfJSclNumSrpH0uaF9hck3VB4PCTP96uSJuXbh5Im5/tn1IljkqRnJB1TaDtF0quF402StFpu+zdJ90l6Ns/hMkkr5uNdWBpjnKSWWue+sH12HmOKpLGVsXJbP0m35ufIxHw+dqwyh8ptsxrzvUnSPoXHz0o6qfD4BklfLj73Cm1znk/FOeVr0aON89qRMb1VOubQwv3XStdr2WrjmZlZx3MibR1lOPBA/i/AaGBoqc8wYLQkATcCN0dEP2AjYCWgVgI6JiK2zn3PAG6UtGkHxXkT8O+SViz0GQKMjYgPclI3AFhV0vptHPdc4IsRsQVwWZ0Y2prPEcBAYKuI2Ag4HbhF0vKF/QeUk7OIuCIi+kdEf+AvwC758ffqxNEf2B4YKWndQts5lePl2z8k9QKuA06MiI0jYmvgdmDlOvOtKJ/7ivfyGFsAb+RzQJ7zbcClEbFBRAwAjgKK12FMKc6naow9nnRekbQm8H/A5wvtnwcebHAe9XRGTPeXjjmmcL0vZt7r9WEHzcPMzOpwIm0LTNJKwA7A10nJMhExFXhT0raFrgeQEuxdgfcj4orcdzZwDPC1UkI7n4i4B7gUOKyJOAXsD4wgJc/LR8TbwL3AXoWuw3KcAF8GxgLXVOZWw4fAOjnGGY3GVGU+JwJHRsS7uf2PpGTqoMJuZwMjGx2jgRheB54DPl2n6xHAbyJiQmHf6yPib/XGqHbua3SdAKyd7x8ETIiIWwrjTYmIUfXGq+JBctKa/zsW6Jk/AfgMKZl/rYnjLohFMSYzM2sHJ9LWEfYGbs/J8+uSBuTto8nJp6TtgDciYhqwOTCxeICc0L4EbNjAeI8CmzQR50BgRkRMB8YBX6wSZ2/SCnnlb+gOz+2jmX8llbzPUsBTwOWS+jYR16PAJpJWAT4ZEc+X2ltJ56ziWmAbSY2cq7okrQcsDzxR2HxMoVTgnrxtC0rXraRYbjAJaCm01Tr3xTiWBnYDKonz5qRz05Z5xpS0Qo1+E4EtctnDQFLC/iywaX5cXI0eVJrHl+rEsNBjkrRBo8FIOkxSq6TWmTNntnMqZmbWFifS1hGGk1Zsyf+tJJxjgCE50Syu8i4oNblfrThvA7bPiewBwA0RMTuXMvQDHshvEj6StEWV4x4FPA58Gxgrqaekz0m6vpPmMxs4E/h+O/crGyrpCdJq9C8j4v1CW7FUYJcGjzdPSQPpDUBFrXMPsEJOWF8DegF3Vjt4rimeIunGWmNGxHvV9o2ID4AngW2A7YA/kxLXgfk2vtD9/tI8bikfr45Ojym/IWlIRFwaES0R0dKzZ892TsXMzNriRNoWiKQ1SKUal0l6ATgBOECSIuJlYAawE7AfKbGGtHo7oHScVYD1SEldPVsDT7czzqVzDCfnOC8ABktaOSc6twP7Mm/CfwCwOjAj79OX6qvSewD3RcRdwE9IifmhzE0cG5pPXpX/vyq12ANICVfRVcCOwLo0b0xEfJaUtJ0haa06/Z+kdN0a0da5z13eywlrH9KbiiMK421TOU5E7EsqDVmjvTFk40nnbOWIeBN4iLlJa0fVR3eHmMzMrEFOpG1BDQGuiog+EdE3ItYlJc+Dcvto4Bzg+Yh4JW/7E7CipENgTqJ1NjCqUhtci6SdSPXEv2pnnLsBT0TEujnOPsANpOS5EuexpBXRSg3wcGBw7t+XlERWq5N+DDhY0lIRcS0wDTiQlFC3qcp8zgTOr5QDSNqdVH9+dXG/iPiIdF6PYQFFRCspMf/vOl0vBA4t1r3nX5XoVWe/eue+Ese7wNHAcZKWIc15e0nF0oo2a+jreBD4FunTA0ilLNuR3sBNWYDjLohFMSYzM2uQE2lbUMNJv3xRdANzV26vI9W6zinriIggJVH7S5oGTAXeB35QY4xKzenU3Ge/iKi3In2JpFfybUIDcd4J9Cat0kaude5DWiGsxD0DeKv0BUpIvzYiYIqkicDfgEuAq3NZS3vmcwHwCDBZ0rPAD4G9a5QH/BpYps55aNTPgK8WVomLNdKTJPXNXyocBpyl9FNtT5NW4/9Z59j1zv0cEfEYKZkcnue8J3C4pOfzdTwJOLWwS7keua2fRnyQ9IsfE/JY/wL+DrRGxMd15lDLE4Xn2S86MaZyjXTVn3c0M7OFSymnMTOz7q6lpSVaW1vrd7Ru7enT7q7fCdh05K6dHInZ4kHSxIhoqdbmFWkzMzMzsyZ01MfCZgudpItIf0yk6LzK71MbSPoq89c+j4+II6r1X9xJ2pJU7130QUSUy3EWmkUxJjMz6xhOpG2x1V2TwY6U31QsMW8sImIy0L+r4yhaFGMyM7OO4dIOMzMzM7MmeEXazMxsCeIvEZp1HK9Im5mZmZk1wYm0mZmZmVkTnEibmZmZmTXBibSZmZmZWROcSJuZmZmZNcG/2mFmZrYEOeWUU7o6BGuAr9PiwSvSZmZmZmZNcCJtZmZmZtYEJ9JmZmZmZk1wIm1mZmZm1gQn0mZmZmZmTXAibWZmZmbWBCfSZmZmZmZNcCLdwSTNljSpcPuepB9JOr3Ur7+kp/P9FyRNLuxzft4+StKrkpbLj3vkvlsW+r4haUa+f5eknSXdWhprlKQhhcc9JH0k6fBSvxck9ShtGyHpwnz/U7nPWoX2iyR9v8a52FnSWzm2ZySdVTruzNK52iy3bSTpD5KmSXpU0rWSenXA3CZLekLSvZL6FNp6Sbpa0vOSJkqaIGnfKnOo3HavMtflJd0saYqkxyStX+2clGKZLOkpSadKWr7QvrmkuyU9m8/BDyWpcN4+lvTZQv8pkvpK+nOO76XSue1bJ45q52S+53He/glJZxSuzQRJXygcr0fhGNWu182SHiptOyU/zyfl8zG81H5sfv5MlvS4pF9I+kRpDvO8dqrMdStJkwqPh0t6r3CcLSU9ke+Pk9RS6NtX0pTynFR4bdQ4rx0d07OFY14vaWThcfF6HV1tPDMz63j+gywd772I6F/cIGkj4HagmHAOA0YXHu8SEbOqHG828DXgfysbImIy0D8fexRwa0Rcnx/v3ECM+wMPAcOBixvoXxn375LOAM4CDpa0DTAIGNDGbvdHxJ6SVgAek3RTRIzPbWMi4shi55xQ3gYcGxFjC3Pq2WCYbc1tl4iYJenHwEnAN3OCejPwm4g4MI/XB/hSeQ4NjPtWRGwhaXUg6vSvxLIScClwCXBoPk+3AN+OiD9KWhG4Afgv4KK87yvASGBo8YARsW2OfwTQUj63deKYc07y9vmex9lPgE8DW0TEB5J6ATs1MA6SViM9V96RtH5EPF9oPicizpLUD5go6fqIqLwh+g9gu4j4h6RlgWOBFYCPinOoM/xkYD1JK0fEP4GBwNPA1sDD+fGDjcyjQZ0R00ER0Vo6xmkAkt6pcb3MzKwTeUV6IYiIqcCbkrYtbD6AeRPpWs4FjpHUkW96hgPHAWtLWqed+14KbCBpF1Jid2REfFRnHyLiPWASsHadrgcCEypJdN53XERMaTC+RuY2oRDHrsCHETEn6Y6IFyPiggbHq/gwj6mIeDMi/tHIThHxDnA4sI+kNUjzHx8Rf8zt7wJHAt8r7HYrsLmkjdsZY1uK56SqnNR/EzgqIj7I8f0tIq5tcIwvA2OBa0hvJOcTEdOAd4HV86aRpDcV/8jtH0bEGRHxdoNjVo77MdAKVF6DA0jP34H58UBgfJVdO82iGJOZmbWPE+mOt0LpI/HKquFocvIgaTvgjZw0VNxT2OeYwvaXgAeAr3REcJLWBT4dEQ8D11Ja1awn/+P/bdIq6bMRcV+D464O9AOK/YeWztUKwBbAxDYONai4D4WV43bMbTBpFRpgc+DROuEPKsW5QZU+zwPbAKdXaWtTTgpnkM7P5pTmHxHTgZUkrZI3fQz8HPhBe8dqQ/GcQPXn8YbAS3WS2HsK1+ayUttw0utgdL4/n/wpx7T86ccqwEoRMaNO7LVeO2XjgYGSPkk6h+OYN2ktrv7+rjCPP9QZf6HHJOnMRgORdJikVkmtM2fObOc0zMysLS7t6Hi1PhIfAzwo6TjmL+uAtj8KPh34PankoZ5aJQWV7UNJSSaklcHLgbMbOO7cA0VMyjWjv2yg+yBJj5OSxHMj4rVCW7XSjnrHm6fMIpe2VNSb2z151fcd4IfVDi7pImAH0ir156qNWWWfFYArgI2BqyR9JyLOlXQbcGKDq+l1J15yNTBS0mfauV9ZrXNSrUTps9Q353mcS3KOz/d7kZ4DD0REKNWxb1E4N8dI+iqwEbBXtQNL2gP4GbAacGBEVJLMRsooICWlxwH3A49ExHRJG0rqSUrYpxf6zimjUKoxv7V8sDo6Nab2iIhLSZ8k0dLSUq/kyMzM2sEr0gtJRLxMWnXcCdiPlFg3uu+0/9/evUfdNd95HH9/kpAwajSoEiWlbnFJVKodSVXKTE0Zl9Z1hYrLWrSpXtQYyqxJx+oaRlfRalhtkbAMLSal1CWICovEJSQkLlnCohPXBk0bl/CdP37f49l5ep7nnJznqfN4ns9rrayc/dv77PM9v72z8j2//d2/TSmLOKSJzV+l47J4zXCg9p/64cAkSc9QanF3yrrU1fVe/mlkdkSMpoy0HiupUR3nY3Rfc92dRt9tArA5pS9/UPm8T9c2iIjJwJ40X5MNsCPwSkS8TDm2h+YNX8Nz/92S9BFgJPAksJBO31/lxsXl1ZHgiFhJ+ZHwb6sRZz31+qQriyk1ves22K6eQyjn5ZI8PiNZdVT63IjYntJ/F0salt93ee3HQkTcksn9o8CaLcRwH/AZYByllAVKvflhleUPWl+MyczMmuRE+oN1JXAu8HREPL+a7/0hObrXwFPAJpK2g/dvnBsNPJw3Pa4TESMiYmREjKSMdte9zN6b8vL8WTRO/P6Hcql7n1qDpN0l7dDdm5r9bpmAfgf4Wo7E3gEMk/T1ymZrN/m1ap4CtpW0fUT8GTiWckPmdRHR7Qhg3mw4FfhNRCwDrgDGK2cGydHun1BKOTqbBuzF6iX9f6VOn3S13V+Ai4Hz86Y/JG0o6eAmPuZwYO/KsdmFOnXSEXE9pW74qGz6L+DCvFERlUsWwzq/rxl5Q99zwNF0JKn3Ur57W2qR+2JMZmbWPCfSva9zbelZlXVXU0Zm691kWK2pvKzzyoh4jMa1vORNYEcAl2Z95zXAcRHxOiWZmdHpLdeyarI5X9Lz+efH2Tap0vZ8Czco1lwE7K6O6dg610jvljcl7gucqDLF2kLKjBWNijub+W4ARMRSyjGYnInuAcAXVKYRnAtMZ9WEv3ON9EGd9reMkvhdLmkeJTGeCBwnaTfqm5XlMXMpdfDH575WAPsDZ0h6gjKzw/3AX02zFhFvU5Lsj3XVKc2q9kk2dXUen0E5Fgsz/huAbm/8y+O9OWX0tfZ5S4DXteoNuDX/CZwkaRBltprbgTkqU8HdA8zLPzXd/tvp5B5gaF4hgpK0bkHrM3Z09W/jbxFTtUb6thbjNTOzXqQGA2ZmZtZPjB07Nh54YLXLrK2fmTJlSrtDsCb4OPUdkh6MiLH11nlE2szMzMysBZ61w3qsMptC1ZKIOLAd8diqJM0BhnZqPjLKg336nZx5ZVyn5vMj4tJ2xAN9MyYzM+s5J9LWYxFxC3BLu+Ow+mpPPBwocuaVPqUvxmRmZj3n0g4zMzMzsxY4kTYzMzMza4FLO8zMzAYQzwZh1ns8Im1mZmZm1gLPI21mNkBIehl4tt1xfAA2AF5pdxB9mPune+6fxgZaH20eEXWfIuxE2szM+hVJWV/eYgAACyZJREFUD3T18ARz/zTi/mnMfdTBpR1mZmZmZi1wIm1mZmZm1gIn0mZm1t/8vN0B9HHun+65fxpzHyXXSJuZmZmZtcAj0mZmZmZmLXAibWZmZmbWAifSZmb2oSfpHEmPS5ovaYak9SrrTpO0WNITkr7UzjjbTdLe2Q+LJZ3a7njaTdInJM2StFDSY5K+ne3DJc2U9FT+/dF2x9pOkgZLmifphlz+pKQ5eR79StKa7Y6xXZxIm5lZfzAT2CEidgKeBE4DkDQKOAzYHtgbmCppcNuibKP83j8D/hkYBRye/TOQrQS+FxGjgM8Bk7NPTgVuj4itgNtzeSD7NrCosnw2cG5EfApYBhzblqj6ACfSZmb2oRcRt0bEyly8D9g0X+8PXBURb0XEEmAxsGs7YuwDdgUWR8TTEfE2cBWlfwasiFgaEQ/l6z9RksURlH6ZnptNBw5oT4TtJ2lTYB/gl7ks4IvANbnJgO4fJ9JmZtbfHAPclK9HAM9V1j2fbQOR+6IbkkYCOwNzgI0iYmmuegHYqE1h9QXnAacA7+Xy+sBrlR+uA/o8GtLuAMzMzJoh6Tbg43VWnR4R1+U2p1Mu11/xQcZmH26S1gGuBb4TEW+UQdciIkLSgJwrWNK+wEsR8aCkPdodT1/kRNrMzD4UImKv7tZLmgTsC+wZHQ9J+APwicpmm2bbQOS+qEPSGpQk+oqI+N9sflHSxhGxVNLGwEvti7CtxgH7SfoyMAxYFzgfWE/SkByVHtDnkUs7zMzsQ0/S3pTLz/tFxF8qq64HDpM0VNInga2Aue2IsQ+4H9gqZ1xYk3IT5vVtjqmtst73YmBRRPy4sup64Kh8fRRw3QcdW18QEadFxKYRMZJyvtwREROBWcBBudmA7R/wkw3NzKwfkLQYGAq8mk33RcQJue50St30Ssql+5vq76X/y5HF84DBwCUR8cM2h9RWksYDs4EFdNQAf59SJ/1rYDPgWeCQiPhjW4LsI7K04+SI2FfSFpSbVYcD84AjIuKtdsbXLk6kzczMzMxa4NIOMzMzM7MWOJE2MzMzM2uBE2kzMzMzsxY4kTYzMzMza4ETaTMzMzOzFjiRNjOzfkfS8h689xlJCySNzeU7JT0h6RFJ90japrLtNTkVWOd9TJJ0Qasx9AZJIyXd2YbPvUrSVpXlWZKW1/qzyX2MlPRoD2J4V9LDkjbJ5doxnS/pVkkfz3ZJukPSunX2MUXSya3G0Bsk7SFpWqe29fO7PSzpBUl/qCyvWfnuj0r6raT1Kvu6odO+pkk6KF/XzvPavq7J9m9KOqbynnPyc9vaN32FE2kzM7O/NiEiHqgsT4yI0cB04BwASdsDgyPi6XYE2IddSHk4DgARMQF4oOvN/yZWRMSYiPi/StuEiNgpY/l+tn0ZeCQi3viA42tZRLya320McBFwbm05It6m47vvAPwRmLwau59Y2VftgSuXACdWPv9f83MNJ9JmZtaP5YjjOTk6t0DSodk+SNJUSY9Lminpd7WRuQbuAj6VrydSeaKbpKMlPSlpLuXRyrX2DSVdK+n+/DMu26dImi5ptqRnJX1F0n9nnDfno6uRtKekedl+iaSh2X6WpIU5yvqj1eiTwTkSWeuT72b7nZLOr4xm7prtf5efOzfj2L+ynx/ltvMl1ZKt2cBekoY0G1ODeIdJujRjnSdpQravLenX2QczJM1pctS7u2N4eh7Du4HqlYct85g8mMdr22yfJulCSfdJejpHfS+RtKg6kizp8Iz/UUlnZ1vd49DL7gVG9GQH+aTQZ2rng62qV05yMzOzPuorwBhgNLABcL+kuyiJ7khgFPAxYBFl5K2Rf6E8BY/cx5UAkjYGfgDsArxOeYTyvNzufMqo4d2SNgNuAbbLdVsCEzKOe4GvRsQpkmYA+0i6GZgG7BkRT0q6DPi6pMuBA4FtIyJql++bNAYYkSOWdHrv2hExRtLu2R87AKdTHg19TG47V9JtwNcofTgmIlZKGg4QEe+pPGlyNPDgasTVlcllt7FjJrC3Stoa+AawLCJGSdoBeLjJ/e3LqsfweABJu1Aegz2Gkh89VIn/58AJEfGUpM8CU4Ev5rqPAv8A7Ed5tPg44DjKuTYGeAk4m3JuLMv4DwCeo+vj0GOSBgN7Uh6B3qwrJK3I1zNz9BnKKP7ngbm9GGK/4ETazMz6s/HAlRHxLvCipN8Dn8n2qyPiPeAFSbMa7KeWYDxDx2XujYGX8/VngTsj4mUASb8Cts51ewGjJNX2ta6kdfL1TRHxjqQFlMd235ztCyhJ6jbAkoh4MtunUxLLC4A3gYtV6l5XqX1t4GlgC0k/BW4Ebq2suxIgIu6StG4md/8E7KeOmthhlEdn7wVcFBEr8z3VR2i/BGxC7yTS44Gf5mc8LulZSt+Op/xIISIelTS/wX5mSXoXmA+ckW3DI+JP+frzwIwcgUXS9fn3OsBuwNWVYzi0st/f5o+ZBcCLEbEg3/cY5RhuzqrnxhXA7sCZdH0cemItSQ9TRqIXATOzvatHWVfbJ3Yqaap5Cdi2l+LrV5xIm5mZNVYvwVhBSSobGQR8LiLerDZmUvYWvD+K+05E1JKa9+jm/+gcAd6VMuJ4EPBNOkZIuxURyySNBr4EnAAcAtRuJuucbAUgykj5E3Xi78owSv90SdKBwH/k4nFdJHC9aUJEvNKpbaWkQfmDqiuDgNeyJrmet/Lv9yqva8tDgHfqvanBceiJFXlVYW3K1Y/JwE+AVymj51XDgc59Uk/D4zlQuUbazMz6s9nAoVmPuiFlJHAucA/wVZVa6Y2APVrY9yI6am3nAF9QmVFhDeDgyna3UrlZKy/3N+sJYKSk2uccCfw+R0n/PiJ+B3yXUkbRFEkbAIMi4lrKyOynK6trNeTjgdcj4nVKMnaiMnOWtHNuOxM4vlYLXSvtSFsD3c66EREzKje2dZdEz6bUMpMlHZtR+uUeSvKJpFHAjo2+ex1PALVZV+4CDpC0lqSPUMp4yBsRl0g6OD9LmQA3ay7l3Nggyy0OpxzD7o5Dj+XI+reA7+UxegrYRNJ2+T02p5w3zZTENDyeA5VHpM3MrD+bQalffYQyunpKRLwg6VrKaO5CSq3qQ5Ta5tVxIyUBvy0ilkqaQqlzfo1Vk5NvAT/L0oMhlITthGY+ICLelHQ0paxgCHA/ZcaE4cB1koZRRoxPWo24RwCXSqoNpp1WWfempHnAGnSMjp4JnAfMz/csodQZ/5KSYM2X9A7wC+CC/GGyIiJeWI2YujMVuDBLJ1YCkyLiLUlTgemSFgKPA4/R+jFcHBEPZUnOI5RShvsr203MGM6g9M1VuV1DeW6cSqmbF3BjRFyXyXhXx6FXRMS8PO8Oj4jLJR2RnzmMMlJ+XP5YqqnWSL8SEXvl63HAlN6Orz9Qx1UkMzOzgUPSOhGxXNL6lFHDcZlkPwOMrVMG0Pn9a1GSo3FZg92nSBoJTIuIPZrc/k7g5J6WWOTsE29ExMWVtl7Zd6fPGQyskT82tgRuA7aJiLclLY+IdRrsonaT6GUR8Y+9FVdvkrQH5YfDpDbGsDNwUkQcWWmbAiyPiKZni+mvXNphZmYD1Q15U9Zs4MzKCOrLwO1qMJVaRKyg1Pj2aHqxfug1yk2RQHkgC6V8om6tcA+sDdwt6RHKlYdv5DzKAG+o8kCWrkTEUuAXqvNAFnvfBsC/1xYknQMcAfy5bRH1IR6RNjMz64dyxo0DImJau2Ox1uRVhTER8Zs2h2JdcCJtZmZmZtYCl3aYmZmZmbXAibSZmZmZWQucSJuZmZmZtcCJtJmZmZlZC5xIm5mZmZm14P8BNZnTEjZ8NyUAAAAASUVORK5CYII=\n", | |
| "text/plain": [ | |
| "<Figure size 432x288 with 1 Axes>" | |
| ] | |
| }, | |
| "metadata": { | |
| "needs_background": "light" | |
| }, | |
| "output_type": "display_data" | |
| } | |
| ], | |
| "source": [ | |
| "def plot_scores(scores):\n", | |
| " sns.barplot(y=SPEC_NAMES, x =scores, orient='h')\n", | |
| " plt.title('Relative likelihoods for each specification')\n", | |
| " plt.xlabel('log[P(demos | spec)] - log[P(demos | TRUE)]')\n", | |
| " plt.show()\n", | |
| "\n", | |
| "plot_scores(scores1)" | |
| ] | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "Hopefully, you can see that the most likely demonstration is the intended one, namely,\n", | |
| "\n", | |
| "\n", | |
| "1. Avoid the red tiles (lava).\n", | |
| "2. Reach the yellow tiles (recharge).\n", | |
| "3. If the agent touches a blue tile (water), then it must dry off (brown tile) before recharging.\n", | |
| "\n", | |
| "This is despite there being an unlabeled negative demonstration (TRC5) which fails to recharge." | |
| ] | |
| }, | |
| { | |
| "cell_type": "markdown", | |
| "metadata": {}, | |
| "source": [ | |
| "## Another set of demonstrations\n", | |
| "\n", | |
| "Now consider the situation where TRC5 is given twice in a row, where we recall that TRC5 fails to dry off before recharding." | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 36, | |
| "metadata": {}, | |
| "outputs": [ | |
| { | |
| "data": { | |
| "text/html": [ | |
| "trc 0: ↑<text style='border: solid 1px;background-color:white'> </text>→<text style='border: solid 1px;background-color:#9595ff'> </text>↑<text style='border: solid 1px;background-color:#9595ff'> </text>↑<text style='border: solid 1px;background-color:white'> </text>←<text style='border: solid 1px;background-color:white'> </text>←<text style='border: solid 1px;background-color:white'> </text>←<text style='border: solid 1px;background-color:white'> </text>↑<text style='border: solid 1px;background-color:#ffff8c'> </text>↑<text style='border: solid 1px;background-color:#ffff8c'> </text>\n" | |
| ], | |
| "text/plain": [ | |
| "<IPython.core.display.HTML object>" | |
| ] | |
| }, | |
| "metadata": {}, | |
| "output_type": "display_data" | |
| } | |
| ], | |
| "source": [ | |
| "print_trc(TRC5)" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 40, | |
| "metadata": {}, | |
| "outputs": [ | |
| { | |
| "name": "stdout", | |
| "output_type": "stream", | |
| "text": [ | |
| "encoding traces\n", | |
| "done encoding traces\n", | |
| "concretizing spec\n", | |
| "concretizing spec\n", | |
| "concretizing spec\n", | |
| "concretizing spec\n", | |
| "done spec\n", | |
| "fitting policy\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 1\n", | |
| "Controller Size: 0\n", | |
| "log_prob: -87.33654475055322\n", | |
| "build spec: 1.3s\n", | |
| "fit: 0.0033s\n", | |
| "surprise: 0.0052s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 1.2919392585754395, 'fit': 0.003260374069213867, 'surprise': 0.0052225589752197266}\n", | |
| "concretizing spec\n", | |
| "done spec\n", | |
| "fitting policy\n", | |
| "done spec\n", | |
| "fitting policy\n", | |
| "done spec\n", | |
| "fitting policy\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 1628\n", | |
| "Controller Size: 328\n", | |
| "log_prob: -82.49648318493705\n", | |
| "build spec: 1.5s\n", | |
| "fit: 0.74s\n", | |
| "surprise: 0.0048s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 1.4929251670837402, 'fit': 0.7406604290008545, 'surprise': 0.0047533512115478516}\n", | |
| "concretizing spec\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 850\n", | |
| "Controller Size: 195\n", | |
| "log_prob: -89.77841117137949\n", | |
| "build spec: 2.0s\n", | |
| "fit: 0.39s\n", | |
| "surprise: 0.0042s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 1.9750003814697266, 'fit': 0.3940000534057617, 'surprise': 0.0042362213134765625}\n", | |
| "concretizing spec\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 1797\n", | |
| "Controller Size: 348\n", | |
| "log_prob: -92.81852146235173\n", | |
| "build spec: 1.7s\n", | |
| "fit: 0.81s\n", | |
| "surprise: 0.0041s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 1.7426140308380127, 'fit': 0.8115346431732178, 'surprise': 0.004128456115722656}\n", | |
| "concretizing spec\n", | |
| "done spec\n", | |
| "fitting policy\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 577\n", | |
| "Controller Size: 132\n", | |
| "log_prob: -87.32193989773135\n", | |
| "build spec: 2.0s\n", | |
| "fit: 0.27s\n", | |
| "surprise: 0.0063s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 1.999612808227539, 'fit': 0.2711455821990967, 'surprise': 0.006339073181152344}\n", | |
| "done spec\n", | |
| "fitting policy\n", | |
| "done spec\n", | |
| "fitting policy\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 523\n", | |
| "Controller Size: 118\n", | |
| "log_prob: -77.1876963244796\n", | |
| "build spec: 1.7s\n", | |
| "fit: 0.5s\n", | |
| "surprise: 0.0067s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 1.6537911891937256, 'fit': 0.49933838844299316, 'surprise': 0.006686687469482422}\n", | |
| "done spec\n", | |
| "fitting policy\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 1842\n", | |
| "Controller Size: 372\n", | |
| "log_prob: -85.52927920428995\n", | |
| "build spec: 2.0s\n", | |
| "fit: 0.83s\n", | |
| "surprise: 0.0097s\n", | |
| "done fitting\n", | |
| "compute log likelihood of demos\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "BDD size: 1913\n", | |
| "\n", | |
| "----------------------------\n", | |
| "Controller Size: 374\n", | |
| "\n", | |
| "{'build spec': 2.0062806606292725, 'fit': 0.8324692249298096, 'surprise': 0.00965571403503418}\n", | |
| "log_prob: -89.02936303916954\n", | |
| "build spec: 1.9s\n", | |
| "fit: 1.1s\n", | |
| "surprise: 0.0048s\n", | |
| "\n", | |
| "----------------------------\n", | |
| "\n", | |
| "{'build spec': 1.9228413105010986, 'fit': 1.133453369140625, 'surprise': 0.004793882369995117}\n" | |
| ] | |
| } | |
| ], | |
| "source": [ | |
| "scores2 = evaluate_demos([TRC5, TRC5])" | |
| ] | |
| }, | |
| { | |
| "cell_type": "code", | |
| "execution_count": 39, | |
| "metadata": {}, | |
| "outputs": [ | |
| { | |
| "data": { | |
| "image/png": "iVBORw0KGgoAAAANSUhEUgAAAtIAAAEXCAYAAACAp6MwAAAABHNCSVQICAgIfAhkiAAAAAlwSFlzAAALEgAACxIB0t1+/AAAADh0RVh0U29mdHdhcmUAbWF0cGxvdGxpYiB2ZXJzaW9uMy4yLjEsIGh0dHA6Ly9tYXRwbG90bGliLm9yZy+j8jraAAAgAElEQVR4nOzdebxd873/8dcbRdQsaTSGpEjMFXJ6aYj5XnpLUSEJSjqpXsOtqdpGVW8pLWruRZWUVsRcoT9KiSGinBASUyJibLUxlLrGxuf3x/e7k5WVfc7eZ+XESY738/HYD3uv73et7+e71t7y2d/92fsoIjAzMzMzs45ZoqsDMDMzMzNbHDmRNjMzMzOrwIm0mZmZmVkFTqTNzMzMzCpwIm1mZmZmVoETaTMzMzOzCpxIm5lZtyNpvKRvVNx3bUlvSVqyk2MaKenewuO3JK2T74+WdFKFY87ZT9IQSU8V2p6VtHNnxN4ghhMl/bbCfutLmizpn5KOWBixLShJ/SSFpKW6OpZ6JP0/SQcVHp8k6RVJLy+s53EeZ85z9+NukXximJmZSXoW6A3MBt4CbgEOi4i3FsI434iI2wEi4nlg+c4co56I6NQxIuIeYP3OPOZC9l3gzogY2NWBLK4i4gu1+5LWBo4G+kbE3/PmBX6OSRoP/DYiLi6Mu9BfH4sLr0ibmdmibPf8j/ZAYHPg+10cj3WevsBjVXZcVFeIu9jawKuFJNo+Ak6kzcxskRcRLwO3khJqACRtJek+Sf+Q9Iik7evtK2ldSXdIejV/7P07SSvntstJCci4/HH1d4sf50saJqm1dLwjJd2Y7y8j6XRJz0v6m6QLJPVoZk55jPXqbF9B0p2SzlGygaTbJL0m6SlJ+7ZxvO0lvVjaPFDSo5LekDRW0rKF/t+U9HQ+7o2S+hTaBkt6MO/3oKTBhbbPSLorl2TcBvQstC0r6bf5XP8j79u7Tqx3ADsA5+XzPkDSSpIukzRL0nOSjpe0RO4/UtIESWdKehU4sc4xl5D0PUkz8vhXSVq10H51Lnl4Q9LdkjYutPWQdEYe9w1J95au4/75Gr8iaVS985+P85+SHs/n5iVJxxSvjaQf5GM8K2n/wn7tPo8k7aFUBvNmnt+ueft4Sd9QKuG5DeiTz+dolcpSJK0q6VJJf5H0uqQb8vZVJN2Uz/vr+f6aue1kYEjhOp2Xt8957jZx3e7Nc3td0kxJc1bRuwMn0mZmtsjL/7B/AXg6P14DuBk4CVgVOAa4VlKversDpwB9gA2BtciJWER8BXievPIdET8v7TsOWF9S/8K2/YAr8v1TgQGkBH89YA3ghAWY52rAn4AJEXEEsBwpQboC+BQwHPilpI2aPOS+wK7AZ4DPAiPzODuSzsm+wKeB54Arc9uqpHN7DrAa8Avg5hwbOZZJpAT6J8CcGt18fyXSOV4NOAR4pxxUROwI3EMq1Vk+IqYB5+Z91wG2Aw4EvlrYbUvgGVK5z8l15no4sGfetw/wOnB+of3/Af1J5/Eh4HeFttOBQcBg0vPpu8CHhfZtSGUzOwEnSNqwzvgAvwa+FRErAJsAdxTaViedszVI5+kiSbVSnDafR5L+DbgMOBZYGdgWeLY4aC5L+gLwl3w+R9aJ7XLS82njfA7OzNuXAC4lfUKwNul6nZePO4p5r9NhdY7bzHV7Ks/958CvJanOcRZPEeGbb7755ptvi9yNlCy8BfwTCFKCuXJuOw64vNT/VuCgfH88qe653nH3BB4ujbNz4XG/PN5S+fFvgRPy/f45nuVICfr/AesW9v08MLONcUcC9xYeB7Bevj8auASYChxb6DMMuKd0nAuBHxX2Oynf3x54sTSvAwqPfw5ckO//Gvh5oW154IM8968AD5TGnJjjXxv4F/DJQtsVpBpagK8B9wGfbeL6zrlGwJLA+8BGhfZvAeML5+75Bsd7Atip8PjTeU5L1em7cj7/K5ESyXeAzer0qz0X1ixsewAY3kYMz+e4Vyxt377OebsK+GGj51G+3mc2cQ7L178W+1L5XHwIrNLEdRkIvF5vjPJzt8nr9nShbbm87+qN4lhcbl6RNjOzRdmekVb3tgc2YG4ZQV9gn1w+8A9J/yCtGn66fABJvSVdmT9qf5OUGPcs92vHFcCIfH8/4IaIeBvoRUoMJhViuCVvr+KLQA/ggsK2vsCWpXnuT1rdbMbLhftvM/fLZ31Iq9AARPoC56ukldB52rLnCm2vR8T/ldpqLie9obkylxD8XNInmoizJ/CJ0rFqY9a80OAYfYHrC+fpCdIXVXtLWlLSqbks4k3mruj2zLdlgRntHLut81i2N/CfwHNK5S+fL7TVO299aPw8WqtBbM1YC3gtIl4vN0haTtKFuSzjTeBuYGU192sfzVy3Oecuv27gI/gy70fFibSZmS3yIuIu0urr6XnTC6QV6ZULt09GxKl1dv8paRVs04hYETiAtAo45/ANhr8N6CVpICmhrpV1vEJaydy4EMNKUf0XDX5FSqD+IOmTedsLwF2leS4fEd+uOEbNX0iJJwB5vNWAl8pt2dq57a/AKoX4am0ARMQHEfHjiNiIVCaxG+mj/kZeIa0eF8etjTnn8A2O8QLwhdK5WjYiXiK9AdoD2Jm0Ct0v76M89rvAuk3E2a6IeDAi9iCVTtxAWnWuqXfe/kLj59ELnRDbC8Cqyt8NKDmaVLayZX59bJu3114j7Z33Zq5bt+ZE2szMFhdnAf8uaTPSqvLuknbJq43L5i90rVlnvxVIJSJv5NrqY0vtfyPVd9YVER8AVwOnkepnb8vbPyQlv2dK+hSk2m1JuyzAHA8j1ZOOy182uwkYIOkrkj6Rb59rp0a3WWOAr0oaKGkZ0puNP0fEs8Af8pj7KX/hEtgIuCkingNagR9LWlrSNsDutYNK2kHSpnk1801SkvUhDUTEbFLSebLSly37AkeRrnOzLsj7982x9JK0R25bAXiPtOq+XJ5vbewPSWU1v5DUJz+fPp/PS9Py+dhf0kr5OfMm88+9dt6GkN5kXN3E8+jXpGu1k9IXKteQtEFHYouIv5JqxH+p9OXCT0iqJcwrkBL5f+T6+B+Vdm/z9dFJ122x5kTazMwWCxExi/SlqxMi4gXSCuMPgFmkFbdjqf/v2o+BLYA3SF+iu67UfgpwfP5Y/Zg2hr+CtJp5dUT8q7D9ONIXIO/PH4vfzgL8lnOkQtKDgReB35MS0f8gfcnwL6SPyX8GdCjJqzPO7aT63GtJq8zr5jGIiFdJSd7RpMTzu8BuEfFK3n0/0hfIXiMlXZcVDr06cA0piXwCuItU7tGMw0m1ws8A95LO+SUdmNbZwI3AHyX9E7g/x0mO8TnSSunjua3oGGAK8GCe18+oliN9BXg2PxcOIZXh1LxM+gLkX0hfdDwkIp7MbW0+jyLiAdKX984kPYfvYv5PDJqN7QPgSeDvwHfy9rNIJUWvkM7LLaX9zgaG5l/dOKfOcRf0ui3WlIu/zczMzGwhUPppxt9GRL1PTGwx5hVpMzMzM7MKnEibmZmZmVXg0g4zMzMzswq8Im1mZmZmVoETaTMzMzOzCpbq6gDMzOyj0bNnz+jXr19Xh2FmtliZNGnSKxFR9y+WOpE2M/uY6NevH62trV0dhpnZYkXSc221ubTDzMzMzKwCJ9JmZmZmZhU4kTYzMzMzq8CJtJmZmZlZBU6kzczMzMwqcCJtZmZmZlaBE2kzMzMzswqcSJuZmZmZVeBE2szMzMysAifSZtatSFpd0pWSZkiaJOkPkgZI2ljSHZKekjRd0g8lKe8zUtKHkj5bOM5USf3y/a9JmiLp0bx9D0nnS5os6XFJ7+T7kyUNrRNTm30ljZY0Mz9+RNJOhf2eldSz8Hh7STcVYp5VONZkSRstvDNrZmZl/hPhZtZt5MT4euA3ETE8b9sM6A2MBr4dEX+UtBxwLfBfwPl59xeBUcCw0jHXzNu3iIg3JC0P9IqI3+f2fsBNETGwrbgi4tC2+kraDTg2Iq6RtANwEdC/ySmPjYjDmuxrZmadzCvSZtad7AB8EBEX1DZExCPAAGBCRPwxb3sbOAz4XmHfm4CNJa1fOuangH8Cb+V934qImQsp/onAGp15QEkHS2qV1Dpr1qzOPLSZ2ceeE2kz6042ASbV2b5xeXtEzACWl7Ri3vQh8HPgB6V9HwH+BsyUdKmk3Ts35HnsCtzQgf7DSqUdPcodIuKiiGiJiJZevXp1XqRmZuZE2sys4ApgK0mfqW2IiNmkBHcoMA04U9KJnTzuaZKm5fF/VtgedfoWt42NiIGF2zudHJeZmbXDibSZdSePAYPqbH+8vF3SOsBbEfFmbVtE/As4Aziu2DeSByLiFGA4sHcnx31sRAzI415S2P4qsErh8arAK508tpmZVeRE2sy6kzuAZSQdXNuQf4njKWAbSTvnbT2Ac0ilHGWjgZ2BXrlvH0lbFNoHAs8tlOjhPGAJSbvkx+OBr+Q4lgQOAO5cSGObmVkHOZE2s24jIgLYC9g5//zdY8ApwMvAHsDxkp4CpgAPkhLX8jHeJyXZn8qbPgGcLulJSZNJv+rx3wsx/pOA7+ZNPwHWk/QI8DDwNPDbwi7lGunBCyMuMzOrT+n/22Zm1t21tLREa2trV4dhZrZYkTQpIlrqtXlF2szMzMysAv9BFjOzTiTpfGDr0uazI+LSrojHzMwWHifSZmadqPZXDM3MrPtzaYeZmZmZWQVOpM3MzMzMKnAibWZmZmZWgRNpMzMzM7MKnEibmZmZmVXgRNrMzMzMrAIn0mZmZmZmFfh3pM3MrCnP/8+mXR2CdZG1T5jS1SGYLZK8Im1mZmZmVoETaTMzMzOzCpxIm5mZmZlV4ETazMzMzKwCJ9JmZmZmZhU4kTYzMzMzq8CJtJmZmZlZBU6kzazbk7SnpJC0gaQfSTql1D5Q0hP5/pqSfi9puqQZks6WtHRu217STfn+SEmzJD2c+94qaXCDOEZLGtpG28Ac46758UGSxpT69MxjLpMf3yDp/qrnxczMFowTaTP7OBgB3Jv/OwYYVmofDoyRJOA64IaI6A8MAJYHTm7juGMjYvPc91TgOkkbdkKMANcD/y5puUKfocC4iHhP0srAIGAlSetUHNPMzBaAE2kz69YkLQ9sA3wdGB4R04DXJW1Z6LYvKcHeEXg3Ii4FiIjZwJHA10oJ7Xwi4k7gIuDgCjEK2AcYSUqel42IN4G7gN0LXYfnOAG+DIwDrszbzczsI+ZE2sy6uz2AW3IC/aqkQaRkdDiApK2A1yJiOrAxMKm4c05onwfWa2Ksh4ANKsQ4GJgZETOA8cAX8/ZinH1IK+R35Lba6voY5q5iz0fSwZJaJbXOmjWrQmhmZtYWJ9Jm1t2NIK3akv87AhgLDJW0BPOu8i4oVdyvXowANwNbS1qRtGp+bUTMltQb6A/cm98gfCBpk3oHjoiLIqIlIlp69epVMTwzM6tnqa4OwMxsYZG0KqlcY1NJASwJBHAsMBPYDtgb+Hze5XFSHXLxGCsCawNPA//WYMjNgSc6GOOSOYY9JI0iJeOrSVohIv4p6RZgL1LCf1TebV9gFWBmqgphRVLyPaojY5uZ2YLxirSZdWdDgcsjom9E9IuItUgJ9BDSKvSZwDMR8WLu/ydgOUkHwpwk9wxgdES83d5AkrYj1Uf/qoMx7gQ8GhFr5Rj7AteSkmdynEcBvYGJedsIYNfcvx/pS4eukzYz+4g5kTaz7mwE6dcviq7N268m1UTPKeuIiCAlsPtImg5MA94FftDG8YdJmixpWu6zd0Q0WpG+UNKL+TaxQYwAtwF9SL8QEpL6AX2BOT97FxEzgTdKX6A0M7OFTOnfDTMz6+5aWlqitbW18v7P/8+mnRiNLU7WPmFKV4dg1mUkTYqIlnptXpE2MzMzM6vAXzY0M+tkks4Hti5tPrv2+9RmZtY9OJE2M+tkEXFoV8dgZmYLn0s7zMzMzMwqcCJtZmZmZlaBSzvMzKwp/uUGM7N5eUXazMzMzKwCJ9JmZmZmZhU4kTYzMzMzq8CJtJmZmZlZBf6yoZmZmbVr63PLf1/IFhcTDp/Q1SF0a16RNjMzMzOrwIm0mZmZmVkFTqTNzMzMzCpwIm1mZmZmVoETaTMzMzOzCpxIm5mZmZlV4ETazMzMzKwCJ9JmHxOSZkuaXLh9T9KPJJ1S6jdQ0hP5/rOSphT2OSdvHy3pJUnL5Mc9c99NC31fkzQz379d0vaSbiqNNVrS0MLjnpI+kHRIqd+zknqWto2UdF6+/6ncZ/VC+/mSvt/Gudhe0hs5ticlnV467qzSudootw2Q9AdJ0yU9JOkqSb07YW5TJD0q6S5JfQttvSVdIekZSZMkTZS0V5051G4715uvmZktHP6DLGYfH+9ExMDiBkkDgFuAYsI5HBhTeLxDRLxS53izga8B/1vbEBFTgIH52KOBmyLimvx4+yZi3Ae4HxgBXNBE/9q4f5d0KnA6cICkLYAhwKB2drsnInaT1AN4WNL1EVH7ywVjI+KwYmdJywI3A0dFxLjCnHo1GWZ7c9shIl6R9GPgeOCbkgTcAPwmIvbL4/UFvlSeQ5Pjm5lZJ/OKtNnHWERMA16XtGVh877Mm0i35SzgSEmd+YZ8BHA0sIakNTu470XAupJ2AM4HDouIDxrtFBHvAJOBNRp03Q+YWEui877jI2Jqk/E1M7eJhTh2BN6PiDlJd0Q8FxHnNjmemZktZE6kzT4+epTKAIbl7WNIq9BI2gp4LSKmF/a7s7DPkYXtzwP3Al/pjOAkrQV8OiIeAK4ChjXYZR4R8SHwbeBa4KmIuLvJcVcB+gPF/sNK56oHsAkwqZ1DDSnuQ2HluANz25W0Cg2wMfBQg/CHlOJct878DpbUKql11qxZDQ5nZmYd4dIOs4+P+Uo7srHAfZKOZv6yDmi7tAPgFOD3pJKHRqLB9mGkJBPgSuAS4Iwmjjv3QBGTJU0FftlE9yGSHiEl0WdFxMuFtnqlHY2ON0+ZRS5tqWk0tzslrQq8Bfyw3sElnQ9sQ1ql/ly9MeuJiItIq/W0tLS0dQ3MzKwCr0ibfcxFxAvATGA7YG9SYt3svtNJZRH7NtH9VWCV0rZVgVqSPgIYKelZ4Ebgs5L6NxtLwYf51sg9EbEZaeX365Lqvckoeoz2a67b02huOwB9Sefyx4Xxtqh1iIhDgZ1ovibbzMwWMifSZgZpFfpM4JmIeLGD+54MHNNEv+lAH0kbwpwvzm0GTM5felw+ItaIiH4R0Y+02j2ig7F0WETMBE4FjmvQ9QpgsKQv1jZI2lbSJu3t1OzcIuJfwHeAA/Pq9B3AspK+Xei2XJPTMjOzj4ATabOPj3KN9KmFtqtJK7P1vmRYrJG+rNwYEY/RuJaXiHgPOAC4NNcQXwN8IyLeICWV15d2uZZ5k81HJb2Yb7/I20YWtr1Y4QuKNRcA20rqlx+Xa6QH5y8l7gYcnn/+7nHgv4BGhcfNzA2AiPgr6RocGhEB7Alsp/Qzgg8Av2HehL9cIz20fEwzM1t4lP5fbWZm3V1LS0u0trZ2dRi2GNr63K27OgSraMLhExp3snZJmhQRLfXavCJtZmZmZlaBf7XDzLotSbsAPyttnhkRe3VFPGZm1r04kTazbisibgVu7eo4zMyse3Jph5mZmZlZBU6kzczMzMwqcGmHmZmZtcu//GBWn1ekzczMzMwqcCJtZmZmZlaBE2kzMzMzswqcSJuZmZmZVeAvG5qZmS0m7tp2uy4Zd7u77+qScc0WdV6RNjMzMzOrwIm0mZmZmVkFTqTNzMzMzCpwIm1mZmZmVoETaTMzMzOzCpxIm5mZmZlV4ETazMzMzKwCJ9JmHzFJsyVNlvSYpEckHS1piUL7NpIekPRkvh1caDtR0tuSPlXY9pak1fIxJ0t6WdJLhcdLN4hjqqRxklbO2/tJeqew/2RJB+a25SVdKGmGpEmSxkvashZH6fgjJZ1X2jZZ0pWlbaMlzcxtj0jaqdC2lKSfSppeiGVUnTnUbt9rY657SLqh8Pj7kp4uPN5d0o35/rOSehbatpd0U3lO+Voc08557eyYphSOeY6k8/P9x0vXa2i98czMrPP5D7KYffTeiYiBADkhvgJYEfiRpNXz4z0j4qGc0N0q6aWIuDnv/wpwNHBc7YAR8SpQO+aJwFsRcXoH4vgNcChwcm6bUWsruRiYCfSPiA8lfQbYqJlJS9oQWBIYIumTEfF/heZjI+IaSTsAFwH98/aTgNWBTSPiXUkr5LnPN4cG7gMuLDz+PPCmpE9FxN+BwblPZ1hYMe0QEa+UDyKpH3BTk2OamVkn8oq0WRfKCdPBwGGSREpmR0fEQ7n9FeC7QHFV8xJgmKRVOzGUicAa7XWQtC6wJXB8RHyY45tZSPAbGQFcDvwR2KNRHJKWA74JHB4R7+bx/hkRJzY53hwRMYuUpK6XN60BXEtKVsn/ndDR4y6IRTEmMzPrGCfSZl0sIp4hrdR+CtgYmFTq0pq317xFSqb/uzPGl7QksBNwY2HzuqXyhCE5hskRMbuNQ/Uo7gP8T6l9GHAlMIaUVNezK1Ard1gPeD4i/tlO+D1KcQ5rp+8EYLCk9YHpwP358VLAZsCDhb53FuZxcTvH7JKYJB3ZbDCSDpbUKql11qxZHZyKmZm1x6UdZounc4DJkhqVb7SnR04U1wCeAG4rtM1X2iHpSw2ON09Jg6SRQEu+3wK8EhHPS3oJuETSqhHxWu5+mqSfAmuSShzmI+mrpDcPqwGDI+KF8pgN3Eda5V2StPL9AHACsDnwZG3VO5tTRiFpe2C+Wuh2LPSYOiIiLiKVy9DS0hId3d/MzNrmFWmzLiZpHWA28HfgcWBQqcsg4LHihoj4B6mW+tAFGLqW8PUFamUl7XkM2CyvYHfUCGADSc8CM0g14XsX2o+NiAGkuu9L8rangbVzXTQRcWmO9w1S4tlRE0hJ62BgYl7pXhbYns6rj+4OMZmZWZOcSJt1IUm9gAuA8yIigPOBkZJqXwJcDfgZ8PM6u/8C+BYL+MlSRLwNHAEcnUsK2uo3g1Rm8uNcz137hY8vtnd8pV8k2Zf0hcF+EdGPVCNdr7zjPGAJSbvkuH4NnCdp2XysJYG6v0LShCeAPsA2wMN522TgELquFnlRjMnMzJrkRNrso1eroX0MuJ305bsfA0TEX4EDgF9JepK0KnlJRIwrHyR/zH89sMyCBhQRDwOPMje5LddIH5G3fwPoDTwtaSowmrSS3p4hwEsR8ZfCtruBjSR9uhRHkH6p47t50yjgr8BUSQ8D9wC/AWrHKtcjn9rOHAP4M/BqRHyQN08E1qH66u/xkl6s3RZyTMUa6csqxmtmZp1I6f/jZmbW3bW0tERra2tXh2EL4K5tt+uScbe7+64uGddsUSBpUkS01GvzirSZmZmZWQX+1Q6zbizXWP+pTtNO+Y+4dDuSrgc+U9p8XETc2hXxwKIZk5mZLTgn0mbdWPEvHn5cRMReXR1D2aIYk5mZLTiXdpiZmZmZVeBE2szMzMysApd2mJmZLSb86xlmixavSJuZmZmZVeBE2szMzMysAifSZmZmZmYVOJE2MzMzM6vAXzY0MzOzdp139LiuDqHTHXbG7l0dgnUDXpE2MzMzM6vAibSZmZmZWQVOpM3MzMzMKnAibWZmZmZWgRNpMzMzM7MKnEibmZmZmVXgRNrMzMzMrIKmEmlJe0oKSRvkxz+SdEqpz0BJT+T7a0r6vaTpkmZIOlvS0rlte0k35fsjJc2S9HDue6ukwQ1iGS1paBttA3Ocu+bHB0kaU+rTM4+5TH58g6T7G4y5u6THJU2VdHI7/WrzmVy4bSTpGUnrl/qeJem4fD7eKO2zc+4Tks4o7HOMpBMljSr0nV24f0S98yPprdLj70h6V9JKhW1zrkup73hJLfn+NyWNLbStmK/vOm2cj9GSZubYHpG0U+m4TxViv6bQdmA+11Pyc+OYwvGqzq12jp+UdHppn10lPZDbJksaK2ntOnOYLOm+Nua6VZ7jFEm/qdenFMvDef53S9qt1OfgHMuTOa5tSuettfC4JW/bpRDjW4Vze1mDOOY7J209j3PbAEl/UHq9PiTpKkm96z1/ytdL6bX3gaRDSv2ezeftUUl3SepbaOst6Qql19AkSRMl7VVnDvO8durM90xJ3yk8vlXSxYXHZ0g6SlI/SVNL+55Y7zlYfG20cV47M6Z3Ssc8UNKf8/3nS9erX73xzMys8zW7Ij0CuDf/F2AMMKzUZzgwRpKA64AbIqI/MABYHmgrAR0bEZvnvqcC10nasANzaC/O64F/l7Rcoc9QYFxEvCdpZWAQsJLaSAazs4AvRsQmwMXt9IM0n4GF2+PAlaTzA4CkJXIcV+ZN95T2uT1vfw/4sqSexQEi4uRaX+Cdwn7nNIitZgTwIPDlJvvXXAysVUgM/ge4JCKeaWefY3Oc3wEuKLXtX4i9lpx8Iff9j4jYFNgKeKMDMbY1t3tyHJsDu0naOo+3CXAucFBEbJD7/A7oV55DvrX1Ru9k4Ds55hMbxHhPfs6vDxwBnKf8JiMn1d8CtomIDYBDgCskrV7Y/1P5PM0REbcWnhOtzD23BzaIY75zks33PJa0LHAz8L8R0T8itgB+CfRqMN+afYD7mfv6LNohIj4LjAeOz+dCwA3A3RGxTkQMIr2O1izPoc5rp2wCMDgfdwmgJ7BxoX0wUPdNUgULI6YZpWNeFhFb5ut3AvNer2c7aR5mZtZAw0Ra0vLANsDXyclgREwDXpe0ZaHrvqQEe0fg3Yi4NPedDRwJfK2U0M4nIu4ELgIO7uhE8j+6+wAjScnzshHxJnAXUPzzRcNznJCSrXGUEt063if/4x0RMzsaG/O/8dgWeC4inmuw379I5+PICmPWJWld0hub46mf0LQpIoKU2J2VV+J2Ak5rcveJwBpN9Ps+cExE/CWP+V5E/KqZAZqZW0S8A0wuxHIc8NOIeKLQ58aIuLuZMQsqPUciYjLpDclhhXiOjYhXcvtDwG+AQwu7nQaM6mB87cVQPidt2Q+YGBFz/sRZRIyPiKnt7FM0AjgaWEPSmm30KT5PdgTej4g5b8Ai4rmIOLfJ8YruAz6f728MTAX+KWkVpU+nNgQeqnDcBVu9O3EAACAASURBVLEoxmRmZh3QzIr0HsAtOXl+VdKgvH0MOfmUtBXwWkRMJ/2DMKl4gJzQPg+s18R4DwEbNBf+PAYDMyNiBmlV64t14uxDWiG/I7eNyO1jaCPxyitFjwOXNPmR6bDSR7A9ImIK8KGkzXKfYjIPMKS0z7qFtvOB/VUoVVhAw0lvHO4B1pfUuyM7R8SjwK3An4DDI+L9JnfdlbS6WPS7wpxrCfkmlJ4/JacVz1WpreHcJK0C9AdqifLGNE5WimP+ro0+M4Cflj/qb1LxOT/f64e0wlxcqZwIvC9phwpjzafOOYE6z2MaX5shpWvzpcIYawGfjogHgKuY/xOtmuLzpJlr095rZ478xuxfSiU7g0nn8M+kRLYFmFJ4Lq9bmsch9Y7ZlTFJGtJsMEqlQq2SWmfNmtXBqZiZWXuaSaRHMLcE4UrmJpxjgaE50SwnhgtCFfdrK86bga0lrUhaNb82ImbnJKs/cG9+k/BB/pi/7HDgEeDbwDhJvSR9ToWa3pLyR+Lv5O1jgOGSlgL2BK4u7FP+KHhGrSG/CbmMVALQjGiwbQRwZUR8CFxLWsXvqPOBlyJifBN9T5M0DbgC+FmprVjacWyTYxfLLAaW2tqb2xBJjwAvAbdGxMvlA0taLScp05RrYuuMuX+d/fYAlgP+k1SG0T8/T1rLfdtQ5Tl/ErkEYgG0d07aeh63557Stbmx0DaMlEDDvK/PmjslvQR8gTb+XyLpfKU69AfbGrP42qnjPlLCWktaJxYeTyj0m1GaR7kkqZGFHlNE3NNsMBFxUUS0RERLr17NVuGYmVkz2k2kJa1K+nj1YknPAscC+0pSRLwAzAS2A/YmJdaQVm8HlY6zIrA28HQTMW0OPNGw17zHXzLHcEKO81xgV0kr5ATgFmAv5k349wVWAWbmffpRf1V6F1KN5u3AT0iJ+UHMTdqbdWUec2fg0Yj4Wwf2PYtUWvPJJvq+SpoXMOcavpLvb0p683BbnvNwOljekX2Yb804NiIGkEoWLmmi/2OUnj/NaGJu90TEZqRVzq9LqiXhjwFbAETEqzlxuohUItKs2nNkCuk6/Z5UqtHsc6T4nJ/v9ZMfP1bcEBF3AD1INeRVtXVO2lLp2mQjgJH52twIfFZS/0L7DkBfUonJjwvjbVHrEBGHksqJqmaDtZrkTUllFPeTVn87sz66O8RkZmZNarQiPRS4PCL6RkS/iFiLlDzXPlYcA5wJPBMRL+ZtfwKWk3QgzElyzwBGR8Tb7Q0maTtSfXRTNbEFO5GS07VynH1JK5J7FeI8CuhNWvGB9A/7rrl/P1KCUK9O+mHgAElLRMRVwHRSrejNHQkwr0q9QvpCZYdW7yPiNdJq3teb6D6e9LH80vnxSODOfH8EcGJtzhHRB+ijwq8kLETnAUtI2qVBv1NIq9irA0haWtI3mjh+U3PL9cunkhJ7gJ8DozTvF1zbreWv42HSOV8mrxReT6phbnidJX0W+CFplb8Wz88krZbbB5Ku4S/r7H4S8N0OxjqfOuekLVcAgyXVyqaQtG0bn+RQ6DMAWD4i1ii83k6h9CYuIv5F+qLpgfkN4B3AspK+XejW0WtTdB+wG6kMbXZ+Xa1MSly7KmldFGMyM7MmNUqkR5CSgqJrmfsP4NWk1aw5CUP+QtpewD6SpgPTgHeBH7QxRq0Wc1rus3fxi19tuFDSi/k2sYk4bwP6kD6ujlzr3Je0+lOLeybwhub9AiWkX2MQMFXSJOBvwIWkj/Drnb9ybWnxVx7GkGphryvtU66prPfzfmeQvtXfroi4iVQjPCnXd27N3ARpOPOfp+uZ+wZip8J5fVFS7YtQNxe2XU0F+XlRTvyKNdK3535/ICXdt0t6jFQju2ITQzSaW9EFwLaS+uVV5P8GLlP6ybgJpC95XVHof1rp+ixdOt6vgSnAI7mc49PAMcA1qv8F2yHKP39HSqCPiIg/5fnfSFq5v0/Sk6Q3lQdExF/LB8nnqrOKXueck/x4vudx/nRnN+BwpZ+/exz4ryZiaPT6nCPPcwxwaH7O7Alsp/QThA+QvnhZTPibee3UTCG9hu4vbXsj8pc7K6j32lgYMZVrpJst9TIzs4VI6d8qMzPr7lpaWqK1tdnSfbO5zjt6XONOi5nDzti9cSczQNKkiKj7YwL+y4ZmZmZmZhUs1dUBtEXS+aSyhKKzI/8+tS06fK0WXbkmvfxrKTMjYq96/Rd3ubb8T3WadoqIVz/qeGDRjMnMzDrHIptI52/o22LA12rRFRG3kn73+2MhJ6aNfn3kI7UoxmRmZp3DpR1mZmZmZhU4kTYzMzMzq2CRLe0wMzOzRYN/4cKsPq9Im5mZmZlV4ETazMzMzKwCJ9JmZmZmZhU4kTYzMzMzq8BfNjQzM7N2nXzA0K4OwWyBjPrtNQvluF6RNjMzMzOrwIm0mZmZmVkFTqTNzMzMzCpwIm1mZmZmVoETaTMzMzOzCpxIm5mZmZlV4ETazMzMzKwCJ9JmZmZmZhU4kbbFnqQ9JYWkDfLjH0k6pdRnoKQn8v01Jf1e0nRJMySdLWnp3La9pJvy/ZGSZkl6OPe9VdLgBrGMllT3LxfkGELSrvnxQZLGlPr0zGMukx/fIOn+BmPuLulxSVMlndxOv9p8JhduG0l6RtL6pb5nSToun483SvvsnPuEpDMK+xwj6URJowp9ZxfuH1Hv/Eh6q/T4O5LelbRSYduc61LqO15SS77/TUljC20r5uu7ThvnY7SkmTm2RyTtVDruU4XYrym0HZjP9ZT83DimcLyqc6ud4yclnV7aZ1dJD+S2yZLGSlq7zhwmS7qv3lzNzGzhcCJt3cEI4N78X4AxwLBSn+HAGEkCrgNuiIj+wABgeaCtBHRsRGye+54KXCdpw06K83rg3yUtV+gzFBgXEe9JWhkYBKzUVjKYnQV8MSI2AS5uEMPYiBhYuD0OXEk6PwBIWiLHcWXedE9pn9vz9veAL0vqWRwgIk6u9QXeKex3ToPYakYADwJfbrJ/zcXAWrVEH/gf4JKIeKadfY7NcX4HuKDUtn8h9qEAkr6Q+/5HRGwKbAW80YEY25rbPTmOzYHdJG2dx9sEOBc4KCI2yH1+B/QrzyHf2n2jZ2ZmncuJtC3WJC0PbAN8nZwMRsQ04HVJWxa67ktKsHcE3o2IS3Pf2cCRwNdKCe18IuJO4CLg4ApxCtgHGElKnpeNiDeBu4DdC12H5zghJVvjKCW6dbwPrJljnNnR2Jj/jce2wHMR8VyD/f5FOh9HVhizLknrkt7YHM/cNxxNiYgADgHOyqvUOwGnNbn7RGCNJvp9HzgmIv6Sx3wvIn7VzADNzC0i3gEmF2I5DvhpRDxR6HNjRNzdzJh53IMltUpqnTVrVrO7mZlZE5xI2+JuD+CWnDy/KmlQ3j6GnHxK2gp4LSKmAxsDk4oHyAnt88B6TYz3ELBBhTgHAzMjYgYwHvhinTj7kFbI78htI3L7GNpIvPLq8ePAJZL6NRHHsFKZRo+ImAJ8KGmz3KeYzAMMKe2zbqHtfGD/YqnCAhpOeuNwD7C+pN4d2TkiHgVuBf4EHB4R7ze5667ADaVtvyvMuZaQb0Lp+VNyWvFcldoazk3SKkB/oJYob0x6zrWnOObvyo0RcVFEtERES69evRocyszMOsKJtC3uRjC3BOFK5iacY4GhOdEsJ4YLQhX3ayvOm4GtJa1IWjW/NiJm5ySrP3BvfpPwQf6Yv+xw4BHg28A4Sb0kfa5Y01tSLu14J28fAwyXtBSwJ3B1YZ9yaceMWkN+E3IZcEST5yEabBsBXBkRHwLXklbxO+p84KWIGN9E39MkTQOuAH5WaiuWdhzb5NjFMouBpbb25jZE0iPAS8CtEfFy+cCSVsvJ8rRaXXadMfdvMk4zM+sETqRtsSVpVVKpxsWSngWOBfaVpIh4AZgJbAfsTUqsIa3eDiodZ0VgbeDpJobdHHiiYa95j79kjuGEHOe5wK6SVsiJ7C3AXsyb8O8LrALMzPv0o/6q9C7A3blu+SekxPwg5ibtzboyj7kz8GhE/K0D+55FKq35ZBN9XyXNC5hzDV/J9zclvXm4Lc95OB0s78g+zLdmHBsRA0glFJc00f8xSs+fZjQxt3siYjPSCvTXJdWS8MeALQAi4tWcnF9EKhExM7Mu5kTaFmdDgcsjom9E9IuItUjJ85DcPgY4E3gmIl7M2/4ELCfpQJiT5J4BjI6It9sbTNJ2pPropmpiC3YiJadr5Tj7klYk9yrEeRTQm1SrCynJ2jX370dK3urVST8MHCBpiYi4CpgO7EdKqJuWV5lfIX2hskOr9xHxGnAVKZluZDypvGTp/HgkcGe+PwI4sTbniOgD9JHUtyPxVHQesISkXRr0O4W0ir06gKSlJX2jieM3Nbdc434qKbEH+DkwqvQF13Zr+c3M7KPjRNoWZyNIv3xRdC1zV/quJq3wzUkM8xfS9gL2kTQdmAa8C/ygjTFqNcXTcp+9i1/8asOFkl7Mt4lNxHkb0IdUdhG51rkvMOdn73KC9UbpC5SQfm1EwFRJk4C/ARcCV+SylrbmU7sVf+VhDKn++7rSPuUa6Xo/73cG0LPO9nlExE2kGuFJuYZ4a+YmjcOZ/zxdz9w3EDsVzuuLkj6ft99c2HY1FeTnxUnAdwubizXSt+d+fyAl3bdLeoxUv7xiE0M0mlvRBcC2kvrl+vX/Bi5T+jm+CcCGpFKUmtNK12fpOsc0M7OFQOnfDzMz6+5aWlqitbW1q8OwxdDJB9T9eXyzxcao37b11aHGJE2KiJZ6bV6RNjMzMzOrYKmuDsBscSTpfFJZQtHZtd+ntkWHr5WZmS0sTqTNKoiIQ7s6BmuOr5WZmS0sLu0wMzMzM6vAK9JmZmbWrgX5opZZd+YVaTMzMzOzCpxIm5mZmZlV4ETazMzMzKwCJ9JmZmZmZhU4kTYzMzMzq8C/2mFmZtYNPXHyHZ12rA1H7dhpxzLrTrwibWZmZmZWgRNpMzMzM7MKnEibmZmZmVXgRNrMzMzMrAIn0mZmZmZmFTiRNjMzMzOrwIm0mZmZmVkFTqStU0jaU1JI2iA//pGkU0p9Bkp6It9fU9LvJU2XNEPS2ZKWzm3bS7op3x8paZakh3PfWyUNbhDLaElD22gbmOPcNT8+SNKYUp+eecxl8uMbJN3fYMzdJT0uaaqkk9vp1+58lByf26ZJulPSxoX2ZyVdW3g8NM/3q5Im59v7kqbk+6c2iGOypCclHVloO1HSS4XjTZa0cm77N0l3S3oqz+FiScvl451XGmO8pJa2zn1h++w8xlRJ42pj5bb+km7Kz5FJ+XxsW2cOtdtGbcz3ekl7Fh4/Jen4wuNrJX25+NwrtM15PhXnlK9Fz3bOa2fG9EbpmMMK918uXa+l641nZmadz4m0dZYRwL35vwBjgGGlPsOBMZIEXAfcEBH9gQHA8kBbCejYiNg89z0VuE7Shp0U5/XAv0tartBnKDAuIt7LSd0gYCVJ67Rz3LOAL0bEJsDFDWJobz6HAoOBzSJiAHAKcKOkZQv7DyonZxFxaUQMjIiBwF+AHfLj7zWIYyCwNTBK0lqFtjNrx8u3f0jqDVwNHBcR60fE5sAtwAoN5ltTPvc17+QxNgFey+eAPOebgYsiYt2IGAQcDhSvw9hSnI+3MfYE0nlF0mrA/wGfL7R/HrivyXk0sjBiuqd0zLGF630B816v9ztpHmZm1oATaVtgkpYHtgG+TkqWiYhpwOuStix03ZeUYO8IvBsRl+a+s4Ejga+VEtr5RMSdwEXAwRXiFLAPMJKUPC8bEW8CdwG7F7oOz3ECfBkYB1xZm1sb3gfWzDHObDamOvM5DjgsIt7O7X8kJVP7F3Y7AxjV7BhNxPAq8DTw6QZdDwV+ExETC/teExF/azRGvXPfRteJwBr5/v7AxIi4sTDe1IgY3Wi8Ou4jJ635v+OAXvkTgM+QkvmXKxx3QSyKMZmZWQc4kbbOsAdwS06eX5U0KG8fQ04+JW0FvBYR04GNgUnFA+SE9nlgvSbGewjYoEKcg4GZETEDGA98sU6cfUgr5LW/rTsit49h/pVU8j5LAI8Dl0jqVyGuh4ANJK0IfDIinim1t5LOWc1VwBaSmjlXDUlaG1gWeLSw+chCqcCdedsmlK5bSbHcYDLQUmhr69wX41gS2AmoJc4bk85Ne+YZU1KPNvpNAjbJZQ+DSQn7U8CG+XFxNXpIaR5fahDDRx6TpHWbDUbSwZJaJbXOmjWrg1MxM7P2OJG2zjCCtGJL/m8t4RwLDM2JZnGVd0Gp4n5txXkzsHVOZPcFro2I2bmUoT9wb36T8IGkTeoc93DgEeDbwDhJvSR9TtI1C2k+s4HTgO93cL+yYZIeJa1G/zIi3i20FUsFdmjyePOUNJDeANS0de4BeuSE9WWgN3BbvYPnmuKpkq5ra8yIeKfevhHxHvAYsAWwFfBnUuI6ON8mFLrfU5rHjeXjNbDQY8pvSJoSERdFREtEtPTq1auDUzEzs/Y4kbYFImlVUqnGxZKeBY4F9pWkiHgBmAlsB+xNSqwhrd4OKh1nRWBtUlLXyObAEx2Mc8kcwwk5znOBXSWtkBOdW4C9mDfh3xdYBZiZ9+lH/VXpXYC7I+J24CekxPwg5iaOTc0nr8r/X51a7EGkhKvocmBbYC2qGxsRnyUlbadKWr1B/8coXbdmtHfuc5d3csLal/Sm4tDCeFvUjhMRe5FKQ1btaAzZBNI5WyEiXgfuZ27S2ln10d0hJjMza5ITaVtQQ4HLI6JvRPSLiLVIyfOQ3D4GOBN4JiJezNv+BCwn6UCYk2idAYyu1Qa3RdJ2pHriX3Uwzp2ARyNirRxnX+BaUvJci/Mo0oporQZ4BLBr7t+PlETWq5N+GDhA0hIRcRUwHdiPlFC3q858TgPOqZUDSNqZVH9+RXG/iPiAdF6PZAFFRCspMf/vBl3PAw4q1r3nX5Xo3WC/Rue+FsfbwBHA0ZKWIs15a0nF0op2a+gbuA/4FunTA0ilLFuR3sBNXYDjLohFMSYzM2uSE2lbUCNIv3xRdC1zV26vJtW6zinriIggJVH7SJoOTAPeBX7Qxhi1mtNpuc/eEdFoRfpCSS/m28Qm4rwN6ENapY1c69yXtEJYi3sm8EbpC5SQfm1EwFRJk4C/ARcCV+Sylo7M51zgQWCKpKeAHwJ7tFEe8GtgqQbnoVk/A75aWCUu1khPltQvf6lwOHC60k+1PUFajf9ng2M3OvdzRMTDpGRyRJ7zbsAhkp7J1/F44KTCLuV65PZ+GvE+0i9+TMxj/Qv4O9AaER82mENbHi08z36xEGMq10jX/XlHMzP7aCnlNGZm1t21tLREa2tr447WLTxx8h2NOzVpw1E7dtqxzBY3kiZFREu9Nq9Im5mZmZlV0FkfC5t95CSdT/pjIkVn136f2kDSV5m/9nlCRBxar//iTtKmpHrvovciolyO85FZFGMyM7PO4UTaFlvdNRnsTPlNxcfmjUVETAEGdnUcRYtiTGZm1jlc2mFmZmZmVoFXpM3MzLohf0HQbOHzirSZmZmZWQVOpM3MzMzMKnAibWZmZmZWgRNpMzMzM7MKnEibmZmZmVXgX+0wMzOzdp144oldHUIli2vctvjwirSZmZmZWQVOpM3MzMzMKnAibWZmZmZWgRNpMzMzM7MKnEibmZmZmVXgRNrMzMzMrAIn0mZmZmZmFTiR7mSSZkuaXLh9T9KPJJ1S6jdQ0hP5/rOSphT2OSdvHy3pJUnL5Mc9c99NC31fkzQz379d0vaSbiqNNVrS0MLjnpI+kHRIqd+zknqWto2UdF6+/6ncZ/VC+/mSvt/Gudhe0hs5ticlnV467qzSudootw2Q9AdJ0yU9JOkqSb07YW5TJD0q6S5JfQttvSVdIekZSZMkTZS0V5051G4715nrspJukDRV0sOS1ql3TkqxTJH0uKSTJC1baN9Y0h2Snsrn4IeSVDhvH0r6bKH/VEn9JP05x/d86dz2axBHvXMy3/M4b/+EpFML12aipC8UjtezcIx61+sGSfeXtp2Yn+eT8/kYUWo/Kj9/pkh6RNIvJH2iNId5Xjt15rqZpMmFxyMkvVM4zqaSHs33x0tqKfTtJ2lqeU4qvDbaOK+dHdNThWNeI2lU4XHxeh1RbzwzM+t8/oMsne+diBhY3CBpAHALUEw4hwNjCo93iIhX6hxvNvA14H9rGyJiCjAwH3s0cFNEXJMfb99EjPsA9wMjgAua6F8b9++STgVOBw6QtAUwBBjUzm73RMRuknoAD0u6PiIm5LaxEXFYsXNOKG8GjoqIcYU59WoyzPbmtkNEvCLpx8DxwDdzgnoD8JuI2C+P1xf4UnkOTYz7RkRsImkVIBr0r8WyPHARcCFwUD5PNwLfjog/SloOuBb4L+D8vO+LwChgWPGAEbFljn8k0FI+tw3imHNO8vb5nsfZT4BPA5tExHuSegPbNTEOklYmPVfekrRORDxTaD4zIk6X1B+YJOmaiKi9IfoPYKuI+IekpYGjgB7AB8U5NBh+CrC2pBUi4p/AYOAJYHPggfz4vmbm0aSFEdP+EdFaOsbJAJLeauN6mZnZQuQV6Y9AREwDXpe0ZWHzvsybSLflLOBISZ35pmcEcDSwhqQ1O7jvRcC6knYgJXaHRcQHDfYhIt4BJgNrNOi6HzCxlkTnfcdHxNQm42tmbhMLcewIvB8Rc5LuiHguIs5tcrya9/OYiojXI+IfzewUEW8BhwB7SlqVNP8JEfHH3P42cBjwvcJuNwEbS1q/gzG2p3hO6spJ/TeBwyPivRzf3yLiqibH+DIwDriS9EZyPhExHXgbWCVvGkV6U/GP3P5+RJwaEW82OWbtuB8CrUDtNTiI9PwdnB8PBibU2XWhWRRjMjOzjnEi3fl6lD4Sr60ajiEnD5K2Al7LSUPNnYV9jixsfx64F/hKZwQnaS3g0xHxAHAVpVXNRvI//t8mrZI+FRF3NznuKkB/oNh/WOlc9QA2ASa1c6ghxX0orBx3YG67klahATYGHmoQ/pBSnOvW6fMMsAVwSp22duWkcCbp/GxMaf4RMQNYXtKKedOHwM+BH3R0rHYUzwnUfx6vBzzfIIm9s3BtLi61jSC9Dsbk+/PJn3JMz59+rAgsHxEzG8Te1munbAIwWNInSedwPPMmrcXV398V5vGHBuN/5DFJOq3ZQCQdLKlVUuusWbM6OA0zM2uPSzs6X1sfiY8F7pN0NPOXdUD7HwWfAvyeVPLQSFslBbXtw0hJJqSVwUuAM5o47twDRUzONaO/bKL7EEmPkJLEsyLi5UJbvdKORsebp8wil7bUNJrbnXnV9y3gh/UOLul8YBvSKvXn6o1ZZ58ewKXA+sDlkr4TEWdJuhk4rsnV9IYTL7kCGCXpMx3cr6ytc1KvROmzNDbneZxLco7J93uTngP3RkQo1bFvUjg3R0r6KjAA2L3egSXtAvwMWBnYLyJqSWYzZRSQktKjgXuAByNihqT1JPUiJewzCn3nlFEo1ZjfVD5YAws1po6IiItInyTR0tLSqOTIzMw6wCvSH5GIeIG06rgdsPf/b+/ug6Wq7zuOvz+gggZtQ1CjtkK0PqGGm0hMK8RApdEmaUTjE4NGfJhqgmYam1pT7YSU6dTEtNbEgBOLgo7R+jBEolZFhYCOEVCQJ0UYwREq4iOWBB+Qb//4/VYOy967e/de7l7vfl4zO3f3t+ec/Z7fbxm++zvfcw4psa513ZWksogzalj8DbYdFi/pD5T+Ux8DjJO0hlSL+9lcl9peW/OjmrkRMYQ003qBpGp1nMtou+a6LdX2bSQwkNSXPyp83udLC0TEeOAEaq/JBjgaeD0iXiON7Zn5hK/+efttkrQnMAh4AVhO2f4rnbi4qTgTHBFbSD8S/rEdcVZSqU9as4pU07tXleUqOYP0vVydx2cQ289KXxsRR5L6b4qkvnl/N5V+LETEQzm5XwrsVkcMvwO+AAwjlbJAqjc/q/C6q3XHmMzMrEZOpLvW7cC1wIsRsbad6/4reXavipXA/pKOgI9OnBsCLMonPfaLiAMiYlBEDCLNdlc8zN6Z8uH5q6me+P2KdKj7a6UGScdLOqqtlWrdt5yA/h3wrTwT+xjQV9K3C4vtUeNulawEDpd0ZET8HriAdELmvRHR5gxgPtlwEvDriHgLuA0YrnxlkDzb/TNSKUe5qcAo2pf076BCn7S23B+AKcB1+aQ/JO0t6fQaPmYMcFJhbI6hQp10RMwg1Q2fm5v+DZicT1RE6ZBF3/L1apFP6HsZOI9tSeqTpH1vSC1yd4zJzMxq50S685XXll5deO8u0sxspZMMizWVt5S/GRHLqF7LSz4J7Gzg5lzfeTdwYURsJCUz08tWuYftk83Fktbmx3/ktnGFtrV1nKBYcgNwvLZdjq28Rvq4fFLi14FLlS6xtpx0xYpqxZ217BsAEfEKaQzG50R3NPBlpcsIzgOmsX3CX14jfVrZ9t4iJX63SlpISozHAhdKOo7KZuXymHmkOviL8rY2AycDV0laQbqyw3xgh8usRcT7pCR7n9Y6pVbFPslNrX2PryKNxfIc/31Amyf+5fEeSJp9LX3eamCjtj8Bt+RfgMsk9SJdreZR4CmlS8E9ASzMj5I2/+2UeQLok48QQUpaD6L+K3a09m9jZ8RUrJF+pM54zcysE6nKhJmZmfUQQ4cOjQUL2l1mbcaECRMaHUJdPq5xW/ci6emIGFrpPc9Im5mZmZnVwVftsA4rXE2haHVEnNKIeGx7kp4C+pQ1nxPpxj49Tr7yyrCy5usi4uZGxAPdMyYzM+s4J9LWYRHxEPBQo+Owykp3PGwW+cor3Up3jMnMzDrOpR1mZmZmZnVwIm1mZmZmVgeXdpiZmVmbfPULs8o8I21mZmZmVgdfR9rMrElIeg14qZ2rDQBe3wnhfJy4D9wHzb7/0Nx9MDAiKt5F2Im0mZm1StKCKQsW9wAACtdJREFU1m5E0CzcB+6DZt9/cB+0xqUdZmZmZmZ1cCJtZmZmZlYHJ9JmZtaWXzY6gG7AfeA+aPb9B/dBRa6RNjMzMzOrg2ekzczMzMzq4ETazMzMzKwOTqTNzGwHkk6XtEzSVklDy977gaRVklZIOrFRMXYlSRMkrZO0KD++2uiYuoKkk/I4r5J0RaPjaQRJayQtyeO+oNHxdAVJN0naIGlpoa2/pJmSVua/n2xkjN2FE2kzM6tkKXAqMKfYKGkwcBZwJHASMElS764PryGujYiW/Hig0cHsbHlcfwH8NTAYGJPHvxmNzOPeLNdRnkr69110BfBoRBwCPJpfNz0n0mZmtoOIeC4iVlR462Tgjoh4LyJWA6uAY7s2OusixwKrIuLFiHgfuIM0/tbDRcQc4M2y5pOBafn5NGB0lwbVTTmRNjOz9jgAeLnwem1uawaXSFqcD3s3w2HtZh7rogAelvS0pL9tdDANtG9EvJKfrwf2bWQw3cUujQ7AzMwaQ9IjwKcrvHVlRNzb1fE0Wlv9AUwGJpKSqonAvwPnd1101kDDI2KdpH2AmZKezzO2TSsiQpKvn4wTaTOzphURo+pYbR3wp4XXf5LbPvZq7Q9JNwL37eRwuoMeO9btERHr8t8NkqaTSl6aMZF+VdJ+EfGKpP2ADY0OqDtwaYeZmbXHDOAsSX0kfQY4BJjX4Jh2upw4lJxCOhmzp5sPHCLpM5J2I51kOqPBMXUpSZ+QtGfpOfAVmmPsK5kBnJufnws03VGrSjwjbWZmO5B0CvBzYG/gfkmLIuLEiFgm6U5gObAFGB8RHzYy1i7yE0ktpNKONcBFjQ1n54uILZIuAR4CegM3RcSyBofV1fYFpkuClDP9KiIebGxIO5+k24ERwABJa4EfAlcDd0q6AHgJOKNxEXYfvkW4mZmZmVkdXNphZmZmZlYHJ9JmZmZmZnVwIm1mZmZmVgcn0mZmZmZmdXAibWZmZmZWByfSZmbW40ja1IF110haImlofj1b0gpJz0p6QtJhhWXvlnRQhW2Mk3R9vTF0BkmDJM1uwOfeIemQwutZkjaV+rPGbQySVPf1miV9KGmRpP3z69KYLpb0sKRP53ZJekzSXhW2MUHS9+uNoTNIGiFpalnbp/K+LZK0XtK6wuvdCvu+VNJvJP1xYVv3lW1rqqTT8vPS97y0rbtz+yWSzi+sc03+3Ib2TXfhRNrMzGxHIyNiQeH12IgYAkwDrgGQdCTQOyJebESA3dhk4PLSi4gYCSxoffGdYnNEtETE/xbaRkbEZ3Ms/5Tbvgo8GxHvdHF8dYuIN/K+tQA3ANeWXkfE+2zb96OAN4Hx7dj82MK2TsttNwGXFj7/H/LnGk6kzcysB8szjtfk2bklks7M7b0kTZL0vKSZkh4ozcxVMQf4s/x8LIW7u0k6T9ILkuYBwwrte0u6R9L8/BiW2ydImiZprqSXJJ0q6Sc5zgcl7ZqXO0HSwtx+k6Q+uf1qScvzLOtP29EnvfNMZKlPvpfbZ0u6rjCbeWxu/0T+3Hk5jpML2/lpXnaxpFKyNRcYJalTbvomqa+km3OsCyWNzO17SLoz98F0SU/VOOvd1hhemcfwcaB45OHgPCZP5/E6PLdPlTRZ0u8kvZhnfW+S9FxxJlnSmBz/Ukk/zm0Vx6GTPQkc0JENRMQfgDWl74Ntz3c2NDOznuxUoAUYAgwA5kuaQ0p0BwGDgX2A50gzb9X8DbAkPx8G3A4f3UL8R8AxwEZgFrAwL3cdadbwcUkHku4UeER+72BgZI7jSeCbEXG5pOnA1yQ9CEwFToiIFyTdAnxb0q2kW5UfHhFROnxfoxbggDxjSdm6e0REi6Tjc38cBVwJPBYR5+dl50l6BPgWqQ9b8l0Q+wNExFZJq0h9/nQ74mrN+LTZODonsA9LOhT4DvBWRAyWdBSwqMbtfZ3tx/AiAEnHkG6D3kLKj54pxP9L4OKIWCnpi8Ak4C/ze58E/gL4Buk22sOAC0nftRZgA/Bj0nfjrRz/aOBlWh+HDpPUGzgBmNKO1W6TtDk/n5lnnyHN4n8JmNeJIfYITqTNzKwnGw7cnm9j/qqk3wJfyO13RcRWYL2kWVW2U0ow1rDtMPd+wGv5+ReB2RHxGoCk/wYOze+NAgYr3WYaYC9J/fLz/4mIDyQtId2Gu3T76SWkJPUwYHVEvJDbp5ESy+uBd4EpSnWv29W+VvEicJCknwP3Aw8X3rsdICLmSNorJ3dfAb6hbTWxfYED837dEBFb8jpvFrazAdifzkmkh5NuV09EPC/pJVLfDif9SCEilkpaXGU7syR9CCwGrspt/SPi//LzLwHT8wwskmbkv/2A44C7CmPYp7Dd3+QfM0uAVyNiSV5vGWkMB7L9d+M24HhgIq2PQ0fsLmkRaSb6OWBmbm/tVtbF9rFlJU0lG4DDOym+HsWJtJmZWXWVEozNpKSyml7An0fEu8XGnJS9Bx/N4n4QEaWkZitt/B+dZ4CPJc04ngZcwrYZ0jZFxFuShgAnAhcDZwClk8nKk60ARJopX1Eh/tb0JfVPqySdAvwwv7ywlQSuM42MiNfL2rZI6pV/ULWmF/B2rkmu5L38d2vheen1LsAHlVaqMg4dsTkfVdiDdPRjPPAz4A3S7HlRf6C8TyqpOp7NyjXSZmbWk80Fzsz1qHuTZgLnAU8A31Sqld4XGFHHtp9jW63tU8CXla6osCtwemG5hymcrJUP99dqBTBIUulzzgF+m2dJ/ygiHgC+RyqjqImkAUCviLiHNDP7+cLbpRry4cDGiNhISsYuVc6cJX0uLzsTuKhUC10q7cgOBdq86kZETC+c2NZWEj2XVMtMLuk4kNQvT5CSTyQNBo6utu8VrABKV12ZA4yWtLukPUllPOQTEVdLOj1/lnICXKt5pO/GgFxuMYY0hm2NQ4flmfXvAn+fx2glsL+kI/J+DCR9b2opiak6ns3KM9JmZtaTTSfVrz5Lml29PCLWS7qHNJu7nFSr+gyptrk97icl4I9ExCuSJpDqnN9m++Tku8AvcunBLqSE7eJaPiAi3pV0HqmsYBdgPumKCf2BeyX1Jc0YX9aOuA8AbpZUmkz7QeG9dyUtBHZl2+zoROA/gcV5ndWkOuP/IiVYiyV9ANwIXJ9/mGyOiPXtiKktk4DJuXRiCzAuIt6TNAmYJmk58DywjPrHcFVEPJNLcp4llTLMLyw3NsdwFalv7sjLVZW/G1eQ6uYF3B8R9+ZkvLVx6BQRsTB/78ZExK2Szs6f2Zc0U35h/rFUUqyRfj0iRuXnw4AJnR1fT6BtR5HMzMyah6R+EbFJ0qdIs4bDcpK9BhhaoQygfP3dScnRsFyD3a1IGgRMjYgRNS4/G/h+R0ss8tUn3omIKYW2Ttl22ef0BnbNPzYOBh4BDouI9yVtioh+VTZROkn0loj4q86KqzNJGkH64TCugTF8DrgsIs4ptE0ANkVEzVeL6alc2mFmZs3qvnxS1lxgYmEG9TXgUVW5lFpEbCbV+Hbo8mI90NukkyKBdEMWUvlExVrhDtgDeFzSs6QjD9/J11EGeEeFG7K0JiJeAW5UhRuy2EcGAP9ceiHpGuBs4PcNi6gb8Yy0mZlZD5SvuDE6IqY2OharTz6q0BIRv25wKNYKJ9JmZmZmZnVwaYeZmZmZWR2cSJuZmZmZ1cGJtJmZmZlZHZxIm5mZmZnVwYm0mZmZmVkd/h8YLrKom1DC9QAAAABJRU5ErkJggg==\n", | |
| "text/plain": [ | |
| "<Figure size 432x288 with 1 Axes>" | |
| ] | |
| }, | |
| "metadata": { | |
| "needs_background": "light" | |
| }, | |
| "output_type": "display_data" | |
| } | |
| ], | |
| "source": [ | |
| "plot_scores(scores2)" | |
| ] | |
| } | |
| ], | |
| "metadata": { | |
| "kernelspec": { | |
| "display_name": "Python 3", | |
| "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.8.2" | |
| } | |
| }, | |
| "nbformat": 4, | |
| "nbformat_minor": 4 | |
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| attrs==19.3.0 | |
| bdd2dfa==0.4.1 | |
| blessings==1.7 | |
| dd==0.5.5 | |
| funcy==1.14 | |
| lazytree==0.3.1 | |
| multiprocess==0.70.9 | |
| py-aiger==4.0.2 | |
| py-aiger-bdd==0.3.1 | |
| py-aiger-bv==2.0.0 | |
| py-aiger-cnf==3.0.0 | |
| py-aiger-coins==1.4.0 | |
| py-aiger-gridworld==0.2.0 | |
| py-aiger-ptltl==1.2.0 | |
| py-aiger-sat==1.1.0 | |
| termplotlib==0.2.4 | |
| mce-spec-inference==0.1.0 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment