Include file:

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

Algorithm class for the parelm algorithm.

Protected types

type edge_descriptor

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

The edge type of the dependency graph.

type graph

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

The graph type of the dependency graph.

type vertex_descriptor

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

The vertex type of the dependency graph.

Protected member functions

core::identifier_string find_predicate_variable(const pbes &p, std::size_t index) const

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

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

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

int variable_index(const data::variable_list &variables, const data::variable &d) const

Finds the index of a variable in a sequence.


  • variables A sequence of data variables
  • d A data variable

Returns: The index of d in v, or -1 if the variable wasn’t found

Public member functions

void run(pbes &p) const

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


  • p A pbes