Include file:

#include "mcrl2/pbes/parelm.h
class mcrl2::pbes_system::pbes_parelm_algorithm

Algorithm class for the parelm algorithm.

Protected types

type mcrl2::pbes_system::pbes_parelm_algorithm::edge_descriptor

typedef for boost::graph_traits< graph >::edge_descriptor

The edge type of the dependency graph.

type mcrl2::pbes_system::pbes_parelm_algorithm::graph

typedef for boost::adjacency_list< boost::setS, boost::vecS, boost::directedS >

The graph type of the dependency graph.

type mcrl2::pbes_system::pbes_parelm_algorithm::vertex_descriptor

typedef for boost::graph_traits< graph >::vertex_descriptor

The vertex type of the dependency graph.

Protected static member functions

static void compute_dependency_graph(const pbes &p, const std::map<core::identifier_string, std::size_t> &propvar_offsets, graph &G)
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.


  • p A pbes
  • index A positive number

Returns: The name of the predicate variable that corresponds with index

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

Finds unbound variables in a pbes expression.


  • t A PBES expression
  • bound_variables A sequence of data variables

Returns: The unbound variables in t that are not contained in bound_variables

Public member functions

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
void run(pbes &p)

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


  • p A pbes

Public static 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)