From 2c267dd89442c9d9886ccccc0f9631c9c43e3b55 Mon Sep 17 00:00:00 2001
From: philipp <philipp@lrde.epita.fr>
Date: Tue, 10 Aug 2021 23:58:26 +0200
Subject: [PATCH] Adding dot suppport for aiger class

* spot/twaalgos/aiger.cc: Useless assert
* spot/twaalgos/dot.hh,
spot/twaalgos/dot.cc: aig to dot
* python/spot/__init__.py: Adapting
* tests/python/games.ipynb: Additional tests
---
 python/spot/__init__.py  |  53 ++++++
 spot/twaalgos/aiger.cc   |   2 -
 spot/twaalgos/dot.cc     | 197 ++++++++++++++++++++++
 spot/twaalgos/dot.hh     |   5 +
 tests/python/games.ipynb | 343 +++++++++++++++++++++++++++++++++++++--
 5 files changed, 583 insertions(+), 17 deletions(-)

diff --git a/python/spot/__init__.py b/python/spot/__init__.py
index 25ca26138..9ce1701c1 100644
--- a/python/spot/__init__.py
+++ b/python/spot/__init__.py
@@ -136,6 +136,28 @@ def __om_init_new(self, str=None):
 
 option_map.__init__ = __om_init_new
 
+@_extend(aig)
+class aig:
+    def _repr_svg_(self, opt=None):
+        ostr = ostringstream()
+        print_dot(ostr, self, opt)
+        return _ostream_to_svg(ostr)
+
+    def show(self, opt=None):
+        from spot.jupyter import SVG
+        return SVG(self._repr_svg_(opt))
+
+    def to_str(self, format='circuit', opt=None):
+        format = format.lower()
+        if format == 'circuit':
+            ostr = ostringstream()
+            print_aiger(ostr, self)
+            return ostr.str()
+        if format == 'dot':
+            ostr = ostringstream()
+            print_dot(ostr, self, opt)
+            return ostr.str()
+        raise ValueError("unknown string format: " + format)
 
 __twa__acc1 = twa.acc
 __twa__acc2 = twa.get_acceptance
@@ -683,6 +705,37 @@ def automaton(filename, **kwargs):
     except StopIteration:
         raise RuntimeError("Failed to read automaton from {}".format(filename))
 
+def aiger_circuits(*sources, bdd_dict = None):
+    """Read aiger circuits from a list of sources.
+
+    Parameters
+    ----------
+    *sources : list of str
+        These sources can be either commands (end with `|`),
+        textual representations of the circuit in restricted aag format
+        (start with aag and contain '\n'), or filenames (else).
+    bdd_dict : If not supplied, a fresh bdd_dict will be created, common for
+        all of the circuits.
+    """
+
+    bdd_dict = bdd_dict if bdd_dict is not None else make_bdd_dict()
+
+    for source in sources:
+        if (source.startswith("aag") and '\n' in source):
+            yield aig.parse_aag(source, "<string>", bdd_dict)
+        else:
+            yield aig.parse_aag(source, bdd_dict)
+
+def aiger_circuit(source, bdd_dict = None):
+    """Read a single aiger circuit from file or textual representation.
+
+    See `spot.aiger_circuits` for a list of supported formats."""
+    try:
+        return next(aiger_circuits(source, bdd_dict = bdd_dict))
+    except StopIteration:
+        raise RuntimeError("Failed to read an aiger circuit "
+                           "from {}".format(source))
+
 
 def _postproc_translate_options(obj, default_type, *args):
     type_name_ = None
diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc
index 78ca35f58..17cfbc5da 100644
--- a/spot/twaalgos/aiger.cc
+++ b/spot/twaalgos/aiger.cc
@@ -1086,8 +1086,6 @@ namespace spot
     std::function<bdd(unsigned)> get_gate_bdd;
     get_gate_bdd = [&](unsigned g)->bdd
       {
-        assert(v2g(circ.gate_var(g) == g));
-
         unsigned v = circ.gate_var(g);
         auto it = var2bdd.find(v);
         if (it != var2bdd.end())
diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc
index 2fb9d7772..5eed4f65c 100644
--- a/spot/twaalgos/dot.cc
+++ b/spot/twaalgos/dot.cc
@@ -1065,5 +1065,202 @@ namespace spot
     return os;
   }
 
