dupexp: rename to copy, and preserve named states on request

* src/twaalgos/dupexp.cc, src/twaalgos/dupexp.hh: Rename to...
* src/twaalgos/copy.cc, src/twaalgos/copy.hh: ... these.
Get rid of dupexp_bfs, rename dupexp_dfs as copy, and add
an option to preserve named states.
* src/twaalgos/Makefile.am, src/tests/dupexp.test,
src/tests/ikwiad.cc, src/tests/sccsimpl.test,
src/twa/twagraph.hh, src/twaalgos/dot.cc,
src/twaalgos/stutter.cc, wrap/python/spot_impl.i: Adjust.
* NEWS: Mention this change.

NEWS

@@ -49,6 +49,9 @@ New in spot 1.99.3a (not yet released)
   * For similar reasons, the spot::ltl namespace has been merged
     with the spot namespace.
 
+  * The dupexp_dfs() function has been renamed to copy(),
+    and as learn to preserve named states if required.
+
 New in spot 1.99.3 (2015-08-26)
 
   * The CGI script for LTL translation offers a HOA download link

src/tests/dupexp.test

@@ -28,7 +28,7 @@ set -e
 
 dorun()
 {
-  run 0 ../ikwiad -f -s "$1" >output1
+  run 0 ../ikwiad -f "$1" >output1
   run 0 ../ikwiad -f -S "$1" >output2
   test `wc -l <output1` = `wc -l <output2`
 }

src/tests/ikwiad.cc

@@ -40,7 +40,7 @@
 #include "twa/twaproduct.hh"
 #include "twaalgos/reducerun.hh"
 #include "parseaut/public.hh"
-#include "twaalgos/dupexp.hh"
+#include "twaalgos/copy.hh"
 #include "twaalgos/minimize.hh"
 #include "taalgos/minimize.hh"
 #include "twaalgos/neverclaim.hh"
@@ -334,7 +334,7 @@ checked_main(int argc, char** argv)
   int formula_index = 0;
   const char* echeck_algo = nullptr;
   spot::emptiness_check_instantiator_ptr echeck_inst = nullptr;
-  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
+  bool dupexp = false;
   bool expect_counter_example = false;
   bool accepting_run = false;
   bool accepting_run_replay = false;
@@ -740,13 +740,9 @@ checked_main(int argc, char** argv)
         {
           opt_monitor = true;
         }
-      else if (!strcmp(argv[formula_index], "-s"))
-	{
-	  dupexp = DFS;
-	}
       else if (!strcmp(argv[formula_index], "-S"))
 	{
-	  dupexp = BFS;
+	  dupexp = true;
 	}
       else if (!strcmp(argv[formula_index], "-CL"))
 	{
@@ -1266,17 +1262,8 @@ checked_main(int argc, char** argv)
 				// pointless.
 	}
 
-      switch (dupexp)
+      if (dupexp)
-	{
+	a = copy(a, spot::twa::prop_set::all());
-	case NoneDup:
-	  break;
-	case BFS:
-	  a = tgba_dupexp_bfs(a, spot::twa::prop_set::all());
-	  break;
-	case DFS:
-	  a = tgba_dupexp_dfs(a, spot::twa::prop_set::all());
-	  break;
-	}
 
       //TA, STA, GTA, SGTA and TGTA
       if (ta_opt || tgta_opt)

src/tests/sccsimpl.test

@@ -237,7 +237,7 @@ grep 'Acceptance: 2 ' out8.txt
 # This formula gives a 12-state automaton in which one acceptance
 # condition can be removed, and after what direct simulation should
 # simplify the automaton to 6 states.
-run 0 ../ikwiad -R3 -s -RDS -ks \
+run 0 ../ikwiad -R3 -RDS -ks \
   '(G(!((b) R (a)))) R (((c) R (!(d))) U (G((a) | (!(G(e))))))' > out9.txt
 grep 'states: 6$' out9.txt
 

src/twa/twagraph.hh

@@ -24,7 +24,7 @@
 #include "graph/ngraph.hh"
 #include "twa/bdddict.hh"
 #include "twa/twa.hh"
-#include "twaalgos/dupexp.hh"
+#include "twaalgos/copy.hh"
 #include "tl/formula.hh"
 #include <sstream>
 
@@ -494,6 +494,6 @@ namespace spot
     if (a)
       return std::make_shared<twa_graph>(a, p);
     else
-      return tgba_dupexp_dfs(aut, p);
+      return copy(aut, p);
   }
 }

src/twaalgos/Makefile.am

@@ -34,13 +34,13 @@ twaalgos_HEADERS = \
   cleanacc.hh \
   complete.hh \
   compsusp.hh \
+  copy.hh \
   cycles.hh \
   dtgbacomp.hh \
   degen.hh \
   dot.hh \
   dtbasat.hh \
   dtgbasat.hh \
-  dupexp.hh \
   emptiness.hh \
   emptiness_stats.hh \
   gv04.hh \
@@ -91,13 +91,13 @@ libtwaalgos_la_SOURCES = \
   cleanacc.cc \
   complete.cc \
   compsusp.cc \
+  copy.cc \
   cycles.cc \
   dtgbacomp.cc \
   degen.cc \
   dot.cc \
   dtbasat.cc \
   dtgbasat.cc \
