diff --git a/spot/twaalgos/copy.cc b/spot/twaalgos/copy.cc index 3ae73af12..9e9934e70 100644 --- a/spot/twaalgos/copy.cc +++ b/spot/twaalgos/copy.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2014, 2015 Laboratoire de Recherche +// Copyright (C) 2009, 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -22,73 +22,68 @@ #include #include -#include -#include -#include -#include -#include +#include namespace spot { - namespace - { - class copy_iter: public tgba_reachable_iterator_depth_first - { - public: - 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 - result() - { - return out_; - } - - virtual void - 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; - } - - virtual void - process_link(const state*, int in, - const state*, int out, - const twa_succ_iterator* si) - { - out_->new_edge - (in - 1, out - 1, si->cond(), - si->acc()); - } - - protected: - twa_graph_ptr out_; - std::vector* names_ = nullptr; - }; - - } // anonymous - twa_graph_ptr copy(const const_twa_ptr& aut, twa::prop_set p, bool preserve_names) { - copy_iter di(aut, p, preserve_names); - di.run(); - return di.result(); + twa_graph_ptr out = make_twa_graph(aut->get_dict()); + out->copy_acceptance_of(aut); + out->copy_ap_of(aut); + out->prop_copy(aut, p); + std::vector* names = nullptr; + if (preserve_names) + { + names = new std::vector; + out->set_named_prop("state-names", names); + } + + // States already seen. + state_map seen; + // States to process + std::deque::const_iterator> todo; + + auto new_state = [&](const state* s) -> unsigned + { + auto p = seen.emplace(s, 0); + if (p.second) + { + p.first->second = out->new_state(); + todo.push_back(p.first); + if (names) + names->push_back(aut->format_state(s)); + } + else + { + s->destroy(); + } + return p.first->second; + }; + + out->set_init_state(new_state(aut->get_init_state())); + while (!todo.empty()) + { + const state* src1; + unsigned src2; + std::tie(src1, src2) = *todo.front(); + todo.pop_front(); + + for (auto* t: aut->succ(src1)) + out->new_edge(src2, new_state(t->dst()), t->cond(), t->acc()); + } + + + auto s = seen.begin(); + while (s != seen.end()) + { + // Advance the iterator before deleting the "key" pointer. + const state* ptr = s->first; + ++s; + ptr->destroy(); + } + + return out; } } diff --git a/spot/twaalgos/copy.hh b/spot/twaalgos/copy.hh index ae453f38d..b4a6a0296 100644 --- a/spot/twaalgos/copy.hh +++ b/spot/twaalgos/copy.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -25,7 +25,6 @@ #include #include #include -#include namespace spot { @@ -34,6 +33,5 @@ namespace spot /// /// This works for using the abstract interface for automata SPOT_API twa_graph_ptr - copy(const const_twa_ptr& aut, twa::prop_set p, - bool preserve_names = false); + copy(const const_twa_ptr& aut, twa::prop_set p, bool preserve_names = false); } diff --git a/tests/python/ltsmin.ipynb b/tests/python/ltsmin.ipynb index ae61fb603..de6a7d238 100644 --- a/tests/python/ltsmin.ipynb +++ b/tests/python/ltsmin.ipynb @@ -1,7 +1,7 @@ { "metadata": { "name": "", - "signature": "sha256:f568358fc00acf6332b52560daa1a34f21cb30c73d81197ab7c5c015de11e12e" + "signature": "sha256:83724638edf025d8183ef0d5193234734b94f7e3470d9034bea411e730c834c6" }, "nbformat": 3, "nbformat_minor": 0, @@ -94,8 +94,8 @@ "prompt_number": 4, "text": [ "{'state_size': 3,\n", - " 'types': [('P', ['x']), ('int', [])],\n", - " 'variables': [('P', 0), ('P.a', 1), ('P.b', 1)]}" + " 'variables': [('P', 0), ('P.a', 1), ('P.b', 1)],\n", + " 'types': [('P', ['x']), ('int', [])]}" ] } ], @@ -149,214 +149,214 @@ "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", - "\n", - "12\n", + "\n", + "2\n", "\n", "P.a=0, P.b=1\n", "\n", - "\n", - "0->12\n", + "\n", + "0->2\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", - "\n", - "2\n", + "\n", + "3\n", "\n", "P.a=2, P.b=0\n", "\n", - "\n", - "1->2\n", + "\n", + "1->3\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", - "\n", - "9\n", + "\n", + "4\n", "\n", "P.a=1, P.b=1\n", "\n", - "\n", - "1->9\n", + "\n", + "1->4\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", - "\n", - "12->9\n", + "\n", + "2->4\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", - "\n", - "13\n", + "\n", + "5\n", "\n", "P.a=0, P.b=2\n", "\n", - "\n", - "12->13\n", + "\n", + "2->5\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", - "\n", - "3\n", + "\n", + "6\n", "\n", "P.a=3, P.b=0\n", "\n", - "\n", - "2->3\n", + "\n", + "3->6\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", - "\n", - "4\n", + "\n", + "7\n", "\n", "P.a=2, P.b=1\n", "\n", - "\n", - "2->4\n", + "\n", + "3->7\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", - "\n", - "9->4\n", + "\n", + "4->7\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", - "\n", - "10\n", + "\n", + "8\n", "\n", "P.a=1, P.b=2\n", "\n", - "\n", - "9->10\n", + "\n", + "4->8\n", "\n", "\n", "!"P.a<1" & !"P.b>2" & !dead\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!"P.a<1" & !"P.b>2" & dead\n", - "\n", - "\n", - "5\n", - "\n", - "P.a=3, P.b=1\n", - "\n", - "\n", - "4->5\n", - "\n", - "\n", - "!"P.a<1" & !"P.b>2" & !dead\n", - "\n", - "\n", - "6\n", - "\n", - "P.a=2, P.b=2\n", - "\n", - "\n", - "4->6\n", - "\n", - "\n", - "!"P.a<1" & !"P.b>2" & !dead\n", - "\n", - "\n", - "5->5\n", - "\n", - "\n", - "!"P.a<1" & !"P.b>2" & dead\n", - "\n", - "\n", - "7\n", - "\n", - "P.a=3, P.b=2\n", - "\n", - "\n", - "6->7\n", - "\n", - "\n", - "!"P.a<1" & !"P.b>2" & !dead\n", - "\n", - "\n", - "8\n", - "\n", - "P.a=2, P.b=3\n", - "\n", - "\n", - "6->8\n", - "\n", - "\n", - "!"P.a<1" & !"P.b>2" & !dead\n", - "\n", - "\n", - "7->7\n", - "\n", - "\n", - "!"P.a<1" & !"P.b>2" & dead\n", - "\n", - "\n", - "8->8\n", - "\n", - "\n", - "!"P.a<1" & "P.b>2" & dead\n", - "\n", - "\n", - "10->6\n", - "\n", - "\n", - "!"P.a<1" & !"P.b>2" & !dead\n", - "\n", - "\n", - "11\n", - "\n", - "P.a=1, P.b=3\n", - "\n", - "\n", - "10->11\n", - "\n", - "\n", - "!"P.a<1" & !"P.b>2" & !dead\n", - "\n", - "\n", - "11->11\n", - "\n", - "\n", - "!"P.a<1" & "P.b>2" & dead\n", - "\n", - "\n", - "13->10\n", + "\n", + "5->8\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", - "\n", - "14\n", + "\n", + "9\n", "\n", "P.a=0, P.b=3\n", "\n", - "\n", - "13->14\n", + "\n", + "5->9\n", "\n", "\n", ""P.a<1" & !"P.b>2" & !dead\n", "\n", - "\n", - "14->14\n", + "\n", + "6->6\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & dead\n", + "\n", + "\n", + "10\n", + "\n", + "P.a=3, P.b=1\n", + "\n", + "\n", + "7->10\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "11\n", + "\n", + "P.a=2, P.b=2\n", + "\n", + "\n", + "7->11\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "8->11\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "12\n", + "\n", + "P.a=1, P.b=3\n", + "\n", + "\n", + "8->12\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "9->9\n", "\n", "\n", ""P.a<1" & "P.b>2" & dead\n", "\n", + "\n", + "10->10\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & dead\n", + "\n", + "\n", + "13\n", + "\n", + "P.a=3, P.b=2\n", + "\n", + "\n", + "11->13\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "14\n", + "\n", + "P.a=2, P.b=3\n", + "\n", + "\n", + "11->14\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & !dead\n", + "\n", + "\n", + "12->12\n", + "\n", + "\n", + "!"P.a<1" & "P.b>2" & dead\n", + "\n", + "\n", + "13->13\n", + "\n", + "\n", + "!"P.a<1" & !"P.b>2" & dead\n", + "\n", + "\n", + "14->14\n", + "\n", + "\n", + "!"P.a<1" & "P.b>2" & dead\n", + "\n", "\n", "\n" ], "text": [ - " *' at 0x7f54f809d9c0> >" + " *' at 0x7f95344639c0> >" ] } ], @@ -426,7 +426,7 @@ "\n" ], "text": [ - " *' at 0x7f54f809dde0> >" + " *' at 0x7f9534463de0> >" ] } ], @@ -556,7 +556,7 @@ "\n" ], "text": [ - " *' at 0x7f54f809d7e0> >" + " *' at 0x7f95344637e0> >" ] } ],