diff --git a/NEWS b/NEWS index 95bacca2b..8572a9030 100644 --- a/NEWS +++ b/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 diff --git a/src/tests/dupexp.test b/src/tests/dupexp.test index 5b659cb97..e3730631c 100755 --- a/src/tests/dupexp.test +++ b/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 out9.txt grep 'states: 6$' out9.txt diff --git a/src/twa/twagraph.hh b/src/twa/twagraph.hh index 70dffbc17..9f20e9525 100644 --- a/src/twa/twagraph.hh +++ b/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 @@ -476,24 +476,24 @@ namespace spot } inline twa_graph_ptr make_twa_graph(const twa_graph_ptr& aut, - twa::prop_set p) + twa::prop_set p) { return std::make_shared(aut, p); } inline twa_graph_ptr make_twa_graph(const const_twa_graph_ptr& aut, - twa::prop_set p) + twa::prop_set p) { return std::make_shared(aut, p); } inline twa_graph_ptr make_twa_graph(const const_twa_ptr& aut, - twa::prop_set p) + twa::prop_set p) { auto a = std::dynamic_pointer_cast(aut); if (a) return std::make_shared(a, p); else - return tgba_dupexp_dfs(aut, p); + return copy(aut, p); } } diff --git a/src/twaalgos/Makefile.am b/src/twaalgos/Makefile.am index e6cc05fef..bf600ea36 100644 --- a/src/twaalgos/Makefile.am +++ b/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 \ diff --git a/src/twaalgos/dupexp.cc b/src/twaalgos/copy.cc similarity index 73% rename from src/twaalgos/dupexp.cc rename to src/twaalgos/copy.cc index 8236e517a..a1f4f1eea 100644 --- a/src/twaalgos/dupexp.cc +++ b/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 . -#include "dupexp.hh" +#include "copy.hh" #include "twa/twagraph.hh" #include #include @@ -32,16 +32,22 @@ namespace spot { namespace { - template - class dupexp_iter: public T + class copy_iter: public tgba_reachable_iterator_depth_first { public: - dupexp_iter(const const_twa_ptr& a, twa::prop_set p) - : T(a), out_(make_twa_graph(a->get_dict())) + copy_iter(const const_twa_ptr& a, twa::prop_set p, + 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; + 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(n) - 1); (void)ns; (void)n; @@ -71,22 +79,15 @@ namespace spot protected: twa_graph_ptr out_; + std::vector* 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 di(aut, p); - di.run(); - return di.result(); - } - - twa_graph_ptr - tgba_dupexp_dfs(const const_twa_ptr& aut, twa::prop_set p) - { - dupexp_iter di(aut, p); + copy_iter di(aut, p, preserve_names); di.run(); return di.result(); } diff --git a/src/twaalgos/dupexp.hh b/src/twaalgos/copy.hh similarity index 76% rename from src/twaalgos/dupexp.hh rename to src/twaalgos/copy.hh index ba5f5c5a6..16f8ada22 100644 --- a/src/twaalgos/dupexp.hh +++ b/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); - /// \ingroup twa_misc - /// \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); + copy(const const_twa_ptr& aut, twa::prop_set p, + bool preserve_names = false); } diff --git a/src/twaalgos/dot.cc b/src/twaalgos/dot.cc index 02053754b..a9cd9ed91 100644 --- a/src/twaalgos/dot.cc +++ b/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 #include @@ -534,7 +535,7 @@ namespace spot dotty_output d(os, options); auto aut = std::dynamic_pointer_cast(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; } diff --git a/src/twaalgos/stutter.cc b/src/twaalgos/stutter.cc index 1866b7105..c2cdf99b2 100644 --- a/src/twaalgos/stutter.cc +++ b/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" diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 56f79a676..890aee1d8 100644 --- a/wrap/python/spot_impl.i +++ b/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"