+  namespace
+  {
+    class dotty_aig final
+    {
+      public:
+      bool vertical = true;
+      bool latex = false;
+      std::ostream& os_;
+
+      void
+      parse_opts(const char *options)
+      {
+        while (char c = *options++)
+          switch (c)
+          {
+          case 'h':
+          {
+            vertical = false;
+            break;
+          }
+          case 'v':
+          {
+            vertical = true;
+            break;
+          }
+          default:
+            throw std::runtime_error("unknown option for print_dot(): "s + c);
+          }
+      }
+
+      dotty_aig(std::ostream &os, const char *options)
+          : os_(os)
+      {
+        parse_opts(options ? options : "");
+      }
+
+      void print(const aig_ptr &circuit)
+      {
+        if (!circuit)
+          return;
+        auto is_input = [nb_in = circuit->num_inputs()](unsigned val)
+        {
+          return (val & ~1) <= (2 * nb_in);
+        };
+
+        const auto& in_names = circuit->input_names();
+        const auto& out_names = circuit->output_names();
+
+        auto num_latches = circuit->num_latches();
+        auto latches = circuit->next_latches();
+        auto num_inputs = circuit->num_inputs();
+        auto num_outputs = circuit->num_outputs();
+        auto outputs = circuit->outputs();
+        auto num_gates = circuit->num_gates();
+        auto gates = circuit->gates();
+
+        // If a circuit doesn't use an input, we need a special placement
+        bool uses_in = false;
+
+        auto add_edge = [](std::ostream &stream, const unsigned src,
+                           const unsigned dst) {
+          auto src_gate = src & ~1;
+          stream << src_gate;
+          stream << " -> " << dst;
+          if (src & 1)
+            stream << " [arrowhead=dot]";
+          stream << '\n';
+        };
+
+        if (vertical)
+          os_ << "digraph \"\" {\nrankdir = BT;\n";
+        else
+          os_ << "digraph \"\" {\nrankdir = LR;\n";
+
+        os_ << "# latches left\n";
+        for (unsigned i = 0; i < num_latches; ++i)
+        {
+          auto first = circuit->latch_var(i);
+          auto first_m_mod = first & ~1;
+          os_ << "node[shape=box, label=\"L" << i << "_out\"] "
+              << first_m_mod << ";\n";
+        }
+
+        //Predefine all nodes
+
+        os_ << "# input nodes\n";
+        for (unsigned i = 0; i < num_inputs; ++i)
+          os_ << "node [shape=triangle, label=\""
+              << in_names[i] << "\"] "
+              << circuit->input_var(i) << ";\n";
+
+        os_ << "# latch nodes\n";
+        for (unsigned i = 0; i < num_latches; ++i)
+          os_ << "node[shape=box, label=\"L" << i << "\"] L" << i << ";\n";
+
+        os_ << "# gate nodes\n";
+        for (unsigned i = 0; i < num_gates; ++i)
+          if ((gates[i].first != 0) && (gates[i].second != 0))
+          {
+            uses_in |= is_input(gates[i].first) | is_input(gates[i].second);
+            auto gate_var = circuit->gate_var(i);
+            os_ << "node [shape=circle, label=\"" << gate_var
+                << "\"] " << gate_var << ";\n";
+          }
+
+        os_ << "# and ins\n";
+        for (unsigned i = 0; i < num_gates; ++i)
+          if ((gates[i].first != 0) && (gates[i].second != 0))
+          {
+            auto gate_var = circuit->gate_var(i);
+            add_edge(os_, gates[i].first, gate_var);
+            add_edge(os_, gates[i].second, gate_var);
+          }
+
+        bool has_alone_gate = false;
+
+        os_ << "# Latches\n";
+        for (unsigned i = 0; i < num_latches; ++i)
+        {
+          auto second = latches[i];
+          os_ << "node[shape=box, label=\"L" << i << "_in\"] L" << i << ";\n";
+          if (second <= 1 && !has_alone_gate)
+          {
+            os_ << "node[shape=box, label=\"Const\"] 0" << std::endl;
+            has_alone_gate = true;
+          }
+          os_ << (second & ~1) << " -> L" << i;
+          if (i & 1)
+            os_ << "[arrowhead=dot]";
+          os_ << '\n';
+        }
+
+        // Outs can be defined after everything else
+        os_ << "# Outs\n";
+        const char* out_pos = vertical ? ":s" : ":w";
+        for (unsigned i = 0; i < num_outputs; ++i)
+        {
+          os_ << "node [shape=triangle, orientation=180, label=\""
+             << out_names[i] << "\"] o" << i
+             << out_names[i] << ";\n";
+          auto z = outputs[i];
+          uses_in |= is_input(z);
+          if (z <= 1 && !has_alone_gate)
+          {
+            os_ << "node[shape=box, label=\"Const\"] 0" << std::endl;
+            has_alone_gate = true;
+          }
+          os_ << (z & ~1) << "->" << 'o' << i << out_names[i] << out_pos;
+          if (outputs[i] & 1)
+            os_ << " [arrowhead=dot]";
+          os_ << '\n';
+        }
+
+        if (has_alone_gate || num_inputs > 0)
+        {
+          os_ << (uses_in ? "{rank = source; " : "{rank = same; ");
+          for (unsigned i = 0; i < num_inputs; ++i)
+            os_ << circuit->input_var(i) << "; ";
+          if (has_alone_gate)
+            os_ << "0; ";
+          os_ << "}\n";
+        }
+        if (num_outputs > 0)
+        {
+          os_ << "{rank = sink; ";
+          for (unsigned i = 0; i < num_outputs; ++i)
+            os_ << 'o' << i << out_names[i] << "; ";
+          os_ << "}\n";
+        }
+        if (num_latches > 0)
+        {
+          os_ << "{rank = same; ";
+          for (unsigned i = 0; i < num_latches; ++i)
+            os_ << 'L' << i << "; ";
+          os_ << "}\n{rank = same; ";
+          for (unsigned i = 0; i < num_latches; ++i)
+          {
+            auto first = circuit->latch_var(i);
+            auto first_m_mod = first & ~1;
+            os_ << first_m_mod << "; ";
+          }
+          os_ << "}\n";
+        }
+        os_ << "}\n";
+      }
+    };
+  }
+
+  std::ostream &
+  print_dot(std::ostream &os, aig_ptr circuit, const char* options)
+  {
+    dotty_aig d(os, options);
+    if (!circuit)
+      return os;
+    d.print(circuit);
+    return os;
+  }
 
 }
