From b9a39c557625279eed37f96e66979460264da431 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 7 Oct 2021 11:23:51 +0200
Subject: [PATCH] aiger: fix forcing of input properties

* spot/twaalgos/aiger.cc: Here.
* tests/python/synthesis.ipynb: Adjust.
---
 spot/twaalgos/aiger.cc       |   6 +-
 tests/python/synthesis.ipynb | 116 +++++++++++++++++------------------
 2 files changed, 58 insertions(+), 64 deletions(-)

diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc
index ad10db6e9..a7c2edafc 100644
--- a/spot/twaalgos/aiger.cc
+++ b/spot/twaalgos/aiger.cc
@@ -1473,7 +1473,7 @@ namespace
     std::vector<std::string> input_names_all = input_names;
     input_names_all.insert(input_names_all.end(),
                            unused_ins.cbegin(),
-                          unused_ins.cend());
+                           unused_ins.cend());
     std::vector<std::string> output_names_all = output_names;
     output_names_all.insert(output_names_all.end(),
                             unused_outs.cbegin(),
@@ -1872,7 +1872,7 @@ namespace spot
           unused_outs.push_back(ao);
       for (const auto& ai : ins)
         if (!used_aps.count(ai))
-          unused_outs.push_back(ai);
+          unused_ins.push_back(ai);
     }
     // todo Some additional checks?
     return auts_to_aiger({{aut, get_synthesis_outputs(aut)}}, mode,
@@ -1934,7 +1934,7 @@ namespace spot
           unused_outs.push_back(ao);
     for (const auto& ai : ins)
       if (!used_aps.count(ai))
-        unused_outs.push_back(ai);
+        unused_ins.push_back(ai);
 
     return auts_to_aiger(new_vec, mode, unused_ins, unused_outs);
   }
diff --git a/tests/python/synthesis.ipynb b/tests/python/synthesis.ipynb
index 09a8febff..24efe9d8e 100644
--- a/tests/python/synthesis.ipynb
+++ b/tests/python/synthesis.ipynb
@@ -696,7 +696,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa0f4223360> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8d9c0983f0> >"
       ]
      },
      "metadata": {},
@@ -2509,7 +2509,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa0f4b39690> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8d9c4f8b10> >"
       ]
      },
      "execution_count": 5,
@@ -2749,7 +2749,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa0f4b395a0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8d9c098510> >"
       ]
      },
      "execution_count": 6,
@@ -2838,7 +2838,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fa0f4b39b70> >"
+       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f8d9c4f8a80> >"
       ]
      },
      "metadata": {},
@@ -3056,7 +3056,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa0f4223090> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8d9c098ed0> >"
       ]
      },
      "metadata": {},
@@ -3133,7 +3133,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fa0f5be7ed0> >"
+       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f8d9c098d80> >"
       ]
      },
      "metadata": {},
@@ -3173,27 +3173,27 @@
        "<!-- Generated by graphviz version 2.43.0 (0)\n",
        " -->\n",
        "<!-- Pages: 1 -->\n",
-       "<svg width=\"344pt\" height=\"352pt\"\n",
-       " viewBox=\"0.00 0.00 344.50 352.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<svg width=\"328pt\" height=\"352pt\"\n",
+       " viewBox=\"0.00 0.00 327.70 352.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 348)\">\n",
-       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-348 340.5,-348 340.5,4 -4,4\"/>\n",
-       "<!-- 4 -->\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-348 323.7,-348 323.7,4 -4,4\"/>\n",
+       "<!-- 6 -->\n",
        "<g id=\"node1\" class=\"node\">\n",
-       "<title>4</title>\n",
+       "<title>6</title>\n",
        "<polygon fill=\"none\" stroke=\"black\" points=\"65,-118 0,-118 0,-82 65,-82 65,-118\"/>\n",
        "<text text-anchor=\"middle\" x=\"32.5\" y=\"-96.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0_out</text>\n",
        "</g>\n",
