mCRL2
Loading...
Searching...
No Matches
Classes | Public Types | Public Member Functions | Protected Attributes | Friends | List of all members
mcrl2::pbes_system::structure_graph Class Reference

#include <structure_graph.h>

Classes

struct  integers_not_contained_in
 
struct  vertex
 
struct  vertices_not_contained_in
 

Public Types

enum  decoration_type {
  d_disjunction = 0 , d_conjunction = 1 , d_true , d_false ,
  d_none
}
 
using index_type = unsigned int
 
using vertex_vector = atermpp::vector< vertex, std::allocator< atermpp::detail::reference_aterm< vertex > >, mcrl2::utilities::detail::GlobalThreadSafe >
 

Public Member Functions

 structure_graph ()=default
 
 structure_graph (vertex_vector vertices, index_type initial_vertex, boost::dynamic_bitset<> exclude)
 
index_type initial_vertex () const
 
std::size_t extent () const
 
decoration_type decoration (index_type u) const
 
std::size_t rank (index_type u) const
 
const vertex_vector & all_vertices () const
 
const std::vector< index_type > & all_predecessors (index_type u) const
 
const std::vector< index_type > & all_successors (index_type u) const
 
boost::filtered_range< vertices_not_contained_in, const vertex_vector > vertices () const
 
boost::filtered_range< integers_not_contained_in, const std::vector< index_type > > predecessors (index_type u) const
 
boost::filtered_range< integers_not_contained_in, const std::vector< index_type > > successors (index_type u) const
 
index_type strategy (index_type u) const
 
vertex & find_vertex (index_type u)
 
const vertex & find_vertex (index_type u) const
 
const boost::dynamic_bitset & exclude () const
 
boost::dynamic_bitset & exclude ()
 
bool contains (index_type u) const
 
bool is_empty () const
 
bool is_defined () const
 

Protected Attributes

vertex_vector m_vertices
 
index_type m_initial_vertex = 0
 
boost::dynamic_bitset m_exclude
 

Friends

struct detail::structure_graph_builder
 
struct detail::manual_structure_graph_builder
 

Detailed Description

Definition at line 42 of file structure_graph.h.

Member Typedef Documentation

◆ index_type

using mcrl2::pbes_system::structure_graph::index_type = unsigned int

Definition at line 58 of file structure_graph.h.

◆ vertex_vector

using mcrl2::pbes_system::structure_graph::vertex_vector = atermpp::vector<vertex, std::allocator<atermpp::detail::reference_aterm<vertex> >, mcrl2::utilities::detail::GlobalThreadSafe>

Definition at line 112 of file structure_graph.h.

Member Enumeration Documentation

◆ decoration_type

enum mcrl2::pbes_system::structure_graph::decoration_type
Enumerator
d_disjunction 
d_conjunction 
d_true 
d_false 
d_none 

Definition at line 49 of file structure_graph.h.

Constructor & Destructor Documentation

◆ structure_graph() [1/2]

mcrl2::pbes_system::structure_graph::structure_graph ( )
default

◆ structure_graph() [2/2]

mcrl2::pbes_system::structure_graph::structure_graph ( vertex_vector  vertices,
index_type  initial_vertex,
boost::dynamic_bitset<>  exclude 
)
inline

Definition at line 153 of file structure_graph.h.

Member Function Documentation

◆ all_predecessors()

const std::vector< index_type > & mcrl2::pbes_system::structure_graph::all_predecessors ( index_type  u) const
inline

Definition at line 184 of file structure_graph.h.

◆ all_successors()

const std::vector< index_type > & mcrl2::pbes_system::structure_graph::all_successors ( index_type  u) const
inline

Definition at line 189 of file structure_graph.h.

◆ all_vertices()

const vertex_vector & mcrl2::pbes_system::structure_graph::all_vertices ( ) const
inline

Definition at line 179 of file structure_graph.h.

◆ contains()

bool mcrl2::pbes_system::structure_graph::contains ( index_type  u) const
inline

Definition at line 234 of file structure_graph.h.

◆ decoration()

decoration_type mcrl2::pbes_system::structure_graph::decoration ( index_type  u) const
inline

Definition at line 169 of file structure_graph.h.

◆ exclude() [1/2]

boost::dynamic_bitset & mcrl2::pbes_system::structure_graph::exclude ( )
inline

Definition at line 229 of file structure_graph.h.

◆ exclude() [2/2]

const boost::dynamic_bitset & mcrl2::pbes_system::structure_graph::exclude ( ) const
inline

Definition at line 224 of file structure_graph.h.

◆ extent()

std::size_t mcrl2::pbes_system::structure_graph::extent ( ) const
inline

Definition at line 164 of file structure_graph.h.

◆ find_vertex() [1/2]

vertex & mcrl2::pbes_system::structure_graph::find_vertex ( index_type  u)
inline

Definition at line 214 of file structure_graph.h.

◆ find_vertex() [2/2]

const vertex & mcrl2::pbes_system::structure_graph::find_vertex ( index_type  u) const
inline

Definition at line 219 of file structure_graph.h.

◆ initial_vertex()

index_type mcrl2::pbes_system::structure_graph::initial_vertex ( ) const
inline

Definition at line 159 of file structure_graph.h.

◆ is_defined()

bool mcrl2::pbes_system::structure_graph::is_defined ( ) const
inline

Definition at line 246 of file structure_graph.h.

◆ is_empty()

bool mcrl2::pbes_system::structure_graph::is_empty ( ) const
inline

Definition at line 240 of file structure_graph.h.

◆ predecessors()

boost::filtered_range< integers_not_contained_in, const std::vector< index_type > > mcrl2::pbes_system::structure_graph::predecessors ( index_type  u) const
inline

Definition at line 199 of file structure_graph.h.

◆ rank()

std::size_t mcrl2::pbes_system::structure_graph::rank ( index_type  u) const
inline

Definition at line 174 of file structure_graph.h.

◆ strategy()

index_type mcrl2::pbes_system::structure_graph::strategy ( index_type  u) const
inline

Definition at line 209 of file structure_graph.h.

◆ successors()

boost::filtered_range< integers_not_contained_in, const std::vector< index_type > > mcrl2::pbes_system::structure_graph::successors ( index_type  u) const
inline

Definition at line 204 of file structure_graph.h.

◆ vertices()

boost::filtered_range< vertices_not_contained_in, const vertex_vector > mcrl2::pbes_system::structure_graph::vertices ( ) const
inline

Definition at line 194 of file structure_graph.h.

Friends And Related Symbol Documentation

◆ detail::manual_structure_graph_builder

friend struct detail::manual_structure_graph_builder
friend

Definition at line 45 of file structure_graph.h.

◆ detail::structure_graph_builder

friend struct detail::structure_graph_builder
friend

Definition at line 44 of file structure_graph.h.

Member Data Documentation

◆ m_exclude

boost::dynamic_bitset mcrl2::pbes_system::structure_graph::m_exclude
protected

Definition at line 117 of file structure_graph.h.

◆ m_initial_vertex

index_type mcrl2::pbes_system::structure_graph::m_initial_vertex = 0
protected

Definition at line 116 of file structure_graph.h.

◆ m_vertices

vertex_vector mcrl2::pbes_system::structure_graph::m_vertices
protected

Definition at line 115 of file structure_graph.h.

The documentation for this class was generated from the following file: