From 3c5928d216025dc6d8a8e48e89e1cfa8c6c5f432 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 5 Nov 2021 12:15:40 +0100
Subject: [PATCH] tl: fix AST rendering of Star/FStar nodes

* spot/tl/dot.cc: Show the min/max argument for Star/FStar nodes.
* tests/python/formulas.ipynb: Adjust test.
---
 spot/tl/dot.cc              |  22 +++-
 tests/python/formulas.ipynb | 253 +++++++++++++++++++-----------------
 2 files changed, 155 insertions(+), 120 deletions(-)

diff --git a/spot/tl/dot.cc b/spot/tl/dot.cc
index a67de5fab..2bfbb43da 100644
--- a/spot/tl/dot.cc
+++ b/spot/tl/dot.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009-2015, 2018-2019 Laboratoire de Recherche et
+// Copyright (C) 2009-2015, 2018-2019, 2021 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -42,7 +42,7 @@ namespace spot
         {
           os_ << "digraph G {\n";
           rec(f);
-          os_ << "  subgraph atoms {\n     rank=sink;\n"
+          os_ << "  subgraph atoms {\n     rank=sink\n"
               << sinks_->str() << "  }\n}\n";
         }
 
@@ -61,9 +61,23 @@ namespace spot
         op o = f.kind();
         std::string str = (o == op::ap) ? f.ap_name() : f.kindstr();
 
+        if (o == op::Star || o == op::FStar)
+          {
+            unsigned min = f.min();
+            unsigned max = f.max();
+            if (min != 0 || max != formula::unbounded())
+              {
+                str += "\n" + std::to_string(min);
+                if (max != min)
+                  str += "..";
+                if (max != formula::unbounded())
+                  str += std::to_string(max);
+              }
+          }
+
         if (o == op::ap || f.is_constant())
-          *sinks_ << "    " << src << " [label=\""
-                  << str << "\", shape=box];\n";
+          *sinks_ << "    " << src
+                  << " [label=\"" << str << "\", shape=box];\n";
         else
           os_ << "  " << src << " [label=\"" << str << "\"];\n";
 