-       "<!-- 6 -->\n",
-       "<g id=\"node4\" class=\"node\">\n",
-       "<title>6</title>\n",
-       "<ellipse fill=\"none\" stroke=\"black\" cx=\"62.5\" cy=\"-172\" rx=\"18\" ry=\"18\"/>\n",
-       "<text text-anchor=\"middle\" x=\"62.5\" y=\"-168.3\" font-family=\"Times,serif\" font-size=\"14.00\">6</text>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"63.5\" cy=\"-172\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"63.5\" y=\"-168.3\" font-family=\"Times,serif\" font-size=\"14.00\">8</text>\n",
        "</g>\n",
-       "<!-- 4&#45;&gt;6 -->\n",
+       "<!-- 6&#45;&gt;8 -->\n",
        "<g id=\"edge2\" class=\"edge\">\n",
-       "<title>4&#45;&gt;6</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M39.92,-118.3C43.66,-127.03 48.25,-137.76 52.32,-147.25\"/>\n",
-       "<ellipse fill=\"black\" stroke=\"black\" cx=\"54.01\" cy=\"-151.18\" rx=\"4\" ry=\"4\"/>\n",
+       "<title>6&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M40.16,-118.3C44.12,-127.25 49.01,-138.29 53.29,-147.94\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"54.94\" cy=\"-151.67\" rx=\"4\" ry=\"4\"/>\n",
        "</g>\n",
        "<!-- 2 -->\n",
        "<g id=\"node2\" class=\"node\">\n",
@@ -3201,71 +3201,65 @@
        "<polygon fill=\"none\" stroke=\"black\" points=\"93.5,-46 54.51,-11.5 132.49,-11.5 93.5,-46\"/>\n",
        "<text text-anchor=\"middle\" x=\"93.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i0</text>\n",
        "</g>\n",
-       "<!-- 2&#45;&gt;6 -->\n",
+       "<!-- 2&#45;&gt;8 -->\n",
        "<g id=\"edge1\" class=\"edge\">\n",
-       "<title>2&#45;&gt;6</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M89.57,-42.62C84.15,-68.35 74.32,-114.94 68.12,-144.35\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"64.65,-143.84 66.01,-154.35 71.5,-145.28 64.65,-143.84\"/>\n",
+       "<title>2&#45;&gt;8</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M89.64,-42.92C84.4,-68.61 74.99,-114.68 69.01,-144\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"65.54,-143.48 66.97,-153.98 72.4,-144.88 65.54,-143.48\"/>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"189.5,-46 150.51,-11.5 228.49,-11.5 189.5,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"189.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">i1</text>\n",
        "</g>\n",
        "<!-- L0 -->\n",
-       "<g id=\"node3\" class=\"node\">\n",
+       "<g id=\"node4\" class=\"node\">\n",
        "<title>L0</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"62.5,-262 8.5,-262 8.5,-226 62.5,-226 62.5,-262\"/>\n",
-       "<text text-anchor=\"middle\" x=\"35.5\" y=\"-240.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0</text>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"63.5,-262 9.5,-262 9.5,-226 63.5,-226 63.5,-262\"/>\n",
+       "<text text-anchor=\"middle\" x=\"36.5\" y=\"-240.3\" font-family=\"Times,serif\" font-size=\"14.00\">L0</text>\n",
        "</g>\n",
-       "<!-- 6&#45;&gt;L0 -->\n",
+       "<!-- 8&#45;&gt;L0 -->\n",
        "<g id=\"edge3\" class=\"edge\">\n",
-       "<title>6&#45;&gt;L0</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M56.24,-189.24C53.13,-197.3 49.29,-207.26 45.76,-216.4\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"42.44,-215.29 42.1,-225.88 48.97,-217.81 42.44,-215.29\"/>\n",
+       "<title>8&#45;&gt;L0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M57.24,-189.24C54.13,-197.3 50.29,-207.26 46.76,-216.4\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"43.44,-215.29 43.1,-225.88 49.97,-217.81 43.44,-215.29\"/>\n",
        "</g>\n",
        "<!-- o0o0 -->\n",
-       "<g id=\"node5\" class=\"node\">\n",
+       "<g id=\"node6\" class=\"node\">\n",
        "<title>o0o0</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"90.5,-298 134.89,-332.5 46.11,-332.5 90.5,-298\"/>\n",
