{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Formal verification of deep neural networks: a tutorial\n",
"\n",
"The aim of this tutorial is to give a glimpse on the practical side of Formal Verification for Deep Neural Networks.\n",
"This tutorial is divided in four part:\n",
"1. Verification by hand\n",
"2. Small problem verification\n",
"3. Real use case application\n",
"4. Image classification\n",
"\n",
"The tutorial material was written by Augustin Lemesle (CEA List) with material provided by Serge Durand (CEA) based on a previous tutorial created by Julien Girard-Satabin (CEA LIST/INRIA), Zakaria Chihani (CEA LIST) and Guillaume Charpiat (INRIA)."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Part 1: Verification by hand\n",
"\n",
"This first part aims to give a rough overview of the challenges posed by the verification of a neural network. In the first part of the lesson you should have seen a technique called Abstract Interpretation which can leverages intervals to estimate the output of a network. You should have seen an example by hand of this method. In this part, we will developp a small class that will calculate the output automatically with intervals.\n",
"\n",
"### Step 1: Encode the network\n",
"\n",
"\n",
"\n",
"With the above network create a function `network(x1, x2)` which reproduces its comportement. It must pass the tests created in `test_network`. For the relu layer, its function is already implemented here."
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [],
"source": [
"def relu(x):\n",
" return max(0, x)\n",
"\n",
"def network(x1, x2):\n",
" # apply all the operations\n",
" x3 = 2*x1 + x2 + 1\n",
" x4 = -x1 + x2\n",
" x3p = relu(x3)\n",
" x4p = relu(x4)\n",
" x5 = 2*x4p - 0.5*x3p - 1\n",
" x6 = x4p - x3p + 2\n",
" y = x5 - x6\n",
" return y"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {
"scrolled": true
},
"outputs": [],
"source": [
"def test_network():\n",
" assert network(0, 0) == -2.5\n",
" assert network(0, -1) == -3\n",
" assert network(0, 1) == -1\n",
" assert network(-1, 1) == -1\n",
" assert network(-1, 0) == -2\n",
" assert network(-1, -1) == -3\n",
" assert network(1, 0) == -1.5\n",
" assert network(1, -1) == -2\n",
" assert network(1, 1) == -1\n",
" \n",
"test_network()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Step 2: Create an Interval\n",
"\n",
"Following the rules of interval arithmetic write a class representing an Interval by overriding Python operators. A skeleton is avalaible below.\n",
"\n",
"Intervals rules:\n",
"- $[l, u] + \\lambda = [l + \\lambda, u + \\lambda]$\n",
"- $[l, u] + [l', u'] = [l + l', u + u']$\n",
"- $-[l, u] = [-u, -l]$\n",
"-$[l, u] - [l', u'] = [l - u', u - l']$\n",
"- $[l, u] * \\lambda =$\n",
" - si $\\lambda >= 0$ -> $[\\lambda * l, \\lambda * u]$\n",
" - si $\\lambda < 0$ -> $[\\lambda * u, \\lambda * l]$\n",
" \n",
"We will also need to update the relu for it to work on intervals.\n",
"\n",
"Some tests are available for you to check if the class implementation is correct."
]
},
{
"cell_type": "code",
"execution_count": 64,
"metadata": {},
"outputs": [],
"source": [
"class Interval:\n",
" def __init__(self, lower, upper):\n",
" self.lower = lower\n",
" self.upper = upper\n",
" \n",
" def __add__(self, other):\n",
" if isinstance(other, Interval):\n",
" return Interval(self.lower + other.lower, self.upper + other.upper)\n",
" else:\n",
" return Interval(self.lower + other, self.upper + other)\n",
" \n",
" def __sub__(self, other):\n",
" if isinstance(other, Interval):\n",
" return self.__add__(other.__neg__())\n",
" else:\n",
" return Interval(self.lower - other, self.upper - other)\n",
" \n",
" \n",
" def __neg__(self):\n",
" return Interval(-self.upper,-self.lower)\n",
" \n",
" def __mul__(self, other):\n",
" if isinstance(other, Interval):\n",
" return Interval(self.lower, self.upper)\n",
" else:\n",
" if(other < 0):\n",
" return Interval(self.upper * other,self.lower * other)\n",
" else:\n",
" return Interval(self.lower * other, self.upper * other)\n",
" \n",
" \n",
" def __rmul__(self, other):\n",
" return self.__mul__(other)\n",
" \n",
" def __str__(self):\n",
" return f\"[{self.lower}, {self.upper}]\"\n",
"\n",
" def __repr__(self):\n",
" return self.__str__()\n",
"\n",
" def __eq__(self, other):\n",
" return self.lower == other.lower and self.upper == other.upper"
]
},
{
"cell_type": "code",
"execution_count": 65,
"metadata": {},
"outputs": [],
"source": [
"def relu(x):\n",
" if isinstance(x, Interval):\n",
" lower = max(0, x.lower)\n",
" upper = max(0, x.upper)\n",
" return Interval(lower, upper)\n",
" else:\n",
" return max(0, x)"
]
},
{
"cell_type": "code",
"execution_count": 66,
"metadata": {},
"outputs": [],
"source": [
"def test_interval():\n",
" assert Interval(0, 1) == Interval(0, 1)\n",
" assert -Interval(0, 1) == Interval(-1, 0)\n",
" assert Interval(0, 1) + Interval(1, 2) == Interval(1, 3)\n",
" assert Interval(0, 1) - Interval(1, 2) == Interval(-2, 0)\n",
" assert Interval(-1, 2) * 3 == Interval(-3, 6)\n",
" assert Interval(-1, 2) * -3 == Interval(-6, 3)\n",
" assert relu(Interval(-2, 3)) == Interval(0, 3)\n",
" \n",
"test_interval()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Step 3: Run the network with intervals\n",
"\n",
"At this point you should be able to run the network using the interval class and see the output reached."
]
},
{
"cell_type": "code",
"execution_count": 67,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[-7.0, 5.0]\n"
]
}
],
"source": [
"print(network(Interval(-1, 1), Interval(-1, 1)))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Bonus step: To go further\n",
"\n",
"- Reproduce the first neural network from the slides to confirm the results\n",
"- Implement a class for an AffineForm to compute more precise outputs"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"*****\n",
"\n",
"## Part 2: Small problem verification\n",
"\n",
"We provided a toy problem representative of current challenges in neural network verification. We also trained a deep neural network to answer this problem.\n",
"\n",
"The goal of this section for the participants is to formally verify that the neural network is _safe_, using the bundled tools."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Problem definition\n",
"\n",
"This toy problem is inspired by the Airborne Collision Avoidance System for Unmanned vehicles (ACAS-Xu) specification and threat model. \n",
"\n",
"\n",
"\n",
"Let A be a Guardian, and B a Threat.\n",
"The goal for the Guardian is to send an ALARM when the Threat arrives too close.\n",
"\n",
"The Guardian has access to the following data:\n",
"* The distance from B to A, $d = ||\\vec{d}||$\n",
"* the speed of B, $v =||\\vec{v} ||$\n",
"* the angle $\\theta$ between $\\vec{d}$ and $\\vec{v}$\n",
"\n",
"All values are normalized in $\\left[0,1\\right]$, the angle is not oriented.\n",
"\n",
"We want to define three main ”zones”:\n",
"1. a **”safe”** zone: when B is in this zone, it is not considered a threat for any $||\\vec{d}|| > \\delta_2$, no ALARM is issued.\n",
"2. a **”suspicious”** zone: when B is in this zone, if $||\\vec{v}|| > \\alpha$ and $\\theta < \\beta$\n",
" then a ALARM should be issued. Else, no ALARM is issued.\n",
"3. a **”danger”** zone: when B is in this zone, a ALARM is issued no matter what. When $||\\vec{d}|| < \\delta_1$, B is in the danger zone.\n",
"\n",
" \n",
"### Solving this problem with a neural network\n",
"\n",
"A neural network was pre-trained to solve this task (all files used to this end are available). \n",
"It has 5 fully connected layers, the first layer takes 3 inputs and the last layer has 1 output. There are four hidden layers: first and second hidden layers are of size 10, the third is size 5 and the fourth is size 2. We used ReLUs as activation functions. \n",
"\n",
"The network was trained to output a positive value if there is an alarm, and a negative value if there is no alarm. For a detailed summary of hyperparameters, you may check the defaults in `train.py`. It achieved 99.9% accuracy on the test set, with a total training set of 100000 samples.\n",
"\n",
"The specification used to train the network is based on :\n",
"- $\\alpha = 0.5$\n",
"- $\\beta = 0.25$\n",
"- $\\delta_1 = 0.3$\n",
"- $\\delta_2 = 0.7$\n",
"\n",
"We will aim to prouve that it respects these values.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Create the safety property\n",
"\n",
"The trained network is in the repository, under the filename `network.onnx`. Your goal is to learn how to write a safety property and launch different tools on the network.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Step 1: Visualization \n",
"\n",
"You can first visualize the network answer on the output space by sampling inputs,\n",
"using the function below (**careful, it may take time if you input a big number of samples!**).\n",
"\n",
"`sample2d` is faster but sample only on a 2d slice, `sample3d` gives a full representation of the output space.\n",
"\n",
"Blue color denotes no alert, red color denotes an alert.\n"
]
},
{
"cell_type": "code",
"execution_count": 68,
"metadata": {},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "e8da9a4d8fc34662a3ec0b9c451ce959",
"version_major": 2,
"version_minor": 0
},
"image/png": "iVBORw0KGgoAAAANSUhEUgAAAoAAAAHgCAYAAAA10dzkAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjMuNCwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy8QVMy6AAAACXBIWXMAAA9hAAAPYQGoP6dpAACgZklEQVR4nO29f5BlRZnn/VRf7ALD/kH9ALvrFnTAoG7ouIZjFCHaC6gRxijSbsvCitG27+6AM3aHlDrlMlIzTc2ouMpYMIBj6CzDzBZNvVVUoztKiFNu9zutKLs7C7MGzbirNGPTdrc/B9hBCm+R7x9nTvepU+dkPk/mkz/Ovc8n4kbB7XvvyZPnycxvPvnkk31KKQWCIAiCIAhCz7AmdgEEQRAEQRCEsIgAFARBEARB6DFEAAqCIAiCIPQYIgAFQRAEQRB6DBGAgiAIgiAIPYYIQEEQBEEQhB5DBKAgCIIgCEKPIQJQEARBEAShxxABKAiCIAiC0GOIABQEQRAEQegxRAAKgiAIgiD0GCIABUEQBEEQegwRgIIgCIIgCD2GCEBBEARBEIQeQwSgIAiCIAhCjyECUBAEQRAEoccQASgIgiAIgtBjiAAUBEEQBEHoMUQACoIgCIIg9BgiAAVBEARBEHoMEYCCIAiCIAg9hghAQRAEQRCEHkMEoCAIgiAIQo8hAlAQBEEQBKHHEAEoCIIgCILQY4gAFARBEARB6DFEAAqCIAiCIPQYIgAFQRAEQRB6DBGAgiAIgiAIPYYIQEEQBEEQhB5DBKAgCIIgCEKPIQJQEARBEAShxxABKAiCIAiC0GOIABQEQRAEQegxRAAKgiAIgiD0GCIABUEQBEEQegwRgIIgCIIgCD2GCEBBEARBEIQeQwSgIAiCIAhCjyECUBAEQRAEoccQASgIgiAIgtBjiAAUBEEQBEHoMUQACoIgCIIg9BgiAAVBEARBEHoMEYCCIAiCIAg9hghAQRAEQRCEHkMEoCAIgiAIQo8hAlAQBEEQBKHHEAEoCIIgCILQY4gAFARBEARB6DFEAAqCIAiCIPQYIgAFQRAEQRB6DBGAgiAIgiAIPYYIQEEQBEEQhB5DBKAgCIIgCEKPIQJQEARBEAShxzgtdgGazAsvvAA/+tGPYN26ddDX1xe7OIIgCIIgIFBKwTPPPAObN2+GNWt60xcmAtCBH/3oRzA6Ohq7GIIgCIIgWHDkyBFot9uxixEFEYAOrFu3DgAyA1q/fn3k0giCIAiCgOHpp5+G0dHRk+N4LyIC0IF82Xf9+vUiAAVBEAShYfRy+FZvLnwLgiAIgiD0MCIABUEQBEEQegwRgIIgCIIgCD2GCEBBEARBEIQeQwSgIAiCIAhCjyECUBAEQRAEoccQASgIgiAIgtBjiAAUBEEQBEHoMSQRtNAYlpcBDh4EOHYMYNMmgK1bAVqt2KUSBEEQhObRNR7Av/mbv4F3vOMdsHnzZujr64MvfelLxu8cOHAAXvva10J/fz/82q/9Gtx1113eyynYsW8fwJYtAJdeCnD11dnfLVuy94UwLC8DHDgAcM892d/l5d4sgw+69b4EQUiXrhGA//RP/wT/8l/+S7jjjjtQnz98+DC8/e1vh0svvRQeeeQRGB8fh9/6rd+CBx54wHNJBSr79gFccQXAk0+ufP/o0ez9XhSBoQVDCgI8hTL4ILX7EjHaHORZCU6oLgQA1H333af9zEc/+lH1yle+csV7V111lXrrW9+Kvs5TTz2lAEA99dRTNsUUEHQ6SrXbSgFUv/r6lBodzT5X/M7+/Urt3Zv9Lf5bN7CwsLpO2u3sfV/X6+urrvu+Pn/XTa0MWCj2l9p9hbYtwR55Vm7I+K1UzwrArVu3quuuu27Fe3feeadav3597Xeee+459dRTT518HTlypOcNyDf799eLv+Jr//7s893eKYYWDDYCnJsUyoCFYn+p3VcqYrTbJ3Ac1D2r/NUt/Z1PRAAq1TVLwFSOHz8OZ5999or3zj77bHj66afhl7/8ZeV3brrpJtiwYcPJ1+joaIiiJo3vJYhjx/Cf6/al4uVlgOuuy7r4Mvl74+O8z+DgwdX1Wb7ukSPZ53yRQhkwUO0vpfuKYVtVmJbDZclT/6xyrr22N+tGoNGzAtCG3/u934Onnnrq5OvIkSOxixSVELFLmzbhPnfWWfYDWFMGlRiCgSLAbdHV//IywDe+4b8MrtgIqBB1iyUFMWoS0B/9aFqxkrEwPSsAgJ/9DOATnwhTHqG59KwAfOlLXwonTpxY8d6JEydg/fr1cMYZZ1R+p7+/H9avX7/i1auE8rZt3QrQbgP09VX/e18fQO6ItRnAUgvA1xFDMGAFOPZzZXT1n//bxz/utwwc2Ago33VLIbYYNQlopQA+85nu9e5TwD6DP/mTdCezQhr0rAB8/etfD98ouRb++q//Gl7/+tdHKlFzCLlc1GoB3Hpr9t9lEZj//y23APz4x7jfK3aeIZeMObyMMQQDVoBv3Ur/bV39v+td2cvk6bApgw+Pr42A8lm3VGKLUYxXq4qQy9OpgH0GP/sZj8e2KSskggWxgxC5eOaZZ9TDDz+sHn74YQUA6rOf/ax6+OGH1T/8wz8opZS6/vrr1Y4dO05+/vHHH1cvfvGL1cTEhHrsscfUHXfcoVqtlvra176GvmavBpFSN2ZwUBVcPzp6KtiZWiaOAHxssDrXxpS8zHXB3742DeQB5+XrumwOMNU/9kUtg69NQrZtwkfd2hDLtnL27nW3Bdv+pmmbTjodpQYGcHWyd6/btbp5U12vjt9FukYA7t+/XwHAqtfOnTuVUkrt3LlTXXzxxau+85rXvEatXbtWnXfeeerP//zPSdfsVQPCdtaunU8ZXUdNHcCwA/biYvU1sR0j987KWILBJMCpYOvf9KKUwecuVxcBxV23tuhsC0Cp8XE7gYQRWBz2sHs3vXxNFThTU35FsVLmncbz82y3E4VeHb+LdI0AjEGvGlAMDyAGijjCitjyTLvdVmpiQi8k5ueze5+ZUWp4uP63bb0qsQRD1UBu6z3h8Pi8613464VIueIizlPxQlXZVqtlL5CwAsskoCkvbPlSSXtjQ6ej1OCgP3vGeOhbLaXm5njvKyS9On4XEQHoQK8aUOzlIh1YcbS46D7Q6DpGyudthHIKgsHFe8LlAcQO0qEmLal481zIbWt8vL59YwQSVWDVCWjqCyu4U8rBaINPAUtpn02y7SK9On4XEQHoQC8bUCqxS1VgxJFPAUh9cS+Vh8B18OHy+GAHadewBYrgTkGcu+IqkDAepIGBrB0Wf6NOQOded6y9mMqHFTiTk2k/Q44JR26vMzNKTU9nfycn8W1weFippSVfd+iPXh6/c0QAOtDrBtRkbwfHEiTXK/RSuStc3hNTzBln/WEH/Olp+3jPbsLVY0rxIJXrsk5AVz0H2/JR23/Kz9tlwmFTp1WvoaF066eOXh+/lRIB6IQYUHO9HVxLkC6vJiwzVcG5nKqbRNQtQZZfGA8qxuNYFetmiveMNej5bneuHlOKwKLUZX7fu3fjy1dVV9T2H/t5+8C0ycOmP2tS/cj4LQLQCTGg5sIZdG7bWTatw8zh3gVeJ2a44/aoMWamz8US8FWieWiINyA/pAfQpi6xvz81Ve29nZ+nt3/O5x174syVhimF9mCLjN8iAJ0QA0oLaqfqugTpIh59LpX7HlxCbajwsdkIs8uV+gq5hG/y2kxM8FzHte5tJ1jYusSUb3Cw3nsLoNRll8V53imEFPhcAWlKSIuM30r17EkgQtpQs8/bHOm2fTvAvfcCjIysfL/dBpiYyE5iqDp9pK8v+/fy91ot3L0BAHz2s9n1uQlxtF1+goWOdjt7ZranBzz/PMBttwG86lXZsFKmeAoMpd63bwd44gmA/fsB9u4FmJ52P9kg1BnEuhN4cj7zmcymXcGewFNX97rv61hYwNmLqXx5HVXVVf7eV75y6rcouDzvkKcP6fBpszHP5BaIxFagTUZmEH6gzpA5dqRig86Lnrvy9+bm8B6PwUGa5wrj1TN5h6am+LyBExP6+3vJS+w9HBMTZq8clwc15gkUVLBem+Fh9+dcTAVTzmVJTb5ts9RIyeVX1UaxiZLzfgJAqSuu8Pu8U0o9Q/UATk3pc5rGaA+uyPitZAnYhV43IB9LjVQx57tTtVlWHhrCd6oYMIIYG9MzMuIunGzih7Bi3CQsL7uMd1nbZSksdMwTRay6ngBRFWPochLI4iL++DKKveS/X26jVGHf15fd88iIv/ymKSXQx7bh4j0vLen7NokBbB4iAB3oZQPyEcdiI+ZS6lRzZmZwZRoYwMcpmgZIipAJmSSWMkAsLZk9f60Wb84x21i1GJt4KPVum1vSZ3Jhm004toLC1kanpvzlN411hGYdmF3A5XtOOf8rlV4ev3MkBlAg4yuO5eDB1b9ZRCmAI0eyz+Vg403qPkeNNcRQjg2s4+c/X3kvVWWri/nK3xsfzz5HibtRKvtd23u1jfGpen5FPvc5c5mWl7PPcWGKJcvjPcsxj+12FmvnI46zjq1bAYaGcJ/dtIn++xR7s6Eu5rYOk73oyONUKfGHAAAXXFAfF+z6vLHPxObZ2ZA/j7p43tHR1fesi5sO3R4EBmIr0CbTizMIn0uuNjNkFw8g5ZxSyjJwp4Nf7tLN9in3ZnOyCXYJ2rZc1HvG5nbbvduu3Dqo8Z6xlrnm5sz149trxrG7m5rLzwabo+Xye/PxvFM9QrPqJJBeOO2mF8fvMiIAHehFA/I5SNj8tm2nil3qslnq7nSU+n/+H/d6oghi26PtbJZsXHMoLi5WDx7T07jvT0/Ty4y9r6pypTbY6eIkXZbhQi9RhhCc2E0oocRXNy2hNp1eHL/LiAB0oBcNyOcggRVzS0srB+T5eVqnivVi5r9rEolFOAccygBpu5vVdtCz8a7kudnqBHWMGEDMfdpMAHwLxvl5t925VYSOpw3lESvuaK67Tkjx1eQjNLuJXhy/y4gAdCCWAcX0SPgeJEwz5ImJ6gG56v26TpWSToMi4ChHK2HT02AHSJdlWZdnVa7zwcFTZSuXVVcXeX2YdgFzJTrG3h/HBMBXkl/ufmB21mwra9Yo9cADfH1OaI9YKuIrRh+emic7NiIARQA6EcOAYmeRDzFrr+ukTeeyzs3hOjiO3G9l8URJjdJqZR4cbF1gBkiXZVmXJb2qQaXORnNxaLKbqjyArVZY8WcT66qbAKS+vNfp4NMXcfc5oUVZLwqh2ONGiogAFAHoRGgD8pmiwaYcPmft5U56aYlv8wnnMUi5eKL+JsXrhh0gbZZl87KYBkWbjTDFz2NjFPN6WVrKYv12787+hlz2VQr/PCcncfYJQE/+HRKbs3vLbd1FWPWiKMPiWjepjBs5qTxrEYAiAJ0IaUApZZFXKvysnXPpGePFpGa9p3oVqV43bKdJOXmhGOuo8w5U/ebw8OrEwLoyppYDzQT1eXIn/w6NjVe82OeIh8kPrvXKMW5wCraU7EQEoAhAJ0IaUIoJj0PO5LgFhMmLOTdHW+qm7sLlfk7FZ7G4mL327j11JJYuplLnHaj793IHXhebSU1UncoxUpxe4uKrKvl3qHaku47L/ebJk+tsSESgHRyeO+yReHXtzlaw1YWGpGQnIgBFADoR0oCa5kHhxoeAMHkxsUvdCwvZEVLYAZPbU2vqpOvuMxe5deXs6zPvyjW98npKNQdaHa6pbrA2GsojYrqOzfF++UuX8zK15+pCyAkvh+duYQH/DKvGDVvBVmVrIyP4GOBQiABUIgBd6HUPYEh8CQhTp44ViVRBxAW2k666T19ervIrj31rWg4025hK7GAbyiNCyXnpQ/B2Q78UeunStb+nCvry72C+327j86umaCciAJUIQBdixAA2xYPig1gCQpcgmNLJcsdIunoJOHdDm1557FsqaTiwUGIqKYNcqJhe6nWoMaQ6r07x1eSViRhLl64rPpTJXZWdYb9fjGl18SLHsBMRgEoEoAuxdgE3xYNii84rl5KAwHaSH/uYnyUjVy9BKA8gwMrYt1R2AWLJyzs56V4Pw8OnjtxyeXZYbE/XyZ+PKYbUNcYsdWJtvnNt25TJXVXfafN9jv5EPIBhgdgFaDKp5AFM2YNioiwGTDtSq74TS0DEjst0vT7Gq+waA0jt3LmfLefvYeoL6xHDvlxth8NGdX1Ot69MxAq9ca1XGw+ezfdzW+h03FcUJAYwPBC7AE2mF08C4aLTyTofXQB5sbPDeDhD10vsuEyO62NOXuGKgzOJGZc4K0pCapfJEsYLz7lsHMMDWIXJK9+tKxMxJ3ku9YrZxNRurz5W0za8Zf9+dw8gNpE/FyIARQA6IQZkx8IC3VNimvHGyC8V2/vBdX3MRhcOQYMRolX3YBrsdEfSVf0eQDb5cEmsa/LC54JpZgafU9KH7YSy0W5bmciJPclzqVeTgPzIR1bbZjl7ANZe9+51iwG87LLw/beM3yIAnRADouNjl1jM/FKxvR9c18eeBHLZZdl5sMVrtVpKnX66vZhxibPi2LlqM9Bgvc02XhFfu4B922g3rEyUwXjS8rhOX/dcl+MTc706Abltm94Gp6ay377qKlq/bDrLO2Y7KCPjtwhAJ8SAaPjYJZbCCSmxvR+mGC3OLP51QtulE7f1snDYk++BxiYuyoftxLbRJkNJB+TTa8WVlHl2FmeHmFWaYv/K1R5D9d8yfosAdEIMiIaPXWKxl2hyYns/fMfAYYT24ODqhNgYkWEbZ8W5i7lqoKmqU+pzxpZxejruSSCCHmwYhK/JBNcqR6eDP7YQ2244dwHXvRYXeetTKRm/lRIB6IQYEA2XXWJ1M0HOIO1uGiBNS6P5Eg8WbOe+uEivQ1sR7yOPYX6NurjCslfEJKhjx4k2idTbHzauk/uZcq5ycIu04i5in3lFBwb4RbWM30qtAUEIxKZNdt/r68v+3nILQKt16v3lZYATJ3iuvW8fwLnnAlx6KcDVV2d/zz03ez+/1oEDAPfck/1dXibeRECWlwGuuy7rOuvYs2fl/Zn48pdxn/vxjwEuuQTg3e/O/hafVx1btwK026eec5m+PoDR0exzxeeAffYUjh3L6uSKKwCefHLlv/3sZ9mryNGj2Wfr6rHVArj11uy/y/dXZ9e9yL59AFu2rGx/W7bg7TMErVZm0yMjAD/5Sf3nlAI4cgTg4EGe6x48uNoWba937BhPmXIuuODUf9v27xh+/nN9OxMsia1Am4zMIGhgAqqrXlXLiJQlGdczMycmwu9Qc4Eyy8em18HuZLVdardNr8KZpxAg82BS45iwNiYxeNXE3MRlQ+jUMJzX4/YAlhOI+zo/G9vOKMj4rWQJ2AUxoAzK0o0poHpw0JwPCrvzE5svyyZ5b6qDk1K0pRhMp4odNIaH3TeZ1IkkmzOXc3ui1MPiIs9gWEXqS5wxSGETF5XQccec1+PcOFX1XHydn+2jXmX8ViIAXRADsttoUBdfhYlLo3RgGA+Ly4Cf4uCklN0sX9epYgXl+Lh72es2XpieedkTWLULemrK7GV0iWNq8nm3sUhlExeFEHGd5dQvnNdzTZ1kmvza5g1dty5sO5PxW4kAdKHbDIjqoXBZurH1hlB2VWJ+k+N815QGJ6XslmJ0nWrsQRp7/R07sue5uEhLGF6cKLgskcW2gyZ6GGMfp4ilXLfz8265FU0nq9QlNufK5YgRaXVedMzE2kbAPvBA2HbWbeO3DSIAHegmA6J68mIt3XAPGBwCMPbgVAV1lq/rVGPvZKV65TA7c+sGXxvxnIInOMZJOBxMTaUvruvqtio2GCOOdM/KlGvTRozVUfaOU3KJ2joLdAI2dD/TTeO3LSIAHegWA7Lx5MXquLm9US5LwCkMTjqws3zscXGxTjyhPiPXMlHimFKIBW3aJooczCQltrjWlbGvj35+relZ6WJW+/qy9kw5CYQCVtTZTjYwG6FC9jPdMn67IALQgW4wIBtPHvWMSB/l5Zol2m4CyV+uGx980+nUi3VqpxpjJ6ttPJGrcMDmAYy9kzflTRQYTyvmWcaqX0wZBwdpfY3vM7V94zrZwIjMUP1MN4zfrogAdKAbDIjqUaN2Yj46K+5ZIkXQll8cGx84qetguTrVkHFmHOf8utgfx9KXb2LHZ9Zh8hJhy11MNBwa7jJypWAJHXJSTICtO0WEc7IRop11w/jtymnhMw8KIVlezhKEHjuWJercunVl0llsYtD8c6akpEXy5L3cbN8OcO+9WbLjYlna7Syp7vbt9N9bWFj9exi2baN93if79lXXya23Zve4bZveFjDkyXB9g0lmjcEl8W3dvXLev6l9mqC23xDkibTLzy5Pmn3vvQBLS7jfKiYaDg22zm69FeCGG8zPjesZUBMuu9hYVZ9Sh1KnElK7tpFQ/UzPE1uBNpnUZxCYWA2qB4ESkM/hsjctI3HOEn2mXvBNU+PA6uDylvjyfHHYXlX7HB7OdphiSc0DiF2SxsZ1xlzupNggppyuNm3T57hsDrL1wKe4Ka6K1MfvEIgAdCBlA8IKAmpMXcilm9g7G2NufKCQchyYLRznivq6Zw67NA2uExO434m9Q7sM5czolMpdRaeTnUHLJXowz6ou3Uv+okwOXNN02cYrproprkzK43coRAA6kKoBUQUBRehg0mS02+4ddyoerSYc4ZWaF4gDDg/g3Fz979t68DjsEju46spfVaYUJiqUNE0plbsO7mwHtkceFvtWDhszCWyb9peCaKeQ6vgdEhGADqRqQDaCgCJ0uLwXdaTm0Uot8L9MU5LpUuA4V7RuUK6y9aGhbENP3fPtdDKvlc4jhLVLH0frpTJRofY9qZS7DlOWAK5l2fI9z83VX6+8glPVN2Gfw+Rktc1TPfApiXYsqY7fIREB6ECqBmQrCChCZ2JC3xm4dARN8WilIgybUl9UXHcBVwlezG+WvSzUVDSmeqYMrouLeBvD2qNPu7VZkk6lHdVRlyXARfS4pMjJ63B+vj4UwTV5OtUDmJJox5Lq+B0SEYAOpGpAvgWBbw8dtvOanIw3aMSOTyySWhwYJ7Z5AKvsG7v0Wl6Oo4pQk6eVMriWPY6uNhbCbpuwtEslpKfSJfwhr+OrrrL7HjY2HECp9euV+tjH9Ecvpkyq43dIRAA6kKoB+RYEvgWmTQdYHsR8ehVSiU+sKhM2jjNlj0uZYh6y6Wml/vIvs+VRqn1T7Co/dcFGfJrsvtPJyu8ywNvYWEi7TX1p14ZQ7YZjA5StbWFiw019b1NIdfwOiQhAB1I2IJ+zcN8xZ7bxX7ogaq5OKrX4xCLYo5ZS8Vy6YGPfvgdWyrOfnw9znZwYdtu0iYZPKHXBlQLJ9mWKDa+ynSZ6dlMev0MhAtCBFAxI17H4moWHiDnDzj7Lr3Xr3DspXZ2mHm9nsofUPJcuzM+v9qTp7NvnwGpTh7o4Wm4bS91uTTRVTOZHMVKW8jk2QLm8qmLDuTZApUQK43dsIHYBmkxsA8J4c3x0nKFizlziv2zLZarTpu64TdlzaUPdTl5T6hdfA6vtxGpubvXxWpy553KaardKNddrvbBQv4PYNGHQebh9iL7iq2oS0PQJRBWxx+8UgNgFaDIxDSi2NydUoHdRwE5O+uvgivekq9OmdoRNLXcVLraPXXotxgDqBt3BQfcg+PIkzfWUjKpJX1Off+x+zhbM5iHTpKtuBWduzs9ERleeJk8g6hABKALQiVgGFNubkw8o4+OrvRc+A719HqaOrdOlpXA7bjm9t93SgbvYPtajXLULOOSOVhcPe523LE8Z0qSd4rH7OUz5qton9RQNneiuuwa3h9Bkz02dQOgQASgC0IlYBhSzMVYNMMPD+iS6XFCOZqLWC6VOfYiCckevy/FlQ7d04Lb3QUnngtk443tHq42NmbxlExPNSs8Sw2axky7dsjR1omo76aqzy/w5U8pgsuduTDUlAlAEoBOxDCiWNyeF5Rjs0UzUTopap5yiwMYzRaVbOnAb28d4ZIaHszQzupNAQm9CoNgY1luWLx9y2K1vOPs50/OjbNYw9YPj47R+yUXA6jyE2Mny5CTOnrstv6MIQBGATvSSB9DHcozNoGo6mqlYHkonZVOnmPKbPkNNNOwi1LqhA7d5Tk32fmLbCOUem7Kjluu5mTaRUDZrYPpBSo5Hn32maywpti5TnUCYEAEoAtCJ2DGAIb053IModWdfseOr8wIWl7qonZSPOjXdIzVWiEOsNL0Dt3lOtl7DVEQSpixc3rKY912+Nke8LWZZ3FRnxetg+0FdovLiy9QnFeujynvrmk5mYIC+iQnjTU2l7egQAdhlAvD2229X5557rurv71djY2PqoYce0n5+enpavexlL1Onn366arfbanx8XP3yl79EXy+FXcChvDmcyzHUpeQq0bJmzervDw6uFFd5J7S4mL0wcT1cdcq5o9i2nutoSgddB/U5UScvKaUdwZaFY4KGmbD4spu6a9vELeblnJlZvUmt/ButFr7N5feO+ez4eHW5q/oqbH3U3YOub8LmU+Wy75TajgkRgKp7BODs7Kxau3atuvPOO9Wjjz6qrrnmGrVx40Z14sSJys/ffffdqr+/X919993q8OHD6oEHHlCbNm1SH/rQh9DXjG1A1Bghl86bywNIXUqmLJFixaOuQ+LwkGHvcWYGP/hQ69lUvqYIQF2MU9VmpPn56t/AepJSiHPNoZTF1YON8ZT5Gthtrl3XJrlzhxZfuQ1i22dVWQYGshUMG68lts+0qRMO+6baa+w+KPb4nQIQuwBcjI2NqV27dp38/+XlZbV582Z10003VX5+165d6k1vetOK9z784Q+rN7zhDehrpmBAmIbEMSvjWiKlxipROnOqeKzriG28hzb3OD1NH4Rcl/dDz9BdOnpTWauSKNclQq8LzC8OTimlHbEpi60H2zYUgUM0UNIvYfo56u5Xymt6GudVLE4mRkZW/vvICC4UxaZ8pnQyPk/zoNhrKl7CFMbv2EDsAnCwtLSkWq2Wuu+++1a8/973vlddfvnlld+5++671YYNG04uE//gBz9Qr3jFK9QnPvEJ9HWbYECmTlF3ckLdb7kskVKWkm2XSCniUdchV3VUIyOZcOSIx5qZoSV0dR1wQ3u3XDp6bEoT3b1UXb+85Ff0JKW0WcQl3Q3Vg+0SiuAqikOtLLi+MEvFZduzmXz6DAvxad/Y356aSsfD3oTx2zcQuwAcHD16VAGAevDBB1e8PzExocbGxmq/d+utt6oXvehF6rTTTlMAoH77t39be53nnntOPfXUUydfR44cSdqAMJ1iq1W9bFaHaYAxeXywHcXiov3JH1TxWLd0jBFmrvFY2Bidcj1TCe3dchGbWLvV3cvgYP31AZT6zd/MPDpLS6eum1KybGpZXLzW2GuZbDnEfdbhIpy4Xnn7xIrRqr7D5VlUPYOiXWD7Uxv7xpY7pfOERQCq3hWA+/fvV2effbb64he/qP7X//pfat++fWp0dFT94R/+Ye119uzZowBg1StVA6J0itTlYGxcVtWSnGkpeXBw9dIJtSOkdKTljofiTbCJx8o7wnz3XZ2onpuzWz6tej4hvVuuYjPkYF60z6Z6AF2X1Djq21YUc9U5h4itelVtNivacVX+SJfJp82zqGtPtvGQPj2AqbQvpUQAKqW6QwDaLAG/8Y1vVL/7u7+74r3//J//szrjjDPU8vJy5Xea5gGkdIquMy+dxwdg5bLp3Fz9UrJLx1HsCG06pLzjoX6XEo9VfuUDNVdQdJ0YwCan5fBuuQ7qvgbzumdXjgF0jXPlAFuWvC3p7sv1Wi7Pkus+uWKL617luL6BAaXe9z67e+eYfLqGhdjEQ1aVBdsnYZ4jNjF1qOMoRQCq7hCASmWbQHbv3n3y/5eXl9XIyEjtJpDXvva16qMf/eiK9/bu3avOOOMM1UH28KkbELVTdO3EsdfJ0ztUCRVMkmdMR2gzqOUdj60AwcRjYTtwG0winMMGQuSkC72cV7UL2CXOlQtTWaqOC6y7L9trUerO132GELG5F69o17Z27DL5pD6LqrAQm3jIcl3beJUXFvS/jT3FSTyA4YDYBeBidnZW9ff3q7vuuksdOnRIXXvttWrjxo3q+PHjSimlduzYoa6//vqTn9+zZ49at26duueee9Tjjz+uvv71r6vzzz9fXXnllehrpm5A1I7A9zJO1QCWx/pNTir1x3+M/w1dMH8OdRZs6wGsq798593HPqbUunX6+nAdRLFxc1hPS5XQC5WTDjOY6+7F9qXLAxgrWbauLNxL1nXXCnGGMEed24rYujqyrV8bAVbuO+rqY37ePAGz6b+KdW0bv7uwUD2Bz3MepuRhVyr98TsEELsAnNx2223qnHPOUWvXrlVjY2PqO9/5zsl/u/jii9XOnTtP/v+vfvUrdeONN6rzzz9fnX766Wp0dFR94AMfUL/4xS/Q12uCAdXNylwGijI2HjOXWL/JSVxaiPz+MV442xjAuvqzib9xmflS4450HXtV2bFHZRXrz6WjN3mF6kRJ/jrjDPrza9pJID42rVDie7lFMUedY3Z+Y23RxY4xJ4yY2r5tfWDtYnJy9W/bxu/qJtvlviUVD3sTxm/fQOwCNJmmGNDcnH0niCH0kh1VKHU65uPjqryHlDLZJq+2HajLUE4o0A3kHLFDxd9x6ehNosM2yJ3LrmLj4gG0ERcuAi2koC5fa37e3hZt7JjShnx4vVzswua7VNGYioe9KeO3TyB2AZpMCgaE7Vjn52kCiFoG1yDyEJ0ltePBxqwArI49DC1AKB13nc245lLDxEDanKqis2+duA9lV7Gw9VCFTsTLdT0XEelii5TvumYQ4MDFc2njVbYVjbE97CmM37GB2AVoMrENiNqx1n3elNgYWxbb+JuQnaXNzjZduVotpfbsOfV7i4txBAjHsqurJ7fKg+m7o3cVrfkrRnwfB1QPlUt+RpfyuV6PQ0SG8GBS2pBPr5etB95GzKWUP5NC7PE7BUQAOhDTgGw71mJHNjW1OgbPxRNQFwTM8YoZhK8TtuX7xaY6KL8oJ7JQy4odbF3Tr8RYQuUIP5iaCl9uTrAeKtf8jFS4rudLtPqYnFDa0Oys+/V02Hg9bSaSKeXPpCACUIkAdCGWAXF0rD461U7HLYFz+TU9nUYQPmVThO2LawnOZanLVkzFXELlyBmYimfCt4cq9EDNcT2Mh3d4eOWJLhh8LYNT2hD1FCYbbGyKOpFMbXcvFhGASgSgC7EMiCvNBveAji3X8HD9UV2pdhjFjnRxkVfoFjtXTJoHSlkpv2ETyxlj914RDg9gCp6JEHF5oZfqOK6Hfb5DQ7TlZF/L4DYhCSmGH1Ankint7sUiAlAEoBOxDChUol3qwIgt18xMMzuMHJ+7nsu7tX0G51ehey4Aqz2fsZbmc1w2IFEnGr7iGUPF5TXRA0g9VcNUVyGWwV0yCKQE1t7zz42PZ5P7lPoHHSIARQA60VQPoC9PALVc3OkAQu0s4zj4nDKohRbEuueSwu69MjYbkGJsQqgiZFxe6KW60BuTOH/PVQRTd6an4IW2oapdDA1lYjCV/qEOEYAiAJ2IHQNo27H66gQ7HXNs3ODgynJxCQqfA3S5fNj6y0854RCBtgOzy3JwakJPh26Hu6tnwqeHLrRXLrTn3fV6Nh5eDo+i6zI4NR46lThUCqF3lHMjAlAEoBMxDUiXad7U+Hx5AmwEIAe+OqI6UZGfwYqpP87lYqoICJ3vLTY60eoaF+lDnCsVJ4WG70S8VYmYXa5HTU7OEVPIIbgpS8E+PYA+JnOhd5T7QASgCEAnYhmQqUOcmMD/BqcnIEY6AF8dkUlUYs9H5UySTREBTZ+d+4I6GPq26VBtpnzf2KMUqdRNOubm3K63sLDai2tTV6GXwU2nMAFk9zUz48fTrpsEugjDpqZ+KSICUASgEyENKG+sMzNZjIWu0WE7MO7E0DG8GT46IqyonJvDeTaoQeGu92Ajipu25GuDjUfUxaYxdRpCkITyBPuedCwtmfs+TEqY0MvgdacwVb24nkunoz/+EmD1ag3l2rbtIqV+RgSgCEAnQhlQVQfOKRaKiaFdBooYs0IfopNyH5gOzVUAUkUAx2acblsqthUntjZNqVOfgiSUJzjUkiBmww/Gdquez/Cwv7x82D6c65nbnI5DubZNu0itnxEBqEQAuhDCgKjxLzaCR3cdSqdgCnz2kXbDh+jkFJUcR5VRBwRK+Zt0yoItLuLExkNnU6c+4vJCxmmFjq3TxRpjbXdubrVH0acgKa7i6JazXZ6L7XhhunZVCAGlXaQYkiICUIkAdMG3AbmIBx9LnqYOSdcx+0q74WMJzXYwc9kxXPeiJLilln9x0V/8ZEozfVdxYvI6Fb1GrmKTUzSHFGUhwz8wHnWT7cYUJD6zMHCci12+dl17psZBc/czrogAVCIAXfBtQDbiIaTgKWKaeQ4O8qTdAFgdo8i9hIbpSKu8PlWd5Pi4W0f8wAO0shfLbxLFi4v8A1GKM30OcaJbViuK25SC4ymJ2TGxirrPhNzMQhE5VdeLLUhi52GlXBuzGc7kuU6pTRQRAahEALrg24Co55zaDrKuHRKmU263cR0qtYPPB1/uJTRdmh2AlTutTYKVoyOmghHFlOdO2dCgs0/M8hJl4A0ZJjA3Z253MTZC1YG97/JyZNlbi/HohtpdSxU5VfUcW5BwrjAU4TgXu3htbHs27ShPqU0UEQGoRAC6kJoH0FbwuHaInB0q9Z6Lgy/XEhrFA4jpJE1pIHwNQiZRjK1r7Oag0IHhIcMEsIOhD6+qLbYpiIptiuLRDbG7lipyquo5tiCxjSs12TqXBzDfSc3Vr8cW3HWIAFQiAF0IFQOo6yg4cki5DpCcHarNLJZ7yYbSYVE6XcpAXL4nl0TGdd/DPPfBQbwAoNqBy3Ix9buu4oQaV+nbE4YFs2u2rpztNn1Tl+8k05T2VlfPKQgSij1ibR0r+PMjKnWfo4SvmPr10LkXsYgAVCIAXQi5C9jnrNr1OtgOdXraLGBcZrFcHTZFyGA/Oz6+emDMN8yY6tznpgrdcy+WEdNxU9PnuO7MpX63atcnVpzY7Kz23WaxVNnP+vX27czU7nzuAO90zKcN5XVdV8+pCBKMWKbauknwT02dips2/a7t86+7V+yGkVDZA0QAKhGALsTMA8g5q3a9DmbmWV4GrRMwtstW+eDLgQ8PYF3OQFOd+95UkSeMzb0CxTJgD7TPBwDKwOriheFaaqbkfePIreijzWIp5/uktq0Q7Q4DZgcwZsNZKiKdc3NN/lvYs6+XlszpaHThK1ShjOnrQmYPEAGoRAC6EOMkEN8zI9vrUJeadB2t7bIVlweQImS44suq6tz3bsWqDndg4JSXwGZpHzuwuoQNUJemuHJcUp9zSrkQczhThXC3O46yr19vPgkkJzWRXoXLCsPQUPa+6+ao3L5t206RujYRI3uACEAlAtCFphqQr4GpqkO1nUGalig4hVDdvVBjdGw7ybrn4TNWCdPh2l4fM7C67IQ0HQdW/C6niE7Fa+QCZdDPYwBjL5VSy05pD776Qq7fdQmJMdmli7jkFMqx0vI0dfzmBGIXoMk00YB8u9mLHd/0NL3DLn5/cTF7YTw+PgZfiofAtl513/O1W5GS3sHWu6nzau7ff+o0BOpvU1KbuC41Y59Xal4jperrn7LJqrgL2FX0cgii0Lt3XVZDuPpYjOfZdpLtGr7CRaxNOU0cv7mB2AVoMk0zoNBudptdoeWOc2TEHPQ9OBh/SXxhYfWOyZERt52s1Bg8LJQOl9PrhfXq6n6b4rWgfJ4iGlJc2i2iEyCU1D+636OIXi5BFFIoUMpcjq/k7mNNG7Vs6ySVzTCx0vI0bfz2AcQuQJNpkgHFcLPbCA1sh+aj07fFRlhjnke77SZ+Xb1AeYc7MbHay9BqrUyGbVtHVS+duKB6LWy80E3GZIvz8+ZNVlVJ211jgzkEEadg0d0PpcyhQlXqRLhrqpYYsXdlxAMYD4hdgCbTJAOK0ciwHXa+1IgpH7WD8w0mML0qVyP2eaxbp//3OgHI4QUyCXPqBgpqHel+SydgRkdPCR2fg3IqlJfVTfc6N6evP4qwN5WLe9LJ4ZHWtQ1KmW0nrbZ9bJVodU08vrBQPcmkHN3pSixPZJPGb19A7AI0mSYZUCw3O6bDdgl0du1Ubck748lJWjmp8X02926a1c/N8QhzbMfsIw5PZ1P5IfWm6zVp80YdFA9UsZ51Rx1y1YmvSafLkjRX2EWe8NumvXL1sZhnb9pop2snIdtFjA1WTRq/fQGxC9BkmmRAsdzsSpk7bBcxxDE7pC5v2Qy6tgMNdUDBejDm5/mEuclmfEw+6mwqF7eY66W4eYOCrQdqZiZMOIjPSafNkjTGE13Oh1n3ok78KO0FA+bZu4aghPaMh95g1aTx2xcQuwBNpkkGFDvgV9dh23oAOWaH2GDvYpJV246/WG5Mig3dcl7dgEJd3uUQ5pOTervxNfkoLn1OT5/6i7nW9HTzl31tJyGh4iJdUv342GTDsdJQtHmbds/Rx2KfvW6jTUyHgI6QG6yaNH77AmIXoMnENiAbz1VoNzsGjDgdHOSfHWIDoF08frpXvmOw7nmYAvarBhSq14VLmOsGG5+TD9tnEytmlAsbMZPX88xMmDqyee4+01Rh28ZLXmIuMzb2rq5PcQH77BcX3euibAOp74CnEHv8TgGIXYAmE9OAOPPODQ9nS2cxwYhTzs4HuwRiCph3eeXnxmKOgsOKds6ZPWbDBXaA8zH5cNk53vRdv7ZhE5xL+xgoz51rR6prYvX163F9EXa5uNymXeFYWrexAd85ZEMjAlCJAHQhlgFhgvx1Qml+fvXyYgoNOWQMCLYDxJ464SJCTMKWUi/c3ra6ARz72+UcaVzP12UJ1GfeyFDYeADz+w4dDoKxX66YNNMOX2x7xtgqNo6XO9yAQ8BTbSCFdDHciABUIgBdiGFAmIGvnLOtKO5Sb8ihlhg4d+GWXx/7mN0pF1z1wu1toy6z5gNP1fdGRrKBM+YRWd0gACne2bpnEzIcxGS/HKIGk7KIkjfPVOZOR5+n01dcNZeAx9pAihtGOBABqEQAuhDDgGxjf4oxZd3WkG3gDAivqr+FBf2z4Bpg6wYpbm9qp4MPfM+XtusmGgDuItBVwDd9CVgpmne2+GyK30/lWDvXZU3MxJgSu0dJSRSinVddl0PAY2zAd8hArLhCEYBKBKALMQzIduCz3VVaR9ODgTGzaGx9VXW8IRKsmmJyuJ8RJfic4jH0eSwYVUjEwOU52XpnOa7NiavIoNomp3eeQ0jbPAcuAW+6ts90PjHjCkUAKhGALjTFA8g9OHZLMLBpFo05Nquq48UsRXGVver3fXkesEtPIXZI2i6BmoREaDjaUn4ihG5TQurefddlTezO5pkZe++ZTihxi3isDYQQ8D4TescMRxIBKALQiZgxgL52plY15HIgP9cgbnPv3J2d7S7c/PWud2WDb16WEPEyPq+B2ZBiGjxtvNS2nhfqEmhKQoh7AEw1zRMWl/JT8j/m16J4z3xNemOLIAw+Ng2lEFcoAlAEoBOxdwHbiMChIVpDpiwx+Wy0Pr2ONrtw68oRIsUG9RpY4YytY9Pg6eKltvEilMuSL72nLIR8DYBUYZPKEnCO7bImxQOYQ2kXVJGG+e0URBAW7slFComoRQCKAHQitTyA5d2/VZ1JntcO05Bt86xxN9oUZsmdDs77GeLMZco1KKKOUsem5bCQ56RWlSWlDQ5V+BwAuQV/aGxEqa/6tBFp2HpNQQRR4GxTsc6mLyICUASgE7ENqNxRYs53VYonL1eoRpvKLBlbDmz82/S0vdcFO3DkJ42YRJ2POp6YsLMdzsEuNe9WEc4TW2xIYVJFAZOSBbML2FdbK6fXwdRrCiKICpcdpiB+Y4/fKSAC0IEUDQg7S+PKy+W70abQUVDKYdplCKDP04gBE5OTnzWMEXXcdWzrOW61lFpasng4DYRS59yeulQmVVjq7r+c8J6yuoGFItKo9ZpK3xYDH3GFVFIcv0MDsQvQZFI1II5ZWqhAfq5y+J4lU5ddKTGaNgOUKSYHe0rB/v205LgmXDzH3TrYVYEdAOfm+Gwmp0nCgzKZaLczzzPn0j+lrmxic2OLoJjE3rSU6vgdkjUgdB2tFsAllwC8+93Z31aL/hubNtE+39eX/b3lFrvruZaDWl6f5di+HeDeewFGRlb+W129KJX9HR8HWF7GXafuGu129v4FF+B+5+hRgLvvxn0WUwcHDwI8+STu96o4dsz+u02i1QK49dbsv/O2k5P//2c/C/A7v1P9fRubycHW8dGjtN+1ZXkZ4MABgHvuyf7m97O8DHDddafu1cTRowA33wwwPQ2wfz/A3r3Z38OHs/Ziw9atWZsqP6Ocvj6A0dHsc9h6zT+HsQFKf1pXjzZw/lYdpj7M9pkJBGIr0CbTzTMIaroZXwH2qcySbcpR9MTefLMfr0udtxfrjcCmzxgextWxnNBBQxeyQfHiUsDaxvCwfy+MbnnbJgzFR3+A9VTZelY5NldwhgmE3hwkJ4HEQwSgA91uQJhlxhCNNvZSgWs5Fhb0SXqLL66lbKxgxabPGB/HXdc2djS15a6Qg1LVtTodfzaDndz5bl+mDRPY0AQOUYwpK3bjnCk2d3FxtV25JpLm2tDTtM1BLnT7+I1BBKADvWBAqaTTaGo5qBsiFhf5hAdGsHLHg9kkKk9tcEkhPQpFSFOejSmhu60wpwoYzIYJylGMrqIYA+YedW0OYPXxkK52xbmhp2mbg1zphfHbhAhAB3rFgFJJp1FXDs7yYRO4Yq5H2RDR15cNDtzCwyRYfSyxUwfBlPLzpeIBwS6lDwzgnk1dwux169xFpo1gpixD2+won5qi1rgZl/yKVeeCc9gV5wSuSZuDOOiV8VuHCEAHYhtQKsLMhM9yphz74pJKh1N4YE464V5i1wlPDnvwYVMpeUAouR5N6EQt1g7rPGq2ghkrcMfHaTvqi9fnFOtV9jwyUh8GU7TPxUV8SiYqnFkSuH6rKeNS7PE7BUQAOuDLgLBLDbGXqXJ05bUpp88jmurw4fmheHHqPAShhIePJXZfA4Ev20/JA4JZSh8cdF9qxb6q7tlFMLvmQcQIQK42gw3jqLNBn3aVmgcwpXHJhAhAJQLQBR8GhGlAqSxTmcprU05sB9KE2Bdsh+prhzCVJszcfdp+Kjknc3T5JLH36uqF5hJxZaihB2XbvPHGMG2GGsZR9Vx82hVnCIfrb9m0zZh9jghAJQLQBW4DMs005+fTWqYyLS1RvVqUDiS1mW8V3DtxUzoSKga+bT8lD2BO3YQIuwOfkpaHGgLgKmxcQg9CiXWqgK6yQd92halH6qoK9ZnYtM3Y3kIRgEoEoAucBoSZabZaSu3ZE3eQyjuSmRm3XXrlclI7kBRjX6qIsRM3BXzM7H3XUyo5J6vKVdy9W44n0w2alFhCaggAR55CW4Ebqs3YpqIpXjeEXelCOKhCyyYchPo8UljFEgGoRAC6wGlAHBsGXMWKCZtYHGw5qR1IEzyAunor78TVeUsBcPFeqeBrZh/C65NKzkld2SiDJkV8UET7woL5OdikkKkSoroQEN+iiqv/DWFXVc/PVmhRJ3A+z0z2hQhAJQLQBU4Dcj1BgUus1EHNZ0ctJ3VwTyn2BYOuQ01FAHJ47bhm9lVlCeX1SSXnZBGXQZNbfGDj4nxvxPIpqlw3z1TZYGi7Cim0KG0zlRUPEYBKBKALKXoAbWbdpsGeayehrpw2nQLnABDT85NCh8jhteMacOrKMj8fbomWKoZ9B7O72gin+OBMUZNjazu+RJVLf6yzwZCbHkL2K5Tnl8pmKxGASgSgC6FjAKsalY1YoQ723MvTVeW09cJxDgCxPD+xO0Qurx1XGgldWSYm7IV609LSFOGwEa7792GvrjuKOZ9rp6PU5KR9/zYx4a9sFEL3KxMT+j4/bw8pTHiVEgGolOouAXj77berc889V/X396uxsTH10EMPaT//i1/8Qn3gAx9QL33pS9XatWvVBRdcoL761a+ir+djFzC2k7EJ2s6vQR3suZen68rpsgONq5ON0WHH7BA5l4lcBxxsWebm6LbvS6SFCmZPZdD0VZbYk6AcjjjnvL3E3uUa0mZMIUJlUZzCZisRgKp7BODs7Kxau3atuvPOO9Wjjz6qrrnmGrVx40Z14sSJys8vLS2p173udeptb3ub+uY3v6kOHz6sDhw4oB555BH0NX0Y0Px8ttsXMyDbLFPZDPacHsDJSXNweWrxV77BeH99dYgpbaahfL9s+0tL9W3BV34yzHNrt7OTIFwnFKkMmhxliRnfWXd9pXjjnKem9PUToj8LZTO2KWB09Se7gMMAsQvAxdjYmNq1a9fJ/19eXlabN29WN910U+Xn//RP/1Sdd9556vnnn7e+pi8Dmpurb0gunYdtJ2vqSACU2rCBrwOPuWwSC93yCcDKGTQnnJ4X1x2ntmXReVp85iezmRi5eIBS2qFsW5a6us29ur7Fiun61OdZ9xoY0P97qF39IWzGNn5b91kRgGGA2AXgYGlpSbVaLXXfffeteP+9732vuvzyyyu/85u/+ZvqPe95j7rmmmvUWWedpV75yleqT3ziE6pDaJU+DciHJ8xlsDd1JKE68BRxFazd4gFUCjfg6HK/2QwkOu8e9Tcp3kJsAm/Ogde3h5yaCoZSFp/xnRh016c+R45XcZOMz0mvjc1QymObwUHXRmQJOAwQuwAcHD16VAGAevDBB1e8PzExocbGxiq/8/KXv1z19/erf/fv/p36H//jf6jZ2Vk1MDCgbrzxxtrrPPfcc+qpp546+Tpy5IhXA+LuFHzvJEzJQxEKjjifmPFd8/Pm61I7Y52dmETA4CB+EoEZSEyemOLgRB2YpqftBn7XAS6lzSzYsmDrNt/pTRErGLgyGXzsY+aJrimlU/4aGMjKNT+/Oqk+d6wgxWbm5pQaGsKXh9p/pRLPKgJQ9a4AvOCCC9To6OgKj98f//Efq5e+9KW119mzZ48CgFWvphgQR0yIqSPppRg+1w0AeV3u3o0XKZxgB8W5ObvfLtsJRgTkgydmEsEZm0rJTzY9nd2LjQcw5ABHwfdmFpf4zpB56jDlM010sV5nAKWuukrfHkL3m9idvEqdek75qVDYcSWVDT8iAFV3CECbJeB/9a/+lXrzm9+84r37779fAYBaWlqq/E5oD6AO204yVkb6bsN1GcNmtyG3YAg9E6fkj8NMIrADycAAbnCi7HYfGsIfyxhrgMMSYkku9qDvmsmgXAdV7XdgILPdZ5/lW1YOGTYzO4svD7b/cpm4iQfQPxC7AFyMjY2p3bt3n/z/5eVlNTIyUrsJ5Pd+7/fUueeeq5aXl0++d8stt6hNmzahrxnLgFyXHZvipUtZSLp0YtTdhr5iYkIPytjrjY/jnj1FUGImPTZeope8xH5wn5xMw65DDMixB33Ks8VOjjudzLbKYQbl5VPXVwhP8fy8UmvW0NoT5rNV40oqO9pFAKruEYCzs7Oqv79f3XXXXerQoUPq2muvVRs3blTHjx9XSim1Y8cOdf3115/8/A9/+EO1bt06tXv3bvW9731PfeUrX1FnnXWW+vjHP46+ZgwD4lqqSVlcKRU/h5YJW/FEjUXyGT9JEVAhrzc8jLNHykCCmfRgdrv7eMW26xATgdiDPvb6lBhEzrQxvuodAyX/LIA5rnZ4OFsW1o0rKcSLiwBU3SMAlVLqtttuU+ecc45au3atGhsbU9/5zndO/tvFF1+sdu7cueLzDz74oLrwwgtVf3+/Ou+885LaBVxFKrunfBMquS6GOqFs69GgeplCnBWKGcS4QgPKwe51r8VF3ASFMpBgJj11v6d7vfjFbgN87E1Sobxz3IM+dRKLvT5XDkiul08PoK/70JU5r9/x8dX9QciVKBGAqrsEYGhCG1DsZZQQpCRyMfnlqB4NrLdl924+z6xuQMN4MTjrfHwcd/9lL4POS8Yd0mATn+m67Bdz8hbSO8f1rGxXCLiuz7kBSffCesNtod7H+vW4z9V5Lavqf2go6xdCr0SJAFQiAF0IbUBY8ZC731Nd3tWRisjFeCFtPBqh7w8zUNrk37PFduA0eYm4Qxo6HVqal/Fxuucwhl3XEXJJzvVZce2+N3n4dJ/hPh6z7jU/T6sbKtT7wG58osQ+x/KAiwBUIgBd8GlAVR0QJYZKN+CnTAqH3lO8kFSPQmhvC6bDDbkZxGXJKbSXrNPBe/by9CDle8MueXPWsS1N2BwWYoUAM2my7YtHR/ETrquucq4uI5QJ2cREduQixqbLwjWllZ0cEYBKBKALvgyorgPKA5SpXobYMUYUfCSrrhLAOpFILYOvWCQXKB1uDK+ki7cspJes7ljG8qBeTE5dtAVqrsDY4Rupbw7zbavYSRN2Ild1RjUm9jZPEu0bTFnWrMlSxFBCI8piLpWVnSIiAJUIQBd8GJDtcUmmV18f38H0PnHxkGE7b5NIxHrEJift69C3t4WaeDf0Ds2q+8eeoBDaS2ZKjjs/7z6ZyAf9xcV022UKwpCSSogK1UvlMpEzTYJCxsSZyjI/b7fjuSjmYueBrEIEoBIB6AK3AWGWx4aHlfrgB1cvTVGXmsqiJyVsOlZs5z03ZxaJlEHbpQ59DqrUDjdGWoby/S8u0geWqt/xMWhWHdc1OpqJQ91kwia1TGrtMqWUTJS26WtjR9H+XCZyVd9tteLUs+4+bMM2imJOPIBpArEL0GS4DYgaID88fGqmGONgeldMu1MpHSu27nQxXcVlG+ygHbsO6wg9mHHQ6Sg1MmJ+PiY7sRk0bTYGYCYTeRkpXvuUbIojcJ9ToGPFiI3X2naHvsv9FVOixLYF15RXur4ldh7IKkQAigB0gtuAqDuybL1WsRueUriBm9Kxcu7KywP6sYN2zBQedVA63GI9Ly7GCxNYWDAvA09NrV6Ccx00bUSkzXJh+fM620rBpjgC9314DymJiykeJWofyuWdS3GDRBGbcamqvCkkfy4iAlCJAHQhtgew2NiefdZuGdimo3TFRzoAzrxcxWVRytJH7AD+MpgON5XlPUqMUbuded84Bk1bW7TxsBaFNjbFjKtNuXinODZk+Ur7gc0nSYkpoy7XcwmXGMujFLug9K2mOom9ylBEBKASAeiCrxhAm92RroloQwXf+prtYjxeWIFcHrQnJ9OqQwq6DtdmgPYRb0eNMaK0D92g6WKLrkHtIYLiXcW9Sxld6hZjY75Ek81yvat3LvQGCapdUMYljJhLZUORCEAlAtAFn7uAbVNk2L5Cea98znZNHi9TGp26zhy7OWFxMft8Kh1cTlV5bAZoX95CTu8tZdB0sUVXO3b5Psa+OLxvMeqHksbJV0wZ1fPv2n9y9InYPsfWLkwe+ssuS6OvoyACUIkAdCFkHkDb19BQFlifSvCt79muaYnBJg6FIgBTWVI1QR10fC7n+TxVQTdocni4bNuV7fexsbMcXnZqGYsixMZrTrUxnzFl+b3s3u23v8qv5WJLVNFsaxemdEip9XEmRAAqEYAuhDgJZGYmW7p08QhOTaUTfBsi3sU0G6bGoWCFwmWX1Q9g+XNIxStIyXWY26CroKjDhwcQUyauGDfbdkX9vk4gAZzKCGCbTseljLaT1rwMtuIkpXyaLtjaEkU0u3qdfSzpx1wtEQGoRAC6EMqAXJeF9+5NJ/g2lXQAPoKg16zBP5PYXkEfost2EHSJfc1thjJoYq9ru8uV0q6w36fESQ4M4PsFjjJSNvDU1a3vJXFbQvZXVFuiijIXj7ePJf3YqyUiAJUIQBdCGlBVY6Fuauh0Mu/A5GT2inXqgM1sN+ZMsdNx32RT1TlzeF9t68VVdLkIiipsg+/zuE7KoFmVyw9ri3XxlC62ybnpgfKiCPa6MlI38NTVbYonReSETF/iY2KaP2cXkW3zfEwea5/9IgYRgEoEoAuhDajcOfy//6+5QZpykcXyRFFmuza71rjFIjbtBHUgdPEeuD5P7g1HHMtg2CS/xUECm8ewrr6qTvOossWY7YczTpLTa2UjTKvqNkYqFAqprKAUoYqyTsecZ3P9+izkY//+lecYU9MW2UwMfNinDhGASgSgCzENCNvA5uayz/sM4ne5B+7djE3cqeqy49n1eXJsOOLssKs8dOXyDQysTAitu5ficpOuvnTn+XLWty1c9sddXkosqemUlRRCQ3SktrufKpoxArD4Kh9LV/7/8qt4ljWHvfoW+yIAlQhAF2IaEKXx+8q95xtquamDNKVDxwxQpg6y7kVd1uJ+nja7N30JirryTU2tjm0rCnvTcpNu4MPu2I3ZfmyX7Mufb7UyjycXnJ67kEut3QBVNPucxJbbJceKie/lfhGASgSgCzENiOL+xzb86em0RKBPkWvjKTQNUBMTdkuqxcERI0o5d3na/nb+CrEMhvHecaRN8pGzz0c9uC7Zc4opbs9dikutKUMRzVxhBKaJbiohJSZEACoRgC7EMKBcIGA9NbmYwDa62LtTi/gQufv3uy3nYXZEYsWIjShdWODf5VkEKwA/9rEwy2AYYe9yBCKmvlLaoJDakn1eJp0AXFjQbyLh3lTTa2BFM6cH8Oabzf1Qq2UnBiUGMBwQuwBNJrQB2YoLSsNPabkFW+58ZzPmszMz7st5pgGq+O/YHIwYUUpNt2Ezg05J7CgVbtlKV1+peABzcvtyXWbjLO/ERHXM2MQEbfON7wloyuLSpWyY73Lu/KeEilT1fbrPyi7gcEDsAjSZ0GlgKCkyyrskqYecpxATiFleGhykeUSou9k4MM3QMV6udtves0jBJrDc54Dq85QQbH2lvEGhyrawgf6cZ8tS031wCACq7aWUBSFW2bjCCLACcHx89X3plpBDLveLAFQiAF0IZUDULfV1KSyoDT9WyoUiuhgXm0F+Zsb/4Ehd1uL2crnMoCliJ8Sgha2boSHzRMFlg0HKGxTKtuUzRrTq2lzHVlbZWB1U24u9i1tH6LK5hBHkz4ZiY1iPddXOfp+IAFQiAF0IZUDYQXByUj8Tpjb8GElXq6jr7LGejmJH6ns5z0YUcXq5BgfdBwyM2Ak1aGEFKSahs+sGg6ZsUAjpsYyRHslmt3+oXdzUyR/W+1+X25KjnHVhKrr6pdpYCjvpy4gAVCIAXQhlQJxxWZ1OnGVQV2y9HGVRxD04ljtSU8dZBecgurjoXtdK6cVO6M4c633DCDTXJeuUY8iKhPJY+lyir+rPbGwvVAxn3XJ8eaJanBDatH1fS8OmpdpyW1pYwPd3qcXRKiUCUCklAtCF1DyA2MaTckwTFsrAU+6MuAZHlx2/RTDPI48BDPnM6sROjM4c631rikDD4nI/ITyWoT2ANrYXYmOTbYy2jYD2tTRctrXiSSB1ydGrVmGqViFS21ymlAhApZQIQBdCxwByDv4pxzRhoO5sLtcPx3KgTSC1aVkLs+wa+5lxe6Qpybi7SdyZ4Iix9F1noWMAbWzP94TFpg6osXQcfT4nmNQ/RSi5aEO1bxGAIgCdiLELuG4zxPh4mh4CX9ikNCgnXM7Tx0xOnjrCiHJtm45bJ4owzyOFZ8Y1oC4sKDUysvI7IyPNsD/fpLxpoUidF6jYN5X/G/NyDZcot3Wf3nMXL+jioltqFl0b8yX+bZbhMf11ecnZ9w5tEYAiAJ1IIQ+ga6NpsleF6oXLxZerZ8WlwzeJImw+r5jPjGNArYsfMgmAXsB3jCWX/ZjaX74UaJOqpu75Y22vvHw5P+/Pe+4SB7l3r1tqlroJpc8d+rYTQOp9+p7siAAUAehEzJNA6rbUuzSa2MLChoWFLAUItkPi8KzYxu2kHldJwWU5utMxC4DBwe6pKyo+lyy5hAHGC95ur9wFmvctudfLtq2YbK8uwXTV+xzec44JoW1qliob8O09dgkBwTgxQvWbIgBFADoRy4B8eAhSTpJqYmlJfxxY0SvAUW/UDj+1ZTsubJejsXFPXDuam4avgHlOYeAiUjkEbp3t5edx193j3Bz/JNcmHKUqTUoxJOWBB+y87CF26Ls+v+JkIGZGChGAIgCdiGVA3B6CpsQb6cAsKXLVG7XDTzmuMkZaFOwpApOT4e4jJXx4ALmFgYtI5RK4VbtWbe6Rw3Yoy5uY9EW5x5LqZQ+xQ58zpjLm7mARgEqdBkLjOHaM73PLywDXXZc1szJKAfT1AYyPA2zbBtBqkYqZHFz11moBfPazAFdeufrf+vqyvzfeCHDBBQCbNgFs3Zpm3e3blz37J5889V67DXDrrdnzPngwqwvdPbRaAJdcEqzIlejuY/v2eOWyZevWrPxHj1a3y76+7N+3btX/zvLyqWd44sTK+imjFMCRI9nnMc9z0ybzZ+o+5/LdImXbO3CAfo9ctrN9O8C9967+rcHB7O/Pfrby92+5JfvOvn0AV1yx+jkfPQpw880Av/u7APfcs7p8+ffLcI4NdbRaWf1ccUVmi8Wy5/3fLbfg+jwuWxAsia1Am0w3eABTTNBJBevd4DoiSxevk7K3r4jO6wugT17rCucScDd4r6twTfljG1OG9bRgvODDw5lXjvpd22VKqjfJh+1QTgLB9lumfHxFQvbnHBkJYuakFQ+gkiVgF2LHADbdBc8FttMzpVzA7l7VDXrz88Fu2xrbvGVcgoprEwj3sib3MrLr79kOsLY5KqnCALPsWTdx8JHTkiJ+UjiazOdSfyhB5XP5XHYB+0cEoAMxDYir0YSKGfEZn0URsa67V2OeKcqF7a5FzvvjSANja7tVdavbBGXzLKp+b2CAfuA99dq2OSptn63J06hrV9w5LSniJ4WVD9+bfUILqhyu9uJ7NUUEoAhAJ2IbUBNc8CF2F1M7c0y9VXVi3INGXUfpu85cz2/lGhRd7xN7HzMzp+p5amp18mlTImPqcjg2P54PbMS9qzBYWtKnYtL1IeX0MIuLYbxJKax8hE73EyI8xaVNh97IFXv8TgERgA6kYEApu+BDxWfZiNi83mZmslQEuUjQeYPqci/aDBpV1xgeVuqyy/wM0kVc8pZxD4ou9ou9D2yeSA7BRPHA+RiMbcS9qzDwldbFdtKDET8peAB9T759C6ry78/NNSseN4XxOzYQuwBNppsMyNdyjG4Q5YxFsRGxlBMKKDFVmE0kNjFaVbnDbDp4m7xloQZFCq734fKqs1+KuPYRY4a9PueZq67etFCbMcr/HmvzQZHYy7W2pJTQ2ZZuGr9tgdgFaDLdZkCcM8YYM2yKiLUVYa2W26BhG6NVrjNXj4nN8VMpduK6AZRD6FHtl+qB4xbTGFFcPKGDA5e2HnMzRiriK9ZyrS2hNhn5ptvGbxsgdgGaTC8ZEFUcxoqxwZSTQ4TZDhquy68A2VI0h8eEkiokZY9E3XK6az1jXjMzK8tCfb4+YsxM4p47BtHFmxZ7KTYV8dWUROaufWdK2SR6afyuA2IXoMn0igHZeJtid+w6XEXY+Lj9oOG6AcMkbqgek/l53DVT9kgotXoAnZnhFXp1r6Gh1ZuHKAOkT2GjC2fgFvO23rQUNmM0RXyFxmUjXEr9fR29Mn7rgNgFaDK9YEC28TmpxNhUwbEL1nbQcOlA+/rwni1MR4sRKwMD2c7Mpg2KHJ5Wymt8fOUmItMSmW/773RW73b2fX0bb1rKE8VexnUjXEr9fR29MH6bEAHoQLcbkEt6B6XSibEpEzMPnu3GhbzOOHcid/Pg2+lk4pVSx2WPWf7/lGeVe8ZDe+DKxHq2lJMw8s+nOlHsVUynBNn0mymGj3T7+I1hTchj54TmsG9fdubkT39a/xmlTp2tWUV+PubIyMr32+3s/VjntOZnrebnVmKgnnFZR36OZvE3MeR1tm0b7vOYszNDnBsai1YrO5cVw/AwwMJCdl7u/v0Ae/dmf0+cyN4fGsJf9+jR7IxUgOz7U1MAAwMrP1O0/+Xl7Azbe+7J/i4v46+lI9azzc/nffe7s79f/jLAli0Al14KcPXV2d8tW7L+Jf98XXvI//+zn836GO46ElZjOhseIHtmur6r3D/G7u8FDbEVaJPp1hkEdZeXydsUMsYGey3T7tGy94Y7Bg5zggLAyqXF/P64PCbd7AFUCnfkXPm82ir7ocYTYtP1+Ez4ncKzpYSP1G3k+chH/CeSbyo++lXK6kjdys78fDNiKrt1/KYgAtCBbjQgm11eqQgE6oCqi1kKIVrza4yPr15q1wlOrqX1Xlh+cxUh7XZ2egilPWDahe8k6bGfrU16l/l5XIyrzyXFpmwI8TV5wMZHu2yES4VuHL+piAB0oBsNiDoDTEUguGxWSaHDp5bDFHDP4QlNMW7HhomJ1UlqW63s/RyT/QwO0mOgqjzjnU62qUYXn8jVrmI+W5vjGWPnpAxxbCUHPicPlOeWSt9pSzeO31READrQjQZE2SGbikCImUw2JtSlxbk5/OebNpuvQycscvvF2I/NhpCyB5CSd7Hq+7b3H/rZdjpKTU7iRbJLbjnOc6l9emS58N3XxfYch6Qbx28qIgAd6EYDws4Ah4fT6RRTiHdKBYonpejdaPpsvgrsYLm4iKuvqSlzTGHdIGlzegJX7ruQz9ZG5Lqk7OGooyZNIG37OooNYD3HTe8zunH8pnJarM0nQprkO2SPHs2afRXDwwBPPgmwdm3YstXRzbtZKeh28FWR71jNd+hdconX4gXn4MHMTutQKtvFfuAA7vd+8QuAn/9c/5m+vux33/Wu7Ppbt2bvU55LDmYnN4Z8Z65v9u3L7Al7n+12Vj9zc/bX5KgjrJ0cPMhXj8vL2e8dO5bdw9atuOwCNn3dvn2Z/RXvcWAge++GG1ZfN8/eUP5Ou51lQdi+vfo32+1sR7dpt6/tvQseiK1Am0y3ziBMO2Snpuxmfb5mjL3qASzXJ9aTlap3gxtsOMM734n7nC4nZv4qxxrabCJp4jOxWcbNj6Sz9QAODvLUUejTSFxiDbljK3XHAupCTGyXy1OKs+zW8ZuCCEAHutmAqhrq4ODqJTBs4/XZ8HspbiWnqj6piY+rBoxugus0EMoJLFXfpX4+pZgzLDZ1nd/r3JxdcvSpKZ5J5VVXhWsjrrGGmKMb874OK8ptMgfofquur00tzrKbx28sELsATabbDajYuU5Nuc36fDf8btnNihnQbOLJTK+UDmnHgKknTB5ArEixPQKL+mrq5hvb4xVzwTA/X91+616Dg9l3XCeVS0urvbZVrzPPdJ9AusYaYgXd3Fz2eYoo9507NMU4y24fvzFA7AI0mV4xIJfGG7LhY3Y8ci1Dm463srnGwsLq81tHRlaX33bHJKXDThmsN5lDAOb24/ts4Ze8JOyZy9zhGK71s38/Pg8gQJbCR3dcGTZMZXoaX0ZXYe4aqkL9PlWUY/oA2+XyFMN0emX81gGxC9BkutWAbGPLqhovR8OnDFa6z3ItQ+t+x/YaCwu4wYdbiMRcHrcRIRRvsktdTU7STmDheIXy/PkIx3Ctn6rEwuvXrw5rGB09tWSM/W3dve3ejf8d13biGmtI/T7V/n2eHx46zhJDt47fFCB2AZpMNxqQS2xZVeN1bficoo1jGdrmoHRMMmqTpyoPeMfWJ+aZxVwet3muVG+y7bJknT3WhRlgXyYbCSHEudpBlXh3rZ+6MpW9eVRho7s3igcQwM1DhS334qLb9/MyUlcLMPdmG28tHsA0gdgFaDLdZkCusWXcHkDOwYpjGdpl+VV3DayHdXGRNogUB+iqeKlY8Wa2z5VqSy4ewLqBqE642pwUEnoAdA3lKMYDUzzgphg73b9XlclG2NfdGzYGMH+5eKiwXtK6iZCN+DKtLJieexU28dYpbtTrtvHbBohdAE5uv/12de6556r+/n41NjamHnroIdT37rnnHgUAatu2baTrdZMBucaWDQ8rNTNTHQ9n0/A5Ywe5Zp8cy69V18CemjA5iRtEhoezga3qGRdF4dISz9I6BZfnSvUm2yxLYuzKp/fL5xKYbTvAJHcuDv7l+qnb4EGpq2KZuIX9xITb9ylg7EQnpGzE18JC/QqD7SqAzQkzqW3U66bx2xaIXQAuZmdn1dq1a9Wdd96pHn30UXXNNdeojRs3qhMnTmi/d/jwYTUyMqK2bt3a0wKQM7asPIO1aficSwZc8ScuS4r5a3x89e9SBKCuPnXPoAxlCZYzZszludp8lyLMXAeiqnqipo/x6QG0aQeUVQFTCpAqwYDdXV0sk0u8YV0b/93ftb83KlWbvTjq0hQ+MTVVHVNpa++2MbyprER00/htC8QuABdjY2Nq165dJ/9/eXlZbd68Wd1000213+l0Ouqiiy5Sf/Znf6Z27tzZ0wLQd2wZteFzBg2n5AEEWH3PlCVgXX2ankHxu9glWO4UPi7P1dabjM1pyTEQlQfFmRm8XfheAvMdQ2ZqR1WCwcUraeNxrUpPkpfp93+f3pZscdlYV1eXGFI4vi2FMijVXeO3LRC7ABwsLS2pVqul7rvvvhXvv/e971WXX3557ff+4A/+QL3zne9USimUAHzuuefUU089dfJ15MiRRhlQ3vBmZrLg5+KSLTW2bGZG792oGowpDZ/TA8gVf8KxE7SuXrCbQIosLZlPp2i3q5fkMeXzkcLH9bnaLiNV2V6IgYgyafDtBaG2A9sJD2UZ26VtYpamdb8TcmJQxsbzyU0qQiwWIgBVdwjAo0ePKgBQDz744Ir3JyYm1NjYWOV3Dh48qEZGRtRPfvITpRROAO7Zs0cBwKpXEwxI11m22+Zs/LaDg+2SFnfQMFf8ie53KINklUeDKg6wz2Bqiv6d/fv9PGOO55rKMhJmAMVMGlqtU8l7fWNqB8UdtxTvpUubd2mb5c0p2N8xebZtj7vE0OngjhV06T9N+EgF1DREAKreFIBPP/202rJli7r//vtPvtfNHkBMHE9f36nkqpgONEReJ+6gYS7hoPsdl5k9tVOmxCTmv0F5br6eMcdzje29oMZQ6pYrBwbCDrxYzxc1ftElTi5E28zx4dmmgJ1YDQ/7KQN3WEdTEQHYJQKQugT88MMPKwBQrVbr5Kuvr0/19fWpVqulvv/976Ou69OAQu26LHd62HQhofI6cXt7OOu16ndc64VSPmwcUV5n1Jgrn884FS+eDTYDqI+dmC6UPWd15aKIP9d78N02c2LnpMNOrKo2jLkSW/ymhAjALhGASmWbQHbv3n3y/5eXl9XIyEjlJpBf/vKX6rvf/e6K17Zt29Sb3vQm9d3vflctVeXQqMCXAcXYdVns9DiWtjg7ktjeHgqc8Ya6e6bEP5WfLbZ8vp9xk55rju0A2unod37GGnhd0z81TbwrFf9UijrBHUKAxha/KSECsIsE4OzsrOrv71d33XWXOnTokLr22mvVxo0b1fHjx5VSSu3YsUNdf/31td9PZRdwrF2XNp1eanmdUsG1XkwTANuE3fmzpZRPnvFKbAdQmx24IcQxtlzlmLV222+cnE9iiiCs4C5v3sq/62oTNrk0Oe0wpUmfCMAuEoBKKXXbbbepc845R61du1aNjY2p73znOyf/7eKLL1Y7d+6s/W4KAjDmrkvbTq/JS3k+sa0X0wSAeg5q3bOtE5lVgzr3M15aynah796d/UU63JPA1ntE+V7IAH1sufKMASkM3K6EXL0oY7Nxqy6Hn41NUMQvtx2mtvFEBGCXCcDQcBuQz12Xpt906fRSmtWlBLVeMBMAamC+7tmW48B0nTPXM56YWH30VquVvc+Bb1v07QHMd7JWPUMfHleXPqfJ7T6WZ5s6geCOHcWK37k5XjtMceOJCEARgE5wG5DvXZcmkdDrXrvY2OZdMz1X07MN1TmbjtxyFYEhPAy23iPM99rt8AH62Ani/PzK7/ms61DCMsbqBdUDh2nfVJswid+qjYAu10x144kIQBGATjTBA5gzP1/vPZIl2zTgOGqO+mxDdc5LS6s9f+VXq2W/HBzSw2DrPcLk4PPV/nXMzeHsqBgS4KuuQy8ThvZiYicQS0u0UA/O0B3ucSjVjSciAEUAOuErBpA7NqWqsa9fr9QHP9i8pZtuhpIfTGcjw8MrT3nhuKZr5zw9jbvO9DT9t2N4GFxiPOu+F2t3KsUGfNZ1isuEPsBMIKirATY2USd+ue0w9q7rOkQAKrUGhGRotQBuvTX7776+lf+W//8tt2Sfw7JvH8AVVwA8+eTK9595BuC22wB+/nPa7wn+2LoVoN1e/exz+voARkcBPve5U/9f/ncAgM9/HuA97wG45BLzsz12DFc27Ofq+MEPeD9X5ODB1fZdRCmAI0eyz9myvAxw4ADAPfdkf7dtA3jiCYD9+wH27s3+Hj4MsH27/ne2b6//3qZNuLJgP4eFYgO+6np5GeC667LvV/0mAMD4ePa5prN9O8C99wKMjKx8v93O3t++nd7ebGyi1cr6iHe/e2Vfgf2ts87iLRu3XQtmTotdAGEleedw3XUrO9p2OxN/pgGmCKZTve66bDCrEgrLy1lHfuxY1ji3bhWx6JtrrgHYs6f635Q6ZQNcNhKqcz7/fNznlMpEFsXefIvYffuq6/rWW6vr2tRu8oG3TD4BOHq0us329WX/vnWr3X3UQbEBX3WNFZYHDmT1d/QowE9+AjA8nAmppvVN27dn/W6dnVDa2+gor02Y7DDnfe/L2oDuPjC/19cHMDSU/fuBA817lo0mtguyyaR+EohNyoEcaixOk3cEpgA2sXP5SCvXOg+VEgMTA1h+YWO/fJ9YQlmWdI1hi7E7lWIDvjIVTE7ifrecCsWmjpsA5gzp/Nn4uG/T8YX5tQFW71KuehaY3wv9LGUJWEkMoAsxDQgz+NucFatU+EHPN6mLU2xiZ1+75UKJDtMuYKy9lfElYqnxblwxbL52p+raAdYGuOva5kSb0GKIG2x/ZBJNg4N+j95bWNCfXkNtt9hnHSrmUwSgCEAnYhkQVnBRAonLx3+FHvR80QRxanOkGzehUmJU5QE0DQYYQWFKmeHzGEUfmyO4Jy2YdoC1AZ2QpwpdzMSH8kr9HFtqf1T1+YGBbNXG5T6x5aCcN46x99yuZ2ZWny7j0l5sEAGoRAC6EMOAKIKLKi72709nR2DouoqFTe4/X7vlQnlKiyeB7NqFtzcd3AKQsiyZ1xfHffiA2meYvEI60YbN5ch1BnEqdYzBtj/yMRnAlsM1NVXds0ihvYgAVCIAXQhtQDaCC5NMtDiQjY93x6CXujjNselgUx3gbOBIEcH9rKnLkvng7HofPuCsG4xow/4WZeJTF/eXSh1jSKU/opYDm5uS+ixSaC8iACUNTKOwScGwfTvA1BTu9886C+Duu3Gf9bkjkIMQqUE4oOz2y9PAcO8CjQnHLmTOZ12XNqmK4vNINdUFZ92YfgsA/1vYPmFyEmBuDvfZnBTTiaTSH1HKsbwM8MUvul2v7lmk2l56DRGADcJWcN1ww+qcU0XygQwgS61gYng47UEPIG1xWiRPkYCFmgcydbC5D3WiF/sMv/ENfR45XdqkqnIBnHoeHPfhA852wPlb2D7hzW/OUubo6rZI6Dou54ess69U+iPOnI86TPaeanvpNUQANghbwdVqAfzJn2SNSpdg+sc/xv3+e97DM+hhO08K+W8eOoT7fOwZZquVJWI1MTp6KklsN+Ga/Hx5GeDECdy1Pv5xgC1bMi9fFZQB78wzAW68McuBBuAniTsHnJM0zt+i9B3FutXR1xe2jvfty+zp0ksBrr46+1tnX6lMln3kfCyDsfdU20vPEXsNusnEigG0TcFg2uVnE9Pnci4q9+5cSuxWKjGAmLiq4WH7M3Kbgs0uZJsUIjq7tInHtN1Jawt1QwBn2hbOGECl6H2H7nmHPs+cuqEjVL5NEz5yPpZ382KeRf774+Orz6gP9SwlBlDJJhAXYu4Cts3ZphtAbDsp6qA3P08fnLH14ioCfFJV9ylvpAkNRdy4pBCps2ObHdk2O2ltsZ00ceZ5NOVyxO4C1t2Tru8ophGZnlbqL/8y+4s9+5oD2w0dMZJ8V8Gd83FpiWbvVc98aCgTgyHztIoAFAHoREp5ALlmTbadFHbQm5vT54GzmQlTU0pw1RVVsFQN3pRd10IGVwqRsqjGnr7AYbNUXFMacfQZ3B7A4u/q2lHdv8fK8ekyaQuVb9NEVTmGh1eLMG7RmlJqLhGAIgCdCGFAdZ2fz5xtpk7K9tqUlDQUjxe2Q56c5KsryuCj6/R81EdqcNuqjaeu6jU+vvq3KUdWVT0jzL3aLuO6ClDX5xDDW13XziYm4gkJ1xQmqZxMpFuGLfZlXKI1lVQ4OSIARQA64duAYp5iwT3rpnptKB6v0DmluJNxt1rxY4N84cOGXZPTFl91gt3Gwzg+bnfahqk+UgkTwNb75CSPuLFd5vfdZlJ5Hhxg+zIO0ZpavYkAVCIAXfBpQCm5yjnKRPXa+PAAcnQs1Fks5b5jxwZx48uGbY+nqnrVCYXigDc9bf/7xXu1rY8UkuYqZed5tRX7HMv8voREKhs6XAntkUvFjnNEACoRgC74MqDUXOUcZaJ4bWxjAEN0yFSxib3vKu9RjNggLnzZMMY719dHOz3CJBQw9mWKa223lRoZsauPVDwnNjGStptkOJb5fQqJVDZ0uBDarlKx4xwRgHISSJKkkjWes0yU/FbU/E8+ckrV5SikJnTF3ve2bQBPPAGwfz/A3r3Z38OHm5v3z4cNY07pyJ/3ddfhf9f0TE32pZQ+h6VSWZmPHtV/pq4+Ukmam9eDUvjv5J8dH8/qCJs7jyMhss+cetu3Z3k5ywn22+3m5Ou0TU6Nzd9a/txFF6Vhx0KB2Aq0yfiaQcR2lVfN0DkCn03eg1YrSxGDLVMZrmBlXZwWdRbbLctFOdhYIG4bxi4J5s+J4nHGehzq7Au7k9ulPmJ6nIrP3OVs2Kkp/BK4iwfQpU3ZbNBJYUOHDbZ5XzExrKbNOyl4TsUDqGQJ2AVfBhTTVV6Xo+mKK9zLZNphOTeHL1NdbJFrh2yK05qbowu6blguUor2HLhtGPt7i4u0zw8P08MNbHM5crSf0GECthtiql66Zflyu8EuN3O2qZib7mJAnZxiY1hNn5uYSCPcRQSgEgHogu8YwNBeIx/JdauuQWn8ITfDYOPW5ufpgi6V/F+2xD75YGYGZ4czMyuvb/p83aSDAuZe8xhA1/oI6XFy6Q9sX5RThjiFRIqb7nxR9uhi+jJs37i0hP9cbM+pCEARgE6E2AUcymvksuuOWibsIBZ6MwzFa2Uj6Jq6XETp/Iv3ZyOU68DuxJ2ePvUdk4ChnlqhA9Nem+QJ5kq2nd/f4CDus+UlcGpOUhthkeKmO19U1efg4OrnU+7LsH0jtp2mkCJHBKAIQCdi5AEcHq6Pk3PBZRnLlycr9FI4NW6tqYKOCvY5lM8EzWN+OLw0VA9gTsg2hJkU+PQEc9oj17J2Lm6xsYNVbRl7X7rTLRYXs1fVb3D1M776A67fNSWkn5qqvwa2b9y9m9aHxkQEoBIB6EIIA5qbqx5YuQWXTXJdzpM1XMrE1ZmklqaAC9ujtnJsEy8X4yZjJpENKdR9nASCgTt+zfaZl9Ph5OLWd1gLdbm6WDcc/QxX/ZdtY36e73ddvJziAexOIHYBmkwID2CouBSbGX8qiWe5OpNu27GrlHlgwgxcrt6g4eFsac4FzJJk054NFz76Ceozz681P18vbn0tgdssVxev6drPcNU/dsONTX253iO2b8xjAJvQh4oAFAHohE8DCh2XYtOJxk4866MzaVKclgnMbjzMwGWTALhKBLrWnc7L07Rnw4WvfoL6zLHL2D6WwG0nKByihav+qR5M6mYKLi8npm9sSh8qAlAEoBM+DSjGciQlx1eoWVyMzqTpO3aVwg1MptMrqlJAuIhAjucV8tk0IcbTZz+ha3sA+pgxHdz16no2dL6py6af4ah/lw032PAgLjvBtr8m9KEiAEUAOuHTgGIkg6Z0pCEbcowdt00Y/HVwBfGbksAOD9MEIMfEIcSzaUpOOB8Jt4t1m+e9THkgd7X1vXuz+56aWp2r0HSvHPXPmUeyTrByrqZQsjik3IeKAFTqtLDnjghYsMcYHTqUHbOzdSvtqDOXa05NhT3qaPv27Ki0gwezY4k2bdLf77592VFgxSPD2u3sGCtsuVstgEsucS56NDiO0ir/TtVzuOgigPPPz445U0r/W0qdOu5MV7fLy/pn7fvZ5EfOle/n6NHs/ZSO+sK22RMnsnrV9RF17WZ6GmBoCNf2YpAflYexwSr+z//JjqMr3vfAQFYXN9ygv1ds/es+x9VWAbL77+vLjt7btu1U2fNj/K644tTxhTnU4zKx7a/pfWhPEFuBNpmYMYDlF4d3AhP3026nN5Mr0ksJXZWqn2X78ADWQY1fCrGb0pam5YSjxOrp6rHp7cYmREGXnxB73xyeNU4PoKntUldTUvfiuSAeQCVLwC74NqC5OVpnxhVj1YQA3iqaNni7ostxhxmYdDGAANly2OIirr4WFlbHI1FFZQoipImpgLDix7Q82PR2g91FW6wLXYJq6gYO2z6TY5NV1Ut3LrttXkWO1Dap2JEIQBGATvg2IJtUDBwddRMCeKto4uBtC+aUC8xRWhjhgO30l5b0MYEhdlO6EiP2lgNKCpFyPXZTu8nFxvi4fkIyOuqWnLqMa59J8WBi425dnpfP1DapxNKKABQB6IRvA7Ld3cbRUac6a9PR1MGbCuWcW9PAhBEOlE4/5m5KDnyXg9KuqG2w07FLxNut7aZYf4uLSj3wQJa8fnIy+3/s6TK2G2iofWZdWy0nUveda893apu8L7DdRc6FCEARgE6k5gFsakfNRUwREVIwY+9zeDgrB+YkkMXF1TsgbQcVG29IKiLE527Jqh21dd4QW8+JTT2mIr594rKDPeR9U5ZnfYXqxEhtE8MrKAJQBKATvg3INjakyR21C7FO8gi9zEHxDGNtgVsEUAVxSiKEY3B1OdXBdvnN1gPYjSfgFNHVp+nZpHzfvkJ1YqS2iRFjLgJQBKATIQyIurttcBDfYcVe5vV1JmrITSwxNi5QOlesxwzb6Y+P89+PUrjJDmVTiisug6vtqQ65t9Zm+c0lBrBY5iZu/tJhm2S5Kfftow/lmIzZhC+FFtwiAEUAOhHKgCi727ACMHZwrs/rh9rEEmvjQqfjvuO2DEVU+rIR7GQnlJ3aDK4upzrs3283+GIFp0nUNHXzlw5sfZbbU9Pv24XYqW1CrWCJABQB6ERIA7Jd3qkidroNlyUuXwH0NsRatlxY0KevKAolijcYG27gc5Zusykltie7iMvAt3cvffmNIjgxoialuuQAW58zM91xugUXMVPbhIphFwEoAtCJ0AbEEZsRO90G5xLX8HC2JIndIcndccfYuEBZXhwcpIn5hQV8J+1zlk7ZlDI/7+5J5rQNl3NpbTyA2M9PT3evWNGBrZ+pKfNvxV41CU3I1Dah+pYiIgBFADoR2oA4PE6xg+19LXENDWW7LKvw1XGHrkvq8qKNR3d8HPfbpkmGq6By8aS5btZwsQ2bclfFAGKX31LZPZ0qWE+UyV5ir5rEwrUtz8/Tzgtfs0ap2Vkfd7IaEYBKBKALoQ0I05kND2d5ouqIPWD4XOICyJIbF/HZcYfePekqLjivoTvNg0NQuXjSsG3Bh21Ql77ya83Pnxpop6bwy2+xJ3RNAOPZbkKS8qZR1ResX2/Xj/tABKASAehCDAPCuNV1A27sAcPXElfxNT+ffTdEx62LlQHAL1FjcF1exNDpmOML6zYacQoqFw9g8TU8XH1dH7ZRPIWiaAO61+hoNtiVyzI4uPo5VC2/+ZyENC3eTVdel1M/QvSZTatrE6bUO2vW4PtxX4gAVCIAXYhlQKZAed2Ai/FQUFLJFH8XG0TtY4mrPOjn5bHpuKmdcdXzKJ+zG3LJuepV9KiakkKbBOC6ddXf4xRULkHkVdcu1z33oI6xgTxmsZwcWjdQYk5L8JHCpWnxbqbyuqx8+F41aVpdm3DZCV/Vj/tCBKASAehCTANaWtKnAtENuJglEermAUoHRhmwbEVPPshSO27bzrjs/al6Hr6XnE31gbk326B5H14Sk3cV+6pqC5yDuilGtc4LzCmaOVO4NC3ezVT/uei2tU+fHsCm1TUGLu+9bZ1iEQGoRAC6ENOAXDolk5eHOvDovHmuOcdsRU8+6FLqyLUzjrnkbLqmztNUvDesMBoY8Ceoyvdbdz4q1S6KbQFrG4uL+vK5PHNsGSYnw+10x3hvUop3w5S31co2FtgulftaZu/W2EKO+F3b/oKCCEAlAtCFEAZU16m7DLhcM9pOR6mREfvBAjtg2aQTyDcAYAczjs44VHwl9ZixqlQpdfdGmb3bCCqbe6+zE+qJG8W2gJ1YmLy/LmEGk5O0wTDEsmDsGGEqFHudmLBfKjf1QVNTdKHWtLrGwukBNE3AXBABqNQaEJJl3z6ALVsALr0U4Oqrs79btmTvb9qE+42qzx07hvuu6XOf+ATA0aP6zxw5AnDwYPW/tVoAl1wC8O53Z39brerPbdsGcOONAGeeaShwgZ/8BODBB7Pf1vFv/2123YMHAZ58sv5zSunvBYCvXk1s3w7wxBMA+/cD7N2b/Z2fB2i3V36u3Qa4916AoSH8vW3dCjAwgCtH8T62bs2u19dX//lWK3suVOrsZPv2zC6wFNtCqwVw663Zf+vKfPQowBVXZG2uCptnnrfrj38c911sWTjA3s+Xv+yvDBQobWl2FmBuDmBkZOX7eTvZvr3+u9u3Z58pfzdnz55TfTMWn/3F8jLAgQMA99yT/V1epv+GLaa+oK8PYHAQ91vve59fe+95YivQJuNzBmFajsy9OthliaIXheNEEUrS4JkZt3ooe69OOw1/XYwHcGkJ743RnYUbe0bP5S223TGJ8chxxzVh7023c9nkxc7txGUZ1xRmgH35XhbE3o/vAH0sVG9T3i5sl8o7nfr2QY3b89VfpLCpBBPnPTGBs3dfsZDiAVSyBOyCLwPCLkfmcV2mJQ3MDkXdIFPuMDFLq8XX9LRdPbgOllihiz1XN3/pjqrzscPaFepA4xIjOj9Ps61Q96Y76WFx0X4gpsSHce2OrCsLB50O/znTPqHWqWtMGWfcno/YwpQ2lWDivOfnzfbma9IjAlCJAHTBlwFRBmxTI6OKKIx4pGR2B7DzALoMlnmHMTPDM9hSOiPuHdYc2Aw0dfdhGkhinY7iIrqxdlJnx9hd7ZyxUT6D4zlOg7HFxjsX8ghDH+mDuFL4pLipBPM8XSZgLogAlBjAJMHGfHzjGwBLSwB33QWwuHgqHuzw4SxmZXkZ4LrrsuZTRznurhgPs29fFnNUjh+jxnHVxc3oMMXk1ZHHndxyi911TSiljwXctk0f39LXBzA+HjYmRxfvVqyvoi1s3w6wsLC6DkdG9PFSoeIgczCxfF/4QnV8aR4n9bWv4a5VZ/d18WHl2DKuewbAxwDbsG1bnDLoYp51bN+excDWxRADZLYxOprFp9mQ28rCAu7zpmed/97SUhbHahOXWIYjjpkbTJz3j3+M+y3O9iP8M7EVaJOJ7QEsvqpiPLC/Mz29eobGtVzVbmczPGq8DdYLMTCw8v+L3k/OZMJY70fsOEAd1FxxNrFEse6f495ML5Mn2+TtwNbN0BB/yhEKPk8XqYNj6XJurr68LsufNrZiip8u/97ICC7pt47Yx3zaEqvPEA+gkiVgF3zHALos3SoVJlWM6VWOJTMJiE4nE4zr1uF+f3FRP+japJBx6YxCdMJLS5lo3707+6s777YMNfUOdTDFioelJf6jr1zvzfcAxB3b6xMfp4vUkWpC7Pz3qP2wKUTEV4xeypNPHTEmHEqJAFRKdZcAvP3229W5556r+vv71djYmHrooYdqP/uFL3xBvfGNb1QbN25UGzduVG9+85u1n6/CpwDE7sTUNRSXDsE1medLXlJfxrqOjjrTxu5E5IhjxHZGlATDNgJoYmL1JotWi/fwdNcB2SQeqs6+5dylqBOCtp5tjgFoYaF+cw0m9tZFyNiWN0QZuIULR0Ls/HcotoKdHNm2K2x5Y3qPbVmY66hLYL96N+xVF8N+tQY6qDp1QQSg6h4BODs7q9auXavuvPNO9eijj6prrrlGbdy4UZ04caLy81dffbW644471MMPP6wee+wx9b73vU9t2LBBPfnkk+hr+jAgm+WGuo7SpUOgLFcV/39gQKk9e+gdnY1XRpeSpUzdTmZXL2vVdUx1PjhoJ4BMaRMuu4zHm8YxINeJhzwZr03dYjAtW9t4trnKZdqoUnUKTlnIcIkbLCGul+rSJdVWqs56LtZXCA+db8+tF3uoaLQ/hLb617DgddIjAlB1jwAcGxtTu3btOvn/y8vLavPmzeqmm25Cfb/T6ah169apv/iLv0Bfk9uATIPEu95F7yhtOwSXpTybtCM2otf1VIncy1pVN/mgXO7gFxbMnaDNGbam57G0pE+vUid4bOAakKnpg1w9FJjlNapnm2MAwth3u22+7xTyu/kg1aVLrK3s3p2VLT+esO75UH/PpR348Nxa25+uw6xptC/886szO+dWaA0iAFV3CMClpSXVarXUfffdt+L99773veryyy9H/cbTTz+tTj/9dPVXf/VX6OtyGhBmeQC7bFmVoNemQ7AVj1QBQZ1p2wqFqnoYHKQJPVMnmH9nfHz1746M2OfXw+Y0xDwfE74GZJ8DPXZ5DZtyAnv+bqj75o4dC+1JNJUlxaVLajou0/Oh9nMu4p77+Vrbn67DxMyMWq3MreoBEYCqOwTg0aNHFQCoBx98cMX7ExMTamxsDPUbv/M7v6POO+889ctf/rL2M88995x66qmnTr6OHDnCZkCUDPw2HaVth2AjHqkDHsUrYzvgmTowzA48029UxbYVXy4Jdnfvpg0eLoOmrwHZ51IfJfbSdPKH7c51X/eNEbeUMmMnMSHFoW6zVqiNL2UoqyDYE4coYSchN/1g6oHc12A6XWyH5qESRAAqEYBKKXXTTTepM888U/3d3/2d9nN79uxRALDqxWFA2EFifDz8DkHqgEAVEJSZsc1SBkfwNecpDjZCgOIBLL5sl818xBL59ABS2o/OCwuwegOT6zKr631zpYVSym4SE2qZuW6TTFV8ZCgw7cDGU0gRgbE3bljZL6bTLefw0r08VIIIQNUdAtBlCfgzn/mM2rBhg/rv//2/G6+Tggcw70Ri7xA0QREQ2NMcFhft+gAO4cGVFse2HJQYwOLLJXCe2858LvX5fD6uk6ulJX34hum+bXbk69pZ6PvHsrAQ9/q6cunaAWXyUfd7Ln2Tb6w82D4aJHMliABU3SEAlco2gezevfvk/y8vL6uRkRHtJpD/+B//o1q/fr369re/bXVNHzGA2MGRY5nG91IPRUD43L3GsfTomhYHO9DqhADm8HTuPtNXLBH3c8ZMImwENPbZ6O7X5Agx3bftWOriaee6fyy2XvpQy9W661DCd8r9Nza0I2byZqsJNLbDpHgBmStBBKDqHgE4Ozur+vv71V133aUOHTqkrr32WrVx40Z1/PhxpZRSO3bsUNdff/3Jz3/qU59Sa9euVffee686duzYydczzzyDvqavXcAhlndD7SikdNC+PJtN8ABin3FdGpW6vjXJnF8edylSd19TXxRBjUlthLlvjLjFlJljEuPLE2XTRlPZFd3p2Mf3proDuoiV5x57Y5Q4QPEAsgOxC8DJbbfdps455xy1du1aNTY2pr7zne+c/LeLL75Y7dy58+T/n3vuuaoqnm/Pnj3o64XKA8i9vMu9o5ATHzN6jqVH10G4/CoPGJRn/PWv4/vWVPHlualrPx/8IM9zKzsh6u4Ds9w6PIw/xYUaO1ZVZo5JjC9PFNVLn1ofhj26spziJdUd0Cf5ZwNfGP8b1QcvqL6+F3D1TbmxuTmzex6TJ4mICEDVXQIwND5PAvG1rOE7G32qcHhXXQbh4vXa7UzETU5mL2psI0aMrl+fnV0bO8UHFp3N22xCKn/edhNN+YX1QPnw7NgmiS/n23SxX1+TCkp9ufRhvvpWlxQvIVd+6qisl5LBLcC/Vu3W0RVl1E5cKTc2P6+vMA87gUQAigB0ookG1IQlB19weFfrfiNfmtUNrvm/Uc9HrisHVoymnixYJ6S4lvlmZuxFT5WoMHmgsB4hqketOFDnKW0o3iPXSYzPTANYh5FtH4axJYpALD8LlxQvMTf2VdbL4D+pBdi+quAdaKn9cInaO/4QTkBTA8FNiVIZK6SJ4zc3ELsATaaJBpTqsUs5rjN00/d9bp4xeWiw58BiwXqEXDwJITYK1Qkpzvtx3QBRvB7GA2WbtN22/ijeI90kBlMXvlYIsPdi04dhloyr6mVoKBPzZduv+mzevikikHtjn22dryobLKs+WFYL8K/djQB7Y5i4CUbja+L4zQ3ELkCTaaIBpewBdPX2+Ehw67L8uLh4Kjlv7iHgHljz683MuKUaqcJ3kL1LbkWbMQhzLd3JMDnYNjQ0FCa2y8Z7VGfX2Jh8X/0D5l6ofRhGsJtyQxZt3zRpwfxW7L4WVS+wrEbhH1QH1tAKbqtkAw9OTRy/uYHYBWgyTTSgVIOOXYO6fSS45RRAHH0bRyoKbN8ZIsieY1OCza7cOtufmsrqVLexg5K6I2TSdi7vUQorBBgvvq9E87pX/txMq5T5qSypp3hB9xlwMb7gLp0mNk5jZobl/ps4fnMDsQvQZJpqQCkEHRdx3Zhi60kyLZNxCiDXgdXUr3IO3NwbheoGdI60JNTB0zbWyjZ5L6d3LgQprxAUofRhIXJ4VtVP6nWJ7jPg3+IK7tppYndqTU+z3H9Tx29OIHYBmkyTDShm0HEZ147SNb6rLGZ87JTGlnFxcfV3Mf2qbR1WiQ3OgYtjpyz34EkVWJh8fjr7cM2FadqosLTEJxhTXSGoAtuHcXkAKa+9e4OHtJGx9gD66jTFAxgciF2AJtN0A4rpaSji6r3iTnDrY+aOTcExMrJ6sMf0q6aD5ut2hFaJDewO1slJve2YhOvcnH1aklBChOpddvGi225UKKdQc417TW2FQAfm/jjS39j2J6aNNRMT8fpho9ivigGsMwKOTlNiAIMDsQvQZMSAeIjpAcxfRXHpK4UHJQVHHo9GqRvKwG2z+1b3qvJSYYTr/Dy+TsovbiHi4g3NX7ZedK6NCsXnbRP3mpPSCgEHprYxOMgjEIsTE8zkYXAw7mkm2nqBF9TC4G/hjIAjBkV2AQcHYhegyXSrAYWekS4t0XawVi2Buc7wizsGbY91wkCJJRsZoYtRzMCN6WdbLfqyZ1FkUoWryatVNXBy2qWrN7R8wkOxrjFtKdQyJcWLl8oKARe6toFd5i8KcdNEy/aZhva0avsMbgM2dZoB3c/dOn5TgNgFaDLdaEC+U39grqdr93Xlq0vEbOrUbXcMFg92p7K4yD+wF/tVU4yYj+uX65LqECiWGRsLbhpLsGMXhze0qiyUthRyo0JKcXyh0dkEpS/CTLRcnmnZk+hbiDtfgzN4NJD7uRvHbyoQuwBNptsMaGHB3PFxX880yBbbvU2qF90pHS47BsfH7e+bOjDovHGmfrWqLx0YoF2bOni57oDkWE3Cii9Xb2hd/VM3RMbYqBB7J2+K5EJofHz1qkSVJ10nmjie6dRU3CViEpzeuwCqt9vGbxsgdgGaTDcZUKdjzm+FncBRArN1nd/wcOa9wny+uBmi6trcOwZdBk9bDxy1X6XuXtVdc3w82/SB+U5xB6SNcHV9BhTxRRmksfVvsyEyxkaFWPnnmoKNBil+x3RUn0ubTG0zzkkaFDzaTeO3LRC7AE2mmwyI6wQArOeFOshzCDOuHYOuy2c2AnB8nNav2uZG1AkWbLnzZ2DrEMA8g4GBrDx1SYJN90LNRfiSl5hPCMmxtVWTB55rowK2LQs0qvo+6vFw1DaZ5DJ+Q4JHu2n8tmUNCD3P8jLArbfiPnvsWP2/7dsHcMUVAE8+ufL9o0ez9/ftw/1O1fWon6+i1QK45BKAd787+9tqVX8mr4u+vpX/1teXvW65pfq7WH78Y/p3tm0DeOIJgP37Afbuzf4ePgywfXv15w8eXP0cbFEK4MiR7L/b7dX1ktPXBzA6CrB1a/b/27cD3HsvwMjIys+129n7dWXXPYOcn/8c4C1vAdiyZaVdme47v5eDB7P/37Sp/rNF/u//BfjZzwCmpsz172Krg4Or3xsYyOrrC1/I/r+uTnIw/158TsvLAAcOANxzT/Z3edlUcqFMXd/3859nfwcGVr7fbmfP2vSs6ijbMTsuRoHpaIU0iK1Am0y3zCAoy2B1XgOq5yWGB5CCz5UM6rKjzUzfx6aCvXuztC06L1VV/dg6BDA7psvXtdl8gl16xT4LG1vVLdebNkGV4zQpca+hN311I5i+Lz8ertgGdB5ySptkp0eMolvGbxcgdgGaTLcYEHbQHBjgywKAXaKcn1/5eY5NZlh8rWRQRYdNv+tjU0FVQHpRdPgYHzqdbODUbVwpPntu8WX6bl2ZKbZKnTxhTwIxTWJcT+4SMlwmp3XPyDokR9dpYTq0HjKKbhm/XYDYBWgyoQ3IlyDBdmBTU/W/YbNzc27O/PniwNekEwpMYJJCu4gqzk0Fxdxnda89e/yF+lAGWNuJwsICfnc0xutCsVWf3u26PsNmo4pQjeuu9apnZGXHOs8d9ozBHjIKEYAiAJ0IaUA+vfIYsWBKvGsziNl6axqyycxI1b0MD2cbPnSbVLCTAK5dwBgByGmPZagDrO1EgbrJxQTWVjnS3lAJHVLRzfiqS5Id2ySzLP9QjxmFCEAlAtCFUAYUwiuv80hhrmEzebQd+HxvMgu5iY0q6KiTAOxS0uRk9RIvZTkKaytUQk0UfIQZYJ5vjHE3huhsEpR26TM8BWXHLlv+i4XrMaMQASgC0IkQBhTSK+/qXdMdfO6S/DbkhDPV+GfbSYDLiRz5wEfZUOIrFtPkoW61spCC8veoQj5GLtsY8a2ubQ+bUqkB2UBWYdMH+AxPMdYjR8Cva/Z2TgIZjghAEYBOhDCg0G3SZcemboCemKi+VuiBz+YeYscYukwCOOzHZnzhHiMwy9mc3nDXMAOqiAgd3+rS9jD3Fmsi5aodXPqAaOEpHFv+XbO3cxHQcEQAigB0IoQB+fTKc020XARKKhs7Uo5/dhFxHH26zYYSH6tE8/P6o+k4n5FL27AVEaEFhE3bMwnx+fl4EylX7cDRB0TxenJ5AJWK2yEHNhwRgCIAnWiyB5BzouVaxhQ2dqSy+lGF6ySAo0/nTpViQ8rPKMdVRHBOynS/k/875sxb7L0BZAIdm7KHEw7t0AT7qsRly3/VA7HZncZ1DwENRwSgCEAnQsYAcnrlKZ0lZkAaH3cTKNjr+CRlTyvHwMS1rDkyQh9PuGhCjHoKIsI0uav696Eh8/jOmVuymA/Utd1zaYcm2FctNlv+depYN0PwsSQboeGIABQB6EToXcAmD06nk6WymJzMXq5npWJTRw0NxR/0XEnZ04qZ4A8PKzUzszKPWFVuMY7Btm5XsO9VohTElYnYIsI0uctPCLF5dpyny+zdy7cKwWUXTbAvLZRklgDmGWDIJdkIDUcEoBIB6ELsPIDlrP5VudoGB+2Szk5N4do+9veGh9PcBZiLopkZvZD17WnF/hZmkj84uNoWuCftVI8iVXzaJMfN7awohEMTU0RgJncuMZScHkBs/4KBSzt0Ovp8lzHjgNFgk1lOT+MCf0NVhngAowCxC9BkUjkJZGHB3G7yDpVy7Bum7WN/b3w8SBWRqBIxdfdrkwKEq//UrcZgX9R74EzzYbMjVnegAVYIx0jfE3MjJZdA06V+sU03V7z/dlsfSkCtIy7tQOlHk4XLAGOknwjccEQAKhGALqRgQNhOud0+NWBzDBJ522/qsgklZMZmQwrnoFQVr/XBD9LFILYP5dwgRPWCYj7vU7hz4LLpxmWZnmuJVucpw4gk0/OwPudWU2dcO9115TGdhpQMHLu+YsQyBN6BnML4HRuIXYAmE9OA8oFichLfAecDiussvtj2MctyqS2bYLxzrkuJHP2nTgy5PDfTZhGupTmqF5Ty+eLSvU4Ix1q2q9tIOT9P+86GDUrNzuKu6dsDmINJxzM4WB8i4ENbuGqHpk5ka3Hd9RWrQgKmhBABqEQAuhDLgLAekLoOdX6ed6BIJZcflhB9m+s1OIU6dmDlDvuh1oFNnaU8cM/NrY4rrfOkmjzS27aZr4fxhHHlUZybq/+NvM3XeTNDbrjCaofYm3e84OJOjhnLECglhAhAJQLQhRgGZLPb33agpQwUKeTywxKis3ftPzmX6rEDK/fATE0PZPNcUh24qamWMGL/Ix/BX7duMpbvAuaYrNm2eZ/awlY7pDyRiEbTZvZERAAqEYAuxNgEYusVymMAlaKf7Ypt+7Fz+WHLEqqzd+k/OVNuYAdWTjHV6eBjFLvNA0j1pGLvYc0apZ591tzGMBkDuCZrtm0+NW0R0+EVHd1DbNLMnogIQBGAToQ2IBevkG0qmHLbHxzM3k+5IzRtYgjZ2dv2n9weQMzAyimmbNIDmdJw5PZXfC6+nqXLZIZajxSxv2FDvV1Typ/CZC01bZGaKD2Jz4eFTfYa21g8IAJQBKAToQ3IxitUzgOoFG3QzBP/ltPCmHaFxuozsEtvITt7m7rAbK6hvEIvzdmkB7IRgErxP0vXXdBUT6qL2I8uThyhtI0QfUrx2a+BjroY9qtdA3vV/zfFdEHqTXBuya/6ba4dXw1EBKAIQCdS9QDu2FF/EkgOdtC06SN89lk6qEtvscqJhZLzrnyf7Xb2/H0vzXEG+rt4IF29ScVci65Ci3ofnc5qzx71eXft8uQ/E6ytdjqqs7hf/fCKcfXsOuQOHiw2CTF9CbTQiZ4TRASgCEAnYsUAci13mQZNmz4i5qSSOvAuLKxOSDsyko4AVKr+GXEG82OvWZWzr248s7FV1xhEl3g0bF5BTPuyuffZWXsBWLbrbiNYn2IyBJcLUm/Ct0BLMXg2MCIARQA6EXMXMNfAz7lZIvakkiIgmrT6UfeMfMZQmcSUqf7m5uhnBtuOSS5Lgza76jFjok073bbNTQA2KkUJkmB9CtYQbC5ocxO+BVqq2+cDIgJQBKAToQyoPMDNzZk9dxyxMr5imXxNKrHXX1zsntWPGLGWmN3ounxzdSLVxnPmsjRou6seOybaCPSPfCTb7Vv8Tvn/fbSrVOP8g/QpNoZAuSD2fN7ib/oWaLE76wQQAajUaSAkzb59ANddB/Dkk6fea7cBpqcBhoYAjh0D2LQJYOtWgFar/vO33gqwfTvt2ps20T537Bju89jPUVhezl4DAwA//3n1Z/r6sroAWFk/ZZQCOHIE4OBBgEsuYS8qK61W+DIePKivP4DsWVQxNQVwww1Zucu0WpmdXnFF9qyUOvVvfX3Z31tuOfXdffuyzxY/BwBw9Gj2/r336m0ecx9VYNvF9u0A27Zl1ym30zpuvhngk58E+NznAH7wA4Dzzwd4//sBXvay7L7K9wpwyq63bjWXaXl5dXm+/GVcn1H1Xd29cBCkT7ExBOwF9+0DuOYa+m+edRbuO9jPldm6NXvIHEYlNJfYCrTJ+J5BUJcpuZc1MTtRbfKZcU8qMTFcxTropdUPH54d2xyFWM8qxnPGsTRIvY+YnmGO0I+qeq3bdV21GSzGhqkgfYqNQVPiAGx+E+s1XFy0v+9k896EQTyASpaAXfBpQNQBzlesjKkPm5hYXeYQ+fWw5ctfw8PZDs/9++1WZJqIr0HbNUchpl5NwpVDGFDuI4Ux0SXm0ybWMW+v8/Px4mWD9ClUQ6DsBLL9zZkZ3Hf/8i8dblyll4wxICIAlQhAF3waEHWA8zlTnpjQ913FviJ0fj1TH/uSl1Sfxzo4GFaohiZEBgmqoMhfHJ5VDi9up7N6F3jdK5X0QC45JW2eFYD+RJcQbcV7n0IVa5y5gOp+c3oa990NG/ABr2XDyd+bmcmuNzOTVgCo58BUEYBKBKALPg2IOsD5Wta0TQUTYlJp64kqDiTduPoRYuekbY5CgPpJCKW/55rw1O1ULr9cVtpM+B6HuU+VsalnV7z2KQsL5gzk1AtiO+SBgerfxHoA8wat2wFYt/ZfvudUZjlKBYk5EAGoRAC60AsewBipObC4nJfb15f1f2UPUDesfoSKxazqo3W7f3XCk9rfcy0Nxo4H1cWvco13Ps6VDlU/Rbz0Kaa18fXrT8WOUC5ISUng8v2isc/P44M8634nhdlvoBxdIgCVCEAXQsQAYgc4X7EysQdIHRyejcXFNNNf2NLpZKfAhHpm5UE5jxejeFZt+3uOpUGsDU1NOVRSDZi4PI7xzsVTrlv+Lb4aGS+LWfptt+06BdcOeWkJX/mcr9jxLwGTyYoAVCIAXQi1Cxg7wJmW5aam6O0m5XRRrrFoXCIoFbAnWvh+ZlUnrNR5s1z7e44j4DA2FCN+tXg/LuNdp7P6LG+MDsgTeofe2MUOx3mFNu5H2xkKtSH7eMVS9AEHHBGASgSgCyEMiDrAmfoO6rJSjJ29FFxi0WL2c9xQd3naOjawZcEu53L0965LgwsLOEHEaedUr5yrnWJjHav6mGSzhWAevM4Yscsb4+P28Wg2HbjLjJbrFWtmHHDJSQSgEgHoQqyTQDAZCKjHcOlIdgAolK+qf+72nb45Nrs8Bwf9PDfqcm4qIQZYgcQ1YaDG5bnef6ejDwfLl3vrNqBEzxZSFWtgEmUmY6SqYtvOD9uBu27X5nyJB7AngNgFaDKpGpCPMAqXASDEhpC6zW/YHIYpw5UTz3b8opQztSNPsYQWoqE9gErhxXmdvUU7Lg67JFq8EYwxttvm9X/bXU022DZkG4Hn655cjSTgklOq43dIIHYBmkyqBuRrULUNg4lxgkAOJYdhbLAZHMr15/tkDiw2dpdKiEFoIUqJX+W8f9NELnZ7rSwwReTkBoPN9j41Vb+8gb1mlVFQvH7557C7t8oPr+pweNsOATMT0D0rDuMJtOSU6vgdEohdgCaTqgGlsqwWaDd/LQE3lDnjckxXiJM5MNjaXegQg7qcuCmeYhPq/nXliRbq4bIkStkKX6eKx8ftDRojhGw3e0xPr54lUtK95J1L+TsuMwFu4wkQc5Dq+B0SiF2AJpOqAaWwrJaC+EqhHjDYxH0X6y+FkzmUcqvvUDFmunEtRqyrTgOEjLFLob2uwmVmgxWAuTFWqWIbg8YKIdvNHq1W5vEzXU/3et/7Vp4E4joT8GU8chKIdyB2AZpMSAOitIUUltVSEF+peEJ1uMZ95/Xnshs61LKmye58x5hhxrUqQTY8vHLM5cb3SSB113PVOt5xyWC9uOjeCdomYzUJoaUlt0aPjXOsew0M2G9ESTmQl4gIQCUC0IVQBmQTWmESBL49CymIryb0S67Lt8X64zyZw5ZUd4xTxrX5+dU5eFM6JcuFur7EdrXTK7abIvIHyWGMlI4Uu6sYe86v6R6xcY6UTs+m00yhs7dABKBSa0BImn37AK64AuDJJ1e+f/Ro9v6+fdXf274d4N57AQYGVv/b4CB/Octs2sT7ORu2bgVotwH6+qr/va8PYHQ0+1wsjh1z+36x/rZvB3jiCYD9+wH27s3+zs5m91mug/z/b7kFoNVyK0OR3O5GRla+325n72/fznctCgcPrm5DRZQCOHIE4BOfALjySoCf/GTlv5vaWxPQ9SW33IL7DZ/tdRWmBlymbNQcxojtSPftA9izB1fOH/wA97k6cmM9cMD+N+o6HmyHVPxcCp29YEdsBdpkfM8gOE5JiBXUncIytFLpeqRyXI7pwtZfjBxudRstqPksuZaEsU4K3YkZ3DYbMq0KZrWw1YrfXldBiW2oM2qOTOG6jrQqJ6Hu5eoBzF82u4arPHhFbDyAS0v6pYbcuJaWaPXuGfEAqu5aAr799tvVueeeq/r7+9XY2Jh66KGHtJ+fm5tTL3/5y1V/f7961atepb761a+SrufbgFyWMFMI6k5FfEVPYqvBZgOHTf1Fy+H2z9hsKuRMR+K61I4ZOymETrdCuf/Y7XUVdQ14bi5MglFTR0o5s7cYA+iaw88U52jT8dvM3JsQa1OBCEDVPQJwdnZWrV27Vt15553q0UcfVddcc43auHGjOnHiROXnv/Wtb6lWq6U+/elPq0OHDqnJyUn1ohe9SH33u99FX9O3AbmEVqTSJlMRX7EFkA6dUAbQZ2toAlRPtA/PNWZcw2bScA1liuGZdzn1LAl7i9WAOWcOAKt3AdepbewxRhQPKdbAqDN3iQFsLF0jAMfGxtSuXbtO/v/y8rLavHmzuummmyo/f+WVV6q3v/3tK9678MIL1fvf/370NVP2AKbUJlMWX6mgE8pNrj+qJ9qn59o0roU4Di6WZ57SlzTZ3thx2Ylcfk1NrfxtXaOniLC6JKIuM0fKzD0VbwMREYBdIgCXlpZUq9VS991334r33/ve96rLL7+88jujo6Nqenp6xXt/8Ad/oF796lejrxsqBtAmLqehbbKn6caBl2qHvu3WJLR9x63GapepxOQ2DuwDGxrSe+Ha7erK1TV6igjjCLqllK38uQYalwhApU6LtfmEk5/+9KewvLwMZ5999or3zz77bPj7v//7yu8cP3688vPHjx+vvc7S0hIsLS2d/P+nn37aodRmWi2AW2/Ndu719WWtKce0izPfQHf06MrvFb/fbsfdASuspNUCuOSS2KXghbqp0GYTIoXt2wG2bct2BR87lm1M3Lr1VBuybW9YfN9fHS59SU+D7Uj/+I8BrrqqvnJvvbW6cnWN3mSsmN9x6VCwHZIYV2ORNDAEbrrpJtiwYcPJ1+joqPdr2mYyyNskQLgUIIJQhpohIkRGiXxce/e7s7/FNuA7jU3MjBmppuhJGmxH+m/+jZ/K1RlrSohxNZI+paqmNc3i+eefhxe/+MVw7733wjvf+c6T7+/cuRP+8R//Eb785S+v+s4555wDH/7wh2F8fPzke3v27IEvfelL8Hd/93eV16nyAI6OjsJTTz0F69evZ7ufKpaXcRPBMvv2AVx33crcX6OjWZ8lbVLwzfIywJYtZgfK4cOZPVM/77PcNu0N87ux78/XvXU12I601yu3Qff/9NNPw4YNG4KM36nSFQIQAODCCy+EsbExuO222wAA4IUXXoBzzjkHdu/eDddff/2qz1911VXw7LPPwl/91V+dfO+iiy6CV7/61fD5z38edc2mGFCD2qTQheQJiAGqV4fKDgLq55tGt99f1yIdaVfRlPHbK3FDEPmYnZ1V/f396q677lKHDh1S1157rdq4caM6fvy4UkqpHTt2qOuvv/7k57/1rW+p0047Td18883qscceU3v27EkuDYwgdAvUdECppA/yRbffnyCkjozfSnWNBxAA4Pbbb4fPfOYzcPz4cXjNa14Df/InfwIXXnghAABccsklsGXLFrjrrrtOfn5+fh4mJyfhiSeegAsuuAA+/elPw9ve9jb09WQGIQh4qA6Ubne4dPv9CULKyPjdRUvAMRADEgRBEITmIeO37AIWBEEQBEHoOUQACoIgCIIg9BgiAAVBEARBEHoMEYCCIAiCIAg9hghAQRAEQRCEHkMEoCAIgiAIQo8hAlAQBEEQBKHHEAEoCIIgCILQY4gAFARBEARB6DFOi12AJpMfovL0009HLokgCIIgCFjycbuXD0MTAejAM888AwAAo6OjkUsiCIIgCAKVZ555BjZs2BC7GFGQs4AdeOGFF+BHP/oRrFu3Dvr6+th+9+mnn4bR0VE4cuRIz55RGAqp6zBIPYdD6joMUs9h8FXPSil45plnYPPmzbBmTW9Gw4kH0IE1a9ZAu9329vvr16+XjiUQUtdhkHoOh9R1GKSew+CjnnvV85fTm7JXEARBEAShhxEBKAiCIAiC0GOIAEyQ/v5+2LNnD/T398cuStcjdR0GqedwSF2HQeo5DFLP/pBNIIIgCIIgCD2GeAAFQRAEQRB6DBGAgiAIgiAIPYYIQEEQBEEQhB5DBKAgCIIgCEKPIQIwEnfccQds2bIFTj/9dLjwwgvhv/23/6b9/Pz8PLziFa+A008/HX79138d7r///kAlbT6Uuv7iF78IW7duhTPPPBPOPPNMeMtb3mJ8NkIG1aZzZmdnoa+vD975znf6LWCXQK3nf/zHf4Rdu3bBpk2boL+/H172spdJ/4GEWte33HILvPzlL4czzjgDRkdH4UMf+hA899xzgUrbTP7mb/4G3vGOd8DmzZuhr68PvvSlLxm/c+DAAXjta18L/f398Gu/9mtw1113eS9nV6KE4MzOzqq1a9eqO++8Uz366KPqmmuuURs3blQnTpyo/Py3vvUt1Wq11Kc//Wl16NAhNTk5qV70ohep7373u4FL3jyodX311VerO+64Qz388MPqscceU+973/vUhg0b1JNPPhm45M2CWs85hw8fViMjI2rr1q1q27ZtYQrbYKj1vLS0pF73utept73tbeqb3/ymOnz4sDpw4IB65JFHApe8eVDr+u6771b9/f3q7rvvVocPH1YPPPCA2rRpk/rQhz4UuOTN4v7771c33HCD2rdvnwIAdd9992k///jjj6sXv/jF6sMf/rA6dOiQuu2221Sr1VJf+9rXwhS4ixABGIGxsTG1a9euk/+/vLysNm/erG666abKz1955ZXq7W9/+4r3LrzwQvX+97/fazm7AWpdl+l0OmrdunXqL/7iL3wVsSuwqedOp6Muuugi9Wd/9mdq586dIgARUOv5T//0T9V5552nnn/++VBF7Bqodb1r1y71pje9acV7H/7wh9Ub3vAGr+XsJjAC8KMf/ah65StfueK9q666Sr31rW/1WLLuRJaAA/P888/D3/7t38Jb3vKWk++tWbMG3vKWt8C3v/3tyu98+9vfXvF5AIC3vvWttZ8XMmzqusyzzz4Lv/rVr2BgYMBXMRuPbT3/4R/+IZx11lnw7//9vw9RzMZjU8//5b/8F3j9618Pu3btgrPPPhte9apXwSc/+UlYXl4OVexGYlPXF110Efzt3/7tyWXixx9/HO6//35429veFqTMvYKMh3ycFrsAvcZPf/pTWF5ehrPPPnvF+2effTb8/d//feV3jh8/Xvn548ePeytnN2BT12X+w3/4D7B58+ZVHY5wCpt6/uY3vwn/6T/9J3jkkUcClLA7sKnnxx9/HP7rf/2v8J73vAfuv/9++P73vw8f+MAH4Fe/+hXs2bMnRLEbiU1dX3311fDTn/4U3vjGN4JSCjqdDvz2b/82fOxjHwtR5J6hbjx8+umn4Ze//CWcccYZkUrWPMQDKAg1fOpTn4LZ2Vm477774PTTT49dnK7hmWeegR07dsAXv/hFGBoail2cruaFF16As846C77whS/Ab/zGb8BVV10FN9xwA3z+85+PXbSu48CBA/DJT34SPve5z8H//J//E/bt2wdf/epX4Y/+6I9iF00QKhEPYGCGhoag1WrBiRMnVrx/4sQJeOlLX1r5nZe+9KWkzwsZNnWdc/PNN8OnPvUpWFxchFe/+tU+i9l4qPX8gx/8AJ544gl4xzvecfK9F154AQAATjvtNPje974H559/vt9CNxAbe960aRO86EUvglardfK9f/Ev/gUcP34cnn/+eVi7dq3XMjcVm7r+/d//fdixYwf81m/9FgAA/Pqv/zr80z/9E1x77bVwww03wJo14m/hoG48XL9+vXj/iIhFBmbt2rXwG7/xG/CNb3zj5HsvvPACfOMb34DXv/71ld95/etfv+LzAAB//dd/Xft5IcOmrgEAPv3pT8Mf/dEfwde+9jV43eteF6KojYZaz694xSvgu9/9LjzyyCMnX5dffjlceuml8Mgjj8Do6GjI4jcGG3t+wxveAN///vdPCmwAgP/9v/83bNq0ScSfBpu6fvbZZ1eJvFx4K6X8FbbHkPGQkdi7UHqR2dlZ1d/fr+666y516NAhde2116qNGzeq48ePK6WU2rFjh7r++utPfv5b3/qWOu2009TNN9+sHnvsMbVnzx5JA4OEWtef+tSn1Nq1a9W9996rjh07dvL1zDPPxLqFRkCt5zKyCxgHtZ5/+MMfqnXr1qndu3er733ve+orX/mKOuuss9THP/7xWLfQGKh1vWfPHrVu3Tp1zz33qMcff1x9/etfV+eff7668sorY91CI3jmmWfUww8/rB5++GEFAOqzn/2sevjhh9U//MM/KKWUuv7669WOHTtOfj5PAzMxMaEee+wxdccdd0gaGEtEAEbitttuU+ecc45au3atGhsbU9/5zndO/tvFF1+sdu7cueLzc3Nz6mUve5lau3ateuUrX6m++tWvBi5xc6HU9bnnnqsAYNVrz5494QveMKg2XUQEIB5qPT/44IPqwgsvVP39/eq8885Tn/jEJ1Sn0wlc6mZCqetf/epX6sYbb1Tnn3++Ov3009Xo6Kj6wAc+oH7xi1+EL3iD2L9/f2Wfm9ftzp071cUXX7zqO695zWvU2rVr1Xnnnaf+/M//PHi5u4E+pcQ3LQiCIAiC0EtIDKAgCIIgCEKPIQJQEARBEAShxxABKAiCIAiC0GOIABQEQRAEQegxRAAKgiAIgiD0GCIABUEQBEEQegwRgIIgCIIgCD2GCEBBEARBEIQeQwSgIAiCIAhCjyECUBAEQRAEoccQASgIgiAIgtBjiAAUBEEQBEHoMUQACoIgCIIg9BgiAAVBEARBEHoMEYCCIAiCIAg9hghAQRAEQRCEHkMEoCAIgiAIQo8hAlAQBEEQBKHHEAEoCIIgCILQY4gAFARBEARB6DFEAAqCIAiCIPQYIgAFQRAEQRB6DBGAgiAIgiAIPYYIQEEQBEEQhB5DBKAgCIIgCEKPIQJQEARBEAShxxABKAiCIAiC0GOIABQEQRAEQegxRAAKgiAIgiD0GCIABUEQBEEQegwRgIIgCIIgCD3G/w8C6qah3B79zwAAAABJRU5ErkJggg==",
"text/html": [
"\n",
"
\n",
" "
],
"text/plain": [
"Canvas(toolbar=Toolbar(toolitems=[('Home', 'Reset original view', 'home', 'home'), ('Back', 'Back to previous …"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"from visualize_outputs import sample2d, sample3d, plot2d, plot3d\n",
"from onnx2pytorch import convert\n",
"\n",
"%matplotlib widget\n",
"\n",
"n_sample = 1000 # number of points to sample\n",
"frozen_dim = 0 # which dimension will have a constant value for the 2d plot, (0: distance, 1: speed, 2: angle)\n",
"frozen_val = 0.9 # constant value to give to the frozen dimension\n",
"model = convert(\"network.onnx\")\n",
"dim_1, dim_2, colours = sample2d(model, n_sample, frozen_dim, frozen_val)\n",
"plot2d(dim_1, dim_2, colours)\n",
"dim_1, dim_2, dim_3, colours = sample3d(model, n_sample)\n",
"plot3d(dim_1, dim_2, dim_3, colours)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"On this plot we can already start to see some tendencies of alarms. As always the difficult part will be at the decision boundary."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Step 2: Write some safety property\n",
"\n",
"Let us say we would like to check the following property:\n",
"\n",
"\"No input above a distance .95 output an alarm\". \n",
"\n",
"If our neural network correctly follows our specification, it should respect this property (since the distance is above 0.7, no alarm should be issued).\n",
"\n",
"The basics for formulating properties to our various tools is the following:\n",
"\n",
"1. Write constraints on inputs as defined in the specification\n",
"1. State the contraint on outputs you want to check\n",
"1. For tools using SMT, write down the negation of this constraint\n",
" (remember in the course section, VALID(F) is equivalent to ¬SAT(¬F)). \n",
"\n",
"For this tutorial, we wrote a simple API to make easier the writing of properties to check. This API is detailed inside `formula_lang.py` in the repository.\n",
"This API allows to define linear constraints on symbolic variables and real values.\n",
"* To define a new variable, use the constructor `Var(x)`, where `x` must be a string\n",
"* To define a new real number, use `Real(r)` where `r` is a python number\n",
"* A constraint is a linear inequality between two variables or reals. To create a new constraint, use\n",
" `constr = Constr(var1, bop, var2)` where `bop` is either `'>='` or `<`.\n",
"* You can create multiple constraints\n",
"* Finally, once you are satisfied, you can add your constraints to a formula. A formula is a conjunction of constraints\n",
"* `f = Formula()` creates an empty constraint, and `f.add(constr)` add the constraint `constr` to the formula.\n",
" `f.add(c1)` followed by `f.add(c2)` is equivalent to adding a conjunction of `c1` and `c2`\n",
"\n",
"\n",
"Here is how to use it:\n",
"#### Variables creations\n",
"1. Create a new variable with `var = Var(str)`; `str` should be \n",
" either `'x0'`, `'x1'`, `'x2'` or `'y0'`, respectively the first, \n",
" second and third input and only output. For convenience, they \n",
" are already defined when executing the cell below as\n",
" `distance`, `speed`, `angle` and `output`\n",
" \n",
"2. Create a new real value with `real = Real(r)` where `r`\n",
" can be an integer or a float (all variables will be converted\n",
" as real values). For instance, `real = Real(0.95)`\n",
" \n",
" \n",
"#### Creating constraints and adding them to a formula\n",
"1. Create a new constraint between a variable `var` and a\n",
" real value `real` with `constr = Constr(var, bop, real)` where\n",
" `bop` is either `'>='` or `'<'`. For instance, `constr = Constr(distance,'>=',real)`\n",
"2. Create a new empty formula with `f = Formula()`\n",
"3. Add a constraint `constr` to a formula `f` with `f.add(constr)`. \n",
" \n",
"#### Printing and saving to disk\n",
"1. Print a formula `f` with `print(f)`\n",
"2. Write down a formula `f` to SMTLIB2 format at destination `dest`\n",
" with `f.write_smtlib(dest)`; similarly for Marabou format,\n",
" use `f.write_marabou(dest)` or PyRAT format `f.write_pyrat(dest)`.\n",
" For smtlib or marabou the negation of the output is done automatically.\n",
"\n",
"A simple example is given below for the property \"No input above a distance .95 output an alarm\"."
]
},
{
"cell_type": "code",
"execution_count": 69,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"x0 >= 0.95; x0 < 1; x1 >= 0.95; x1 < 1; x2 >= 0.95; x2 < 1; y0 < 0; \n",
"Wrote SMT formula in file formula.smt2\n",
"Wrote marabou formula in file formula.marabou\n",
"Wrote pyrat formula in file formula.txt\n"
]
}
],
"source": [
"from formula_lang import *\n",
"\n",
"distance = Var('x0')\n",
"speed = Var('x1')\n",
"angle = Var('x2')\n",
"\n",
"output = Var('y0')\n",
"\n",
"one = Real(1)\n",
"real = Real(0.95)\n",
"zero = Real(0)\n",
"\n",
"constrs = []\n",
"constrs.append(Constr(distance, '>=', real))\n",
"constrs.append(Constr(distance, '<', one))\n",
"constrs.append(Constr(speed, '>=', real))\n",
"constrs.append(Constr(speed, '<', one))\n",
"constrs.append(Constr(angle, '>=', real))\n",
"constrs.append(Constr(angle, '<', one))\n",
"constrs.append(Constr(output, '<', zero))\n",
"\n",
"formula = Formula()\n",
"for c in constrs:\n",
" formula.add(c)\n",
" \n",
"print(formula)\n",
" \n",
"formula.write_smtlib()\n",
"formula.write_marabou()\n",
"formula.write_pyrat()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Launch solvers and recover results\n",
"\n",
"As mentioned, we will use three tools in this tutorial:\n",
"\n",
"1. Z3, a theorem prover from Microsoft Research [https://github.com/Z3Prover/z3](https://github.com/Z3Prover/z3), used as a state-of-the-art SMT solver; however it does not have any particular heuristics to work on neural networks \n",
"2. PyRAT, a tool internally developped at the lab, that leverages abstract interpretation to verify reachability properties on neural networks. The source is currently not available, if you want to access it just send us an email\n",
"3. Marabou, a solver tailored for neural network verification: it uses a specialized Simplex algorithm and merges relevant neurons. See [the paper](https://arxiv.org/abs/1910.14574) for more details\n",
"\n",
"You will notice that PyRAT performs a \"reachability analysis\" (given the input range, what is the possible output range?). Marabou does not deal with disjunction of clauses ($a< x1 z3_input\n",
" \n",
" t = time.perf_counter()\n",
" output = !z3 z3_input\n",
" output = \"\\n\".join(output)\n",
" if verbose:\n",
" print(output)\n",
" \n",
" return \"unsat\" in output, time.perf_counter() - t "
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"To launch Z3, provide the filepath of the network's control flow in SMTLIB as well as the filepath of the\n",
"formula you generated. \n",
"\n",
"A **SAT** result will be followed by an instanciation of the input and outputs that satisfies the negation of your property, i.e. a counter-example. \n",
"\n",
"An **UNSAT** result signifies that it could not find such a counter example and that your property holds."
]
},
{
"cell_type": "code",
"execution_count": 73,
"metadata": {
"scrolled": false
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"cat: network_QF_NRA.smt2: Aucun fichier ou dossier de ce type\n",
"/bin/bash: z3 : commande introuvable\n"
]
}
],
"source": [
"res, t_z3 = launch_z3('network_QF_NRA.smt2','formula.smt2')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Step 2: Marabou the simplex-based solver\n",
"\n",
"As opposed to Z3, Marabou is tailor-made for neural network. It uses its own property format and can only read network under the NNet format. We already provide a copy of the ONNX network in NNET that was made using a converter `network.nnet`."
]
},
{
"cell_type": "code",
"execution_count": 74,
"metadata": {},
"outputs": [],
"source": [
"def launch_marabou(network, constraints, verbose=True):\n",
" \"\"\"Launch marabou on the verification problem:\n",
" network is a .nnet description of the network (provided here\n",
" for simplicity) and constraints is a property file you wrote\"\"\"\n",
" t = time.perf_counter()\n",
" output = !./bin/marabou.elf --timeout=100 $network $constraints\n",
" output = \"\\n\".join(output)\n",
" if verbose:\n",
" print(output)\n",
" return \"unsat\" in output.lower(), time.perf_counter() - t "
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Similarly for Marabou, provide the filepath of model and the property you generated in the Marabou format. The output of Marabou is more verbose dans Z3, the important part lies at the end: SAT or UNSAT. "
]
},
{
"cell_type": "code",
"execution_count": 75,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"/bin/bash: ./bin/marabou.elf: Permission non accordée\n"
]
}
],
"source": [
"res, t_marabou = launch_marabou(\"network.nnet\", 'formula.marabou')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Step 3: PyRAT with Abstract Interpration\n",
"\n",
"PyRAT API provide directly a function to launch the analysis `launch_pyrat`. Remember that a _negative value_ means\n",
"no alarm issued, while a _positive value_ means that an alarm is issued. \n",
"\n",
"PyRAT can directly work on the ONNX network while its input format is similar to the Marabou with only the difference of having the property to prouve instead of its negation.\n",
"- **True** means the property holds,\n",
"- **False** means it does not.\n",
"\n",
"PyRAT will also output the bounds reached at the end of the analysis."
]
},
{
"cell_type": "code",
"execution_count": 76,
"metadata": {
"scrolled": false
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Output bounds:\n",
" [-6.0188885]\n",
"[-5.915209]\n",
"Result = True, Time = 0.00 s\n"
]
}
],
"source": [
"from pyrat_api import launch_pyrat\n",
"\n",
"res, t_pyrat = launch_pyrat(\"network.onnx\", \"formula.txt\")"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"With PyRAT you can also use different abstract domains to get a more precise results, avalaible domains are \"poly\", \"zono\", \"symbox\". While they increase precision they also increase computation time. Nevertheless, unless we are in such simple setting the interval by themselves are often too imprecise to conclude.\n",
"\n",
"An additional argument `split_timeout` can also help to increase the precision of the analysis. Try it for now and we will see it in more details in the next section."
]
},
{
"cell_type": "code",
"execution_count": 77,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Result = True, Time = 0.01 s, Safe space = 100.00 %, number of analysis = 1\n"
]
}
],
"source": [
"res, t_pyrat = launch_pyrat(\"network.onnx\", \"formula.txt\", domains=[\"zono\"], split_timeout=10)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Moving to bigger properties\n",
"\n",
"You were able to launch solvers to verify this simple property. We can already notice that Z3 took significantly more time than the others to return a result: it comes from the suboptimal encoding of the problem as well as the lack of heuristics tailored to neural network verification. Using Z3 on more complex properties will likely hang your session; don't hesitate to terminate the cell's execution if it takes too much time.\n",
"\n",
"Even so, with all three tools we managed to prove the simple property we created. But this property was not the one we initially mentioned. We should aim to answer the following questions:\n",
"- With the setting of $\\alpha = 0.5$, $\\beta = 0.25$, $\\delta_1 = 0.3$, $\\delta_2 = 0.7$ can we prove our three initial properties on this network ?\n",
"- If not for what values of $\\alpha, \\beta, \\delta_1$ and $\\delta_2$ do they hold ?\n",
"\n",
"Initial properties of the zones:\n",
"1. a **”safe”** zone: when B is in this zone, it is not considered a threat for any $||\\vec{d}|| > \\delta_2$, no ALARM is issued.\n",
"2. a **”suspicious”** zone: when B is in this zone, if $||\\vec{v}|| > \\alpha$ and $\\theta < \\beta$\n",
" then a ALARM should be issued. Else, no ALARM is issued.\n",
"3. a **”danger”** zone: when B is in this zone, a ALARM is issued no matter what. When $||\\vec{d}|| < \\delta_1$, B is in the danger zone.\n",
"\n",
"**Write these properties and try proving them with the different tools**. "
]
},
{
"cell_type": "code",
"execution_count": 154,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"x0 >= 0.7; x0 < 0.3; x1 >= 0.4; x1 < 1; x2 < 0.25; x2 >= 0; \n",
"Wrote pyrat formula in file safe.txt\n",
"Wrote pyrat formula in file suspicious.txt\n",
"Wrote pyrat formula in file danger.txt\n"
]
}
],
"source": [
"from formula_lang import * \n",
"\n",
"distance = Var('x0')\n",
"speed = Var('x1')\n",
"angle = Var('x2')\n",
"\n",
"output = Var('y0')\n",
"\n",
"one = Real(1)\n",
"delta_1 = Real(0.2)\n",
"delta_2 = Real(0.78)\n",
"alpha = Real(1)\n",
"beta = Real(0.01)\n",
"zero = Real(0)\n",
"\n",
"# Safe\n",
"constrs = []\n",
"constrs.append(Constr(distance, '>=', delta_2))\n",
"constrs.append(Constr(distance, '<', one))\n",
"constrs.append(Constr(speed, '<', zero))\n",
"constrs.append(Constr(speed, '>=', zero))\n",
"constrs.append(Constr(angle, '>=', zero))\n",
"constrs.append(Constr(angle, '<', one))\n",
"constrs.append(Constr(output, '<', zero))\n",
"\n",
"formula_safe = Formula()\n",
"for c in constrs:\n",
" formula_safe.add(c)\n",
" \n",
"# Suspicious\n",
"constrs = []\n",
"constrs.append(Constr(distance, '>=', zero))\n",
"constrs.append(Constr(distance, '<', one))\n",
"constrs.append(Constr(speed, '>=', alpha))\n",
"constrs.append(Constr(speed, '<', one))\n",
"constrs.append(Constr(angle, '>=', zero))\n",
"constrs.append(Constr(angle, '<', beta))\n",
"constrs.append(Constr(output, '>=', zero))\n",
"\n",
"formula_sus = Formula()\n",
"for c in constrs:\n",
" formula_sus.add(c)\n",
" \n",
" \n",
"# Danger\n",
"constrs = []\n",
"constrs.append(Constr(distance, '>=', zero))\n",
"constrs.append(Constr(distance, '<', delta_1))\n",
"constrs.append(Constr(speed, '>=', zero))\n",
"constrs.append(Constr(speed, '<', one))\n",
"constrs.append(Constr(angle, '>=', zero))\n",
"constrs.append(Constr(angle, '<', one))\n",
"constrs.append(Constr(output, '>=', zero))\n",
"\n",
"formula_danger = Formula()\n",
"for c in constrs:\n",
" formula_danger.add(c)\n",
" \n",
"print(formula)\n",
" \n",
"formula_safe.write_pyrat(\"safe.txt\")\n",
"formula_sus.write_pyrat(\"suspicious.txt\")\n",
"formula_danger.write_pyrat(\"danger.txt\")"
]
},
{
"cell_type": "code",
"execution_count": 155,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Result = True, Time = 0.01 s, Safe space = 100.00 %, number of analysis = 1\n",
"Result = False, Time = 0.04 s, Safe space = 75.00 %, number of analysis = 7\n",
"Result = True, Time = 0.07 s, Safe space = 100.00 %, number of analysis = 11\n"
]
}
],
"source": [
"res, t_pyrat = launch_pyrat(\"network.onnx\", \"safe.txt\", domains=[\"zono\"], split_timeout=10)\n",
"res, t_pyrat = launch_pyrat(\"network.onnx\", \"suspicious.txt\", domains=[\"zono\"], split_timeout=10)\n",
"res, t_pyrat = launch_pyrat(\"network.onnx\", \"danger.txt\", domains=[\"zono\"], split_timeout=10)\n",
"#res, t_marabou = launch_marabou(\"network.nnet\", 'formula.marabou')\n",
"#res, t_z3 = launch_z3('network_QF_NRA.smt2','formula.smt2')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"*****\n",
"\n",
"## Part 3: A real problem ACAS-Xu\n",
"\n",
"Let's tackle a more complex network of the public benchmark of Airborne Collision Avoidance System for Unmanned vehicles (ACAS-Xu). For an introduction of the ACAS-Xu benchmark, see _An Introduction to ACAS Xuand the Challenges Ahead , Manfredi G., Jestin Y._\n",
"\n",
"Formerly, programs such as ACAS were implemented as a lookup table. The neural network approach was partly introduced to reduce the memory requirements for hardware of the original 2GB tables down to 3MB. Neural network becoming more and more efficient, industrials considered using them as a possible replacement. Since we are dealing with critical systems, software safety is a major concern.\n",
"\n",
"In _Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks_ , Katz et al. provided a neural network implementation of a ACAS-Xu system, as well as a tooling to formally verify several safety properties. It was then adopted as a common benchmark in the literature.\n",
"\n",
"The problem is similar to our previous one, a neural network needs to give direction advisory to a drone when an intruder is detected at proximity. The advisory can be \"Clear of Conflict\" meaning there is no risk of collision, \"Right\", \"Strong Right\", \"Left\", \"Strong Left\" for evasion direction. The minimum score will correspond to the decision taken.\n",
"\n",
"\n",
"\n",
"The network takes 5 inputs:\n",
"- ρ (m): Distance from ownship to intruder.\n",
"- θ (rad): Angle to intruder relative to ownship heading\n",
"direction.\n",
"- ψ (rad): Heading angle of intruder relative to ownship\n",
"heading direction.\n",
"- $v_{own}$ (m/s): Speed of ownship.\n",
"- $v_{int}$ (m/s) Speed of intruder.\n",
"\n",
"We want to prove one property on this network: \n",
"\n",
"**Property 1.**\n",
"- Description: If the intruder is distant and is significantly slower than the\n",
"ownship, the score of a COC advisory will always be below a certain fixed\n",
"threshold.\n",
"- Input constraints: ρ ≥ 55947.691, $v_{own} ≥ 1145$, $v_{int} ≤ 60$.\n",
"- Desired output property: the score for COC is at most 1500.\n",
"\n",
"The formulas for this property are already written. Normalised values will be given below."
]
},
{
"cell_type": "code",
"execution_count": 156,
"metadata": {
"scrolled": false
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Wrote pyrat formula in file formula_p1.txt\n",
"Wrote marabou formula in file formula_p1.marabou\n",
"Output bounds:\n",
" [-10710.81020574 -9110.01167952 -12047.17947303 -2730.80270361\n",
" -13194.04888676]\n",
"[ 5272.51746506 5429.67755395 4817.41682782 10864.69018591\n",
" 5844.88081043]\n",
"Result = Unknown, Time = 0.01 s\n"
]
}
],
"source": [
"from formula_lang import formula_p1\n",
"from pyrat_api import launch_pyrat\n",
"\n",
"formula_p1().write_pyrat(\"formula_p1.txt\")\n",
"formula_p1().write_marabou(\"formula_p1.marabou\")\n",
"\n",
"res, t_pyrat = launch_pyrat(\"acas.nnet\", \"formula_p1.txt\", domains=[\"zono\"])\n",
"#res, t_marabou = launch_marabou(\"acas.nnet\", 'formula_p1.marabou') # does not finish"
]
},
{
"cell_type": "code",
"execution_count": 158,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Result = True, Time = 2.97 s, Safe space = 100.00 %, number of analysis = 281\n"
]
}
],
"source": [
"# splitting the inputs\n",
"res, t_pyrat = launch_pyrat(\"acas.nnet\", \"formula_p1.txt\", domains=[\"zono\"], split_timeout=100)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We can see here that PyRAT performs 281 analysis on this property in total. Indeed after failing to prove the property at the begining it divides the input space and perform subsequent analysis until it proves the property. At the same time we see that Marabou takes too long to prove the property so we might want to accelerate this.\n",
"\n",
"In this part, we will aim to facilitate the analysis similar to the `split_timeout` option of PyRAT. For this we will divide the input space into smaller parts before performing the analysis on smaller parts.\n",
"\n",
"### Step 1: Divide a formula\n",
"\n",
"We will first look at how to divide the input space for our problem. As we worked until now on Formulas it might not be evident to divide them as they are mostly in a textual form. We will thus come back to our Interval class, which we can easily divide, then transform an Interval into a constraint that we can add into a Formula.\n",
"\n",
"**Write the following functions.** `create_formula_p1` is already written and should properly create a formula if `interval_to_constraint` is correctly implemented."
]
},
{
"cell_type": "code",
"execution_count": 169,
"metadata": {
"scrolled": true
},
"outputs": [],
"source": [
"def divide_interval(x: Interval) -> (Interval, Interval):\n",
" if isinstance(x, Interval):\n",
" return Interval(x.lower, (x.upper+x.lower)/2), Interval((x.upper+x.lower)/2, x.upper)\n",
" raise NotImplementedError\n",
"\n",
"assert divide_interval(Interval(0, 1)) == (Interval(0, 0.5), Interval(0.5, 1))\n",
"assert divide_interval(Interval(-5, 1)) == (Interval(-5, -2), Interval(-2, 1))"
]
},
{
"cell_type": "code",
"execution_count": 171,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"x0 >= 0.6; x0 < 0.6798577687; x1 >= -0.5; x1 < 0.5; x2 >= -0.5; x2 < 0.5; x3 >= 0.45; x3 < 0.5; x4 >= -0.5; x4 < 0.45; y0 < 3.9911256459; \n"
]
}
],
"source": [
"from typing import List\n",
"\n",
"def interval_to_constraint(x: Interval, name: str) -> (Constr, Constr):\n",
" if isinstance(x, Interval):\n",
" return Constr(Var(name), '>=', Real(x.lower)), Constr(Var(name), '<', Real(x.upper))\n",
" \n",
"\n",
"def create_formula_p1(inputs: List[Interval]) -> Formula:\n",
" output = Var('y0')\n",
"\n",
" constrs = []\n",
" for i in range(len(inputs)):\n",
" constrs.extend(interval_to_constraint(inputs[i], f\"x{i}\")) # for each input interval we create and add the constraint\n",
" \n",
" constrs.append(Constr(output, '<', Real(3.9911256459))) # constraint on the output\n",
"\n",
" formula = Formula()\n",
" for c in constrs:\n",
" formula.add(c)\n",
"\n",
" return formula\n",
"\n",
"initial = [Interval(0.6, 0.6798577687), Interval(-0.5, 0.5), Interval(-0.5, 0.5), Interval(0.45, 0.5), Interval(-0.5, 0.45)]\n",
"print(create_formula_p1(initial))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Step 2: Iteration algorithm\n",
"\n",
"Now we can generate formula from intervals and divide the intervals, we can start working on an algorithm to divide the input space for the analysis. The general idea of the algorithm would be:\n",
"\n",
"1. Initial: 1 Interval per input as defined by the property\n",
"2. Create a formula from the intervals\n",
"3. Run an analysis with eith PyRAT or Marabou (Marabou has a timeout of 100 it can be changed in `launch_marabou`)\n",
"4. If property is verified stop. \n",
" Otherwise, divide an interval in 2 and come back to step 2 for both subspaces created\n",
"5. If all subspaces are proven True/unsat we can conclude that the initial space is as well.\n",
"\n",
"`launch_pyrat` and `launch_marabou` both return a tuple of `boolean, float` the boolean indicates if the property holds when it equals `True`. The float is the time taken for the analysis. Here do not use `split_timeout = 0` for PyRAT not to do any splitting on its own."
]
},
{
"cell_type": "code",
"execution_count": 182,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-13703.76840556 -11650.49647462 -15399.48471075 -3491.64369193\n",
" -16873.93784018]\n",
"[ 6741.31879213 6948.28653093 6161.77284022 13889.18982366\n",
" 7474.49709356]\n",
"Result = Unknown, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-3550.55339166 -3023.83749887 -4002.8480418 -902.79341163\n",
" -4383.57122813]\n",
"[1745.18966127 1794.98362025 1593.07387949 3605.36711416 1933.38484528]\n",
"Result = Unknown, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-55.06820859 -46.94232084 -65.63917304 -19.87184717 -73.61251578]\n",
"[37.9098227 37.86804778 35.40315467 70.01284302 43.81451971]\n",
"Result = Unknown, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-0.02121775 -0.01879782 -0.01952425 -0.01893638 -0.0185982 ]\n",
"[-0.01423817 -0.01179154 -0.00823094 -0.01761423 -0.00731985]\n",
"Result = True, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-0.0207541 -0.01877377 -0.01951269 -0.01891985 -0.01858325]\n",
"[-0.02016294 -0.01871954 -0.01948663 -0.01888259 -0.01854955]\n",
"Result = True, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-352.70570723 -303.42657267 -401.7464177 -90.58138666 -436.26610886]\n",
"[172.19825764 173.99488784 157.01285023 362.83767465 192.71922046]\n",
"Result = Unknown, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-0.15568065 -0.1716002 -0.20014387 -0.699908 -0.27070714]\n",
"[0.92424944 1.04669573 1.47032404 0.97590631 1.82164312]\n",
"Result = True, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [ -7.47190445 -6.81427319 -10.90876595 -6.29717939 -14.23650304]\n",
"[12.45968295 12.90411493 12.33305946 16.50971771 15.35373532]\n",
"Result = Unknown, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-0.02050728 -0.01878764 -0.01951936 -0.01892939 -0.01859188]\n",
"[-0.0042468 0.00676165 0.05240967 0.00147856 0.06137028]\n",
"Result = True, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-0.05395529 -0.07882239 -0.0844974 -0.09567312 -0.23208993]\n",
"[0.10340051 0.15111863 0.11976172 0.14357011 0.18966976]\n",
"Result = True, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-3695.87115685 -3150.16992906 -4167.56277234 -945.01871031\n",
" -4559.71282389]\n",
"[1821.48322914 1870.45224624 1662.87037422 3759.04988596 2018.72527643]\n",
"Result = Unknown, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-282.51928827 -241.91368502 -320.69790512 -73.04203202 -349.31167125]\n",
"[138.68520869 140.0404299 127.11648591 288.24411521 156.15636524]\n",
"Result = Unknown, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-1.60438756 -1.94363294 -3.4275154 -3.51762934 -4.9584253 ]\n",
"[6.10297656 7.01423348 7.20661815 8.34524076 8.29646485]\n",
"Result = Unknown, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-0.02100108 -0.01882828 -0.01953889 -0.01895731 -0.01863867]\n",
"[-0.0172831 -0.01226754 -0.01223274 -0.01425342 -0.0132472 ]\n",
"Result = True, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-0.02078877 -0.01879703 -0.01952387 -0.01893584 -0.01859771]\n",
"[-0.01966997 -0.01630435 -0.01706997 -0.01716751 -0.01701337]\n",
"Result = True, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-0.02383511 -0.01882766 -0.03147746 -0.05449972 -0.01881987]\n",
"[0.08913946 0.19379825 0.13595365 0.15602469 0.15905256]\n",
"Result = True, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-1.95314583 -2.29833054 -4.66155779 -4.11012113 -6.49521951]\n",
"[ 6.57163797 8.37302401 7.80644603 11.1525727 9.50623178]\n",
"Result = Unknown, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-0.02041463 -0.01878185 -0.01951658 -0.01892541 -0.01858828]\n",
"[-0.02007477 -0.01875068 -0.01950159 -0.01890399 -0.0185689 ]\n",
"Result = True, Time = 0.01 s\n",
"Wrote pyrat formula in file formula.txt\n",
"Output bounds:\n",
" [-0.02037451 -0.01878399 -0.0195176 -0.01892688 -0.0185896 ]\n",
"[-0.02005151 -0.01875436 -0.01950336 -0.01890652 -0.01857119]\n",
"Result = True, Time = 0.01 s\n"
]
}
],
"source": [
"def analyse(inputs: List[Interval]):\n",
" formula = create_formula_p1(inputs)\n",
" formula.write_pyrat(\"formula.txt\")\n",
" res, t_pyrat = launch_pyrat(\"acas.nnet\", \"formula.txt\", domains=[\"zono\"])\n",
" \n",
" if(res == True):\n",
" return True \n",
" else:\n",
" i1 = []\n",
" i2 = []\n",
" for i in range(len(inputs)):\n",
" i_div = divide_interval(inputs[i])\n",
" i1.append(i_div[0])\n",
" i2.append(i_div[1])\n",
" \n",
" analyse(i1)\n",
" analyse(i2)\n",
" \n",
"initial = [Interval(0.6, 0.6798577687), Interval(-0.5, 0.5), Interval(-0.5, 0.5), Interval(0.45, 0.5), Interval(-0.5, 0.45)]\n",
"analyse(initial)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"You can print some statistic like the number of analysis you do or the time taken. **Can you do less analysis than PyRAT?**\n",
"\n",
"### Heuristics to go further\n",
"\n",
"How could we reach the same number or lower of analysis from PyRAT:\n",
"- Can we select the interval to split more carefully?\n",
"- Can we ignore some of the preliminary analysis because we know they won't succeed?"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"*****\n",
"\n",
"## Part 4: Choosing a network for image classification\n",
"\n",
"For this section we will focus on an open source image dataset for classification purpose. The images we will use are a subset of the Fashion Mnist dataset ([available here](https://www.kaggle.com/datasets/zalando-research/fashionmnist)). This dataset was developed to replace the MNIST dataset which was overused and presents the same caracteristics:\n",
"- 28x28 grayscales images\n",
"- 10 output classes: T-shirt, Trouser, Pullover, Dress, Coat, Sandal, Shirt, Sneaker, Bag, Ankle boot\n",
"\n",
"\n",
"\n",
"We will use a subset of 50 images for the purpose of this TP.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The goal for this part is to decide which model would be best suited for our needs. Let's suppose we are in a critical system where picking the right class for the cloth might lead to any potential damage (ecological, financial, loss of clients, ..). \n",
"\n",
"We propose 5 models trained with different methods:\n",
"1. **Baseline model**, normal training\n",
"2. **Adversarial model**, adversarial training\n",
"3. **Pruned model, normal** training + pruning\n",
"4. **Certified model**, certified training\n",
"5. **Pruned certified model**, certified training + pruning\n",
"\n",
"We must decide on a model to use. The accuracy of the models is already calculated on the whole test set (more than 50 images). This is already a first criteria of choice as some training lead to less accuracy.\n",
"\n",
"|Model | Accuracy|\n",
"|--- | ---|\n",
"|Baseline | 90.50%|\n",
"|Adversarial | 79%|\n",
"|Pruned | 89%|\n",
"|Certified | 72.30%|\n",
"|Pruned Certified | 73.20%|\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Step 1: Local robustness \n",
"\n",
"We will look at the local robustness of the five models around the 50 images from our subdataset. All models and images are available in the `fmnist` folder. We already created two utility functions to read images and to launch PyRAT on an image and a network. `read_images` return a list of `(image_i, label_i)` while `local_robustness` returns the robustness of a network around an image for a given perturbation.\n",
"\n",
"An example is given below with a bag image and a perturbation of 1/255 (1 pixel modified)."
]
},
{
"cell_type": "code",
"execution_count": 84,
"metadata": {
"scrolled": false
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Image shape: (28, 28), label: 7\n",
"Robust: True, Time: 0.39942956200047774\n"
]
},
{
"data": {
"image/png": "iVBORw0KGgoAAAANSUhEUgAAAaAAAAGdCAYAAABU0qcqAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjMuNCwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy8QVMy6AAAACXBIWXMAAA9hAAAPYQGoP6dpAAAdTUlEQVR4nO3df2yV5f3/8dcp0FN+tKeU0p5WChZQcPJjG5PaqQxDQ8HNCLJEnX/A4nS4YqZMXVim6FzSjU/ijAvTJUtkZoLOZEAkC4kWW/ajxYAwwpwNxU6q9IeinEOLLaW9vn/w9cwjP6+b077b8nwkV0LPfb97v3v15rx6n3P3asg55wQAQD9Ls24AAHB5IoAAACYIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgYrh1A1/W29urI0eOKDMzU6FQyLodAIAn55yOHz+uwsJCpaWd+zpnwAXQkSNHVFRUZN0GAOASNTU1acKECefcPuBegsvMzLRuAQCQAhd6Pu+zAFq/fr2uvPJKZWRkqKSkRG+99dZF1fGyGwAMDRd6Pu+TAHrllVe0evVqrV27Vm+//bZmz56t8vJytbW19cXhAACDkesDc+fOdRUVFYmPe3p6XGFhoausrLxgbSwWc5IYDAaDMchHLBY77/N9yq+ATp48qT179qisrCzxWFpamsrKylRbW3vG/l1dXYrH40kDADD0pTyAPv74Y/X09Cg/Pz/p8fz8fLW0tJyxf2VlpSKRSGJwBxwAXB7M74Jbs2aNYrFYYjQ1NVm3BADoByn/PaDc3FwNGzZMra2tSY+3trYqGo2esX84HFY4HE51GwCAAS7lV0Dp6emaM2eOqqqqEo/19vaqqqpKpaWlqT4cAGCQ6pOVEFavXq3ly5frG9/4hubOnatnnnlGHR0d+v73v98XhwMADEJ9EkB33HGHPvroIz3++ONqaWnRV7/6VW3fvv2MGxMAAJevkHPOWTfxRfF4XJFIxLoNAMAlisViysrKOud287vgAACXJwIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCYIIAAACYIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCYIIAAACYIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCYIIAAACYIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCYIIAAACYIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJhIeQA98cQTCoVCSWP69OmpPgwAYJAb3hef9Nprr9Ubb7zxv4MM75PDAAAGsT5JhuHDhysajfbFpwYADBF98h7QwYMHVVhYqMmTJ+vuu+/W4cOHz7lvV1eX4vF40gAADH0pD6CSkhJt2LBB27dv13PPPafGxkbddNNNOn78+Fn3r6ysVCQSSYyioqJUtwQAGIBCzjnXlwc4duyYJk2apKefflr33HPPGdu7urrU1dWV+DgejxNCADAExGIxZWVlnXN7n98dkJ2drauvvloNDQ1n3R4OhxUOh/u6DQDAANPnvwfU3t6uQ4cOqaCgoK8PBQAYRFIeQA8//LBqamr03//+V//85z+1dOlSDRs2THfddVeqDwUAGMRS/hLcBx98oLvuuktHjx7V+PHjdeONN6qurk7jx49P9aEAAINYn9+E4CsejysSiVi3AQC4RBe6CYG14AAAJgggAIAJAggAYIIAAgCYIIAAACYIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCYIIAAACYIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAICJ4dYNAIPd1KlTvWsyMjK8aw4cOOBd05+GD/d/Ojl16lQfdHKmtLRgP2v39vamuBN8EVdAAAATBBAAwAQBBAAwQQABAEwQQAAAEwQQAMAEAQQAMEEAAQBMEEAAABMEEADABAEEADBBAAEATLAYKXCJPv30U++aN99807vmgQce8K6pqanxrulP4XDYu6arq6sPOoEFroAAACYIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCYYDFS4BJ1d3d714wdO9a75gc/+IF3TdCFO+vq6rxrTp065V3T29vrXZOW5v9zc5DjDHRFRUWB6pqbm71rgnxvLwZXQAAAEwQQAMCEdwDt3LlTt956qwoLCxUKhbRly5ak7c45Pf744yooKNDIkSNVVlamgwcPpqpfAMAQ4R1AHR0dmj17ttavX3/W7evWrdOzzz6r559/Xrt27dLo0aNVXl6uzs7OS24WADB0eN+EsHjxYi1evPis25xzeuaZZ/Tzn/9ct912myTpxRdfVH5+vrZs2aI777zz0roFAAwZKX0PqLGxUS0tLSorK0s8FolEVFJSotra2rPWdHV1KR6PJw0AwNCX0gBqaWmRJOXn5yc9np+fn9j2ZZWVlYpEIokR9NZCAMDgYn4X3Jo1axSLxRKjqanJuiUAQD9IaQBFo1FJUmtra9Ljra2tiW1fFg6HlZWVlTQAAENfSgOouLhY0WhUVVVVicfi8bh27dql0tLSVB4KADDIed8F197eroaGhsTHjY2N2rdvn3JycjRx4kQ9+OCD+uUvf6mrrrpKxcXFeuyxx1RYWKglS5aksm8AwCDnHUC7d+/WzTffnPh49erVkqTly5drw4YNevTRR9XR0aH77rtPx44d04033qjt27crIyMjdV0DAAa9kHPOWTfxRfF4XJFIxLoNDHLXX399oLry8nLvmn/961/eNStWrOiX4xw9etS7RpKqq6u9a/bv3x/oWJAmT57sXfPDH/4w0LE2bdrkXbNv375Ax4rFYud9X9/8LjgAwOWJAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCYIIAAACYIIACACQIIAGDC+88xYGAL8hdl29vbAx1r2bJl/XKsICtU792717tGktLS/H8mmzNnjnfNK6+84l1z6tQp75qg5s+f710zd+5c75o//OEP3jUDXZBzqKyszLtm1KhR3jWSNHPmTO+aoKthXwhXQAAAEwQQAMAEAQQAMEEAAQBMEEAAABMEEADABAEEADBBAAEATBBAAAATBBAAwAQBBAAwQQABAEyEnHPOuokvisfjikQi1m0MWk899ZR3zXvvvRfoWBMmTPCuOXjwoHdNc3Ozd01mZqZ3jSR1dHR41+Tm5vZLTTQa9a658sorvWsk6cCBA941Y8aM8a4J8n99w4YN3jVBF9MMh8PeNUVFRd41t9xyi3dNLBbzrpGkEydOeNfU1dV57d/b26sPP/xQsVjsvAskcwUEADBBAAEATBBAAAATBBAAwAQBBAAwQQABAEwQQAAAEwQQAMAEAQQAMEEAAQBMEEAAABMEEADAxIBdjDQUCikUCl103dixY72PFWShQen0Qnv9UfPNb37Tu6a9vd27ZtSoUd41kvTJJ5941wRZqDE9Pd27ZsSIEd41UrDzKMj3dty4cd41Qb6mjIwM7xpJmjRpknfN+++/711z6NAh75qvfOUr3jVBFuCUpHfeece7pqCgwLtm6dKl3jWffvqpd40kbdu2zbvGd+HTkydP6sUXX2QxUgDAwEQAAQBMEEAAABMEEADABAEEADBBAAEATBBAAAATBBAAwAQBBAAwQQABAEwQQAAAEwQQAMDEgF2MNBqNKi3t4vOxsLDQ+1jFxcXeNZLU1tbmXZObm+td4/P1fy4ej3vXRKNR7xop2OKYXV1d3jXXXHONd03QhRqHDx/uXRPkPAqyaGyQBUy7u7u9a6Rg83f99dd711x11VXeNTt27PCuCbrg7rRp07xrpk+f7l3z8ccfe9ccOHDAu0YKdk74/l/v6OjQd77zHRYjBQAMTAQQAMCEdwDt3LlTt956qwoLCxUKhbRly5ak7StWrEj8LZ/Px6JFi1LVLwBgiPAOoI6ODs2ePVvr168/5z6LFi1Sc3NzYmzatOmSmgQADD3e77guXrxYixcvPu8+4XA48BvbAIDLQ5+8B1RdXa28vDxNmzZN999/v44ePXrOfbu6uhSPx5MGAGDoS3kALVq0SC+++KKqqqr061//WjU1NVq8eLF6enrOun9lZaUikUhiFBUVpbolAMAA5P9LDxdw5513Jv49c+ZMzZo1S1OmTFF1dbUWLFhwxv5r1qzR6tWrEx/H43FCCAAuA31+G/bkyZOVm5urhoaGs24Ph8PKyspKGgCAoa/PA+iDDz7Q0aNHVVBQ0NeHAgAMIt4vwbW3tyddzTQ2Nmrfvn3KyclRTk6OnnzySS1btkzRaFSHDh3So48+qqlTp6q8vDyljQMABjfvANq9e7duvvnmxMefv3+zfPlyPffcc9q/f7/++Mc/6tixYyosLNTChQv11FNPKRwOp65rAMCgN2AXI73iiiu8FuMcPXq097GCviyYn5/vXRNkIckgt6SPHTvWuyboDwexWMy7JiMjw7umP394CbJobJA5D7pIqK8gi1xKwc7xTz75xLsmEol413zta1/rl+NIwRYxDbKgbV1dnXdNkMWAJQW6yevUqVNe+7e3t2vBggUsRgoAGJgIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCYIIAAACZS/ie5U2XkyJEaNmzYRe/f0dHhfYz6+nrvGkn69NNPvWuCrJg8ceJE75ogfOb5i6ZMmeJdE2R14ezsbO+aIKtaS8H66+3t9a4JsmJye3u7d03QFd9HjhzpXTN16lTvmra2Nu+aDz/80LsmqL/97W/eNZ2dnd41QZ4furq6vGsk6b333vOu+etf/+q1/8Wuns0VEADABAEEADBBAAEATBBAAAATBBAAwAQBBAAwQQABAEwQQAAAEwQQAMAEAQQAMEEAAQBMEEAAABMh55yzbuKL4vG4IpGI0tPTFQqFLrpuzJgx3scKsvBkUN3d3f1SE2RhzCALT0rB5i/IIpyjR4/2rgn6NY0YMcK7JsicZ2RkeNccP37cuyZIb0EFWYTzs88+864JMg8XuzjmlwX5PxhET0+Pd82JEycCHSvI4sO+/Tnn1NPTo1gspqysrHPuxxUQAMAEAQQAMEEAAQBMEEAAABMEEADABAEEADBBAAEATBBAAAATBBAAwAQBBAAwQQABAEwQQAAAE/4rQ/aTkydPeu3f1dXlfYwgNVKwRTiDLJaalub/80GQxSeDLIQoSe3t7d41QRZ3bG1t7ZfjXEqdryDnUJDegn5vgyxYGWQh1yA1Qb6moN/XIIvGhsNh75og8xBUkOcV3/O1p6dH//73vy/ci3cnAACkAAEEADBBAAEATBBAAAATBBAAwAQBBAAwQQABAEwQQAAAEwQQAMAEAQQAMEEAAQBMEEAAABMDdjHS/hBkMc2gdW1tbd41QRYNDLKoYZDjSFJubq53TZCFGoMsjJmenu5dI0mnTp3yrgmy0OXIkSO9a4II8vVIwRbhDKK/FlgNskhv0GMF+T84fHj/PRUHOSd8n78udr65AgIAmCCAAAAmvAKosrJS1113nTIzM5WXl6clS5aovr4+aZ/Ozk5VVFRo3LhxGjNmjJYtWxbo77kAAIY2rwCqqalRRUWF6urq9Prrr6u7u1sLFy5UR0dHYp+HHnpIr732ml599VXV1NToyJEjuv3221PeOABgcAs551zQ4o8++kh5eXmqqanRvHnzFIvFNH78eG3cuFHf/e53JUnvvvuurrnmGtXW1ur666+/4OeMx+OKRCJBWxpShuJNCEGOxU0IwXETwmnchPA/Qc4J3xuvent71dbWplgspqysrHPud0nvAcViMUlSTk6OJGnPnj3q7u5WWVlZYp/p06dr4sSJqq2tPevn6OrqUjweTxoAgKEvcAD19vbqwQcf1A033KAZM2ZIklpaWpSenq7s7OykffPz89XS0nLWz1NZWalIJJIYRUVFQVsCAAwigQOooqJCBw4c0Msvv3xJDaxZs0axWCwxmpqaLunzAQAGh0AvPK5atUrbtm3Tzp07NWHChMTj0WhUJ0+e1LFjx5KuglpbWxWNRs/6ucLhcKBfTgQADG5eV0DOOa1atUqbN2/Wjh07VFxcnLR9zpw5GjFihKqqqhKP1dfX6/DhwyotLU1NxwCAIcHrCqiiokIbN27U1q1blZmZmXhfJxKJaOTIkYpEIrrnnnu0evVq5eTkKCsrSw888IBKS0sv6g44AMDlwyuAnnvuOUnS/Pnzkx5/4YUXtGLFCknSb37zG6WlpWnZsmXq6upSeXm5fve736WkWQDA0HFJvwfUF/g9IAAYGvr094AAAAiKAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCYIIAAACYIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCYIIAAACYIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCYIIAAACYIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCYIIAAACYIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJrwCqLKyUtddd50yMzOVl5enJUuWqL6+Pmmf+fPnKxQKJY2VK1emtGkAwODnFUA1NTWqqKhQXV2dXn/9dXV3d2vhwoXq6OhI2u/ee+9Vc3NzYqxbty6lTQMABr/hPjtv37496eMNGzYoLy9Pe/bs0bx58xKPjxo1StFoNDUdAgCGpEt6DygWi0mScnJykh5/6aWXlJubqxkzZmjNmjU6ceLEOT9HV1eX4vF40gAAXAZcQD09Pe7b3/62u+GGG5Ie//3vf++2b9/u9u/f7/70pz+5K664wi1duvScn2ft2rVOEoPBYDCG2IjFYufNkcABtHLlSjdp0iTX1NR03v2qqqqcJNfQ0HDW7Z2dnS4WiyVGU1OT+aQxGAwG49LHhQLI6z2gz61atUrbtm3Tzp07NWHChPPuW1JSIklqaGjQlClTztgeDocVDoeDtAEAGMS8Asg5pwceeECbN29WdXW1iouLL1izb98+SVJBQUGgBgEAQ5NXAFVUVGjjxo3aunWrMjMz1dLSIkmKRCIaOXKkDh06pI0bN+qWW27RuHHjtH//fj300EOaN2+eZs2a1SdfAABgkPJ530fneJ3vhRdecM45d/jwYTdv3jyXk5PjwuGwmzp1qnvkkUcu+DrgF8ViMfPXLRkMBoNx6eNCz/2h/x8sA0Y8HlckErFuAwBwiWKxmLKyss65nbXgAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCYIIAAACYIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCYIIAAACYIIACACQIIAGCCAAIAmCCAAAAmBlwAOeesWwAApMCFns8HXAAdP37cugUAQApc6Pk85AbYJUdvb6+OHDmizMxMhUKhpG3xeFxFRUVqampSVlaWUYf2mIfTmIfTmIfTmIfTBsI8OOd0/PhxFRYWKi3t3Nc5w/uxp4uSlpamCRMmnHefrKysy/oE+xzzcBrzcBrzcBrzcJr1PEQikQvuM+BeggMAXB4IIACAiUEVQOFwWGvXrlU4HLZuxRTzcBrzcBrzcBrzcNpgmocBdxMCAODyMKiugAAAQwcBBAAwQQABAEwQQAAAE4MmgNavX68rr7xSGRkZKikp0VtvvWXdUr974oknFAqFksb06dOt2+pzO3fu1K233qrCwkKFQiFt2bIlabtzTo8//rgKCgo0cuRIlZWV6eDBgzbN9qELzcOKFSvOOD8WLVpk02wfqays1HXXXafMzEzl5eVpyZIlqq+vT9qns7NTFRUVGjdunMaMGaNly5aptbXVqOO+cTHzMH/+/DPOh5UrVxp1fHaDIoBeeeUVrV69WmvXrtXbb7+t2bNnq7y8XG1tbdat9btrr71Wzc3NifH3v//duqU+19HRodmzZ2v9+vVn3b5u3To9++yzev7557Vr1y6NHj1a5eXl6uzs7OdO+9aF5kGSFi1alHR+bNq0qR877Hs1NTWqqKhQXV2dXn/9dXV3d2vhwoXq6OhI7PPQQw/ptdde06uvvqqamhodOXJEt99+u2HXqXcx8yBJ9957b9L5sG7dOqOOz8ENAnPnznUVFRWJj3t6elxhYaGrrKw07Kr/rV271s2ePdu6DVOS3ObNmxMf9/b2umg06v7v//4v8dixY8dcOBx2mzZtMuiwf3x5Hpxzbvny5e62224z6cdKW1ubk+Rqamqcc6e/9yNGjHCvvvpqYp///Oc/TpKrra21arPPfXkenHPuW9/6lvvxj39s19RFGPBXQCdPntSePXtUVlaWeCwtLU1lZWWqra017MzGwYMHVVhYqMmTJ+vuu+/W4cOHrVsy1djYqJaWlqTzIxKJqKSk5LI8P6qrq5WXl6dp06bp/vvv19GjR61b6lOxWEySlJOTI0nas2ePuru7k86H6dOna+LEiUP6fPjyPHzupZdeUm5urmbMmKE1a9boxIkTFu2d04BbjPTLPv74Y/X09Cg/Pz/p8fz8fL377rtGXdkoKSnRhg0bNG3aNDU3N+vJJ5/UTTfdpAMHDigzM9O6PRMtLS2SdNbz4/Ntl4tFixbp9ttvV3FxsQ4dOqSf/exnWrx4sWprazVs2DDr9lKut7dXDz74oG644QbNmDFD0unzIT09XdnZ2Un7DuXz4WzzIEnf+973NGnSJBUWFmr//v366U9/qvr6ev3lL38x7DbZgA8g/M/ixYsT/541a5ZKSko0adIk/fnPf9Y999xj2BkGgjvvvDPx75kzZ2rWrFmaMmWKqqurtWDBAsPO+kZFRYUOHDhwWbwPej7nmof77rsv8e+ZM2eqoKBACxYs0KFDhzRlypT+bvOsBvxLcLm5uRo2bNgZd7G0trYqGo0adTUwZGdn6+qrr1ZDQ4N1K2Y+Pwc4P840efJk5ebmDsnzY9WqVdq2bZvefPPNpD/fEo1GdfLkSR07dixp/6F6PpxrHs6mpKREkgbU+TDgAyg9PV1z5sxRVVVV4rHe3l5VVVWptLTUsDN77e3tOnTokAoKCqxbMVNcXKxoNJp0fsTjce3ateuyPz8++OADHT16dEidH845rVq1Sps3b9aOHTtUXFyctH3OnDkaMWJE0vlQX1+vw4cPD6nz4ULzcDb79u2TpIF1PljfBXExXn75ZRcOh92GDRvcO++84+677z6XnZ3tWlparFvrVz/5yU9cdXW1a2xsdP/4xz9cWVmZy83NdW1tbdat9anjx4+7vXv3ur179zpJ7umnn3Z79+5177//vnPOuV/96lcuOzvbbd261e3fv9/ddtttrri42H322WfGnafW+ebh+PHj7uGHH3a1tbWusbHRvfHGG+7rX/+6u+qqq1xnZ6d16ylz//33u0gk4qqrq11zc3NinDhxIrHPypUr3cSJE92OHTvc7t27XWlpqSstLTXsOvUuNA8NDQ3uF7/4hdu9e7drbGx0W7dudZMnT3bz5s0z7jzZoAgg55z77W9/6yZOnOjS09Pd3LlzXV1dnXVL/e6OO+5wBQUFLj093V1xxRXujjvucA0NDdZt9bk333zTSTpjLF++3Dl3+lbsxx57zOXn57twOOwWLFjg6uvrbZvuA+ebhxMnTriFCxe68ePHuxEjRrhJkya5e++9d8j9kHa2r1+Se+GFFxL7fPbZZ+5HP/qRGzt2rBs1apRbunSpa25utmu6D1xoHg4fPuzmzZvncnJyXDgcdlOnTnWPPPKIi8Vito1/CX+OAQBgYsC/BwQAGJoIIACACQIIAGCCAAIAmCCAAAAmCCAAgAkCCABgggACAJgggAAAJgggAIAJAggAYIIAAgCY+H/886fbPE6KqwAAAABJRU5ErkJggg==\n",
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"from pyrat_api import read_images, local_robustness\n",
"import matplotlib.pyplot as plt\n",
"%matplotlib inline\n",
"\n",
"images = read_images()\n",
"image_0, label_0 = images[0]\n",
"print(f\"Image shape: {image_0.shape}, label: {label_0}\")\n",
"plt.imshow(image_0, cmap='gray')\n",
"\n",
"res, elapsed = local_robustness(model_path=\"fmnist/baseline.onnx\", image=image_0, label=label_0, pert=1/255, domains=[\"zono\"])\n",
"print(f\"Robust: {res}, Time: {elapsed}\")"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now its your turn create a function that analyse all the given images for a given network and a given perturbation and returns a robustness score including safe images, unknown images and unsafe images as well as a mean time for the analysis."
]
},
{
"cell_type": "code",
"execution_count": 85,
"metadata": {},
"outputs": [
{
"ename": "NotImplementedError",
"evalue": "",
"output_type": "error",
"traceback": [
"\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
"\u001b[0;31mNotImplementedError\u001b[0m Traceback (most recent call last)",
"Cell \u001b[0;32mIn[85], line 4\u001b[0m\n\u001b[1;32m 1\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21mrobustness\u001b[39m(images, model_path, pert):\n\u001b[1;32m 2\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mNotImplementedError\u001b[39;00m\n\u001b[0;32m----> 4\u001b[0m \u001b[43mrobustness\u001b[49m\u001b[43m(\u001b[49m\u001b[43mimages\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[38;5;124;43mfmnist/baseline.onnx\u001b[39;49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;241;43m1\u001b[39;49m\u001b[38;5;241;43m/\u001b[39;49m\u001b[38;5;241;43m255\u001b[39;49m\u001b[43m)\u001b[49m \u001b[38;5;66;03m# should return [1, 48, 1]\u001b[39;00m\n",
"Cell \u001b[0;32mIn[85], line 2\u001b[0m, in \u001b[0;36mrobustness\u001b[0;34m(images, model_path, pert)\u001b[0m\n\u001b[1;32m 1\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21mrobustness\u001b[39m(images, model_path, pert):\n\u001b[0;32m----> 2\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mNotImplementedError\u001b[39;00m\n",
"\u001b[0;31mNotImplementedError\u001b[0m: "
]
}
],
"source": [
"def robustness(images, model_path, pert):\n",
" raise NotImplementedError\n",
" \n",
"robustness(images, \"fmnist/baseline.onnx\", 1/255) # should return [1, 48, 1]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"With these results you can now try and plot the results to show the evolution in function of the level of intensity for the perturbation. We aim to see if a model is more robust than another to what could be adversarial perturbation. You can use matplotlib to plot these results. "
]
},
{
"cell_type": "code",
"execution_count": 86,
"metadata": {},
"outputs": [],
"source": [
"def plot_robustness():\n",
" raise NotImplementedError"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### Step 2: Metamorphic testing\n",
"\n",
"We checked with the engineer in charge of taking pictures of the clothes on the condition in which he takes pictures. After a careful investigation we realised that the following issues might be happening in our picture:\n",
"- Luminosity of the setting varies from -30 to +30\n",
"- Angle of the clothes might vary from -15° to + 15°\n",
"- Picture can be blurry \n",
"\n",
"In that sense, to test the robustness of our model we will proceed to see if it is sensitive to these perturbations. Following the examples [here](https://opencv-tutorial.readthedocs.io/en/latest/trans/transform.html) use opencv library to implement transformation on the images. You can visualise the image with matplotlib."
]
},
{
"cell_type": "code",
"execution_count": 87,
"metadata": {},
"outputs": [
{
"ename": "NotImplementedError",
"evalue": "",
"output_type": "error",
"traceback": [
"\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
"\u001b[0;31mNotImplementedError\u001b[0m Traceback (most recent call last)",
"Cell \u001b[0;32mIn[87], line 10\u001b[0m\n\u001b[1;32m 7\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21mblur\u001b[39m(image, intensity):\n\u001b[1;32m 8\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mNotImplementedError\u001b[39;00m\n\u001b[0;32m---> 10\u001b[0m plt\u001b[38;5;241m.\u001b[39mimshow(\u001b[43mblur\u001b[49m\u001b[43m(\u001b[49m\u001b[43mimage_0\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;241;43m15\u001b[39;49m\u001b[43m)\u001b[49m)\n",
"Cell \u001b[0;32mIn[87], line 8\u001b[0m, in \u001b[0;36mblur\u001b[0;34m(image, intensity)\u001b[0m\n\u001b[1;32m 7\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21mblur\u001b[39m(image, intensity):\n\u001b[0;32m----> 8\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mNotImplementedError\u001b[39;00m\n",
"\u001b[0;31mNotImplementedError\u001b[0m: "
]
}
],
"source": [
"def luminosity(image, intensity):\n",
" raise NotImplementedError\n",
" \n",
"def rotation(image, angle):\n",
" raise NotImplementedError\n",
"\n",
"def blur(image, intensity):\n",
" raise NotImplementedError\n",
" \n",
"plt.imshow(blur(image_0, 15))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"To apply these transformation and compute the stability of a network towards we will use a tool developed at CEA called AIMOS which does exactly that.\n",
"\n",
"After installing the aimos module (which is provided locally), the function below will call aimos on your transformation and a specified range before plotting the result."
]
},
{
"cell_type": "code",
"execution_count": 88,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Processing ./bin/aimos_compile\n",
"Building wheels for collected packages: AIMOS\n",
" Building wheel for AIMOS (setup.py) ... \u001b[?25ldone\n",
"\u001b[?25h Created wheel for AIMOS: filename=AIMOS-1.0-py3-none-any.whl size=27865 sha256=b6149cb0febece22984ce1e9319ee6cb64109d5fac6dca16f576ffb60d8673fa\n",
" Stored in directory: /tmp/pip-ephem-wheel-cache-mr8hxog1/wheels/70/50/9d/c65b449093c72794e4464fe38d49de849130fb6a47de22aede\n",
"Successfully built AIMOS\n",
"Installing collected packages: AIMOS\n",
"Successfully installed AIMOS-1.0\n",
"\u001b[33mWARNING: You are using pip version 20.3.3; however, version 22.3.1 is available.\n",
"You should consider upgrading via the '/home/NEMO18/.virtualenvs/tuto_seti/bin/python -m pip install --upgrade pip' command.\u001b[0m\n"
]
}
],
"source": [
"!pip install ./bin/aimos_compile\n",
"from aimos import core"
]
},
{
"cell_type": "code",
"execution_count": 89,
"metadata": {
"scrolled": false
},
"outputs": [
{
"ename": "NotImplementedError",
"evalue": "",
"output_type": "error",
"traceback": [
"\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
"\u001b[0;31mNotImplementedError\u001b[0m Traceback (most recent call last)",
"Cell \u001b[0;32mIn[89], line 24\u001b[0m\n\u001b[1;32m 12\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m y\n\u001b[1;32m 14\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m core\u001b[38;5;241m.\u001b[39mmain(\n\u001b[1;32m 15\u001b[0m \u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mfmnist/images/\u001b[39m\u001b[38;5;124m\"\u001b[39m,\n\u001b[1;32m 16\u001b[0m \u001b[38;5;124m\"\u001b[39m\u001b[38;5;124mfmnist/\u001b[39m\u001b[38;5;124m\"\u001b[39m,\n\u001b[0;32m (...)\u001b[0m\n\u001b[1;32m 21\u001b[0m verbose\u001b[38;5;241m=\u001b[39m\u001b[38;5;28;01mFalse\u001b[39;00m,\n\u001b[1;32m 22\u001b[0m )\n\u001b[0;32m---> 24\u001b[0m res \u001b[38;5;241m=\u001b[39m \u001b[43mcall_aimos\u001b[49m\u001b[43m(\u001b[49m\u001b[43mluminosity\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;28;43mrange\u001b[39;49m\u001b[43m(\u001b[49m\u001b[38;5;241;43m0\u001b[39;49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[38;5;241;43m10\u001b[39;49m\u001b[43m)\u001b[49m\u001b[43m)\u001b[49m\n",
"Cell \u001b[0;32mIn[89], line 14\u001b[0m, in \u001b[0;36mcall_aimos\u001b[0;34m(transformation, value_range)\u001b[0m\n\u001b[1;32m 11\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21midentity\u001b[39m(y):\n\u001b[1;32m 12\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m y\n\u001b[0;32m---> 14\u001b[0m \u001b[38;5;28;01mreturn\u001b[39;00m \u001b[43mcore\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mmain\u001b[49m\u001b[43m(\u001b[49m\n\u001b[1;32m 15\u001b[0m \u001b[43m \u001b[49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[38;5;124;43mfmnist/images/\u001b[39;49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[43m,\u001b[49m\n\u001b[1;32m 16\u001b[0m \u001b[43m \u001b[49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[38;5;124;43mfmnist/\u001b[39;49m\u001b[38;5;124;43m\"\u001b[39;49m\u001b[43m,\u001b[49m\n\u001b[1;32m 17\u001b[0m \u001b[43m \u001b[49m\u001b[43m(\u001b[49m\u001b[43mtransformation\u001b[49m\u001b[43m,\u001b[49m\u001b[43m \u001b[49m\u001b[43midentity\u001b[49m\u001b[43m)\u001b[49m\u001b[43m,\u001b[49m\n\u001b[1;32m 18\u001b[0m \u001b[43m \u001b[49m\u001b[43mcustom_load\u001b[49m\u001b[38;5;241;43m=\u001b[39;49m\u001b[43mload_image\u001b[49m\u001b[43m,\u001b[49m\n\u001b[1;32m 19\u001b[0m \u001b[43m \u001b[49m\u001b[43mfn_range\u001b[49m\u001b[38;5;241;43m=\u001b[39;49m\u001b[43mvalue_range\u001b[49m\u001b[43m,\u001b[49m\n\u001b[1;32m 20\u001b[0m \u001b[43m \u001b[49m\u001b[43msingle_plot\u001b[49m\u001b[38;5;241;43m=\u001b[39;49m\u001b[38;5;28;43;01mTrue\u001b[39;49;00m\u001b[43m,\u001b[49m\n\u001b[1;32m 21\u001b[0m \u001b[43m \u001b[49m\u001b[43mverbose\u001b[49m\u001b[38;5;241;43m=\u001b[39;49m\u001b[38;5;28;43;01mFalse\u001b[39;49;00m\u001b[43m,\u001b[49m\n\u001b[1;32m 22\u001b[0m \u001b[43m \u001b[49m\u001b[43m)\u001b[49m\n",
"File \u001b[0;32m.\\aimos\\core.py:408\u001b[0m, in \u001b[0;36mmain\u001b[0;34m(inputs_path, models_path, transformation, alt_predict, custom_predict, custom_load, custom_global_load, fn_range, out_mode, per_input, custom_comparison, single_plot, save_single_fig, verbose, individual_load, export_path)\u001b[0m\n",
"File \u001b[0;32m.\\aimos\\core.py:254\u001b[0m, in \u001b[0;36m_loop_over_inputs\u001b[0;34m(inputs, inputs_name, model, predict_fn, alt_predict_fn, out_mode, custom_comparison, transform, transformation, per_input, range_value, verbose, custom_load, individual_load, export_path)\u001b[0m\n",
"File \u001b[0;32m.\\aimos\\core.py:169\u001b[0m, in \u001b[0;36mcompute_results\u001b[0;34m(transformation, input_ori, predict_fn, alt_predict_fn, out_mode, comparison_fn, export_path)\u001b[0m\n",
"File \u001b[0;32mC:\\Users\\AL253370\\Documents\\Projets\\AIMOS\\git_aimos\\aimos\\core_functions.py:138\u001b[0m, in \u001b[0;36m\u001b[0;34m(x)\u001b[0m\n",
"Cell \u001b[0;32mIn[87], line 2\u001b[0m, in \u001b[0;36mluminosity\u001b[0;34m(image, intensity)\u001b[0m\n\u001b[1;32m 1\u001b[0m \u001b[38;5;28;01mdef\u001b[39;00m \u001b[38;5;21mluminosity\u001b[39m(image, intensity):\n\u001b[0;32m----> 2\u001b[0m \u001b[38;5;28;01mraise\u001b[39;00m \u001b[38;5;167;01mNotImplementedError\u001b[39;00m\n",
"\u001b[0;31mNotImplementedError\u001b[0m: "
]
}
],
"source": [
"import numpy as np\n",
"import cv2\n",
"\n",
"%matplotlib inline\n",
"\n",
"\n",
"def load_image(path):\n",
" return np.load(str(path)).astype(np.float32).reshape((1, 28, 28))\n",
"\n",
"def call_aimos(transformation, value_range):\n",
" def identity(y):\n",
" return y\n",
" \n",
" return core.main(\n",
" \"fmnist/images/\",\n",
" \"fmnist/\",\n",
" (transformation, identity),\n",
" custom_load=load_image,\n",
" fn_range=value_range,\n",
" single_plot=True,\n",
" verbose=False,\n",
" )\n",
"\n",
"res = call_aimos(luminosity, range(0, 10))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"At this point, you can run the above function on the different transformations that we want to test to see the different responses from the models. \n",
"\n",
"**What do you notice?**\n",
"\n",
"### Step 3: Choose a model\n",
"\n",
"**With all of these results, what model would you choose, why?**\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.9.1"
}
},
"nbformat": 4,
"nbformat_minor": 4
}
\n",
" 
\n",
"