From 4903f086e3a873c01a3f4807c612cfb8b5fa694d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 23 Nov 2016 21:08:11 +0100 Subject: [PATCH] graph: replace the existing "alternating" interface * spot/graph/graph.hh: Use the sign bit of destination state X to designate a universal edge. Store the destinations of such an edge in a separate array, at index ~X. * spot/graph/ngraph.hh, tests/core/graph.cc, tests/core/graph.test, tests/core/ngraph.cc: Adjust test case to the new interface. --- spot/graph/graph.hh | 159 ++++++++++++++++++++++++++++++++++++------ spot/graph/ngraph.hh | 28 ++++---- tests/core/graph.cc | 29 ++++---- tests/core/graph.test | 15 +++- tests/core/ngraph.cc | 24 +++---- 5 files changed, 188 insertions(+), 67 deletions(-) diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index 28df515d7..88a3b7feb 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -31,7 +31,7 @@ namespace spot { - template + template class SPOT_API digraph; namespace internal @@ -529,6 +529,33 @@ namespace spot } }; + class SPOT_API const_universal_dests + { + private: + const unsigned* begin_; + const unsigned* end_; + unsigned tmp_; + public: + const_universal_dests(const unsigned* begin, const unsigned* end) noexcept + : begin_(begin), end_(end) + { + } + + const_universal_dests(unsigned state) noexcept + : begin_(&tmp_), end_(&tmp_ + 1), tmp_(state) + { + } + + const unsigned* begin() const + { + return begin_; + } + + const unsigned* end() const + { + return end_; + } + }; } // namespace internal @@ -536,8 +563,7 @@ namespace spot /// /// \tparam State_Data data to attach to states /// \tparam Edge_Data data to attach to edges - /// \tparam Alternating whether the automaton should be alternating - template + template class digraph { friend class internal::edge_iterator; @@ -548,12 +574,6 @@ namespace spot typedef internal::edge_iterator iterator; typedef internal::edge_iterator const_iterator; - /// Whether the automaton is alternating - static constexpr bool alternating() - { - return Alternating; - } - // Extra data to store on each state or edge. typedef State_Data state_data_t; typedef Edge_Data edge_data_t; @@ -563,23 +583,23 @@ namespace spot typedef unsigned state; typedef unsigned edge; - // The type of an output state (when seen from a edge) - // depends on the kind of graph we build - typedef typename std::conditional, - state>::type out_state; - typedef internal::distate_storage> state_storage_t; - typedef internal::edge_storage> + typedef internal::edge_storage> edge_storage_t; typedef std::vector state_vector; typedef std::vector edge_vector_t; + + // A sequence of universal destination groups of the form: + // (n state_1 state_2 ... state_n)* + typedef std::vector dests_vector_t; + protected: state_vector states_; edge_vector_t edges_; + dests_vector_t dests_; // Only used by alternating automata. // Number of erased edges. unsigned killed_edge_; public: @@ -617,6 +637,12 @@ namespace spot return edges_.size() - killed_edge_ - 1; } + /// Whether the automaton is alternating + bool is_alternating() const + { + return !dests_.empty(); + } + /// \brief Create a new states /// /// All arguments are forwarded to the State_Data constructor. @@ -725,7 +751,7 @@ namespace spot /// \param args arguments to forward to the Edge_Data constructor template edge - new_edge(state src, out_state dst, Args&&... args) + new_edge(state src, state dst, Args&&... args) { edge t = edges_.size(); edges_.emplace_back(dst, 0, src, std::forward(args)...); @@ -740,6 +766,61 @@ namespace spot return t; } + /// \brief Create a new universal edge + /// + /// \param src the source state + /// \param dst_begin start of a non-empty container of destination states + /// \param dst_end end of a non-empty container of destination states + /// \param args arguments to forward to the Edge_Data constructor + template + edge + new_univ_edge(state src, I dst_begin, I dst_end, Args&&... args) + { + unsigned sz = std::distance(dst_begin, dst_end); + if (sz == 1) + return new_edge(src, *dst_begin, std::forward(args)...); + SPOT_ASSERT(sz > 1); + unsigned d = dests_.size(); + dests_.emplace_back(sz); + dests_.insert(dests_.end(), dst_begin, dst_end); + return new_edge(src, ~d, std::forward(args)...); + } + + /// \brief Create a new universal edge + /// + /// \param src the source state + /// \param dsts a non-empty list of destination states + /// \param args arguments to forward to the Edge_Data constructor + template + edge + new_univ_edge(state src, const std::initializer_list& dsts, + Args&&... args) + { + return new_univ_edge(src, dsts.begin(), dsts.end(), + std::forward(args)...); + } + + internal::const_universal_dests univ_dests(state src) const + { + if ((int)src < 0) + { + unsigned pos = ~src; + const unsigned* d = dests_.data(); + d += pos; + unsigned num = *d; + return { d + 1, d + num + 1 }; + } + else + { + return src; + } + } + + internal::const_universal_dests univ_dests(const edge_storage_t& e) const + { + return univ_dests(e.dst); + } + /// Convert a storage reference into a state number state index_of_state(const state_storage_t& ss) const { @@ -875,6 +956,21 @@ namespace spot } /// @} + /// @{ + /// \brief The vector used to store universal destinations. + /// + /// The actual way those destinations are stored is an + /// implementation detail you should not rely on. + const dests_vector_t& dests_vector() const + { + return dests_; + } + + dests_vector_t& dests_vector() + { + return dests_; + } + /// @} /// Dump the state and edge storage for debugging void dump_storage(std::ostream& o) const @@ -883,9 +979,13 @@ namespace spot for (unsigned t = 1; t < tend; ++t) { o << 't' << t << ": (s" - << edges_[t].src << ", s" - << edges_[t].dst << ") t" - << edges_[t].next_succ << '\n'; + << edges_[t].src << ", "; + int d = edges_[t].dst; + if (d < 0) + o << 'd' << ~d; + else + o << 's' << d; + o << ") t" << edges_[t].next_succ << '\n'; } unsigned send = states_.size(); for (unsigned s = 0; s < send; ++s) @@ -894,6 +994,23 @@ namespace spot << states_[s].succ << " t" << states_[s].succ_tail << '\n'; } + unsigned dend = dests_.size(); + unsigned size = 0; + for (unsigned s = 0; s < dend; ++s) + { + o << 'd' << s << ": "; + if (size == 0) + { + o << '#'; + size = dests_[s]; + } + else + { + o << 's'; + --size; + } + o << dests_[s] << '\n'; + } } /// \brief Remove all dead edges. diff --git a/spot/graph/ngraph.hh b/spot/graph/ngraph.hh index e579ecce1..0e883ad2b 100644 --- a/spot/graph/ngraph.hh +++ b/spot/graph/ngraph.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -137,27 +137,25 @@ namespace spot std::forward(args)...); } - template + template edge - new_edge(name src, const std::vector& dst, Args&&... args) + new_univ_edge(name src, I dst_begin, I dst_end, Args&&... args) { - std::vector d; - d.reserve(dst.size()); - for (auto n: dst) - d.emplace_back(get_state(n)); - return g_.new_edge(get_state(src), d, std::forward(args)...); + std::vector d; + d.reserve(std::distance(dst_begin, dst_end)); + while (dst_begin != dst_end) + d.emplace_back(get_state(*dst_begin++)); + return g_.new_univ_edge(get_state(src), d.begin(), d.end(), + std::forward(args)...); } template edge - new_edge(name src, - const std::initializer_list& dst, Args&&... args) + new_univ_edge(name src, + const std::initializer_list& dsts, Args&&... args) { - std::vector d; - d.reserve(dst.size()); - for (auto n: dst) - d.emplace_back(get_state(n)); - return g_.new_edge(get_state(src), d, std::forward(args)...); + return new_univ_edge(src, dsts.begin(), dsts.end(), + std::forward(args)...); } }; } diff --git a/tests/core/graph.cc b/tests/core/graph.cc index c8e41d2a8..1de3b6481 100644 --- a/tests/core/graph.cc +++ b/tests/core/graph.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -225,30 +225,29 @@ f6() f += t.first; h += t.second; } - return f == 3 && (h > 2.49 && h < 2.51); + return f == 3 && (h > 2.49 && h < 2.51) && !g.is_alternating(); } static bool f7() { - spot::digraph g(3); + spot::digraph g(3); auto s1 = g.new_state(2); auto s2 = g.new_state(3); auto s3 = g.new_state(4); - g.new_edge(s1, {s2, s3}, 1); - g.new_edge(s1, {s3}, 2); - g.new_edge(s2, {s3}, 3); - g.new_edge(s3, {s2}, 4); + g.new_univ_edge(s1, {s2, s3}, 1); + g.new_univ_edge(s1, {s3}, 2); + g.new_univ_edge(s2, {s3}, 3); + g.new_univ_edge(s3, {s2}, 4); int f = 0; for (auto& t: g.out(s1)) - { - for (auto& tt: t.dst) - { - f += t.label * g.state_data(tt); - } - } - return f == 15; + for (unsigned tt: g.univ_dests(t)) + f += t.label * g.state_data(tt); + + g.dump_storage(std::cout); + + return f == 15 && g.is_alternating(); } diff --git a/tests/core/graph.test b/tests/core/graph.test index ca1c199a8..425b47a09 100755 --- a/tests/core/graph.test +++ b/tests/core/graph.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2014, 2016 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -71,6 +71,16 @@ digraph { 2 [label="4"] 2 -> 1 [label="4"] } +t1: (s0, d0) t2 +t2: (s0, s2) t0 +t3: (s1, s2) t0 +t4: (s2, s1) t0 +s0: t1 t2 +s1: t3 t3 +s2: t4 t4 +d0: #2 +d1: s1 +d2: s2 digraph { 0 [label="(2,4)"] 0 -> 1 [label="(1,3)"] @@ -84,4 +94,3 @@ digraph { EOF diff stdout expected - diff --git a/tests/core/ngraph.cc b/tests/core/ngraph.cc index b7704b07f..69726398f 100644 --- a/tests/core/ngraph.cc +++ b/tests/core/ngraph.cc @@ -264,32 +264,30 @@ static bool f6() f += t.first; h += t.second; } - return f == 3 && (h > 2.49 && h < 2.51); + return f == 3 && (h > 2.49 && h < 2.51) && !g.is_alternating(); } static bool f7() { - typedef spot::digraph graph_t; + typedef spot::digraph graph_t; graph_t g(3); spot::named_graph gg(g); auto s1 = gg.new_state("s1", 2); gg.new_state("s2", 3); gg.new_state("s3", 4); - gg.new_edge("s1", {"s2", "s3"}, 1); - gg.new_edge("s1", {"s3"}, 2); - gg.new_edge("s2", {"s3"}, 3); - gg.new_edge("s3", {"s2"}, 4); + gg.new_univ_edge("s1", {"s2", "s3"}, 1); + // Standard edges can be used as well + gg.new_edge("s1", "s3", 2); + gg.new_univ_edge("s2", {"s3"}, 3); + gg.new_univ_edge("s3", {"s2"}, 4); int f = 0; for (auto& t: g.out(s1)) - { - for (auto& tt: t.dst) - { - f += t.label * g.state_data(tt); - } - } - return f == 15; + for (unsigned tt: g.univ_dests(t.dst)) + f += t.label * g.state_data(tt); + + return f == 15 && g.is_alternating(); }