diff --git a/spot/twaalgos/dot.hh b/spot/twaalgos/dot.hh
index 0fdea7ff7..1ef8c3e27 100644
--- a/spot/twaalgos/dot.hh
+++ b/spot/twaalgos/dot.hh
@@ -25,6 +25,7 @@
 #include <iosfwd>
 #include <spot/twa/fwd.hh>
 #include <spot/misc/common.hh>
+#include <spot/twaalgos/aiger.hh>
 
 namespace spot
 {
@@ -44,4 +45,8 @@ namespace spot
   print_dot(std::ostream& os,
                   const const_twa_ptr& g,
                   const char* options = nullptr);
+
+
+  SPOT_API std::ostream &
+  print_dot(std::ostream &os, aig_ptr circuit, const char * = nullptr);
 }
diff --git a/tests/python/games.ipynb b/tests/python/games.ipynb
index 1030da908..de78d9ce9 100644
--- a/tests/python/games.ipynb
+++ b/tests/python/games.ipynb
@@ -769,7 +769,7 @@
        "<text text-anchor=\"start\" x=\"189.96\" y=\"-158.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;4 -->\n",
-       "<g id=\"edge6\" class=\"edge\">\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
        "<title>2&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M167.95,-196.4C181.93,-193.79 201.45,-190.14 216.79,-187.27\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"223.94,-185.94 217.64,-190.32 220.5,-186.58 217.06,-187.22 217.06,-187.22 217.06,-187.22 220.5,-186.58 216.48,-184.13 223.94,-185.94 223.94,-185.94\"/>\n",
