Line data Source code
1 : // Author(s): Wieger Wesselink
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/pbes/structure_graph.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_STRUCTURE_GRAPH_H
13 : #define MCRL2_PBES_STRUCTURE_GRAPH_H
14 :
15 : #include <iomanip>
16 : #include <boost/dynamic_bitset.hpp>
17 : #include <boost/range/adaptor/filtered.hpp>
18 :
19 : #include "mcrl2/atermpp/standard_containers/vector.h"
20 : #include "mcrl2/core/detail/print_utility.h"
21 : #include "mcrl2/pbes/pbes.h"
22 :
23 : namespace mcrl2 {
24 :
25 : namespace pbes_system {
26 :
27 : namespace detail {
28 :
29 : struct structure_graph_builder;
30 : struct manual_structure_graph_builder;
31 :
32 : } // namespace detail
33 :
34 : constexpr inline
35 6267 : unsigned int undefined_vertex()
36 : {
37 6267 : return std::numeric_limits<unsigned int>::max();
38 : }
39 :
40 : // A structure graph with a facility to exclude a subset of the vertices.
41 : // It has the same interface as simple_structure_graph.
42 : class structure_graph
43 : {
44 : friend struct detail::structure_graph_builder;
45 : friend struct detail::manual_structure_graph_builder;
46 :
47 :
48 : public:
49 : enum decoration_type
50 : {
51 : d_disjunction = 0,
52 : d_conjunction = 1,
53 : d_true,
54 : d_false,
55 : d_none
56 : };
57 :
58 : using index_type = unsigned int;
59 :
60 : struct vertex
61 : {
62 : atermpp::detail::reference_aterm<pbes_expression> m_formula;
63 : decoration_type decoration;
64 : std::size_t rank;
65 : std::vector<index_type> predecessors;
66 : std::vector<index_type> successors;
67 : mutable index_type strategy;
68 :
69 3776 : explicit vertex(pbes_expression formula_,
70 : decoration_type decoration_ = structure_graph::d_none,
71 : std::size_t rank_ = data::undefined_index(),
72 : std::vector<index_type> pred_ = std::vector<index_type>(),
73 : std::vector<index_type> succ_ = std::vector<index_type>(),
74 : index_type strategy_ = undefined_vertex()
75 : )
76 3776 : : m_formula(std::move(formula_)),
77 3776 : decoration(decoration_),
78 3776 : rank(rank_),
79 3776 : predecessors(std::move(pred_)),
80 3776 : successors(std::move(succ_)),
81 3776 : strategy(strategy_)
82 3776 : {}
83 :
84 : void remove_predecessor(index_type u)
85 : {
86 : predecessors.erase(std::remove(predecessors.begin(), predecessors.end(), u), predecessors.end());
87 : }
88 :
89 : // Downcast reference aterm
90 0 : inline pbes_expression formula() const
91 : {
92 0 : return m_formula;
93 : }
94 :
95 : void remove_successor(index_type u)
96 : {
97 : successors.erase(std::remove(successors.begin(), successors.end(), u), successors.end());
98 : }
99 :
100 3776 : bool is_defined() const
101 : {
102 1161 : return ((decoration != structure_graph::d_none) || (rank != data::undefined_index()))
103 4937 : && (!successors.empty() || (decoration == d_true || decoration == d_false));
104 : }
105 :
106 0 : void inline mark(atermpp::term_mark_stack& todo) const
107 : {
108 0 : mark_term(m_formula, todo);
109 0 : }
110 : };
111 :
112 : using vertex_vector = atermpp::vector<vertex, std::allocator<atermpp::detail::reference_aterm<vertex>>, mcrl2::utilities::detail::GlobalThreadSafe>;
113 :
114 : protected:
115 : vertex_vector m_vertices;
116 : index_type m_initial_vertex = 0;
117 : boost::dynamic_bitset<> m_exclude;
118 :
119 : struct integers_not_contained_in
120 : {
121 : const boost::dynamic_bitset<>& subset;
122 :
123 8244 : explicit integers_not_contained_in(const boost::dynamic_bitset<>& subset_)
124 8244 : : subset(subset_)
125 8244 : {}
126 :
127 11735 : bool operator()(index_type i) const
128 : {
129 11735 : return !subset[i];
130 : }
131 : };
132 :
133 : struct vertices_not_contained_in
134 : {
135 : const vertex_vector& vertices;
136 : const boost::dynamic_bitset<>& subset;
137 :
138 : vertices_not_contained_in(const vertex_vector& vertices_, const boost::dynamic_bitset<>& subset_)
139 : : vertices(vertices_),
140 : subset(subset_)
141 : {}
142 :
143 : bool operator()(const vertex& v) const
144 : {
145 : std::size_t i = &v - &static_cast<const vertex&>(vertices.front());
146 : return !subset[i];
147 : }
148 : };
149 :
150 : public:
151 133 : structure_graph() = default;
152 :
153 0 : structure_graph(vertex_vector vertices, index_type initial_vertex, boost::dynamic_bitset<> exclude)
154 0 : : m_vertices(std::move(vertices)),
155 0 : m_initial_vertex(initial_vertex),
156 0 : m_exclude(std::move(exclude))
157 0 : {}
158 :
159 209 : index_type initial_vertex() const
160 : {
161 209 : return m_initial_vertex;
162 : }
163 :
164 575 : std::size_t extent() const
165 : {
166 575 : return m_vertices.size();
167 : }
168 :
169 3072 : decoration_type decoration(index_type u) const
170 : {
171 3072 : return find_vertex(u).decoration;
172 : }
173 :
174 : std::size_t rank(index_type u) const
175 : {
176 : return find_vertex(u).rank;
177 : }
178 :
179 219 : const vertex_vector& all_vertices() const
180 : {
181 219 : return m_vertices;
182 : }
183 :
184 3791 : const std::vector<index_type>& all_predecessors(index_type u) const
185 : {
186 3791 : return find_vertex(u).predecessors;
187 : }
188 :
189 4453 : const std::vector<index_type>& all_successors(index_type u) const
190 : {
191 4453 : return find_vertex(u).successors;
192 : }
193 :
194 : boost::filtered_range<vertices_not_contained_in, const vertex_vector> vertices() const
195 : {
196 : return all_vertices() | boost::adaptors::filtered(vertices_not_contained_in(m_vertices, m_exclude));
197 : }
198 :
199 3791 : boost::filtered_range<integers_not_contained_in, const std::vector<index_type>> predecessors(index_type u) const
200 : {
201 7582 : return all_predecessors(u) | boost::adaptors::filtered(integers_not_contained_in(m_exclude));
202 : }
203 :
204 4453 : boost::filtered_range<integers_not_contained_in, const std::vector<index_type>> successors(index_type u) const
205 : {
206 8906 : return all_successors(u) | boost::adaptors::filtered(integers_not_contained_in(m_exclude));
207 : }
208 :
209 0 : index_type strategy(index_type u) const
210 : {
211 0 : return find_vertex(u).strategy;
212 : }
213 :
214 4476 : vertex& find_vertex(index_type u)
215 : {
216 4476 : return m_vertices[u];
217 : }
218 :
219 15370 : const vertex& find_vertex(index_type u) const
220 : {
221 15370 : return m_vertices[u];
222 : }
223 :
224 0 : const boost::dynamic_bitset<>& exclude() const
225 : {
226 0 : return m_exclude;
227 : }
228 :
229 479 : boost::dynamic_bitset<>& exclude()
230 : {
231 479 : return m_exclude;
232 : }
233 :
234 5796 : bool contains(index_type u) const
235 : {
236 5796 : return !m_exclude[u];
237 : }
238 :
239 : // TODO: avoid this linear time check
240 176 : bool is_empty() const
241 : {
242 176 : return m_exclude.all();
243 : }
244 :
245 : // Returns true if all vertices have a rank and a decoration
246 133 : bool is_defined() const
247 : {
248 3909 : return std::all_of(m_vertices.begin(), m_vertices.end(), [](const vertex& u) { return u.is_defined(); });
249 : }
250 : };
251 :
252 : template <typename StructureGraph>
253 0 : std::vector<typename StructureGraph::index_type> structure_graph_predecessors(const StructureGraph& G, typename StructureGraph::index_type u)
254 : {
255 0 : std::vector<typename StructureGraph::index_type> result;
256 0 : for (auto v: G.predecessors(u))
257 : {
258 0 : result.push_back(v);
259 : }
260 0 : return result;
261 0 : }
262 :
263 : template <typename StructureGraph>
264 0 : std::vector<typename StructureGraph::index_type> structure_graph_successors(const StructureGraph& G, typename StructureGraph::index_type u)
265 : {
266 0 : std::vector<typename StructureGraph::index_type> result;
267 0 : for (auto v: G.successors(u))
268 : {
269 0 : result.push_back(v);
270 : }
271 0 : return result;
272 0 : }
273 :
274 : inline
275 0 : std::ostream& operator<<(std::ostream& out, const structure_graph::decoration_type& decoration)
276 : {
277 0 : switch (decoration)
278 : {
279 0 : case structure_graph::d_conjunction : { out << "conjunction"; break; }
280 0 : case structure_graph::d_disjunction : { out << "disjunction"; break; }
281 0 : case structure_graph::d_true : { out << "true"; break; }
282 0 : case structure_graph::d_false : { out << "false"; break; }
283 0 : default : { out << "none"; break; }
284 : }
285 0 : return out;
286 : }
287 :
288 : inline
289 0 : std::ostream& operator<<(std::ostream& out, const structure_graph::vertex& u)
290 : {
291 0 : out << "vertex(formula = " << u.formula()
292 0 : << ", decoration = " << u.decoration
293 0 : << ", rank = " << (u.rank == data::undefined_index() ? std::string("undefined") : std::to_string(u.rank))
294 0 : << ", predecessors = " << core::detail::print_list(u.predecessors)
295 0 : << ", successors = " << core::detail::print_list(u.successors)
296 0 : << ", strategy = " << (u.strategy == undefined_vertex() ? std::string("undefined") : std::to_string(u.strategy))
297 0 : << ")";
298 0 : return out;
299 : }
300 :
301 : template <typename StructureGraph>
302 0 : std::ostream& print_structure_graph(std::ostream& out, const StructureGraph& G)
303 : {
304 0 : auto N = G.all_vertices().size();
305 0 : for (std::size_t i = 0; i < N; i++)
306 : {
307 0 : if (G.contains(i))
308 : {
309 0 : const structure_graph::vertex& u = G.find_vertex(i);
310 0 : out << std::setw(4) << i << " "
311 0 : << "vertex(formula = " << u.formula()
312 0 : << ", decoration = " << u.decoration
313 0 : << ", rank = " << (u.rank == data::undefined_index() ? std::string("undefined") : std::to_string(u.rank))
314 : << ", predecessors = " << core::detail::print_list(structure_graph_predecessors(G, i))
315 : << ", successors = " << core::detail::print_list(structure_graph_successors(G, i))
316 0 : << ", strategy = " << (u.strategy == undefined_vertex() ? std::string("undefined") : std::to_string(u.strategy))
317 0 : << ")"
318 0 : << std::endl;
319 : }
320 : }
321 0 : if (G.is_empty())
322 : {
323 0 : out << " empty" << std::endl;
324 : }
325 0 : return out;
326 : }
327 :
328 : inline
329 0 : std::ostream& operator<<(std::ostream& out, const structure_graph& G)
330 : {
331 0 : return print_structure_graph(out, G);
332 : }
333 :
334 : } // namespace pbes_system
335 :
336 : } // namespace mcrl2
337 :
338 : #endif // MCRL2_PBES_STRUCTURE_GRAPH_H
|