{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 76,
   "metadata": {
    "collapsed": false,
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "The autoreload extension is already loaded. To reload it, use:\n",
      "  %reload_ext autoreload\n"
     ]
    }
   ],
   "source": [
    "%load_ext autoreload\n",
    "%autoreload 2\n",
    "import networkx as nx\n",
    "import numpy as np\n",
    "from nxpd import draw, nxpdParams\n",
    "nxpdParams['show'] = 'ipynb'\n",
    "from utils import *"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Problem Set - Temporal Logic\n",
    "In this problem set, we are going to build a model of a linear temporal logic\n",
    "\n",
    "1. [LTL Modeling](#ltl-modeling)\n",
    "2. [LTL to Buchi Automata](#ltl-to-buchi)\n",
    "3. [LTL to PDDL](#ltl-to-pddl)\n",
    "  1. [Elevator Example](#elevator-example)\n",
    "  2. [Elevator Problem Revisited](#elevator-problem)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# LTL Modeling: Modeling a Dog’s Life <a id=\"ltl-modeling\"/>\n",
    "\n",
    "They say a dog is a man’s best friend. They’re always there for you, willing to let you pet them, ridiculously excited about running after a slobbery tennis ball, and overall pretty great :) This next part of the pset is to develop a set of LTL sentences to model certain aspects of a dog’s life.\n",
    "\n",
    "If you have any questions on this Part 1 (LTL Modeling), please feel free to email ellies@mit.edu\n",
    "\n",
    "## Stage 1: Puppy Life <a id=\"puppy-life\" />\n",
    "Several Hints will be given in stage one to get you started.  \n",
    "\n",
    "<img src=\"puppy.png\" style=\"width: 500px;\"/>\n",
    "\n",
    "### Statements to Model about Puppies \n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Modeling Each Condition Seperately\n",
    "\n",
    "<br/>\n",
    "<div class=\"alert alert-info\">\n",
    "Remember that the Logical Operators for LTL are as follows:\n",
    "</div>\n",
    "\n",
    "•\tand = ^\n",
    "\n",
    "•\tnot (just write not)\n",
    "\n",
    "•\tor (just write or)\n",
    "\n",
    "•\timplies = ->\n",
    "\n",
    "•\tif and only if = <->\n",
    "\n",
    "\n",
    "\n",
    "<br/>\n",
    "<div class=\"alert alert-info\">\n",
    "\n",
    "And the Temporal Operators for LTL are as follows: N = next, F = future/eventually, G = global/always, U = until, R = release\n",
    "\n",
    "</div>\n",
    "\n",
    "### States:\n",
    "h = happy, f = being fed, t = going to the bathroom, c = chewing/biting, b = being born, p = being a puppy, r = running\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "\n",
    "#### Let's model this example together:\n",
    "\n",
    "•\tIf a dog is a puppy, it is happy. \n",
    "\n",
    "This is representative of the implies condition, stating that whenever the dog is a puppy, it is  happy\n",
    "\n",
    "p->h is the correct way to model this; \n",
    "\n",
    "#### Now it's your turn!"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "•\tA puppy must always be fed at some point in the future, and after a puppy is fed, it must go to the bathroom immediately after it is fed(Think global & future & implies) \n",
    "\n",
    "(ignore the fact that it has to be a puppy for this to hold, just for this subproblem - ie, you don't need to do p -> ...)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "•\tThe first thing that happens in a dogs’s life is that it is born (Think how to ensure a state is true in the first state)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "•\tWhen a dog is a puppy, it is chewing something or running. \n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Stage 2: Adult Doggy Life\n",
    "\n",
    "<img src=\"dog.svg\" style=\"width: 500px;\">\n",
    "\n",
    "### Old States:\n",
    "h = happy, f = being fed, p = going to the bathroom/peeing, c = chewing/biting, b = being born, p = being a puppy\n",
    "\n",
    "### Additional States:\n",
    "a = adult dog, s = sleeping dog, k = hunting, w = hiking\n",
    "\n",
    "### Statements to Model about Adult Dogs\n",
    "\n",
    "\n",
    "#### Let's begin by modeling everything seperately again\n",
    "\n",
    "•\tA dog is a puppy until it is an adult dog, at which point it transitions from being a puppy into an adult dog forever\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "\n",
    "•\tAt any given point in time, there will come another time when the adult dog needs to be fed (Think Always Eventually), but now, it has to go to the bathroom sometime after it is fed, but not necessarily right away after.\n",
    "\n",
    "(Again, ignore the fact that it has to be an adult dog for this to hold, just for this subproblem)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "•\tAt any given point, there will come a time in the future when the dog (regardless of whether it is a puppy or adult dog ) needs to sleep \n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "•\tNow, the adult dog must go hunting or hiking at least once at some point in the future\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Combine\n",
    "Please combine all the statements now into one statement about dogs modeling these aspects of their life. Be ensure to have distinguishing information for puppies & adult dogs. Some statements apply to just dogs in general. This is kind of tricky, so if it doesn't come to you in more than 10 minutes, feel free to just put down what you have so far and points won't be taken off.\n",
    "\n",
    "Hint: Setup is something like (information about all dogs) AND (information about puppies UNTIL ALWAYS information about adult dogs)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# LTL to Buchi Automata <a id=\"ltl-to-buchi\"/>\n",
    "\n",
    "Now that you've had some practice writing LTL formulas, we are going to practice converting some simple LTL formulas to Buchi automata. Buchi automata are extensions of finite state machines used to capture temporal goals expressed by LTL on an infinite timeline. Converting LTL to Buchi automata is the first step to generating actual plans with temporally extended goals.\n",
    "\n",
    "In this section, we will be using the Python library NetworkX for building graphs and nxpd for drawing graphs. The examples below should be enough to create your graphs but you can find the documentation here: https://networkx.readthedocs.io/en/stable/"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## LTL Operators to Buchi Automata\n",
    "\n",
    "In lecture, we saw how to convert a couple of the LTL operators to Buchi automata. To get started, we are just going to convert the rest of the LTL operators to Buchi automata. You can find the examples of LTL operators converted in lecture below. (Note: We will use '!' to represent the logical operator \"not\")\n",
    "\n",
    "**F**uture - **F**p"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAALAAAABwCAIAAAAxPW29AAAABmJLR0QA/wD/AP+gvaeTAAAYfElE\nQVR4nO2deVxTV9rHz80eEnYBQUoSWYKApVQWLTgSBB0XtIqitKgFpTNVtB1UUIG2ih1Hu0hph+IU\nnYEirbX9OJV+iguSOsqmQZyigDQaxApY1kIggWzvH2eaN1y25OYCMeb7V+7JWR4efrn33HvP8xxE\npVIBEyZ+hzDdBpgwLEyCMDEMkyBMDMMkCBPDMAnCxDBMgjAxDJMgTAzDJAgTwzAJwsQwTIKYBvh8\nPoIgFhYWzz//fFBQEIIgNBotKCjIx8eHRqMhCNLa2jpdtpGma+BnmYGBgdDQ0O+//57BYAAAEARh\ns9lVVVUAgM7Ozvnz50skkumyzXSGmAYkEklycjJUAwpbW9vt27dPoyAQ08utqWdgYIBCoZBI/zs9\nIwjC5XIbGhrgoVQqJRAIFAplWmzD5wzx7bffurq6trW14dKb0WNmZqZWw0jIZHJ5eflbb73FZrNb\nWloWLVrk4uJy5MgRBEEQBAEA9Pb2fvjhh+pDAIBYLD58+HBcXJy/v394eHhtbS1241R48MYbbwAA\nfvjhB1x6e9YAAHC5XPWhVCotKyuj0WgAgCNHjly+fHnr1q19fX2zZ8/W/H+pD5VK5aZNm+rr62F5\nRESEvb39b7/9htEYPf6Q/ycjIwMAUF5ejktvzxooQUDc3d0BAJ2dneoSLperKQj14bVr10b+zouK\nirAZg89dBovFAgCw2WxcejMBACAQCAAAGxubCWvevHnTy8vr7t27+IyLSy9sNptKpTo4OKhUqoqK\nit27d7PZ7Obm5hUrVlhZWQUGBv7nP//BZSATIxGLxSKRqL+/X7NQoVBg6w0fQXA4HBaLRSAQlEpl\nZ2dndnb2w4cPP/nkk5SUlOzs7Pr6+sWLF6tn0SY0UWl9lwenkFKpFB4ODQ3B5l5eXhKJ5OjRo+qa\ndXV1n376KXaD9EehUERGRqoP4fVvcHAQHh4/fhwAkJCQgMtYRkZfXx8AwMXFBVUOr78ymUxdsnbt\nWgDAgQMHGhsbP/nkE3g1KS4uHhgYgA6Pj48vKChITU2NiIiY5kmlSqV677331J9R05/79+8DAObP\nn4/XWEbDhQsXXnvtNfjLTElJKSsrU6lUYrH40KFDsHDXrl23bt2ClUUiEY/HMzMzCwwMrKmpCQkJ\niY2NLSwslEqlzc3Nq1evtra2dnBwSEhI+PXXXzGbhJsgBAKB+jNKEPC5W0REBF5jmZg8cHt0PW/e\nvLG+6uzsBAAsWrQIr7FMTB74COKLL75wcXF58OCBZqF6oltSUuLp6ZmUlITLWCYmFXwEMTQ0JJfL\nZTKZZmFubm5HR0dHR0dra2tlZSWdTsdlLBOTyqS83PL09Lx3795k9PxMIRQKP//88x9//PHRo0dS\nqdTOzo7D4bz66qtRUVFmZmaTNKhJEIaIVCrdv3//p59+6uzsvHbtWvhgu62t7fbt2xcvXrS2ts7K\nyoqKipqUsSdjpurk5AQ0nkOY0ImOjg5/f38rK6uTJ09qPoeA/PbbbwkJCQCAAwcOTMboOAuir69v\n7969UGpbtmyBN9YmtGdgYMDPz4/D4dy/f3+cav/4xz8QBDl69CjuBuApiK6urmPHjgUHBzs5OVlb\nW3O53BUrVpw9e9Z0qtCexMREKyurBw8eTFjz/fffJ5FIlZWV+BqA2xwiLy/vL3/5C4VCWbdu3fPP\nP69UKtva2q5fv87n8318fM6cOePp6YnLQEaMQCAICgrKy8uLjY2dsLJKpVq2bFlzc3NtbS2RSMTN\nCFxklZ6ejiBIenp6f38/6qv6+np/f38mk3njxg1cxjJiFi9eHBISolQqtawvFAqJRGJBQQGONuAg\niOzsbAKB8MUXX4xVYXBwcOXKlQ4ODk1NTfoPZ6z897//BQBcvHhRp1avvvqqj48PjmboK4iGhgY6\nnX7w4MHxq/X39/v5+S1dulTP4YyYN99809PTU/vTA6S8vBxea/AyQ19BREZG+vn5jbw7GklVVRWB\nQDh79qyeIxolCoVi1qxZb7/9tq4NlUrl7Nmzd+/ejZclegmipqYGQZDvv/9ey/oxMTEvvviiPiMa\nKzU1NQCA6upqDG13797t7e2NlyV6CSIxMdHT01P7+pWVlQCAa9eu6TOoUXL8+HFbW1uFQqFrw76+\nvsLCQgRBBAKBUCgUCAQCgUCfuRp2QSiVSnt7+7/+9a86tfLx8dm1axfmQY2VLVu2/PGPf9S+/viv\njm1tbTFbgv1t5507d3799dfly5fr1GrVqlVFRUWYBzVWGhsb4aoiLXnuuefUUTooSCTSH/7wB8yW\nYBdEWVmZpaWlj4+PTq2WLFkiEomampowj2uUNDY2wnWRWrJ58+axYr8UCkV0dDRmS7AL4urVqyEh\nIbo+IwsICCASiQKBAPO4xkdXV1dnZ6eHh4f2TWxsbFatWkUmk0d+RSKRVq5cidkY7IE6AoFg8+bN\n2tRsaGiAC68h5ubmWVlZak0wmcy33nqLyWRituRp55dffgEAuLi46NRq69at3377LaqQSCSGh4fr\n5UxsUw+lUkmj0fLz87WpfOnSJWgrmUwmk8kkEon6O/C899NPP2EzwzioqKgAADQ3N+vUSqFQzJw5\nE/XfJBAIJ0+e1McYjJeMrq4uqVQK1z1MSFhYmLW1tUKhkMlkMplMLpcP/o5CofDy8po7dy42M4wD\nGHuj6xJDAoEQHx+PyhqAIMjq1av1MQajIFpaWgAAWgqCSCRGRUWNmvCASCTGx8djs8FogGEKMNxb\nJ1577TXNdawEAiE4ONjW1lYfYzAKAqaCGHnKGovo6GgYeoZCpVJp86rXuIFnCAyCcHd3DwoKUs/r\nEQRZv369nsZgFAT871KpVC3r83g8KysrVCGJRAoPD3dwcMBmg9EAJ1KoNetaAgMk4WelUrlmzRp9\njcHWDKpSqVRqOwyJtHbt2oKCAs3zhFKpVAeyPcvAKM3u7m7UNKKvr+/Bgwc9PT3d3d0ymYzBYFhb\nW9va2s6ePVv9EGLDhg2JiYkSiQRBED8/v1mzZulpDEZBwOwFOsWcR0dHnzp1SrPEzMzs5ZdfxmaA\nMWFtbQ0A6O7utrW1raqqKi0tLSsra2hogLejI6FQKG5ubnPnzl20aBGPx4uKivr6669VKtW6dev0\nN2aKzhAAgLCwMAsLi97eXnhIoVBiYmIwXDiNDwsLCwBAUlJSWVlZf38/l8vl8XiRkZFubm4cDodO\np1taWgIA5HJ5X19fd3e3UCgUCoU1NTVpaWldXV2Ojo7wvKv/BAIArM8hrl69CgBoa2vTqVVcXJzm\nwzXTa0+JRJKdnQ3z78ydO/ezzz7T6WmEXC6/cePGvn374O9zyZIlV69e1dMkjIJobGwEAKgj1bXk\nhx9+UKvBxcVF19VBxoRCocjNzXVycmIwGElJSXouLrxw4cKxY8eWLl0KAFi0aJGu/xdNMApiYGAA\nAHD+/HmdWg0NDZmbmwMAyGTyu+++i21oI0AgEAQGBpLJ5L1793Z0dODY882bN0NDQ4lE4htvvNHd\n3Y2hB4xzCDqdbmtrC2c9YrH4+vXr169fr6uru3v3bnt7u7oakUhks9ne3t6+vr6hoaG+vr6rV68u\nLCyUy+WvvPIKtqGfalQqVWZm5r59+wICAm7dujXqu2Kd/Aln92r8/f1LS0vz8/P37t178eLFM2fO\n+Pv762Qh9rgMX19fNzc3iURy+fJluVzO4XD8/Py8vb2dnZ3VdWQyWWNj4507d27dutXT02Nra/vS\nSy8VFRUtWLAArg59pujv74+NjT1//nx6enp6ejrqRfHQ0ND58+dPnTqlkz9jYmLi4uJefPFF1Fgt\nLS2vvPJKRUVFVlbWn/70Jx2sxHBW6enp+dvf/mZlZUUkEiMjIwsLCx8/fjx+E4VCcfv27WPHjnl7\newMA3N3dv/vuu2dqDtHR0REUFGRjY3P58mXUV9Cfjo6OJBJJV3/Cc0xwcPBIf8pksuTkZABAenq6\n9nbqJgilUpmXl2dnZ2dubp6SktLa2qpTc0hpaenKlSsRBAkODq6trcXQw1PHkydP5syZw2Kx6urq\nNMtx8WdFRcU4/jxx4gSJRNq+fbuWvekgiNbW1oiICCKRuGPHDv2nQlVVVfPnzyeTyYcPH8awuPQp\nore3d968ee7u7i0tLZrlU+bPc+fOkUgkLc8T2gqitLTUwcFhzpw5NTU1Ohs7BkqlMicnh06nL168\nuL29Ha9uDQqZTBYeHj5z5kxUNPcU+/Pzzz9HEOTEiRMTdqKVIM6cOUOhUDZt2jQydFN/amtr3d3d\nuVyuUQb6paWl0Wg0VGTVtPgzNTWVSqVO+IhiYkHk5+cTCIQ9e/ZM3hywra3Nz8/P2dnZyDRRUlJC\nIBBQv8vp8qdcLg8LC3N3d+/t7R2n7QSCKCoqIpPJ+/btw8fSsenp6fH19fXw8NAn6aZB0d/fz2az\no6OjNQun15+tra12dnbjx8WMJ4h79+4xmcz4+PipuT9saWlhs9k8Hs845ph79uyxs7PT3N/AEPxZ\nWFhIIBDGSTMypiCkUqmfn5+/v/9U5n8RCARUKjUjI2PKRpwkhEIhhULJyclRlxiIP5VKZWho6MKF\nC8dqMqYg3nnnHSaTKRQKcbZxIj7++GMymXznzp0pHhdf4uLivL29Nc8EhuNPGKI9ViKK0QVx7949\nKpX6wQcfTIqN46JQKAICAhYuXIjveVWpVJaXlyclJbFYrIcPHy5fvtzS0jIgIED/98UjaW5uplAo\nubm56hJD82d4eDiPxxu1/uiC2LBhg5eX19DQ0KTYOBFVVVUIgnz33Xc49imXy4uKiuB6nD179ly9\nevX06dNMJpNEIql3q8KLt99+29HRUfPSYGj+hJEyd+/eHVl5FEHU1tYiCDK9mT3Wrl37wgsv4D75\nmoKNPBQKBYvFSk5OVpcYoD+VSqWrq2tKSsrImqMIYufOnW5ubnK5fHJtHBeYSQL3NJdTsJFHWVkZ\nAEDz+aNh+jM1NZXFYo38yaEFIZVKbWxsjhw5Muk2ToSvry/um/BMwUYeaWlprq6u6kOD9Wd1dTUA\nYOTkHR2Xwefzu7u7DWH1SkxMzLlz53Rax6srk7GRR0lJSXh4uPrQYP3p5+c3Y8aMkpISVDW0IK5c\nueLt7a1rJLIalUp18uTJ9evXp6ambtu2rbCwEFs/AIDly5d3dHTcvn0bcw9jMXkbeQwMDFRXV2sq\nTE9/AgAeP3586tSp6OjoBQsW6GMbyp/wdfkoe36izhiBgYE7duzAfF46ePAgi8Xq6upSqVRdXV0s\nFiszMxNbVwqFYsaMGcePH8dszEjgJSMnJ6e9vb29vf3IkSM9PT0TtoL5xgsLCyd8FwVzHMCdACB6\n+hPS1dUFRtvsVSdG+vPQoUPu7u6oagDVhk6n//Of/8Q2ZFNTE4lE0sw6dfjwYTMzM8wv+5csWRIX\nF4et7aig5hBacvPmTfjjodFoMTExRUVFY91AFhQUkMlkdZJGPf2pif6CUI3w55kzZ4hEolQq1awz\n7JLxyy+/SCQSnVKZaHL69Gm5XL548WJ1SVhY2MDAQG5uLrYOuVzuvXv3sLWdDKRS6TfffLNq1Spz\nc/P169cXFRWhAjKFQiGbzVbH2enpT9xB+dPDw0OhUKDSOw0TxKNHj8Dv+zZj4Pr16wAAzUWhzz33\nHAAAJu3FgIuLCzQJL+AmmaPGoWsJ/PUPDg6eP39+1apVM2bM2Lx5c0lJCfwRd3d329nZqSvr6U/c\nQflzxowZAAB4PVIzTBDQXzB0AgMwaQSMVITAMFaRSIStQ0tLS3Xon56IxeLk5GRo4euvv67/mm+o\nqt7e3rNnz0ZERMyaNevNN9+8f/++ZjofPf2JOyh/QsOgkWqGxWXA/aMZDAa28WCMoma6PPgZ8y+S\nwWCIxeKx8u9hJi8vLy8vD6/eYHaH1tbWrKwsAEBgYKD6Kz39iTsMBkNzi3BomFgs1qwzTBAw38Pg\n4CC2Pb48PT2vXbvW09OjTiTS3d0NtE40M5LBwUEqlfqvf/0LW3O8uH///v79+8epQKVSBwcHPTw8\nGAwGDMxVlwM9/Ik70J/qw1ETlQwTBDyHiMVibH+Al5cXAKClpUUtCHiKDgkJwdAbAKCvr8/S0hKf\noGY9EAgEowoC3lC4uromJCRs3LiRxWLt3LlTc8Kkpz9xp6+vD57F1Yfg9/O6mmFzCDghgumCMLBu\n3ToCgVBaWqou4fP5ZDIZ83O61tZWe3t7bG0nD5gsy9nZ+cCBA3fu3BEKhSkpKXDmqJnvAOjtT9xB\n+bOnpweMLwg3NzcSidTQ0IBtPGdn5/379584cQI6pbe398SJE2lpafBeAwMNDQ06JfydVMhkMoIg\nTCZz48aNxcXFIpHo3XffhYFoambPng2XwMBDPf2pBl749X+Kj/KnUChEEITD4WjWGXbJoFAoHA7n\n7t27mIfMyMjgcDg7duxwcXFpbGxMSUnZtm0b5t7q6uo2btyIuTle2NnZWVhY8Hi82NjYFStWjJM/\nkMvl9vf3t7S0wNQ++vsTAMDn8wsKCgAATU1NH330UVhY2AsvvICtK5Q/GxsbHR0d0TdBqIdZ27Zt\nCw4O1vOJGC7Am9UrV65MtyE68OTJEwDApUuX1CWG7M/4+PiwsDBUNfTLrdDQ0Js3b6LuTacFPp9P\no9H0fKMzxdjb23O5XD6fry4xZH/y+fyFCxeiqqEFERkZSSQSz549O+kGTkRhYeGyZcueui3kw8LC\nNKfVButPkUgkEol4PB663shzy8svvxweHj6556+JaG1tJZFIX3311fSagYGvv/6aRCI9efJEXWKY\n/vz73//OYDAkEgmq5iiCKCoqQhAExyBUDKSkpNjZ2Q0MDEyjDdiQSCRWVlYfffSRusQw/RkYGLh5\n8+aRNUcRhFKp9PX1jYqKmkQDx6W9vd3c3NwQlp1hY8uWLQEBAepDA/Tnzz//jCBIcXHxyMqjLw44\nd+4cgiB8Pn+STByf119/3cHBYfyYVEMG5mzUTLpoaP7cvn27i4vLqJtrjrlaZMWKFd7e3qjVE1NA\nZWUlgUDAd/viqSc0NBR1R2c4/mxqaiKTyZphhpqMKQiRSGRhYbFz5078bRybnp4eV1dXnfanM0yK\ni4sBAJphYYbjzz//+c+Ojo4jp5OQ8daTffnllwiCTNlUX6FQrFmzZubMmbomyDVMVq5ciYrWMgR/\nVlRUjL9R+wQLDBMTE6lUamlpKW5mjs3OnTunbKwpAMZzohYJT68/5XL5ggULQkJCxgmJm0AQCoVi\nw4YNFhYWP/74I26WjkCpVKakpBCJRJjV3WjIyMig0Wi3b99Wl0yvP9955x0ajTZ+5r+JlyAPDg5u\n3LiRTqefO3dOX0tHY2hoKCEhgUwmnz59ejL6n0bkcnloaKiHh4fmDH+6/Hn58mUCgZCdnT1+c63W\npCsUil27diEIsmfPHnxDmEUi0fz58y0sLC5cuIBjt4bD48eP7e3tly5dqum3qfdnXV2djY3N+vXr\nJ+xBhyCFr776ytLScu7cubjcTw8NDb3//vsWFhYBAQFTn0ZjKrlx4waTyYyNjUVduafMn48fP2ax\nWC+99JI2Se90i1ppamqCu8auXr0alWpPe2QyWV5enru7O51Oz8jImMoUO9PFpUuXKBRKbGws6o+d\nAn82Nja6ubl5e3trZrsaByy5rv/973/PmzcPABAWFpafny8Wi7VsKBKJDh48yOFwyGRybGzszz//\njGH0p5RLly4xmczw8PCRuxZMnj/Ly8vt7Oz8/f21z+2Hcb8MlUp15cqV6OhouEFvcHBwcnLyl19+\n+dNPP3V1dcG0ZxKJ5MmTJ9euXfvss8/i4+NhAJOTk9O+ffuMLB+llty4ccPe3t7V1bW6unrkt/j6\nU6lUZmZmUiiUJUuW9PX1aW8kdkFAOjo68vPzoX1jbQzPYDAWLFiwf/9+mPhfzxGfah49erRw4UIq\nlfrhhx+O6gpc/NnS0rJmzRoCgZCWlqarw7HvlzGSwcHB+vr6jo4OGFJNpVLNzc3ZbDabzcY92Obp\nRS6XHzp06OjRo97e3jk5OZqBPSgw+FOhUOTk5KSmplpaWubm5kZEROhsHxadm9CbR48ebdq0CQAQ\nHBys605Vo9Lf35+Zmeni4mJubp6ZmYn5btYkiOmkpKQELmILCgrKysrSXGelPdXV1UlJSU5OTnQ6\nPTEx8eHDh/qYhOclwwQ2Kisrc3Nzv/nmG7FYHBAQAJNIzpkzx9HRcdT6MplMJBLV1NSUlJSUlJQ0\nNTV5enrGxsZu3bpV+93Yx8IkCENBKpUWFxdfuXKFz+fX1dUBABgMxqgbuTY3N8vlcriEmsfjLVu2\nTNed1sbBJAhDpLu7u6Ghob6+ftS9v7lc7pw5c9zd3WFQIb6YBGFiGOi4DBPPOCZBmBjG/wEFUp/f\nUe1IdwAAAABJRU5ErkJggg==\n",
      "text/plain": [
       "<IPython.core.display.Image object>"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "F = nx.DiGraph()\n",
    "F.graph['rankdir'] = 'LR' #Graph should be drawn left to right\n",
    "F.add_node(0, shape='circle')\n",
    "F.add_node(1, shape='doublecircle')\n",
    "F.add_edge(1, 1, label = 'True')\n",
    "F.add_edge(0, 1, label = 'p')\n",
    "F.add_edge(0, 0, label = '!p')\n",
    "draw(F)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**G**lobally - **G**p"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAALUAAABwCAIAAADXFKb5AAAABmJLR0QA/wD/AP+gvaeTAAAcGUlE\nQVR4nO2deVQTydbAq7OyBGQNyA4RiBF9I8gqyADijj4d0YMoLriP+4b45h1FUMf1ecbliI+nIoMz\nZ2Z0ZtwXMOKCyvIGFFmVgGwugAQSCGT7/qjv9ekJISRNB2Yy+f2Vru6qe2luV1dV33sLkcvlQI+e\nPiANtQJ6/tDo7UOPKvT2oUcVevvQowq9fehRhd4+9KhCbx96VKG3Dz2q0NuHHlXo7UOPKvT2oUcV\nevvQowq9fehRhbbsQy6XP336dOvWrS4uLm/fvp0+fbqZmZmfn9/Dhw+1JFGX4HK5CIKYmpqOGTPG\n398fQRADAwN/f38vLy8DAwMEQZqamgZJFbl2kEgk165dMzAwAABs27YtJycnMzOTwWBQKJSysjIt\nCdUZrl+//vnnnwsEAngIAPD09IS/m5ubR4wY8ebNm8HRRFv2AXF3dwcAdHd3w8N//etfAIAVK1Zo\nVagO8OOPP968eRM9xNqHXC4/duxYSUnJ4GiiXfvw9PTEdlFv3rwBAAQEBGhVqA4gFArFYjF6qGAf\nXV1d6COnbQZ1fGpnZwcAMDExGUyhf0aMjIwoFEpfZ6lUam5u7qZNm1xcXBobG0NDQ52cnA4cOIAg\nCIIgAID29vajR4+ihwAAgUCQkpKydOnScePGTZw48eXLl+qqolXrU+g/6uvrAQApKSlaFap7gN/3\nHyKR6MmTJ3Bsd+DAgXv37sXHx3d0dLi5uWHvNnook8kWLVqEDvsiIyOZTCafz1dLNKF/iCLQPiQS\nCTy8cOECm83u7OzUqlDdQ8E+IHBs19LSgpYoPI3o4aNHj3r3C9euXVNH9GC8X9LS0pqbm5ubm5ua\nmp49e2ZoaDgIQnUeEokEALCwsOj3yvz8fA6Ho/CPnzFjhjpS+nzJEciqVavgj507dw6COD0KCAQC\nHo8nFAqNjY3RQqlUSiaT+62rXz/9oyNXOwAFjkZFIhE87OnpgdU5HE5XV9fBgwfRK0tLS0+ePKlO\nm9rtPzo6OgAAPT09NBpNq4J0GKFQCADo6upSKO/u7gYASCQSdKbD4XDKy8uTk5OXLFly584dPp8P\nALhz5860adPc3d2Tk5MbGhrCw8PLysry8vJ++ukntcTjGjD1T0dHx/bt26GIxYsXP3nyREuCdJvb\nt28vWbIE3saEhAR4GwUCwd69e2Hhhg0b/vvf/8KLeTxeWFiYkZGRn5/fb7/9FhwcvHDhwkuXLolE\nordv386aNcvc3NzGxmbFihUfPnxQUwFErrX4uebm5rS0tPv371dWVra3txsZGdna2k6cODEuLo7D\n4WhJqB5i0Yp9SKXSw4cP79u3j06nz5w509fXl0wmd3R08Hi8q1ev1tXVxcTEHDlyBC6X6flDQ3iX\n2N7eHhERYWhoeOjQIaFQqHBWKpX+8ssvLi4uVlZWRUVFhEvXQywE24dIJAoKCrKxsXnx4oWKywQC\nQXh4uKWl5atXr4hVQA+xEGwf69evZzAYqo0D0tnZGRQU5OXlpV9Oxc2DBw9WrVrFZrOtrKyYTKaX\nl9eiRYvu378vlUqJEkGkfTx58gRBkMzMTDWvr62ttbCw2LZtG4E6/EWor6+PjIwEAISGhh48eDA1\nNfWbb77ZuXPnZ599BgCIiIior68nRBCR9uHv7x8ZGalRlVOnThkaGjY0NBCohs5TVFTEZDJHjRql\ndNUgNzcX9ijq9OL9Qph95OTkAACeP3+uUS2RSOTo6Lhp0yai1NB53rx5w2Qyp0+f3nvsjyIUCkND\nQ21sbAbuZkaYfSxYsGD8+PE4Ku7fv9/S0nLQHF7+1IjF4sDAQB8fn34HbW1tbRwOJywsTCaTDUQi\nMfYhEAiMjY1Pnz6No25dXR2JRLpy5Qohmug2Z8+epdFoajrw5uXlkcnkjIyMgUgkxj6uX7+OIMi7\nd+/wVQ8ODo6PjydEEx2mp6fHwcFh/fr16ldZuXKlp6fnQKYzxHy/zcrKGjNmjI2NDY66fD4/KCjo\n3r171dXVlZWVhYWFhYWFHz9+JEQxXeL69etNTU3oVy112Lp1a1VV1a+//opfKm7LwjJhwoQ1a9Zo\nVCU8PFyFVpMnTyZEMV1i1qxZU6dO1bRWZGRkdHQ0bqHE9B/l5eUjR47UqIq9vX1f/ikUCiU0NJQI\nvXSHzs7Ou3fvzp07V9OKc+bMuXnzJuoUojG4LQultbUVAHDnzh2Nail1ikSpqqoauGK6RFZWFgCg\nrq5O04o1NTUAgAcPHuCTS0D/UVlZCQCA3rDqExwczGKxlJ7y8PAYMWLEwBXTJZ4+feri4uLg4KBp\nRWdnZzs7u+fPn+OTS4D/WG1tLZlMdnR01LRifHz87t27xWIxtpBKpc6fP3/gWukYxcXFPj4+al7c\n3Nz8z3/+UyaTwUMKhZKRkQG7eQAAjUb78ssv1Z1M4Ot2sJw/f97Y2BhHxYaGBuiErQDqEKUHxd/f\nf8uWLWpeXF1dDQAgk8lUKpVCoZDJZDqdTqPRqFQqHPOpv9pEwPulq6sLX8iCnZ1dZGQklUrFFjo4\nOIwdO3bgWukY9fX19vb2al7s6ur62WefyWQysVgskUikUml3d3dPT49YLJZKpSYmJlOnTlWzqaG0\nDwDA8uXLJRIJekij0ebNmzdwlXQMqVT67t079e0DABATE6M0QpNGo8XGxsLYO3UYYvuYOXPmsGHD\n0MOenp7Zs2cPXCUd48OHD1KpdPjw4epXiY6Oxj54KD09PXFxceq3Q4B9kMlkhTGm+tBotCVLlqDR\nD1ZWVkFBQQNXSceAkSzqP/QAAFdX19GjR6Px2SgsFiswMFD9dgiYv1hYWKBjYywSiaS6urqlpeXT\np09CoZBKpZqbm5ubm7u5uTEYDPSy+Pj448ePAwBoNNqcOXOUjlj/4sBBJTofUZOYmJiysjLso0ul\nUtFoCTUhxj7a29thoE5ZWRmXy83JyXn58uXr16/76lccHR3ZbPb48ePDw8Nh2qRXr1719PTMmjVr\n4ProHvCZkUqlGtWaN29eYmIitkQikSxatEijRoixD7lcnpCQcOXKlZqaGktLy7CwsIULF7JYrBEj\nRpibm5uamsIngM/nd3V1VVdXv379uqys7NKlS3v27GEwGKNGjZLL5QwGA/rM6VEAX//h5ubm5eVV\nUlKCNhIUFOTs7KyZbHzTcRQulxsQEAAAsLe3T0xMzM/P1+hrcm1t7alTp/z9/QEAxsbGZ86cEYlE\nA1RJ92hpaQEAZGdna1px37596PIBiUQ6f/68pi3gt4+CgoKQkBAEQaZOncrlcgfop3T48OGFCxca\nGRnZ29ufP39+gK3pGDKZzNDQMD09XdOK8NMHxNDQEE14pz547KO1tXXlypUkEikiIoLYtc4PHz5s\n3ryZQqEEBAToV1GxeHh44Mu7BENZaTTawoULcVTXePzx/Pnz+fPnd3V1paenL1y4sPcFUqm0uLj4\nwYMHxcXFpaWlPB4P++K0trYeNWoUh8MJCQkJDg7GZqSAZ48dO7Z48eLVq1cHBgYeOnRow4YNmmqo\nkzg6OtbV1cHfdXV1XC43Ly+vrKysvLwcG9pvZGTEZrNHjhzp5+cXFhbm4OAwb9685OTknp4epf+s\nftEs/vbUqVObN28OCQnJzMy0tbVVOFtYWHju3Lnvv/++tbXVzMzMx8fHy8vL3d0du4JeV1f36tWr\noqIiHo9HpVInTZq0dOnSqKgohQQQUql0z549+/fvnz179sWLF42MjHD8bbrEsmXLamtrp0yZcuHC\nhdLSUiqVOmbMmNGjR48aNcrU1BS9rL29vaSkpKSkpLi4WCKReHl5TZ8+/eDBg7a2tn197eoHNfsZ\nmUwGJ0u7du1C84lBYEgtXNcaPXr04cOHi4uL+x2lNjQ0ZGZmzpgxg0Kh2NnZHTp0qHfGtFu3bpmZ\nmQUFBWGzbP0FKS0tnTRpEoVCsbS0XL9+fXZ2dr8jCYFAkJWVtW7dOktLSwRB/va3v+FLS6yWfchk\nstWrV1MolLS0NIVTL168CAwMRBAkKirq6dOnODRoamrasWMHg8FgMpm9na1LSkqcnJw4HI76KSt0\nCT6fv27dOjKZ7OnpmZ6ejiMKpLu7+9///re7uzuZTN6wYUN7e7tG1dWyj127dlEolF9//RVbKJFI\nkpKSqFRqYGBgfn6+RlJ78/HjxzVr1pDJ5ClTpij4wTc0NLBYLF9f346OjgFK+XORnZ1tb2/PZDLT\n0tIGGFIrkUjOnj1rbW3t4ODA5XLVr9i/fZw+fRpBEIWp8/v372GqmrNnzxI4Fy0sLGSz2ba2tgr+\ncFVVVUwmc/LkyQqvNl1FJpPt3r2bRCItWrTo06dPRDXb2toaGxtLJpOTkpLU/K/1Yx/5+fk0Gm3P\nnj3YQh6P5+Hh4enpqY3sDB0dHQsWLKDT6T/++CO2/NmzZ3Q6XUETnUQsFi9evJhOp1+4cEEb7ael\npdFotKVLl2JTePeFKvvg8/ksFmvSpEnYzo3H49nb2/v4+GhvQCCTyTZv3kwmk7/99lts+YkTJ8hk\nMm5X2z8FEonkiy++YDAYWVlZ2pNy584dBoMBfQBUX6nKPtauXWtra/v+/Xu05P379+7u7mPHjm1r\nayNG077ZsWMHlUq9ceMGtnDOnDlubm7aSxny008/ubm5NTU1aal91chksuXLlxsaGj569Ejbsh4+\nfGhoaLhy5UrVL5o+7SM3N5dEImE7eYlEEhoaymKxcMdRaoRMJouLizMxMcHGOjQ3N1tZWSUmJmpJ\n6Jo1awAA2L01BpPjx4+TyeSrV68Ojriff/6ZRCKdPHlSxTV92kdAQMDEiROxJbt37zYwMPjtt98I\nU7A/RCKRt7f3uHHjsPO6kydP0un0mpoabUhMTk4GAOTm5mqjcdUUFhbS6fS9e/cOplD4P1WRCE65\nfdy4cQNBkOLiYrSkqKiIQqGcOHGCeB1VUlVVxWAwkpOT0RKJROLh4aGlTYYuXrwIAGhsbNRG4yoQ\ni8VjxowJCwsjMDWUOsB3gre3d18DEeX2MWHChClTpqCHUqk0MDAwICBgkLWHHDx40NDQ8PXr12hJ\namoqnU4nKoUSlocPH9LpdKlUKpPJcnNzt2zZ4uzsXFtbO23atGHDhvn6+ubk5BAuVC6XHzlyhE6n\nV1RUaKNx1ZSVldFotOPHjys9q8Q+Xrx4AX7vbXD58mUEQQoLC7Wlo0q6u7s9PDxiY2PREpFIZGNj\nk5SURLisuro6Dw8P+eDun8fn883NzXft2kVss+qzfft2S0tLpUurSuxj69atLBYLHdbKZLIxY8YM\nJAZ84Hz33XckEunly5doyfbt27FKEoVUKo2KikIPB2f/vL1795qbm6u5YY82aGtrMzMzU+o/oGgf\nMpnMwcEBa8swkDovL0+7OqpEIpG4ublt3LgRLSkqKgKapztTh3379qG/B2H/PIlEYm9vv2PHDgLb\nxMG2bdscHR17jx8U7aO4uBgAgH2VLFu2zNvbW+sK9kdKSopCmjIWi6WN5dSCggL0t4J9QE8LTXM0\nqubmzZsIgmBHV0NCZWUlgiC9kzAoOgRkZWVZWVmhEY5SqfTnn39esGCBxn4DRBMTE9PS0oLdXjki\nIgJmPSAWFWHQ0A+U2Nwkly9f9vPz6yuVwaDh7u7u7e19+fJlhXJF+3j06NGECRPQuJrCwsJPnz5N\nmzYNn1S5XP6f//wnOjr6H//4x/Llyy9duoSvHQCAm5vbyJEjsQYxYcKEvLw8/JlPlJGRkeHk5ATj\nm1HQwIKsrCw2m71lyxYCJd69exf37QUANDQ0nDt3bt68eRpFPSll+vTpSp43hf7Ezc0NO045cuQI\nk8nEPQxMSkpydnZubW2Vy+Wtra3Ozs59zaPUATodoodlZWUAAGLX69LS0oYPH15eXg4P4fvlzJkz\nHz9+/Pjx44EDB9T5sFBdXb1y5crr16/39PSovrK2thYMIHkLBAan9d7AUFOgcSisGvzOPjo7OxXW\n1OPi4nDkvILU1NRQKJT9+/ejJSkpKUZGRs3NzfgaTEtLMzY2Ro21p6eHSqV+9913+FpTB4Xxh5pk\nZmbCZ2/YsGGrV6/Oycnpa93o2rVrCILgcCtXgBD7aGtrA72+Lfzu/QJ9ieGkDlJRUaFpYiCUzMxM\niUQSERGBloSHh3d2dqalpeFr0MPDQygUNjY2wkMqlers7Pz69Wt8rWkV+ILm8/nnzp0LDQ01NzeP\ni4uDn2Sxl1VUVNjZ2Sk4aQ8Vw4YNs7W1raiowBb+zj4+ffoEALCyskJL6uvrnZyc8Ml7/PgxAACb\nEgnmGIJTJBzA2C/UjRuqqjT0lyjQ/fNwtwDrtre3//DDD5GRkfb29hs3boR3BgBQV1encUCbNnF2\ndsbeXqBgH/B2YPc/7+jowL0dOnzQzc3N0RK4WSuPx8PXIMwE0d7ejpaYmJhAnQlHIBDs2LED/gkr\nV67Mzc0dYINwO8GmpqYzZ86EhIR4enru2bOnsbHxD7XbvKmpKfb2AoX4W7hVIra7U9g0VVNh4H89\nLQT+xv04Qk0EAgFawmAw7t271zuLAbGkp6enp6drVEWFSvDPr6qqSkpKQhAkLCxsoPoRB4PBgDaA\n8jv7gJ8buru70XgTOp0ODR8HbDb70aNHbW1taKQMfH/h3nYOaoJNgyESiWBEBb4GtcTjx49PnDjR\n11kSiUShUMRisa+vL4lEotPpg6mbakQiETZdD1CwD9jXdXR0oPbBYDCwz6tGwMi+xsZG1D5gdx0c\nHIyvwd6vv/b2dh8fn+joaHwNagmxWKzUPigUilQq9fHxiY2NjY6OtrOzW7du3cuXLwdfw77o6OjA\nzk6AwvgD3nq4ry6EyWS+e/cOn7C5c+eSSKT79++jJVwul0ql4l6NbWpqgiqhJXw+Hxs99scE9hAs\nFislJYXH4+Xl5W3cuBF2otbW1rhvrzZoamqytrbGlvzOPtzc3AAA2Bmjp6dneXk5PmEODg6JiYmp\nqalwyNPe3p6amvrVV1/hyJQKKS8vp1Kp6FK0TCZ78+YN1PkPCHwPWlhYrFix4smTJ1VVVQkJCQqz\nFTabXV1dPZD5EfjfqFHT7CC9EYlEPB6PzWZjC3/3foEz4MrKSnTFl81mX7lyBbfI5ORkV1fXL7/8\n0snJqbKyMiEhYfny5bhbe/XqFYvFQtPy1dfXd3V14V6e0R729vampqZ///vfY2JiIiIilOYRhHh6\nekokksrKSi8vL3yyuFzut99+CwCoqak5duxYeHg43IIOBxUVFTKZTPF+KiyihYaGYv0b7t69C3Cl\n/dYGAQEBq1atQg9v3boFAPj48eMQqjRApFKphYXFQL45EMiRI0esra0VvqUofp8LCQnhcrnoYVBQ\nEI1Gw5YMFW1tbQUFBdjZIJfL5XA42NW8Px0kEikkJCQ7O3uoFQEAgOzsbOyn2f9HwYigrljv8Kio\nKKwv6lBx9uxZQ0NDrA+cj4/PunXrhlAlQrh48SKVSh3yXvDdu3cUCqX33rSK9iEUCg0NDVNTU9GS\nzMxMKpWKjZIaEsLDw7/44gv0sLGxkUwm68CudXw+39DQ8MyZM0OrxunTp42MjHpHwCv5OBkbGxsU\nFIQeCoVCKyurIfSelcvlBQUFCIJgY+kOHz6sM7texsXFsdnsIYkNgMCQkaVLl/Y+pcQ+4GaD1dXV\naElKSoqpqekQJmmZOXOmt7c3dujk7e29bNmyodKHWEpLS0kkklYdFVSTkZFBJpOVRlcosQ+4T+KG\nDRvQkra2Nmtr67Vr12pRx765d+8eAODatWtoCRwvP378eEj00QYLFixwcXFRseWx9hAIBI6OjosX\nL1Z6VrnzC4xhxLoSpaenk8nkwfdi7+rqYrPZs2bNwhYGBQUpxH7+2WlsbBw2bJj24opVsH37dnNz\n875iqpXbh1AoZDKZ2K1WZTJZZGSku7u7pgmKBsjatWvNzMxqa2vREjjD0mr6gyEhNTWVTCZrlNxn\n4GRlZZFIpN5pw1D6dJ47d+4ciUTCBpg0NjYymczo6OhBG0lBR70ffvgBLRGJRCNGjFDoTnSGOXPm\nDB8+XBtxo0p5+/atra3tvHnzVFzTp31IpdKAgIDg4GCsNWRlZdFotE2bNhGpZh9AWdiYKLlcfvjw\nYYVYXF2itbWVzWZ7eXlBj26t0tLSwuFwOByO6vxVqpxvi4qK6HQ6NnZeLpd///33JBJJ229KLpdr\nYmISExODtc6CggI6nX7gwAGtih5a3r596+jo6Ofnp9XZYnNzs6+vL/QmVH1lP87Z33zzTe+XYkZG\nBpVKXbVqVb/++/i4fPmygYHBggULsO23tbWxWKyIiIghXCcYHKqqqlxdXUeNGoUddRFITU0Nh8Nh\nsVjqdMP92IdMJps9e7aVlRUaEgK5ceOGiYlJYGAgsXlauru7t2zZgiDIli1bsHbQ3d0dERFha2s7\nVJmfBpnGxsaxY8daWloSnkvol19+sbCwGDdunJp3sv/gDoFA4O/v7+LiopA1pbKy0tvb29TU9OjR\no4R0JNnZ2V5eXmZmZgqZC2UyWWxsrKmp6VAlmBgSurq61q5diyBIbGxsQ0PDwBusr6+PiYlBEGT9\n+vXqb6KiVvBPc3PzyJEj3d3dFXqk7u7upKQkAwMDT0/PixcvqpMvUSn5+flRUVEAgJkzZ759+1ZB\nBEx3qXsTWnW4efOmq6srg8FITEzEnTDyw4cPCQkJDAaDxWLdvn1bo7rqBoe9e/fO29ubyWQ+e/ZM\n4VRlZWVsbCyFQnF1dd27d6/6bxyBQJCeng4/2fv6+vbuS1tbW8PCwkxMTP6axgERCoXJycnW1tbG\nxsbLli17+PChmuGuMpksJydn6dKlxsbGTCZz3759OPI+ahA8yOfzIyIi6HS60ox3NTU1CQkJcA9O\nT0/P+Pj4M2fOPHr06P37911dXXK5XCqVtra2FhcXX7p0aceOHePHj6fRaAYGBvPnz79//37vBvPy\n8lxcXGxtbf9Sr5W+6OzsTE1N9fX1BQBYWVnNmjXr66+/vnHjRk1NDZpYhs/n19TUXL9+/euvv545\nc6alpSUAwN/f/+zZs7gzgmoWXCoWi3fu3IkgyNy5c5WuyIrF4jt37uzcuTMgIKCvTTnIZLKHh0d8\nfHxGRobSWZxYLD506BCNRvv8888JefXqEiUlJUePHp0xYwbWT1sBGxubqKioY8eOlZaWDlCcZvu/\nQG7fvr1ixQqhULh//364kZTSy+RyeU1NDY/HEwgE3d3dCIKYmZlZW1uz2WwVQR9Pnz5ds2ZNeXl5\nYmLiV199Bbfm06OUlpaW8vLy9vZ2GINiYmJiamrKZrNhnCIx4DOr7u7u48ePMxgMmLKBkITGV69e\nHT9+PABg0aJFg7bGrEc1A9q/sqamZu3atQYGBvb29lu3bsW3Y1xTU9Px48f9/PwAABEREYP8gUqP\navC8XxRoampKS0vLzMysqKhwdXWdOHHixIkTx44d6+Ligt1ZDEtjYyPcSTkrK6ugoMDExCQ6Onr5\n8uXQSvT8cSDAPlDy8/Nv3brF5XKfPXsmEokoFIqTk5PS/ZE7OzsRBOFwOOHh4REREZMnT9Zoc3k9\ngwaR9oHS09NTWVlZXl5eUVHR3Nzc1tYmFAqpVKq5ubm5uTnMJObp6YlN/aDnj4lW7EOPzqD5hpd6\n/kro7UOPKv4PbRVj/0O42xcAAAAASUVORK5CYII=\n",
      "text/plain": [
       "<IPython.core.display.Image object>"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "G = nx.DiGraph()\n",
    "G.graph['rankdir'] = 'LR' #Graph should be drawn left to right\n",
    "G.add_node(0, shape='doublecircle')\n",
    "G.add_node(1, shape='circle')\n",
    "G.add_edge(1, 1, label = 'True')\n",
    "G.add_edge(0, 1, label = '!p')\n",
    "G.add_edge(0, 0, label = 'p')\n",
    "draw(G)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<div class=\"alert alert-info\">\n",
    "Convert the following LTL operators to Buchi automata.\n",
    "</div>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Ne**X**t - **X**p"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "X = nx.DiGraph()\n",
    "X.graph['rankdir'] = 'LR'\n",
    "#Your code here"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**U**ntil - p**U**q"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "U = nx.DiGraph()\n",
    "U.graph['rankdir'] = 'LR'\n",
    "#Your code here"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**R**elease - p**R**w"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "X = nx.DiGraph()\n",
    "X.graph['rankdir'] = 'LR'\n",
    "#Your code here"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## LTL Formulas to Buchi Automata\n",
    "LTL operators can be combined into formulas to express more complex logical statements. Let's return to the traffic light example from lecture.\n",
    "\n",
    "Example: The at some point the traffic light is going to break at remain red forever.\n",
    "\n",
    "**FG** r"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAK0AAABwCAIAAADjbWflAAAABmJLR0QA/wD/AP+gvaeTAAAa30lE\nQVR4nO2deVgT1/rHzySZJCyJoGxFhLCGTS0oCrIH3MWFSl1ArQqty9W6tCJefRThwVartVWr3ser\nFyxLr7fu61UMXlxAUMGNsFyDC0HKDglknfz+mNv8xmExTIZFzOcv5syZOS8z35xtzvseSK1WAz0f\nPZT+NkDPgECvAz0A6HWgB0WvAz0A6HWgB0WvAz0A6HWgB0WvAz0A6HWgB0WvAz0A6HWgB0WvAz0A\n6HWgB0UrHfD5fAiC2Gz2qFGjxo8fD0EQk8kcP368p6cnk8mEIKi6urq3Df14UKlUOTk569at43A4\nIpEoODjY1ta2oaGhVwulaZOpra0tJCTk4sWLRkZGAAAIgjgcTn5+PgCgvr7e19e3vb29V638qFAq\nlXQ6/ejRo1KpNC0tbdu2bVlZWXQ6vXdLVWvBqVOnLl++rDkEAHC5XM3hvn37nj59qs199GiPs7Mz\nAKC+vr5vioPUWqxDaWtro9PpNNr/Kg8IgrhcrkAgQA+lUimFQul1wX5kuLq6lpaWavN2SEGr/oGh\noaFGBB2BYfju3bu49mzXrl0QBEEQBABoaWnZu3ev5hAAIBaLk5OTly5dOnbs2PDw8CdPnpDyz+gh\nDoE6BLzbLkil0jt37jCZTADArl27rl+/vnz58tbWVgcHB+z9NYcIgixatKikpARNnzhxooWFRXNz\nsy7V2uCDy+USezvEIEEHKB3bM9x/ojnMzc3tKMcLFy4Qsn/QwuFwAAAKhaJviiNt/oBCoQAAhg4d\n+t6cBQUF7u7uODtmzJhBliUfOhKJJCkpqbKyEgCwcePGR48e9UGhWo0byUUsFguFQolEgo5CUVQq\nFZVK7XtjBiBGRkbbtm3btm1bXxba4/pArXUPFu0VSqVS9FAul6OXu7u7t7e3f//995qcz58/P3jw\nYE8t0UMiPa4PJBIJAKDjxJFMJgMAKJVKzcjC3d1dIBAkJSV98cUX165da25uBgBcu3Zt2rRpzs7O\nSUlJVVVVPB6vpKTk/v37//rXv3T9V/ToQo96E1evXv3iiy/QC+Pj4+/cuaNWq8Vi8c6dO9HEtWvX\nPnz4EM0sFApDQ0MNDQ3HjRv36NGjgICAmJiYjIwMqVT66tWrWbNmmZqaWlpaxsXF/fHHHyR0dfTo\ngFbzSHr6EoVCkZmZee7cuUePHjU1NRkbG3M4nMjIyOjoaHNz814qVK+DgUVeXl50dPSrV6+mTJky\nadIkBoPR3t5eUVFx6tQpqVSakpKycuVKzXQcmfR3haTn/zl9+jSdTp8+fbpQKMSdksvlW7dupdFo\nK1asQBCE9KL1Ohgo3L17l06nd/+aT506BcPw1q1bSS+dTB20tbUdOXKEx+NZW1sPHTrUzc1twYIF\naF9ST/dIJBInJ6dp06apVKruc/7yyy9UKvXu3bvkGkBa/+DWrVvR0dHNzc1RUVHoWpXGxsYrV67c\nunVr/vz5hw8fNjExIaWgQUliYuKPP/5YWlpqaWnZfU61Wj116tTa2trCwkIyOwqkqOny5csMBmPW\nrFkikQh36ubNm9bW1p6eno2NjaSUNfhABwW7du3SMv/jx48pFMr58+dJtIEEHQgEAhaLtXTp0q7q\ntFevXtnY2PB4vPdWeh8nBw4cYLFYPfriGhkZyePxSLRBVx0gCBIUFOTt7S2TybrJ9uDBAxqNdvjw\nYR2LG5QEBATExsb26JLz589TKJRXr16RZYOuOjh9+jQEQQUFBe/NuX79elNT09bWVh1LHGTU19dT\nqdSzZ8/26Cq5XD506NC9e/eSZYauOhg7dmxkZKQ2OWtraw0MDA4dOqRjiYOMkydPMplMsVjc0wvn\nz58/efJksszQabzw9OnTkSNH5uTkBAcHa5M/Li7u/v37xcXFhEscfCxevFgkEt24cUObzOfOnRMI\nBK2trVKp9OHDh+Xl5ePHj29ubhaLxVKpdMmSJevWrSNohy4i2rlz54gRI7Sf3srOzgYAVFRU6FLo\nIGPUqFEJCQlaZraxsaFQKAwGg8Fg0Ol0GIbR5T8AAAiCtL9PR3Raj3T79u2QkBDtR7FBQUFDhw69\nePGiLoUOJhAEKS8vR5f0acOyZcuoVKpMJpPJZHK5XKFQIAiCnlKr1bNnzyZsCXEdKJXKO3fuBAYG\nan8JjUYLDAy8c+cO4UIHGW/evGlvb3dxcdEyf2xsrEql6vSUubm5j48PYUuI66CoqEgikQQEBLw3\np1wub/wTT0/P/Pz8RgyEDRgEVFRUAACcnJy0zD9ixIjw8PCOPgQwDM+ePVun6UXCLcqJEycMDQ21\n6Rx0P1e6Zs0awjZ86GRlZVGp1B5dgg7Ucc8QgiAdF3wTrw+qqqpsbGy00aCHh4emO9PxHxg5ciRh\nGz50JBKJoaFhjy6JiIgwMzPDJTIYjLCwMF0sIa4DkUhkbW2tTc4lS5Z0dQqG4Xnz5hG24UOnra2t\npzqg0WixsbEwDGtSqFTqxIkTDQwMdLFEp/pg+PDh2uScM2dOp25xNBpt6tSpbDabsA0fOgTqAwBA\nXFycUqnEpugyUkAhroPa2lotl8uxWKzp06d3lIJKpYqJiSFswCBAJpMxGIyeXmVvbx8SEqJ5nmoy\nvICI6wBBkG6cX3HExMR0HPAYGhp+5G5MhoaGbW1tBC5csWIF+jwhCBozZoyFhYWOlujkz6TWek56\n2rRphoaGqO8DCgzDc+fORb1jP1rYbHZLSwsuUalUvnjxor6+vrGxUSKRwDBsampqamrq4OBgbGyM\n5pk9e7aJiUljYyONRouMjNTdEuI66NFolclkfvbZZ5mZmQqFAk1RKBQLFy4kXPrggMVioR9gBQIB\nn8+/devWkydPKioqNE8Jx4gRI1xdXf39/Xk83qJFiw4ePKhQKEipU/vOv3HhwoVpaWmaw2HDhuk4\n1BkEtLS0qFQqe3v7ly9fDhs2LDQ0NCYmxtHR0cnJydTUlM1moz6fzc3N7e3tL168qKioKCkpycjI\n2LFjBzp5Y2Fh4ebmRoIphGcewsLCVqxYoX1+hUKh8YaGYXjt2rWEix4E8Pn88PBwAICZmdmmTZsK\nCgp6tFjr5cuXhw4dGjJkCADA3t7+yJEjUqlUF3uI6yAmJmbmzJk9umTVqlWage+9e/cIF/1BU1hY\nGBgYCEHQ1KlT+Xy+js4IL168WLdunaGh4fDhw0+cOEH4bsR18O233/r4+PTokpycHFQEw4cP7w1n\njAFOQ0PDl19+SaFQwsLCNF6gpPDHH3+sX7+eRqP5+voSuzPx/oGlpSUaNlEsFt++ffv27dvPnz9/\n9uxZbW2tJg+VSuVwOB4eHqNHjw4JCQkICLC2thaJREuXLu0V56wBTH5+/rx589rb21NTUzudNVGp\nVMXFxTk5OcXFxc+fPxcKhZpvygAAc3NzDw8Pd3f3wMDAgIAAbOgI9Oy+ffuWLFmyYsUKPz+/3bt3\nr127tkfmEV+PlJqaunHjxnHjxl2/fl2pVNrb23t5eXl4eNjY2GjyKBSKsrKyp0+fPnz4sKmpadiw\nYba2to8ePXr8+PFH9Vnh0KFD69evDwwMTE9Pt7Kywp198ODB8ePHs7KyGhoaTExMxowZ4+np6ezs\njJ08fv369bNnz4qKioRCIQzDkyZNWrp0aUREBC5MnUql2rFjR0pKypw5c9LS0nowWUmgDmlqavru\nu+8++eQTGo0WERGRkZFRVVXV/SUqlaqoqGj37t1olCR/f/9z5859DE0DgiAJCQkAgC1btiiVSuwp\nlUp19uzZCRMmAABGjhy5Z8+e4uLi9/YWq6qq0tPTZ8yYQaPRrK2td+/e3XHB+5UrV0xMTCZMmKB9\n+MWe6QBBkNTUVHNzcxaLFR8fX11d3aPLUe7duzdjxgwIgvz9/Z88eULgDh8KCIKsWLGCRqMdO3YM\nd+rx48d+fn4QBEVERBDrMldXV2/atMnY2NjCwuLkyZO4s0+fPrW1tXV3d9cytkQPdFBdXT1x4kQq\nlbp69eq6uroemNwZ+fn5vr6+MAwnJycPVv+WLVu20Gi0c+fOYROVSmViYiIMw35+ftqs9++e2tra\nlStXUqnUKVOmvH37FnuqqqrK0dHRx8dHG18BbXVw8+ZNS0tLNze3R48eEbG3MxAEOXLkiIGBQVhY\nWG1tLVm3HSD88ssvEASdOHECm1hTU4PGiPnb3/5GYrP44MEDV1dXKyurnJwcbHp5ebmFhcXkyZNx\nTVJHtNLBb7/9RqfTFy1aJJFIiBvbBU+ePHF2duZyuZWVlaTfvL8oKCig0+k7duzAJgqFQhcXFy6X\n++zZM9JLbG1tXbhwIYPBOHXqFDY9Ly+PwWDgLOnI+3WQlpZGoVC++eab3uvWvX371svLy8bGZnBI\nobm52dHRcdKkSdj2TigUDh8+fMyYMb0XDApBkPXr11Op1F9//RWbfuDAASqViqsqcLxHBxcuXIBh\nePPmzSSY2S1NTU2jR492cXEZBDGzVq1aZWVlVVNTo0mpqalxdnb28vJqamrq7dI3bdoEw/ClS5ew\niZGRkQ4ODm1tbV1d1Z0OSktLjY2Nly1b1jcDPJFIxOFwQkNDP+hu4927dykUCrZyViqVwcHBjo6O\nuH5cL4EgyOLFi1ksVnl5uSaxrq7OzMysG0eXLnUglUq9vLzGjh3bvSMzuRQWFjIYjKSkpD4rkXR8\nfX3Dw8OxKdu3b2cymST2r9+LVCr19vbGvbuDBw8yGIyuWt4udbB9+3ZjY+O+90H76aefYBj+QDf2\nuHTpEgRBxcXFmpSioiIajXbgwIE+tqS8vNzY2Bj7i1IqlS4uLnFxcZ3m71wHpaWlDAbjhx9+6BUb\nu0WlUvn4+AQGBpLbGCmVSj6f//XXX9vZ2VVVVQUFBY0YMYL03U6CgoKmTJmiOVSpVH5+fr6+vv3S\n0n3//fcGBgbYX/LRo0cZDMabN286Zu5cB/PmzXN3d5fL5b1lY7fk5+dDEISbftGRrjaJILGIx48f\nAwCys7M1Kb///jsEQQ8ePCCxFO2RyWQuLi7R0dGaFKlUamlpmZiY2DFzJzp48uQJBEG4YWgfExkZ\n+emnn5LeP+3VTY82btzo6OiosRlBkFGjRkVFRfVGWVqSmZlJoVCwk/fffvst1kgNnehgzZo1Tk5O\n752B6lXy8vIAAKTH3Ou9TU4QBLGxsdmyZYsmBd1u5P79+71RnJYolUoHB4evv/5ak1JUVAQAyM/P\nx+XEPxSpVDp06FDtY3f1HqNHj+6qU0OY3tMBGtwD2wQsW7bM29u7N8rqEcnJycOGDcMOHBwdHTtO\nL+L9F/h8fmNj40BYSbxgwYIzZ85g12IMZG7cuGFmZubl5YUeqlSqM2fODJDHWF9f/5///EeTEhYW\n1jH8Cl4H2dnZHh4etra2xEpVq9V///vfo6Ki/vrXv8bGxmZkZBC7DwBg2rRpdXV1aD1GFppNIki8\nJ0pubm5QUJBmkdWDBw8aGxunTZtG+IZVVVXHjx///PPP/fz8dDHMwcHBzc0N++KDgoLu37+v2R/l\nf+Dqh3Hjxq1evZpwLZSYmGhnZ9fQ0KBWqxsaGuzs7Pbv30/sViqVyszM7McffyRsDJauNononoyM\njISEBG0WSTg4OCQnJ2sOf/jhBwsLCx37uehevh23ROsp6GI1zWFJSQkAADev9Y4OVCqVgYEB7lOp\n9lRWVtJotJSUFE1KcnKyoaEh4cUK6OorYteSgsZFxM3NLSUlpWMYdJS2tjbcXPLixYunTp2quwGk\n6ODYsWNGRkYaUcrlchiGMzMzsXneaRd6GqYFR3p6ulKpxHqn8Hi8tra2Y8eOEbshl8stLS0ldi25\nlJSUbN++3d7ensvl7tix48WLF9iz6JpSbJij0tJStE86EHBxcZFIJCKRCD2EYdjOzg4NxaLhHR28\nfv0aAGBnZ0esvNu3bwMAsOtUR4wYAQAgHCjP1tYWNWkggPqalZeXp6SkODk5+fn5/fTTTzU1NQAA\nNLoPNjzFmzdvCPexSAd9odgnaWZmhttA/p11662trQAAFotFrDxUcaamppoU1IFJKBQSu+GQIUM6\nuoH2L2q1GhVEQUFBYWHhhg0bgoODx4wZA959bq2trYQfI+mgbk/YJ4n6VWLzvKMD1B8ZtzZee9CI\nFljHBPRvdMc+AhgZGYnF4n70dMDWbTg0bvw5OTl8Ph+8+9xwu1P2L6glYrFYk2JsbIz1PQc4HaAx\nGWQyGYEgHQAAV1fX3NzcpqYmzRJ9tMLUMnxOR9AwEf/4xz+IXa47P//885s3b7o6S6PREASh0+k+\nPj65ubnY58ZgMNAx6kAAtQQbYkAqleK2w3hHB2hVJhaLienA3d0dACASiTQ6QFsKbWLrdUpra+uQ\nIUOioqKIXa47WAdtDVQqFUEQBoMRGRk5f/78SZMm5efnBwcHt7a2ap6bsbEx9vfXv3Rs7ltaWnDB\nO9/pJ6Jxbt6+fUusvLlz51IolJs3b2pS+Hw+DMOEp9Wqq6t1j/RBFhQKhUqlUqnUSZMm/fbbb/X1\n9enp6REREQwGA33E6EalKBYWFoQfI+mg7ofYJ9nc3IwLS/WODpycnGg0mkAgIFaejY1NQkLC0aNH\n0S5JS0vL0aNHt27dio4aCCAQCAbC6AttLj09Pb/77juhUHj58uWoqChsleng4AD+DIqJwuVyCT9G\nDWgTrvvMukAggGHY0dERPUQQ5L///S9qs4Z32gU6nW5vb//s2TPCRSYlJdnb269evdrW1rasrCw+\nPj42Npbw3Z4/fz5//nzCl+uOra0th8NZvHjxggULXF1du8o2ZMgQKyursrIyzUSyq6vr6dOndSma\nz+f/+uuvAIDKysp9+/bxeLxPP/2U2K2ePXvm6OioCWaFzhLhf2C4uafY2Fh/f38dJ7BIAR1tYpd1\nDGSCg4OxX0f//e9/AwBev37djyZp8PX1/eqrrzSHV65cAQDgHIfw35lCQkIKCgpwg8t+gc/nM5lM\nHb+y9BmBgYHo6BFlwoQJdDodm9JfNDU1FRYWhoaGalL4fL67uzsuKCteBxEREVQq9dSpU31hY7dk\nZGRMnTpVxzChfUZoaGhFRcXLly/RQyMjo8mTJ+vyuZUs0K0/sV8+s7OzeTwePl/HamT27Nm4ldd9\nT3V1NY1Gy8rK6l8ztEcikRgYGBw9elSTkp6eDsMw1pulX+DxeJ999pnmUCQSUanU06dP47J1ooML\nFy5AENSX6+07Eh8fb25u3o3/zQAkOjp6woQJmkOJRGJmZoZdqdb3oHt9Yn2b9uzZg1uehNKJDhAE\nGT16NFZEfUxtbS2LxRoIa+N6xMWLFyEIevHihSYlOTmZzWb30rJYbZg5c6a3tzd2GYS3t/eyZcs6\n5ux8sd6ZM2cgCOLz+b1kX/d8+eWXlpaWLS0t/VI6YeRyuY2NDTYeYFNTk7m5+apVq/rFnuvXrwMA\nsPsyoP3W27dvd8zc5aLN6dOne3h46BiVjwB5eXkUCgXnsfuhgPqOYR1FUlNTqVRq369abm9vd3V1\nnTVrFjZxwoQJXfX8utSBUChks9l9vFlKU1OTo6Mj1iXow0IikVhYWGAfGoIgEydOdHZ27uPqbdWq\nVSYmJi9fvtSkoJvl3bhxo9P83S3izszMhCCozzrtKpVqzpw5VlZWfeMX3EscP36cQqFgHQREIpGF\nhUVUVFSfebelp6cDAP75z39qUqRSqZOTE656wPKexfx/+ctfGAzGzZs3SbOxa9asWdNnZfUeKpXK\n19c3ICAA+9Zv3LhBp9PXrVvXBwagZWF9V9Rq9Z49e3C+jjjeowOVSjVv3jw2m919NA0dQRAkPj6e\nSqViJfzhUlRU1NF7Pysri0Kh6LLVpjbw+XwWi7VgwQKsCtFoAt2Pv97v3COTyebPn29gYHDmzBkS\nLO2AXC6Pi4uDYTg9Pb037t8v/Pzzz1QqFTfgOnnyJAzDX331VS85EP/+++9MJnPhwoXY+6NdrrCw\nsO5bJa2cvFQq1dq1ayEI+uabb8j9H4RCoa+vL5vNvnr1Kom37XcQBJkzZ46ZmZlAIMCmX7p0icVi\n+fn5kRsJSiaTbdiwAYKgDRs2YN+3TCYLCwuzsrJ6b6TLHjj7ZWVlDRkyZOTIkaTMK8jl8j179rDZ\nbB8fn0G547NYLB4/fjyHwxGJRNj0srIyb29vNpu9d+9eUn5U2dnZnp6eJiYmOBd1BEGio6PZbLY2\njvc9c/qsrKxEXTtmzZpVWFjYM3v/RKFQpKamOjs7GxgYJCUl9WXcnT6mrq7Ozc3N2dkZJ3SZTJaY\nmMhkMrlcblpamkKhIHb/goKCiIgIAMDMmTNfvXqFKwINo9fVQBEHEeffs2fPoiu1eTxeWlqaWCzW\n8kKhUJiYmGhvbw/DcExMDDaQ02Dl7du33t7eFhYWeXl5uFNlZWXR0dE0Gs3e3n7nzp3atxRisTg1\nNRX9lOzj43P+/HlchoaGhtDQUBaLpaUI1Lrsv5Cdnf3555+je9D7+/tv2rQpMzPz8ePHDQ0NaBPV\n3t5eU1OTm5t7+PDhZcuWoW5S1tbWmzdvHhxxErWkubk5LCyMwWAcPHiw49nKysr4+PhPPvkEAMDl\ncpcvX37kyJHc3Nyampr29na1Wq1SqRoaGoqLizMyMjZt2uTv70+n05lM5rx58zodY9+/f5/D4VhZ\nWfUoDouuwQDq6urS0tLQ14xuJtQRIyMjPz+/hIQENEK/jiV+iCgUis2bN0MQNHfu3E5nyRQKxbVr\n1zZv3uzr69vVYnEqleri4rJ8+fKTJ092+u1KoVDs3r2bTqeHhIS8NwI+DuL7L3REJpOVlJTU1dWh\n0SLRhbwcDofD4Xxsu250ytWrV+Pi4iQSSUpKCroxS6fZ1Gp1ZWWlUCgUi8UymQyCIBMTE3Nzc1dX\n1242/bx3797KlSsFAkFCQsLWrVu7+k12CRF56yGKTCbbv3+/sbExGhGAlAUW58+f9/f3BwAsWrSo\n01ho2qDXQT9QWVm5atUqJpM5fPjwjRs3EttRqbq6ev/+/ePGjQMAhIWF6TiYJ7Nd0NMjqqurjx07\nlp6eXlpaam9vHx4eHh4e7uXlxeFwsDvyYBGJRCUlJXw+/8aNG4WFhSwWKyoqKjY2FlWDLuh10P8U\nFBRcuXKFz+fn5eVJpVIajWZra9vpPp5tbW0QBLm7u/N4vLCwsMmTJ5O1MbJeBwMIuVxeVlYmEAhK\nS0vR7jZuf2c3Nzcul4uNLEAWeh3oAaCj/4KejxO9DvQAAMD/AemlMEfw2QhAAAAAAElFTkSuQmCC\n",
      "text/plain": [
       "<IPython.core.display.Image object>"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FG = nx.DiGraph()\n",
    "FG.graph['rankdir'] = 'LR'\n",
    "FG.add_node(0, shape = 'circle')\n",
    "FG.add_node(1, shape = 'doublecircle')\n",
    "FG.add_edge(0,1, label = 'r')\n",
    "FG.add_edge(0, 0, label = 'True')\n",
    "FG.add_edge(1, 1, label = 'r')\n",
    "draw(FG)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<div class=\"alert alert-info\">\n",
    "Convert the following LTL formulas to Buchi automata.\n",
    "</div>"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In two states from now, the traffic light is going to turn green.\n",
    "\n",
    "**XX** g"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "XX = nx.DiGraph()\n",
    "XX.graph['rankdir'] = 'LR'\n",
    "#Your code here"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The traffic light is always red until it turns green and the light must be green inifinitely often.\n",
    "\n",
    "**G**(r **U** g) $\\wedge$ **GF** g"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "GUGF = nx.DiGraph()\n",
    "GUGF.graph['rankdir'] = 'LR'\n",
    "#Your code here"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "(Optional) Once the light is green, the light cannot become red immediately.\n",
    "\n",
    "**G** (g $\\Rightarrow$ $\\neg$**X** r)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "GX = nx.DiGraph()\n",
    "GX.graph['rankdir'] = 'LR'\n",
    "#Your code here"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "# LTL to PDDL <a id=\"ltl-to-pddl\"/>\n",
    "\n",
    "Generally, PDDL 2.2, which we are going to use, does not support temporal logic modal operators without additional predicates and functions. In this section, we are going to implement additional predicates and functions that allow us to specify LTL goals and constraints in PDDL 2.2.\n",
    "\n",
    "## Elevator Example <a id=\"elevator-example\"/>\n",
    "Recall the elevator problem where there are four elevators, two fast elevators and two slow elevators each with different reachable floors and capacities, delivering passengers in a nine-floor building. To begin, we are going to incorperate some temporal components into the our elevator plan *goals*.\n",
    "\n",
    "\n",
    "Try running the elevator problem in the `example` folder using `planviz` _without_ any goal modification, and observe the sequence of actions in the output plan.<br/>\n",
    "\n",
    "Run the solver on the domain and problem file (`domain-elevators-al.pddl` and `prob-elevators-al.pddl`) using following command\n",
    "\n",
    "<code>optic-clp -N /path_to/domain-elevators-al.pddl /path_to/prob-elevators-al.pddl | planviz.py\n",
    "</code>\n",
    "\n",
    "<br/>\n",
    "<div class=\"alert alert-info\">\n",
    "Copy the generated plan in the 'Activities' box from the bottom of the Plan Visualizer page and assign it into the activities variable in the code box below\n",
    "</div>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 64,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "activities = None # YOUR RESULT HERE\n",
    "solution = [{\"duration\": 1.0, \"time_start\": 0.0, \"id\": 0, \"activity\": \"(board p0 fast0 n2 n0 n1)\"}, {\"duration\": 11.0, \"time_start\": 0.0, \"id\": 1, \"activity\": \"(move-down-fast fast1 n2 n0)\"}, {\"duration\": 12.0, \"time_start\": 0.0, \"id\": 2, \"activity\": \"(move-down-slow slow1-0 n7 n6)\"}, {\"duration\": 12.0, \"time_start\": 0.0, \"id\": 3, \"activity\": \"(move-up-slow slow0-0 n0 n1)\"}, {\"duration\": 15.0, \"time_start\": 1.0, \"id\": 4, \"activity\": \"(move-up-fast fast0 n2 n8)\"}, {\"duration\": 1.0, \"time_start\": 11.0, \"id\": 5, \"activity\": \"(board p6 fast1 n0 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 12.0, \"id\": 6, \"activity\": \"(board p5 slow1-0 n6 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 12.0, \"id\": 7, \"activity\": \"(board p2 slow0-0 n1 n0 n1)\"}, {\"duration\": 15.0, \"time_start\": 12.0, \"id\": 8, \"activity\": \"(move-up-fast fast1 n0 n6)\"}, {\"duration\": 12.0, \"time_start\": 13.0, \"id\": 9, \"activity\": \"(move-down-slow slow1-0 n6 n5)\"}, {\"duration\": 12.0, \"time_start\": 13.0, \"id\": 10, \"activity\": \"(move-down-slow slow0-0 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 16.0, \"id\": 11, \"activity\": \"(leave p0 fast0 n8 n1 n0)\"}, {\"duration\": 11.0, \"time_start\": 17.0, \"id\": 12, \"activity\": \"(move-down-fast fast0 n8 n6)\"}, {\"duration\": 1.0, \"time_start\": 25.0, \"id\": 13, \"activity\": \"(leave p5 slow1-0 n5 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 25.0, \"id\": 14, \"activity\": \"(leave p2 slow0-0 n0 n1 n0)\"}, {\"duration\": 0.001, \"time_start\": 26.0, \"id\": 15, \"activity\": \"(collect-goal-passenger-at p0 n8)\"}, {\"duration\": 12.0, \"time_start\": 26.0, \"id\": 16, \"activity\": \"(move-up-slow slow1-0 n5 n6)\"}, {\"duration\": 12.0, \"time_start\": 26.0, \"id\": 17, \"activity\": \"(move-up-slow slow0-0 n0 n1)\"}, {\"duration\": 0.001, \"time_start\": 26.001, \"id\": 18, \"activity\": \"(collect-goal-passenger-at p5 n5)\"}, {\"duration\": 1.0, \"time_start\": 27.0, \"id\": 19, \"activity\": \"(leave p6 fast1 n6 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 28.0, \"id\": 20, \"activity\": \"(board p1 fast0 n6 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 28.001, \"id\": 21, \"activity\": \"(board p4 fast1 n6 n0 n1)\"}, {\"duration\": 15.0, \"time_start\": 29.0, \"id\": 22, \"activity\": \"(move-down-fast fast0 n6 n0)\"}, {\"duration\": 15.0, \"time_start\": 29.001, \"id\": 23, \"activity\": \"(move-down-fast fast1 n6 n0)\"}, {\"duration\": 1.0, \"time_start\": 38.0, \"id\": 24, \"activity\": \"(board p6 slow1-0 n6 n0 n1)\"}, {\"duration\": 12.0, \"time_start\": 38.001, \"id\": 25, \"activity\": \"(move-down-slow slow0-0 n1 n0)\"}, {\"duration\": 12.0, \"time_start\": 39.0, \"id\": 26, \"activity\": \"(move-down-slow slow1-0 n6 n5)\"}, {\"duration\": 1.0, \"time_start\": 44.0, \"id\": 27, \"activity\": \"(leave p1 fast0 n0 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 44.001, \"id\": 28, \"activity\": \"(leave p4 fast1 n0 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 45.001, \"id\": 29, \"activity\": \"(board p2 fast0 n0 n0 n1)\"}, {\"duration\": 15.0, \"time_start\": 46.001, \"id\": 30, \"activity\": \"(move-up-fast fast0 n0 n6)\"}, {\"duration\": 1.0, \"time_start\": 50.001, \"id\": 31, \"activity\": \"(board p1 slow0-0 n0 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 51.0, \"id\": 32, \"activity\": \"(leave p6 slow1-0 n5 n1 n0)\"}, {\"duration\": 12.0, \"time_start\": 51.001, \"id\": 33, \"activity\": \"(move-up-slow slow0-0 n0 n1)\"}, {\"duration\": 0.001, \"time_start\": 52.0, \"id\": 34, \"activity\": \"(collect-goal-passenger-at p4 n0)\"}, {\"duration\": 12.0, \"time_start\": 52.0, \"id\": 35, \"activity\": \"(move-up-slow slow1-0 n5 n6)\"}, {\"duration\": 0.001, \"time_start\": 52.001, \"id\": 36, \"activity\": \"(collect-goal-passenger-at p6 n5)\"}, {\"duration\": 1.0, \"time_start\": 61.001, \"id\": 37, \"activity\": \"(leave p2 fast0 n6 n1 n0)\"}, {\"duration\": 11.0, \"time_start\": 62.001, \"id\": 38, \"activity\": \"(move-down-fast fast0 n6 n4)\"}, {\"duration\": 1.0, \"time_start\": 63.001, \"id\": 39, \"activity\": \"(leave p1 slow0-0 n1 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 64.0, \"id\": 40, \"activity\": \"(board p2 slow1-0 n6 n0 n1)\"}, {\"duration\": 12.0, \"time_start\": 64.001, \"id\": 41, \"activity\": \"(move-down-slow slow0-0 n1 n0)\"}, {\"duration\": 12.0, \"time_start\": 65.0, \"id\": 42, \"activity\": \"(move-up-slow slow1-0 n6 n7)\"}, {\"duration\": 28.0, \"time_start\": 76.002, \"id\": 43, \"activity\": \"(move-up-slow slow0-0 n0 n3)\"}, {\"duration\": 1.0, \"time_start\": 77.0, \"id\": 44, \"activity\": \"(leave p2 slow1-0 n7 n1 n0)\"}, {\"duration\": 0.001, \"time_start\": 78.001, \"id\": 45, \"activity\": \"(collect-goal-passenger-at p2 n7)\"}, {\"duration\": 0.001, \"time_start\": 78.002, \"id\": 46, \"activity\": \"(collect-goal-passenger-at p1 n1)\"}, {\"duration\": 1.0, \"time_start\": 104.002, \"id\": 47, \"activity\": \"(board p3 slow0-0 n3 n0 n1)\"}, {\"duration\": 12.0, \"time_start\": 105.002, \"id\": 48, \"activity\": \"(move-up-slow slow0-0 n3 n4)\"}, {\"duration\": 1.0, \"time_start\": 117.002, \"id\": 49, \"activity\": \"(leave p3 slow0-0 n4 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 118.003, \"id\": 50, \"activity\": \"(board p3 fast0 n4 n0 n1)\"}, {\"duration\": 13.0, \"time_start\": 119.003, \"id\": 51, \"activity\": \"(move-down-fast fast0 n4 n0)\"}, {\"duration\": 1.0, \"time_start\": 132.003, \"id\": 52, \"activity\": \"(leave p3 fast0 n0 n1 n0)\"}, {\"duration\": 0.001, \"time_start\": 133.004, \"id\": 53, \"activity\": \"(collect-goal-passenger-at p3 n0)\"}]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "You can check whether two activity objects are the same using `check_equal(activities1, activities2)` as following"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 65,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "ename": "AssertionError",
     "evalue": "",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mAssertionError\u001b[0m                            Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-65-d13c2c91e7dd>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mcheck_equal\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mactivities\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0msolution\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m      2\u001b[0m \u001b[0mtest_ok\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32m/home/student/jupyter/psets/MiniProblemSets/TemporalLogic_Release/utils.py\u001b[0m in \u001b[0;36mcheck_equal\u001b[1;34m(activities1, activities2)\u001b[0m\n\u001b[0;32m     16\u001b[0m     \u001b[0mp1\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mPlan\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mactivities1\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     17\u001b[0m     \u001b[0mp2\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mPlan\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mactivities2\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m---> 18\u001b[1;33m     \u001b[1;32massert\u001b[0m \u001b[0mp1\u001b[0m \u001b[1;33m==\u001b[0m \u001b[0mp2\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m     19\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     20\u001b[0m \u001b[0muniversal_goals\u001b[0m \u001b[1;33m=\u001b[0m \u001b[1;33m[\u001b[0m\u001b[1;34m'(collect-goal-passenger-at p5 n5)'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;34m'(collect-goal-passenger-at p1 n1)'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;34m'(collect-goal-passenger-at p3 n0)'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;34m'(collect-goal-passenger-at p2 n7)'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;34m'(collect-goal-passenger-at p6 n5)'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;34m'(collect-goal-passenger-at p4 n0)'\u001b[0m\u001b[1;33m,\u001b[0m \u001b[1;34m'(collect-goal-passenger-at p0 n8)'\u001b[0m\u001b[1;33m]\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mAssertionError\u001b[0m: "
     ]
    }
   ],
   "source": [
    "check_equal(activities, solution)\n",
    "test_ok()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We'll introduce some example predicates augmented to the problem to demonstrate the LTL modeling in PDDL.\n",
    "\n",
    "* `(at-goal-next ?a - passenger ?b - passenger)` - true when passenger `a` gets to his destination _right after_ `b` does\n",
    "* `(at-goal-sometime-before ?a - passenger ?b - passenger)` - true when passenger `a` gets to his goal _sometime before_ `b` does\n",
    "* `(at-goal-sometime-after ?a - passenger ?b - passenger)` - true when passenger `a` gets to his goal _sometime after_ `b` does\n",
    "* `(never-move-fast)` - true when fast elevators are _never_ used (no elevator ever moves fast)\n",
    "* `(never-move-slow)` - true when slow elevators are _never_ used (no elevator ever moves slow)\n",
    "* `(move-fast-until-collected ?a - passenger)` - true when only fast elevators are used _until_ passenger `a` reached his goal, then only slow elevator will be used\n",
    "\n",
    "Now, consider the following scenario:\n",
    "\n",
    "> \"Donald Duck (`p0`) is in our building! Mr.Duck is here for a special comedy show and he needs a quiet time to prepare for his show, which starts right after everyone gets to the target floors. Unfortunately, the fast elevators are being very loud so he requests that everyone **always** uses the _slow_ elevators\"\n",
    "\n",
    "You, as the building elevator moderator, are appointed to find a plan that deliver everyone, including Mr. Duck, to their intended destinations with minimum total-cost while satisfing his request. Each passenger's destination in this scenario is identical to the one in the original problem. \n",
    "\n",
    "<br/>\n",
    "<div class=\"alert alert-warning\">\n",
    "**Important!** In this [Elevator Example](#elevator-example) section, you do *not* need to modify any other part of the problem file but the `:goal` clause\n",
    "</div>\n",
    "\n",
    "<div class=\"alert alert-info\">\n",
    "Modify the **goal description** in the `prob-elevators-al.pddl` file in the example folder. \n",
    "</div>\n",
    "\n",
    "<div class=\"alert alert-info\">\n",
    "Run the solver on the domain file (`domain-elevators-al.pddl`) and your modified `prob-elevators-al.pddl`.<br/>\n",
    "Copy the text from the bottom of the Plan Visualizer page into the code box below\n",
    "</div>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 67,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "activities = None # YOUR RESULT HERE"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "Run `check_elevator_always(activities)` to check your answer"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 68,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "ename": "AssertionError",
     "evalue": "",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mAssertionError\u001b[0m                            Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-68-23e1a24c1916>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mcheck_elevator_always\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mactivities\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m      2\u001b[0m \u001b[0mtest_ok\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32m/home/student/jupyter/psets/MiniProblemSets/TemporalLogic_Release/utils.py\u001b[0m in \u001b[0;36mcheck_elevator_always\u001b[1;34m(activities)\u001b[0m\n\u001b[0;32m     28\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     29\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m---> 30\u001b[1;33m     \u001b[1;32massert\u001b[0m \u001b[0mlen\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mcollected_goal\u001b[0m\u001b[1;33m)\u001b[0m \u001b[1;33m==\u001b[0m \u001b[0mlen\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0muniversal_goals\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m     31\u001b[0m     \u001b[1;32massert\u001b[0m \u001b[0mcompare\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mcollected_goal\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0muniversal_goals\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     32\u001b[0m     \u001b[1;32massert\u001b[0m \u001b[1;32mnot\u001b[0m \u001b[0mmove_up_fast\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mAssertionError\u001b[0m: "
     ]
    }
   ],
   "source": [
    "check_elevator_always(activities)\n",
    "test_ok()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Great job! Mr.Duck is so impressed that he is thinking about coming back play golf in the club inside the building the next day with some new constraints.\n",
    "\n",
    "> \"Mr.Duck (`p0`) realizes that Daisy Duck (`p1`) is in a hurry so, to build a good impression, he requests that he arrives at the golf club (`n8`) **sometime after** Mrs.Duck arrives at her destination. \n",
    "Further, his nephews, Huey(`p3`) and Dewey(`p4`) would also be in the building. Dewey(`p4`) would like to be at his destination **right after** his brother, Huey(`p3`), because he does not like waiting and he does not want his brother to wait for a long time.\"\n",
    "\n",
    "Again, each passenger's destination in this scenario is identical to the one in the original problem and you want to minimize the total-cost while satisfying all the requests.\n",
    "\n",
    "<div class=\"alert alert-info\">\n",
    "Modify the **goal description** in the `prob-elevators-al.pddl` file in the example folder. \n",
    "</div>\n",
    "\n",
    "<div class=\"alert alert-info\">\n",
    "Run the solver on the domain file (`domain-elevators-al.pddl`) and your modified `prob-elevators-al.pddl`.<br/>\n",
    "Copy the text from the bottom of the Plan Visualizer page into the code box below\n",
    "</div>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 69,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "activities = None # YOUR RESULT HERE"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 71,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "ename": "AssertionError",
     "evalue": "",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mAssertionError\u001b[0m                            Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-71-460ff1a32a78>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mcheck_sometime_next\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mactivities\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m      2\u001b[0m \u001b[0mtest_ok\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32m/home/student/jupyter/psets/MiniProblemSets/TemporalLogic_Release/utils.py\u001b[0m in \u001b[0;36mcheck_sometime_next\u001b[1;34m(activities)\u001b[0m\n\u001b[0;32m     37\u001b[0m     \u001b[0mcollected_goal\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mp\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mextract\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m\"collect-goal-passenger-at\"\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     38\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m---> 39\u001b[1;33m     \u001b[1;32massert\u001b[0m \u001b[0mlen\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mcollected_goal\u001b[0m\u001b[1;33m)\u001b[0m \u001b[1;33m==\u001b[0m \u001b[0mlen\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0muniversal_goals\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m     40\u001b[0m     \u001b[1;32massert\u001b[0m \u001b[0mcompare\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mcollected_goal\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0muniversal_goals\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     41\u001b[0m     \u001b[1;31m# Mr.Duck must arrive at the golf club (`n8`) **sometime after** Mrs.Duck arrives at her destination\u001b[0m\u001b[1;33m\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mAssertionError\u001b[0m: "
     ]
    }
   ],
   "source": [
    "check_sometime_next(activities)\n",
    "test_ok()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "## Elevator Problem Revisited <a id=\"elevator-example\"/>\n",
    "\n",
    "In the previous part, the notation of time is _global_. Now, consider a model where each elevator has its own _local_ temporal component represented by `energy-level`. In this section, we are going to implement some functions and predicates in PDDl that allows us to impose some LTL constraints on the `energy-level` of the elevators.\n",
    "\n",
    "Scenario:\n",
    "> Suppose that the elevators can be exhausted after a certain number of _durative actions_ they take. Whenever an elevator performs a durative action (`move-up`,`move-down`, `board`, `leave`, except for `recharge`), its energy decrements by one. Once its energy reaches zero, it has to stop and recharge for one time unit `(= ?duration 1.0)` to fully restore to its full energy level, which is 4.0 for all elevators. However, it can also stop and recharge at anypoint before it is exhausted\"\n",
    "\n",
    "<div class=\"alert alert-info\">\n",
    "Modify the `domain-elevators-recharge.pddl` and `prob-elevators-recharge.pddl` in the `problem` folder to implement the constraint described in the preceding scenario.\n",
    "Submit the modified PDDL file along with this ipython notebook.\n",
    "</div>\n",
    "\n",
    "You are free to come up with your own implementation, but to speed up the proccess, we have provided the following guildlines to walk you through the implementation:\n",
    "* We have added a function `(energy-level ?elevator)` to the domain file. You can use that to keep track of the energy level of each elevator. A given elevator, its energy level is initially at its max energy-level, which is 4.\n",
    "* You need to implement recharge, `:durative-action recharge`. `recharge` checks if the input elevator's energy level is lower than 4.0. It restores the (energy-level ?elevator) back to 4.0 after a duration of 1.0 time unit.\n",
    "* When an elevator is recharging, it will not perform any other durative action until it's done.\n",
    "* Each `:durative-action` requires `energy-level ?elevator` > 0.0\n",
    "* Each `:durative-action` decreases the `energy-level ?elevator` by one\n",
    "\n",
    "<div class=\"alert alert-info\">\n",
    "Submit the modified `domain-elevators-recharge.pddl` and `prob-elevators-recharge.pddl` along with this ipython notebook.\n",
    "</div>\n",
    "</br>\n",
    "You can check your result here."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 73,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "activities = None # YOUR RESULT HERE"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 74,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "ename": "AssertionError",
     "evalue": "",
     "output_type": "error",
     "traceback": [
      "\u001b[1;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[1;31mAssertionError\u001b[0m                            Traceback (most recent call last)",
      "\u001b[1;32m<ipython-input-74-cb13f04b376b>\u001b[0m in \u001b[0;36m<module>\u001b[1;34m()\u001b[0m\n\u001b[1;32m----> 1\u001b[1;33m \u001b[0mcheck_recharge\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mactivities\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m      2\u001b[0m \u001b[0mtest_ok\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;32m/home/student/jupyter/psets/MiniProblemSets/TemporalLogic_Release/utils.py\u001b[0m in \u001b[0;36mcheck_recharge\u001b[1;34m(activities)\u001b[0m\n\u001b[0;32m     50\u001b[0m     \u001b[0mcollected_goal\u001b[0m \u001b[1;33m=\u001b[0m \u001b[0mp\u001b[0m\u001b[1;33m.\u001b[0m\u001b[0mextract\u001b[0m\u001b[1;33m(\u001b[0m\u001b[1;34m\"collect-goal-passenger-at\"\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     51\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n\u001b[1;32m---> 52\u001b[1;33m     \u001b[1;32massert\u001b[0m \u001b[0mlen\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mcollected_goal\u001b[0m\u001b[1;33m)\u001b[0m \u001b[1;33m==\u001b[0m \u001b[0mlen\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0muniversal_goals\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0m\u001b[0;32m     53\u001b[0m     \u001b[1;32massert\u001b[0m \u001b[0mcompare\u001b[0m\u001b[1;33m(\u001b[0m\u001b[0mcollected_goal\u001b[0m\u001b[1;33m,\u001b[0m \u001b[0muniversal_goals\u001b[0m\u001b[1;33m)\u001b[0m\u001b[1;33m\u001b[0m\u001b[0m\n\u001b[0;32m     54\u001b[0m \u001b[1;33m\u001b[0m\u001b[0m\n",
      "\u001b[1;31mAssertionError\u001b[0m: "
     ]
    }
   ],
   "source": [
    "check_recharge(activities)\n",
    "test_ok()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<div class=\"alert alert-warning\">\n",
    "**Congratulations! You are done.**\n",
    "</div>\n",
    "\n",
    "\n",
    "### Constraint Formulation (Optional)\n",
    "\n",
    "\n",
    "Let's reformulate the problem in LTL predicate\n",
    "> Whenever the energy of an elevator is below the full energy level (4.0), it should be recharging within 3.0 time units (since it can take only 3 more actions) and remain recharged there until its energy is fully restored:\n",
    "\n",
    "$r = $ `(recharge ?elevator)` - true when the elevator is being recharged<br/>\n",
    "$f = $ `(full-energy ?elevator)` - true when the elevator has full energy<br/>\n",
    "$l = $ `(energy-level ?elevator < 4.0)` - true when the energy of the elevator is below the full energy level (4.0)\n",
    "\n",
    "$$G(r U f) \\land G((l \\land r)\\lor(l \\land Xr)\\lor(l \\land XXr)\\lor(l \\land XXXr))$$\n",
    "\n",
    "With PDDL 3.0, we can express the constraints as following<br/>\n",
    "`(:constraints \n",
    "  (and \n",
    "    (always-until (recharge ?elevator) (full-energy ?elevator))\n",
    "    (always-within 3.0 (< (energy-level ?elevator) 4.0) (recharge ?elevator))))`\n",
    "\n",
    "\n",
    "### References for Images:\n",
    "\n",
    "\n",
    "References for images: https://www.google.com/search?q=cute+puppies&client=ubuntu&hs=6nW&channel=fs&biw=1182&bih=565&tbm=isch&tbo=u&source=univ&sa=X&ved=0ahUKEwjj1P-P5rHMAhXMeD4KHea6DSoQsAQIGw#channel=fs&tbm=isch&q=dog+running+snow&imgrc=XiA4f8leDEOiQM%3A\n",
    " and https://www.google.com/search?q=cute+puppies&client=ubuntu&hs=6nW&channel=fs&biw=1182&bih=565&tbm=isch&tbo=u&source=univ&sa=X&ved=0ahUKEwjj1P-P5rHMAhXMeD4KHea6DSoQsAQIGw#channel=fs&tbm=isch&q=puppies+cute&imgrc=vcBpl3-Hi9ohCM%3A"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "celltoolbar": "Raw Cell Format",
  "kernelspec": {
   "display_name": "Python 2",
   "language": "python",
   "name": "python2"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 2
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython2",
   "version": "2.7.6"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 0
}