@@ -783,7 +783,7 @@
        "<text text-anchor=\"middle\" x=\"427.92\" y=\"-137.06\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;5 -->\n",
-       "<g id=\"edge7\" class=\"edge\">\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
        "<title>2&#45;&gt;5</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M160.75,-208.85C168.39,-214.75 179.16,-222.01 189.96,-225.76 275.06,-255.28 319.26,-296.01 391.92,-242.76 413.34,-227.05 401.22,-210.86 409.92,-185.76 412.38,-178.66 415.21,-170.99 417.85,-164.03\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"420.4,-157.35 420.84,-165.01 419.15,-160.62 417.9,-163.89 417.9,-163.89 417.9,-163.89 419.15,-160.62 414.96,-162.76 420.4,-157.35 420.4,-157.35\"/>\n",
@@ -833,7 +833,7 @@
        "<text text-anchor=\"start\" x=\"277.96\" y=\"-198.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;6 -->\n",
-       "<g id=\"edge12\" class=\"edge\">\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
        "<title>5&#45;&gt;6</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M442.18,-129.03C460.14,-113.14 492.15,-84.82 511.36,-67.81\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"516.89,-62.92 513.73,-69.92 514.27,-65.24 511.65,-67.56 511.65,-67.56 511.65,-67.56 514.27,-65.24 509.56,-65.2 516.89,-62.92 516.89,-62.92\"/>\n",
@@ -841,7 +841,7 @@
        "<text text-anchor=\"start\" x=\"463.92\" y=\"-110.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;7 -->\n",
-       "<g id=\"edge11\" class=\"edge\">\n",
+       "<g id=\"edge12\" class=\"edge\">\n",
        "<title>5&#45;&gt;7</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M409.86,-142.24C399.69,-142.52 386.71,-141.81 375.92,-137.76 366.67,-134.29 357.82,-127.88 350.82,-121.79\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"345.4,-116.81 352.69,-119.22 347.98,-119.18 350.56,-121.55 350.56,-121.55 350.56,-121.55 347.98,-119.18 348.43,-123.87 345.4,-116.81 345.4,-116.81\"/>\n",
@@ -865,7 +865,7 @@
        "<text text-anchor=\"start\" x=\"375.92\" y=\"-107.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
        "</g>\n",
        "<!-- 8&#45;&gt;4 -->\n",
-       "<g id=\"edge15\" class=\"edge\">\n",
+       "<g id=\"edge16\" class=\"edge\">\n",
        "<title>8&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M327.6,-192.49C320.95,-181.1 309.32,-164.86 293.96,-157.76 282.73,-152.57 270.27,-158.46 260.47,-165.83\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"255.04,-170.26 258.47,-163.39 257.75,-168.04 260.47,-165.83 260.47,-165.83 260.47,-165.83 257.75,-168.04 262.46,-168.27 255.04,-170.26 255.04,-170.26\"/>\n",
@@ -879,7 +879,7 @@
        "<text text-anchor=\"middle\" x=\"427.92\" y=\"-209.06\" font-family=\"Lato\" font-size=\"14.00\">9</text>\n",
        "</g>\n",
        "<!-- 8&#45;&gt;9 -->\n",
-       "<g id=\"edge16\" class=\"edge\">\n",
+       "<g id=\"edge15\" class=\"edge\">\n",
        "<title>8&#45;&gt;9</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M356.13,-206.53C369.86,-207.74 388.1,-209.35 402.62,-210.62\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"409.84,-211.26 402.59,-213.78 406.35,-210.95 402.86,-210.64 402.86,-210.64 402.86,-210.64 406.35,-210.95 403.14,-207.51 409.84,-211.26 409.84,-211.26\"/>\n",
@@ -912,7 +912,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa3979355d0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc7c65c660> >"
       ]
      },
      "execution_count": 8,
@@ -1112,7 +1112,7 @@
        "<text text-anchor=\"start\" x=\"189.96\" y=\"-158.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;4 -->\n",
