{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 4,
   "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",
    "### 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: GF(f -> Nt)"
   ]
  },
  {
   "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: b"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "•\tWhen a dog is a puppy, it is chewing something or running. \n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Answer:  p -> (c or r)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Stage 2: Adult Doggy Life\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: pU(Ga)"
   ]
  },
  {
   "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: GF(f -> (Ft ))"
   ]
  },
  {
   "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: GF(s)"
   ]
  },
  {
   "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: p -> F(k or w) but just F(k or w) is fine if they put that"
   ]
  },
  {
   "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: b ^ GF(s) ^ [ [ p ^ (c or r) ^ F(f -> Nt)^ h ] U G[ a ^ F(f -> Ft)  ] ^ F(k or w) ] - or whatever they have"
   ]
  },
  {
   "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": false
   },
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAALAAAABwCAIAAAAxPW29AAAABmJLR0QA/wD/AP+gvaeTAAAVQ0lE\nQVR4nO2deVQT19vH74QsQFhkVRAJCCECWqSyWbQssrhbXBAtWkGxrYjtsQoqWKt4atWqlGMVWrQF\nFddzrNBz2IkWQVbBhVUwiLIVBIRAEsjy/jGvc0LYkslAYn/z+cu5ucvD43fu3Dtz73MhkUgEcHDe\nQ1C0ATjKBS4InGHggsAZBi4InGHggsAZBi4InGHggsAZBi4InGHggsAZBi4IBcBkMiEI0tLS+uij\nj5ydnSEIUlVVdXZ2njt3rqqqKgRBra2tirKNqKiG/5cZGBhwd3f/+++/qVQqAACCIDMzs6KiIgDA\n27dvXVxcOByOomzDewgFwOFwwsPDYTVIoKent2vXLgUKAsI/bk09AwMDZDKZSPz/7hmCIAaDUVNT\nA19yuVwCgUAmkxViG95DKAB1dXVEDSMhkUgFBQXffvutmZlZS0uLm5ubqanpiRMnIAiCIAgA0Nvb\ne+bMGeQSAMBms48fPx4UFOTg4ODl5fXs2TP0xolwFA0AgMFgIJdcLjc/P19VVRUAcOLEiaysrO3b\nt/f19c2ePVv8/wu5FAqFW7Zsqa6uhtO9vb0NDQ3fvXuH0hg5/hAcbJAQBAydTgcAvH37FklhMBji\ngkAu8/LyRt7nqamp6IzBZxlKCoFAAADo6upOmLOkpMTGxqayshKbdjGpBUeBsNlsFovV398vnigQ\nCNDVhgtCwYiknuXBQ0gulwtfDg4OwsVtbGw4HM7JkyeRnFVVVefPn0dnD/7IUDDwnT3yxQOPxwMA\n8Pl8ZD5iY2NTU1MTHR29bdu2jIyMd+/eAQAyMjKWL19Op9Ojo6Obm5s9PT2rq6uLi4vv3LmD0iB0\nQw8cTEhPT9+2bRv8HxEREZGfny8Sidhs9rFjx+DEPXv2PH78GM7MYrE8PDzU1dWdnJzKy8sXLVoU\nGBiYnJzM5XKbmprWrFmjo6Mzffr0kJCQf//9F7VJ+IspnGHgYwicYeCCwBkGLgicYeCCUF7q6+sj\nIiKcnZ2NjY11dXUZDMbSpUuvXLkyMDAweY3ig0plhMvlHjx48Pz58yYmJmvXroVfbLe1tVVUVGRk\nZOjo6MTGxq5bt25S2sZg8oSDKZ2dnQ4ODtOmTbt06dLQ0JDEr+/evQsJCQEAHDp0aDJaxwWhXAwM\nDNjb25ubmzc0NIyT7bfffoMg6OTJk5gbgAtCudi9e/e0adNevnw5Yc7Tp08TicTCwkJsDcAFoUSU\nlJQQCIQrV65Ik1koFPr6+lpbW/P5fAxtwAeVSoSXlxePx/vnn3+QpVDj09DQwGAwEhMTP//8c6xs\nwAWhLDx9+tTOzi4jI8PHx0f6UoGBgU+ePJFrzdxw8PcQysLly5fnzJnj7e0tU6nQ0NDnz5+XlZVh\nZQYuCKVAKBTeuXPH399fyocFgouLy+zZs69fv46VJbgglIKnT582NzevWbNG1oIQBPn5+aWnp2Nl\nCb5ARim4f/++np7e/PnzZS3IZrMXLFhw9uzZsrKyadOm9fT0AAD09fVpNBo6S3BBKAUVFRWOjo7w\nwlpp+O67786ePSue4uDggPxbT0+vs7MTnSX4I0MpqKurg5fVS8msWbPGGm0QicRPP/0UtSW4IJSC\nuro6eCOGlGzdunWsvV8CgcDf3x+1JbggFE9XV9fbt2+trKykL6Krq7t69WoSiTTyJyKRuHLlStTG\n4IJQPG/evAEAmJqaylRq+/btQ0NDEokqKipeXl4aGhqojcEFoXjgBS/q6uoylfL19Z0xY4ZEokgk\nWr9+vTzG4IJQPPDeGzU1NZlKEQiE4OBgiagBEASheJkxrFp5CuNgArxLB97uLRPbtm0Tf2oQCARX\nV1c9PT15jMEFoXjgHgKFIOh0urOzs4qKCnwJQdCGDRvkNAYXhOKBJ5AjR4jSEBISgnyvFgqFfn5+\nchqDf/5WPPn5+YsWLWpubjY2NhZP7+vre/nyZU9PT3d399DQEJVK1dHR0dPTmz17NvISor+/38DA\ngMPhQBBkb28v/2dP/NW14tHR0QEAdHd36+npFRUV5ebm5ufn19TUwNPRkZDJZEtLy3nz5rm5uXl4\neKxbt+7WrVvyzy9g8B5C8bx582bWrFk+Pj75+fn9/f0MBsPDw8Pa2trS0tLc3FxNTU1bWxsAwOfz\n+/r6uru76+vr6+vry8vLmUxmV1eXkZERHNfyxYsXlpaW8lqD4XI8HFnhcDgXLlyAv0zOmzfv4sWL\nTU1N0hfn8/nFxcUHDhyAx5U+Pj4PHjyQ0yRcEIpBIBAkJCQYGxtTqdS9e/c2NjbKU1t6evqpU6d8\nfX0BAG5ubkgEARTgglAApaWlTk5OJBJp//79nZ2dGNZcUlLi7u6uoqLy9ddfd3d3o6gBgzEEm81+\n+PDhw4cPq6qqKisrOzo6kJ9UVFTMzMxsbW3t7Ozc3d3t7Oyk/+T/n0QkEsXExBw4cMDR0TEuLm7u\n3Lkj88jpT5FIlJSUtH//fk1NzZs3b4qvk5AG9IIYHBxMSUm5fPlyVlYWn883Nze3t7e3tbU1MTFB\n8gwNDdXV1T1//vzx48c9PT16enqbNm0KCgr6+OOP0TX6QdPf3x8YGJiSknL48OHDhw8jL5RgsPVn\nS0vL5s2bHz16FBsb++WXX8pgJYpepaen56effjIyMiISiatWrUpOTm5ubh6/iEAgqKioOHXqFHxP\nuLq63rt3TygUomj9A6Wzs9PZ2VlXVzcrK0vip0ny59DQUHh4OADg8OHD0tspmyCEQmFiYqKBgYGm\npmZERERra6tMxWEePXq0cuVKCIJcXV2fPXuGooYPjvb2dmtraxqNVlVVJZ4+Bf6Mj48nEom7du2S\nsjYZBNHa2urt7a2iohIaGir/UKioqMjFxYVEIh0/flwgEMhZmzLT29u7YMECOp3e0tIinj5l/rx7\n9y6RSJSyn5BWELm5udOnT7e2ti4vL5fZ2DEQCoVxcXFqampLlizp6OjAqlqlYmhoyMvLa8aMGRK7\nuafYn7///jsEQfHx8RNWIpUgbt68SSaTt2zZ0t/fj9LYsXn27BmdTmcwGHLOxZWTqKgoVVXV0tJS\n8USF+DMyMpJCoUz4imJiQSQlJREIhH379k3eGLCtrc3e3t7ExOQ/pons7GwCgSBxXyrKn3w+39PT\nk06n9/b2jlN2AkGkpqaSSKQDBw5gY+nY9PT02NnZWVlZyRN0U6no7+83MzPz9/cXT1SsP1tbWw0M\nDPbs2TNOwfEEUVtbq6GhERwcPDXzw5aWFjMzMw8Pj//GGHPfvn0GBgbi5xsogz+Tk5MJBMI4YUbG\nFASXy7W3t3dwcODxeBhbOjalpaUUCiU6OnrKWpwk6uvryWRyXFwckqIk/hQKhe7u7osXLx6ryJiC\nOHLkiIaGRn19PcY2TsQvv/xCIpGeP38+xe1iS1BQkK2trXhPoDz+LC8vhyAoIyNj1PyjC6K2tpZC\nofz888+TYuO4CAQCR0fHxYsXY9uvCoXCgoKCvXv30mi0V69eLV++XFtb29HRUf7vxSNpamoik8kJ\nCQlIirL508vLy8PDY9T8owti48aNNjY2g4ODk2LjRBQVFUEQdO/ePQzr5PP5qamp8ELWffv2PXjw\n4Nq1axoaGkQiETmtCiu+//57IyMj8UeDsvkzMzMTAFBZWTky8yiCePbsGQRBt2/fnkQbJ2Lt2rXz\n58/HfPAF759E/qvOnTsH3q9TxQqBQECj0cLDw5EUJfSnUCi0sLCIiIgYmXMUQYSFhVlaWmIb20xW\nCgsLAQDw+REYInGOWUNDAwDAxcUFwyby8/MBAOLvH5XTn5GRkTQabeQtJykILperq6t74sSJSbdx\nIuzs7LC9d0UjBAHvkPH29sawiaioKAsLC+RSaf0Jr88eOXiXXF7BZDK7u7s3b94swxf0yWHTpk13\n794VCoWT18Tbt28BAG5ubhjWmZ2d7eXlhVwqrT/t7e319fWzs7MlskkKIicnx9bWVtadyAgikejS\npUsbNmyIjIzcsWNHcnIyunoAAMuXL+/s7KyoqEBdw1ggJ9ZlZ2fPmTNn7969WNU8MDBQVlYmrjA5\n/QkAaG5uvnz5sr+//8KFC+WxTcKf8OfyUc78lOgxnJycQkNDUfdLR48epdFoXV1dIpGoq6uLRqPF\nxMSgq0ogEOjr6587dw61MSOBHxlxcXEdHR0dHR0nTpzo6emZsBQcbzw5OXnCb1GlpaUAgNraWiRF\nTn/CdHV1gdEOe5WJkf48duwYnU6XyAYkyqipqf3xxx/ommxsbCQSiT/++COScvz4cXV1ddQf+318\nfIKCgtCVHRWJMYSUlJSUwDePqqrqpk2bUlNTx5pAXr16lUQiISHs5fSnOPILQjTCnzdv3lRRUeFy\nueJ5hj0y3rx5w+FwZAplIs61a9f4fP6SJUuQFE9Pz4GBgYSEBHQVMhiM2tpadGUnAy6Xe+fOndWr\nV2tqam7YsCE1NVViQ2Z9fb2ZmRmyz05Of2KOhD+trKwEAkFjY6N4nmGCeP36NQAAdUS7hw8fAgDE\nF4XOmjULAPDkyRN0FZqamsImYUVfXx94fwQqOuC7n8fjpaSkrF69Wl9ff+vWrdnZ2fBN3N3dbWBg\ngGSW05+YI+FPfX19AAD8PEIYJgjYX5qamujaa2lpAe93KsLAR1ezWCx0FWpra/f29qIrKwGbzQ4P\nD4ct3LlzZ0FBgZwVwqrq7e29ffu2t7f3zJkzv/nmm4aGBvFwPnL6E3Mk/AkbBhuJMGyzL3zKLJVK\nRdeelpYWeH8iMQz8b9R3JJVKZbPZskb7nZDExMTExESsaoOjO7S2tsbGxgIAnJyckJ/k9CfmUKlU\n8SPCYcPYbLZ4nmGCoFAoAAAejydrvCOYOXPm5OXl9fT0ILGPuru7AQASu9ylh8fjUSiUP//8E11x\nrGhoaDh48OA4GSgUCo/Hs7KyolKp8MZcJB3I4U/Mgf2JXI4aqGSYIOA+hM1mo/sDbGxsAAAtLS2I\nIOAuetGiRShqAwD09fVpa2vLHxVFTkpLS0cVBDyhsLCwCAkJCQgIoNFoYWFh4gMmOf2JOX19fXAv\njlyC9/06wrAxBDwgamtrQ9fe+vXrCQRCbm4uksJkMkkkEur3dK2trYaGhujKTh5wnC8TE5NDhw49\nf/4cPkwRHjlqaWmJP6Tl9CfmSPgTDow9niAsLS2JRGJNTQ269kxMTA4ePBgfHw87pbe3Nz4+Pioq\nCp5roKCmpkamgL+TColEgiBIQ0MjICAgLS2NxWL98MMPtra24nlmz54NL4GBL+X0JwL84Jf/Lb6E\nP+vr6yEIMjc3F88z7JFBJpPNzc0rKytRNxkdHW1ubh4aGmpqalpXVxcREbFjxw7UtVVVVQUEBKAu\njhUGBgZaWloeHh6BgYErVqwYJ34gg8Ho7+9vaWmZOXMmwMKfAAAmk3n16lUAQGNj49mzZz09PVEE\nzYeR8GddXZ2RkZHkJEjiZdaOHTtcXV3lfCOGCfBkNScnR9GGyEB7ezsAIDMzE0lRZn8GBwd7enpK\nZJP8uOXu7l5SUiIxN1UITCZTVVVVzi86U4yhoSGDwWAymUiKMvuTyWQuXrxYIpukIFatWqWionL7\n9u1JN3AikpOTly1bJmt8V4Xj6ekpPqxWWn+yWCwWi+Xh4SGZb2Tf8tlnn3l5eU1u/zURra2tRCLx\nxo0bijUDBbdu3SISie3t7UiKcvrz119/pVKpHA5HIucogkhNTYUgCMNNqCiIiIgwMDAYGBhQoA3o\n4HA406ZNO3v2LJKinP50cnLaunXryJyjCEIoFNrZ2a1bt24SDRyXjo4OTU1NZVh2ho4vvvjC0dER\nuVRCf7548QKCoLS0tJGZR18ccPfuXQiCmEzmJJk4Pjt37pw+ffr4e1KVmQcPHgAA8vLykBRl8+eu\nXbtMTU2RdRvijLlaZMWKFba2thKrJ6aAwsJCAoFw9erVKW4XW9zd3SVmdMrjz8bGRhKJJL7NUJwx\nBcFisbS0tMLCwrC3cWx6enosLCyWLl06lY1OBmlpaQAA8W1hyuPPr776ysjIaORwEma89WTXr1+H\nIGjKhvoCgcDPz2/GjBltbW1T0+KksnLlSondWsrgz0ePHhEIhCtXroxVaoIFhrt376ZQKLm5uZiZ\nOTZhYWFT1tYUAO/nlFgkrFh/8vn8hQsXLlq0aJwtcRMIQiAQbNy4UUtL6/79+5hZOgKhUBgREaGi\nogJHdf/PEB0draqqWlFRgaQo1p9HjhxRVVUdP/LfxEuQeTxeQECAmpra3bt35bV0NAYHB0NCQkgk\n0rVr1yajfgXC5/Pd3d2trKzER/iK8mdWVhaBQLhw4cL4xaVaky4QCPbs2QNB0L59+7DdwsxisVxc\nXLS0tNLT0zGsVnlobm42NDT09fUV99vU+7OqqkpXV3fDhg0T1iDDJoUbN25oa2vPmzcPk/n04ODg\n6dOntbS0HB0dpz6MxlRSXFysoaERGBgo8eSeMn82NzfTaLRPPvlEmqB3su1aaWxshE+NXbNmjUSo\nPekZGhpKTEyk0+lqamrR0dFTGWJHUWRmZpLJ5MDAQIk/dgr8WVdXZ2lpaWtrKx7tahzQxLr+66+/\nFixYAADw9PRMSkpis9lSFmSxWEePHjU3NyeRSIGBgS9evEDR+gdKZmamhoaGl5fXyFMLJs+fBQUF\nBgYGDg4O0sf2Q39eRk5Ojr+/P4VCoVAorq6u4eHh169ff/r0aVdXFxz2jMPhtLe35+XlXbx4MTg4\nGN7AZGxsfODAgf9YPEopKS4uNjQ0tLCwKCsrG/krtv4UCoUxMTFkMtnHx6evr096I+U9QKWzszMp\nKQm2TyLePwKVSl24cOHBgwfhwP9ytvhB8/r168WLF1MolDNnzozqCkz82dLS4ufnRyAQoqKiZHU4\nloew8Xi86urqzs5OeEs1hULR1NQ0MzMzMzPDfLPNhwufzz927NjJkydtbW3j4uLEN/ZIgMKfAoEg\nLi4uMjJSW1s7ISHB29tbZvvQ6BxHbl6/fr1lyxYAgKura0pKivwV9vf3x8TEmJqaampqxsTEoJ7N\n4oJQJNnZ2fAiNmdn59jYWPF1VtJTVla2d+9eY2NjNTW13bt3v3r1Sh6T8HM7FU9hYWFCQsKdO3fY\nbLajoyMcRNLa2trIyGjU/ENDQywWq7y8PDs7Ozs7u7Gxcc6cOYGBgdu3b0f2zKEGF4SywOVy09LS\ncnJymExmVVUVAIBKpY56kGtTUxOfz4eXUHt4eCxbtkzWk9bGAReEMtLd3V1TU1NdXT3q2d8MBsPa\n2ppOp8ObCrEFFwTOMP6nT9HEGQkuCJxh/B/mJiZ2VodrswAAAABJRU5ErkJggg==\n",
      "text/plain": [
       "<IPython.core.display.Image object>"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "X = nx.DiGraph()\n",
    "X.graph['rankdir'] = 'LR'\n",
    "X.add_node(0, shape='circle')\n",
    "X.add_node(1, shape='doublecircle')\n",
    "X.add_edge(0,1, label='p')\n",
    "X.add_edge(1,1, label='True')\n",
    "draw(X)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**U**ntil - p**U**q"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAALAAAABwCAIAAAAxPW29AAAABmJLR0QA/wD/AP+gvaeTAAAYOUlE\nQVR4nO2de1xTR/bA5+YdAuElIEghyCMIWErLQwtWgoDrKlJFUVrUgmUfirarKILQ1sdnXa2tLLZU\nt9hdWaS1th+34mfxgaSuIqBRrCggjQ2iAlZeJYEkJLn5/TG/5hNueCQ3NxBpvn9xh5k5h8O5c2fu\nnXMGUavVwIKFXyFNtgIWzAuLQ1gYhsUhLAzD4hAWhmFxCAvDsDiEhWFYHMLCMCwOYWEYFoewMAyL\nQ0wCfD4fQRA2m/3iiy9GREQgCMJgMCIiIoKCghgMBoIgHR0dk6UbZbIE/5YZHByMjo4+e/Ysi8UC\nACAIwuFw6urqAADd3d1z5syRSqWTpZtlhJgEpFLp9u3boTdgcHR03LBhwyQ6BGL5uDXxDA4O0mg0\nCuX/h2cEQbhcbnNzM7yUyWQkEolGo02KbpYRYhKwsrLSeIMuVCr12rVr7777LofDaW9vnz9/voeH\nx759+xAEQRAEANDf3//RRx9pLgEAEolk7969aWlpoaGhsbGxDQ0N+JVTW5hsAABcLldzKZPJqqur\nGQwGAGDfvn0XL15cv369WCyeOXOm9v9Lc4mi6Jo1a5qammB5XFycs7PzL7/8glMZI/4QC8SAcQiI\nr68vAKC7u1tTwuVytR1Cc3nlyhXd+7y8vByfMpZVhplCIpEAAA4ODuPWvHHjRkBAwL1794iRS0gv\nAAC1Wl1TU7N161YOh9PW1rZ48WI7O7vw8PD//e9/RImwMCISiUQkEg0MDGgXqlQqfL0R5hAoinZ3\ndxcVFT18+PDw4cPZ2dlFRUVNTU0LFizQzJ8t6KLWe5UHp5AymQxeDg0NweYBAQFSqXT//v2amo2N\njZ988gl+hQgEPvnkcjm8PHToEAAgIyODWClTCbFYDADw8PDAlHM4HACAQqHQlCxfvhwAkJub29LS\ncvjwYfg0qaioGBwchGZPT08vLS3duXNnXFycuUwqMROfBw8eAADmzJlDrJQpw7lz59566y14Z2Zn\nZ1dXV6vVaolEsnv3bli4efPmW7duwcoikYjH41lZWYWHh9fX10dFRaWmppaVlclksra2tsTERHt7\nexcXl4yMjJ9//hm3SgS/mPL3979//76mT5lMxmQy4+LiLly4QKAUC6bDtC+muru7AQDz5883qRQL\nBGISh9BMcSsrK/39/bds2WIKKRZMgUkcori4uKurq6urq6Ojo7a2lslkmkKKBVNg2jmEBWMQCoWf\nf/75999//+jRI5lM5uTk5OXl9eabbyYlJVlZWZlIqMUhzBGZTJaTk/PJJ5+4u7svX74cvtju7Oy8\nffv2+fPn7e3tCwsLk5KSTCLbyIUTBjc3N6D1HsICDrq6ukJDQ+3s7I4dO6b9HgLyyy+/ZGRkAABy\nc3NNIZ0whxCLxdu2bYNOtm7dOriktmAog4ODISEhXl5eDx48GKPaP/7xDwRB9u/fT7gCRI4QPT09\nBw4ciIyMdHNzs7e353K5ixcvPnXqlGXA0J/MzEw7O7uffvpp3JoffvghhUKpra0lVgHC5hDHjx//\ny1/+QqPRVqxY8eKLL6Io2tnZefXqVT6fHxQUdPLkSX9/f0IETWEEAkFERMTx48dTU1PHraxWqxct\nWtTW1tbQ0EAmkwlTghC3ys/PRxAkPz9/YGAA86umpqbQ0FBra+vr168TImsKs2DBgqioKBRF9awv\nFArJZHJpaSmBOhDgEEVFRSQS6d///vdoFeRy+ZIlS1xcXFpbW40XN1X54YcfAADnz583qNWbb74Z\nFBREoBrGOkRzczOTydy1a9fY1QYGBkJCQhYuXGikuCnMO++84+/vr//wALl27Rp81hClhrEOkZCQ\nEBISors60qWuro5EIp06dcpIiVMSlUo1Y8aM9957z9CGKIrOnDlz69atRGlilEPU19cjCHL27Fk9\n66ekpLz88svGSJyq1NfXAwBu3ryJo+3WrVsDAwOJ0sQoh8jMzPT399e/fm1tLQDgypUrxgidkhw6\ndMjR0VGlUhnaUCwWl5WVIQgiEAiEQqFAIBAIBMbM1fA7BIqizs7Of/3rXw1qFRQUtHnzZtxCpyrr\n1q373e9+p3/9sT8gOzo64tYE/9fOu3fv/vzzz7///e8NarV06dLy8nLcQqcqLS0tcLOZnrzwwgua\nKB0MFArltddew60Jfoeorq62tbUNCgoyqFV8fLxIJGptbcUtd0rS0tIC90Xqydq1a0eL/VKpVMnJ\nybg1we8Qly9fjoqKMvQdWVhYGJlMFggEuOVOPXp6erq7u/38/PRv4uDgsHTpUiqVqvsrCoWyZMkS\n3MrgD9QRCARr167Vp2ZzczPcfg2xsbEpLCzU+IS1tfW7775rbW2NW5PnncePHwMAPDw8DGq1fv36\nb7/9FlNIJpNjY2ONMia+qQeKogwGo6SkRJ/KcIctmUymUqlUKpVCodB/BY57d+7cwafG1KCmpgYA\n0NbWZlArlUo1ffp0zH+TRCIdO3bMGGVwPjJ6enpkMhnc/TAuMTEx9vb2KpVKoVAoFAqlUin/FZVK\nFRAQMHv2bHxqTA1g7I2hGw1JJFJ6ejomawCCIImJicYog9Mh2tvbAQB6OgSZTE5KShox4QGZTE5P\nT8enw5QBpgeB4d4G8dZbbykUCs0liUSKjIx0dHQ0RhmcDtHZ2QkA0B2yRiM5ORmGnmFQq9X6fOqd\n2sARAodD+Pr6RkREaOb1CIKsXLnSSGVwOgT879LpdD3r83g8Ozs7TCGFQomNjXVxccGnw5QBTqS0\n73X9gWGS8GcURZctW2asMviaQa9EUVRfMRTK8uXLS0tLtccJFEU1gWy/ZWCUZm9vL2YaIRaLf/rp\np76+vt7eXoVCwWKx7O3tHR0dZ86cqXkJsWrVqszMTKlUiiBISEjIjBkzjFQGp0PA7AUGxZwnJyd/\n8cUX2iVWVlavv/46PgWmEvb29gCA3t5eR0fHurq6qqqq6urq5uZmuBzVhUaj+fj4zJ49e/78+Twe\nLykp6euvv1ar1StWrDBemQkaIQAAMTExbDa7v78fXtJotJSUFBwPzqkHm80GAGzZsqW6unpgYIDL\n5fJ4vISEBB8fHy8vLyaTaWtrCwBQKpVisbi3t1coFAqFwvr6+ry8vJ6eHldXVzjuGj+BAADve4jL\nly8DADo7Ow1qlZaWpv1yzfLZUyqVFhUVeXp6AgBmz5792WefGfQ2QqlUXr9+fceOHfD+jI+Pv3z5\nspEq4XSIlpYWAIAmUl1P/vvf/2q8wcPDw9DdQVMJlUpVXFzs5ubGYrG2bNli5ObCc+fOHThwYOHC\nhQCA+fPnG/p/0QanQwwODgIAzpw5Y1CroaEhGxsbAACVSv3ggw/wiZ4CCASC8PBwKpW6bdu2rq4u\nAnu+ceNGdHQ0mUz+85//3Nvbi6MHnHMIJpPp6OgIZz0SieTq1atXr15tbGy8d+/es2fPNNXIZDKH\nwwkMDAwODo6Ojg4ODk5MTCwrK1MqlW+88QY+0c81arW6oKBgx44dYWFht27dGvFbsUH2hLN7DaGh\noVVVVSUlJdu2bTt//vzJkydDQ0MN0hB/XEZwcLCPj49UKr148aJSqfTy8goJCQkMDHR3d9fUUSgU\nLS0td+/evXXrVl9fn6Oj46uvvlpeXj537ly4O/Q3xcDAQGpq6pkzZ/Lz8/Pz8zEfioeGhs6cOfPF\nF18YZM+UlJS0tLSXX34ZI6u9vf2NN96oqakpLCz84x//aICWOEaVvr6+v/3tb3Z2dmQyOSEhoays\n7MmTJ2M3UalUt2/fPnDgQGBgIADA19f3u++++03NIbq6uiIiIhwcHC5evIj5FbSnq6srhUIx1J5w\njImMjNS1p0Kh2L59OwAgPz9ffz0NcwgURY8fP+7k5GRjY5Odnd3R0WFQc0hVVdWSJUsQBImMjGxo\naMDRw3PH06dPZ82a5enp2djYqF1OiD1ramrGsOfRo0cpFMqGDRv07M0Ah+jo6IiLiyOTyRs3bjR+\nKlRXVzdnzhwqlbp3714cm0ufI/r7+1955RVfX9/29nbt8gmz5+nTpykUip7jhL4OUVVV5eLiMmvW\nrPr6eoOVHQUURY8cOcJkMhcsWPDs2TOiujUrFApFbGzs9OnTMdHcE2zPzz//HEGQo0ePjtuJXg5x\n8uRJGo22Zs0a3dBN42loaPD19eVyuVMy0C8vL4/BYGAiqybFnjt37qTT6eO+ohjfIUpKSkgkUlZW\nlunmgJ2dnSEhIe7u7lPMJyorK0kkEua+nCx7KpXKmJgYX1/f/v7+MdqO4xDl5eVUKnXHjh3EaDo6\nfX19wcHBfn5+xiTdNCsGBgY4HE5ycrJ24eTas6Ojw8nJaey4mLEc4v79+9bW1unp6ROzPmxvb+dw\nODweb2rMMbOyspycnLTPNzAHe5aVlZFIpDHSjIzqEDKZLCQkJDQ0dCLzvwgEAjqdvmfPngmTaCKE\nQiGNRjty5IimxEzsiaJodHT0vHnzRmsyqkO8//771tbWQqGQYB3H4+9//zuVSr179+4EyyWWtLS0\nwMBA7ZHAfOwJQ7RHS0QxskPcv3+fTqcfPHjQJDqOiUqlCgsLmzdvninGVblcvmvXroyMjJycnIyM\njH379hkUrKwnbW1tNBqtuLhYU2Ju9oyNjeXxeCPWH9khVq1aFRAQMDQ0ZBIdx6Ourg5BkO+++47Y\nbpVK5WuvvbZq1Sr4TJVIJDCghVgparX6vffec3V11X40mJs9YaTMvXv3dCuPYI6GhgYEQSY3s8fy\n5ctfeuklYgeJTz/9FABw+/ZtTQmMniNQhFqtVqlUnp6e27dv15SYoT1RFPX29s7OztatOYI5Nm3a\n5OPjo1QqTavjmMBMEsQmu0xISICfHDUlmNM9CKG6uhoAoP3+0TztuXPnTk9PT91bDmsOmUzm4OCw\nb98+k+s4HsHBwcQexQO/EWungDSFQ+Tl5Xl7e2suzdaeN2/eBADoTt6xcRl8Pr+3t9ccdq+kpKSc\nPn3aoH28YwMfEGfPntWUaM6vIpDKysrY2FjNpdnaMyQkZNq0aZWVldh6GAfJysoyJs0diqLFxcUr\nVqzIzc1dv379iRMncHd1584dgDft0ojALTlsNvvEiRP19fWHDx+Gp28T1b9arR4YGKBSqWVlZZoS\nI+2pVqsfP3587NixlStXGnlSla49ExMTk5KSMNWw5ggPD9+4cSNuqbt27fL09Ozp6VGr1T09PZ6e\nngUFBfi6UqlU06ZNO3ToEG5ldPn2228DAwNtbW3j4+N/+OEHPR8ZMN94WVnZuN+iYI4DeB4AxEh7\nQnp6esBIh70ahK49d+/e7evri6kGMG2YTOY///lPfCJbW1spFIp21qm9e/daWVnh/tgfHx+flpaG\nr60+6OkQN27cgKMpg8FISUkpLy8fbQFZWlpKpVI1SRqNtKc2xjuEWseeJ0+eJJPJMplMu86wOcTj\nx4+lUqlBqUy0OXHihFKpXLBggaYkJiZmcHCwuLgYX4dcLvf+/fv42poCmUz2zTffLF261MbGZuXK\nleXl5ZiATKFQyOFwNHF2RtqTcDD29PPzU6lUmPROwxzi0aNHAAAYN4KDq1evAgC0N4W+8MILAACY\ntBcHHh4eUCUTASeVBkXZwrtfLpefOXNm6dKl06ZNW7t2bWVlJbyJe3t7nZycNJWNtCfhYOw5bdo0\nAAB8HmkY5hDwUFEYOoEDmDQCRipCYBirSCTC16Gtra0m9I9YmpqasrKyHj58CADIzc2VSCSG9gCj\n5/r7+0+dOhUXFzdjxox33nnnwYMH2ul8jLQn4WDsCRWDSmoYFpcBz4+Gc28cwBhF7XR58OcRM0Po\nA4vFkkgko+XfI4qDBw8ePHgQd3M4zHR0dBQWFgIAwsPDNb8y0p6Ew2KxtI8Ih4phboZhDgHzPcjl\ncnxnfPn7+1+5cqWvr0+TSKS3txfonWhGF7lcTqfT//Wvf+FrThQPHjzIyckZowKdTpfL5X5+fiwW\nCwbmasqBEfYkHGhPzeWIiUqGOQQcQyQSCb4/ICAgAADQ3t6ucQj4EImKisLRGwBALBbb2toSE9Rs\nBAKBYESHgAsKb2/vjIyM1atXe3p6btq0SXvCZKQ9CUcsFsNRXHMJfh3XNQybQ8AJEUwXhIMVK1aQ\nSKSqqipNCZ/Pp1KpuN/TdXR0ODs742trOmCyLHd399zc3Lt37wqFwuzsbDhz1M53AIy2J+Fg7NnX\n1wfGdggfHx8KhdLc3IxPnru7e05OztGjR6FR+vv7jx49mpeXB9caOGhubjYo4a9JoVKpCIJYW1uv\nXr26oqJCJBJ98MEHMBBNw8yZM+EWGHhppD01wAe/8W/xMfYUCoUIgnh5eWnXGfbIoNFoXl5e9+7d\nwy1yz549Xl5eGzdu9PDwaGlpyc7Ofvvtt3H31tjYuHr1atzNicLJyYnNZvN4vNTU1MWLF4+RP5DL\n5Q4MDLS3t8PUPsbbEwDA5/NLS0sBAK2trR9//HFMTMxLL72EryuMPVtaWlxdXbGLIMzLrLfffjsy\nMtLIN2KEABerly5dmmxFDODp06cAgAsXLmhKzNme6enpMTExmGrYr53R0dE3btzArE0nBT6fz2Aw\n5s6dO9mKGICzszOXy+Xz+ZoSc7Ynn8+fN28ephrWIRISEshk8qlTp0yu4HiUlZUtWrTouTtIPiYm\nRntabbb2FIlEIpGIx+Nh6+mOLa+//npsbKxpx6/x6OjooFAoX3311eSqgYOvv/6aQqE8ffpUU2Ke\n9vz0009ZLJZUKsXUHMEhysvLEQQhMAgVB9nZ2U5OToODg5OoAz6kUqmdnd3HH3+sKTFPe4aHh69d\nu1a35ggOgaJocHCw7taJCePZs2c2NjbmsO0MH+vWrQsLC9NcmqE9f/zxRwRBKioqdCuPvBvg9OnT\nCILw+XwTqTg2f/jDH1xcXMaOSTVnYM5G7aSL5mbPDRs2eHh4jHi45qjbQxYvXhwYGIjZPTEB1NbW\nkkgkYo8vnniio6MxKzrzsWdrayuVStUOM9RmVIcQiURsNnvTpk3E6zg6fX193t7eBp1PZ55UVFQA\nALTTiJqPPf/0pz+5urrqTichY20g+/LLLxEEmbCpvkqlWrZs2fTp0w1NkGueLFmyBBOtZQ72rKmp\nGfug9nF2FGZmZtLp9KqqKsLUHJ1NmzZNmKwJAMZzYjYJT649lUrl3Llzo6KixgiJG8chVCrVqlWr\n2Gz2999/T5imOqAomp2dTSaTYVb3KcOePXsYDIZ28ODk2vP9999nMBhjZ/4bf8+xXC5fvXo1k8k8\nffq0sZqOxNDQUEZGBpVKNSaIwzxRKpXR0dF+fn7aM/zJsufFixdJJFJRUdHYzfUKU1GpVJs3b0YQ\nJCsri9gQZpFINGfOHDabfe7cOQK7NR+ePHni7Oy8cOFCbbtNvD0bGxsdHBxWrlw5bg8GxC199dVX\ntra2s2fPJmQ9PTQ09OGHH7LZ7LCwsIlPozGRXL9+3draOjU1FfPknjB7PnnyxNPT89VXX9Un6Z1h\ngWytra3w1NjExERMqj39USgUx48f9/X1ZTKZe/bsmcgUO5PFhQsXaDRaamoq5o+dAHu2tLT4+PgE\nBgZqZ7saAzyRjf/5z39eeeUVAEBMTExJSYlEItGzoUgk2rVrl5eXF5VKTU1N/fHHH3FIf065cOGC\ntbV1bGys7qkFprPntWvXnJycQkND9c/thz/U9dKlS8nJyfCA3sjIyO3bt3/55Zd37tzp6emBKVqk\nUunTp0+vXLny2WefpaenwwAmNze3HTt2TLF8lHpy/fp1Z2dnb2/vESOYibUniqIFBQU0Gi0+Pl4s\nFuuvpLGxz11dXSUlJVC/0Q6GZ7FYc+fOzcnJgYn/jZT4XPPo0aN58+bR6fSPPvpoRFMQYs/29vZl\ny5aRSKS8vDxDDY7/vAxd5HJ5U1NTV1dXX1+fWq2m0+k2NjYcDofD4Zg62OY5QqlU7t69e//+/YGB\ngUeOHNEO7MGAw54qlerIkSM7d+60tbUtLi6Oi4szWD88fm7BaB49erRmzRoAQGRkpKEnVY3IwMBA\nQUGBh4eHjY1NQUEB7tWsxSEmk8rKSriJLSIiorCwUHuflf7cvHlzy5Ytbm5uTCYzMzPz4cOHxqhE\n5CPDAj5qa2uLi4u/+eYbiUQSFhYGk0jOmjXL1dV1xPoKhUIkEtXX11dWVlZWVra2tvr7+6empq5f\nv17/09hHw+IQ5oJMJquoqLh06RKfz29sbAQAsFisEQ9ybWtrUyqVcAs1j8dbtGiRoSetjYHFIcyR\n3t7e5ubmpqamEc/+5nK5s2bN8vX1hUGFxGJxCAvDwMZlWPiNY3EIC8P4PwGgUT/fV2L8AAAAAElF\nTkSuQmCC\n",
      "text/plain": [
       "<IPython.core.display.Image object>"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "U = nx.DiGraph()\n",
    "U.graph['rankdir'] = 'LR'\n",
    "U.add_node(0, shape='circle')\n",
    "U.add_node(1, shape='doublecircle')\n",
    "U.add_edge(0,1, label='q')\n",
    "U.add_edge(1,1, label='True')\n",
    "U.add_edge(0,0, label='p')\n",
    "draw(U)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**R**elease - p**R**w"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAMgAAABwCAIAAADUo6jRAAAABmJLR0QA/wD/AP+gvaeTAAAZw0lE\nQVR4nO2deVhTV/rHz80ewqJsgjIQZAmCSq2yFSmb2IJS6wIqxQVF6/7MWAQtOLXClLYzWrSt4jPU\nKgWs7fhYwBkUELTI4opTFBAREGUrq5CQhJvc/P4488sTE7bc3EC09/MX9+Sc877k/d7t5Jz3IDKZ\nDJCQEA1lsh0geT0hhUWiFUhhkWgFUlgkWoEUFolWIIVFohVIYZFoBVJYJFqBFBaJViCF9QpTXFyM\nIIihoeHcuXM9PDwQBGGxWB4eHrNnz2axWAiCtLW1TZZvtMkyTKI5g4ODfn5+ly5d4nA4AAAEQbhc\n7s2bNwEA3d3dnp6eQqFwsnwjr1ivMEKhMDY2FqpKCRMTkx07dkyisBDyR+hXl8HBQQaDQaP977aD\nIAiPx6utrYWHIpGIQqEwGIxJ8Y28Yr3C6OnpyVWlCp1OLysr+/Of/8zlcltbW319fa2trZOTkxEE\nQRAEANDf33/kyBH5IQCAz+cnJSVFRUUtWLBg0aJFVVVV+J2TkbwuAAB4PJ78UCQSlZaWslgsAEBy\ncnJBQcHmzZsHBgZmzpypGHf5IYZh69atq6mpgeVBQUHm5uYvXrzA6YwG/wiJbqEkLIiDgwMAoLu7\nW17C4/EUhSU/LCkpUb3u5Obm4nOGfCt8zaFQKAAAY2PjMWvevn3b2dn54cOHxNglpBcAgEwmKy8v\n/+ijj7hcbnNz85IlS6ZMmeLu7v7rr78SZYJEq/D5/MbGRoFAoFgolUrx9UaYsDAM6+7uPnHixNOn\nT7/++uu4uLgTJ07U1NQEBgbK31NItIds3G/38FFdJBLBw6GhIdjc2dlZKBR+8cUX8prV1dXffPMN\nfocIBN7RxWIxPPzqq68AAFu2bCHWCokqAwMDAABra2ulci6XCwBAUVResmLFCgDAxx9/XFdX9/XX\nX8O7ZF5e3uDgIAzfpk2bMjIy4uPjg4KCdOXhXenB8MmTJwAAT09PYq2QKHH58uWNGzfCK0VcXFxp\naalMJuPz+YcPH4aFe/bsuXfvHqzc2Njo7++vp6fn7u5eWVm5cOHCyMjIrKwskUjU3Ny8bNmyqVOn\nTps2bcuWLb///jtulwgeIHVycnr06JG8T5FIxGazg4KC8vPzCbRCovtod4C0u7sbAODr66tVKyQ6\niFaEJX+VKCwsdHJy2rt3rzaskOgyWhFWWlpaV1dXV1dXW1tbRUUFm83WhhUSXUa7z1gkk45AIDh3\n7ty1a9fu3bvX09MzNDRkZGRkbm7u6+u7cuVKd3d3+Q+FxEIK67UFRdEjR458+eWXYrE4MDDQx8fH\nyMgIANDd3d3S0pKfn//48WMPD4+jR4++9dZbxJvX9E33ZaZPnw4UxrFIJounT5/OnTuXzWYnJCR0\ndnYOW+f+/fvBwcEIghw4cADDMGIdIExYAwMD+/btg2LdsGEDHEohmRQeP348ffp0V1fXhoaGMStn\nZmayWKzIyEipVEqgD4TdCjEMu3Tp0r///e/S0tKuri54L582bVpAQEBYWNi8efMIsUIyJj09PV5e\nXlOmTCkoKDA0NBxPk9LS0qCgoJiYGPmAquYQI6zs7OyYmJiGhgY3NzdfX98ZM2awWKyurq7m5ubs\n7Oz29vaQkJBvvvnG1tZWc1sko/PBBx/8+uuvt2/ftrCwGH+rM2fObNq0KS8v75133iHGDw2veFKp\ndPv27QiCREdHP378WLWCRCLJyclxdHTU09PDPbmHZJzAXzguXbqEo214eLijoyNRz8caCQvDsPXr\n1+vp6Y35n4jF4ujoaAaDceHCBU0skoyOl5dXSEgIvrZNTU0sFuurr74ixBONhJWUlMRgMIqKisZT\nGcOwXbt2cTgc+eRXEmKBU9/Ky8tx97B7924ul0vIUzx+Yd27d49KpZ48eXL8TVAU9fLymjdvnuIs\nDhKiWLt2rZubmyY91NbWIgiSk5OjuTP4hfX22297e3urO/5RX1/PYDDOnDmD2y7JsIhEIg6Hc/z4\ncQ378fLyWrduneb+4BTWjRs3AAD4Bqu2bt3q4OAgkUjwmSYZlsuXLwMAnj17pmE/ycnJpqammt8N\ncQ43rF69urm5uby8HEfbhoYGe3v7//znP++++y6O5iTDEh8ff+HCBXyzwMvKyuRLdGpra3Nyctas\nWYNhGIZhAAAul3vgwAG1O8UhRj6fz2az09LScMv57bffjoyMxN2cRJWgoKANGzbgaxsREYEgCPNl\n6HQ6nU5HEGTu3Lk4+sQzbaawsHBoaCg0NBRHW0hYWFhubi7uFSAkqlRVVb3xxhv42sKTXPwyKIqi\nKEqj0SIiInD0iUdY165dc3V1NTc3x9EWEhgY+OLFi//+97+4eyBRhM/nt7e329nZ4Wu+ePFiU1PT\nYT9CUTQsLAxHn3iEVVFR4enpqW4rFEUbGhoaGhpaWlrMzc0NDQ1v3bqFwzqJKs+fPwcAWFtb42tO\npVKjoqLodLrqRy4uLnANvrrgEVZNTc2cOXPUbZWVlWVnZ2dnZ2dlZWVqatrf3w9/C9LT0zMwMLCw\nsGhubsbhDAkAAK79gtOt8LFx40YURZUK6XT6mjVr8HWotrB+//33Fy9eODo6qtvQw8Nj2HKhUMjn\n8wcGBsazDJxkWMRiMQAA5v/Ah7Ozs6urq9JsUhRFw8PD8XWotrBaWloAAH/605/Ubejk5DSSHOl0\nemRkpL6+vrp9kkDgsmYmk6lJJ9HR0TDRgxwHBwccVxCI2sKCK7pMTExwGAsPDx/2Ro6i6ObNm3F0\nSAKBVywNhRUREaEoLDqdju99EKK2sGD2QXwLb5YvX656I0cQxNnZ2d3dHUeHJBA4cKN0vVEXY2Pj\nJUuWyM98FEVXrlyJuze10xjB1IMoiuLQ1ptvvjljxgx4M5VDoVC2bNmiblckisDBgq6uLisrK9VP\nBwYGGhoa+vr6ent7URTlcDhTp041MTGZOXOmUkLAqKioX375Bf49c+ZMHK9ocnAKC6YowcGqVatO\nnjyp2JxCoaxbtw5fbySQadOmAQA6OjqgsMRi8c2bN4uKikpLS2tra+FghCoMBsPe3n7OnDm+vr7+\n/v5OTk4hISEmJibd3d0MBmPt2rWauDTRwlq+fPmxY8fkh3Q6PTQ0FN8TG4kcOFjd3t5+5cqVjIyM\nixcvCgQCHo/n7+8fGhpqb29va2vLZrPheIREIhkYGOjt7a2vr6+vr6+srExISOjp6bG1tY2MjAwO\nDj537tzQ0ND777+vkU/q/gYERzWbmppw/H4kk8kkEsmUKVMUHcjLy8PXFYkcoVDIYDBMTU0RBPHx\n8Tl58mRzc/P4m0skklu3bu3fv9/GxkauVA1dUltYDQ0NAICKigrcJhUHeS0tLYlddfRHQyqVpqWl\nTZ8+ncFgrF+/HvcJD8EwrKioyMDAAADg6+srz3yEA7WFJZVKWSxWeno6bpO5ublQVXQ6/eDBg7j7\nIblz5467uzudTt+3b19XVxdR3QqFwoqKCj8/PyqVun379t7eXhyd4JmP5ezsHB4efujQIXjI5/Nv\n3Lhx48aN6urqhw8fdnZ2ymtSqVQul+vi4uLq6urn5+fq6kqhUIRCobGxsUgkQhCkrq7O3t5eXQdI\nZDJZSkrK/v373dzcUlNTZ8+erVpH3biomkhPT9+3b5+BgcH58+cXLFiglod4hPXee+8ZGhqePn06\nJyfn9OnTBQUFEonE1tZ23rx5Li4uim+8KIrW1dU9ePDg3r17fX19JiYma9eujYqK+uyzzy5cuODr\n63vt2jV1rZMIBILIyMicnJyDBw8ePHiQSqUqfjo0NIQ7Lm+++aaSrdbW1oiIiPLy8uPHj3/44Ydq\neInjKrd9+3ZHR0dLS0sajRYaGpqVldXS0jJ6E6lUev/+/S+//BKeW/CHgrNnz+Kw/genq6vLw8PD\n2Ni4oKBA6aO+vr7PP/9ck7h4e3tnZ2crrWNAUTQ2NhYAoNZzi3rCwjDs7NmzZmZmBgYGcXFxbW1t\najWHlJeXBwcHAwC8vLyqqqpw9PCHpaOjY9asWTY2NtXV1YrlRMVl6dKlCIJ4e3urxuXUqVM0Gm3H\njh3j7E0NYbW1tQUFBVGp1J07d2r+qHjz5k1PT086nZ6UlES+GI6H/v7++fPnOzg4tLa2KpZPWFwu\nXrxIo9HGed0ar7CKioqmTZs2a9asyspKtZ0dAQzDUlNT2Wx2YGDgSKl2SCAoii5atMjCwuLJkyeK\n5RMcl3/+858Igpw6dWrMTsYlrPPnzzMYjHXr1gkEApzOjkxVVZWDgwOPx9NwDOb1JiEhgcVi3blz\nR7FwUuISHx/PZDLHHOIaW1jp6ekUCiUmJobw3Fxy2tvb582bZ2VlRWprWAoLCykUitJ1YrLiIpFI\nAgICHBwc+vv7R2k7hrByc3PpdPr+/fuJ8XRk+vr6XF1dHR0dNUla/1oiEAi4XG54eLhi4eTGpa2t\nzczMbM+ePaM0HE1Yjx490tfX37Rpk/bOCUVaW1u5XK6/vz/5LK9ITEyMmZmZ4r5wuhCXrKwsCoUy\nyi97IwpLJBLNmzdvwYIFE5lQ9M6dO0wmMzExccIs6jgw1UVqaqq8REfigmGYn5+fj4/PSE1GFNYn\nn3yir69fX19PsI9jcezYMTqd/uDBgwm2q5tERUW5uLgoXpl0Jy6VlZUIgly5cmXY+sML69GjR0wm\n8x//+IdWfBwVqVTq5ubm4+ND7HUew7CysrK9e/fa2Ng8ffo0JCTEyMjIzc3t+vXrY7a9evUqnU7n\ncDjXr1/v7e394IMPAAB+fn5wFPHu3bsWFhaKFxWiaG5uZjAYiqkMdC0uixYt8vf3H7b+8MJavXq1\ns7Pz0NCQVnwci5s3byIIkp2dTWCfEokkNzcXLpCKiYm5fv16Zmamvr4+jUYbTyK47du3M5nMvr4+\nmUw2ODhobm4eEREBP0JRlPDTAPLXv/7V0tJS8Zana3GBmSkfPnyoWnkYYVVVVSEI8vPPP2vRx7FY\nsWLFG2+8QXi0cG+nCDe0/fbbb+FhaGionp4e3MsvOztbG5crqVRqY2MTGxsrL9HBuGAYZmdnFxcX\np1pzGGHt3r3b3t5+cvNXVVRUALz5t0ZBk+0U/f39XV1dMQxraGgICQmh0+lQT6tWreLz+cT6KZPJ\nSktLAQCK4+m6GZf4+HgbGxvVS4CysEQikbGxcXJystZ9HAtXV1fCt2ZVEhZcyhYUFDSethcuXAAA\n3Lx5c9u2bQ8ePFi9evX8+fMfPHjw0UcfEeskJCEhwc7OTn6os3G5e/cuAED1ZUtZWHl5eQiCPH36\nVOsOjsXnn39OSGo5RZSEBZevJCUljactiqJWVlbBwcEwk2JxcTEAwNfXV+nHO6Lw9PT88MMP5Yc6\nGxcMw0xNTVNSUpSqKQsrJiZm9uzZuK1iGJaWlrZq1aqPP/548+bNmZmZuLv67bffAAB3797F3YMq\nUFjyu8mZM2ecnJwGBwdlMtnf/vY3Gxub06dPj9I8MTERQRD4MohhGI/HW7p0KYHuyREIBHQ6PSsr\nS16iYVxkMtnz58+/++67sLAwDXdSVo3LsmXLVq5cqVRNWVju7u47d+7EbfXTTz+1sbHp6emRyWQ9\nPT02NjaqWh4nUqnU1NSUqLTjECis1NTUzs7Ozs7O5ORk+KInk8lg6hsjI6NRmnd2dv7lL3+RH54+\nfVqt3NcYhu3Zsyc1NXXMyS137twBAMB91CAaxgXS09MDAODxeJp0ohqXw4cPOzg4KFUDSm3YbPb3\n33+Pz2RTUxONRvvss8/kJUlJSXp6ergnCS1evDgqKgpf22FRuhUqUV1dvWDBAgLNKcHn8+GsXSqV\nGhISkpmZOdJTf0ZGBp1Olyct1zAuimguLJlKXM6fP0+lUkUikWKdl6bQP3/+XCgU4k4wkpmZKZFI\nAgMD5SUBAQGDg4NpaWn4OuTxeI8ePcLXVl34fP6hQ4dOnTo1AbakUumVK1fWr18/derUJUuWpKen\nyzUHqa+v53K58vXvGsaFcJTi4ujoKJVKm5qaFOu8JKxnz54BAOSrFtUF5uhWnLQPsx3hTglpbW0N\nXSIKmKBs2GXcT548SUlJUV1NoCWkUqlUKkVRtKCgYOPGjSYmJjAvK0ya0tvba2ZmJq+sYVwIRyku\nMHMEvM/KeUlY8HuH6xVx0NraCgCYOnWqvATmUmtsbMTXoZGRUX9/P762SvD5/NjYWOjh1q1by8rK\nlCq4urpaWloSYkst4P0OLq157733TExM1q9fX1dXp5gtTMO4EI5SXKBj0Ek5L+VuEAgEAAAOh4PP\nHtwdTzErHPwbd6IHDocjEAgI37T47NmzZ8+eJbZPzYHf0sDAwA8//AAAcHZ2ln+kYVwIB8ZF8RAA\noHQ3f0lYMHOXWCzW09PDYc/JyamkpKSvr0++U15vby8AAO7niwOxWMxkMrOysvA11zXEYvHoeXUY\nDMbQ0JClpaWJiYnirVDDuBAOjIv8EOYTVEpU+ZKw4DWNz+fj+wfgSdba2ioXFrz1LFy4EEdvAICB\ngQFDQ0N86aB1EMWzXBGopxkzZkRHR4eFhbm4uOzevVvxwVTDuBAOjIviIfj/+5Wcl56x4FnS3t6O\nz96qVasoFEpRUZG8pLi4WJOMg21tbZpkk9dxYGYUY2Pjbdu2lZSUNDc3Hzp0yMXFBQBgaGio+BCj\nYVwIRykufX19YHRh2dvb02g0fPuxAACsrKwOHDhw6tQp+KX09/efOnUqISEBRyZcSG1tLRx5ep2g\n0WhUKpVOp4eEhJw/f/758+fHjh1buHChYvaEmTNnwql88FDDuMiBl0y4Q44mKMWlvr4eQRClfZlf\nuhUyGAxbW1s4RQQfiYmJtra2O3futLa2rquri4uLi46Oxt1bdXU17jzjOgiTyYRrANetW7dixQql\nPGGK8Hg8gUDQ2to6Y8YMQERcAADFxcUZGRkAgKampqNHjwYEBODeIkUpLnV1dZaWlsovrUqDqtHR\n0d7e3hqOzBICHKS4evXqZDsyCXR0dAAA8vPz5SW6HJdNmzYFBAQoVVNOXuPn53f79m2lMYlJobi4\nmMVieXl5TbYjk4C5uTmPx4MTKCC6HJfi4mIfHx+lasrCCg0NpVKpP//8s9YdHIusrKzg4GB8eb9f\nAwICAhRfg3Q2Lo2NjY2Njf7+/sr1VK9177///qJFi7R7PR2LtrY2Go32448/Tq4bk8hPP/1Eo9E6\nOjrkJboZl2+//ZbD4QiFQqWawwgrNzcXQRACk0zgIC4uzszMDM6U+mMiFAqnTJly9OhReYluxsXd\n3X39+vWqNYcRFoZhrq6uqlO3JozOzk4DAwNdmIY7uWzYsEFxV3odjMvjx48RBBk27/Xwk5MuXryI\nIEhxcbGWXBydrVu3Tps2bfScE38Erl+/DgAoKSmRl+haXHbs2GFtbS2fN6bIiLPelixZ4uLiojR7\nawKoqKigUCgZGRkTbFc38fPzU3qT1524NDU1yZcqqTKisBobGw0NDXfv3k28jyPT19dnZ2f37rvv\nTqRRXSYvLw8AoLhcW3fism3bNktLS9XHdsho2WbOnTuHIMiEvZpJpdLly5dbWFi0t7dPjMVXgqVL\nlyqtftaFuJSXl1MolB9++GGkVmPkx9q1axeTySwqKiLMzZHZvXv3hNl6hYD5GpQWlUxuXCQSiZeX\n18KFC0dZqj6GsKRS6erVqw0NDa9du0aYpypgGBYXF0elUn/66SftWXl1SUxMZLFY9+/fl5dMblw+\n+eQTFos1esbrsVNFisXiNWvWsNnsixcvaurpcAwNDW3ZsoVOp2uyCPH1RiKR+Pn5OTo6Kr6RTVZc\nCgoKKBTKiRMnRm8+ruS2Uql0z549CILExMQQm+qksbHR09PT0NDw8uXLBHb7+tHS0mJubv7OO+8o\nfv8TH5fq6mpjY+OwsLAxe1Ajz/uPP/5oZGQ0Z84cQsZRhoaG/v73vxsaGrq5uU18GrFXkVu3bunr\n60dGRio92UxYXFpaWmxsbN56663xJGlWb2eKpqampUuXAgCWLVumlBp6/KAoevbsWQcHBzabnZiY\nOJEpD1918vPzGQxGZGSk0pc2AXGB22m5uLgoZkMdBTx76fzyyy/z588HAAQEBMDFluNs2NjY+Omn\nn9ra2tLp9MjIyMePH+Ow/gcnPz9fX19/0aJFqru9aS8uZWVlZmZmCxYsGH9OazzCgly9ejU8PJzJ\nZDKZTG9v79jY2HPnzv322289PT0wFYlQKOzo6CgpKTl58uSmTZvgQt7p06fv37+fzOeuCbdu3TI3\nN7ezsxs2YwqxccEwLCUlhcFgLF68eGBgYPxO4hcWpKurKz09HfqntL+ZHA6H4+XldeDAAbjRmYYW\nSWQy2bNnz3x8fJhM5pEjR4b9SgmJS2tr6/LlyykUSkJCgrqBw7Nf4UiIxeKampquri6YwoXJZBoY\nGHC5XC6XS/iiUxKJRHL48OEvvvjCxcUlNTXV3d19pJo44iKVSlNTU+Pj442MjNLS0oKCgtT2D8/5\nQqIzPHv2DC6C9fb2zsnJ0bxDgUCQkpJibW1tYGCQkpKCexSDFNbrQGFhIZwc7OHhcfz4ccV5p+Pn\n7t27e/funT59OpvN3rVrl4bZA4m8FZJMLhUVFWlpaf/617/4fL6bmxtMwj5r1qyRkp2gKNrY2FhZ\nWVlYWFhYWNjU1OTk5BQZGbl582b5WnbckMJ63RCJRHl5eVevXi0uLq6urgYAcDgcW1tbNpttZGQE\nAJBIJAMDA729vc3NzRKJBC658ff3Dw4OVndH8VEghfU609vbW1tbW1NT09DQ0NfX19vbi6Ioh8OZ\nOnWqiYkJj8ebNWuWg4MDg8Eg3DQpLBKtoLyukISEEEhhkWiF/wMljXFGcdeLZAAAAABJRU5ErkJg\ngg==\n",
      "text/plain": [
       "<IPython.core.display.Image object>"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "R = nx.DiGraph()\n",
    "R.graph['rankdir'] = 'LR'\n",
    "R.add_node(0, shape='circle')\n",
    "R.add_node(1, shape='doublecircle')\n",
    "R.add_edge(0,1, label='p, w')\n",
    "R.add_edge(1,1, label='True')\n",
    "R.add_edge(0,0, label='p')\n",
    "draw(R)"
   ]
  },
  {
   "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": 10,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAATMAAABwCAYAAABy45coAAAABmJLR0QA/wD/AP+gvaeTAAAgAElE\nQVR4nO3deVxUVf8H8M+dgRn2RRBQATFkEVDUAFdMUMvMxF0xUcGtx4V8nlcqlk+mmEuaVi/LMLPc\nKzMtTSFkSdBSLHcU0TBlcWWRZQaYme/vD3/M4zjDNtyZYTnv16s/PDP3nO90hu/ce86953BERGAY\nhmnZDggMHQHDMAwfWDJjGKZVYMmMYZhWgSUzhmFaBZbMGIZpFVgyYximVWDJjGGYVoElM4ZhWgWW\nzBiGaRVYMmOYNiolJQUcx8HKygo9evRAnz59wHEcTExM0KdPH/j5+cHExAQcx6GgoMDQ4dbLyNAB\nMAxjGBUVFRg8eDCOHj0Kc3NzAADHcXBzc8OZM2cAAI8fP0bfvn0hkUgMGWqDsDMzhmmjJBIJlixZ\nokxkmtjZ2WHevHktIplx7EFzhmmbKioqIBKJYGT0vws0juPg5eWF69evK8ukUikEAgFEIpEhwmwo\n9qA5w7RVZmZmKomsNsbGxjh9+jQWLVoENzc35Ofn46WXXoKrqyvWrl0LjuPAcRwA4MmTJ/joo49U\nygCgrKwMq1evRmRkJAICAjB06FBcvnyZ3w9EDMMw/w8AeXl5qZRJpVI6deoUmZiYEABau3YtJSYm\n0syZM6m0tJReeOEFej6VPFumUCgoIiKCrl27pnx92LBh5ODgQCUlJXyF/j27zGQYRknTZWYNT09P\nZGdn4/Hjx2jXrp2y3NvbG1lZWXg2lTxblp6ejuDgYI3tHTlyBCNHjuQj9ANsNpNhmAYRCJ6OSj2b\nyBoiIyMDPj4+uHr1qi7CUmJjZgzD6FRZWRlycnJQXl6u9ppcLuetHZbMGIYBAGg74lQz0C+VSpVl\nVVVVyjp9fHwgkUiwfv16leMyMzOxZcsWLaNVxy4zGYYBAOWZU233lFVWVgIAZDKZyiyoj48Prl+/\njtjYWMyYMQMJCQkoKSkBACQkJGDEiBHw8PBAbGws8vLyEBoaimvXruHs2bP44YcfeItf+P7777/P\nW20Mw7RICQkJ2LBhAy5cuICSkhJIpVKYmZnBxcUF5eXlWL9+PQ4dOgQAKCkpgZOTEzp06AAA6NOn\nDy5duoSDBw8iPT0d8+fPx7lz5zBo0CC4uLjAx8cH48ePx99//42EhAQkJSXB2dkZn332WaPH3+qQ\nyWYzGYZpDdhNswzDtA4smTEM0yqwZMYwTKvAkhnDMA12/PhxREZGwsfHB+3bt4ejoyO6d++OqKgo\npKena317Bx/YrRkMw9Tr5s2bmDFjBk6dOoXg4GBMnz4dtra2qKysRF5eHpKTkxEcHIzQ0FB88cUX\n8PDw0HuMLJkxDFOnlJQUhIWFwdPTExkZGQgICND4vkuXLmH69Ono1asXEhISMGDAAL3GyW7NYBim\nVhkZGRg8eDBGjx6Nr7/+ut41zaqqqjBu3DicPHkSJ0+ehL+/v54ixQGWzBiG0aisrAw9e/aEu7s7\njh07BqFQ2KDjKisrMXToUBQVFeHcuXMwMTHRcaQA2H1mDMPU5oMPPkBhYSF27tzZ4EQGAGKxGHv2\n7EFubi4++OADHUaoiiUzhmHUFBQUYPPmzVixYgWcnJwafXznzp3xzjvv4JNPPkFhYaEOIlTHkhnD\nMGq2bt0Ka2trzJ07V+s6/vWvf8HY2JjXlTHqwpIZwzAqFAoFvv76a8yePbtJ412WlpaYPn06du3a\npZf7z1gyYxhGxenTp5Gbm4vJkyc3ua4pU6bg1q1byn04dYklM4ZhVBw/fhzu7u7w8/Nrcl0BAQFw\ndXVFfHw8D5HVjd00yzCMitTUVISGhja5HiJCcXEx+vXrh8TEREybNg1VVVXKRSA9PDxgZWXV5HZq\nsGTGMIwSEeHixYuYOXOm1nU4OzsjLy9Prdzd3V3l3/Pnz+d1coBdZjIMo5SXl4fy8nJ4eXlpXYez\ns7NyJ6e6DBo0SOs2NGHJjGEYpezsbABo0oPiDbmdQywW87VfphJLZgzDKGVnZ8PGxgYODg5a1zFx\n4kSIxeJaXzcyMsLLL78MMzMzrdvQhCUzhmGUcnNz4eLi0qQ6zM3NMXny5FofSlcoFBg/fnyT2tCE\nJTOGYZQqKipgbm7e5HqioqKUe2c+TyAQYNSoUU1uQ61e3mtkGKbFkkgkvKxyMXDgQLi7uys3CK4h\nFAoRHBwMGxubJrfxPJbMGIZRkkqlMDU15aWumTNnqmwWXGPChAm81P88lswYhlGSSqV1Dt43xrRp\n0yCXy1XKFAoFxo4dy0v9z2PJjGEYJaFQiOrqal7q6tSpE4YOHao8O+M4DoGBgXB0dOSl/uexJwAY\nhlGytbXFrVu3an29oKAAeXl5KC4uRlFRkfIYGxsbdOrUCR06dFB5/6xZs5CYmAjgaaKcOHGizmJn\nyYxhGCVbW1tlknr48CF+++03pKSk4Ny5c8jKykJJSUmdx1tbW8Pb2xsBAQEICQlB//79YWFhgdLS\nUshkMoSFheksdpbMGIZRMjExQX5+PgYNGoT09HQYGRmhX79+GDJkCObMmYOuXbvC2dkZpqamyokC\niUQCiUSC3Nxc3Lx5Ezdv3sSpU6ewbds2yOVydOjQAaWlpfD29kbXrl11Fjvb0IRhGNy9excbNmxA\nXFwcZDIZwsPDMWnSJISEhMDCwkKrOsvKypCcnIytW7ciPj4exsbGmDdvHhYvXoxOnTrx/AnY7kwM\n06YVFhbivffew5dffglXV1csWbIEU6ZM4eXG2WetWbMGRkZGiIuLQ15eHubOnYuVK1fyeb8ZS2YM\n0xYREbZv34533nkHYrEY69evx+TJkxu1C5M2ZDIZ9u7di2XLlkEmk2HdunWIiorio2rdJbOysjKk\np6cjPT0dmZmZuHr1Kh4+fKjyHqFQCDc3N/j6+sLf3x+DBw+Gv79/g5YPYVqOu3fvIiUlBWfPnsW1\na9dw/fp1SCQSlfeYmZnB29sb3bp1Q1BQEEJCQuDs7GygiFu3oqIiREZG4ujRo5g/fz5iY2PrXCRR\nF/1XUlKCd999F1u3bsXo0aPx1VdfNfUsjd9kVlVVhZ9//hk7duxAYmIiZDIZunTpgl69esHX11ft\nw1VXV+PGjRu4cuUK/vrrLxQXF8POzg7h4eGIjIxE7969+QqN0bN79+5h9+7d+Oabb5CZmQljY2P0\n6NED3bt3h6+vr9ofz5MnT3DlyhVcuXIFFy9ehEwmg5+fH2bMmIGpU6fq7N6ktubixYsICwuDVCrF\nvn37al1RVl/99+uvv2Lq1KmwtLTE4cOH0b17d20/2gEQD4qLi2ndunXUoUMHMjIyotdff5327dtH\neXl5Da5DLpfThQsX6MMPPyQ/Pz8CQAMGDKCffvqJFAoFH2EyepCZmUmRkZEkEonIzs6OFi5cSElJ\nSVRWVtbgOsrKyujEiRO0YMECsrOzI5FIRFFRUXTt2jUdRt76paSkkLW1NQ0YMIDy8/M1vscQ/Zeb\nm0t9+/YlGxsbOnnypFafjYi+b1IyUygUtHPnTmrfvj1ZWlrS0qVLqaCgoClVKv3+++80cuRI4jiO\nBgwYQJcvX+alXkY3SkpKaMGCBSQUCsnLy4t27txJlZWVTa63srKSvvnmG/Lw8CChUEjR0dH05MkT\nHiJuW3755RcyMTGhcePGkUQiUXvd0P1XUVFBY8aMIRMTEzp+/Lg2TWmfzAoKCmjYsGEkFApp/vz5\n9OjRI22rqtOZM2eob9++ZGxsTKtXrya5XK6TdhjtJSUlUadOncjBwYG2b9+ukz6SyWS0bds2at++\nPTk7O1NKSgrvbbRWp0+fJjMzM4qKitLYN82l/2QyGc2YMYPMzc3pjz/+aGwT2iWz5ORkcnR0pG7d\nutH58+e1qaJRFAoFffHFF2RqakpDhgyhhw8f6rxNpn4KhYJWrFhBAoGAIiIiqKioSOdtFhYW0htv\nvEFCoZBWrlzJhiDqkZWVRe3ataNRo0ZRdXW1ymvNsf+qq6tpxIgRZG9vT9nZ2Y2puvHJ7LvvviOR\nSEQRERFUXl7e2MOb5PLly+Th4UFeXl50+/ZtvbbNqKqurqbp06eTWCymb775Ru/tb9++nUQiEUVG\nRqr9kTJPSSQS8vf3p4CAAKqoqFB5rTn3X1lZGfXs2ZN69+5NUqm0oVU2Lpnt2rWLBAIBvf322wb7\nRbx37x716tWLnJ2dWUIzEJlMRuPGjSMLCws6ceKEweJISEggCwsLmjBhAslkMoPF0VzNmzePbGxs\n6NatWyrlLaH/bty4QVZWVhQdHd3Q6hqezI4cOULGxsYUExPTiHB1o7i4mPz9/cnT05MePHig9/aT\nk5MJAFlaWlL37t0pKCiIAJBYLKagoCDy9fUlsVhMAGqdNWqpFAoFzZo1i0xNTSktLc3Q4dDJkyfJ\n1NSU5syZwy45n5GSkkIcx9GBAwdUyltS/+3fv584jmtonA1LZllZWWRhYUFRUVHN5guTn59Pbm5u\nFBISovdJgaNHj9LgwYNVpqsBkJeXl/Lfjx49oq5du6r9KrZ0H3/8MQmFQvr5558NHYrSoUOHSCAQ\n0JYtWwwdSrMgkUioa9euNGHCBLXXWlr/jRkzhjw9PRtyuVl/MpNKpdSrVy8KCAjgZaqWT+fOnSOx\nWEyxsbF6bffAgQN07NgxlbLnkxkR0aZNm+jKlSv6DE2n/vzzTxKLxbRq1SpDh6JmxYoVZGJiQhcu\nXDB0KAa3adMmsrCwoH/++UelvCX2399//01mZmb06aef1ldF/clsxYoVZGFhQTdv3mxCqLrzySef\nkLGxsV6TRnl5udqgpaZkJpFImt0PgLaqq6upR48eBjkTbgiZTEYvvfQS9e7du02Pn5WWlpK9vT0t\nX75cpbwl919MTAw5OjqqTWI8p+5klpWVRWKxmDZu3MhDuLohl8spMDCQgoODDXoJrCmZyWQySklJ\nobfeeos6d+5MeXl5NGjQIHJxcaE1a9YQAAKedkFJSQlt3LhRpYzo6ZczNjaWZsyYQS+++CINGTKE\nLl26pNfPRkS0ceNGEovFlJWVpfe2G+ratWskEono448/1nvbCoWCPvroI5o8eTLNnTuXRCKRsi+f\n7U9d27JlC5mamtK9e/dUylty/+Xn55OJiQlt3bq1rsPrTmaTJk0iHx8fqqqq4iFU3Tlz5gxxHEc/\n/fSTwWLQlMykUimdOnWKTExMCACtXbuWEhMTaebMmVRaWkovvPCC2hf92TKFQkEREREqj4EMGzaM\nHBwcqKSkRPcf6v+VlJSQra0tvfPOO3prU1uLFy8mOzs7vT8l8PHHH5NAIFDePP7ZZ58RAPr3v/+t\n1zi6detGc+fOVSlrDf03e/Zs8vPzq+vQ2pPZ5cuXNc6GNFdjx46lnj17GuzsTFMyq+Hh4UEA6PHj\nxyrlXl5easns2bK0tDSVX/dn/zty5IhuPogGq1atIltbW70mUG0VFxeTjY0NrV69Wq/tvvLKK8Rx\nnHJY4f79+wSA+vbtq7cYzpw5QwAoIyNDpbw19N/Zs2cJAJ07d662Q7+vda2dbdu2wd3dHWPGjNH2\nKXa9WrJkCS5cuIDff//d0KGoqVnSqF27do06LiMjAz4+PiAitf9Gjhypi1DVyOVyxMXFYfbs2XUu\nE9NcWFtbY9asWYiLi4NCodBbu/379wcR4ZdffgEA5Tr6w4YN01sM+/fvh4eHBwICApRlraX/AgMD\n4enpiW+//bb2gzWlOKlUSu3ataO1a9fylnH1wd/fn2bPnm2QtlHHmZmmM7Dayp8tW7VqFZmammpc\nsUBfg9zHjh0jjuOa7QSQJjdu3CCO4yghIUFvbSoUCvryyy/J1taW3n77bRo9ejStXbtWr5MRXl5e\naveBtqb+i4mJIV9f39oO03xmlpKSgqKiIkyZMoXXrKtr4eHhOHTokF5/kYGnq3Zqo2breqlUqiyr\nqqpS1unj4wOJRIL169erHJeZmYktW7ZoGW3jHDx4EEFBQXB3d9dLe3zw8PBA7969cfDgQb21KZfL\nceXKFfzxxx/YsGEDDh06hJiYGJ2v3Frjzp07yMrKwtChQ1XKW1P/hYaG4urVq8jLy9N4nMZklpSU\nBF9fX7i6uvIWIBHhq6++woQJE/Duu+9i1qxZ2LdvH2/1A8CIESPw6NEjXLhwgdd661NeXg4Aaqtv\n1qisrATwdMngZ/n4+AAAYmNjkZ2djS1btii38kpISMCIESPg4eGB2NhYzJw5E3v37sXy5cuxaNEi\nREZG6urjqPj1118xYsQIXuvMy8vDjh07MHHiRPTr14/Xumu89tprOHHihE7q1mTNmjU4cuQI0tLS\nEB8fj9OnTyMrK0v546Rr6enpEIlEav8/+e4/hUKBzZs3w9fXFxYWFggMDMR3332n9Q96bTT1X79+\n/WBsbIz09HTNB2k6XwsKCqL58+fzeOJItHLlSurcuTMVFhYS0dOn5zt37szrNLpcLid7e3vavHkz\nb3XWJz4+nmbMmKEcmF+6dCmdOnWKiJ4+MLtq1Srla9HR0fTXX38pj83JyaGQkBAyMzOjoKAgOn/+\nPA0cOJCmTp1K+/btI6lUSnfu3KGwsDCytbUlR0dHmj17tlaPcP373/+mzz//vFErjvzzzz8EgFJT\nUxvdXn0KCwvrvDRvqhMnThAAys3N1Un9z/v111/JwcFBbaLG1taW9uzZ0+B6fvvtN4qOjqb09PRG\nTWbFxMSQv7+/Spku+i86OpreeOMN2rJlC0VHRytn6r/88kve2iCqvf/8/Pzo3Xff1XSI+mymXC4n\nU1NT+vrrr3kL7Pbt22RkZERr1qxRKV+9ejWZmZnxuhbayy+/TJGRkbzV1xpUVVUp/7iEQiENHz6c\ndu/eXe/tC0eOHCGO4xq1ymhj6DKZFRcXEwC1JzV0Zffu3So/onK5nO7evUu7du0iOzu7BtezdOlS\nZV916tSJYmJi6OLFi/UeN3r0aLXHl/juv5ycHAoPD1cpS0hI0Ek/1tZ/48ePp3Hjxmk6RH3MLDc3\nFxKJBJ6enk08UfyfvXv3QiaTYciQISrloaGhqKiowPbt23lry8vLC1lZWbzV19rI5XIkJiZixowZ\nsLGxwZAhQ7Br1y6UlZWpvTcrKwsdO3bkfdsxfbC2toaTk5NevgurVq1CREQEpk+friwTCARwdnZG\n//79Gz1eJRaLATy9HN+0aRP8/f3RqVMnvPXWWzh//rzGY27evAkPDw+VMr77Lzc3F5s2bVIpGzZs\nGOzt7Wsdx9JWbf3n4eGB7OxsjceoJbO7d+8CADp37sxbYDXXuM9vaOLi4gLg6SYLfHF1dVV+BkYz\nuVwOuVwOhUKBtLQ0REZGws7ODiNHjsSBAweU4zx3797l9Xugb507d9bLd6Hm+71582blZA4RISMj\nA8uWLcPu3bu1rrumL/Lz8xEXF4fevXvDy8sL77//Pm7duqV8X2FhIezt7VWO5bv/Bg4cCCcnJ40x\n9u/fn7d2amjqP3t7exQWFmp8v1oyKy0tBQBYWlryFlR+fj4AwNbWVqW85r6rnJwc3tqytrbGkydP\neKuvtauuroZCoUBVVRUSExMxceJE2NvbY9q0acjMzNR6N+vmwMrKSi/fhd27d2PevHnYs2cPOnbs\niODgYIwfPx5//fUX9uzZw9tVTs1EUnZ2NtasWYOuXbuiV69e+OSTT1BaWqr2N1tWVsbr37Emp06d\nglQqxapVq3ivW1P/WVpaKnPU84yeL6iZmePz0qLmZr2aWxFq1Pybzxkfc3NzlJaWqrXF1K+mH0pL\nS5VnE97e3oYMqUksLCxw9uxZvX8Xas7UfvzxR7z55puNPl4kEtX5OhGhuroawNOrmkWLFgFQ//sq\nLy/X6RCBTCZDTEwMtm3bhj59+vBev4WFhTIf1TA3N1crq6GWzGqu1ysrK2FmZsZLUN7e3khLS0Nx\ncbHKaWrNXdIdO3bkpR3gadxisRg7d+7krc6WTi6XIzw8vEHvFYvFqKyshJOTE+zs7Fr0fpVSqRTu\n7u5Yvny5oUNpsL179yI+Pr7e9wmFQnAcByLC0KFDkZqaqrZ5tlgsrvUshg/vvfceXnrpJZWxQj5J\npVJYW1urlZmYmGh8v1oyqzktLSsr4y2Z1dxPlZ+fr5LMai4/Bw4cyEs7wNOzChsbG0yYMIG3Olu6\nml/x2hgbG6O6uhoODg6IjIxEREQEfH19sWDBAly+fFlPUfKvtLQUHh4eLeq78Oeff9aazAQCgfLs\na9iwYQgPD0dYWJhysPz5SRwLCwteh3CedfjwYZiYmOC///2vTuoH/td/z5fVdumsNmbWvn17AE93\nNObL+PHjIRAIkJycrFKekpICY2NjXp80KCgogIODA2/1tVbGxsYAABsbG7z55ptIS0tDQUEB1q1b\nB19fXwBPvwt8fg/0raCgQPl9bqk4joOxsTE4jkNgYCA+//xz3L9/H8ePH8e0adOUZy5WVlbKG65r\n6Kr/4uPjkZubi/fee0/l0jYtLY3XdjT1X0lJidrZWg21M7OuXbvCyMgI169fR48ePXgJytnZGcuW\nLUNcXBzmzJmjHNiLi4vD8uXLlbOafLh+/Tq8vLx4q681MTIyAhFBIBBg+PDhmDJlCkaNGlXrGbi3\ntzf+/vtvVFVV1TuO01g14x66evRMKpUiJyenRY75VVdXw9TUFBKJBK6uroiIiEB4eLjyCkeTF154\nQWV2E9BN/yUmJmL9+vUYN26c8pE6hUKBrKwsWFtbIzg4mJd2auu/mzdvokuXLhqPUUtmIpEIXbp0\nwdWrV3kJqkZsbCy6dOmC+fPnw9XVFTdu3MDSpUsxa9YsXtvJzMzE5MmTea2zpRMKhejYsSO6du2K\niIgIjBs3Tm1mWRMvLy/IZDLcuHEDfn5+vMWTkpKCPXv2AABu376NTZs2ITQ0FD179uStjaysLCgU\nihb3w+bi4gJ7e3uEh4cjPDy8wQPrXl5eyMjIUCvjs/9Onz6NsLAwSCQSpKamqr3+fDJtitr6Lysr\nq/bbQDTdSjtr1iwaMGAAr3f06kNOTg4BoKSkJEOH0irI5XJq166dQVZubaqNGzdS+/btm80GPLq2\nZcsWsrW1VVkSu7X1n1wuJ2tr69pWnNW8asbgwYORkZGh05kQXUhJSYGJiYnOHl5uawQCAYKDg5GU\nlGToUBotKSkJgwYNajO36AQHB6OoqEhlkYXW1n9//vknSkpKar2U1ZjMXn/9dQiFQhw4cEA3kerI\nvn378Oqrr8LU1NTQobQa48aNQ3x8PB49emToUBrs/v37SExMxNixYw0dit50794djo6OapNsran/\nkpOT4eTkVOvYocZkZmVlhVdeeQX79+/nP1IduXfvHlJTUzFp0iRDh9KqhIWFwcjISK9rgzXVjz/+\nCJFIhFGjRhk6FL3hOA6DBg1Su62jNfXf8ePHERISUvvZdm3XrDVP3J8/f14HV8T8W7p0KbVv376+\n7agYLUybNo28vb2b5RZlz5PJZOTp6dkmV045fPgwcRxHOTk5KuWtof9u3bpFHMfR0aNHazu09g1N\nFAoF+fv717bcRrPy8OFDsrS0bHHLfLcUmZmZJBAIaP/+/YYOpV67d+8moVDYrLdU0xWpVEq2tra0\nfv16lfLW0H9r1qwhOzu7uvahrXuruUOHDhHHcZSSksJPpDoyZ84ccnR01Pv2Ym3JlClTyM3NjcrL\nyw0dSq3KysrIxcWFpk+fbuhQDGbhwoXk6uqq9kffkvtPKpWSs7MzLVq0qK7D69/R/LXXXiNfX1+S\nSqVNi1RH/vjjDxIIBI1azZNpvPz8fLK2tqZly5YZOpRaLV68mGxtbdU2wG1L7t69S2KxWO32hZbc\nf59++imZmppSQUFBXYfXn8xycnLIysqKFi5c2MRQ+VdcXEzu7u40fPhwQ4fSJsTFxZFQKGyWZ+on\nTpwggUBA27dvN3QoBhcVFUVubm5q48ctsf/Ky8vJxcVFbWNjDepPZkRE+/fvJ47j6Ntvv9UyVP7J\n5XIaM2YMOTk5telfYn0bO3YsdejQQW9r6zfEnTt3yMnJiSZOnGjoUJqFgoICsrGx0biDeUvrv5qz\ntfv379dXTcOSGRHRggULSCwWU3JyciND1Y2FCxc2q3jaisLCQvL29iY/Pz/l5jSG9PjxY/Lx8SEf\nHx8qKioydDjNxsaNG8nExISys7NVyltS/12/fp3EYnFDn2BoeDKTy+U0adIksrKy0sluPQ2lUCho\n6dKlJBQK6fvvvzdYHG3ZnTt3yMXFhYKCgujx48cGi+PRo0cUGBhInTt3prt37xosjuaourqaevfu\nTQEBAWrj3S2h/yQSCfXq1YuCgoKourq6IdU1PJkREVVWVtLkyZPJ1NSUDh061JhDeVFVVUWzZ88m\nY2Nj2rt3r97bZ/4nOzubunTpQr6+vvTPP//ovf3bt2+Tj48Pubu7t6jduvXpxo0bZGlpqXG8u7n3\n35tvvknW1tZ069athlbZuGRG9PQMLTo6mjiOo7fffpuqqqoaW4VWcnJyqG/fvmRlZUXx8fF6aZOp\nW35+PvXq1Yvs7Ozo559/1lu7hw8fpnbt2lFAQEB9M1xt3t69e4njOPr888/VXmuu/ffpp58Sx3GN\nvfJqfDKr8e2335K1tTV1795dp7MjVVVVtGHDBrKysqLAwED2K9zMSCQSmjdvHnEcR2+88Qbl5eXp\nrK3c3FwKDw8njuNo4cKFzfZ2oeZm1apVJBQK6eDBg2qvNbf+++GHH0ggEKjtsdsA2iczoqeniiNH\njiQAFBYWRufOnWtKdSqqq6tp586d5OHhQaamphQbG1vX3b+MgR07doy6dOlCFhYWtGzZMq12Xa/N\ngwcPaOnSpWRhYUHu7u7szFwL8+fPJ5FIVOvwTHPov927d5NIJKLo6GhtmmlaMqtx+PBhevHFFwkA\nhYaG0q5du7TeRTknJ4dWrlxJXbp0IWNjY5o6darajAzTPJWXl1NsbCy1b9+ezM3NKSoqik6ePKnV\nmmIKhYJ+++03ioyMJHNzc3JwcKAPPviAPXurJYVCQf/5z3+I4zhat26dxmxwW98AAAMfSURBVPcY\nqv8UCgWtXr2aOI6jxYsXa7sGHT/JrEZSUhJNnDiRxGIxicViGjBgAC1ZsoT2799Ply5dosLCQuXD\nrhKJhO7fv09paWm0detWioqKIk9PTwJAHTt2pJiYGLp9+zaf4TF6UlFRQXFxcRQYGEgAyN7ensLC\nwmjdunX0yy+/0O3bt6mkpET5/pKSErp9+zYdPXqU1q1bR6NGjSI7OzsCQH369KFt27axJMaT9evX\nE8dxNH78eCouLtb4Hn32X1FREY0ePZoEAgFt2rSpKR/te46IiO8lPB4/foxjx44hNTUV6enpuHXr\nFuRyea3vNzc3R48ePTB48GCEhoYiJCQEQqGQ77AYA7h69SoSEhKQkpKCs2fP4sGDB3W+39HREUFB\nQQgJCcHw4cPRrVs3PUXadsTHxys3Q9mxY0ed6/brsv9SU1Mxc+ZMlJWVYc+ePRg2bJjWnwnAAZ0k\ns+dVVlbi2rVrePToEYqLi0FEEIvFsLS0hJubG9zc3NrMiqBt3ePHj3H9+nU8efJEuTWapaUlrKys\n4O3trdzlntGtvLw8REZG4sSJE4iMjMSHH34IOzu7eo/jo/8ePnyIxYsXY9euXXjllVewY8cOdOjQ\noakf6QCvl5kMw7QsJ06coG7dupFYLKY5c+bo9J6z7OxsioiIIJFIRD4+Pnzv1aGby0yGYVoOiUSC\nr776Chs2bMCDBw8watQoTJkyBa+++mqTt6irrKzE8ePHsXfvXhw9ehSOjo5YsmQJoqKiat2ZXEv6\nucxkGKb5q6qqwvfff49du3YhOTkZ5ubmCAkJwdChQzFgwAC4u7vDysqqzjqePHmCmzdv4tSpU0hM\nTERqaioqKiowdOhQTJs2DRMmTFBuQM0zlswYhlGXn5+Pn376CampqUhNTVUO/Ds4OMDZ2RmmpqbK\njYMkEgkkEglyc3OV73N0dMTgwYMREhKCUaNG8TEmVh+WzBiGqRsR4c6dO8jKysK1a9eQn5+P4uJi\nFBUVAQBsbW1hY2ODTp06wdvbG97e3nBxcdH3pB5LZgzDtAoHNG41xzAM09KwZMYwTKvwf7r8Lgpx\nyWRbAAAAAElFTkSuQmCC\n",
      "text/plain": [
       "<IPython.core.display.Image object>"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "XX = nx.DiGraph()\n",
    "XX.graph['rankdir'] = 'LR'\n",
    "XX.add_node(0, shape='circle')\n",
    "XX.add_node(1, shape='circle')\n",
    "XX.add_node(2, shape='doublecircle')\n",
    "XX.add_edge(0,1, label='True')\n",
    "XX.add_edge(1,2, label='g')\n",
    "XX.add_edge(2,2, label='True')\n",
    "draw(XX)"
   ]
  },
  {
   "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": 11,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAALAAAABwCAIAAAAxPW29AAAABmJLR0QA/wD/AP+gvaeTAAAZtUlE\nQVR4nO2deVgURxbAq+fivg8F0WHklCNIwimggIgxAiogQiQYUWMWQRKjIgJRMRsSXcX4bQwo6nJI\nMCbRyGZRFEYXUW5MQAREISiXIhDOGWZ6Zv+oL/MNwzXT0wOzOL+/6O6qem8er6urq+u9QrhcLpAh\n4y8Is62ADOlC5hAyxiBzCBljkDmEjDHIHELGGGQOIWMMMoeQMQaZQ8gYg8whZIxB5hAyxiBzCBlj\nkDmEjDHIHELGGEizrYCMqeByucnJyeXl5WpqahcvXhwdHeWdl6BIGVLLqVOnCARCd3c3l8v99ttv\nAQCffvqpRCXKHhlSTV5eHpfLVVFRAQAEBgYCAB48eCBRiTKHkGqWLVvG5XJ//fVXAEBvby8AYNWq\nVZIViWNvw2az6XR6dHQ0lUpta2tbvnz5woULX79+jaOINw0Oh3Pu3DkNDY29e/euX78+KSmJzWZL\nVCKeg0o2m02hUFJTUxkMRkZGRkJCQk5ODoVCwVHEmwaKorW1tSUlJaampjMjEeHiPV41NTV98uTJ\n69evNTU18W35DSQxMTE9Pf3gwYMLFixQVVXV0tKi0WiSvcdw73PMzMwk0eybSX5+vq6uLv//S0ND\nIysrS3ISZYNKqaarqys2Nhb+q1AUff78+TfffBMdHS05ibKJKeklMTHx0KFDPT098JBAIBgYGCxb\ntszIyEhyQvHvIZhMJgCAzWbj3vKbxr179wAAycnJDAYDAMDlcsvLy2NjYzMzMyUoFcfHz+DgYGJi\nImx29+7dVVVVODb+BtLZ2RkREUGj0TQ0NFxdXf39/VNSUphMpkSF4v+WIQMvmpqazp07d+fOnefP\nnzMYDB0dHRqNtnnz5oCAAEVFRQkJlTmENMJgMGJjY//5z38aGBj4+/ubmZnBDuPhw4c3b97U0NA4\nffp0QECARGRLtP+RgYHu7m47Ozt1dfXz58+zWCyBq3/++eeOHTsAAAcPHpSEdJlDSBfDw8O2trY0\nGu3p06dTFDt79iyCIF9//TXuCuDpED09PceOHXNxcdHX19fQ0DAzM1u7du2VK1ckPQ6aS0RGRqqr\nqz979mzaksePHyeRSCUlJfgqgNsYIj09/dNPP6VQKIGBgW+99RaHw+ns7Lx37x6dTreysrp8+bK5\nuTkuguYwFRUVjo6O6enpoaGh0xbmcrlr1qxpbW2tqakhEom4KYGLWyUkJCAIkpCQMDQ0JHDp8ePH\ndnZ2ysrKZWVluMiaw6xcudLV1ZXD4QhZvqmpiUgk4juTjYNDnDlzhkAgZGZmTlaAyWT6+PjMmzev\npaVFfHFzld9++w0AcPPmTZFqbd682crKCkc1xHWI+vp6BQWFI0eOTF1saGjI1tZ29erVYoqbw0RH\nR5ubmwvfPUDu378PnzV4qSGuQ/j6+tra2o5/OxpPaWkpgUC4cuWKmBLnJCiKLliw4PPPPxe1IofD\nWbx48WeffYaXJmI5RHV1NYIg//73v4UsHxIS8vbbb4sjca5SXV0NAKisrMRQ97PPPrO0tMRLE7Ec\nIjIy0tzcXPjyJSUlAICioiJxhM5JkpOTtbS0UBQVteLAwEB2djaCIBUVFU1NTRUVFRUVFeKM1bA7\nBIfD0dXV/fLLL0WqZWVltXv3bsxC5ypbtmx59913hS+/Z8+eKd4ctbS0MGuC/fN3bW3ty5cv33vv\nPZFq+fn55ebmYhY6V2lsbIQrzYRk4cKFCIJMeIlEIi1fvhyzJtgdori4WE1NzcrKSqRa3t7ezc3N\nLS0tmOXOSRobG01MTIQvHxYWRiJNvLgJRdGgoCDMmmB3iLt377q6uoo6R2Zvb08kEisqKjDLnXv0\n9PS8fv1apHXVmpqafn5+ZDJ5/CUSieTj44NZGexL6CoqKsLCwoQpWV9fn5yczDtUUVE5ffo0zyeU\nlZU/+eQTZWVlzJr8v/PixQsAwKJFi0SqtW3btp9++kngJJFI9PLyEsuY2IYeHA5HXl4+IyNDmML5\n+flQVzKZTCaTSSSS3F/Afu/333/HpsbcAEbntba2ilQLRdH58+cL/DcJBML58+fFUQbjI6Onp4fB\nYOjr6wtT2NPTU0NDA0VRFovFYrHYbDbzL1AUtbCwsLa2xqbG3AAumVRQUBCpFoFACA8PF4jRQBBk\n3bp14iiD0SHa29sBAEI6BJFIDAgImDC8hEgkhoeHY9NhzjAyMgIAkJeXF7Xihx9+yGKxeIcEAsHF\nxUVLS0scZTA6RGdnJwBgfJc1GUFBQbzcBvxwuVxhPvXObWAPgcEhTExMHB0deeN6BEE2btwopjIY\nHQL+d+Xk5IQs7+Hhoa6uLnCSRCJ5eXnNmzcPmw5zBjiQ4r/XhWfHjh3cv1a0cDicDRs2iKsMtmrQ\nKzkcjrBiSCR/f/+srCz+foLD4Xz44YfYFJhLwCDY3t5egWHEwMDAs2fP+vr6ent7WSyWkpKShoaG\nlpbW4sWLeZMQmzZtioyMHBkZQRDE1tZ2wYIFYiqD0SEIBAIAAEVR4asEBQVduHCB/4yiouL69eux\nKTCX0NDQAAD09vZqaWmVlpYWFhYWFxfX19fD19HxUCgUY2Nja2vrFStWeHh4BAQE/PDDD1wuF2YU\nEZMZ6iEAAJ6enqqqqv39/fCQQqGEhIRgeHDOPVRVVQEAe/bsKS4uHhoaMjMz8/Dw8PX1NTY2ptFo\nCgoKampqAAA2mz0wMNDb29vU1NTU1FRdXR0fH9/T06Onpwf7XfEHEABgnYe4e/cuAKCzs1OkWlu3\nbuWfXJN99hwZGTlz5gyVSgUAWFtbf/fddyLNRrDZ7LKysgMHDsD709vb++7du2KqhNEhGhsbAQCi\nBuv95z//4XnDokWLRF0dNJdAUTQtLU1fX19JSWnPnj1iLi68cePGsWPHVq9eDQBYsWKFOEGUGB1i\neHgYAHD9+nWRao2OjsL8WWQy+fDhw9hEzwEqKiocHBzIZPK+fftghjm8KC8vd3d3JxKJf/vb33p7\nezG0gHEMoaCgoKWlBUc9g4OD9+7du3fvXl1d3aNHj169esUrRiQSDQ0NLS0tbWxs3N3dbWxs1q1b\nl52dzWaz33//fWyi/6/hcrmnTp06cOCAvb19VVXVhN+KRbInHN3zsLOzKywszMjI2Ldv382bNy9f\nvmxnZyeShtjjMmxsbIyNjUdGRm7dusVms2k0mq2traWlpYGBAa8Mi8VqbGysra2tqqrq6+vT0tJa\ntmxZbm6us7MzXB36RjE0NBQaGnr9+vWEhISEhASBD8Wjo6PXr1+/cOGCSPYMCQnZunXr22+/LSCr\nvb39/ffff/DgwenTp3fu3CmClhh6lb6+vq+++kpdXZ1IJPr6+mZnZ7e1tU1dBUXRhw8fHjt2zNLS\nEgBgYmLyyy+/vFFjiO7ubkdHR01NzVu3bglcgvbU09MjkUii2hP2MS4uLuPtyWKx9u/fDwBISEgQ\nXk/RHILD4aSnp+vo6KioqMTExHR0dIhUHVJYWOjj44MgiIuLS01NDYYW/u/o6upasmQJlUqtq6vj\nP4+LPR88eDCFPVNTU0kkUkREhJCtieAQHR0dq1atIhKJu3btEn8oVFpa6uTkRCaTv/jiCwyLS/+P\n6O/vf+edd0xMTNrb2/nPz5g9r169SiKRhOwnhHWIwsLCefPmLVmypLq6WmRlJ4HD4aSkpCgoKKxc\nufLVq1d4NStVsFgsLy+v+fPnC0Rzz7A9z507hyBIamrqtI0I5RCXL1+mUCgffPDB+NBN8ampqTEx\nMTEzM5uTgX7x8fHy8vICkVWzYs+4uDg5Oblppyimd4iMjAwCgbB3717JjQE7OzttbW0NDAzmmE/c\nvn2bQCAI3JezZU82m+3p6WliYtLf3z9F3WkcIjc3l0wmHzhwAB9NJ6evr8/GxsbU1PTly5eSljUz\nDA0NGRoaBgUF8Z+cXXt2dHTo6OhMHRczlUM0NDQoKyuHh4fPzPthe3u7oaGhh4fH3Bhj7t27V0dH\nhz/3uzTYMzs7m0AgTJFmZFKHYDAYtra2dnZ2M5n/paKiQk5O7ujRozMmUUI0NTVRKJSUlBTeGSmx\nJ4fDcXd3d3Nzm6zKpA5x6NAhZWXlpqYmnHWcjm+++YZMJtfW1s6wXHzZunWrpaUlf08gPfaEIdqT\nJaKY2CEaGhrk5OT+8Y9/SETHKUFR1N7e3s3NTRL9KofDOXHiRHBw8M6dO/kX/eIrpbW1lUKhpKWl\n8c5Imz29vLw8PDwmLD+xLTZt2mRhYTE6OioRHaejtLQUQZBffvkF95ZnZgurzz//XE9Pj//RIG32\nhJEyjx49Gl94AoeoqalBEGR2M3v4+/svXboU905i9erVCILAf1VXVxcAwMnJCV8RKIpSqdT9+/fz\nzkihPTkcjpGRUUxMzPiSEzhEVFSUsbGxpLfymRqYSaK4uBjfZo8cOQIA+Pnnn7lcbn19vagffoSh\nuLgYAMA//yid9oyLi6NSqeNvOUGHYDAYmpqaSUlJEtdxOmxsbOAacxyZgS2s4uPjjYyMeIdSa8/K\nykoAwPjBu6BD5OXlIQjyxx9/SFzB6fjqq6+0tbXxnZNgsVjR0dENDQ04timAk5PTzp07eYdSa08O\nh6OtrX3q1CmBYoKBOgUFBZaWlqJGIvMP18+fP79x48a4uLjt27dnZ2djawcA8N5773V3dz98+BBz\nC+P58ssvc3Nzi4qKbty4cf/+/YaGhgnjyTAzPDxcWVm5YsUK3hkx7QkAaGtru3DhQlBQkLOzszi6\nCdgTfi4vKioSLCfgIA4ODrt27cLshkeOHKFSqT09PVwut6enh0qljvdBIUFRVFtbOzk5GbMy48G2\nhRXMN56dnT3ttyiY44C/BxLTnhC4qQ7MiY+Z8fZMTEw0MTERKAYE6igoKFy8eBGbyJaWFhKJxJ91\n6osvvlBUVMT8sd/b23vr1q3Y6k5IZmYmzyJwC6uMjIxpMzKVl5dD75GXlw8JCcnNzZ3sBTIrK4tM\nJvOSNIppT37EdwjuOHtevnyZSCQyGAz+MmMeGS9evBgZGcG8ReSlS5fYbPbKlSt5Zzw9PYeHh9PS\n0rA1aGZm1tDQgK3ueBITEz/44IMtW7bAQwxbWDEYjB9//NHPz09FRWXjxo25ubkCAZlNTU2Ghoa8\nODsx7Yk7AvY0NTVFUVQgvdMYh3j+/DkAAMaNYADuEcW/KHThwoUAAJi0FwOLFi2CKuECLltYwbuf\nyWRev37dz89PW1s7LCzs9u3b8Cbu7e3V0dHhFRbTnrgjYE9tbW0AAG+TN8gYhxgYGAAAwNAJDMCk\nETBSEQLDWJubm7E1qKamxgv9E5/MzMyIiIisrCx9fX03N7fAwMCqqqqsrCxsdzAcjfb391+5cmXV\nqlULFiyIjo5++vQpfzofMe2JOwL2hIpBJXmMicsYGhoCACgpKWGTB2MU+dPlwb8xj+SVlJQGBwcn\ny78nDrC3+Pnnnz/++GMxm4L9TUdHx+nTpwEADg4OvEti2hN3lJSUoEq8QwDA4OAgf5kxDgHzPTCZ\nTGx7fJmbmxcVFfX19fESicAN7YVMNDMeJpMpJyf3r3/9C1t1vHj69GlsbOwUBeTk5JhMpqmpqZKS\nEgzM5Z0HYtgTd6A9eYcTJioZ4xCwDxkcHMT2AywsLAAA7e3tPIeADxFXV1cMrQEABgYG1NTU8Alq\nFoOKiooJHQK+UBgZGe3YsSM4OJhKpUZFRfEPmMS0J+4MDAzAXpx3CP7q13mMGUPAARFMF4SBwMBA\nAoFQWFjIO0On08lkMuaovY6ODoFpA2kAfjc3MDA4ePBgbW1tU1NTTEwMHDny5zsAYtsTdwTs2dfX\nB6Z2CGNjYxKJBL/6YMDAwCA2NjY1NRUapb+/PzU1NT4+Hr5rYKC+vl6khL8ShUwmIwiirKwcHByc\nl5fX3Nx8+PBhGIjGY/HixXAJDDwU05484INfpGwcEyJgz6amJgRBaDQaf5kxjwwKhUKj0R49eoRZ\n5NGjR2k02q5duxYtWtTY2BgTE7N9+3bMrdXV1QUHB2Oujhc6OjqqqqoeHh6hoaFr166dIn+gmZnZ\n0NBQe3s7TO0jvj0BAHQ6PSsrCwDQ0tJy8uRJT0/PpUuXYmtKwJ6NjY16enqCL0ECk1nbt293cXER\nc0YMF+DLakFBwWwrIgJwjUV+fj7vjDTbMzw83NPTU6CY4Mctd3f38vJygXfTWYFOp8vLy4v5RWeG\n0dXVNTMzo9PpvDPSbE86ne7m5iZQTNAhfH19iUTilStXJK7gdGRnZ69Zs0bU/K6zjqenJ/+wWmrt\n2dzc3Nzc7OHhIVhufN+yfv16Ly8vyfZf09HR0UEikXJycmZXDQz88MMPJBKpq6uLd0Y67fntt98q\nKSmNjIwIlJzAIXJzcxEEwTEIFQMxMTE6OjrDw8OzqAM2RkZG1NXVT548yTsjnfZ0cHAICwsbX3IC\nh+BwODY2NgEBARJUcEpevXqloqIiDcvOsLFlyxZ7e3veoRTa88mTJwiC5OXljS888TL8q1evIghC\np9MlpOLUfPTRR/PmzZs6JlWagTkb+ZMuSps9IyIiFi1aNOHmmpPGqKxdu9bS0lJg9cQMUFJSgiCI\nhYVFZGTkmTNnCgoKps2vIyRsNptOp0dHR1Op1La2tuXLly9cuJA/9hJH3N3dBd7oZtGeBAKBf1VY\nS0sLmUzmDzPkZ1KHaG5uVlVVjYqKwl/Hyenr6zMyMoJzZwiC8NJyKSoqWltbh4WFJSUlXb16tb6+\nHkPQC4PBKC4uht9ykpKSbt26tW3btoGBAUn8kLy8PAAAfxrRWbSnwH5/H3/8sZ6e3vjhJGSqKLbv\nv/8eQZAZG+qjKLphw4b58+d3dHSEhoaO380LQRA4fwwAIBKJVCrVz8/vyZMnIkmBe51JqGPgx8fH\nRyBaa7bsyZ9w+MGDB1Nv1D5NWGNkZKScnFxhYSFuak5OVFQUT9bo6Oi777472cZz/C7y22+/iSQF\nTuZL5heMAcZzCiwSni17QthstrOzs6ur6xQhcdOYBkXRTZs2qaqq3rlzBzdNx8HhcGJiYohEIszq\nDmEymZ6enlP4BJlMDg0NFVXWzDgEm81OTU1VU1Mjk8kPHz7knZ9Fe3K53EOHDsnLy0+d+W960zCZ\nzODgYAUFhatXr4qr6USMjo7u2LGDTCZfunRJ4FJ/f7+Njc1kPkEikTCkIJoBh6DT6XCjmy1btjg5\nOZmamvKP8GfLnrdu3SIQCGfOnJm6ulCmQVF09+7dCILs3bsX3xDm5uZmJycnVVXVGzduTFjg1atX\nxsbG4zeoJJPJISEhGCQaGhqCv9bK4s6dO3dgPLG/vz+MrW5ra9PV1V29ejW/3WbennV1dZqamhs3\nbpy2BRHulZycHDU1NWtra1zep0dHR48fP66qqmpvbz91Go3W1laY5ZXfISgUCoIg3t7e/J8Wp2Zw\ncDAxMRFW3717tzgp4wVAUfTatWvOzs4Igqxdu7a0tJT/allZmbKycmhoqMCTe8bs2dbWRqVSly1b\nJkzSO9E6z5aWFrhr7Lp16wRS7QkPi8VKT083MTFRUFA4evSoMCl2amtrVVVVee8dMA1nTk6Ovb09\nAMDGxubs2bODg4PY9BGHP//8MzU11cLCgkgkBgcH8w8X+MnPz6dQKKGhoQI/dgbs2djYaGxsbGlp\nKeSLFZan6bVr19555x0AgKenZ0ZGhvD/iebm5iNHjtBoNDgeFOmNsbS0VEFBASZ/19TU5M0f/Pe/\n/w0MDKRQKGpqalFRURMmwcAdDodDp9PDwsIUFRWVlJQ++uijaX9Lfn6+srKyl5fX+F0LJGfP+/fv\n6+jo2NnZCZ/bD/vwqqCgICgoCG7Q6+Lisn///u+///7333/v6emBIcYjIyNdXV1FRUXfffddeHg4\nDH/Q19c/cOAAtnyU165dg53E8ePHBS69fPnyxIkTcJXv0qVLk5KSnj17hvmnTQaHwykrK4uLi4PB\nXo6OjmfPnhV+ir2srExXV9fIyKiysnL8VXztyeFwTp06RaFQvL29RZp8E3e83d3dnZGRAfWbbGN4\nJSUlZ2fn2NhYmPhfHHEXL150dHScbJaNy+WWlpZGR0fDZd/29vaHDx8uKysTM6fA0NDQr7/+unPn\nThhPQKVSP/nkE2xp258/f+7m5iYnJ3fixIkJTYGLPdvb2zds2EAgEOLj40U1OPb9MsbDZDIfP37c\n3d3d19fH5XLl5ORUVFQMDQ0NDQ0lEWwzBSiKFhYW/vTTTzdu3Pjjjz90dXW9vb2dnJwcHBysrKym\nXXTT19dXU1NTVVVVWVlZVVVVX1/P5XIdHBx8fX19fHzeeustcXRjs9mJiYlff/21paVlSkoKf2CP\nABjsiaJoSkpKXFycmppaWlraqlWrRFUPT4eQTh4/fpyXl0en0ysqKuCKeD09PRqNpqKiwr8Cncvl\n9vX19fT0NDc3w/gibW1tu79wdnbGNyDgxYsXBw8ezMzMdHFxiYmJ8fX1FbPB4eHhc+fOnTx5sre3\n9+jRoxEREePf1YVh7jsEPy9evKirq2toaHjy5Mng4KBAFJuGhga8BWk0mqWlJZyxkCgFBQV///vf\n4UTW5s2bN23ahMHtqqqqLl26lJOT09vbu23btn379omTn+TNcgjppKSkJC0t7ccffxwcHLS3t4dJ\nJJcsWaKnpzdheRaL1dzcXF1dffv27du3b7e0tJibm4eGhm7btk343dgnQ+YQ0gKDwcjLyysoKKDT\n6XV1dQAAJSWlCTdybW1tZbPZcAm1h4fHmjVrRN1pbQpkDiGN9Pb21tfXP378eMK9v83MzJYsWWJi\nYsKfjBcvZA4hYwyCcRky3nBkDiFjDP8DkXGNspjPCmQAAAAASUVORK5CYII=\n",
      "text/plain": [
       "<IPython.core.display.Image object>"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "GUGF = nx.DiGraph()\n",
    "GUGF.graph['rankdir'] = 'LR'\n",
    "GUGF.add_node(0, shape='circle')\n",
    "GUGF.add_node(1, shape='doublecircle')\n",
    "GUGF.add_edge(0, 0, label= 'r')\n",
    "GUGF.add_edge(1,0, label= 'r')\n",
    "GUGF.add_edge(0,1, label='g')\n",
    "GUGF.add_edge(1,1, label='g')\n",
    "draw(GUGF)"
   ]
  },
  {
   "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": 12,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "image/png": "iVBORw0KGgoAAAANSUhEUgAAAPUAAABzCAYAAABAWESgAAAABmJLR0QA/wD/AP+gvaeTAAAgAElE\nQVR4nO2deVhUZfvHvzMwDKAQJCAhmyAgqKlgCLjFYi6lpaWilrlW0ptLZqbZZS5papqZvln65iuo\neVX2ZrmgopQrCqa44gYoIqIsouww8/394cX8GGdAwDMzMJzPdXHp3Oec57mfme89c85znnPfEpKE\niIiI0SA1tAMiIiLCIga1iIiRIQa1iIiRIQa1iIiRIQa1iIiRIQa1iIiRIQa1iIiRIQa1iIiRIQa1\niIiRYZCg3r59Ozw9PXHnzh1DdC8i8tQ0Zg0bJKgPHDiA1NRUnD592hDdi4g8NY1ZwwYJaicnJwCA\njY2NIboXEXlqGrOGDRLUbm5uAAB3d3dDdC8i8tQ0Zg0bJKjd3d0hl8vRunVrlY0kVq5ciZEjR+K9\n996DXC6HRCJR/YmINCaqa1ihUOCvv/7CtGnT4O7ujtu3b6NPnz5wdXVFXl6e/p2jAcjIyKC3t7ea\nbdWqVZRKpczJySFJrl27lgA4ffp0Q7goIlIr1TVcWlrKo0eP0tzcnAC4ZMkS7t+/nxMmTODDhw/1\n7ptBglqhUHDQoEFqtn79+lEikbCsrIwkmZ2dTQAMCgoyhIsiIrWiTcNeXl4EwNzcXAN59QiDnH5L\npVIEBQWp2UJCQkASu3btAgDk5+cDAPr27at3/0REnoQ2DUulj8Lp2WefNYRLKkwN1XG/fv3UXn/2\n2WdwcnLChAkTcOzYMVy7dg1LlizBzJkzDeShiEjtPK7hxoLBgjogIEDttUKhwPnz55GQkABvb28D\neSUiUnce13BjwSCn3zExMXB1dUVqaqrKtnjxYvz55584fPgwYmNjcezYMVy+fBnl5eWGcFFEpFa0\nabisrAwAUFlZaSi3ABgoqMvLy1FZWYmKigqVLTg4GIWFhZg4cSIGDBiAHj16oH379nB0dMSWLVsM\n4aaISI1U13BRUREWLlyI9PR0AMCMGTMMutJMQjaObKKbN29GTk4Opk2bBgBQKpW4ffs24uPjMX36\ndOTk5BjYQxGRpoHBrqmrs2DBAsybN0/tRr1UKoWzszNCQkLg6elpQO9ERJoWjeLRyyNHjgAAvv76\na5SWlgJ4tMIsMTERs2fPRkxMjCHdExFpUjSK0+/s7GwsWLAAe/bswf3799GhQwc4ODjgpZdewrhx\n42BmZmZoF0VEmgx6P/1WKBSIj4/HoUOH8M8//+Dy5csoLCxEWVkZLCws4OLiArlcDhcXF7Ru3RqF\nhYUGv5kvIlLFk/RrZ2cHe3t7dOzYES+++CJ69+6td/3q7Zc6Ozsby5cvR0xMDO7duwdfX1906dIF\nvr6+sLa2hrm5OSoqKpCfn4/8/HwcP34cJ0+eBEkMGTIEn376Kbp27aoPV0VENGhS+tX1OtTKykp+\n8cUXbNGiBZ2dnbls2TKmp6fX6dj8/Hxu3bqVXbt2pUQi4RtvvMG8vDwdeywi8v80Rf3qNKizs7PZ\np08fmpub88svv2RJSUmD29q1axfd3NzYtm1bJiUlCeiliIh2mqp+dRbUd+/eZceOHent7c2zZ88K\n0mZeXh5fffVVWlpa8siRI4K0KSKijaasX50EdXFxMf39/enj48PMzExB21YqlRw1ahRtbW0Fe7NF\nRKrT1PWrk6AeM2YM7ezs6nztUV/KysrYt29furu7G+QhdBHjpqnrV/Cg3r17NwEwNjZW6KbVuHv3\nLu3s7Dh16lSd9iPSvDAG/Qoa1BUVFfT19eWwYcOEbLZGYmJiKJVKeerUKb30J2LcGIt+BQ3qrVu3\n0tTUlNevXxey2Vrp1q0bR44cqbf+RIwXY9GvoEEdEBDAyMhIIZt8IjExMZTJZLx586Ze+xUxPoxF\nv4I90JGSkoJTp04hKipKqCbrxPDhw2Fra4vo6Gi99itiXBiTfgUL6t9++w2Ojo7o0aOHUE3WCTMz\nMwwYMAB79uzRa78ixoUx6VewoD5w4AD69++vyqioT/r3748TJ06oMpCKiNQXY9KvICNQKpVISkrS\nSJmqK4YOHapWvWPSpEmQyWRwdXWFk5MTnJ2d4ezsjMjISL34I9K0MTb9CvLoZWpqKh48eKC37Iq+\nvr7YsWMHlEolAKCwsFC1rer/UqlUTFooUieMTb+C/FJXJVzz8PAQorknMnz4cNUbUhNKpRITJ07U\niz8iTRtj068gQX3r1i20aNFCbw+Dd+7cGa6urrXuY29v32iTrYs0LoxNv4IEdX5+PmxtbYVoqs6M\nHDkSMplM6zaZTIZx48bBxMRErz6JNE2MTb+CBHVxcTEsLS2FaKrOvP7662p5w6tTUVGBt99+W6/+\niDRdjE2/ggS1QqHQ+69it27d8Nxzz2nYJRIJunTpAj8/P736I9J0MTb9ChLUlpaWKCoqEqKpOiOR\nSBAZGamRaVQqlYoTZCL1wtj0K8gtrRYtWqC4uLhex1RWViI1NRW5ubnIz89HUVERZDIZbG1tYWtr\nCw8PD7Rs2bLWNl5//XV8/fXXajapVIqRI0fWewwizRdj068gQe3o6Ijc3FyUlpbC3Nxc6z6XLl1C\nfHw8/v77b5w7dw7Xrl2r8ZqiChcXF7Rv3x49evRAWFgYunfvrvbNFhwcDHt7e9y7dw/AowmGwYMH\niymFReqFselXkBTBp06dQrdu3XD16lW0a9dOZU9JScGWLVuwefNmpKeno1WrVggNDUXXrl3h6emJ\ndu3awdbWFtbW1qprmoKCApSUlCA1NRXXrl1TvZlXrlxBy5YtMXToULz55psICwuDiYkJPvjgA/zw\nww+qG/U7d+7Eyy+//LRDEmlGGJ1+hXjU6+7duwTAffv2kSTj4+MZERFBAHRzc+Ps2bOZmJhIhULR\n4D5u3LjBtWvXskePHpRIJGzbti3XrVvHffv2EQAB0M7OjhUVFUIMSaQZYWz6Fex5aicnJ06ZMoW9\nevWiRCLhgAEDGB8fT6VSKVQXKlJTUzlt2jRaWlqyTZs2tLS0JABOnz5d8L5EmgfGpF9BgjovL48u\nLi6USCQMDw/nP//8I0SzT+Tu3bucPn06pVIpAXDbtm166VfEuDA2/T71NfWJEycwYsQIFBUVYcWK\nFRgzZkyN+yoUCiQnJ+Ovv/5CcnIyLl68iLS0NI11sPb29ujQoQP8/PzQq1cv9OzZEy1atKix3Z9/\n/hnTpk1DXl4eli1bhilTpjzNkESaEcao36cK6rVr12L69Ono1asXtmzZAkdHR637nTp1Cj/++CO2\nbduGvLw82NjYICAgAB07doSXl5fGcrmMjAxcuHABZ86cQVpaGmQymaoC5qBBg7RWwVQoFPj888+x\nePFiDBkyBNHR0XpfJSTStDBa/Tbk512pVHL27NkEwDlz5rCyslJjH4VCwd9//50hISEEwE6dOnH5\n8uVMTk6u14RDZmYmt2zZwldeeYWmpqZ0cnLismXLWFBQoHX/PXv20MbGhiEhIczNzW3I8ESMHGPX\nb72DWqlU8r333qOpqSk3bNigdZ+zZ88yODiYEomEgwYN4vHjxxvk3ONkZWXx448/ZsuWLeng4MCY\nmBit+50/f56urq708/Pj3bt3BelbxDhoDvqtd1DPmTOHpqam3LFjh8a2yspKzp8/nzKZjMHBwUxM\nTKy3Q3Xh3r17nDx5Mk1MTNi/f3/euXNHY5/MzEx6enryhRdeEKt4iKhoDvqtV1D/+9//pkQi4caN\nGzW2ZWdnMzQ0lJaWlvzhhx90civgcU6dOsX27dvT0dGRf/31l8b2q1ev0sHBgf369dN6iiXSvGgu\n+q1zUCcmJtLMzIyff/65xra0tDR6e3vTx8eHFy5cqHPnQvDw4UOOGjWKcrmcv/zyi8b2hIQEyuVy\nrX6LNB+ak37rFNQFBQX09PTkSy+9pDFJkJaWxjZt2jAgIMBg169KpZLTp0+niYkJN2/erLH922+/\npYmJidZvQxHjp7npt05BHRUVRUdHR2ZnZ6vZs7Oz6eXlxa5du/L+/ft16lCXfPzxx5TJZNy1a5fG\ntqFDh9LDw4PFxcUG8OzpOHjwIAHQysqKnTp1YmBgIAFQLpczMDCQHTp0oFwuJwDevn3b0O42Opqb\nfp8Y1MeOHaNUKtU4NaisrGSfPn3o6emp9ULfECiVSo4ZM4ZWVla8evWq2racnBza2dlx9uzZBvKu\n4ezcuZMvvvgiCwsLVTYA9PHxUb3Oyclhu3bt9FoHqinQHPX7xKAOCgpiRESEhn3evHk0Nzfn6dOn\n6+G27iktLaW/vz+7devGsrIytW1r1qyhXC7XWd1hXfHLL79w9+7darbHg5okV65cyfPnz+vTtUZP\nc9RvrUG9a9cuSiQSJicnq9nPnDlDU1NTfvvttw10XbdcvXqVLVu25MKFC9XslZWV9Pb25qRJkwzk\nWcMoKirSeHpHW1CXlJRoCKE501z1W2tQ9+7dm/3791ezKRQKBgcHMygo6KkeRdM1S5cupYWFBa9d\nu6Zm//777ymXy3nr1i0DeSYM2oK6srKS8fHxnDp1Kt3c3JiZmcnevXvTxcWFixcvVj3iRz6aPPrq\nq6/UbOSj2diFCxdy7NixDAgIYHh4OM+ePavXsQlFc9VvjUF99uxZAuCBAwfU7Nu3b6dEImn0hd7L\nysro7e3N0aNHq9lLS0vZunVrzp8/30CeCYO2oC4tLeXRo0dpbm5OAFyyZAn379/PCRMm8OHDh/Tw\n8ODjK4Or25RKJd966y1eunRJtb1v3750cHCocVljY6U567fGoJ4xYwY9PT3VbsIrlUo+//zzHDZs\nmABu656ffvqJUqmU586dU7PPnDlTY2xNDW1BXYWXlxcBaKwd9vHx0Qjq6rbDhw+rfrkf//vzzz91\nMxAd0Zz1qzWolUolnZ2dOWfOHDV71Yd+8uRJgdzWLZWVlfTw8ODUqVPV7GfOnCEAnjhxwkCePT21\nBbW24K3JXt22cuVK+vn5Ce+snmnu+tWaIvjcuXO4desWXn/9dTX7xo0b4e/vjxdeeKFhj4TpGRMT\nE4wfPx6bN29WKzbWuXNneHp6ijWtH6OwsBBpaWla0+UqFAoDeNQwmrt+tQZ1XFwc7Ozs0LVrV5VN\noVDgf//7H0aNGiWw67pl5MiRyM3NxaFDh9Ts4eHhiIuLM5BXTwcb+Ai8RCIBAJSWlqpsVWIhCT8/\nP5SUlGDp0qVqx128eBFr1qxpoLf6p7nrV2uK4MOHD6N3794qEQCPHhTPz8/HwIEDBXOYJH788UfE\nxsbC29sb2dnZCAsLE/SN9/DwgK+vL+Li4hAREaGy9+7dG//9739rTQvbWKn6JS0pKdG6vaysDMCj\n3NSmpv//Efv5+SElJQULFy7E2LFjsXfvXhQUFAAA9u7di4EDB8LLywsLFy5EZmYmwsLCcOnSJZw8\neRK//vqrjkclHPrSLwBkZmZi7969iI2NRUZGBo4fPy5o+w3Sr7Zzcg8PDy5atEjN9tVXX9HBwUHQ\nyaX58+fTzc2NeXl5JB/linJzc+OqVasE64Mk33vvPQYHB6vZLl26RACNbvHBk4iNjeXYsWNVE1iz\nZs3i0aNHSZKFhYVcsGCBatuUKVPU8m2lpaWpnkQKDAzk6dOn2bNnT7755pvcunUrS0tLefPmTb76\n6qu0tbVl69atOWnSJIOtif7iiy+4fPly3rx5s17H6Uu/VeTl5dU6x/G01Fe/GkFdXFysdVndmDFj\nOGDAAMEcTU9Pp6mpKRcvXqxmX7RoES0tLZmTkyNYXxs2bGCLFi3UPtDy8nLKZDL+9NNPgvUjIiwO\nDg4EQIlEwh49evC77757oi70pd/H0WVQ11e/GtfUVYnUvLy81OyXL1+Gj4+PYKcVW7ZsQWVlJcLD\nw9XsYWFhKC4uxoYNGwTry9vbG0VFRbh9+7bKJpPJ4ObmhmvXrgnWj4huIIljx47hgw8+gL29PYKD\ng/HNN9+oKltUR1/61Sf11a9GUOfn5wMA7Ozs1Oy3bt16YqHs+nDkyBEAgLOzs5rdxcUFAJCcnCxY\nX25ubgAeJYSrjp2dHfLy8gTrR0R3kERlZSVIIjExETNmzECbNm3w8ssvIzo6GoWFhQD0p199Ul/9\nagT1w4cPAQBWVlYa9sdtT0PVt87jxb6r6gilpaUJ1tczzzwDAHjw4IGa3crKSjVekaaDQqGAQqFA\nRUUF9u/fj3HjxqFVq1YYNmyYakZY1/rVJ/XVr8bsd9XM6uN5iouKimrNXVxfrK2tAUBthrL66+r3\n5Z6WKr+rvs2raNmyJXbs2CHoqb6IcGhLpfs4VUXqysvL8euvv6pm6XWtX31Sm361rSnQCOqq6fGy\nsjK1vMNyuVx1q0QI2rdvj8OHD+P+/ftq+ZarTp+cnJwE66vK78en/ktLSxEQEIDx48cL1peIcLzz\nzjt1+nI3MzNDeXk5bG1tERwcjN27d+tcv/qkNv3a2Nho7K8R1FWnKA8fPlR7U1q2bKnxTfE0+Pn5\nAXh0Gl49qKtOy3v27ClYXzVdUjx48AABAQEYNmyYYH2JCMe//vWvGreZmpqisrISNjY2eOuttzB8\n+HCEhITgyJEj2L17t871q09q0+/jE4KAlmvqqgOrFiVU4eDggDt37gjm6BtvvAGpVIqDBw+q2ePj\n4yGTyQRdgJKVlQXg0RiqU1BQoLoMEGn8mJiYQCKRwMLCApGRkdi/fz9ycnKwevVq9OzZE1KpVG/6\n1Sf11a9GUHt4eACAxlS5j48PUlJSBHPU2dkZs2fPxvfff6+aAHjw4AG+//57zJ07VzULLgQpKSmQ\nyWTw9PRU2ZRKJa5fv64ar0jjRCqVQiaTQSqVolevXli/fj0yMzMRExODiIgIVV3oKvSl3+pUXdc+\nXlNLKOqrX43T72eeeQaOjo64cuWK2pK69u3b47fffhPU2YULF6Jt27Z4//334erqiitXrmDWrFmY\nOHGioP1cuHABnp6eaksmb926hZKSkiZ777I54O7uDmdnZ9XpdV3mWfSpX+DRmeXmzZsBAOnp6Vi5\nciXCwsLQpUsXwfqot361rWDp06ePRsqUquLYGRkZQi6W0QtBQUF899131Wx79uwhAN67d89AXono\niuauX61PafXq1Qvx8fFqtpCQEJiZmWnYGzv3799HUlISQkND1ezx8fHw8/PTWKQg0vRp7vrVGtSh\noaG4du0abty4obK1aNEC/fr1w9atWwV2W7f88ssvkMlkGk/nHDhwAGFhYQbySkSXNHf9ag3qoKAg\nWFhYYO/evWr2yMhIHDhwAHfv3hXIZd2zbds2DBw4UO12QFZWFs6cOaP3oN6+fTs8PT0FmYXNz8/H\n2LFj0bdvX/Tp0wf79u3Ty7HVEXI8QtLs9VvTefzo0aMZEhKiZisqKqKdnZ1GmpjGSlJSEiUSiUbF\ng+XLl7NVq1Z6T6c7efJkAtDI4d0QIiMjaWFhwZKSEp4/f57u7u56ObY6Qo5HaJqzfmsM6p07d1Ii\nkTA1NVXNvmjRIlpbWzeJgu6DBw+mv7+/xjO0/v7+HD9+vN79WbhwIQHw2LFjT92WlZUVnZycSJLX\nr1+njY2NXo6tjpDjEZrmrN8ag7q8vJzOzs6cMmWKmv3+/fu0t7dnVFTUU7qsW/bv3681C2Z8fDwB\n8MiRI3r3KTo6WrB6V15eXpRIJMzOzub777/PGTNm6OXY6gg5HqFpzvqtNZl/VZmPxxOHb9q0iSYm\nJo02K2NJSQnbt2/PV199VWNbSEiI1jIs+uDQoUOUy+VUKBS1Jt6vy69I1a9kt27dOGfOHFZWVnLB\nggUcMWIER4wYwXnz5unk2JrGU4VSqeSKFSsYGRnJd999l2ZmZmqphvVJc9Vvre9yUVERHRwc+MEH\nH6jZlUol+/btSy8vLz548KABbuuWqKgo2tjY8MaNG2r21atXEwA/+eQTHjx4kBcvXtRrtcOMjAx6\ne3uTfHLi/dq4fv06X3vtNVpYWNDPz09VkFypVLJ169acO3euTo6tbTxVrFq1ilKpVJWhZO3atQTA\n6dOn17ldoSgqKuKzzz6rcY+3qer3wIEDBMC4uLhaj3/iV+ePP/5IqVSqkWP49u3bdHBw4LBhwxpV\n+ZItW7YQAH/++Wc1e2lpKVu1aqU1Ub1cLqeLiwu7d+/OESNGcOrUqVy6dCmjo6MZFxfHCxcuCFIC\nV6FQcNCgQWq2mhLv18R3331HFxcXxsbGctmyZQTA9evXkyRTU1MZEBCgUXdLiGPrOp5+/fpRIpGo\nJnGys7MJgEFBQXVuVwgSEhI4aNAgSiQSSiQSo9Bvu3bttP56P84Tg1qhUDAoKIg9e/bUGHxcXBzN\nzMw4bdq0erquG6r8eTz5OfloxtDCwoLjxo2jVCqtsRKFVCqlmZkZzczM1PYbMWKEID5+8cUXaq9r\nSryvjZiYGEqlUlVly6KiIrZu3ZqOjo58+PAhIyMjefHiRcGPrc945s+fTwD87bffSJIpKSkEwM8+\n+6zebdcXpVLJP/74gz169CAAhoaG8u+//zYq/T5eW0sbdVLTmTNnKJfLNarwkeS2bdsolUoNXvc5\nPj6eVlZWHDlypMaHl5SURLlcziVLlpAkZ82aRYlEUmNgP/4nkUi4adMmQfxMSkpSe12foPb29mab\nNm3UbBs3biQABgcHc+3atTo5tjYeH49SqeT69etpa2vLjz76iK+99hqXLFmiOs3XBUqlkrGxsezV\nqxcBMDAwkH/++adq1tjY9Psk6jxzsXr1apqYmDA+Pl5jW0xMDGUyGd99912Wl5fXtUnB2L59O83N\nzTlq1CiN/u/fv09PT0+Gh4ervVlLly6tc0C7urrqTJT1CWorKytKJBK19ctKpZLh4eEEwKVLl6rd\n/qh+Sv80x9aHiooKTp06lZcvX27Q8fUhNzeXX375parI3yuvvMLDhw9r3dfY9FsbdQ5qpVLJIUOG\n0M7OjikpKRrbd+3aRSsrKwYHB+utqHtZWRk//PBDSiQSfvjhhxqDLisrY3h4OB0dHZmVlaVx/IoV\nK574i21iYsLVq1cL4m90dDRdXFx4/fp1lc3d3Z0A6nQtO3ToUAJgQEAAT58+zeLiYsbExHDq1Kns\n0qULAXDgwIFcs2YNZ86cyY0bNwpybH3GM3/+fHp4eHDDhg3cs2cPjx49ypSUFEEX+qSnp3PmzJm0\ntbWlTCbj8OHDawzmKoxRvzVRr3sMhYWF7N69O93d3bXem7xy5Qr9/f1pbW3NFStW6PRb78CBA+zY\nsSNtbGw0cjyTjz7E0aNH09rautaypevWras1sC0sLPjdd9+xsLDwqX3esGEDn3vuOaakpDwx8b42\ncnJyOH78eDo6OtLa2pqhoaGqsRcWFjIqKopt2rSho6MjV65cqfbL+zTH1mU8Vezbt0+Vr7v6n62t\nLTdv3tyQt43ko8/z4MGDHDp0KE1MTGhvb89PP/20XnXGjVG/2qj3jcOcnBz6+vrSy8tL60V7WVkZ\n58+fT3Nzc/r4+DA6OrpeM6pPIjExkYMGDSIADh48WGv1hrKyMo4aNYpyufyJ0/8kuX79eq2BbWpq\nyi5dutDU1JTW1tacPHmyxjWkiDoxMTH8+uuvVa8VCgUzMjIYHR3NVq1a1bu9lJQUzp07V3VG4+/v\nz40bN7K0tLRB/hmjfh+nQasB7ty5Q39/fzo4ODAhIUHrPleuXOHo0aNpamrKtm3bcsGCBQ0+rSks\nLOSmTZsYGhpKAHzhhRf4xx9/aN03Ly+PoaGhtLKyqtcbsmXLFkqlUrXgNjc3Z25uLrOysrhkyRK2\na9eOAOjr68tFixYxLS2tQeMxVqpmvqvKKFXn2rVrDAwMrFM79+7d47fffsvu3bsTAB0dHTlt2jTB\nvlCNUb/VafASn4KCAoaHh1Mul3PNmjU17peens5Zs2bxueeeU5UmmTBhAtetW8fDhw8zOzubJSUl\nJB99q+fl5TE5OZlbt27lxx9/zB49etDMzIzm5uYcMWIEDx48WGNfJ0+epLu7Ox0dHet9ykI+uidf\ndV/TzMyMkydPVtuuVCp55MgRRkVF0c7OjhKJhMHBwfzyyy8bdDvI2Ojbt6/q9lXVZ6pUKnny5EkO\nGzas1smzO3fu8D//+Q8HDx5MMzMztmjRgm+++Sb37Nmjk0lKY9RvFU+1bq+iooKffPIJJRIJ33jj\nDd65c6fWfffu3ctPPvmEQUFBtLS0fOIElbe3NydMmMCYmJhaZ2MrKiq4bNkympmZ8cUXX2RmZmaD\nx7R582ZKpVJKpdJa7wmWl5dz586dHD9+vOoa0svLi1OnTuWOHTuYn5/fYB+aKnfu3GFUVBTbtm1L\nW1tb9uzZk0OHDuW6des0JsrKy8t56NAhzps3j4GBgZRKpbSwsODLL7/M6OjoJ66qEwJj1C9JSsgG\nFjuuRmxsLCZNmoSioiIsXrwY77zzDqRSrY9qqyCJ9PR0pKWlobCwEGVlZZBIJLCxsYG9vT3at28P\nuVz+xL6PHz+OyZMnIyUlBbNnz8bcuXM1ktHVlx07duD69ev48MMP67S/UqnEyZMn8ccffyAuLg7/\n/PMPAKBLly7o3bs3goKCEBQU1GTLvgjBgwcPkJiYiOPHj+Po0aM4fPgwioqK4OXlhYiICLzyyisI\nDQ2FhYWF3n0zNv0KtsK+rKyMq1atYsuWLVXlaIVYWlkT1VcOvfXWW/WaBdU1BQUF3LlzJz/66COG\nhISo1nc7OTlxyJAhXLZsGQ8dOsSioiJDu6oTFAoFz58/zw0bNnDChAns2LGjar7Cx8eHb7/9Njdt\n2lTvErW6xJj0K/hjM+np6YyKiqK5uTnbtGnDGTNmPPFWTV3JysriqlWrGBgYSAAMDw/XupigsVFW\nVsaEhAR+8803HDVqlGqxhKmpKf39/RkVFcVNmzbx9OnTek/cIASpqan8/fffOXfuXEZERNDa2lp1\nG6t///6cN28ed+/erXUCrbFhDPoV5PRbG1lZWdiwYQO2bNmCy5cvo23btoiIiEBERAS6du0Kd3d3\nyGSyWtu4ffs2Ll26hPj4eMTFxSEpKQlWVlYYNmwYJk6ciMDAQF24rhfu3o3bbBIAAAIJSURBVL2L\nEydOICEhAQkJCUhKSsKDBw8gk8nQvn17dOrUCc8//zw6d+6MTp06oU2bNoZ2GQ8fPsS5c+dw7tw5\nJCcn4+zZszh37pzK7w4dOqguNbp37w4fHx+NWmlNhaasX50FdXUSExOxZ88exMfHIyEhAaWlpTA1\nNYWrqytsbW1hbW2tuo4oKChASUkJUlNTUVxcDIlEAj8/P4SFhSE8PBz9+vXTqClkDJBEamoqzpw5\ng+TkZCQnJ+PMmTO4efMmAKBVq1bo2LEjXF1d4ebmBldXV7i6usLFxQXu7u5qJWYaSmVlJTIzM3Hz\n5k3cuHEDN2/exM2bN5GRkYGUlBSkpaWBJJ555hl07twZXbp0Uf3boUOHOl1DNkWamn71EtTVKS8v\nx5UrV5CSkoLLly8jJycH9+/fR1FREWQyGWxtbWFrawsPDw/4+vrCx8dHo9xtcyI/Px+nT59GcnIy\nLl26pAqy9PR0FBcXq/azs7ODk5MTWrVqhWeffVb1VxNFRUXIzc1FXl4e8vLykJWVhaysLCgUCgCP\nipo7OTmpvjQ8PT1VAdy2bVudj7ux0hT0q/egFhGO3NxcZGRkqIL8zp07qiDNzc3F/fv3azzW0tJS\nLfhbt24NFxcXVRA7Ojo+/SysiEEQg1pExMio/WaciIhIk0MMahERI0MMahERI8MUwCeGdkJEREQ4\n/g93TIkfmk3R9wAAAABJRU5ErkJggg==\n",
      "text/plain": [
       "<IPython.core.display.Image object>"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "GX = nx.DiGraph()\n",
    "GX.graph['rankdir'] = 'LR'\n",
    "GX.add_node(0, shape='doublecircle')\n",
    "GX.add_node(1, shape='doublecircle')\n",
    "GX.add_edge(0, 0, label= '!g')\n",
    "GX.add_edge(1,0, label= '!r && !g')\n",
    "GX.add_edge(0,1, label='True')\n",
    "GX.add_edge(1,1, label='!r')\n",
    "draw(GX)"
   ]
  },
  {
   "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": 14,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "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)\"}]\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": 15,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div class=\"alert alert-success\">\n",
       "        <strong>Tests passed!!</strong>\n",
       "        </div>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "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": 18,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "activities = [{\"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": {
    "collapsed": true
   },
   "source": [
    "Run `check_elevator_always(activities)` to check your answer"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div class=\"alert alert-success\">\n",
       "        <strong>Tests passed!!</strong>\n",
       "        </div>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "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": 20,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "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\": 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": "code",
   "execution_count": 21,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div class=\"alert alert-success\">\n",
       "        <strong>Tests passed!!</strong>\n",
       "        </div>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "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": 24,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "activities = [{\"duration\": 12.0, \"time_start\": 0.0, \"id\": 0, \"activity\": \"(move-down-slow slow1-0 n7 n6)\"}, {\"duration\": 1.0, \"time_start\": 0.0, \"id\": 1, \"activity\": \"(board p0 fast0 n2 n0 n1)\"}, {\"duration\": 11.0, \"time_start\": 0.0, \"id\": 2, \"activity\": \"(move-down-fast fast1 n2 n0)\"}, {\"duration\": 12.0, \"time_start\": 0.0, \"id\": 3, \"activity\": \"(move-up-slow slow0-0 n0 n1)\"}, {\"duration\": 15.0, \"time_start\": 1.001, \"id\": 4, \"activity\": \"(move-up-fast fast0 n2 n8)\"}, {\"duration\": 1.0, \"time_start\": 11.001, \"id\": 5, \"activity\": \"(board p6 fast1 n0 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 12.001, \"id\": 6, \"activity\": \"(board p5 slow1-0 n6 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 12.001, \"id\": 7, \"activity\": \"(board p2 slow0-0 n1 n0 n1)\"}, {\"duration\": 15.0, \"time_start\": 12.002, \"id\": 8, \"activity\": \"(move-up-fast fast1 n0 n6)\"}, {\"duration\": 12.0, \"time_start\": 13.002, \"id\": 9, \"activity\": \"(move-down-slow slow1-0 n6 n5)\"}, {\"duration\": 12.0, \"time_start\": 13.002, \"id\": 10, \"activity\": \"(move-down-slow slow0-0 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 16.002, \"id\": 11, \"activity\": \"(leave p0 fast0 n8 n1 n0)\"}, {\"duration\": 11.0, \"time_start\": 17.003, \"id\": 12, \"activity\": \"(move-down-fast fast0 n8 n6)\"}, {\"duration\": 1.0, \"time_start\": 25.003, \"id\": 13, \"activity\": \"(leave p5 slow1-0 n5 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 25.003, \"id\": 14, \"activity\": \"(leave p2 slow0-0 n0 n1 n0)\"}, {\"duration\": 0.001, \"time_start\": 26.003, \"id\": 15, \"activity\": \"(collect-goal-passenger-at p0 n8)\"}, {\"duration\": 1.0, \"time_start\": 26.004, \"id\": 16, \"activity\": \"(recharge slow1-0)\"}, {\"duration\": 0.001, \"time_start\": 26.004, \"id\": 17, \"activity\": \"(collect-goal-passenger-at p5 n5)\"}, {\"duration\": 1.0, \"time_start\": 26.004, \"id\": 18, \"activity\": \"(recharge slow0-0)\"}, {\"duration\": 1.0, \"time_start\": 27.003, \"id\": 19, \"activity\": \"(leave p6 fast1 n6 n1 n0)\"}, {\"duration\": 12.0, \"time_start\": 27.005, \"id\": 20, \"activity\": \"(move-up-slow slow1-0 n5 n6)\"}, {\"duration\": 12.0, \"time_start\": 27.005, \"id\": 21, \"activity\": \"(move-up-slow slow0-0 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 28.004, \"id\": 22, \"activity\": \"(recharge fast0)\"}, {\"duration\": 1.0, \"time_start\": 28.004, \"id\": 23, \"activity\": \"(recharge fast1)\"}, {\"duration\": 15.0, \"time_start\": 29.005, \"id\": 24, \"activity\": \"(move-down-fast fast0 n6 n0)\"}, {\"duration\": 1.0, \"time_start\": 29.005, \"id\": 25, \"activity\": \"(board p4 fast1 n6 n0 n1)\"}, {\"duration\": 15.0, \"time_start\": 30.006, \"id\": 26, \"activity\": \"(move-down-fast fast1 n6 n0)\"}, {\"duration\": 1.0, \"time_start\": 39.006, \"id\": 27, \"activity\": \"(board p6 slow1-0 n6 n0 n1)\"}, {\"duration\": 12.0, \"time_start\": 39.006, \"id\": 28, \"activity\": \"(move-down-slow slow0-0 n1 n0)\"}, {\"duration\": 12.0, \"time_start\": 40.007, \"id\": 29, \"activity\": \"(move-down-slow slow1-0 n6 n5)\"}, {\"duration\": 1.0, \"time_start\": 44.006, \"id\": 30, \"activity\": \"(board p2 fast0 n0 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 45.007, \"id\": 31, \"activity\": \"(leave p4 fast1 n0 n1 n0)\"}, {\"duration\": 15.0, \"time_start\": 45.007, \"id\": 32, \"activity\": \"(move-up-fast fast0 n0 n6)\"}, {\"duration\": 15.0, \"time_start\": 46.008, \"id\": 33, \"activity\": \"(move-up-fast fast1 n0 n6)\"}, {\"duration\": 28.0, \"time_start\": 51.007, \"id\": 34, \"activity\": \"(move-up-slow slow0-0 n0 n3)\"}, {\"duration\": 1.0, \"time_start\": 52.008, \"id\": 35, \"activity\": \"(leave p6 slow1-0 n5 n1 n0)\"}, {\"duration\": 0.001, \"time_start\": 53.009, \"id\": 36, \"activity\": \"(collect-goal-passenger-at p6 n5)\"}, {\"duration\": 1.0, \"time_start\": 53.009, \"id\": 37, \"activity\": \"(recharge slow1-0)\"}, {\"duration\": 0.001, \"time_start\": 53.01, \"id\": 38, \"activity\": \"(collect-goal-passenger-at p4 n0)\"}, {\"duration\": 12.0, \"time_start\": 54.01, \"id\": 39, \"activity\": \"(move-up-slow slow1-0 n5 n6)\"}, {\"duration\": 1.0, \"time_start\": 60.008, \"id\": 40, \"activity\": \"(leave p2 fast0 n6 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 61.009, \"id\": 41, \"activity\": \"(recharge fast0)\"}, {\"duration\": 1.0, \"time_start\": 61.009, \"id\": 42, \"activity\": \"(recharge fast1)\"}, {\"duration\": 15.0, \"time_start\": 62.01, \"id\": 43, \"activity\": \"(move-down-fast fast1 n6 n0)\"}, {\"duration\": 1.0, \"time_start\": 66.011, \"id\": 44, \"activity\": \"(board p1 slow1-0 n6 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 67.012, \"id\": 45, \"activity\": \"(leave p1 slow1-0 n6 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 68.013, \"id\": 46, \"activity\": \"(board p2 slow1-0 n6 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 68.013, \"id\": 47, \"activity\": \"(board p1 fast0 n6 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 69.014, \"id\": 48, \"activity\": \"(recharge slow1-0)\"}, {\"duration\": 15.0, \"time_start\": 69.014, \"id\": 49, \"activity\": \"(move-down-fast fast0 n6 n0)\"}, {\"duration\": 12.0, \"time_start\": 70.015, \"id\": 50, \"activity\": \"(move-up-slow slow1-0 n6 n7)\"}, {\"duration\": 1.0, \"time_start\": 79.008, \"id\": 51, \"activity\": \"(board p3 slow0-0 n3 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 80.009, \"id\": 52, \"activity\": \"(recharge slow0-0)\"}, {\"duration\": 20.0, \"time_start\": 81.01, \"id\": 53, \"activity\": \"(move-down-slow slow0-0 n3 n1)\"}, {\"duration\": 1.0, \"time_start\": 82.016, \"id\": 54, \"activity\": \"(leave p2 slow1-0 n7 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 84.015, \"id\": 55, \"activity\": \"(leave p1 fast0 n0 n1 n0)\"}, {\"duration\": 12.0, \"time_start\": 101.011, \"id\": 56, \"activity\": \"(move-down-slow slow0-0 n1 n0)\"}, {\"duration\": 1.0, \"time_start\": 113.012, \"id\": 57, \"activity\": \"(leave p3 slow0-0 n0 n1 n0)\"}, {\"duration\": 0.001, \"time_start\": 114.012, \"id\": 58, \"activity\": \"(collect-goal-passenger-at p2 n7)\"}, {\"duration\": 0.001, \"time_start\": 114.013, \"id\": 59, \"activity\": \"(collect-goal-passenger-at p3 n0)\"}, {\"duration\": 1.0, \"time_start\": 114.013, \"id\": 60, \"activity\": \"(board p1 slow0-0 n0 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 115.014, \"id\": 61, \"activity\": \"(recharge slow0-0)\"}, {\"duration\": 12.0, \"time_start\": 116.015, \"id\": 62, \"activity\": \"(move-up-slow slow0-0 n0 n1)\"}, {\"duration\": 1.0, \"time_start\": 128.016, \"id\": 63, \"activity\": \"(leave p1 slow0-0 n1 n1 n0)\"}, {\"duration\": 0.001, \"time_start\": 129.017, \"id\": 64, \"activity\": \"(collect-goal-passenger-at p1 n1)\"}]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/html": [
       "<div class=\"alert alert-success\">\n",
       "        <strong>Tests passed!!</strong>\n",
       "        </div>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "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
}
