{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": false,
    "scrolled": true
   },
   "outputs": [],
   "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",
    "import matplotlib.pyplot as plt\n",
    "%matplotlib inline"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# LTL Modeling: Modeling a Dog’s Life <a id=\"ltl-to-pddl\"/>\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.svg\">\n",
    "\n",
    "\n",
    "### Statements to Model about Puppies \n",
    "\n",
    "•\tPuppies are always happy \n",
    "\n",
    "•\tAt any given point, there will come a time when the puppy needs to be fed (Think Always Eventually)\n",
    "\n",
    "•\tAfter a puppy is fed, it must go to the bathroom (Think implies)\n",
    "\n",
    "•\tThe first thing that happens in any dog's life is that it is born (Think how to ensure a state is true in the first state)\n",
    "\n",
    "•\tPuppies are always chewing something or running\n",
    "\n",
    "\n",
    "\n"
   ]
  },
  {
   "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": [
    "### 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",
    "•\tPuppies are always happy \n",
    "\n",
    "This is representative of the Global/Always condition, stating that a puppy is *always* or *globally* happy\n",
    "\n",
    "G(h)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Now it's your turn!\n",
    "\n",
    "•\tAt any given point in time, there will come another time when the dog needs to be fed (Think Always Eventually)\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "•\tAfter a puppy is fed, it must go to the bathroom immediately after it is fed(Think implies)\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",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "•\tPuppies are always chewing something or running\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "It's clear that being a puppy *implies* a lot of things. Combine the above statements into one statement about puppies. Statements about *dogs* in general should not be included in this."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Stage 2: Adult Doggy Life\n",
    "\n",
    "<img src=\"dog.svg\">\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, o = being outside, u = upset owner, s = sleeping dog, k = hunting, w = hiking \n",
    "\n",
    "### Statements to Model about Adult Dogs\n",
    "•\tA dog is a puppy until it is an adult dog, at which point it transitions from being a puppy into a majestic dog\n",
    "\n",
    "•\tNow, the adult dog must be outside to pee\n",
    "\n",
    "•\tNow, if the owner is upset, the adult dog will emphasize with the owner\n",
    "\n",
    "•\tAt any given point, there will come a time in the future when the dog needs to sleep \n",
    "\n",
    "•\tNow, the dog must go hunting or hiking at least once at some point in the future\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 a majestic dog\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "•\tNow, the adult dog must be outside to pee\n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "•\tNow, if the owner is upset, the adult dog will emphasize with the owner\n",
    "\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 needs to sleep \n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "•\tNow, the 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.\n",
    "\n",
    "Hint: You could use implies to indicate the information just about adult dogs or puppies."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Answer: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# LTL to Buchi Automata\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": 2,
   "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": 2,
     "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": 3,
   "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": 3,
     "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": 4,
   "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": 4,
   "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": 4,
   "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": 6,
   "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": 6,
     "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": 4,
   "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": 4,
   "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": 4,
   "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. However, with additional predicates and functions, we can easily model the temporal constraints and goals. \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. In this section, we are going to incorperate some temporal components into the our elevator plan goals.\n",
    "\n",
    "<br/>\n",
    "<div class=\"alert alert-info\">\n",
    "To begin, try running the elevator problem in the example folder using planviz _without_ any goal modification and observe the sequence of the actions in the output plan.\n",
    "</div>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "# Plan with original goal descriptions\n",
    "activities = [{\"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": {},
   "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** of the _original_ problem so that everyone _always_ uses the slow elevators. Copy the generated plan in the 'Activities' box in the bottom of the page and use it to set the `activities` variable below. (This takes up to a minute)\n",
    "</div>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "# YOUR PLAN HERE\n",
    "activities = []\n",
    "solution = [{\"duration\": 12.0, \"time_start\": 0.0, \"id\": 0, \"activity\": \"(move-down-slow slow1-0 n7 n6)\"}, {\"duration\": 12.0, \"time_start\": 0.0, \"id\": 1, \"activity\": \"(move-up-slow slow0-0 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 0.0, \"id\": 2, \"activity\": \"(board p0 fast0 n2 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 1.001, \"id\": 3, \"activity\": \"(leave p0 fast0 n2 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 12.0, \"id\": 4, \"activity\": \"(board p5 slow1-0 n6 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 12.0, \"id\": 5, \"activity\": \"(board p2 slow0-0 n1 n0 n1)\"}, {\"duration\": 12.0, \"time_start\": 13.0, \"id\": 6, \"activity\": \"(move-down-slow slow1-0 n6 n5)\"}, {\"duration\": 12.0, \"time_start\": 13.0, \"id\": 7, \"activity\": \"(move-down-slow slow0-0 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 25.0, \"id\": 8, \"activity\": \"(leave p5 slow1-0 n5 n1 n0)\"}, {\"duration\": 36.0, \"time_start\": 25.001, \"id\": 9, \"activity\": \"(move-up-slow slow0-0 n0 n4)\"}, {\"duration\": 20.0, \"time_start\": 26.0, \"id\": 10, \"activity\": \"(move-up-slow slow1-0 n5 n7)\"}, {\"duration\": 12.0, \"time_start\": 46.001, \"id\": 11, \"activity\": \"(move-down-slow slow1-0 n7 n6)\"}, {\"duration\": 1.0, \"time_start\": 58.001, \"id\": 12, \"activity\": \"(board p1 slow1-0 n6 n0 n1)\"}, {\"duration\": 20.0, \"time_start\": 59.001, \"id\": 13, \"activity\": \"(move-down-slow slow1-0 n6 n4)\"}, {\"duration\": 1.0, \"time_start\": 61.001, \"id\": 14, \"activity\": \"(leave p2 slow0-0 n4 n1 n0)\"}, {\"duration\": 12.0, \"time_start\": 62.001, \"id\": 15, \"activity\": \"(move-down-slow slow0-0 n4 n3)\"}, {\"duration\": 1.0, \"time_start\": 74.001, \"id\": 16, \"activity\": \"(board p3 slow0-0 n3 n0 n1)\"}, {\"duration\": 12.0, \"time_start\": 75.001, \"id\": 17, \"activity\": \"(move-up-slow slow0-0 n3 n4)\"}, {\"duration\": 1.0, \"time_start\": 79.001, \"id\": 18, \"activity\": \"(board p2 slow1-0 n4 n1 n2)\"}, {\"duration\": 1.0, \"time_start\": 80.002, \"id\": 19, \"activity\": \"(leave p1 slow1-0 n4 n2 n1)\"}, {\"duration\": 28.0, \"time_start\": 81.002, \"id\": 20, \"activity\": \"(move-up-slow slow1-0 n4 n7)\"}, {\"duration\": 1.0, \"time_start\": 87.001, \"id\": 21, \"activity\": \"(board p1 slow0-0 n4 n1 n2)\"}, {\"duration\": 28.0, \"time_start\": 88.001, \"id\": 22, \"activity\": \"(move-down-slow slow0-0 n4 n1)\"}, {\"duration\": 1.0, \"time_start\": 109.002, \"id\": 23, \"activity\": \"(leave p2 slow1-0 n7 n1 n0)\"}, {\"duration\": 12.0, \"time_start\": 110.002, \"id\": 24, \"activity\": \"(move-up-slow slow1-0 n7 n8)\"}, {\"duration\": 1.0, \"time_start\": 116.001, \"id\": 25, \"activity\": \"(leave p1 slow0-0 n1 n2 n1)\"}, {\"duration\": 0.001, \"time_start\": 117.001, \"id\": 26, \"activity\": \"(collect-goal-passenger-at p5 n5)\"}, {\"duration\": 12.0, \"time_start\": 117.001, \"id\": 27, \"activity\": \"(move-down-slow slow0-0 n1 n0)\"}, {\"duration\": 0.001, \"time_start\": 117.002, \"id\": 28, \"activity\": \"(collect-goal-passenger-at p1 n1)\"}, {\"duration\": 36.0, \"time_start\": 122.003, \"id\": 29, \"activity\": \"(move-down-slow slow1-0 n8 n4)\"}, {\"duration\": 1.0, \"time_start\": 129.001, \"id\": 30, \"activity\": \"(leave p3 slow0-0 n0 n1 n0)\"}, {\"duration\": 0.001, \"time_start\": 130.002, \"id\": 31, \"activity\": \"(collect-goal-passenger-at p3 n0)\"}, {\"duration\": 1.0, \"time_start\": 130.002, \"id\": 32, \"activity\": \"(board p6 slow0-0 n0 n0 n1)\"}, {\"duration\": 0.001, \"time_start\": 130.003, \"id\": 33, \"activity\": \"(collect-goal-passenger-at p2 n7)\"}, {\"duration\": 36.0, \"time_start\": 131.002, \"id\": 34, \"activity\": \"(move-up-slow slow0-0 n0 n4)\"}, {\"duration\": 1.0, \"time_start\": 167.002, \"id\": 35, \"activity\": \"(leave p6 slow0-0 n4 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 168.003, \"id\": 36, \"activity\": \"(board p6 slow1-0 n4 n0 n1)\"}, {\"duration\": 12.0, \"time_start\": 169.003, \"id\": 37, \"activity\": \"(move-up-slow slow1-0 n4 n5)\"}, {\"duration\": 1.0, \"time_start\": 181.003, \"id\": 38, \"activity\": \"(leave p6 slow1-0 n5 n1 n0)\"}, {\"duration\": 12.0, \"time_start\": 182.003, \"id\": 39, \"activity\": \"(move-up-slow slow1-0 n5 n6)\"}, {\"duration\": 1.0, \"time_start\": 194.003, \"id\": 40, \"activity\": \"(board p4 slow1-0 n6 n0 n1)\"}, {\"duration\": 20.0, \"time_start\": 195.003, \"id\": 41, \"activity\": \"(move-down-slow slow1-0 n6 n4)\"}, {\"duration\": 1.0, \"time_start\": 215.003, \"id\": 42, \"activity\": \"(leave p4 slow1-0 n4 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 216.004, \"id\": 43, \"activity\": \"(board p4 slow0-0 n4 n0 n1)\"}, {\"duration\": 36.0, \"time_start\": 217.004, \"id\": 44, \"activity\": \"(move-down-slow slow0-0 n4 n0)\"}, {\"duration\": 1.0, \"time_start\": 253.004, \"id\": 45, \"activity\": \"(leave p4 slow0-0 n0 n1 n0)\"}, {\"duration\": 0.001, \"time_start\": 254.004, \"id\": 46, \"activity\": \"(collect-goal-passenger-at p6 n5)\"}, {\"duration\": 20.0, \"time_start\": 254.004, \"id\": 47, \"activity\": \"(move-up-slow slow0-0 n0 n2)\"}, {\"duration\": 0.001, \"time_start\": 254.005, \"id\": 48, \"activity\": \"(collect-goal-passenger-at p4 n0)\"}, {\"duration\": 1.0, \"time_start\": 274.004, \"id\": 49, \"activity\": \"(board p0 slow0-0 n2 n0 n1)\"}, {\"duration\": 20.0, \"time_start\": 275.004, \"id\": 50, \"activity\": \"(move-up-slow slow0-0 n2 n4)\"}, {\"duration\": 1.0, \"time_start\": 295.004, \"id\": 51, \"activity\": \"(leave p0 slow0-0 n4 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 296.005, \"id\": 52, \"activity\": \"(board p0 slow1-0 n4 n0 n1)\"}, {\"duration\": 36.0, \"time_start\": 297.005, \"id\": 53, \"activity\": \"(move-up-slow slow1-0 n4 n8)\"}, {\"duration\": 1.0, \"time_start\": 333.005, \"id\": 54, \"activity\": \"(leave p0 slow1-0 n8 n1 n0)\"}, {\"duration\": 0.001, \"time_start\": 334.006, \"id\": 55, \"activity\": \"(collect-goal-passenger-at p0 n8)\"}]"
   ]
  },
  {
   "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 even more 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 would like to be at his destination **right after** his brother, Huey, 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",
    "<br/>\n",
    "<div class=\"alert alert-info\">\n",
    "Modify the **goal description** of the _original_ problem to satisfies all the preceding constraints.\n",
    "</div>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "# YOUR PLAN HERE\n",
    "activities = []\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\": 1.0, \"time_start\": 12.002, \"id\": 8, \"activity\": \"(leave p6 fast1 n0 n1 n0)\"}, {\"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\": 17.0, \"time_start\": 17.0, \"id\": 12, \"activity\": \"(move-down-fast fast0 n8 n0)\"}, {\"duration\": 1.0, \"time_start\": 25.0, \"id\": 13, \"activity\": \"(leave p2 slow0-0 n0 n1 n0)\"}, {\"duration\": 12.0, \"time_start\": 25.001, \"id\": 14, \"activity\": \"(move-up-slow slow1-0 n5 n6)\"}, {\"duration\": 36.0, \"time_start\": 26.0, \"id\": 15, \"activity\": \"(move-up-slow slow0-0 n0 n4)\"}, {\"duration\": 1.0, \"time_start\": 26.001, \"id\": 16, \"activity\": \"(board p2 fast1 n0 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 27.002, \"id\": 17, \"activity\": \"(board p6 fast1 n0 n1 n2)\"}, {\"duration\": 15.0, \"time_start\": 28.002, \"id\": 18, \"activity\": \"(move-up-fast fast1 n0 n6)\"}, {\"duration\": 15.0, \"time_start\": 34.001, \"id\": 19, \"activity\": \"(move-up-fast fast0 n0 n6)\"}, {\"duration\": 12.0, \"time_start\": 37.002, \"id\": 20, \"activity\": \"(move-down-slow slow1-0 n6 n5)\"}, {\"duration\": 1.0, \"time_start\": 43.002, \"id\": 21, \"activity\": \"(leave p6 fast1 n6 n2 n1)\"}, {\"duration\": 1.0, \"time_start\": 44.003, \"id\": 22, \"activity\": \"(leave p2 fast1 n6 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 45.004, \"id\": 23, \"activity\": \"(board p4 fast1 n6 n0 n1)\"}, {\"duration\": 15.0, \"time_start\": 46.004, \"id\": 24, \"activity\": \"(move-down-fast fast1 n6 n0)\"}, {\"duration\": 1.0, \"time_start\": 49.001, \"id\": 25, \"activity\": \"(board p1 fast0 n6 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 49.002, \"id\": 26, \"activity\": \"(leave p5 slow1-0 n5 n1 n0)\"}, {\"duration\": 11.0, \"time_start\": 50.001, \"id\": 27, \"activity\": \"(move-down-fast fast0 n6 n4)\"}, {\"duration\": 12.0, \"time_start\": 50.002, \"id\": 28, \"activity\": \"(move-up-slow slow1-0 n5 n6)\"}, {\"duration\": 1.0, \"time_start\": 61.001, \"id\": 29, \"activity\": \"(leave p1 fast0 n4 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 61.004, \"id\": 30, \"activity\": \"(leave p4 fast1 n0 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 62.002, \"id\": 31, \"activity\": \"(board p6 slow1-0 n6 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 62.002, \"id\": 32, \"activity\": \"(board p1 slow0-0 n4 n0 n1)\"}, {\"duration\": 28.0, \"time_start\": 63.002, \"id\": 33, \"activity\": \"(move-down-slow slow0-0 n4 n1)\"}, {\"duration\": 1.0, \"time_start\": 63.003, \"id\": 34, \"activity\": \"(board p2 slow1-0 n6 n1 n2)\"}, {\"duration\": 12.0, \"time_start\": 64.003, \"id\": 35, \"activity\": \"(move-down-slow slow1-0 n6 n5)\"}, {\"duration\": 1.0, \"time_start\": 76.003, \"id\": 36, \"activity\": \"(leave p6 slow1-0 n5 n2 n1)\"}, {\"duration\": 0.001, \"time_start\": 77.003, \"id\": 37, \"activity\": \"(collect-goal-passenger-at p5 n5)\"}, {\"duration\": 20.0, \"time_start\": 77.003, \"id\": 38, \"activity\": \"(move-up-slow slow1-0 n5 n7)\"}, {\"duration\": 0.001, \"time_start\": 77.004, \"id\": 39, \"activity\": \"(collect-goal-passenger-at p6 n5)\"}, {\"duration\": 20.0, \"time_start\": 91.003, \"id\": 40, \"activity\": \"(move-up-slow slow0-0 n1 n3)\"}, {\"duration\": 1.0, \"time_start\": 97.003, \"id\": 41, \"activity\": \"(leave p2 slow1-0 n7 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 111.003, \"id\": 42, \"activity\": \"(board p3 slow0-0 n3 n1 n2)\"}, {\"duration\": 20.0, \"time_start\": 112.003, \"id\": 43, \"activity\": \"(move-down-slow slow0-0 n3 n1)\"}, {\"duration\": 1.0, \"time_start\": 132.003, \"id\": 44, \"activity\": \"(leave p1 slow0-0 n1 n2 n1)\"}, {\"duration\": 0.001, \"time_start\": 133.003, \"id\": 45, \"activity\": \"(collect-goal-passenger-at p2 n7)\"}, {\"duration\": 12.0, \"time_start\": 133.003, \"id\": 46, \"activity\": \"(move-down-slow slow0-0 n1 n0)\"}, {\"duration\": 0.001, \"time_start\": 133.004, \"id\": 47, \"activity\": \"(collect-goal-passenger-at p1 n1)\"}, {\"duration\": 0.001, \"time_start\": 133.005, \"id\": 48, \"activity\": \"(collect-goal-passenger-at p0 n8)\"}, {\"duration\": 0.001, \"time_start\": 133.006, \"id\": 49, \"activity\": \"(collect-goal-sometime p0 n8 p1 n1)\"}, {\"duration\": 1.0, \"time_start\": 145.003, \"id\": 50, \"activity\": \"(leave p3 slow0-0 n0 n1 n0)\"}, {\"duration\": 0.001, \"time_start\": 146.004, \"id\": 51, \"activity\": \"(collect-goal-passenger-at p3 n0)\"}, {\"duration\": 0.001, \"time_start\": 146.005, \"id\": 52, \"activity\": \"(collect-goal-passenger-at p4 n0)\"}, {\"duration\": 0.001, \"time_start\": 146.006, \"id\": 53, \"activity\": \"(collect-goal-next p4 n0 p3 n0)\"}]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "## Elevator Problem Revisited <a id=\"elevator-example\"/>\n",
    "\n",
    "Now, you are ready to implement another elevator scenario with additional complexity. Please take a look at and try to understand the implementation of the provided elevator example that supports temporal constraints.\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",
    "\n",
    "### Constraint Formulation\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",
    "<br/>\n",
    "<div class=\"alert alert-info\">\n",
    "Modify the domain and problem file of the elevator problem given in the example folder to implement the preceding constraint. Submit the modified PDDL file along with this ipython notebook.\n",
    "(`:goal` clause should contain only `(collected-goal-passenger-at ?a - passenger ?b - count)` clauses)\n",
    "</div>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 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"
   ]
  }
 ],
 "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
}