-       "<g id=\"edge6\" class=\"edge\">\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
        "<title>2&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M167.95,-196.4C181.93,-193.79 201.45,-190.14 216.79,-187.27\"/>\n",
        "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"223.94,-185.94 217.64,-190.32 220.6,-187.07 217.15,-187.72 217.06,-187.22 216.97,-186.73 220.41,-186.09 216.48,-184.13 223.94,-185.94 223.94,-185.94\"/>\n",
@@ -1126,7 +1126,7 @@
        "<text text-anchor=\"middle\" x=\"427.92\" y=\"-137.06\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
        "</g>\n",
        "<!-- 2&#45;&gt;5 -->\n",
-       "<g id=\"edge7\" class=\"edge\">\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
        "<title>2&#45;&gt;5</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M160.75,-208.85C168.39,-214.75 179.16,-222.01 189.96,-225.76 275.06,-255.28 319.26,-296.01 391.92,-242.76 413.34,-227.05 401.22,-210.86 409.92,-185.76 412.38,-178.66 415.21,-170.99 417.85,-164.03\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"420.4,-157.35 420.84,-165.01 419.15,-160.62 417.9,-163.89 417.9,-163.89 417.9,-163.89 419.15,-160.62 414.96,-162.76 420.4,-157.35 420.4,-157.35\"/>\n",
@@ -1176,7 +1176,7 @@
        "<text text-anchor=\"start\" x=\"277.96\" y=\"-198.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;6 -->\n",
-       "<g id=\"edge12\" class=\"edge\">\n",
+       "<g id=\"edge11\" class=\"edge\">\n",
        "<title>5&#45;&gt;6</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M442.18,-129.03C460.14,-113.14 492.15,-84.82 511.36,-67.81\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"516.89,-62.92 513.73,-69.92 514.27,-65.24 511.65,-67.56 511.65,-67.56 511.65,-67.56 514.27,-65.24 509.56,-65.2 516.89,-62.92 516.89,-62.92\"/>\n",
@@ -1184,7 +1184,7 @@
        "<text text-anchor=\"start\" x=\"463.92\" y=\"-110.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">❶</text>\n",
        "</g>\n",
        "<!-- 5&#45;&gt;7 -->\n",
-       "<g id=\"edge11\" class=\"edge\">\n",
+       "<g id=\"edge12\" class=\"edge\">\n",
        "<title>5&#45;&gt;7</title>\n",
        "<path fill=\"none\" stroke=\"#e31a1c\" stroke-width=\"2\" d=\"M409.86,-142.24C399.69,-142.52 386.71,-141.81 375.92,-137.76 366.67,-134.29 357.82,-127.88 350.82,-121.79\"/>\n",
        "<polygon fill=\"#e31a1c\" stroke=\"#e31a1c\" stroke-width=\"2\" points=\"345.4,-116.81 352.69,-119.22 348.32,-118.81 350.9,-121.18 350.56,-121.55 350.22,-121.91 347.64,-119.55 348.43,-123.87 345.4,-116.81 345.4,-116.81\"/>\n",
@@ -1208,7 +1208,7 @@
        "<text text-anchor=\"start\" x=\"375.92\" y=\"-107.56\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff7f00\">❷</text>\n",
        "</g>\n",
        "<!-- 8&#45;&gt;4 -->\n",
-       "<g id=\"edge15\" class=\"edge\">\n",
+       "<g id=\"edge16\" class=\"edge\">\n",
        "<title>8&#45;&gt;4</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M327.6,-192.49C320.95,-181.1 309.32,-164.86 293.96,-157.76 282.73,-152.57 270.27,-158.46 260.47,-165.83\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"255.04,-170.26 258.47,-163.39 257.75,-168.04 260.47,-165.83 260.47,-165.83 260.47,-165.83 257.75,-168.04 262.46,-168.27 255.04,-170.26 255.04,-170.26\"/>\n",
@@ -1222,7 +1222,7 @@
        "<text text-anchor=\"middle\" x=\"427.92\" y=\"-209.06\" font-family=\"Lato\" font-size=\"14.00\">9</text>\n",
        "</g>\n",
        "<!-- 8&#45;&gt;9 -->\n",