diff --git a/tests/python/formulas.ipynb b/tests/python/formulas.ipynb
index de64bbc09..95241be9d 100644
--- a/tests/python/formulas.ipynb
+++ b/tests/python/formulas.ipynb
@@ -57,10 +57,10 @@
     {
      "data": {
       "text/latex": [
-       "$\\{a \\mathbin{\\mathsf{;}} \\mathsf{first\\_match}(b^{\\star} \\mathbin{\\mathsf{;}} c^+ \\mathbin{\\mathsf{;}} d)\\}\\mathrel{\\Diamond\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} (c \\land \\mathsf{G} \\mathsf{F} b)$"
+       "$\\{a \\mathbin{\\mathsf{;}} \\mathsf{first\\_match}(\\{b^{\\star} \\mathbin{\\mathsf{;}} c^+\\}^{\\mathsf{:}\\star3..5} \\mathbin{\\mathsf{;}} b)\\}\\mathrel{\\Diamond\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} (c \\land \\mathsf{G} \\mathsf{F} b)$"
       ],
       "text/plain": [
-       "spot.formula(\"{a;first_match(b[*];c[+];d)}<>-> (c & GFb)\")"
+       "spot.formula(\"{a;first_match({b[*];c[+]}[:*3..5];b)}<>-> (c & GFb)\")"
       ]
      },
      "execution_count": 3,
@@ -69,7 +69,7 @@
     }
    ],
    "source": [
-    "g = spot.formula('{a;first_match(b*;c[+];d)}<>->(GFb & c)'); g"
+    "g = spot.formula('{a;first_match((b*;c[+])[:*3..5];b)}<>->(GFb & c)'); g"
    ]
   },
   {
@@ -497,7 +497,7 @@
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "{a;first_match(b[*];c[+];d)}<>-> (c & GFb)\n"
+      "{a;first_match({b[*];c[+]}[:*3..5];b)}<>-> (c & GFb)\n"
      ]
     },
     {
@@ -509,42 +509,42 @@
        "<!-- Generated by graphviz version 2.43.0 (0)\n",
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
-       "<svg width=\"371pt\" height=\"404pt\"\n",
-       " viewBox=\"0.00 0.00 371.00 404.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 400)\">\n",
+       "<svg width=\"343pt\" height=\"583pt\"\n",
+       " viewBox=\"0.00 0.00 343.00 583.48\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 579.48)\">\n",
        "<title>G</title>\n",
-       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-400 367,-400 367,4 -4,4\"/>\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-579.48 339,-579.48 339,4 -4,4\"/>\n",
        "<!-- 0 -->\n",
        "<g id=\"node1\" class=\"node\">\n",
        "<title>0</title>\n",
-       "<ellipse fill=\"none\" stroke=\"black\" cx=\"161\" cy=\"-378\" rx=\"40.89\" ry=\"18\"/>\n",
-       "<text text-anchor=\"middle\" x=\"161\" y=\"-374.3\" font-family=\"Times,serif\" font-size=\"14.00\">EConcat</text>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"171\" cy=\"-557.48\" rx=\"50.09\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"171\" y=\"-553.78\" font-family=\"Times,serif\" font-size=\"14.00\">EConcat</text>\n",
        "</g>\n",
        "<!-- 1 -->\n",
        "<g id=\"node2\" class=\"node\">\n",
        "<title>1</title>\n",
-       "<ellipse fill=\"none\" stroke=\"black\" cx=\"129\" cy=\"-306\" rx=\"36\" ry=\"18\"/>\n",
-       "<text text-anchor=\"middle\" x=\"129\" y=\"-302.3\" font-family=\"Times,serif\" font-size=\"14.00\">Concat</text>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"125\" cy=\"-485.48\" rx=\"42.79\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"125\" y=\"-481.78\" font-family=\"Times,serif\" font-size=\"14.00\">Concat</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;1 -->\n",
-       "<g id=\"edge9\" class=\"edge\">\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
        "<title>0&#45;&gt;1</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M153.25,-360.05C149.56,-351.97 145.06,-342.12 140.94,-333.11\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"144.02,-331.43 136.67,-323.79 137.65,-334.34 144.02,-331.43\"/>\n",
-       "<text text-anchor=\"middle\" x=\"148.75\" y=\"-348.85\" font-family=\"Times,serif\" font-size=\"14.00\">L</text>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M160.1,-539.89C154.54,-531.44 147.67,-520.97 141.48,-511.56\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"144.24,-509.39 135.82,-502.95 138.39,-513.23 144.24,-509.39\"/>\n",
+       "<text text-anchor=\"middle\" x=\"155.1\" y=\"-528.69\" font-family=\"Times,serif\" font-size=\"14.00\">L</text>\n",
        "</g>\n",
-       "<!-- 10 -->\n",
-       "<g id=\"node11\" class=\"node\">\n",
-       "<title>10</title>\n",
-       "<ellipse fill=\"none\" stroke=\"black\" cx=\"225\" cy=\"-234\" rx=\"27\" ry=\"18\"/>\n",
-       "<text text-anchor=\"middle\" x=\"225\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\">And</text>\n",
+       "<!-- 11 -->\n",
+       "<g id=\"node12\" class=\"node\">\n",
+       "<title>11</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"224\" cy=\"-260.61\" rx=\"28.7\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"224\" y=\"-256.91\" font-family=\"Times,serif\" font-size=\"14.00\">And</text>\n",
        "</g>\n",
-       "<!-- 0&#45;&gt;10 -->\n",
-       "<g id=\"edge14\" class=\"edge\">\n",
-       "<title>0&#45;&gt;10</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M168.59,-360.15C179.67,-335.57 200.36,-289.68 213.36,-260.82\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"216.7,-261.94 217.61,-251.39 210.31,-259.07 216.7,-261.94\"/>\n",
-       "<text text-anchor=\"middle\" x=\"163.59\" y=\"-348.95\" font-family=\"Times,serif\" font-size=\"14.00\">R</text>\n",
+       "<!-- 0&#45;&gt;11 -->\n",
+       "<g id=\"edge16\" class=\"edge\">\n",
+       "<title>0&#45;&gt;11</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M175.09,-539.16C180.7,-515.09 190.88,-470.13 198,-431.48 207.22,-381.44 215.7,-322.68 220.33,-289.03\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"223.81,-289.41 221.69,-279.03 216.87,-288.47 223.81,-289.41\"/>\n",
+       "<text text-anchor=\"middle\" x=\"169.59\" y=\"-527.96\" font-family=\"Times,serif\" font-size=\"14.00\">R</text>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node3\" class=\"node\">\n",
@@ -555,133 +555,154 @@
        "<!-- 1&#45;&gt;2 -->\n",
        "<g id=\"edge1\" class=\"edge\">\n",
        "<title>1&#45;&gt;2</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M107.33,-291.42C94.15,-281.99 78.14,-268.23 69,-252 31.37,-185.16 26.28,-91.96 26.29,-46.34\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"29.79,-46.1 26.38,-36.07 22.79,-46.04 29.79,-46.1\"/>\n",
-       "<text text-anchor=\"middle\" x=\"103.83\" y=\"-280.22\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M98.53,-471.16C82.85,-462.01 63.81,-448.44 52,-431.48 28.52,-397.76 27,-383.57 27,-342.48 27,-342.48 27,-342.48 27,-178.74 27,-132.35 27,-78.38 27,-46.54\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"30.5,-46.26 27,-36.26 23.5,-46.26 30.5,-46.26\"/>\n",
+       "<text text-anchor=\"middle\" x=\"93.53\" y=\"-459.96\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 3 -->\n",
        "<g id=\"node4\" class=\"node\">\n",
        "<title>3</title>\n",
-       "<ellipse fill=\"none\" stroke=\"black\" cx=\"129\" cy=\"-234\" rx=\"51.19\" ry=\"18\"/>\n",
-       "<text text-anchor=\"middle\" x=\"129\" y=\"-230.3\" font-family=\"Times,serif\" font-size=\"14.00\">first_match</text>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"125\" cy=\"-413.48\" rx=\"63.89\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"125\" y=\"-409.78\" font-family=\"Times,serif\" font-size=\"14.00\">first_match</text>\n",
        "</g>\n",
        "<!-- 1&#45;&gt;3 -->\n",
-       "<g id=\"edge8\" class=\"edge\">\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
        "<title>1&#45;&gt;3</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M129,-287.7C129,-279.98 129,-270.71 129,-262.11\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"132.5,-262.1 129,-252.1 125.5,-262.1 132.5,-262.1\"/>\n",
-       "<text text-anchor=\"middle\" x=\"125.5\" y=\"-276.5\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M125,-467.18C125,-459.46 125,-450.19 125,-441.59\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"128.5,-441.58 125,-431.58 121.5,-441.58 128.5,-441.58\"/>\n",
+       "<text text-anchor=\"middle\" x=\"120\" y=\"-455.98\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 4 -->\n",
        "<g id=\"node5\" class=\"node\">\n",
        "<title>4</title>\n",
-       "<ellipse fill=\"none\" stroke=\"black\" cx=\"137\" cy=\"-162\" rx=\"36\" ry=\"18\"/>\n",
-       "<text text-anchor=\"middle\" x=\"137\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\">Concat</text>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"125\" cy=\"-341.48\" rx=\"42.79\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"125\" y=\"-337.78\" font-family=\"Times,serif\" font-size=\"14.00\">Concat</text>\n",
        "</g>\n",
        "<!-- 3&#45;&gt;4 -->\n",
-       "<g id=\"edge7\" class=\"edge\">\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
        "<title>3&#45;&gt;4</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M130.98,-215.7C131.86,-207.98 132.92,-198.71 133.9,-190.11\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"137.39,-190.44 135.05,-180.1 130.43,-189.64 137.39,-190.44\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M125,-395.18C125,-387.46 125,-378.19 125,-369.59\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"128.5,-369.58 125,-359.58 121.5,-369.58 128.5,-369.58\"/>\n",
        "</g>\n",
        "<!-- 5 -->\n",
        "<g id=\"node6\" class=\"node\">\n",
        "<title>5</title>\n",
-       "<ellipse fill=\"none\" stroke=\"black\" cx=\"264\" cy=\"-90\" rx=\"27\" ry=\"18\"/>\n",
-       "<text text-anchor=\"middle\" x=\"264\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">Star</text>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"135\" cy=\"-260.61\" rx=\"40.11\" ry=\"26.74\"/>\n",
+       "<text text-anchor=\"middle\" x=\"135\" y=\"-264.41\" font-family=\"Times,serif\" font-size=\"14.00\">FStar</text>\n",
+       "<text text-anchor=\"middle\" x=\"135\" y=\"-249.41\" font-family=\"Times,serif\" font-size=\"14.00\">3..5</text>\n",
        "</g>\n",
        "<!-- 4&#45;&gt;5 -->\n",
-       "<g id=\"edge3\" class=\"edge\">\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
        "<title>4&#45;&gt;5</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M160.29,-148.16C181.31,-136.57 212.32,-119.48 234.95,-107.01\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"236.72,-110.03 243.78,-102.14 233.34,-103.9 236.72,-110.03\"/>\n",
-       "<text text-anchor=\"middle\" x=\"156.79\" y=\"-136.96\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
-       "</g>\n",
-       "<!-- 7 -->\n",
-       "<g id=\"node8\" class=\"node\">\n",
-       "<title>7</title>\n",
-       "<ellipse fill=\"none\" stroke=\"black\" cx=\"154\" cy=\"-90\" rx=\"27\" ry=\"18\"/>\n",
-       "<text text-anchor=\"middle\" x=\"154\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">Star</text>\n",
-       "</g>\n",
-       "<!-- 4&#45;&gt;7 -->\n",
-       "<g id=\"edge5\" class=\"edge\">\n",
-       "<title>4&#45;&gt;7</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M141.12,-144.05C143.01,-136.26 145.3,-126.82 147.42,-118.08\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"150.85,-118.82 149.8,-108.28 144.04,-117.17 150.85,-118.82\"/>\n",
-       "<text text-anchor=\"middle\" x=\"137.62\" y=\"-132.85\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
-       "</g>\n",
-       "<!-- 9 -->\n",
-       "<g id=\"node10\" class=\"node\">\n",
-       "<title>9</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"126,-36 72,-36 72,0 126,0 126,-36\"/>\n",
-       "<text text-anchor=\"middle\" x=\"99\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">d</text>\n",
-       "</g>\n",
-       "<!-- 4&#45;&gt;9 -->\n",
-       "<g id=\"edge6\" class=\"edge\">\n",
-       "<title>4&#45;&gt;9</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M130.25,-144C126.32,-133.7 121.48,-120.22 118,-108 112.2,-87.61 107.26,-64.15 103.87,-46.44\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"107.24,-45.42 101.97,-36.23 100.36,-46.7 107.24,-45.42\"/>\n",
-       "<text text-anchor=\"middle\" x=\"126.75\" y=\"-132.8\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
-       "</g>\n",
-       "<!-- 6 -->\n",
-       "<g id=\"node7\" class=\"node\">\n",
-       "<title>6</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"299,-36 245,-36 245,0 299,0 299,-36\"/>\n",
-       "<text text-anchor=\"middle\" x=\"272\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
-       "</g>\n",
-       "<!-- 5&#45;&gt;6 -->\n",
-       "<g id=\"edge2\" class=\"edge\">\n",
-       "<title>5&#45;&gt;6</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M265.98,-71.7C266.86,-63.98 267.92,-54.71 268.9,-46.11\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"272.39,-46.44 270.05,-36.1 265.43,-45.64 272.39,-46.44\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M127.17,-323.37C128.13,-315.8 129.3,-306.59 130.43,-297.62\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"133.91,-298.05 131.69,-287.69 126.96,-297.17 133.91,-298.05\"/>\n",
+       "<text text-anchor=\"middle\" x=\"122.17\" y=\"-312.17\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- 8 -->\n",
        "<g id=\"node9\" class=\"node\">\n",
        "<title>8</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"213,-36 159,-36 159,0 213,0 213,-36\"/>\n",
-       "<text text-anchor=\"middle\" x=\"186\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">c</text>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"151,-36 97,-36 97,0 151,0 151,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"124\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;8 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>4&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M109.04,-324.36C100.47,-314.57 90.72,-301.32 86,-287.48 79.41,-268.12 80.24,-83.21 84,-72 87.35,-62 93.42,-52.38 99.83,-44.14\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"102.56,-46.33 106.27,-36.4 97.18,-41.85 102.56,-46.33\"/>\n",
+       "<text text-anchor=\"middle\" x=\"104.04\" y=\"-313.16\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"136\" cy=\"-179.74\" rx=\"42.79\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"136\" y=\"-176.04\" font-family=\"Times,serif\" font-size=\"14.00\">Concat</text>\n",
+       "</g>\n",
+       "<!-- 5&#45;&gt;6 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>5&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M135.33,-233.35C135.44,-225.25 135.55,-216.31 135.65,-208.13\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"139.15,-208 135.78,-197.96 132.16,-207.91 139.15,-208\"/>\n",
+       "</g>\n",
+       "<!-- 7 -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>7</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"124\" cy=\"-98.87\" rx=\"30.59\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"124\" y=\"-95.17\" font-family=\"Times,serif\" font-size=\"14.00\">Star</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;7 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>6&#45;&gt;7</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M133.4,-161.63C131.86,-151.5 129.87,-138.44 128.12,-126.94\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"131.56,-126.31 126.6,-116.95 124.64,-127.36 131.56,-126.31\"/>\n",
+       "<text text-anchor=\"middle\" x=\"128.4\" y=\"-150.43\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 9 -->\n",
+       "<g id=\"node10\" class=\"node\">\n",
+       "<title>9</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"278\" cy=\"-98.87\" rx=\"33.47\" ry=\"26.74\"/>\n",
+       "<text text-anchor=\"middle\" x=\"278\" y=\"-102.67\" font-family=\"Times,serif\" font-size=\"14.00\">Star</text>\n",
+       "<text text-anchor=\"middle\" x=\"278\" y=\"-87.67\" font-family=\"Times,serif\" font-size=\"14.00\">1..</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;9 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>6&#45;&gt;9</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M162.15,-165.47C182.47,-155.01 211.27,-139.89 236,-125.74 238.51,-124.3 241.09,-122.8 243.67,-121.26\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"245.63,-124.17 252.39,-116.01 242.02,-118.17 245.63,-124.17\"/>\n",
+       "<text text-anchor=\"middle\" x=\"157.15\" y=\"-154.27\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- 7&#45;&gt;8 -->\n",
-       "<g id=\"edge4\" class=\"edge\">\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
        "<title>7&#45;&gt;8</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M161.58,-72.41C165.22,-64.45 169.67,-54.72 173.77,-45.76\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"177.05,-47 178.02,-36.45 170.68,-44.09 177.05,-47\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M124,-80.76C124,-70.73 124,-57.84 124,-46.42\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"127.5,-46.08 124,-36.08 120.5,-46.08 127.5,-46.08\"/>\n",
        "</g>\n",
-       "<!-- 10&#45;&gt;8 -->\n",
-       "<g id=\"edge10\" class=\"edge\">\n",
-       "<title>10&#45;&gt;8</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M221.87,-215.85C215.11,-178.75 199.09,-90.81 190.94,-46.1\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"194.38,-45.44 189.14,-36.23 187.49,-46.7 194.38,-45.44\"/>\n",
+       "<!-- 10 -->\n",
+       "<g id=\"node11\" class=\"node\">\n",
+       "<title>10</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"335,-36 281,-36 281,0 335,0 335,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"308\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">c</text>\n",
        "</g>\n",
-       "<!-- 11 -->\n",
-       "<g id=\"node12\" class=\"node\">\n",
-       "<title>11</title>\n",
-       "<ellipse fill=\"none\" stroke=\"black\" cx=\"300\" cy=\"-162\" rx=\"27\" ry=\"18\"/>\n",
-       "<text text-anchor=\"middle\" x=\"300\" y=\"-158.3\" font-family=\"Times,serif\" font-size=\"14.00\">G</text>\n",
+       "<!-- 9&#45;&gt;10 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>9&#45;&gt;10</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M287.49,-72.92C290.78,-64.26 294.49,-54.52 297.83,-45.73\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"301.13,-46.9 301.42,-36.31 294.59,-44.41 301.13,-46.9\"/>\n",
        "</g>\n",
-       "<!-- 10&#45;&gt;11 -->\n",
-       "<g id=\"edge13\" class=\"edge\">\n",
-       "<title>10&#45;&gt;11</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M240.18,-218.83C250.85,-208.87 265.32,-195.37 277.35,-184.14\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"279.92,-186.53 284.85,-177.14 275.15,-181.41 279.92,-186.53\"/>\n",
+       "<!-- 11&#45;&gt;10 -->\n",
+       "<g id=\"edge12\" class=\"edge\">\n",
+       "<title>11&#45;&gt;10</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M239.43,-244.94C262.27,-222.05 304.07,-175.29 320,-125.74 328.47,-99.38 323.08,-67.69 317.06,-45.72\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"320.4,-44.67 314.2,-36.07 313.68,-46.65 320.4,-44.67\"/>\n",
        "</g>\n",
        "<!-- 12 -->\n",
        "<g id=\"node13\" class=\"node\">\n",
        "<title>12</title>\n",
-       "<ellipse fill=\"none\" stroke=\"black\" cx=\"336\" cy=\"-90\" rx=\"27\" ry=\"18\"/>\n",
-       "<text text-anchor=\"middle\" x=\"336\" y=\"-86.3\" font-family=\"Times,serif\" font-size=\"14.00\">F</text>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"224\" cy=\"-179.74\" rx=\"27\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"224\" y=\"-176.04\" font-family=\"Times,serif\" font-size=\"14.00\">G</text>\n",
        "</g>\n",
        "<!-- 11&#45;&gt;12 -->\n",
-       "<g id=\"edge12\" class=\"edge\">\n",
+       "<g id=\"edge15\" class=\"edge\">\n",
        "<title>11&#45;&gt;12</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M308.35,-144.76C312.71,-136.28 318.15,-125.71 323.04,-116.2\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"326.23,-117.64 327.7,-107.15 320.01,-114.44 326.23,-117.64\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M224,-242.5C224,-232.47 224,-219.58 224,-208.16\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"227.5,-207.82 224,-197.82 220.5,-207.82 227.5,-207.82\"/>\n",
        "</g>\n",
-       "<!-- 12&#45;&gt;6 -->\n",
-       "<g id=\"edge11\" class=\"edge\">\n",
-       "<title>12&#45;&gt;6</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M322.43,-74.15C314.3,-65.26 303.76,-53.74 294.43,-43.53\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"296.91,-41.06 287.58,-36.04 291.74,-45.78 296.91,-41.06\"/>\n",
+       "<!-- 13 -->\n",
+       "<g id=\"node14\" class=\"node\">\n",
+       "<title>13</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"200\" cy=\"-98.87\" rx=\"27\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"200\" y=\"-95.17\" font-family=\"Times,serif\" font-size=\"14.00\">F</text>\n",
+       "</g>\n",
+       "<!-- 12&#45;&gt;13 -->\n",
+       "<g id=\"edge14\" class=\"edge\">\n",
+       "<title>12&#45;&gt;13</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M218.91,-162.01C215.76,-151.66 211.65,-138.14 208.06,-126.36\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"211.34,-125.12 205.08,-116.57 204.65,-127.16 211.34,-125.12\"/>\n",
+       "</g>\n",
+       "<!-- 13&#45;&gt;8 -->\n",
+       "<g id=\"edge13\" class=\"edge\">\n",
+       "<title>13&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M186.06,-83.4C175.31,-72.25 160.21,-56.57 147.59,-43.48\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"149.96,-40.89 140.5,-36.12 144.92,-45.75 149.96,-40.89\"/>\n",
        "</g>\n",
        "</g>\n",
        "</svg>\n"
@@ -973,7 +994,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.7.5"
+   "version": "3.9.2"
   }
  },
  "nbformat": 4,