demo.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "%matplotlib inline\n",
    "import sys\n",
    "sys.path.insert(0, 'src')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "import stlcg\n",
    "import stlviz as viz\n",
    "from stlcg import Expression\n",
    "from utils import print_learning_progress"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "import torch\n",
    "import numpy as np\n",
    "import matplotlib.pyplot as plt\n",
    "import importlib"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Create traces from numpy arrays"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "t = t = np.arange(-3, 3, 0.2, dtype=np.float32)\n",
    "x_np = 0.5 * np.exp(-t**2).reshape([1, t.shape[0], 1])\n",
    "w_np = (0.4*np.exp(-(t + 0.5)**2) + 0.2*np.exp(-(t - 3)**2)).reshape([1, t.shape[0], 1])\n",
    "\n",
    "x = torch.tensor(x_np, requires_grad=False)\n",
    "w = torch.tensor(w_np, requires_grad=False)\n",
    "c = torch.tensor(1.0, dtype=torch.float, requires_grad=True)\n",
    "d = torch.tensor(0.9, dtype=torch.float, requires_grad=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Text(0.5, 1.0, 'Traces')"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    },
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAecAAAFBCAYAAABNSGenAAAABHNCSVQICAgIfAhkiAAAAAlwSFlzAAALEgAACxIB0t1+/AAAADl0RVh0U29mdHdhcmUAbWF0cGxvdGxpYiB2ZXJzaW9uIDMuMC4wLCBodHRwOi8vbWF0cGxvdGxpYi5vcmcvqOYd8AAAIABJREFUeJzs3Xl8VNX5+PHPmclCEgiEhLCEBCIgCrKFTUE2FauiuO8rtrj061a629a29lt/trW2av1SxYr7XhcUXFDQICgEwr4vgYRACIFAQvZkzu+PO8mdhEzIMjP3zszzfr18ec+dmXuekMw8c849i9JaI4QQQgj7cFgdgBBCCCEak+QshBBC2IwkZyGEEMJmJDkLIYQQNiPJWQghhLAZSc5CCCGEzURYHYAQwqCUas28xn1a6/7+jkUIYS1JzkLYxzlNyh8A64E/eJyrClg0QgjLSHIWwia01t97lpVSVUBR0/PeKKWitdaSvIUIAXLPWYggpJR6Sym1Syk1WSn1vVKqAnjU/dhtSqlvlFKHlVKlSqk1SqmbmrlGpFLqt0qpbUqpKvfzFyqlBng8p6dSap5S6qD7OVuUUrOaXCdFKfW6x3MOKKUWKKUS/P4PIUSIkpazEMErCXgV+AuwBShzn08H3gJ2ucvTgFeVUlFa65cAlFIKeB/4AfAksBSIBaYCvYDd7uT6nfsavwVygRnAf5RSEVrree7H3gISgTlAvvv104FOPv+JhQgTStbWFsKelFJ7gW+11rc089hbwPXARVrrz1u4hgOjh2w+cLrWerz7/CXAQuBurfXzXl77Z+AhYKjWeq/H+VeB84G+gMa4D36ft+sIIdpOurWFCF7lzSVmpdQZSql3lFIHgFqgBrgFGOzxtAvdj73YwvUvAr4F9iulIur/Az4HegMDtfHtfg3wsFLqPqXUUJ/8ZEKEOUnOQgSvgqYnlFLdgC+BM4CfA+cCY4HXadzNnAgc0lrXtnD9ZIwkXtPkv1c9rgFwJfAZ8Btgk1Jqv1Lq1+6ucyFEO8g9ZyGCV3P3pCYBKcAVWuvV9SeVUpFNnlcE9HTfO/aWoI9g3Lf+uZfHtwForQuAe4B7lFJDgFnAYxhfHua38mcRQniQlrMQoSXW/f+a+hNKqWTgkibP+wLjy/ksvPsMOBPYo7Ve3cx/J5q+QGu9RWv9c6AcOKsjP4gQ4UxazkKElmUYo7afU0o9CsQDjwCHMAZw1fsM+AT4l1IqHfgao9t7KvCe1noF8FfgGuBbpdQ/gR1AF4yEPV5rfbVSqifwEfAGsB2oc78mBljs159UiBAmyVmIEKK1PqCUuhojsf4X2I8xVaofxsjr+udp9/N+jTFY7GfAMWAlRiJHa31UKTUe+D3G/eTeQDFGd/bb7kudADZidGunYSTnrcD1WuvP/PrDChHCZCqVEEIIYTNyz1kIIYSwGUnOQgghhM1IchZCCCFsRpKzEEIIYTOSnIUQQgibsWwqVVJSku7fv79V1QshhBABtWbNmiKtdY/WPNey5Ny/f39Wr1596icKIYQQIUApta+1z5VubSGEEMJmJDkLIYQQNiPJWQghhLAZSc5CCCGEzUhyFkIIIWxGkrMQQghhM7JlpBCC7Nxi5i/PIaeojPSkOGZNTCcjLcHqsISNlZSUUFhYSE1NjdWhWC4yMpLk5GTi4+N9ds1WJWel1EXAU4ATeEFr/XiTx+8A/gbku0/9S2v9gs+iFEL4zZOLtzMvM4fK2jq0hi0HSvhySyGzJ6czZ/pgq8MTNlRSUsKhQ4dISUkhJiYGpZTVIVlGa01FRQX5+Ub681WCPmW3tlLKCTwLXAwMAW5USg1p5qlva61Huv+TxCxEEMjOLWZeZg4VNUZiBnBpqKipY15mDtm5xdYGKGypsLCQlJQUYmNjwzoxAyiliI2NJSUlhcLCQp9dtzX3nMcBu7TWe7TW1cBbwOU+i0AIYZn5y40Wc3OqauuYvzwnwBGJYFBTU0NMTIzVYdhKTEyMT7v4W5OcU4A8j/J+97mmrlZKbVBKvaeUSm3uQkqpu5RSq5VSqw8fPtyOcIUQvrTncFlDi7kpl4a9ReWBDUgEjXBvMTfl638PX43W/hjor7UeDiwGXm7uSVrr57XWY7TWY3r0aNXa30IIP9mUf5x9R8pafE55dS2VNc23rIUQ/tOa5JwPeLaE+2IO/AJAa31Ea13lLr4AjPZNeEIIX6utc/Hs0l1c8exyTlS1nHh3Hy7j8n8tZ8uBkgBFJ4SA1iXnLGCQUipdKRUF3AAs8HyCUqq3R3EmsNV3IQohfGVvURnXPfcdf/t8O7Uuoz87wqGIdCoc7l45pWg4Bth+qJTLn/2WuV/vps7lpQ9cCOFTp5xKpbWuVUrdB3yOMZXqRa31ZqXUo8BqrfUC4AGl1EygFjgK3OHHmIUQbaS15s1Vefzvwi2UV5ut5VFp3XjyupEUl1czf3kOe4vK6Z8Uy6wJ/dl8oIQ/L9pKZY2LmjrNXz7bxpJth/j7tSNJS4y18KcRIvQp7W00iJ+NGTNGy37OQvhfYWklv/rvRpZsM6d5RDgUD54/iHunDiDC6b0DbffhE8x5Zz3r8441nIuLcvK7S4dw/dhUGRQUprZu3cqZZ57ps+uFyiI4p/p3UUqt0VqPac21ZIUwIUJI0w+5M3rF88KyPRSXm1M8BiZ35h/XjWRY366nvN6AHp357z3n8OzS3Ty9ZCd1Lk1ZdR2/en8jX249xE3j+/HB2v1B/6EqrGP1IjhlZWWMHj2a+Ph4li9fTmRkJABffPEFF110Ec888wz/8z//4/c4mpKWsxAhoumHXHPunJjOLy4aTKdIZ5uvvz7vGD95Zx17Djce4a0AjXGfOjrCKSuLhQFftZyzc4u5ed5KKpqZERAT6eT12eMD8mVv7dq1nH322fzkJz/h8ccf59ChQ4wYMYLx48fz0Ucftfo60nIWQjTiudJXcxLjonj6xlFMHJjU7jpGpHZj4f2T+Mtn23hpxd6G8/XfAzxXFps6OFla0GGm/68W+vR6FTV1XPV/K9r12r2Pz2jT80eNGsXjjz/Oz372My644AKeeOIJnE4n//nPf9pVvy9IchYiBLS00hfA2P7dO5SY68VEOfnDzKFsKyjh+z1Hm31O/cpikpxFMHnooYdYvHgxl156KdXV1SxevJikpI6/Z9pLtowUIgTkFHlf6Qsg/1iFT+s7UVXr9TFZWUwEI6UUt956K1VVVYwYMYLzzz/f0nik5SxECEhPimPzgZJmE7RDQf8k3059Sk+KY8uBEpqb9uyP+oT9tbUrGexzzxmgoKCABx98kIyMDNauXctTTz3Fgw8+GJC6myMtZyFCwKyJ6Xib1BQd4WTWxHSf1xcd0fygsginw+f1idCUkZbA7MnpxEQ6Gxa+cSgjMc+eHLiR/1prbr/9dqKjo/nyyy956KGH+OUvf8mGDRsCUn9zpOUsRIho2or1HD3t6w+5+g/VeZk5VNXWNao7MS6KUandfFqfCF1zpg9m6uDkxovgBHhK3pNPPsmXX37JkiVLSEhI4PHHH+frr7/mxhtvZPXq1ZbswCXJWYgQ8MTn2xuOU7p1ontctN8/5Dw/VHcUlLLj0Ak0cPB4Jd/sOMzUwcl+qVeEnoy0BMsGEGZnZ/Pwww/z61//milTpgAQFRXFm2++SUZGBnPmzGHu3LkBj0uSsxBBbvmuIlbsPgKA06F47Udnk54UF5C6PT9Uf/vhRl77PheAJ77YzpTTe8gKYsL2MjIyqKqqOun84MGDKStredc2f5J7zkIEMa01f/NoNV87um/AEnNT9583iOgI4yNlU34Jn20qsCQOIUKBJGchgthXWwtZ5173Osrp4IHzB1kWS8/4Ttw+oX9D+e+Ld8guVkK0kyRnIYKUy6V54guz1Xzz2Wn06Rb4gSue7pkygM7Rxt2yXYUn+Ghd/ileIYRojiRnIYLUJxsPsq2gFDCmnvx46kCLI4LucVHcea45jeofX+6gutZlYURCBCdJzkIEodo6F/9YvKOhfOe5/enRJdrCiEw/mpROt1hjZ5+8oxW8szrP4oiECD6SnIUIQv/NNrZpBOjSKYK7Jg2wOCJTfKdI7plixvPMkp1UetmQQwjRPEnOQgSZqto6nvpyZ0P5nikD6OpuqdrF7eeYLflDJVW8+t0+iyMSIrhIchYiyLyxMpcDxysBSOocxR0eI6TtIibKyf3nmffA/+/rXZRW1lgYkRDBRZKzEEGkvLqWZ5fuaij/eOpA4qLtuZbQDWPT6JtgjB4vLq/hxW/3WhuQEEFEkrMQQWT+8r0UnagGoHfXTtw0Ps3iiLyLinDwoMe86xeW7aG4rNrCiIQIHpKchQgSxytqeO6b3Q3lB84fRKfI5neGsosrR6VwWg9jxbLSqlr+nbn7FK8QQoAkZyGCxrzMPZRU1gLQPzGWa0b3tTiiU4twOvjp9MEN5ZdX7KWwpNLCiIQIDpKchQgCRSeqeHF5TkP5J9NPJ9IZHG/fi8/qxZDe8QBU1rj4l8c9cyEAyMuC9+6E56YY/8/LsjoiywXHu1uIMPd/S3dTXm3MFT6jVxcuG97H4ohaz+FQ/PwHZuv5zVW55B0ttzAiYStLH4NXZsKm9+HgOtj8gVFe+ljAQlizZg1KKb799tuGc8888wxKKX772982nNu5cydKKRYuXOj3mCQ5C2FzB45V8NpKc57wnOmn43AE11aMUwf3YHQ/Y2vJmjrN01/tPMUrRFjIy4IVz0BNOeDeJEW7jPKKpwPWgh41ahTdunVjyZIlDeeWLFlCTEzMSeciIiKYPHmy32Oy5xwMIUSDZ5bsbFifekRqN6YP6WlxRG2nlNF6vuH57wFjhbO7pwxgYHJniyMTPvOHrr69Xk0F/OeCdsZyvE1PdzgcTJ48maVLl/LII4/gcrn45ptvuPfee3n66ac5ceIEnTt3ZunSpYwePZouXbq0L662xOT3GoQQ7ba3qIx3Vu9vKP/8wsEoFVyt5npnn5bIpEFJALi0sSmGEHZx3nnn8d1331FZWcm6des4duwYv/jFL4iOjmbZsmUALF26lGnTpgUkHmk5C2FD2bnFzF+eQ+aOww17Ip99WncmDky0OLKO+emFg1m2swiAhRsOsu3g1wzpE8+sielkpCVYHJ0IZ9OmTaOqqooVK1awdu1aRowYQc+ePTn33HNZunQpaWlpFBYWct555wUkHknOQtjMk4u3My8zh8qauvq7cACkJsQGbau53sjUbpyWFMce96Yduw+XkVNUxpdbCpk9OZ05HtOuRJBpY1cyYNxTfmWm+55zE5ExcNvHkDq247G1wrBhw0hKSmLJkiWsXbu2IQmfd955vPPOO6SmphIVFcXEiRMDEo90awthI9m5xczLzKGiSWIG+GTDQbJziy2Jy1eyc4vJP1bR6JxLQ0VNHfMyc4L+5xNtlDoWJtxvJGLlTkfKYZQnPBCwxAzGuIipU6eyePFili1b1ig5r127lg8++IBx48YRGxsbkHgkOQthI/OX51BZ2/z2ilW1dcz3mOscjOYvz6G6ztXsY6Hw84l2mPaw0UIeeiX0Hmn8/7aPjfOBDmXaNFatWkV5eTmTJk0CjJHcXbp0YenSpQHr0gbp1hbCVnKKytBNm8xuLg17i4J7fnCo/3yinVLHBrSV7E39YK8xY8YQH28snON0OpkyZQoLFiwI2GAwkOQshK2kJ8Wx5UAJrmYSmENB/6TAdKn5S6j/fCK4nXnmmehmvj1+9NFHAY9FurWFsJFZE9OJ8LIsZ3SEk1kT0wMckW/NmphOdETzm3WEws8nhK9IchbCRjLSEkhPbNx6dCiIiXQye3LwTzfKSEtg9uR0YiKdNF3k7MpRKUH/8wnhK9KtLYSNnKiqJfeoOZp5YI/OnNmnS0jNA54zfTBTBye753EXcbyiBoDOneTjSIh68m4QwkY+21RARY0xWntwzy589tCkoJ/b3JyMtAQy0hJYur2QWfON9ZM/WJvPL34w2Gu3vhDhRN4FQtjI+9nmUp1XZaSEZGL2NGlgEkmdowE4XFrF8t1HLI5ICHuQ5CyETeQfq+C7PUZyUgouH5licUT+F+F0cPlIc/tLzy8nwt6aG9Ucznz97yHJWQib+HBtfsMc4HMHJtGraydrAwqQqzLMLyGfby6gtLLGwmhEa0RGRlJRUXHqJ4aRiooKIiMjfXa9ViVnpdRFSqntSqldSqlftfC8q5VSWik1xmcRChEGtNYndWmHiyG94zmjl7EFX2WNi083FVgckTiV5ORk8vPzKS8vD/sWtNaa8vJy8vPzSU5O9tl1TzkgTCnlBJ4FpgP7gSyl1AKt9ZYmz+sCPAis9Fl0QoSJjfnH2X3Y2AwiNsrJD4b2sjiiwFFKcVVGCo8t2gbAB9n5XDcm1eKoREvqV886cOAANTXS0xEZGUnPnj0b/l18oTWjtccBu7TWewCUUm8BlwNbmjzvT8BfgJ/7LDohgl1eFqycC0d2Q+IAGH9vs8sUvp+d33B88Vm9iT20tlWvCxWXj0zh8U+34dLw3Z4j7C8up2+CrBZmZ/Hx8T5NRqKx1nRrpwB5HuX97nMNlFIZQKrWeqEPYxMiuC19zNgOb9P7cHAdbP7AKC99rNHTqmtdLFh/oKH8oPPdVr0ulPSM78S5g3o0lD9ad6CFZwsR+jo8z1kp5QCeBO5oxXPvAu4CSEtL62jVQthXXhaseKbxPrXaZZQz/wbbP4Vo4z5rWXk1c2tKIQq6OSpJ3ZRrPLfp61Y8DQOnh2wL+uqMFDJ3HAbgv9n7+fHUASE/lUwIb1qTnPMBzxtAfd3n6nUBzgK+dr+RegELlFIztdarPS+ktX4eeB5gzJgx4T2KQIS2lXOhxstoVu2Cgg0NxQRgvGcflrd3Rm2Vcd0QTc4XDulFXJSTsuo69hwuY/3+44xM7WZ1WEJYojXd2lnAIKVUulIqCrgBWFD/oNb6uNY6SWvdX2vdH/geOCkxCxFWjuzGe5ZtJ+1yXzc0xUQ5uXhY74ayzHkW4eyUyVlrXQvcB3wObAXe0VpvVko9qpSa6e8AhQhKqqW3loL0yXDHQhaPe5Hrq37H9VW/49ddHzfO00JXbnxoT7HynEL28foDVNe6Wni2EKGrVfectdaLgEVNzj3i5blTOx6WEEFs0/twINv745Gd4LxHIHUs//50BWu0sdjIxeOGQNoYY/CX571qT4c2Q/lRiO3uh8Ctd3Z6In26duLA8UqKy2v4enshF4bRtDIh6skKYUL40q4v4f27zLJSZitaOSAyBiY8AKlj2VtUxpp9xQBEOBSXjehj3E+ecL/xvIbWt0dL+theeP1aqDoRkB8n0BwOxZUerWfPKWZChBNJzkL4Su5KePtWcLkXZUg6HW56F4ZeCb1HGv+/7WOY9jAA7681E8/UwckkujeAYNrDxvPqX3fWVTD11zQk6fzV8PbNxgCxEHTlqL4Nx19tO8Sx8moLoxHCGrJlpBC+ULAJ3rjW7I7umgq3fgBd+8Kg6Sc93eVqvFzn1U2X60wde/Ko7NhEWPQz43jP1/DfH8I1L4EztN7GA5M7MyK1G+vzjlFTp/l4w0FuPbuf1WEJEVDSchaio47shlevhMrjRjmuB9z6oZGYvVi9r5j9xcZUq/hOEZx3ZivW5B03G6b91ixv/Rg+eRBCcG3jq0Z5dm3LqG0RfiQ5C9ERJQfg1SugrNAoR8fDLe9D0sAWX/bBWjPhXDqiD9ERztbVN/lncM59Znnta/DFb0MuQV82og8RDqMbf23uMXKKyiyOSIjAkuQsRHuVHzVazMdyjXJEDNz0DvQe3uLLKmvq+GTDwYbySV3aLVEKLvxfGHmLee67f8G3T7YlctvrHhfFtDPM3oQPpPUswowkZyHao+oEvH4NHDZ2UsIRAde9Av3OOeVLv9x6iNLKWgD6JcaSkZbQtrqVgsuegjMuNc999Shk/adt17E5zy8t76/Nx+UKrd4BIVoiyVmItqqtgrdugvw17hMKrnwOTr+wVS/3nB501ai+7Vs/2hkBV/8H0qeY5xb+FDa+1/Zr2dS0M5LpGmNsXr+/uIKsvUctjkiIwJHkLERr5GXBe3fCvyfDUyMh5xvzsRlPwLBrWnWZw6VVfOPe3AHgylEdWPErshPc8DqkjHaf0MYc6/mXwHNTjHjzstp/fYtFRzi5bITncp4y51mED0nOQpyK59aPBeuh1GM7w/N+B2N/1OpLLVh/gDp39+y4/t1JS+zgnsXRXeDm96DHGUZZ18G+5SGz1eRVGeaI90UbD1JZU2dhNEIEjiRnIVrSaOvHJvc8HRHutbBbz3OU9pVtGQjWktjucP7vOWlNbs+tJoO0BT0qtRvpSXEAlFbVsnjLIYsjEiIwJDkL0ZJTbf248t+tvtT2glI25ZcAEBXh4BKPHZg6bFML95rrt5oMQkqpRl3/MudZhAtJzkK0pKWtH9u4heP7Hq3m6UN6Ngx28gkfxmk3nsk5c2cRhaWVFkYjRGBIchaiJYkD8LqFo3JAYsuLjdSrc2k+9FhLu01zm1sjcYD3bSrbEKcdpXaPZVy6sQtXnUuzYN2BU7xCiOAnyVmIloy72/tjEdEw/p5WXWbF7iIOlRgbVSR1jmLSoB6+iM40/l6I6NT8Yw5nq+O0q6tlpyoRZiQ5C9GSkv2c1F3cZOvH1vBMKDNHpBDp9PFbr9mtJt2c0dBrmG/rC7CLh/UmOsL4ubYcLGFbQYnFEQnhX5KchfCmrhaW/NksJw1uduvHlmTnFvPj19Y06tK+ytdd2vU8t5rsNRycUcb56hOw+kX/1Bkg8Z0iuXBor4byLS+s5P43s8nOLbYwKiH8J7T2mhPCl9a/AUfdA6miu8IPP4eY1i+1+eTi7czLzKGypq6h7a2ALzYXcFZKV5+HCzTeanLlc/DpL4zjZX+HjFuNedFBSnn0YBSdqGbhhoN8uaWQ2ZPTmTN9sIWRCeF70nIWojk1lfD1X8zyxAfalJizc4uZl5lDhUdiBqODfN6ynMC0+EbfYewrDVBeBN+3ftqX3WTnFrN4S2Gjcy4NFTV1zMsM0L+nEAEkyVmI5qyZ777fjLE/cxsHVM1fnkNlbfOrWVXV1jF/eU5HIzy1iGiY+iuzvOJpYyetIGSLf08hAkiSsxBNVZ2AzCfM8uSfQ3TnNl0ip6jM6xbLLg17i8o7EGAbDL8Bkk43jqtKYPlTganXx2zz7ylEgEhyFqKp7+ca3cBgdAuPvqPNl0hPisPhZXq0Q0H/pA6uqd1azgiY9huzvPI5KC0ITN0+ZJt/TyECRJKzEJ7Kjxrdv/Wm/sroHm6jWRPTiYpo/u0VHeFk1sT09kbYdmfOhN4jjOPaCsj8W+Dq9pFZE9OJjnA2+1jA/z2FCABJzkJ4Wv6U0f0LkDjI6BZuh4y0BMb1797onENBTKST2ZPTyUhr/eCyDnM44LxHzPKal+BocN2jzUhLYPbkdGIinTTd/nrWxP6B/fcUIgAkOQtRr7TA6Patd95vjG7hdiqvNgcwpXSLYcbw3rw+e7w1034Gng9pE4xjVy1885eWn29Dc6YP5vXZ47l0WG+inGaGHiWJWYQgSc5C1Mt8wuj2BWMRjzMvb/elCo5XsnqfMb3H6VAsuG8iz9yYYV0LTyk4/3dmef1bULjVmlg6ICMtgWduyuCHk05rOLdo40ELIxLCPyQ5CwFQvNfo7q13/iNGd3A7eSaMc05LJLFz2+9b+1y/CTBwurugYemfW3y6nc3w2G5z8ZZDVNY0P81KiGAlyVkIMBYccdUYx2nnwMALOnQ5z+Ts032bO+q835rHWz+G/DXWxdIBQ/vE0y/RGKF9oqqWZTuLLI5ICN+S5CxE4TbY8JZZPv8RThp11AZNu7R/MLRnRyP0nT4jYcgVZvmrP1kXSwcopRp96ZGubRFqJDkLsfTPoF3G8cALjO7fDvh0k5kozj6tuz26tD1N+425c9WepZCTaW087eTZtf3llkNUeVlBTIhgJMlZhLf8bNi6wCx7dvu2k227tOv1OB1G3mSWv/oTXpffsrGhfeJJ6250bZdW1bJsh3Rti9AhyVmEtyUe3bpDLoc+ozp0uUMlZpe2Q8EPPLY5tJUpvzS3lNy/CnZ8bm087SBd2yKUSXIW4StnGexeYhwrB0zreKv5040HGxqhZ5+WSJLdurTrdUuDMXea5SV/ApfLunjaqemobenaFqFCkrMIT1o3bjWPuMno7u2gRRvNdatt2aXtadJPIdK9JvWhTbD5fWvjaYezUuJJ7R4DGF3b38qobREiJDmL8LTzC8hbaRw7ImHqLzt8ycKSSrL2GVsyOhRcdJZNu7TrdU6Gs+81yx8/AP+eBO/dCXlZ1sXVBk27thdK17YIEZKcRXjJy4J3Z8E7t5nnxtxpdPN20KebChq6tMen27hL29OE+8HpjrO6DAo2wOYP4JWZsPQxa2NrJenaFqFIkrMIH0sfM5LO5g+gttI834H1sz15ttouGW7zLu16RbvMaWT1tAtqyo3duYKgBT0spSt9E9xd25W1LN8lXdsi+ElyFuEhLwtWPGMkHZpMG1r9YoeTUGFJJVl7Pbq07TpKu6mVc42NMJpTW2U8bnNKqUat54Ubgm+/aiGakuQswsPKuVBT0fxjPkhCn202u7THpXenR5cg6NIGOLKbk76s1NMu9+P253nf+YstBVTXBt/IcyE8SXIW4cHPSeiTDWaX9ozhfTp0rYBKHGCuFtaUckDiwMDG007D+zbu2v5212GLIxKiY1qVnJVSFymltiuldimlftXM4/copTYqpdYppb5VSg3xfahCdEDiAO/rZXcwCQVtlzbA+HsholPzj0VEw/h7AhtPO0nXtgg1p0zOSikn8CxwMTAEuLGZ5PuG1nqY1nok8FfgSZ9HKkRHjL8Xr3/uHUxCQdulDZA61hixHRlzcgt6+PXG40HikkajtqVrWwS31rScxwG7tNZ7tNbVwFtAo13otdYlHsU4vPYfCmGRxAFAk5azchhJacIDHUpCCz27tO2+8Ehzpj0Mt30MQ6+ETt3M867gmpLk2bVdIqO2RZBrTXJOAfI8yvvd5xpRSv2PUmo3Rsv5Ad+EJ4SPrH0VtHtUcqeu0HukkYxu+9hITu1UWFrJKneXtlLoEo1fAAAgAElEQVTwA7svPOJN6li45kW46W3z3MZ3ofyodTG1kSxIIkKJzwaEaa2f1VoPAH4JNLtIsVLqLqXUaqXU6sOHZcCGCBBXHWS9YJYv/DPc/Y2RjDrYbfu5x8Ij4/p3J7mLl/u3wSJ1PPQabhzXVkL2K9bG00aNRm1vlq5tEbxak5zzgVSPcl/3OW/eAq5o7gGt9fNa6zFa6zE9evRofZRCdMSOz+BYrnEc0x2GXeOzS3u2zmYEy8IjLVEKxt9tlrP+E1Td2yP6diWlm0fX9m7p2hbBqTXJOQsYpJRKV0pFATcACzyfoJQa5FGcAez0XYhCdNDK58zjjNuM+8w+cLi0ilU5Zpe27dfSbq2zrja+xAAcz4Xtn1obTxsYXdvm72HRBunaFsHplMlZa10L3Ad8DmwF3tFab1ZKPaqUmul+2n1Kqc1KqXXAHOB2v0UsRFsUboOcb4xj5YCxP/TZpT/bXIDL3aU9NhS6tOtFxsDoO8zyque8PtWOGi9IcoiaOunaFsGnVYsKa60XAYuanHvE4/hBH8clhG+set48HnyJTza4qLco2Edpt2TsD2H5U6DrICcTCrdC8plWR9UqI1O7kdIthvxjFRyvqGH5riKmDk62Oiwh2kRWCBOhq/I4rH/LLHveS+2gohNVrMw5Ahhd2heHSpd2va594YwZZnll8LSelVKNfh+LZNS2CEKSnEXoWvs61JQZx8lDoP8kn136s00eXdr9upMcHyJd2p48v8xseBsqiq2LpY08dwX7fLN0bYvgI8lZhCaXC7LmmeVxd3lfvrMdGi08EgqjtJvTbyIkDzWOa8qNLztBYpS7axto6NoWIphIchahadeXcHSPcdypKwy/zmeXDvku7XpKwfi7zHLWvKCZViVd2yLYSXIWoclzhPGoWyEqzmeXDosu7XrDrjOX9CzeCzsXWxpOW3h2bcuobRFsJDmL0FO0y2g5A6Bg7I98ennPVpjnnNqQFBVrzA2vF0TTqkaldqNPV+OL07HyGlbsPmJxREK0niRnEXo87zWffhF0T/fZpYtOVPH9Ho8u7VCbQtWcsT8yd6zavQSKgmONIaVUo9+PLEgigokkZxFaqkobD1zyvGfqA597LDwypl8CPUO5S7teQj84/WKz7Dl33OY8FyT5fEuBdG2LoCHJWYSW9W9BdalxnHQ6nDbNp5dv3KUdBq3mep5fcta9AZUl3p9rI6NSu9Hbo2v7O+naFkFCkrMIHVo3btX5cPpUdm4xd72ymuW7zA/3i88Ko+ScPgV6nGEcV58wEnQQcDhUo9/Tg2+t5f43s8nODZ452yI8SXIWoWPPUijaYRxHdYERN/jksk8u3s7N81ayeMuhhnMOBW+s2ueT6wcFpWDcbLO86nljLnkQKK2saTguLq9h4YaD3DxvJU8u3m5hVEK0TJKzCB2eS0yOuhmiu3T4ktm5xczLzKGipg7tcd6lYV5mTni1wIbfANFdjeOju43BYTaXnVvMJ00Ggrk0VNTUhd/vTwQVSc4iNBzNgR2fm+Wxs70/tw3mL8+hsrb5hTeqauuYvzzHJ/UEhejOMOoWsxwE06rk9yeClSRnERqyXoD6tu3ACyBpoE8um1NUhtbNP+bSsLeo3Cf1BI1xPwLc9/F3LoYjuy0N51Tk9yeClSRnEfyqy2Dtq2Z5nO92n0pPisPhZUyZQ0H/pFif1RUUup8Ggy50F7T7S5F9ye9PBCtJziL4bXjb2B4SjOQx8AKfXXrWxHSinM2/TaIjnMya6LsFToKG57Sqta9B1QnrYjmFWRPTiY5wNvtY2P7+RFCQ5CyCm9aw0mP61NjZ4PDdn3VGWgKj0ro1OudQEBPpZPbkdDLSEnxWV9A47TxIdN82qCqBDW+1/HwLZaQlMHtyOjGRzpNm1d0+oV94/v5EUJDkLILb3mVweKtxHBlnjNL2Ia01h09UN5RTE2KYMbw3r88ez5zpg31aV9BwOBrfOlj5PF5v7NrAnOmDeX32eC4d3ptOkeZH3oAenS2MSoiWSXIWwSkvC967E97yGD084gZje0gf2nyghF2FRrdtbJSTz38ymWduzJAW18gbjbnkAEXb4ZkM4/eRl2VtXF5kpCXwzI0Z/OSC0xvOfbTugIURCdEySc4i+Cx9DF6ZCZveh6rjfq3qo3X5DccXDulJbFSEX+sLGtFdIGmQWT66BzZ/YPxelj5mXVynMHNkn4bu7RW7iygsqbQ2ICG8kOQsgkteFqx4BmrKgSZdqevf8GnLrc6lWbDebF1dPirFZ9cOenlZULil8TntMn4vK562bQu6d9cYxqd3B4ypVJ6/XyHsRJKzCC4r50JNRfOP1VYZj/uqqj1HOFRSBUBiXBSTBib57NpBb+Vc49+7OT7+PfjaFSPNL1nStS3sSpKzCC5HdnNSi7medvl0UYwPPbq0Lx3emwgvU6rCUgB/D7528bDeDdPjNuYfZ/dh+04FE+FLPm1EcEkcAMrLn61ymFN8Oqiypo5PNxY0lKVLu4kA/R78oWtMJNPO6NFQ/mhtfgvPFsIakpxFcBl/Lzgjm38sIhrG3+OTapZuK6S0qhaAfomxjErtdopXhJnx90JEp+Yf8+HvwV88u7Y/XHcAbeOpYCI8SXIWwSV1LHQf0PicckBkDEx4wHjcBzy7tC8f0Qflo32hQ0bqWJhwv/Hv3rQFPeQqn/0e/GXaGcl06WSMvM89Ws7avGMWRyREY5KcRXApPQRFO81y0mAYeiXc9jFMe9gnVRyvqGHptsMNZenS9mLaw8a/+9ArITbRPF/rZcCejXSKdHLxWb0aygtkYJiwGUnOIrhkvwyuGuM4dTzctwquedGnLbXPNh2kus4FwLCUrrKSVEtSxxr//rd/bJ7bugBKDnp/jU14dm1/suEAte7fuRB2IMlZBI+6Glj9olked5f353bAh2s95jaP7OOXOkJOz6HQ71zj2FULa+ZbG08rjD8tkZ7x0QAUnajm211FFkckhEmSswge2z6BUneLLC4Zzpzp8yoKjlfyfc4RwNjgYuYISc6tNm62ebx6PtRWe3+uDTgdqtHvV+Y8CzuR5CyCx6p55vGYWRAR5fMqFqzPb9jDYcKAJJLjvYxIFic7YwZ0cSe7skKje9vmLvfo2v58cwHl1bUWRiOESZKzCA4Fm2DfcuPYEQGjZ/mlGs8u7ZnSpd02zkgYc6dZXvmcdbG00tA+8QzoEQdAeXUdi7ccsjgiIQySnEVwyPJoNZ95GcT39nkVOw+VsuVgCQBREQ4u8hjNK1pp9B3gdPdo7F8FB9ZaGs6pKKVkOU9hS5Kchf1VFMOGd8yyvwaCecxtvuDMZOI7eVnsRHjXuYcxtareqhesi6WVPLu2M3cc5miZve+Vi/AgyVnY37o33LtQAT3PgrRzfF6F1rpRq8nzA1u0keeXp43vQvlR62JphbTEWDLSjBXgal2ahRuk9SysJ8lZ2JvL1Xgg2LjZ4IfVutbsK2Z/sbF4RnynCKYO7nGKVwivUkZDn1HGcV2VMTfd5q4Y1Xg5TyGsJslZ2Nvur6A4xzju1BWGXeuXajy7tGcM7010hNMv9YQFpWDc3WY56z/gqrMunlaYMaw3TofxpW/NvmLyjpZbHJEId5Kchb2tet48HnUrRMX5vIqaOhcLN5grWkmXtg94Lul5PA92fGZtPKeQ2DmayYPM/bo/Wic7VQlrSXIW9nVkN+xc7C6oxtN0fChzx2GKy40lQft07cS4/t39Uk9YiewEGbeb5SCYVtW0a1t2qhJWkuQs7Gv1i4D7A3LQdGMPYT/wvMd42cg+OByyA5VPjLnT3LEq5xs4vN3aeE5h+pCexEYZtzN2FZ5g84ESiyMS4UySs7Cn6jJY+6pZ9tP0qRNVtSzeUtBQvkK6tH2nW6qxalg9z4F9NhQbFcGFQ3o2lKVrW1ipVclZKXWRUmq7UmqXUupXzTw+Rym1RSm1QSn1lVKqn+9DFWFl47tQedw4TkiHAef7pZovNhdQWWPsRjS4ZxfO7B3vl3rClueXqvVvQqW9W6Oe24MuWH+AOpd0bQtrnDI5K6WcwLPAxcAQ4Eal1JAmT1sLjNFaDwfeA/7q60BFGNH65OlTDv908nh2aV8+Spbr9Ln+k6DHGcZx9QkjQdvYpIFJJMYZK5wdKqli5Z4jFkckwlVrPvHGAbu01nu01tXAW8Dlnk/QWi/VWtfPPfge6OvbMEVYyf0ODm0yjiNjYeRNfqnmcGkV3+483FCWHaj8QKnGu1Wtet6Yu25TEU4Hlw43l4b9ULq2hUVak5xTgDyP8n73OW9+CHzakaBEmPOcPjX8OohJ8Es1CzccoL7Xclz/7vRNiPVLPWFv+A0Q7b5dcGQX5HxtaTin4tm1/emmAipr7D1HW/hBXha8dyc8N8X4f15WwEPwaV+hUuoWYAzwNy+P36WUWq2UWn348OHmniLCXckB2PqxWR472/tzO0i6tAMkujOMvNks23xg2KjUbvRLNL6olVbW8vX2QosjEgG19DF4ZSZseh8OroPNHxjlpY8FNIzWJOd8INWj3Nd9rhGl1AXAb4CZWuuq5i6ktX5eaz1Gaz2mRw9ZHlE0Y81L4HLvqdtvIvQ6yy/V7C0qY13eMQAinYoZw3y/y5XwMPZH5vH2T6F4r2WhnIpSiss9bnF4biMqQlxeFqx4xr2Wv7tbTbuM8oqnA9qCbk1yzgIGKaXSlVJRwA1Ao13UlVKjgOcwErN8zRTtU1sNq+eb5XH+azV7bnIx5fRkusVG+a0uASQN9Bhxr40lPW1spseUuiXbCjleUWNhNCJgVs6FmormH6utMh4PkFMmZ611LXAf8DmwFXhHa71ZKfWoUmqm+2l/AzoD7yql1imlFni5nBDebV0AZe7vdl16wxmX+qUaYwcqs/Pn8pHSpR0Q4z3W285+Bartu371wOTOnJVi3CevrnPx2aaDp3iFCAlHdtPQYm5Ku9yPB0ZEa56ktV4ELGpy7hGP4wt8HJcIR54DwcbcCU7f76ecnVvMPxbvYE9RGQCdIhxccGbPU7xK+MTACyChv9GlXXkMNr0HGbdZHZVXV4xMYVO+MS/70Y+38O2uImZNTCcjzT8DFIXFaquhqtT748oBiQMDFo6sECbs4cA6yFtpHDsiG6/L7CNPLt7OzfNWsmxnUcO5mjrN3G92+bwu0QyHs/G951XPG3Paberg8cqG47LqOj7ZcJCb563kycX2XoZUtMOxPJh/MRxtoWUcEQ3j7wlYSJKchT1keYzgHXoFdPFtazY7t5h5mTlUNJkWU6c18zJzyM4t9ml9wouRN0NEjHFcsBH+NcayqSotyc4t5o2VuY3OaQ0VNXXy9xJqdn0Jz02G/NXmOeU014VXDoiMgQkPQOrYgIXVqm5tIfwmLwuWPwXbPjHP+WEd7fnLc6isbX6+alVtHfOX50h3ZSDEdoekQVCwwSgf2QVH9xgjuCfcD9MetjY+N/l7CQOuOvjmL/DNX2m4z6ycMP1RSB0HK/9t3GNOHADj7w1oYgZJzsJKSx9zT1uowByEoYxtIlPH+bSqnKIyrz2oLg17i+w7OCmk5GVB0Y7G5zynqgycHvAPwebI30uIKyuC//4I9iw1z3XpDdfMh37nGGUffwa1lXRrC2s0N58QjOPvnvF5N2d6UhzKy06QDgX9k2R1sIBYOdeYktKcAE9VaUl6Uhzedg6Vv5cgl7sS/j2pcWJOnwx3Z5qJ2Qak5Sys0Zr5hD5sQc2amM6ijQXUNdMcio5wMmtius/qEi2w0VSVlsyamM6XWwpPGqMAEOl0yN9LsMjLMj5LjuyG7gOgc7IxvqV+oSOAyT+Hqb82BizaiCRnYY0Af0inJ8adNDLYoYzEPHuyTI8JmMQBxv1m3czmFwGeqtKSjLQEZk9OZ15mDlW1dXjuHDm4Vxf5ewkGTW+bHVzX+PFO3eCqeXD6hZaEdyqSnIU1EgfAwfU0m6D98CH9ZlYude6qusZEkNY9lv5JcTJvNdDG32sM/qpp5p6tM7BTVU5lzvTBTB2czPzlOWzKLyHHPTd+d+EJSipriO/k+3n4wkca3TZrRtJguOU96JYW2LjaQJKzsMb4e4wF5ZsbdePj+YQ1dS5e/W5fQ/l3lw7lmtGyq6klUscao7JXPG3cvvBsQfebaIvBYJ4y0hLISEtAa80P/pnJjkMnKKuu452sPH406TSrwxPetHTbDCB5iK0TM8iAMGGV6hMnd236aT7hF5sPNSwokdQ5istGyCYXlpr2MNz2MQy9EuI9viQd3up9sJjFlFLcMcG8z/zKd/uoc9l3AZWw19JtM4DinICF0l6SnIU1Mv9uHnc/DXqPND6sb/vY53Nd5y8334g3je9HdIS9Bn6EpdSxcM2LcP9qiEs2zpXkw7o3rI2rBVeOSqFbrNGVnXu0nCXbZI8f2+rSy/tjNhrb0BJJziLw9n0H+741jh0RcNtHcPc3xoe1j7s1N+4/zup9xmpOkU7FLePt3ZUVdiJjjG7uet8+CXX23AEqJsrJDWPNvx/PL33CRk4cNlaf8ybAy3C2lyRnEXjLnjCPh9/g13s/81eYH6AzhvUmOb6T3+oS7TTmTojpbhwfy4WN71obTwtuPacfTvcE6BW7j7CtoMTiiEQjlSXw+tVGL0wD94R1i5bhbC9JziKw8rONtWzBeLOc+xO/VXW4tIpP1ptb/cncVJuK7gzn/NgsL/u7sbSiDaV0i+EHQ811319esde6YERjNZXw1k3uWSAYny/n/wHOusqvt838RZKzCKxlHveah14JSf679/P6yn1U1xmDzjLSujEitZvf6hIdNO4uiO5qHB/ZBVs+tDaeFnh+yXs/O5/ismoLoxEA1NXCf38Ie5eZ5y79J0z6iXG7zE+3zfxJkrMInENbGm9wMemnfquqqraO1743dxW6Q1rN9tapK4y/2yxnPgGuZhYqsYEx/RIY2icegKpaF29m5Z7iFcKvtIZPHmr82XL+72G077edDSRJziJwPFvNg2dAz6F+q2rRxoMUnTCm5fSK78TFZ7UwelPYw9n3QmSccVy4BbYvsjYeL5RSjVrPr363j9o6e36RCAtf/RHWvmqWz7nPr7fLAkWSswiMI7th8/tmebL/Ws1aa+Yv39tQvvWcfkQ65U/d9mK7w9gfmuXMvza/SI0NXDaiN0mdowA4eLySzzcfsjiiMLXiX/DtP8zyiBth+p/wustNEJFPLBEY3z5pLjoy4HxIGe23qrJzi9mw/zgAUREObhib6re6hI9NuB8i3CPqD643Bw/aTHSEk5vG92soy7QqC6x7E774jVk+/SKY+Qw4QiOthcZPIeztWB6sf8ssT/6ZX6vzbDVfMbIPiZ2j/Vqf8KHOyTD6DrP8jX1bz7eMTyPSabTQVu8rZqP7C6EIgO2fwkf/Y5bTJsC1L4EzdNY7l+Qs/G/5U+YWbf0mQr8Jfqvq4PEKPt1U0FD2XHJRBIkJD4DT6DJm/yrIybQ2Hi+S4zsxY5i5FKznnHrhY3lZ8N6d8NwUeHkmvHMbaPd0u57D4MY3jTnMIUSSs/Cv0kOQ/YpZ9uMIbTAG59SveTw+vTtD3KNqRRDpmgIjbzbLmX+zLpZT8BwY9sn6gxwutefa4EFt6WPwykzY9L6x7WPON1Dnnr6W0B9u+S/EhN40SUnOwr++ewbq3B9YfTJgwHl+q6qypo43V5nTWmTRkSB27kOg3Gug710Gud9bG48XI1K7MSrNSAzVdS5eX7nvFK8QbdJo68dmbm9c8Efo0vPk8yFAkrPwn/KjkPWiWZ78M7+OovxoXT7F5ca6zCndYpg+JDTftGEhoT+MuMEsB0nr+bXvc6mulWlVPtPS1o9KwdYFgY0ngCQ5C//5fi7UGBvUkzwUTr/Yb1U1nT51+wRzDWQRpM6dQ8O6yLu+NJZ+taGLz+pFz3hj0GHRiSoWbjxgcUQhpKWtH7V2Px6aJDkL/6g8DiufM8uTf+rXKQ7f7TnCtoJSAGIinVw/RnafCnpJA411ketlPuH9uRaKdDq49WzPaVV70TYdYR50ug/w/liQbP3YXpKchX9kvQBV7qkliQNhyBV+re4lj1bz1aNT6BobOlMqwtokj2l32xdCwSbrYmnBjePSiIowPk437D9Odu4xiyMKEbHdvT8WJFs/tpckZ+F71WXw3bNm+dw54HD6rbq8o+Us3mqu0HTHhP5+q0sEWM8hcMalZnmZPVvPiZ2juWJkn4ayLEriA9sWGV/ymwqyrR/bS5Kz8L01L0P5EeO4axoMv86v1b28Ym/DOhWTBiUxMLmLX+sTAea5aM3mD+HwDutiaYHnnPpPNxVw8LiXgUzi1Ao2wX9/RMP95p7DYMiVQbn1Y3tJcha+VVsFK542y+c+6NdVe8qqanl7dV5D+U6ZPhV6+oyCQRe6C9pYCtaGhvSJZ3y60Q1b59K89r1Mq2qXE4Xw5g3mYNJu/eC2D+G6l4Jy68f2kuQsfGvd61B60Dju3AtG3uLX6t7P3k9ppbH6WHpSHFNO7+HX+oRFJv/cPF7/Jjx7trFiVF6WdTE1w3Na1Rsrc6msqbMwmiBUUwlv3QzH3V+4o7rATW9DXJK1cVkgwuoARIjIy4Lvn228p+qE+yGyk1+qy84tZv63OXy+xbzXfPs5/XDI9KnQlDrOaEEdc7dGD2+Fou3GGssT7rdNF+f0IT1J6RZD/rEKistrOP/vX5PRL4FZE9PJSEuwOjx70xo+fsBYshWMe8vXzofkM62NyyKSnEXHLX3MvYpPBY3mJNbfd/axJxdvZ15mDpU1dY1mQBaUVPqlPmEDeVlQWtD4nHYZK0eteBoGTrdFV6fToUhPiiX/mHG/Of9YJQePH+TLLYXMnpzOnOmDLY7Qxr79B2x42yxf+L8waLp18VhMurVFx7S0vN7KuT7vdszOLWZeZg4VTRIzwMsr9pGdW+zT+oRNrJxrrqfcVG2V8bgNZOcWs3pf479Bl4aKmjrmZebI36c3Wz+Gr/5oljNug7N/bF08NiDJWXRMS8vr+eFDc/7yHCprm7+PV1VbJ1NYQlWLK0W5bLNS1PzlOVR5Wb5T/j69OLge3r/LLPc7Fy75u1+X+g0GkpxFxwT4QzOnqMzr9r4uDXuLyn1an7CJxAHGPcjm2GilKPn7bKPSQ/Dmje6eNyAhHa5/FSKirI3LBiQ5i45JDOzyeulJcXj7Pu1Q0D8p1qf1CZsYfy9EeBlcqBy2WSkqPSkOb2MS5e+ziZoKeOsmKMk3ytHxxsjsllYFCyOSnEXH9B7p/TE/LK93/ZhUb+10oiOcsk1kqEod6x79H3NyC1q7bLOf76yJ6URHNL8ankMp+fvMyzKmwD03Gf41BvJXG+frR2b3kAFz9SQ5i/arOgGrnj/5vB+X18vcWXTSOYcyNruYPVmmq4S0aQ8bK0MNda8U1cn9u9Yu+PhBcFm/VWNGWgKzJ6cTE+k8qQWttSa5S7Q1gdnB0sfglZmw6X3jPvPx/eZjFz0OAy+wLjYbkqlUov2+/n/mYgHR8ZA+xSgnDjC6IX2cmHcVnuDFb80BNaPSulFbp+mfFCvzSMNF6ljz76pgIzw3BXQd7FsOa1+B0XdYGh7AnOmDmTo4mfnLc8gpKiP3SDkllbXUafjzwq3MvWW01SEGXqNZHU04nMYqcKKRViVnpdRFwFOAE3hBa/14k8cnA/8EhgM3aK3f83WgwmYObjD2a6538V9h5I1+q05rzR8/3kyty+jUHts/gXfuPgcV5iM6w1qvYTDxAWN+LMAXj8DpF0GXXtbGhdGCrv+yuHrvUa7593eAseb28l1FTBwYZitetTSrQ2tY+W9joRnR4JTd2kopJ/AscDEwBLhRKTWkydNygTuAN3wdoLAhVx188pDRYgHoPwlG3ODXKr/Ycohl7i5th4I/zBwqiVnAlF8aI3zB2KL0019YG08zxvTvzpWjUhrKv1+wmZo667vgAypIpsLZSWvuOY8Ddmmt92itq4G3gMs9n6C13qu13gCE2V9cmFr9IuSvMY6dUXDpP/w6J7Gypo4/fbKloXzT+DSG9unqt/pEEImMgcv+aZa3fGRsNWgzv774DOKijIFiuwpP8PKKvdYGFGjxfbw/ZqOpcHbSmuScAuR5lPe7z4lwVFoAXz1qlif9FJIG+bXK5zP3sL/Y6BLrFhvJT2UJROHptKkw8mazvOhnUFliVTTNSo7vxAPnm++Tp77cyeHSKgsjCqCKY1C41fvjfpjVEQoCOlpbKXWXUmq1Umr14cOHA1m18JXPfgVV7g++xIFw7k/8Wt3+4nL+7+tdDeWfXTiYhDhZoEA0ceH/Qqz7Pm5JPiz5k7XxNGPWxHRO6xEHQGlVLX/9bJvFEQVATaUxl7nYc2U0dy+bH2d1hILWJOd8INWj3Nd9rs201s9rrcdorcf06CFb+wWdnYth8wdm+dJ/GN96/eixRVuprDHulgzpHc+N49L8Wp8IUrHd4eK/mOVV8yBvlXXxNCMqwsHvLxvaUH53zX7WhvJa2646eP9Hxkj6epN/AWddZUyFG3qlMTXOJjuK2U1rknMWMEgpla6UigJuABb4NyxhO9XlsHCOWR5xI6RP9muVy3cVsWijuRPRHy8filO2hBTenHW1sTsVABoWPAC1XjbLsMiU03swfUjPhvIfFmzG5fK2rE4Q0xoW/dzY0KLeBX+E834D17wId39j/F9azF6dMjlrrWuB+4DPga3AO1rrzUqpR5VSMwGUUmOVUvuBa4HnlFKb/Rm0sEDmX+FYrnEck2B0I/pRTZ2LPyww/4yuGNmHsf1lWT/RAqVgxt8h0r1E5uGtsOIpa2Nqxu9mDCEqwvjoXb//OO+uyTvFK4JQ5t9g9X/M8tk/hokPWhdPEGrVPWet9SKt9ela6wFa6z+7zz2itV7gPs7SWvfVWsdprRO11kNbvqIIKoe2GAsI1Jv+J4jz7zzNV77bx87CEwDERTn59SXhueG6aKOEfn+XtH0AABqvSURBVHDeb83yN3+Dol3en2+BtMRY7pl8WkP5r59t53hFjYUR+dial2Dpn83yWdfAhX8O+12m2kqW7xQtc7mMOc2uWqOcNgFG3eLXKg+XVvHPxTsayvefP4ie8V42PRCiqfH3mCtO1VXZZmlPT/dOHUifrsbf9JGyav7h8fce1LYthE88BomeNhWumAsOSTVtJf9iomVrX4G8lcaxI9Lvc5oB/vrZNkqrjC8DpyXFcWe4bxYg2sbhhJnPgHJvQLHvW1j7qrUxNRET5eQ3M8y1nF79fh/bC0otjMgHcr83NrXQ7i9CvUfA9a/J9o/tJMlZeHeiEBY/YpYnPgjJZ/i1yrW5xby7xlwQ/5HLzPtzQrRar2HGLlb1Fv/O2DvYRi4Z1otzTksEoM6l+f2CTWhvm0HbXeFWeOM6qK00ygnpcPN7EN3F2riCmHzqCe8+/w1UHjeOE9Jh8s/8Wp3LpRsNArvgzJ5MHZzs1zpFCJvyS0jobxxXHod55xkbZbx3p7ERg8WUUo1mIHy/5ygLNx60OKp2OL4fXrva/KyI6wG3vg+d5b3bEZKcRWP1+60+PQo2vmOen/F3Y8EAP3pvzX7W7zfe4FERDn53qQwCEx0QFQuXeiztWbIfDq4z5uq/MtPYwtBip/fswm3n9GsoP7ZwK+XVtRZG1Er1nxNzJ8KzZxsLvwBEdTZazN1Pa/n14pQkOQuT536rR/eY53ucCQPP92vVxytq+IvHikl3TTqNfolxfq1ThIGozua953raZWxduOJpW7SgH7rgdBLdq94dOF7J3K9tvgmE5+fEoU1QXX+v3GHcY+4z0tLwQoUkZ2FotN9qk/texTl++xDLzi3m/jezOe+JrzlSZiwY0adrJ348bYBf6hNhZuVcc4BSU7VVxuMW6xoTyS8vMsdy/GvpLi78xzfc/2Y22XZbQaylzwlnhPFlSPiEJGdhaGm/1bpqv3yIPbl4OzfPW8kn6w82JGaAEaldiY1q1VbjQrQsSLYqvGZ0X5LjjaVwtYYdh06wcMNBbp63kicXb7c4Og8tfU64am3xZSdUSHIWhgB/iGXnFjMvM4eKmrqTav16+2H7tRhEcEocYGyw0CxlPG4D6/Yf43h544VIXBoqauqYl5ljn/dD4VaC4ctOKJDkLAxdenl/zA/7rc5fnkNlbV2zj1XVupi/PKfZx4Rok/H3QoS3BWx0C48F1vzlOVTXNd/9XlVbZ4/3Q8HGxmNRmpJ9mX1KkrOAsiPGG88bP+y3mlNUhrcpnS4Ne4vKfVqfCFOpY435zpExzbeg170Oy54MfFxN2P79sHspvHixOY+5ObIvs09Jcg531WXG4gElnruA+n+/1Sin9z89h4L+SbE+rU+EsWkPG1sTDr3S2KpwyJXQd5z5+Fd/hO//bV18QHpSHC1tuNY3wb/TGFu07k14/RpzVLYzCpzR5pcd2ZfZL2TUTTirqzXmKuavdp9QcP4jxvSII7uN+3Hj7/X5G+673UfY4J7P3JzoCCezZMlO4UupYxv/HddUGF9KczKN8me/NOZFZ9xmSXizJqbz5ZZCKmqav9Wzv7ic6lpXYFfL0xqWPQFLPHagi0+Bm981tpBdOdevnxPhTpJzuNLa2NBix2fmuUv+BuNm+7XabQUl3PXqamrde9gqjKW6XdpoMUdHOJk9OZ2MtAS/xiHCXGQM3PAmvHaVuXb8ggcgIgaGXxvwcDLSEpg9OZ15mTlU1dbh0sZ7o76ne2N+CT97dz3/vH4kjkDsaV5Xa+zfnv2yeS55qJGYu6YYZUnGfiXJOVx9/f8abwZw7hy/J+b8YxXc/uIqSiuNFZCSu0Tz6OVDWbjxIHuLyumfFMusiZKYRYBEdzaSzcuXwcH1gIYP7obITnDmZQEPZ870wUwdnMz85TkN74f4TpG8vtLYR33B+gP06tqJh/29fWrVCXhvFuz8wjyXPgWufxU6dfVv3aKBJOdwtPpF+OYvZnnETUZ3th8dL6/hjhdXcaikCoDO0RG8NGscQ/rEc9FZvf1atxBedeoKt3wAL82Aw1tB18G7s+DGN2HQ9ICHk5GW0OjLqdYapeC1740E/XzmHnrGd+KH5/rpts+JQnj9WmOZ03rDr4eZ/5LdpQJMBoSFm20LYeFPzfLAC2Dm037dBrKypo7Zr6xmZ+EJACKdiuduHc2QPvF+q1OIVotLhNs+gu7uOc+uGnj7FshZZm1cuDfHmHkWFw7p2XDufxdu4ZMNB3xTQf0a2c9NMZLyvyc1TsyTfgpXPieJ2QKSnMNJ7srG+632GQXXvgzOSL9VWefSzHlnHav2Hm0498S1I5g4MMlvdQrRZl16wu0LoGuaUa6thDeuh7xV1sYFOB2Kp28cxeh+Rotaa5jz9nq+33OkYxf2XCP74DqjG/tEgfGYchh7t5//iN/3bxfNk+QcLg7vgDevb7zf6k3vGvfd/ERrzZ8+2cKijQUN5x6+5AwuH5nitzqFaLeufeH2j6CL+zZLTRm8cgW8epXlW012inTywm1jGNDD2Aymus7F7FdWs72g9BSv9KKlNbIBLvgjjLmz/QGLDpPkHA5KDhqjUivcSwDGJrn3W+3h12qfz9zDSyv2NpRnTezP7EmylZywse6nwW0LjPcIGAl691e22GoyIS6Kl+8cR3IXYw3u0spabn9xFQeOeVnruiUtrZGNaty1LSwhyTlUNdpvdTwczzPOR8YZI1T9vN/qh2vz+X+fmltAzhjWm9/NGIKSLjJhdz1Ohx/878nnbbDVZN+EWObPGkvnaGMsb0FJJXfMX8XxippTvNJDVan7frqXJcnQska2Dcho7VC09DF3l1UFjd+ACq57BVIyfF5ldm4x85fnkFNURufoCLI87jGPS+/O368bEZj5mUL4ws7FNJ5p7KF+q0mL5vkO7dOV524dzR3zV1FTp9lx6AQ3Pv89/7+9Ow+Pqj4XOP59ZzJZSdiXsASiIIsLECkWUdSrKFWr4qN1q2sfaGut1tpWn3rvtddWvb2t3tbluS51qS1dVGwv1OUKLqioCAakmCBNIYRAIBCQkIRkkpn3/nEmkOXMZGGSOUzez/PkITM5c+bnz5nznvM7v9/7jhuSSdneOvKHZLkvSQyHYf2fYPlPoLYy+htYjmxPsOCcbFrdS2rDH+iRdYoPLfucp951Clm0zQ983PB+PHXtDNIDfvcXG+NFHVVpK33fuQJNy+7VZjWbPX4Iv7hsKt/7szP8XFRRTVFFtfP7jmqWF1WyYE4+35870XnBttXw2o9gR2HHO7cc2Z5gw9rJppfrrbYq/djmWCbAD8+bSP/MnpsNbkyPiFlqEqjZBQ9Ph9VPO9m0EuCS6aO47stj2z3fstTk34uL4eWF8PQ5rQNzdi5MvLB1QRDLke0pduWcTEJNzhl9L9ZbjVX6EXGyGs2dEqMcpTFedMq34fPX3EegmtXudlJcrnoCzv0pTDi315cd7asLAjBd/sEN/tc5xlfB5nAui0JnM1M3cdwLS0BbVJLypzlVuk673VmpsW215cj2KAvOyaLqn84Zcs2u6Nv0wL2kzbujl7pTL5S6M6Y7mktNfvCwc49Zw873JyUNjjkbKtYeruS253OniEb+GXDuzyD3pF5r5paqWr7nf5GFKa+QRiN+UY6XrXzV/6FT5arld3PyRc5JxMBxrf87LRh7kgXno52qkyP7tbucZR+xxPle0qfbvmBrVfT3tNKP5qh21o9h/Fz3K8vGg/DhY/D+f0PQyXzHlhXwxByYdjVMuhA2vNTjV6RnZW1lYcorZErw0HM+aX22HB42Bd9Xfg75c+L+/qbniEa77OlhM2bM0DVr1nS8oYmutgqW3gob/3b4OV8KjD0Vyle3P+M/9VbngHOEGppCPPzmP3h8xWZC4eifn4yAn0ULTrFCFiZ51VQ6RWQ++a2Tl9uN+CAl3bkS7+j719lh5oYaKP+Yg0vvJH3fJtfRdFVYr/nckf0g/3VFgX0PPUBEPlHVGZ3Z1q6cj1Yly+GvN7cexh5yHFz6FIyc1mP3kjZs388PXvyUjS0yE6X4BBEnVaeVfjR9Sr9hTprLmd+E5fe0LsHarHl99HsPgT/VyWc/cBxkDGi9XdslkDvXO/e9T/0uzFwIZR/C1g+h7AOoWA8aIgOcmZcuREAUSqrquex/PmDBnGO4/ZzjbOXEUcKunL2ubZCdcRMULYGPn2i93ZcWwNx7nYLxPaAxFOaxt0t49K2SQ7WYAU7JH8QvLpvKntqGVqXurPSj6ZOeuxBKO1kwI32AE6QH5TsTtT5bDCG3ZCJR1lt3IIyP13QW32n4zqHnJgzrx4Nfm8pJowfEeKXpKV25crbg7GVtz6RFIt/RFv/PsobBxY/Bcef2WDM27qzmjhc+5bMd1YeeSw/4uHPeJK6fNc6SixjT7Ikzein1pcDw451Mf5teh1Cw/SaBDCrnv8jtHwRYWXK4SIbfJ9x85rF8918mkJpiq2l7kw1rJwO3ZCJtT6QmXuCUe8yKX4Wnlpm+xg3Kon9mgBfWbKMxdPi9Tx47kF9ePpX8IVlxe19jksLgY53h6ObKb60IZI9wEgHtKz1chKazxpwCebOcOSVjZkJGZGTq7fvdZ5WfeivDppzO7ycrv19VxgOvFlMXDBEKK4+8VcKyol0sOD2fdzbtZsue2uiZxUxC2JWzV710k1PKLdpw1sgCWPBWXNdVxsr0BZCa4uOH507kptPy8dvVsjHtbVvtFMdwWx8dyIDrljpzP8JhZ77IvlLnZ+WvYXdxlJ0KTLkEvvZc7PftYI5JWVUdP3zpU1Zt2eu6i5ZzRQ5lFjNxZVfOR7udG2DzO8S8z6ThuAbmlpm+3Iwf1o/Hv34y44f1XIlJY456sdZHt8y85fNBTq7zM3aWk38galBPh1nfaf982/ftYMJn3uBM/rjgy/z2w1IeeLWYYKjNkqsWmcXOnDjMrqATzG44eEWwDtYugt+cA4/PhroYhdTjnExk/8FGfrLks6iBWYBJw7MtMBvTGWf92LlCPn4+5E5z/r1uaexlVM1BvYfTafp8wo2z85k9PvqtsIONIR5643MSNapqHHbl3FuiDTtVFsOaZ51qMfX7O7evOCQTaQqFee8fe3ipsJxlRbsINrndI3MosHWvZfoyptO6k3krVtKTONtd0xDz7++XVHHWL9/h0oLRzJ8+ijGDLJlQb7Pg3Bvc1i8WL3VmWleXt9/eF4ApF4EvFYr/Gnt4LIqWE7taTvT4bMd+Xi7czv+u28GeDr6gh5pjmb6M6R29lE4zf0gWRTuqiZFDiNKqOh5atomHlm1iZv4gLisYzVdOHEF2eiDq8cXEj00I62mxJoi0NegYOPkGmHbN4RnY3Ugm0nZil4iTKCQnPUBVrcuSCyB/SCbl+w62mpXdzDJ9GZNcCsv2cc1Tq1xvZfl9QprfR53L39JSfIwdlElpVR2N4TCqNpGsK2xCWE/qTLAMh2D3Rtj+iZMVKGZgFucq+eQbncT5vjbTALp4Jl1Yto8n391MfePhYWpVaAxpu8A8LDuN+dNHMb9gFJNG5BwK6g1NIcv0ZUwSK8gbyII5+VG/7zefOZ5lRbtYXFjOu5t2H7rCbmgKs6myptW+Dk8k22wTyeKo7145dye9ZbukIJGcuQXXQd6XnWC8vRB2rOu4CEWz4SfAt1dG/XOs4aNwWCnbW0dxRTXFFdUUVRxgZcmeqBO7wPkCfnXqSC4tGM1p44e0WxLV/H6W6cuY5NeZ73vlgXqWrNvB4sLtFFdUR9mTY0BGgHknjGBybg6Tc3OYlJtNTvrheu59fTi8T2UI27jmTWpWPEr/uq3szxxLvzNuYdKMs2O/6O37Ca18GGmqx4cSRtCUdPyzYxSG2LzCKQvX1cQBsYgPjr8ULnva9c/RhqcnjcgmNcXPxopqaoPRA7GbKbk5vHrb6fFovTGmjznnwRWU7K7peMMWRg/MYHJuDvsPNrKubB+NIUXp2nB4d4N6b7+uI3EPziIyD/g14Ad+o6r/2ebvacDzwMlAFXCFqpbG2mc8gvMHT9/BtLLfkUYQvyghFRpIZV3etZz6jQfdX7RtNY3PXkgg3D7INkmAlC/dBP6AkyDgwE44UOH8G+zaB5LskTCqAPoNp+mT35Gi7e/1Bn3p7Lrkz+zodyJVtUHnp6aBvbVBSipr+GhzVcwJG13lE7jgpFweuaogfjs1xvQZ3/1jIa+sr4j7cWnOcUOZODybQVmpDO6XxuCsVAb3S2VQVip/WFXGsytLD12kdDaot7246enXdUZcg7OI+IFNwFygHFgNXKWqRS22uRk4SVW/JSJXAvNV9YpY+z3S4LxxzZvkLb2KTGk/47hR/Xwx5ixycgZAYx0SrIPGWqSxDtm7BX9TXTzzdwBQ78tk/cgr2JYxmdK0iezxDaK+MUzF/oPMKnuCBf7DxdCdk4gATzZdwK9Clx/R+w7OSo0MIWUzOTcHgLv/ssF1aNsmdhljjkSsiWTpKT7u+sokGkMauc1WzT9317hOMo0Hn8CsYwaTOyCD9ICP9BQ/6QE/6QEfe2qCLFq11fW9U/0+7r5gEpNG5JDiF3wipPh8+HywadcB7lr8dxpclpbG4/gZ7wlhM4ESVd0c2fmfgIuBohbbXAz8JPL7S8CjIiLag2PmNSseJQ33mccBCTG0fHn0F3cjMIdU8KGuQT2kwv8Fp3JbydzIM7WRH8dHXM47oWnc4H+dfN9OtoRH8FxoHmt1QtcbEjFucCYvfHMWQ7PTkDaNKq2qtYldxpi462gi2Q2z81ttH2wKU1JZw4Ln17D9i4NxbUtYYeU/YyRriiIYCnPPkqKON2yjoSnEsyu39NoxtDPBeRSwrcXjcuCUaNuoapOI7AcGA3tabiQiC4GFAHl5ed1ssqN/3Vb8Et/YH1Yo1RG8GDqTXTqASgaySweySwdwrOxgUer9ZLqcEDQQ4LnQvJj7XqsTWNvUPhin+n2cOLr/oWGcwVlpDMpK5W/rd7C27AvXBJ4+gRNH92dYTrrre31/7kTOnDjMJnYZY+KuK8eX1BQfU0bmUDB2ABX7D7oOhwtw0uj+nHfCCKpqguytDbKnpoGqmiCbdh1oVaI2kcIKpXt6LxlTry6lUtUngSfBGdY+kn3tzxxLqHqza4AOK2zQfF7yn89BSaeedOdfSWdI/TYe8D9OhrQPsvWk8m++W9g3eNqh4Y7+PmGgT9hcOYgn6y9gYYr78HT1kGncemIuaYHDQyvpKX7+8HEZhVv3RQ2y550w3PUe8LS8AVGHj9JS/NzY5gy1rYK8gRaMjTE9oqvHlxtn57O8qNJ9ODzg556LjnfdX6x73AJMzxvAlV/Ko74pRH1jiPrGMPWNIV7bsJMte6KvmBmclcqxQ/vRFA4TUgiFw4TCUL63lgMN7pNsezsZU2eC83ZgTIvHoyPPuW1TLiIpQH+ciWE9pt8Zt9CwdCWZtL/n3EAqqRc9yL0us7YLy/bxzG+2cyNL2wXZZ/Wr3PGNr7t+SJx7LSFWBNsPT29MmcSiy6e6vi5/aFa3gmxHw0cWeI0xR4vuHs86Cur/euEU19eeM2V41ONuRsDPU9fPiHGc7/5FUTx1JjivBiaISD5OEL4SuLrNNkuA64EPgcuAt3ryfjPApBln88Gn1zK97HlSWwTZIAHW5l3HqVGWUxXkDeSd0+/kpnencTWvMk52Uqoj+APnM3POeVE/JIc/XHB70wTCTZ37cB1JkLXhaWNMsujO8ay7x8/efl1P6OxSqvOBX+EspXpGVe8TkXuBNaq6RETSgd8B04G9wJXNE8iiif865zL2Z+Z1bp0z3U+20duvM8aYvi5Zjtd9KgmJMcYYczToSnC2es7GGGOMx1hwNsYYYzzGgrMxxhjjMRacjTHGGI+x4GyMMcZ4jAVnY4wxxmMsOBtjjDEek7B1ziKyG9gax10OoU2hDQNYv0Rj/eLO+sWd9Ys76xd30fplrKoO7cwOEhac401E1nR2cXdfYv3izvrFnfWLO+sXd9Yv7uLRLzasbYwxxniMBWdjjDHGY5IpOD+Z6AZ4lPWLO+sXd9Yv7qxf3Fm/uDvifkmae87GGGNMskimK2djjDEmKSRVcBaRn4rIehFZJyJviMjIRLfJC0TkFyKyMdI3fxGRAYlukxeIyOUi8pmIhEWkz884FZF5IvK5iJSIyF2Jbo8XiMgzIlIpIhsS3RYvEZExIvK2iBRFvkO3JbpNXiAi6SLysYh8GumX/+j2vpJpWFtEclS1OvL7rcAUVf1WgpuVcCJyLvCWqjaJyM8BVPXOBDcr4URkMhAGngB+oKp9tsC4iPiBTcBcoBxYDVylqkUJbViCicgcoAZ4XlVPSHR7vEJEcoFcVS0UkWzgE+AS+7yIAFmqWiMiAeB94DZV/air+0qqK+fmwByRBSTPmccRUNU3VLUp8vAjYHQi2+MVqlqsqp8nuh0eMRMoUdXNqhoE/gRcnOA2JZyqvgvsTXQ7vEZVK1S1MPL7AaAYGJXYViWeOmoiDwORn27FoaQKzgAicp+IbAOuAf490e3xoJuA1xLdCOM5o4BtLR6XYwdb0wkiMg6YDqxKbEu8QUT8IrIOqASWqWq3+uWoC84islxENrj8XAygqner6hhgEXBLYlvbezrql8g2dwNNOH3TJ3SmX4wx3SMi/YDFwPfajFz2WaoaUtVpOCOUM0WkW7dDUuLbrJ6nqud0ctNFwKvAPT3YHM/oqF9E5AbgQuBsTaaJBh3owuelr9sOjGnxeHTkOWNcRe6pLgYWqerLiW6P16jqFyLyNjAP6PKEwqPuyjkWEZnQ4uHFwMZEtcVLRGQe8CPgIlWtS3R7jCetBiaISL6IpAJXAksS3CbjUZGJT08Dxar6UKLb4xUiMrR5NYyIZOBMsOxWHEq22dqLgYk4M3C3At9S1T5/9i8iJUAaUBV56iObxQ4iMh94BBgKfAGsU9XzEtuqxBGR84FfAX7gGVW9L8FNSjgR+SNwJk6VoV3APar6dEIb5QEichrwHvB3nOMtwI9V9dXEtSrxROQk4Lc43yEf8IKq3tutfSVTcDbGGGOSQVINaxtjjDHJwIKzMcYY4zEWnI0xxhiPseBsjDHGeIwFZ2OMMcZjLDgbY4wxHmPB2RhjjPEYC87GGGOMx/w/KTjjco6w6isAAAAASUVORK5CYII=\n",
      "text/plain": [
       "<Figure size 576x360 with 1 Axes>"
      ]
     },
     "metadata": {
      "needs_background": "light"
     },
     "output_type": "display_data"
    }
   ],
   "source": [
    "plt.figure(figsize=(8, 5))\n",
    "plt.plot(t, x_np[0,:,0], \".-\", linewidth=3, markersize=15, label=\"x\")\n",
    "plt.plot(t, w_np[0,:,0], \".-\", linewidth=3, markersize=15, label=\"w\")\n",
    "plt.legend(fontsize=16)\n",
    "plt.title(\"Traces\", fontsize=16)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Constructing STL formulas"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### One way to construct formulas is to explicitly call the constructors"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(◻ [0, inf]( x <= 1.0 )) ∧ (◻ [0, inf]( w <= 0.9 ))\n"
     ]
    },
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
       " -->\n",
       "<!-- Title: %3 Pages: 1 -->\n",
       "<svg width=\"310pt\" height=\"239pt\"\n",
       " viewBox=\"0.00 0.00 310.00 239.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 235)\">\n",
       "<title>%3</title>\n",
       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-235 306,-235 306,4 -4,4\"/>\n",
       "<!-- 139955138903624 -->\n",
       "<g id=\"node1\" class=\"node\"><title>139955138903624</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"276,-34 26,-34 26,-0 276,-0 276,-34\"/>\n",
       "<text text-anchor=\"middle\" x=\"151\" y=\"-20.4\" font-family=\"Times,serif\" font-size=\"12.00\">And</text>\n",
       "<text text-anchor=\"middle\" x=\"151\" y=\"-7.4\" font-family=\"Times,serif\" font-size=\"12.00\">(◻ [0, inf]( x &lt;= 1.0 )) ∧ (◻ [0, inf]( w &lt;= 0.9 ))</text>\n",
       "</g>\n",
       "<!-- 139952677203192 -->\n",
       "<g id=\"node2\" class=\"node\"><title>139952677203192</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"141,-104 25,-104 25,-70 141,-70 141,-104\"/>\n",
       "<text text-anchor=\"middle\" x=\"83\" y=\"-90.4\" font-family=\"Times,serif\" font-size=\"12.00\">Always</text>\n",
       "<text text-anchor=\"middle\" x=\"83\" y=\"-77.4\" font-family=\"Times,serif\" font-size=\"12.00\">◻ [0, inf]( x &lt;= 1.0 )</text>\n",
       "</g>\n",
       "<!-- 139952677203192&#45;&gt;139955138903624 -->\n",
       "<g id=\"edge1\" class=\"edge\"><title>139952677203192&#45;&gt;139955138903624</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M99.1151,-69.8849C107.544,-61.4557 118.024,-50.9761 127.354,-41.6464\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"129.932,-44.0177 134.528,-34.4717 124.982,-39.068 129.932,-44.0177\"/>\n",
       "</g>\n",
       "<!-- 139952677203248 -->\n",
       "<g id=\"node3\" class=\"node\"><title>139952677203248</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"114.5,-174 51.5,-174 51.5,-140 114.5,-140 114.5,-174\"/>\n",
       "<text text-anchor=\"middle\" x=\"83\" y=\"-160.4\" font-family=\"Times,serif\" font-size=\"12.00\">LessThan</text>\n",
       "<text text-anchor=\"middle\" x=\"83\" y=\"-147.4\" font-family=\"Times,serif\" font-size=\"12.00\">x &lt;= 1.0</text>\n",
       "</g>\n",
       "<!-- 139952677203248&#45;&gt;139952677203192 -->\n",
       "<g id=\"edge2\" class=\"edge\"><title>139952677203248&#45;&gt;139952677203192</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M83,-139.885C83,-132.374 83,-123.234 83,-114.731\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"86.5001,-114.472 83,-104.472 79.5001,-114.472 86.5001,-114.472\"/>\n",
       "</g>\n",
       "<!-- 139955309922712 -->\n",
       "<g id=\"node4\" class=\"node\"><title>139955309922712</title>\n",
       "<polygon fill=\"lightskyblue\" stroke=\"black\" points=\"54,-231 0,-231 0,-210 54,-210 54,-231\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-217.4\" font-family=\"Times,serif\" font-size=\"12.00\">x</text>\n",
       "</g>\n",
       "<!-- 139955309922712&#45;&gt;139952677203248 -->\n",
       "<g id=\"edge3\" class=\"edge\"><title>139955309922712&#45;&gt;139952677203248</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M35.75,-209.891C42.5464,-202.427 52.2756,-191.742 61.1409,-182.006\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"63.8482,-184.231 67.993,-174.481 58.6724,-179.518 63.8482,-184.231\"/>\n",
       "</g>\n",
       "<!-- 139952711194592 -->\n",
       "<g id=\"node5\" class=\"node\"><title>139952711194592</title>\n",
       "<polygon fill=\"palegreen\" stroke=\"black\" points=\"126,-231 72,-231 72,-210 126,-210 126,-231\"/>\n",
       "<text text-anchor=\"middle\" x=\"99\" y=\"-217.4\" font-family=\"Times,serif\" font-size=\"12.00\">1.0</text>\n",
       "</g>\n",
       "<!-- 139952711194592&#45;&gt;139952677203248 -->\n",
       "<g id=\"edge4\" class=\"edge\"><title>139952711194592&#45;&gt;139952677203248</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M96.5,-209.891C94.712,-203.018 92.2135,-193.414 89.8514,-184.335\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"93.1928,-183.277 87.2877,-174.481 86.4183,-185.04 93.1928,-183.277\"/>\n",
       "</g>\n",
       "<!-- 139952677203080 -->\n",
       "<g id=\"node6\" class=\"node\"><title>139952677203080</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"278.5,-104 159.5,-104 159.5,-70 278.5,-70 278.5,-104\"/>\n",
       "<text text-anchor=\"middle\" x=\"219\" y=\"-90.4\" font-family=\"Times,serif\" font-size=\"12.00\">Always</text>\n",
       "<text text-anchor=\"middle\" x=\"219\" y=\"-77.4\" font-family=\"Times,serif\" font-size=\"12.00\">◻ [0, inf]( w &lt;= 0.9 )</text>\n",
       "</g>\n",
       "<!-- 139952677203080&#45;&gt;139955138903624 -->\n",
       "<g id=\"edge5\" class=\"edge\"><title>139952677203080&#45;&gt;139955138903624</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M202.885,-69.8849C194.456,-61.4557 183.976,-50.9761 174.646,-41.6464\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"177.018,-39.068 167.472,-34.4717 172.068,-44.0177 177.018,-39.068\"/>\n",
       "</g>\n",
       "<!-- 139952677203416 -->\n",
       "<g id=\"node7\" class=\"node\"><title>139952677203416</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"250.5,-174 187.5,-174 187.5,-140 250.5,-140 250.5,-174\"/>\n",
       "<text text-anchor=\"middle\" x=\"219\" y=\"-160.4\" font-family=\"Times,serif\" font-size=\"12.00\">LessThan</text>\n",
       "<text text-anchor=\"middle\" x=\"219\" y=\"-147.4\" font-family=\"Times,serif\" font-size=\"12.00\">w &lt;= 0.9</text>\n",
       "</g>\n",
       "<!-- 139952677203416&#45;&gt;139952677203080 -->\n",
       "<g id=\"edge6\" class=\"edge\"><title>139952677203416&#45;&gt;139952677203080</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M219,-139.885C219,-132.374 219,-123.234 219,-114.731\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"222.5,-114.472 219,-104.472 215.5,-114.472 222.5,-114.472\"/>\n",
       "</g>\n",
       "<!-- 139955309411888 -->\n",
       "<g id=\"node8\" class=\"node\"><title>139955309411888</title>\n",
       "<polygon fill=\"lightskyblue\" stroke=\"black\" points=\"230,-231 176,-231 176,-210 230,-210 230,-231\"/>\n",
       "<text text-anchor=\"middle\" x=\"203\" y=\"-217.4\" font-family=\"Times,serif\" font-size=\"12.00\">w</text>\n",
       "</g>\n",
       "<!-- 139955309411888&#45;&gt;139952677203416 -->\n",
       "<g id=\"edge7\" class=\"edge\"><title>139955309411888&#45;&gt;139952677203416</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M205.5,-209.891C207.288,-203.018 209.787,-193.414 212.149,-184.335\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"215.582,-185.04 214.712,-174.481 208.807,-183.277 215.582,-185.04\"/>\n",
       "</g>\n",
       "<!-- 139952711194664 -->\n",
       "<g id=\"node9\" class=\"node\"><title>139952711194664</title>\n",
       "<polygon fill=\"palegreen\" stroke=\"black\" points=\"302,-231 248,-231 248,-210 302,-210 302,-231\"/>\n",
       "<text text-anchor=\"middle\" x=\"275\" y=\"-217.4\" font-family=\"Times,serif\" font-size=\"12.00\">0.9</text>\n",
       "</g>\n",
       "<!-- 139952711194664&#45;&gt;139952677203416 -->\n",
       "<g id=\"edge8\" class=\"edge\"><title>139952711194664&#45;&gt;139952677203416</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M266.25,-209.891C259.454,-202.427 249.724,-191.742 240.859,-182.006\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"243.328,-179.518 234.007,-174.481 238.152,-184.231 243.328,-179.518\"/>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
       "<graphviz.dot.Digraph at 0x7f49459c2b00>"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ϕ1 = stlcg.LessThan(lhs='x', val=c)\n",
    "ϕ2 = stlcg.GreaterThan(lhs='w', val=d)\n",
    "ϕ3 = stlcg.LessThan(lhs='w', val=d)\n",
    "ϕ = stlcg.Always(subformula=ϕ1)\n",
    "ψ = stlcg.Always(subformula=ϕ3)\n",
    "formula = stlcg.And(subformula1=ϕ, subformula2=ψ)\n",
    "print(formula)\n",
    "viz.make_stl_graph(formula)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Another way (preferred way) is to use the math operators which have been overloaded\n",
    "#### (less than, greater than, equal, not, and, or)\n",
    "#### Still need to use the Always and Or constructors explicitly"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "x_exp = Expression('x', x)    # The first argument is the name of the variable, the second argument is the numerical value\n",
    "w_exp = Expression('w', w)\n",
    "c_exp = Expression('c', c)         # If the variable is a parameter of the STL, then input the actual value\n",
    "d_exp = Expression('d', d)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(◻ [0, inf]( x <= c )) ∧ (◻ [0, inf]( w <= d ))\n"
     ]
    },
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
       " -->\n",
       "<!-- Title: %3 Pages: 1 -->\n",
       "<svg width=\"305pt\" height=\"239pt\"\n",
       " viewBox=\"0.00 0.00 305.00 239.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 235)\">\n",
       "<title>%3</title>\n",
       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-235 301,-235 301,4 -4,4\"/>\n",
       "<!-- 139955138903568 -->\n",
       "<g id=\"node1\" class=\"node\"><title>139955138903568</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"263.5,-34 32.5,-34 32.5,-0 263.5,-0 263.5,-34\"/>\n",
       "<text text-anchor=\"middle\" x=\"148\" y=\"-20.4\" font-family=\"Times,serif\" font-size=\"12.00\">And</text>\n",
       "<text text-anchor=\"middle\" x=\"148\" y=\"-7.4\" font-family=\"Times,serif\" font-size=\"12.00\">(◻ [0, inf]( x &lt;= c )) ∧ (◻ [0, inf]( w &lt;= d ))</text>\n",
       "</g>\n",
       "<!-- 139952677203304 -->\n",
       "<g id=\"node2\" class=\"node\"><title>139952677203304</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"138.5,-104 31.5,-104 31.5,-70 138.5,-70 138.5,-104\"/>\n",
       "<text text-anchor=\"middle\" x=\"85\" y=\"-90.4\" font-family=\"Times,serif\" font-size=\"12.00\">Always</text>\n",
       "<text text-anchor=\"middle\" x=\"85\" y=\"-77.4\" font-family=\"Times,serif\" font-size=\"12.00\">◻ [0, inf]( x &lt;= c )</text>\n",
       "</g>\n",
       "<!-- 139952677203304&#45;&gt;139955138903568 -->\n",
       "<g id=\"edge1\" class=\"edge\"><title>139952677203304&#45;&gt;139955138903568</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M99.9301,-69.8849C107.662,-61.5391 117.257,-51.1834 125.835,-41.9238\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"128.511,-44.1861 132.739,-34.4717 123.376,-39.4287 128.511,-44.1861\"/>\n",
       "</g>\n",
       "<!-- 139952677203136 -->\n",
       "<g id=\"node3\" class=\"node\"><title>139952677203136</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"116.5,-174 53.5,-174 53.5,-140 116.5,-140 116.5,-174\"/>\n",
       "<text text-anchor=\"middle\" x=\"85\" y=\"-160.4\" font-family=\"Times,serif\" font-size=\"12.00\">LessThan</text>\n",
       "<text text-anchor=\"middle\" x=\"85\" y=\"-147.4\" font-family=\"Times,serif\" font-size=\"12.00\">x &lt;= c</text>\n",
       "</g>\n",
       "<!-- 139952677203136&#45;&gt;139952677203304 -->\n",
       "<g id=\"edge2\" class=\"edge\"><title>139952677203136&#45;&gt;139952677203304</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M85,-139.885C85,-132.374 85,-123.234 85,-114.731\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"88.5001,-114.472 85,-104.472 81.5001,-114.472 88.5001,-114.472\"/>\n",
       "</g>\n",
       "<!-- 139952677306320 -->\n",
       "<g id=\"node4\" class=\"node\"><title>139952677306320</title>\n",
       "<polygon fill=\"lightskyblue\" stroke=\"black\" points=\"54,-231 0,-231 0,-210 54,-210 54,-231\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-217.4\" font-family=\"Times,serif\" font-size=\"12.00\">x</text>\n",
       "</g>\n",
       "<!-- 139952677306320&#45;&gt;139952677203136 -->\n",
       "<g id=\"edge3\" class=\"edge\"><title>139952677306320&#45;&gt;139952677203136</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M36.0625,-209.891C43.1016,-202.427 53.1783,-191.742 62.3603,-182.006\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"65.1423,-184.157 69.4571,-174.481 60.0497,-179.355 65.1423,-184.157\"/>\n",
       "</g>\n",
       "<!-- 139952677304248 -->\n",
       "<g id=\"node5\" class=\"node\"><title>139952677304248</title>\n",
       "<polygon fill=\"palegreen\" stroke=\"black\" points=\"126,-231 72,-231 72,-210 126,-210 126,-231\"/>\n",
       "<text text-anchor=\"middle\" x=\"99\" y=\"-217.4\" font-family=\"Times,serif\" font-size=\"12.00\">c</text>\n",
       "</g>\n",
       "<!-- 139952677304248&#45;&gt;139952677203136 -->\n",
       "<g id=\"edge4\" class=\"edge\"><title>139952677304248&#45;&gt;139952677203136</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M96.8125,-209.891C95.248,-203.018 93.0618,-193.414 90.995,-184.335\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"94.3842,-183.455 88.7517,-174.481 87.5588,-185.008 94.3842,-183.455\"/>\n",
       "</g>\n",
       "<!-- 139955138902784 -->\n",
       "<g id=\"node6\" class=\"node\"><title>139955138902784</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"267,-104 157,-104 157,-70 267,-70 267,-104\"/>\n",
       "<text text-anchor=\"middle\" x=\"212\" y=\"-90.4\" font-family=\"Times,serif\" font-size=\"12.00\">Always</text>\n",
       "<text text-anchor=\"middle\" x=\"212\" y=\"-77.4\" font-family=\"Times,serif\" font-size=\"12.00\">◻ [0, inf]( w &lt;= d )</text>\n",
       "</g>\n",
       "<!-- 139955138902784&#45;&gt;139955138903568 -->\n",
       "<g id=\"edge5\" class=\"edge\"><title>139955138902784&#45;&gt;139955138903568</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M196.833,-69.8849C188.978,-61.5391 179.231,-51.1834 170.517,-41.9238\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"172.905,-39.355 163.503,-34.4717 167.808,-44.1526 172.905,-39.355\"/>\n",
       "</g>\n",
       "<!-- 139955138902448 -->\n",
       "<g id=\"node7\" class=\"node\"><title>139955138902448</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"243.5,-174 180.5,-174 180.5,-140 243.5,-140 243.5,-174\"/>\n",
       "<text text-anchor=\"middle\" x=\"212\" y=\"-160.4\" font-family=\"Times,serif\" font-size=\"12.00\">LessThan</text>\n",
       "<text text-anchor=\"middle\" x=\"212\" y=\"-147.4\" font-family=\"Times,serif\" font-size=\"12.00\">w &lt;= d</text>\n",
       "</g>\n",
       "<!-- 139955138902448&#45;&gt;139955138902784 -->\n",
       "<g id=\"edge6\" class=\"edge\"><title>139955138902448&#45;&gt;139955138902784</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M212,-139.885C212,-132.374 212,-123.234 212,-114.731\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"215.5,-114.472 212,-104.472 208.5,-114.472 215.5,-114.472\"/>\n",
       "</g>\n",
       "<!-- 139952677304360 -->\n",
       "<g id=\"node8\" class=\"node\"><title>139952677304360</title>\n",
       "<polygon fill=\"lightskyblue\" stroke=\"black\" points=\"225,-231 171,-231 171,-210 225,-210 225,-231\"/>\n",
       "<text text-anchor=\"middle\" x=\"198\" y=\"-217.4\" font-family=\"Times,serif\" font-size=\"12.00\">w</text>\n",
       "</g>\n",
       "<!-- 139952677304360&#45;&gt;139955138902448 -->\n",
       "<g id=\"edge7\" class=\"edge\"><title>139952677304360&#45;&gt;139955138902448</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M200.188,-209.891C201.752,-203.018 203.938,-193.414 206.005,-184.335\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"209.441,-185.008 208.248,-174.481 202.616,-183.455 209.441,-185.008\"/>\n",
       "</g>\n",
       "<!-- 139952677302960 -->\n",
       "<g id=\"node9\" class=\"node\"><title>139952677302960</title>\n",
       "<polygon fill=\"palegreen\" stroke=\"black\" points=\"297,-231 243,-231 243,-210 297,-210 297,-231\"/>\n",
       "<text text-anchor=\"middle\" x=\"270\" y=\"-217.4\" font-family=\"Times,serif\" font-size=\"12.00\">d</text>\n",
       "</g>\n",
       "<!-- 139952677302960&#45;&gt;139955138902448 -->\n",
       "<g id=\"edge8\" class=\"edge\"><title>139952677302960&#45;&gt;139955138902448</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M260.938,-209.891C253.898,-202.427 243.822,-191.742 234.64,-182.006\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"236.95,-179.355 227.543,-174.481 231.858,-184.157 236.95,-179.355\"/>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
       "<graphviz.dot.Digraph at 0x7f49459db5c0>"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ϕ1 = x_exp <= c_exp\n",
    "ϕ2 = w_exp >= d_exp \n",
    "ϕ3 = w_exp <= d_exp\n",
    "ϕ = stlcg.Always(subformula=ϕ1)\n",
    "ψ = stlcg.Always(subformula=ϕ3)\n",
    "formula = stlcg.And(subformula1=ϕ, subformula2=ψ)\n",
    "print(formula)\n",
    "viz.make_stl_graph(formula)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Evaluating the formula\n",
    "### You need to feed in the necessary inputs. If the formula requires multiple inputs, it takes in a tuple of length 2 where each element in the tuple is the input to each subformula, in the order they are created. If the formula requires more than two inputs, then the tuple contains a tuple, eg. (x, (y, z)). The grouping of the input traces depend on how the formula was created.\n",
    "\n",
    "#### the inputs can be made up of tensors, or Expression objects."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(w >= d) ∧ ((◻ [0, inf]( x <= c )) ∧ (◻ [0, inf]( w <= d )))\n"
     ]
    },
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
       " -->\n",
       "<!-- Title: %3 Pages: 1 -->\n",
       "<svg width=\"374pt\" height=\"309pt\"\n",
       " viewBox=\"0.00 0.00 374.00 309.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 305)\">\n",
       "<title>%3</title>\n",
       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-305 370,-305 370,4 -4,4\"/>\n",
       "<!-- 139952677303688 -->\n",
       "<g id=\"node1\" class=\"node\"><title>139952677303688</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"296,-34 0,-34 0,-0 296,-0 296,-34\"/>\n",
       "<text text-anchor=\"middle\" x=\"148\" y=\"-20.4\" font-family=\"Times,serif\" font-size=\"12.00\">And</text>\n",
       "<text text-anchor=\"middle\" x=\"148\" y=\"-7.4\" font-family=\"Times,serif\" font-size=\"12.00\">(w &gt;= d) ∧ ((◻ [0, inf]( x &lt;= c )) ∧ (◻ [0, inf]( w &lt;= d )))</text>\n",
       "</g>\n",
       "<!-- 139952677203360 -->\n",
       "<g id=\"node2\" class=\"node\"><title>139952677203360</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"114.5,-244 37.5,-244 37.5,-210 114.5,-210 114.5,-244\"/>\n",
       "<text text-anchor=\"middle\" x=\"76\" y=\"-230.4\" font-family=\"Times,serif\" font-size=\"12.00\">GreaterThan</text>\n",
       "<text text-anchor=\"middle\" x=\"76\" y=\"-217.4\" font-family=\"Times,serif\" font-size=\"12.00\">w &gt;= d</text>\n",
       "</g>\n",
       "<!-- 139952677203360&#45;&gt;139952677303688 -->\n",
       "<g id=\"edge1\" class=\"edge\"><title>139952677203360&#45;&gt;139952677303688</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M74.5958,-209.976C72.7214,-180.573 71.9559,-116.739 95,-70 100.423,-59.001 109.134,-48.9958 117.942,-40.7646\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"120.427,-43.2395 125.625,-34.0075 115.805,-37.9829 120.427,-43.2395\"/>\n",
       "</g>\n",
       "<!-- 139952677304360 -->\n",
       "<g id=\"node3\" class=\"node\"><title>139952677304360</title>\n",
       "<polygon fill=\"lightskyblue\" stroke=\"black\" points=\"107,-301 53,-301 53,-280 107,-280 107,-301\"/>\n",
       "<text text-anchor=\"middle\" x=\"80\" y=\"-287.4\" font-family=\"Times,serif\" font-size=\"12.00\">w</text>\n",
       "</g>\n",
       "<!-- 139952677304360&#45;&gt;139952677203360 -->\n",
       "<g id=\"edge2\" class=\"edge\"><title>139952677304360&#45;&gt;139952677203360</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M79.375,-279.891C78.9328,-273.092 78.3168,-263.621 77.7319,-254.628\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"81.2137,-254.233 77.0719,-244.481 74.2284,-254.687 81.2137,-254.233\"/>\n",
       "</g>\n",
       "<!-- 139955138902448 -->\n",
       "<g id=\"node11\" class=\"node\"><title>139955138902448</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"195.5,-244 132.5,-244 132.5,-210 195.5,-210 195.5,-244\"/>\n",
       "<text text-anchor=\"middle\" x=\"164\" y=\"-230.4\" font-family=\"Times,serif\" font-size=\"12.00\">LessThan</text>\n",
       "<text text-anchor=\"middle\" x=\"164\" y=\"-217.4\" font-family=\"Times,serif\" font-size=\"12.00\">w &lt;= d</text>\n",
       "</g>\n",
       "<!-- 139952677304360&#45;&gt;139955138902448 -->\n",
       "<g id=\"edge11\" class=\"edge\"><title>139952677304360&#45;&gt;139955138902448</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M93.125,-279.891C103.901,-272.001 119.591,-260.513 133.472,-250.351\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"135.819,-252.97 141.82,-244.239 131.684,-247.322 135.819,-252.97\"/>\n",
       "</g>\n",
       "<!-- 139952677302960 -->\n",
       "<g id=\"node4\" class=\"node\"><title>139952677302960</title>\n",
       "<polygon fill=\"palegreen\" stroke=\"black\" points=\"187,-301 133,-301 133,-280 187,-280 187,-301\"/>\n",
       "<text text-anchor=\"middle\" x=\"160\" y=\"-287.4\" font-family=\"Times,serif\" font-size=\"12.00\">d</text>\n",
       "</g>\n",
       "<!-- 139952677302960&#45;&gt;139952677203360 -->\n",
       "<g id=\"edge3\" class=\"edge\"><title>139952677302960&#45;&gt;139952677203360</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M146.875,-279.891C136.099,-272.001 120.409,-260.513 106.528,-250.351\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"108.316,-247.322 98.1799,-244.239 104.181,-252.97 108.316,-247.322\"/>\n",
       "</g>\n",
       "<!-- 139952677302960&#45;&gt;139955138902448 -->\n",
       "<g id=\"edge12\" class=\"edge\"><title>139952677302960&#45;&gt;139955138902448</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M160.625,-279.891C161.067,-273.092 161.683,-263.621 162.268,-254.628\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"165.772,-254.687 162.928,-244.481 158.786,-254.233 165.772,-254.687\"/>\n",
       "</g>\n",
       "<!-- 139955138903568 -->\n",
       "<g id=\"node5\" class=\"node\"><title>139955138903568</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"335.5,-104 104.5,-104 104.5,-70 335.5,-70 335.5,-104\"/>\n",
       "<text text-anchor=\"middle\" x=\"220\" y=\"-90.4\" font-family=\"Times,serif\" font-size=\"12.00\">And</text>\n",
       "<text text-anchor=\"middle\" x=\"220\" y=\"-77.4\" font-family=\"Times,serif\" font-size=\"12.00\">(◻ [0, inf]( x &lt;= c )) ∧ (◻ [0, inf]( w &lt;= d ))</text>\n",
       "</g>\n",
       "<!-- 139955138903568&#45;&gt;139952677303688 -->\n",
       "<g id=\"edge4\" class=\"edge\"><title>139955138903568&#45;&gt;139952677303688</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M202.937,-69.8849C193.924,-61.3722 182.696,-50.7684 172.744,-41.3696\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"175.114,-38.7935 165.441,-34.4717 170.308,-43.8826 175.114,-38.7935\"/>\n",
       "</g>\n",
       "<!-- 139952677203304 -->\n",
       "<g id=\"node6\" class=\"node\"><title>139952677203304</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"344.5,-174 237.5,-174 237.5,-140 344.5,-140 344.5,-174\"/>\n",
       "<text text-anchor=\"middle\" x=\"291\" y=\"-160.4\" font-family=\"Times,serif\" font-size=\"12.00\">Always</text>\n",
       "<text text-anchor=\"middle\" x=\"291\" y=\"-147.4\" font-family=\"Times,serif\" font-size=\"12.00\">◻ [0, inf]( x &lt;= c )</text>\n",
       "</g>\n",
       "<!-- 139952677203304&#45;&gt;139955138903568 -->\n",
       "<g id=\"edge5\" class=\"edge\"><title>139952677203304&#45;&gt;139955138903568</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M274.174,-139.885C265.373,-131.456 254.431,-120.976 244.69,-111.646\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"246.841,-108.861 237.198,-104.472 242,-113.916 246.841,-108.861\"/>\n",
       "</g>\n",
       "<!-- 139952677203136 -->\n",
       "<g id=\"node7\" class=\"node\"><title>139952677203136</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"322.5,-244 259.5,-244 259.5,-210 322.5,-210 322.5,-244\"/>\n",
       "<text text-anchor=\"middle\" x=\"291\" y=\"-230.4\" font-family=\"Times,serif\" font-size=\"12.00\">LessThan</text>\n",
       "<text text-anchor=\"middle\" x=\"291\" y=\"-217.4\" font-family=\"Times,serif\" font-size=\"12.00\">x &lt;= c</text>\n",
       "</g>\n",
       "<!-- 139952677203136&#45;&gt;139952677203304 -->\n",
       "<g id=\"edge6\" class=\"edge\"><title>139952677203136&#45;&gt;139952677203304</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M291,-209.885C291,-202.374 291,-193.234 291,-184.731\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"294.5,-184.472 291,-174.472 287.5,-184.472 294.5,-184.472\"/>\n",
       "</g>\n",
       "<!-- 139952677306320 -->\n",
       "<g id=\"node8\" class=\"node\"><title>139952677306320</title>\n",
       "<polygon fill=\"lightskyblue\" stroke=\"black\" points=\"294,-301 240,-301 240,-280 294,-280 294,-301\"/>\n",
       "<text text-anchor=\"middle\" x=\"267\" y=\"-287.4\" font-family=\"Times,serif\" font-size=\"12.00\">x</text>\n",
       "</g>\n",
       "<!-- 139952677306320&#45;&gt;139952677203136 -->\n",
       "<g id=\"edge7\" class=\"edge\"><title>139952677306320&#45;&gt;139952677203136</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M270.75,-279.891C273.461,-272.944 277.26,-263.208 280.837,-254.043\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"284.193,-255.069 284.568,-244.481 277.672,-252.524 284.193,-255.069\"/>\n",
       "</g>\n",
       "<!-- 139952677304248 -->\n",
       "<g id=\"node9\" class=\"node\"><title>139952677304248</title>\n",
       "<polygon fill=\"palegreen\" stroke=\"black\" points=\"366,-301 312,-301 312,-280 366,-280 366,-301\"/>\n",
       "<text text-anchor=\"middle\" x=\"339\" y=\"-287.4\" font-family=\"Times,serif\" font-size=\"12.00\">c</text>\n",
       "</g>\n",
       "<!-- 139952677304248&#45;&gt;139952677203136 -->\n",
       "<g id=\"edge8\" class=\"edge\"><title>139952677304248&#45;&gt;139952677203136</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M331.5,-279.891C325.79,-272.575 317.664,-262.164 310.189,-252.585\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"312.775,-250.211 303.863,-244.481 307.257,-254.518 312.775,-250.211\"/>\n",
       "</g>\n",
       "<!-- 139955138902784 -->\n",
       "<g id=\"node10\" class=\"node\"><title>139955138902784</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"219,-174 109,-174 109,-140 219,-140 219,-174\"/>\n",
       "<text text-anchor=\"middle\" x=\"164\" y=\"-160.4\" font-family=\"Times,serif\" font-size=\"12.00\">Always</text>\n",
       "<text text-anchor=\"middle\" x=\"164\" y=\"-147.4\" font-family=\"Times,serif\" font-size=\"12.00\">◻ [0, inf]( w &lt;= d )</text>\n",
       "</g>\n",
       "<!-- 139955138902784&#45;&gt;139955138903568 -->\n",
       "<g id=\"edge9\" class=\"edge\"><title>139955138902784&#45;&gt;139955138903568</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M177.271,-139.885C184.076,-131.623 192.502,-121.39 200.069,-112.202\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"202.78,-114.416 206.435,-104.472 197.376,-109.966 202.78,-114.416\"/>\n",
       "</g>\n",
       "<!-- 139955138902448&#45;&gt;139955138902784 -->\n",
       "<g id=\"edge10\" class=\"edge\"><title>139955138902448&#45;&gt;139955138902784</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M164,-209.885C164,-202.374 164,-193.234 164,-184.731\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"167.5,-184.472 164,-174.472 160.5,-184.472 167.5,-184.472\"/>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
       "<graphviz.dot.Digraph at 0x7f49459dbb70>"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "formula2 = ϕ2 & formula\n",
    "print(formula2)\n",
    "viz.make_stl_graph(formula2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "tensor([[[-0.8992],\n",
       "         [-0.8980],\n",
       "         [-0.8951],\n",
       "         [-0.8892],\n",
       "         [-0.8778],\n",
       "         [-0.8578],\n",
       "         [-0.8262],\n",
       "         [-0.7807],\n",
       "         [-0.7221],\n",
       "         [-0.6549],\n",
       "         [-0.5885],\n",
       "         [-0.5344],\n",
       "         [-0.5040],\n",
       "         [-0.5040],\n",
       "         [-0.5344],\n",
       "         [-0.5885],\n",
       "         [-0.6549],\n",
       "         [-0.7218],\n",
       "         [-0.7801],\n",
       "         [-0.8246],\n",
       "         [-0.8542],\n",
       "         [-0.8699],\n",
       "         [-0.8737],\n",
       "         [-0.8670],\n",
       "         [-0.8506],\n",
       "         [-0.8257],\n",
       "         [-0.7943],\n",
       "         [-0.7604],\n",
       "         [-0.7295],\n",
       "         [-0.7078]]], grad_fn=<MinBackward0>)"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# any of the inputs will work\n",
    "inputs = (w, (x_exp, w_exp))\n",
    "# inputs = (w_exp, (x_exp, w_exp))\n",
    "# inputs = (w, (x, w))\n",
    "\n",
    "pscale = 1     # \"pscale\" is the scale used for evaluting predicates\n",
    "scale = -1     # \"scale\" is the scale used in the maxish/minish function. <0 defaults to the true min/max\n",
    "formula2(inputs, pscale=pscale, scale=scale)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Testing grad functionality"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "◻ [0, inf]( x <= c )\n"
     ]
    },
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
       " -->\n",
       "<!-- Title: %3 Pages: 1 -->\n",
       "<svg width=\"134pt\" height=\"169pt\"\n",
       " viewBox=\"0.00 0.00 134.00 169.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 165)\">\n",
       "<title>%3</title>\n",
       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-165 130,-165 130,4 -4,4\"/>\n",
       "<!-- 139952677177664 -->\n",
       "<g id=\"node1\" class=\"node\"><title>139952677177664</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"116.5,-34 9.5,-34 9.5,-0 116.5,-0 116.5,-34\"/>\n",
       "<text text-anchor=\"middle\" x=\"63\" y=\"-20.4\" font-family=\"Times,serif\" font-size=\"12.00\">Always</text>\n",
       "<text text-anchor=\"middle\" x=\"63\" y=\"-7.4\" font-family=\"Times,serif\" font-size=\"12.00\">◻ [0, inf]( x &lt;= c )</text>\n",
       "</g>\n",
       "<!-- 139952677178952 -->\n",
       "<g id=\"node2\" class=\"node\"><title>139952677178952</title>\n",
       "<polygon fill=\"orange\" stroke=\"black\" points=\"94.5,-104 31.5,-104 31.5,-70 94.5,-70 94.5,-104\"/>\n",
       "<text text-anchor=\"middle\" x=\"63\" y=\"-90.4\" font-family=\"Times,serif\" font-size=\"12.00\">LessThan</text>\n",
       "<text text-anchor=\"middle\" x=\"63\" y=\"-77.4\" font-family=\"Times,serif\" font-size=\"12.00\">x &lt;= c</text>\n",
       "</g>\n",
       "<!-- 139952677178952&#45;&gt;139952677177664 -->\n",
       "<g id=\"edge1\" class=\"edge\"><title>139952677178952&#45;&gt;139952677177664</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M63,-69.8849C63,-62.3737 63,-53.2345 63,-44.7315\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"66.5001,-44.4717 63,-34.4717 59.5001,-44.4718 66.5001,-44.4717\"/>\n",
       "</g>\n",
       "<!-- 139952677176600 -->\n",
       "<g id=\"node3\" class=\"node\"><title>139952677176600</title>\n",
       "<polygon fill=\"lightskyblue\" stroke=\"black\" points=\"54,-161 0,-161 0,-140 54,-140 54,-161\"/>\n",
       "<text text-anchor=\"middle\" x=\"27\" y=\"-147.4\" font-family=\"Times,serif\" font-size=\"12.00\">x</text>\n",
       "</g>\n",
       "<!-- 139952677176600&#45;&gt;139952677178952 -->\n",
       "<g id=\"edge2\" class=\"edge\"><title>139952677176600&#45;&gt;139952677178952</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M32.625,-139.891C36.8211,-132.722 42.7562,-122.583 48.2682,-113.167\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"51.3214,-114.879 53.3527,-104.481 45.2803,-111.343 51.3214,-114.879\"/>\n",
       "</g>\n",
       "<!-- 139952677176824 -->\n",
       "<g id=\"node4\" class=\"node\"><title>139952677176824</title>\n",
       "<polygon fill=\"palegreen\" stroke=\"black\" points=\"126,-161 72,-161 72,-140 126,-140 126,-161\"/>\n",
       "<text text-anchor=\"middle\" x=\"99\" y=\"-147.4\" font-family=\"Times,serif\" font-size=\"12.00\">c</text>\n",
       "</g>\n",
       "<!-- 139952677176824&#45;&gt;139952677178952 -->\n",
       "<g id=\"edge3\" class=\"edge\"><title>139952677176824&#45;&gt;139952677178952</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M93.375,-139.891C89.1789,-132.722 83.2438,-122.583 77.7318,-113.167\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"80.7197,-111.343 72.6473,-104.481 74.6786,-114.879 80.7197,-111.343\"/>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
       "<graphviz.dot.Digraph at 0x7f49459dba58>"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "x_exp = Expression('x', x)\n",
    "w_exp = Expression('w', w)\n",
    "c_exp = Expression('c', c)\n",
    "d_exp = Expression('d', d)\n",
    "lt = x_exp <= c_exp\n",
    "gt = w_exp <= d_exp\n",
    "formula = stlcg.Always(subformula=lt)\n",
    "inputs = x\n",
    "var_dict = {'c': c}\n",
    "print(formula)\n",
    "viz.make_stl_graph(formula)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [],
   "source": [
    "learning_rate = 0.05\n",
    "device = torch.device(\"cpu\")\n",
    "optimizer = torch.optim.Adam(var_dict.values(), lr=learning_rate)\n",
    "scale = 0.5\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "iteration: 0 -- loss: 36.224 ---- c:1.000 ---- scale:0.500 ---- true value:0.500\n",
      "iteration: 500 -- loss: 0.001 ---- c:2.488 ---- scale:1.500 ---- true value:1.988\n",
      "iteration: 1000 -- loss: 0.000 ---- c:1.569 ---- scale:2.500 ---- true value:1.069\n",
      "iteration: 1500 -- loss: 0.000 ---- c:1.190 ---- scale:3.500 ---- true value:0.690\n",
      "iteration: 2000 -- loss: 0.000 ---- c:0.988 ---- scale:4.500 ---- true value:0.488\n",
      "iteration: 2500 -- loss: 0.000 ---- c:0.866 ---- scale:5.500 ---- true value:0.366\n",
      "iteration: 3000 -- loss: 0.000 ---- c:0.787 ---- scale:6.500 ---- true value:0.287\n",
      "iteration: 3500 -- loss: 0.000 ---- c:0.732 ---- scale:7.500 ---- true value:0.232\n",
      "iteration: 4000 -- loss: 0.000 ---- c:0.692 ---- scale:8.500 ---- true value:0.192\n",
      "iteration: 4500 -- loss: 0.000 ---- c:0.663 ---- scale:9.500 ---- true value:0.163\n",
      "iteration: 5000 -- loss: 0.000 ---- c:0.640 ---- scale:10.500 ---- true value:0.140\n",
      "iteration: 5500 -- loss: 0.000 ---- c:0.623 ---- scale:11.500 ---- true value:0.123\n",
      "iteration: 6000 -- loss: 0.000 ---- c:0.608 ---- scale:12.500 ---- true value:0.108\n",
      "iteration: 6500 -- loss: 0.000 ---- c:0.597 ---- scale:13.500 ---- true value:0.097\n",
      "iteration: 7000 -- loss: 0.000 ---- c:0.587 ---- scale:14.500 ---- true value:0.087\n",
      "iteration: 7500 -- loss: 0.000 ---- c:0.579 ---- scale:15.500 ---- true value:0.079\n",
      "iteration: 8000 -- loss: 0.000 ---- c:0.572 ---- scale:16.500 ---- true value:0.072\n",
      "iteration: 8500 -- loss: 0.000 ---- c:0.566 ---- scale:17.500 ---- true value:0.066\n",
      "iteration: 9000 -- loss: 0.000 ---- c:0.561 ---- scale:18.500 ---- true value:0.061\n",
      "iteration: 9500 -- loss: 0.000 ---- c:0.556 ---- scale:19.500 ---- true value:0.056\n",
      "iteration: 10000 -- loss: 0.000 ---- c:0.552 ---- scale:20.500 ---- true value:0.052\n",
      "iteration: 10500 -- loss: 0.000 ---- c:0.548 ---- scale:21.500 ---- true value:0.048\n",
      "iteration: 11000 -- loss: 0.000 ---- c:0.545 ---- scale:22.500 ---- true value:0.045\n",
      "iteration: 11500 -- loss: 0.000 ---- c:0.542 ---- scale:23.500 ---- true value:0.042\n",
      "iteration: 12000 -- loss: 0.000 ---- c:0.539 ---- scale:24.500 ---- true value:0.039\n",
      "iteration: 12500 -- loss: 0.000 ---- c:0.537 ---- scale:25.500 ---- true value:0.037\n",
      "iteration: 13000 -- loss: 0.000 ---- c:0.535 ---- scale:26.500 ---- true value:0.035\n",
      "iteration: 13500 -- loss: 0.000 ---- c:0.533 ---- scale:27.500 ---- true value:0.033\n",
      "iteration: 14000 -- loss: 0.000 ---- c:0.531 ---- scale:28.500 ---- true value:0.031\n",
      "iteration: 14500 -- loss: 0.000 ---- c:0.529 ---- scale:29.500 ---- true value:0.029\n",
      "iteration: 15000 -- loss: 0.000 ---- c:0.528 ---- scale:30.500 ---- true value:0.028\n",
      "iteration: 15500 -- loss: 0.000 ---- c:0.526 ---- scale:31.500 ---- true value:0.026\n",
      "iteration: 16000 -- loss: 0.000 ---- c:0.525 ---- scale:32.500 ---- true value:0.025\n",
      "iteration: 16500 -- loss: 0.000 ---- c:0.524 ---- scale:33.500 ---- true value:0.024\n",
      "iteration: 17000 -- loss: 0.000 ---- c:0.523 ---- scale:34.500 ---- true value:0.023\n",
      "iteration: 17500 -- loss: 0.000 ---- c:0.522 ---- scale:35.500 ---- true value:0.022\n",
      "iteration: 18000 -- loss: 0.000 ---- c:0.521 ---- scale:36.500 ---- true value:0.021\n",
      "iteration: 18500 -- loss: 0.000 ---- c:0.520 ---- scale:37.500 ---- true value:0.020\n",
      "iteration: 19000 -- loss: 0.000 ---- c:0.519 ---- scale:38.500 ---- true value:0.019\n",
      "iteration: 19500 -- loss: 0.000 ---- c:0.518 ---- scale:39.500 ---- true value:0.018\n"
     ]
    }
   ],
   "source": [
    "\n",
    "for i in range(20000):\n",
    "    sc = scale + i/500\n",
    "    loss = formula.robustness(inputs, scale=sc).mean()**2 #+ 0.001*(c**2 + d**2)\n",
    "    if i % 500 == 0:\n",
    "        print_learning_progress(formula, inputs, var_dict, i, loss, sc)\n",
    "    loss.backward()\n",
    "    with torch.no_grad():\n",
    "        c -= learning_rate * c.grad\n",
    "        c.grad.zero_()\n",
    "#         d -= learning_rate * d.grad\n",
    "#         d.grad.zero_()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "tensor(0.5172, requires_grad=True)"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "c"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "@webio": {
   "lastCommId": null,
   "lastKernelId": null
  },
  "kernelspec": {
   "display_name": "Python 3.5 (stlcg)",
   "language": "python",
   "name": "stlcg-env"
  },
  "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.5.2"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}