-       "<g id=\"edge16\" class=\"edge\">\n",
+       "<g id=\"edge15\" class=\"edge\">\n",
        "<title>8&#45;&gt;9</title>\n",
        "<path fill=\"none\" stroke=\"#33a02c\" stroke-width=\"2\" d=\"M356.13,-206.53C369.86,-207.74 388.1,-209.35 402.62,-210.62\"/>\n",
        "<polygon fill=\"#33a02c\" stroke=\"#33a02c\" stroke-width=\"2\" points=\"409.84,-211.26 402.59,-213.78 406.31,-211.45 402.82,-211.14 402.86,-210.64 402.91,-210.15 406.39,-210.45 403.14,-207.51 409.84,-211.26 409.84,-211.26\"/>\n",
@@ -1255,7 +1255,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa37f087db0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc7c250240> >"
       ]
      },
      "execution_count": 11,
@@ -1267,6 +1267,319 @@
     "spot.highlight_strategy(game)"
    ]
   },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "<h2>Reading an aiger-file</h2>\n",
+    "\n",
+    "<p>Read an aiger file. Note that we do not support the full \n",
+    "    <a href=\"http://fmv.jku.at/aiger/FORMAT.aiger\">syntax</a>, but are restricted to:\n",
+    "    <ul>\n",
+    "        <li>Input variables start at index 2 and are consecutively numbered.</li>\n",
+    "        <li>Latch variables start at index (1 + #inputs) * 2 and are consecutively numbered.</li>\n",
+    "        <li>If inputs or outputs are named in the comments, all of them have to be named.</li>\n",
+    "        <li>Gate number $n$ can only have latches, inputs or previously defined gates ($<n$). </li>\n",
+    "    </ul>\n",
+    "</p>"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "aag 5 2 0 2 3\n",
+      "2\n",
+      "4\n",
+      "10\n",
+      "6\n",
+      "6 2 4\n",
+      "8 3 5\n",
+      "10 7 9\n",
+      "i0 a\n",
+      "i1 b\n",
+      "o0 c\n",
+      "o1 d\n",
+      "\n"
+     ]
+    }
+   ],
+   "source": [
+    "#aiger file \n",
+    "aag_txt = \"\"\"aag 5 2 0 2 3\n",
+    "2\n",
+    "4\n",
+    "10\n",
+    "6\n",
+    "6 2 4\n",
+    "8 3 5\n",
+    "10 7 9\n",
+    "i0 a\n",
+    "i1 b\n",
+    "o0 c\n",
+    "o1 d\n",
+    "\"\"\"\n",
+    "print(aag_txt)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 13,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "this_aig = spot.aiger_circuit(aag_txt)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 14,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Title: %3 Pages: 1 -->\n",
+       "<svg width=\"202pt\" height=\"289pt\"\n",
+       " viewBox=\"0.00 0.00 202.39 289.50\" 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 285.5)\">\n",
+       "<title>%3</title>\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-285.5 198.39,-285.5 198.39,4 -4,4\"/>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"44.2,-46 5.2,-11.5 83.19,-11.5 44.2,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"44.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i0</text>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"129.2\" cy=\"-100\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"129.2\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;6 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>2&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M56.74,-35.07C70.27,-47 92.03,-66.21 108.18,-80.46\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"106.23,-83.4 116.04,-87.39 110.86,-78.15 106.23,-83.4\"/>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"65.2\" cy=\"-100\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"65.2\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;8 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>2&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M49.17,-41.77C51.92,-51.58 55.37,-63.89 58.36,-74.59\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"59.46\" cy=\"-78.53\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"140.2,-46 101.2,-11.5 179.19,-11.5 140.2,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"140.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i1</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;6 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>4&#45;&gt;6</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M137.31,-43.71C136.05,-52.28 134.55,-62.48 133.19,-71.76\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"129.72,-71.32 131.73,-81.72 136.64,-72.34 129.72,-71.32\"/>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;8 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>4&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M128.48,-35.72C116.36,-47.83 97.3,-66.9 83.26,-80.94\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"80.41\" cy=\"-83.79\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 10 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>10</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"65.2\" cy=\"-176.75\" rx=\"23\" ry=\"23\"/>\n",
+       "<text text-anchor=\"middle\" x=\"65.2\" y=\"-173.05\" font-family=\"Times,serif\" font-size=\"14.00\">10</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;10 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>6&#45;&gt;10</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M117.75,-114.36C108.69,-124.95 95.81,-139.99 85.07,-152.53\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"82.29\" cy=\"-155.79\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- o1o1 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>o1o1</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"150.2,-235.5 194.59,-270 105.8,-270 150.2,-235.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"150.2\" y=\"-254.8\" font-family=\"Times,serif\" font-size=\"14.00\">o1</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;o1o1 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>6&#45;&gt;o1o1:s</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M133.55,-117.85C139.22,-141.22 148.58,-185.13 150.01,-225.36\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"146.51,-225.56 150.2,-235.5 153.51,-225.43 146.51,-225.56\"/>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;10 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>8&#45;&gt;10</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M65.2,-118.34C65.2,-126.54 65.2,-136.58 65.2,-145.95\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"65.2\" cy=\"-149.95\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- o0o0 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>o0o0</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"44.2,-235.5 88.59,-270 -0.2,-270 44.2,-235.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"44.2\" y=\"-254.8\" font-family=\"Times,serif\" font-size=\"14.00\">o0</text>\n",
+       "</g>\n",
+       "<!-- 10&#45;&gt;o0o0 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>10&#45;&gt;o0o0:s</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M54.45,-196.9C50.57,-205.12 46.74,-215.16 45.07,-225.34\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"41.57,-225.23 44.2,-235.5 48.54,-225.83 41.57,-225.23\"/>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
+      "text/plain": [
+       "<spot.jupyter.SVG object>"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "display(this_aig.show())"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 15,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "aag 5 2 0 2 3\n",
+      "2\n",
+      "4\n",
+      "10\n",
+      "6\n",
+      "6 2 4\n",
+      "8 3 5\n",
+      "10 7 9\n",
+      "i0 i0\n",
+      "i1 i1\n",
+      "o0 o0\n",
+      "o1 o1\n",
+      "\n"
+     ]
+    }
+   ],
+   "source": [
+    "print(this_aig.to_str())"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 16,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "((2, 4), (3, 5), (7, 9))\n"
+     ]
+    }
+   ],
+   "source": [
+    "print(this_aig.gates())"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "<h2>Verifying an implementation</h2>\n",
+    "\n",
+    "<p>\n",
+    "    An aiger circuit can be transformed into a monitor. If the aiger represents the implementation of a strategy in the context of active control, it can be check for correctness. This is done by computing the intersecting of the monitor and the negation of the specification.\n",
+    "</p>"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 17,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"535pt\" height=\"115pt\"\n",
+       " viewBox=\"0.00 0.00 535.00 115.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 111)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-111 531,-111 531,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"260.5\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
+       "<text text-anchor=\"start\" x=\"252.5\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"263.5\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"263.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M208.65,-18C210.29,-18 224.65,-18 238.13,-18\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"245.44,-18 238.44,-21.15 241.94,-18 238.44,-18 238.44,-18 238.44,-18 241.94,-18 238.44,-14.85 245.44,-18 245.44,-18\"/>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M257.12,-35.04C255.82,-44.86 257.95,-54 263.5,-54 267.67,-54 269.9,-48.86 270.21,-42.14\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"269.88,-35.04 273.35,-41.88 270.04,-38.53 270.21,-42.03 270.21,-42.03 270.21,-42.03 270.04,-38.53 267.06,-42.18 269.88,-35.04 269.88,-35.04\"/>\n",
+       "<text text-anchor=\"start\" x=\"0\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">(!i0 &amp; !i1 &amp; !o0 &amp; !o1) | (!i0 &amp; i1 &amp; o0 &amp; !o1) | (i0 &amp; !i1 &amp; o0 &amp; !o1) | (i0 &amp; i1 &amp; !o0 &amp; o1)</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
+      "text/plain": [
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbc7c1f07b0> >"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "aigasmon = this_aig.as_automaton()\n",
+    "display(aigasmon)"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
@@ -1291,7 +1604,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.9.1rc1"
+   "version": "3.8.10"
   }
  },
  "nbformat": 4,