12#ifndef MCRL2_PBES_STRUCTURE_GRAPH_H
13#define MCRL2_PBES_STRUCTURE_GRAPH_H
16#include <boost/dynamic_bitset.hpp>
17#include <boost/range/adaptor/filtered.hpp>
25namespace pbes_system {
29struct structure_graph_builder;
30struct manual_structure_graph_builder;
37 return std::numeric_limits<unsigned int>::max();
72 std::vector<index_type> pred_ = std::vector<index_type>(),
73 std::vector<index_type> succ_ = std::vector<index_type>(),
145 std::size_t i = &v - &
static_cast<const vertex&
>(
vertices.front());
194 boost::filtered_range<vertices_not_contained_in, const vertex_vector>
vertices()
const
224 const boost::dynamic_bitset<>&
exclude()
const
252template <
typename StructureGraph>
255 std::vector<typename StructureGraph::index_type> result;
256 for (
auto v: G.predecessors(u))
263template <
typename StructureGraph>
266 std::vector<typename StructureGraph::index_type> result;
267 for (
auto v: G.successors(u))
283 default : { out <<
"none";
break; }
291 out <<
"vertex(formula = " << u.
formula()
301template <
typename StructureGraph>
304 auto N = G.all_vertices().size();
305 for (std::size_t i = 0; i < N; i++)
310 out << std::setw(4) << i <<
" "
311 <<
"vertex(formula = " << u.
formula()
323 out <<
" empty" << std::endl;
Base class that should not be used.
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)
index_type initial_vertex() const
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
boost::dynamic_bitset m_exclude
const std::vector< index_type > & all_predecessors(index_type u) const
std::size_t extent() const
const boost::dynamic_bitset & exclude() const
structure_graph()=default
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
index_type m_initial_vertex
vertex & find_vertex(index_type u)
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'.
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...
bool operator()(index_type i) const
integers_not_contained_in(const boost::dynamic_bitset<> &subset_)
const boost::dynamic_bitset & subset
void remove_predecessor(index_type u)
std::vector< index_type > successors
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())
decoration_type decoration
const pbes_expression & formula() const
std::vector< index_type > predecessors
void mark(atermpp::term_mark_stack &todo) const
void remove_successor(index_type u)
const boost::dynamic_bitset & subset
vertices_not_contained_in(const vertex_vector &vertices_, const boost::dynamic_bitset<> &subset_)
const vertex_vector & vertices
bool operator()(const vertex &v) const