From d430129bb1fd84546852d3d7b3936f1e4077f00b Mon Sep 17 00:00:00 2001
From: Etienne Renault <renault@lrde.epita.fr>
Date: Wed, 20 Apr 2016 14:22:21 +0200
Subject: [PATCH] convert: simplify interfaces

* spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh,
tests/core/twacube.cc: here.
---
 spot/twacube_algos/convert.cc | 13 ++++++++-----
 spot/twacube_algos/convert.hh |  9 ++++-----
 tests/core/twacube.cc         | 12 +++---------
 3 files changed, 15 insertions(+), 19 deletions(-)

diff --git a/spot/twacube_algos/convert.cc b/spot/twacube_algos/convert.cc
index 44aeb9e49..fdf506eb7 100644
--- a/spot/twacube_algos/convert.cc
+++ b/spot/twacube_algos/convert.cc
@@ -59,12 +59,14 @@ namespace spot
     return result;
   }
 
-  spot::twacube* twa_to_twacube(spot::twa_graph_ptr& aut,
-                                std::unordered_map<int, int>& ap_binder,
-                                std::vector<std::string>& aps)
+  spot::twacube* twa_to_twacube(const spot::const_twa_graph_ptr aut)
   {
+    // Compute the necessary binder and extract atomic propositions
+    std::unordered_map<int, int> ap_binder;
+    std::vector<std::string>* aps = extract_aps(aut, ap_binder);
+
     // Declare the twa cube
-    spot::twacube* tg = new spot::twacube(aps);
+    spot::twacube* tg = new spot::twacube(*aps);
 
     // Fix acceptance
     tg->acc() = aut->acc();
@@ -111,11 +113,12 @@ namespace spot
         }
     // Must be contiguous to support swarming.
     assert(tg->succ_contiguous());
+    delete aps;
     return tg;
   }
 
   std::vector<std::string>*
-  extract_aps(spot::twa_graph_ptr& aut,
+  extract_aps(const spot::const_twa_graph_ptr aut,
               std::unordered_map<int, int>& ap_binder)
   {
     std::vector<std::string>* aps = new std::vector<std::string>();
diff --git a/spot/twacube_algos/convert.hh b/spot/twacube_algos/convert.hh
index bcba3a671..b23e3f6b4 100644
--- a/spot/twacube_algos/convert.hh
+++ b/spot/twacube_algos/convert.hh
@@ -40,16 +40,15 @@ namespace spot
   SPOT_API bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset,
                            std::unordered_map<int, int>& reverse_binder);
 
-  /// \brief Extract the atomic propositions from the automaton
+  /// \brief Extract the atomic propositions from the automaton. This method
+  /// also fill the binder, i.e. the mapping between BDD indexes to cube indexes
   SPOT_API std::vector<std::string>*
-  extract_aps(spot::twa_graph_ptr& aut,
+  extract_aps(spot::const_twa_graph_ptr aut,
               std::unordered_map<int, int>& ap_binder);
 
   /// \brief Convert a twa into a twacube
   SPOT_API spot::twacube*
-  twa_to_twacube(spot::twa_graph_ptr& aut,
-                 std::unordered_map<int, int>& ap_binder,
-                 std::vector<std::string>& aps);
+  twa_to_twacube(spot::const_twa_graph_ptr aut);
 
   /// \brief Convert a twacube into a twa
   SPOT_API spot::twa_graph_ptr
diff --git a/tests/core/twacube.cc b/tests/core/twacube.cc
index 28d8cacfc..73b31a77d 100644
--- a/tests/core/twacube.cc
+++ b/tests/core/twacube.cc
@@ -46,29 +46,23 @@ int main()
   tg->new_edge(s3, s2, p1 >> p2, 0U);
   tg->new_edge(s3, s3, bddtrue, spot::acc_cond::mark_t({0, 1}));
 
-  // Map Bdd indexes to cube indexes
-  std::unordered_map<int, int> ap_binder;
-
-  // Get the set of propositions used by this automaton
-  std::vector<std::string>* aps = extract_aps(tg, ap_binder);
-
   // Test translation
-  auto* aut = twa_to_twacube(tg, ap_binder, *aps);
+  auto* aut = twa_to_twacube(tg);
   spot::print_dot(std::cout, tg);
   std::cout << "-----------\n" << *aut << "-----------\n";
 
+  const std::vector<std::string>& aps = aut->get_ap();
   unsigned int seed = 17;
   for (auto it = aut->succ(2); !it->done(); it->next())
     {
       auto& t = aut->trans_storage(it, seed);
       auto& d = aut->trans_data(it, seed);
       std::cout << t.src << ' ' << t.dst << ' '
-                << ' ' << aut->get_cubeset().dump(d.cube_, *aps)
+                << ' ' << aut->get_cubeset().dump(d.cube_, aps)
                 << ' ' << d.acc_
                 << std::endl;
     }
 
   spot::print_dot(std::cout, spot::twacube_to_twa(aut));
-  delete aps;
   delete aut;
 }