-       "<text text-anchor=\"middle\" x=\"90.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">o0</text>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"91.5,-298 135.89,-332.5 47.11,-332.5 91.5,-298\"/>\n",
+       "<text text-anchor=\"middle\" x=\"91.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">o0</text>\n",
        "</g>\n",
-       "<!-- 6&#45;&gt;o0o0 -->\n",
+       "<!-- 8&#45;&gt;o0o0 -->\n",
        "<g id=\"edge4\" class=\"edge\">\n",
-       "<title>6&#45;&gt;o0o0:s</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M68.58,-189.32C76.1,-210.91 88.19,-250.57 90.21,-287.63\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"86.72,-288.1 90.5,-298 93.72,-287.91 86.72,-288.1\"/>\n",
+       "<title>8&#45;&gt;o0o0:s</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M69.58,-189.32C77.1,-210.91 89.19,-250.57 91.21,-287.63\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"87.72,-288.1 91.5,-298 94.72,-287.91 87.72,-288.1\"/>\n",
        "</g>\n",
        "<!-- o1o1 -->\n",
-       "<g id=\"node6\" class=\"node\">\n",
+       "<g id=\"node7\" class=\"node\">\n",
        "<title>o1o1</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"196.5,-298 240.89,-332.5 152.11,-332.5 196.5,-298\"/>\n",
-       "<text text-anchor=\"middle\" x=\"196.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">o1</text>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"275.5,-298 319.89,-332.5 231.11,-332.5 275.5,-298\"/>\n",
+       "<text text-anchor=\"middle\" x=\"275.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">o1</text>\n",
        "</g>\n",
        "<!-- 0 -->\n",
-       "<g id=\"node7\" class=\"node\">\n",
+       "<g id=\"node8\" class=\"node\">\n",
        "<title>0</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"218.5,-5 276.5,-5 276.5,-41 218.5,-41 218.5,-5\"/>\n",
-       "<text text-anchor=\"middle\" x=\"247.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">Const</text>\n",
+       "<polygon fill=\"none\" stroke=\"black\" points=\"246.5,-5 304.5,-5 304.5,-41 246.5,-41 246.5,-5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"275.5\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">Const</text>\n",
        "</g>\n",
        "<!-- 0&#45;&gt;o1o1 -->\n",
        "<g id=\"edge5\" class=\"edge\">\n",
        "<title>0&#45;&gt;o1o1:s</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M242.04,-41.1C229.34,-82.44 198.69,-191.49 196.61,-287.82\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"193.11,-287.96 196.5,-298 200.11,-288.04 193.11,-287.96\"/>\n",
-       "</g>\n",
-       "<!-- o2i1 -->\n",
-       "<g id=\"node8\" class=\"node\">\n",
-       "<title>o2i1</title>\n",
-       "<polygon fill=\"none\" stroke=\"black\" points=\"297.5,-298 336.49,-332.5 258.51,-332.5 297.5,-298\"/>\n",
-       "<text text-anchor=\"middle\" x=\"297.5\" y=\"-317.3\" font-family=\"Times,serif\" font-size=\"14.00\">i1</text>\n",
-       "</g>\n",
-       "<!-- 0&#45;&gt;o2i1 -->\n",
-       "<g id=\"edge6\" class=\"edge\">\n",
-       "<title>0&#45;&gt;o2i1:s</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M252.85,-41.11C265.31,-82.47 295.35,-191.55 297.39,-287.83\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"293.89,-288.04 297.5,-298 300.89,-287.96 293.89,-288.04\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M275.5,-41.31C275.5,-83.11 275.5,-193.09 275.5,-287.99\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"272,-288 275.5,-298 279,-288 272,-288\"/>\n",
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fa0f4223a80> >"
+       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f8d9c5bade0> >"
       ]
      },
      "metadata": {},
@@ -3424,7 +3418,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fa0f4223e40> >"
+       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7f8d9c4f8a80> >"
       ]
      },
      "metadata": {},
@@ -3536,7 +3530,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa0f4223c60> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f8d9c0720c0> >"
       ]
      },
      "execution_count": 14,