-  dupexp.cc \
   emptiness.cc \
   gv04.cc \
   hoa.cc \

src/twaalgos/copy.cc

@@ -20,7 +20,7 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-#include "dupexp.hh"
+#include "copy.hh"
 #include "twa/twagraph.hh"
 #include <sstream>
 #include <string>
@@ -32,16 +32,22 @@ namespace spot
 {
   namespace
   {
-    template <class T>
+    class copy_iter: public tgba_reachable_iterator_depth_first
-    class dupexp_iter: public T
     {
     public:
-      dupexp_iter(const const_twa_ptr& a, twa::prop_set p)
+      copy_iter(const const_twa_ptr& a, twa::prop_set p,
-	: T(a), out_(make_twa_graph(a->get_dict()))
+		bool preserve_names)
+	: tgba_reachable_iterator_depth_first(a),
+	  out_(make_twa_graph(a->get_dict()))
       {
 	out_->copy_acceptance_of(a);
 	out_->copy_ap_of(a);
 	out_->prop_copy(a, p);
+	if (preserve_names)
+	  {
+	    names_ = new std::vector<std::string>;
+	    out_->set_named_prop("state-names", names_);
+	  }
       }
 
       twa_graph_ptr
@@ -51,9 +57,11 @@ namespace spot
       }
 
       virtual void
-      process_state(const state*, int n, twa_succ_iterator*)
+      process_state(const state* s, int n, twa_succ_iterator*)
       {
 	unsigned ns = out_->new_state();
+	if (names_)
+	  names_->emplace_back(aut_->format_state(s));
 	assert(ns == static_cast<unsigned>(n) - 1);
 	(void)ns;
 	(void)n;
@@ -71,22 +79,15 @@ namespace spot
 
     protected:
       twa_graph_ptr out_;
+      std::vector<std::string>* names_ = nullptr;
     };
 
   } // anonymous
 
   twa_graph_ptr
-  tgba_dupexp_bfs(const const_twa_ptr& aut, twa::prop_set p)
+  copy(const const_twa_ptr& aut, twa::prop_set p, bool preserve_names)
   {
-    dupexp_iter<tgba_reachable_iterator_breadth_first> di(aut, p);
+    copy_iter di(aut, p, preserve_names);
-    di.run();
-    return di.result();
-  }
-
-  twa_graph_ptr
-  tgba_dupexp_dfs(const const_twa_ptr& aut, twa::prop_set p)
-  {
-    dupexp_iter<tgba_reachable_iterator_depth_first> di(aut, p);
     di.run();
     return di.result();
   }

src/twaalgos/copy.hh

@@ -31,12 +31,9 @@ namespace spot
 {
   /// \ingroup twa_misc
   /// \brief Build an explicit automaton from all states of \a aut,
-  /// numbering states in bread first order as they are processed.
+  ///
+  /// This works for using the abstract interface for automata
   SPOT_API twa_graph_ptr
-  tgba_dupexp_bfs(const const_twa_ptr& aut, twa::prop_set p);
+  copy(const const_twa_ptr& aut, twa::prop_set p,
-  /// \ingroup twa_misc
+       bool preserve_names = false);
-  /// \brief Build an explicit automaton from all states of \a aut,
-  /// numbering states in depth first order as they are processed.
-  SPOT_API twa_graph_ptr
-  tgba_dupexp_dfs(const const_twa_ptr& aut, twa::prop_set p);
 }

src/twaalgos/dot.cc

@@ -29,6 +29,7 @@
 #include "misc/escape.hh"
 #include "twa/twagraph.hh"
 #include "twa/formula2bdd.hh"
+#include "twaalgos/copy.hh"
 #include "twaalgos/sccinfo.hh"
 #include <cstdlib>
 #include <cstring>
@@ -534,7 +535,7 @@ namespace spot
     dotty_output d(os, options);
     auto aut = std::dynamic_pointer_cast<const twa_graph>(g);
     if (!aut)
-      aut = make_twa_graph(g, twa::prop_set::all());
+      aut = copy(g, twa::prop_set::all(), true);
     d.print(aut);
     return os;
   }

src/twaalgos/stutter.cc

@@ -19,7 +19,6 @@
 
 #include "stutter.hh"
 #include "twa/twa.hh"
-#include "dupexp.hh"
 #include "misc/hash.hh"
 #include "misc/hashfunc.hh"
 #include "tl/apcollect.hh"

wrap/python/spot_impl.i

@@ -110,7 +110,7 @@
 #include "twaalgos/cleanacc.hh"
 #include "twaalgos/dot.hh"
 #include "twaalgos/degen.hh"
-#include "twaalgos/dupexp.hh"
+#include "twaalgos/copy.hh"
 #include "twaalgos/emptiness.hh"
 #include "twaalgos/gtec/gtec.hh"
 #include "twaalgos/lbtt.hh"
@@ -254,7 +254,7 @@ namespace std {
 %include "twaalgos/cleanacc.hh"
 %include "twaalgos/degen.hh"
 %include "twaalgos/dot.hh"
-%include "twaalgos/dupexp.hh"
+%include "twaalgos/copy.hh"
 %include "twaalgos/emptiness.hh"
 %include "twaalgos/gtec/gtec.hh"
 %include "twaalgos/lbtt.hh"