mcrl2::lps::constelm_algorithm

Include file:

#include "mcrl2/lps/constelm.h

class mcrl2::lps::constelm_algorithm

Algorithm class for elimination of constant parameters.

Private types

type mcrl2::lps::constelm_algorithm::super

typedef for lps::detail::lps_algorithm< Specification >

Protected attributes

bool mcrl2::lps::constelm_algorithm::m_ignore_conditions

If true, conditions are not evaluated and assumed to be true.

std::map<data::variable, std::size_t> mcrl2::lps::constelm_algorithm::m_index_of

Maps process parameters to their index.

bool mcrl2::lps::constelm_algorithm::m_instantiate_global_variables

If true, then the algorithm is allowed to instantiate free variables as a side effect.

const DataRewriter &mcrl2::lps::constelm_algorithm::R

The rewriter used by the constelm algorithm.

Protected member functions

bool is_constant(const data::data_expression &x, const std::set<data::variable> &global_variables) const

void LOG_CONDITION(const data::data_expression &cond, const data::data_expression &c_i, const data::mutable_map_substitution<> &sigma, const std::string &msg = "")

void LOG_CONSTANT_PARAMETERS(const data::mutable_map_substitution<> &sigma, const std::string &msg = "")

void LOG_PARAMETER_CHANGE(const data::data_expression &d_j, const data::data_expression &Rd_j, const data::data_expression &Rg_ij, const data::mutable_map_substitution<> &sigma, const std::string &msg = "")

Public member functions

data::mutable_map_substitution compute_constant_parameters(bool instantiate_global_variables = false, bool ignore_conditions = false)

Computes constant parameters.

Parameters:

• instantiate_global_variables If true, the algorithm is allowed to instantiate free variables as a side effect
• ignore_conditions If true, the algorithm is allowed to ignore the conditions in the LPS.

constelm_algorithm(Specification &spec, const DataRewriter &R_)

Constructor.

void remove_parameters(data::mutable_map_substitution<> &sigma)

Applies the substitution computed by compute_constant_parameters.

void run(bool instantiate_global_variables = false, bool ignore_conditions = false)

Runs the constelm algorithm.

Parameters:

• instantiate_global_variables If true, the algorithm is allowed to instantiate free variables as a side effect
• ignore_conditions If true, the algorithm is allowed to ignore the conditions in the LPS.