mcrl2::pbes_system::pbes_parelm_algorithm Class Reference

Algorithm class for the parelm algorithm. More...

#include <parelm.h>

Classes
struct	parelm_dependency_traverser

Public Member Functions
void	run (pbes &p, bool ignore_cex=false)
	Runs the parelm algorithm. The pbes is modified by the algorithm.
void	print_removed_parameters (const std::vector< data::variable > &predicate_variables, const std::map< core::identifier_string, std::size_t > &propvar_offsets, const std::map< core::identifier_string, std::vector< std::size_t > > &removals) const

Static Public Member Functions
static void	print_dependencies (const pbes &p, const std::vector< data::variable > &predicate_variables, const std::set< std::size_t > &significant_variables, const graph &G)

Protected Types
using	graph = boost::adjacency_list< boost::setS, boost::vecS, boost::directedS >
	The graph type of the dependency graph.
using	vertex_descriptor = boost::graph_traits< graph >::vertex_descriptor
	The vertex type of the dependency graph.
using	edge_descriptor = boost::graph_traits< graph >::edge_descriptor
	The edge type of the dependency graph.

Static Protected Member Functions
static std::set< data::variable >	unbound_variables (const pbes_expression &t, const data::variable_list &bound_variables)
	Finds unbound variables in a pbes expression.
static core::identifier_string	find_predicate_variable (const pbes &p, std::size_t index)
	Finds the predicate variable to which the data parameter with the given index belongs. Here index refers to the cumulative index in the array obtained by concatening all parameters of the predicate variables in the pbes p.
static void	compute_dependency_graph (const pbes &p, const std::map< core::identifier_string, std::size_t > &propvar_offsets, graph &G)

Detailed Description

Algorithm class for the parelm algorithm.

Definition at line 45 of file parelm.h.

Member Typedef Documentation

edge_descriptor

using mcrl2::pbes_system::pbes_parelm_algorithm::edge_descriptor = boost::graph_traits<graph>::edge_descriptor

protected

The edge type of the dependency graph.

Definition at line 55 of file parelm.h.

graph

using mcrl2::pbes_system::pbes_parelm_algorithm::graph = boost::adjacency_list<boost::setS, boost::vecS, boost::directedS>

protected

The graph type of the dependency graph.

Definition at line 49 of file parelm.h.

vertex_descriptor

using mcrl2::pbes_system::pbes_parelm_algorithm::vertex_descriptor = boost::graph_traits<graph>::vertex_descriptor

protected

The vertex type of the dependency graph.

Definition at line 52 of file parelm.h.

Member Function Documentation

compute_dependency_graph()

static void mcrl2::pbes_system::pbes_parelm_algorithm::compute_dependency_graph ( const pbes &  p, const std::map< core::identifier_string, std::size_t > &  propvar_offsets, graph &  G  )

inlinestaticprotected

Definition at line 172 of file parelm.h.

find_predicate_variable()

static core::identifier_string mcrl2::pbes_system::pbes_parelm_algorithm::find_predicate_variable ( const pbes &  p, std::size_t  index  )

inlinestaticprotected

Finds the predicate variable to which the data parameter with the given index belongs. Here index refers to the cumulative index in the array obtained by concatening all parameters of the predicate variables in the pbes p.

Parameters

p	A pbes
index	A positive number

Returns

The name of the predicate variable that corresponds with index

Definition at line 157 of file parelm.h.

print_dependencies()

static void mcrl2::pbes_system::pbes_parelm_algorithm::print_dependencies ( const pbes &  p, const std::vector< data::variable > &  predicate_variables, const std::set< std::size_t > &  significant_variables, const graph &  G  )

inlinestatic

Definition at line 301 of file parelm.h.

print_removed_parameters()

void mcrl2::pbes_system::pbes_parelm_algorithm::print_removed_parameters ( const std::vector< data::variable > &  predicate_variables, const std::map< core::identifier_string, std::size_t > &  propvar_offsets, const std::map< core::identifier_string, std::vector< std::size_t > > &  removals  ) const

inline

Definition at line 278 of file parelm.h.

run()

void mcrl2::pbes_system::pbes_parelm_algorithm::run ( pbes &  p, bool  ignore_cex = false  )

inline

Runs the parelm algorithm. The pbes is modified by the algorithm.

Parameters

p	A pbes
ignore_cex	Ignore counter example equations if present

Definition at line 185 of file parelm.h.

unbound_variables()

static std::set< data::variable > mcrl2::pbes_system::pbes_parelm_algorithm::unbound_variables ( const pbes_expression &  t, const data::variable_list &  bound_variables  )

inlinestaticprotected

Finds unbound variables in a pbes expression.

Parameters

t	A PBES expression
bound_variables	A sequence of data variables

Returns

The unbound variables in t that are not contained in bound_variables

Definition at line 145 of file parelm.h.

---

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

• pbes/include/mcrl2/pbes/parelm.h