From eadcf95363a0e31c089f4c677e3c8741ed6c9474 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 9 Jan 2015 17:10:28 +0100
Subject: [PATCH] powerset: rewrite using the tgba_digraph interface

Fixes #48.

* src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh: Here.
* src/tgbaalgos/minimize.cc: Adjust usage.
---
 src/tgbaalgos/minimize.cc |  7 +++----
 src/tgbaalgos/powerset.cc | 22 +++++++++-------------
 src/tgbaalgos/powerset.hh | 11 ++---------
 3 files changed, 14 insertions(+), 26 deletions(-)

diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc
index 6c6a97bea..38baae608 100644
--- a/src/tgbaalgos/minimize.cc
+++ b/src/tgbaalgos/minimize.cc
@@ -254,12 +254,11 @@ namespace spot
       // Iterate on each original state corresponding to start.
       const power_map::power_state& ps =
 	pm.states_of(det_a->state_number(start));
-      for (auto& it: ps)
+      for (auto& s: ps)
 	{
 	  // Construct a product between LOOP_A and ORIG_A starting in
-	  // *IT.  FIXME: This could be sped up a lot!
-	  if (!product(loop_a, orig_a, 0U,
-		       orig_a->state_number(it))->is_empty())
+	  // S.  FIXME: This could be sped up a lot!
+	  if (!product(loop_a, orig_a, 0U, s)->is_empty())
 	    {
 	      accepting = true;
 	      break;
diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc
index 46611f334..1ecb5d08b 100644
--- a/src/tgbaalgos/powerset.cc
+++ b/src/tgbaalgos/powerset.cc
@@ -41,7 +41,6 @@
 
 namespace spot
 {
-  // FIXME: Redo this algorithm using the tgba_digraph interface.
   tgba_digraph_ptr
   tgba_powerset(const const_tgba_digraph_ptr& aut, power_map& pm, bool merge)
   {
@@ -55,9 +54,7 @@ namespace spot
     res->copy_ap_of(aut);
 
     {
-      power_state ps;
-      const state* s = pm.canonicalize(aut->get_init_state());
-      ps.insert(s);
+      power_state ps{aut->get_init_state_number()};
       todo.push_back(ps);
       unsigned num = res->new_state();
       seen[ps] = num;
@@ -71,8 +68,8 @@ namespace spot
 	// Compute all variables occurring on outgoing arcs.
 	bdd all_vars = bddtrue;
 	for (auto s: src)
-	  for (auto i: aut->succ(s))
-	    all_vars &= bdd_support(i->current_condition());
+	  for (auto i: aut->out(s))
+	    all_vars &= bdd_support(i.cond);
 
 	bdd all_conds = bddtrue;
 	// Iterate over all possible conditions
@@ -84,13 +81,13 @@ namespace spot
 	    // Construct the set of all states reachable via COND.
 	    power_state dest;
 	    for (auto s: src)
-	      for (auto si: aut->succ(s))
-		if ((cond >> si->current_condition()) == bddtrue)
-		  dest.insert(pm.canonicalize(si->current_state()));
+	      for (auto si: aut->out(s))
+		if ((cond >> si.cond) == bddtrue)
+		  dest.insert(si.dst);
 	    if (dest.empty())
 	      continue;
 	    // Add that transition.
-	    power_set::const_iterator i = seen.find(dest);
+	    auto i = seen.find(dest);
 	    int dest_num;
 	    if (i != seen.end())
 	      {
@@ -204,8 +201,7 @@ namespace spot
 	  {
 	    // Check the product between LOOP_A, and ORIG_A starting
 	    // in S.
-	    if (!product(loop_a, ref_,
-			 loop_a_init, ref_->state_number(s))->is_empty())
+	    if (!product(loop_a, ref_, loop_a_init, s)->is_empty())
 	      {
 		accepting = true;
 		break;
@@ -296,7 +292,7 @@ namespace spot
     auto det = tgba_powerset(aut, pm, false);
 
     if ((threshold_states > 0)
-	&& (pm.map_.size() > pm.states_.size() * threshold_states))
+	&& (pm.map_.size() > aut->num_states() * threshold_states))
       return nullptr;
     if (fix_dba_acceptance(det, aut, pm, threshold_cycles))
       return nullptr;
diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh
index 8faecddd4..edd87de46 100644
--- a/src/tgbaalgos/powerset.hh
+++ b/src/tgbaalgos/powerset.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
+// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et
 // Développement de l'Epita.
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -32,7 +32,7 @@ namespace spot
 
   struct SPOT_API power_map
   {
-    typedef std::set<const state*, state_ptr_less_than> power_state;
+    typedef std::set<unsigned> power_state;
     typedef std::map<unsigned, power_state> power_map_data;
 
     const power_state&
@@ -41,14 +41,7 @@ namespace spot
       return map_.at(s);
     }
 
-    const state*
-    canonicalize(const state* s)
-    {
-      return states_(s);
-    }
-
     power_map_data map_;
-    state_unicity_table states_;
   };