From b87693bcc3252ee89b86cdf161b27347a776a161 Mon Sep 17 00:00:00 2001
From: Etienne Renault <renault@lrde.epita.fr>
Date: Sat, 5 Dec 2015 07:58:27 +0100
Subject: [PATCH] convert: twacube to twa translation

* spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh,
tests/core/twacube.cc, tests/core/twacube.test: here.
---
 spot/twacube_algos/convert.cc | 50 +++++++++++++++++++++++++++++++++++
 spot/twacube_algos/convert.hh |  4 +++
 tests/core/twacube.cc         |  1 +
 tests/core/twacube.test       | 18 +++++++++++++
 4 files changed, 73 insertions(+)

diff --git a/spot/twacube_algos/convert.cc b/spot/twacube_algos/convert.cc
index 53daca648..b8bf42266 100644
--- a/spot/twacube_algos/convert.cc
+++ b/spot/twacube_algos/convert.cc
@@ -130,4 +130,54 @@ namespace spot
       }
     return aps;
   }
+
+  spot::twa_graph_ptr
+  twacube_to_twa(spot::twacube* twacube)
+  {
+    // Grab necessary variables
+    auto& theg = twacube->get_graph();
+    spot::cubeset cs = twacube->get_cubeset();
+
+    // Build the resulting graph
+    auto d = spot::make_bdd_dict();
+    auto res = make_twa_graph(d);
+
+    // Fix the acceptance of the resulting automaton
+    res->acc() = twacube->acc();
+
+    // Grep bdd id for each atomic propositions
+    std::vector<int> bdds_ref;
+    for (auto& ap : twacube->get_ap())
+      bdds_ref.push_back(res->register_ap(ap));
+
+    // Build all resulting states
+    for (unsigned int i = 0; i < theg.num_states(); ++i)
+      {
+	unsigned st = res->new_state();
+	(void) st;
+	assert(st == i);
+      }
+
+    // Build all resulting conditions.
+    for (unsigned int i = 1; i <= theg.num_edges(); ++i)
+      {
+	bdd cond = bddtrue;
+	for (unsigned j = 0; j < cs.size(); ++j)
+	  {
+	    if (cs.is_true_var(theg.edge_data(i).cube_, j))
+	      cond &= bdd_ithvar(bdds_ref[j]);
+	    else if (cs.is_false_var(theg.edge_data(i).cube_, j))
+	      cond &= bdd_nithvar(bdds_ref[j]);
+	    // otherwise it 's a free variable do nothing
+	  }
+
+	res->new_edge(theg.edge_storage(i).src, theg.edge_storage(i).dst,
+		      cond, theg.edge_data(i).acc_);
+      }
+
+    // Fix the initial state
+    res->set_init_state(twacube->get_initial());
+
+    return res;
+  }
 }
diff --git a/spot/twacube_algos/convert.hh b/spot/twacube_algos/convert.hh
index 7f3d8c55a..5c6f2569d 100644
--- a/spot/twacube_algos/convert.hh
+++ b/spot/twacube_algos/convert.hh
@@ -50,4 +50,8 @@ namespace spot
   twa_to_twacube(spot::twa_graph_ptr& aut,
 		 std::unordered_map<int, int>& ap_binder,
 		 std::vector<std::string>& aps);
+
+  /// \brief Convert a twacube into a twa
+  SPOT_API spot::twa_graph_ptr
+  twacube_to_twa(spot::twacube* twacube);
 }
diff --git a/tests/core/twacube.cc b/tests/core/twacube.cc
index 08ab25323..c67ffbbab 100644
--- a/tests/core/twacube.cc
+++ b/tests/core/twacube.cc
@@ -68,6 +68,7 @@ int main()
 		<< std::endl;
     }
 
+  spot::print_dot(std::cout, spot::twacube_to_twa(aut));
   delete aps;
   delete aut;
 }
diff --git a/tests/core/twacube.test b/tests/core/twacube.test
index 125e17829..69f82f478 100755
--- a/tests/core/twacube.test
+++ b/tests/core/twacube.test
@@ -66,6 +66,24 @@ init : 0
 2 0  p1 {0,1}
 2 1  p1&p2 {}
 2 0  !p1&p2 {0,1}
+digraph G {
+  rankdir=LR
+  node [shape="circle"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 0 [label="!p1 & !p2"]
+  0 -> 1 [label="p1"]
+  0 -> 2 [label="p2\n{1}"]
+  1 [label="1"]
+  1 -> 2 [label="p1 & p2\n{0}"]
+  2 [label="2"]
+  2 -> 0 [label="!p1 & p2\n{0,1}"]
+  2 -> 0 [label="p1\n{0,1}"]
+  2 -> 1 [label="!p1"]
+  2 -> 1 [label="p1 & p2"]
+  2 -> 2 [label="1\n{0,1}"]
+}
 EOF
 
 diff stdout expected