mCRL2
Loading...
Searching...
No Matches
structure_graph.h
Go to the documentation of this file.
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//
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
21#include "mcrl2/pbes/pbes.h"
22
23namespace mcrl2 {
24
25namespace pbes_system {
26
27namespace detail {
28
29struct structure_graph_builder;
30struct manual_structure_graph_builder;
31
32} // namespace detail
33
34constexpr inline
35unsigned int undefined_vertex()
36{
37 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.
43{
46
47
48 public:
50 {
55 d_none
56 };
57
58 using index_type = unsigned int;
59
60 struct vertex
61 {
64 std::size_t rank;
65 std::vector<index_type> predecessors;
66 std::vector<index_type> successors;
68
69 explicit vertex(pbes_expression formula_,
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 : m_formula(std::move(formula_)),
77 decoration(decoration_),
78 rank(rank_),
79 predecessors(std::move(pred_)),
80 successors(std::move(succ_)),
81 strategy(strategy_)
82 {}
83
85 {
86 predecessors.erase(std::remove(predecessors.begin(), predecessors.end(), u), predecessors.end());
87 }
88
89 // Downcast reference aterm
90 inline const pbes_expression& formula() const
91 {
92 return m_formula;
93 }
94
96 {
97 successors.erase(std::remove(successors.begin(), successors.end(), u), successors.end());
98 }
99
100 bool is_defined() const
101 {
103 && (!successors.empty() || (decoration == d_true || decoration == d_false));
104 }
105
106 void inline mark(atermpp::term_mark_stack& todo) const
107 {
108 mark_term(m_formula, todo);
109 }
110 };
111
113
114 protected:
117 boost::dynamic_bitset<> m_exclude;
118
120 {
121 const boost::dynamic_bitset<>& subset;
122
123 explicit integers_not_contained_in(const boost::dynamic_bitset<>& subset_)
124 : subset(subset_)
125 {}
126
127 bool operator()(index_type i) const
128 {
129 return !subset[i];
130 }
131 };
132
134 {
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 structure_graph() = default;
152
154 : m_vertices(std::move(vertices)),
156 m_exclude(std::move(exclude))
157 {}
158
160 {
161 return m_initial_vertex;
162 }
163
164 std::size_t extent() const
165 {
166 return m_vertices.size();
167 }
168
170 {
171 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
180 {
181 return m_vertices;
182 }
183
184 const std::vector<index_type>& all_predecessors(index_type u) const
185 {
186 return find_vertex(u).predecessors;
187 }
188
189 const std::vector<index_type>& all_successors(index_type u) const
190 {
191 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 boost::filtered_range<integers_not_contained_in, const std::vector<index_type>> predecessors(index_type u) const
200 {
201 return all_predecessors(u) | boost::adaptors::filtered(integers_not_contained_in(m_exclude));
202 }
203
204 boost::filtered_range<integers_not_contained_in, const std::vector<index_type>> successors(index_type u) const
205 {
206 return all_successors(u) | boost::adaptors::filtered(integers_not_contained_in(m_exclude));
207 }
208
210 {
211 return find_vertex(u).strategy;
212 }
213
215 {
216 return m_vertices[u];
217 }
218
220 {
221 return m_vertices[u];
222 }
223
224 const boost::dynamic_bitset<>& exclude() const
225 {
226 return m_exclude;
227 }
228
229 boost::dynamic_bitset<>& exclude()
230 {
231 return m_exclude;
232 }
233
234 bool contains(index_type u) const
235 {
236 return !m_exclude[u];
237 }
238
239 // TODO: avoid this linear time check
240 bool is_empty() const
241 {
242 return m_exclude.all();
243 }
244
245 // Returns true if all vertices have a rank and a decoration
246 bool is_defined() const
247 {
248 return std::all_of(m_vertices.begin(), m_vertices.end(), [](const vertex& u) { return u.is_defined(); });
249 }
250};
251
252template <typename StructureGraph>
253std::vector<typename StructureGraph::index_type> structure_graph_predecessors(const StructureGraph& G, typename StructureGraph::index_type u)
254{
255 std::vector<typename StructureGraph::index_type> result;
256 for (auto v: G.predecessors(u))
257 {
258 result.push_back(v);
259 }
260 return result;
261}
262
263template <typename StructureGraph>
264std::vector<typename StructureGraph::index_type> structure_graph_successors(const StructureGraph& G, typename StructureGraph::index_type u)
265{
266 std::vector<typename StructureGraph::index_type> result;
267 for (auto v: G.successors(u))
268 {
269 result.push_back(v);
270 }
271 return result;
272}
273
274inline
275std::ostream& operator<<(std::ostream& out, const structure_graph::decoration_type& decoration)
276{
277 switch (decoration)
278 {
279 case structure_graph::d_conjunction : { out << "conjunction"; break; }
280 case structure_graph::d_disjunction : { out << "disjunction"; break; }
281 case structure_graph::d_true : { out << "true"; break; }
282 case structure_graph::d_false : { out << "false"; break; }
283 default : { out << "none"; break; }
284 }
285 return out;
286}
287
288inline
289std::ostream& operator<<(std::ostream& out, const structure_graph::vertex& u)
290{
291 out << "vertex(formula = " << u.formula()
292 << ", decoration = " << u.decoration
293 << ", rank = " << (u.rank == data::undefined_index() ? std::string("undefined") : std::to_string(u.rank))
294 << ", predecessors = " << core::detail::print_list(u.predecessors)
295 << ", successors = " << core::detail::print_list(u.successors)
296 << ", strategy = " << (u.strategy == undefined_vertex() ? std::string("undefined") : std::to_string(u.strategy))
297 << ")";
298 return out;
299}
300
301template <typename StructureGraph>
302std::ostream& print_structure_graph(std::ostream& out, const StructureGraph& G)
303{
304 auto N = G.all_vertices().size();
305 for (std::size_t i = 0; i < N; i++)
306 {
307 if (G.contains(i))
308 {
309 const structure_graph::vertex& u = G.find_vertex(i);
310 out << std::setw(4) << i << " "
311 << "vertex(formula = " << u.formula()
312 << ", decoration = " << u.decoration
313 << ", 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 << ", strategy = " << (u.strategy == undefined_vertex() ? std::string("undefined") : std::to_string(u.strategy))
317 << ")"
318 << std::endl;
319 }
320 }
321 if (G.is_empty())
322 {
323 out << " empty" << std::endl;
324 }
325 return out;
326}
327
328inline
329std::ostream& operator<<(std::ostream& out, const structure_graph& G)
330{
331 return print_structure_graph(out, G);
332}
333
334} // namespace pbes_system
335
336} // namespace mcrl2
337
338#endif // MCRL2_PBES_STRUCTURE_GRAPH_H
Base class that should not be used.
std::size_t size() const
Definition vector.h:329
boost::dynamic_bitset & exclude()
boost::filtered_range< vertices_not_contained_in, const vertex_vector > vertices() const
structure_graph(vertex_vector vertices, index_type initial_vertex, boost::dynamic_bitset<> exclude)
boost::filtered_range< integers_not_contained_in, const std::vector< index_type > > predecessors(index_type u) const
const std::vector< index_type > & all_successors(index_type u) const
const std::vector< index_type > & all_predecessors(index_type u) const
const boost::dynamic_bitset & exclude() const
const vertex_vector & all_vertices() const
boost::filtered_range< integers_not_contained_in, const std::vector< index_type > > successors(index_type u) const
const vertex & find_vertex(index_type u) const
bool contains(index_type u) const
std::size_t rank(index_type u) const
index_type strategy(index_type u) const
decoration_type decoration(index_type u) const
add your file description here.
std::stack< std::reference_wrapper< detail::_aterm > > term_mark_stack
std::string print_list(const Container &v, const std::string &message="", bool print_index=false, bool boundary_spaces=true)
Creates a string representation of a container.
constexpr std::size_t undefined_index()
Returns an index that corresponds to 'undefined'.
Definition undefined.h:27
std::vector< typename StructureGraph::index_type > structure_graph_successors(const StructureGraph &G, typename StructureGraph::index_type u)
constexpr unsigned int undefined_vertex()
std::vector< typename StructureGraph::index_type > structure_graph_predecessors(const StructureGraph &G, typename StructureGraph::index_type u)
std::ostream & print_structure_graph(std::ostream &out, const StructureGraph &G)
std::ostream & operator<<(std::ostream &os, const absinthe_strategy strategy)
static constexpr bool GlobalThreadSafe
Enables thread safety for the whole toolset.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.
The class pbes.
integers_not_contained_in(const boost::dynamic_bitset<> &subset_)
atermpp::detail::reference_aterm< pbes_expression > m_formula
vertex(pbes_expression formula_, decoration_type decoration_=structure_graph::d_none, std::size_t rank_=data::undefined_index(), std::vector< index_type > pred_=std::vector< index_type >(), std::vector< index_type > succ_=std::vector< index_type >(), index_type strategy_=undefined_vertex())
const pbes_expression & formula() const
void mark(atermpp::term_mark_stack &todo) const
vertices_not_contained_in(const vertex_vector &vertices_, const boost::dynamic_bitset<> &subset_)