Algorithm class for elimination of constant parameters. More...

#include <constelm.h>

Inheritance diagram for mcrl2::lps::constelm_algorithm< DataRewriter, Specification >:

Public Member Functions
	constelm_algorithm (Specification &spec, const DataRewriter &R_)
	Constructor.

data::mutable_map_substitution	compute_constant_parameters (bool instantiate_global_variables=false, bool ignore_conditions=false)
	Computes constant parameters.

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.

Public Member Functions inherited from mcrl2::lps::detail::lps_algorithm< Specification >
	lps_algorithm (Specification &spec)
	Constructor.

bool	verbose () const
	Flag for verbose output.

data::data_expression	next_state (const action_summand &s, const data::variable &v) const
	Applies the next state substitution to the variable v.

void	instantiate_free_variables ()
	Attempts to eliminate the free variables of the specification, by substituting a constant value for them. If no constant value is found for one of the variables, an exception is thrown.

void	remove_parameters (const std::set< data::variable > &to_be_removed)
	Removes formal parameters from the specification.

void	remove_singleton_sorts ()
	Removes parameters with a singleton sort.

void	remove_trivial_summands ()
	Removes summands with condition equal to false.

void	remove_unused_summand_variables ()
	Removes unused summand variables.

Protected Member Functions
void	LOG_CONSTANT_PARAMETERS (const data::mutable_map_substitution<> &sigma, const std::string &constant_removed_msg="", const std::string &nothing_removed_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="")

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

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

Protected Member Functions inherited from mcrl2::lps::detail::lps_algorithm< Specification >
void	sumelm_find_variables (const action_summand &s, std::set< data::variable > &result) const

void	sumelm_find_variables (const deadlock_summand &s, std::set< data::variable > &result) const

template<typename SummandType >
void	summand_remove_unused_summand_variables (SummandType &summand_)

Protected Attributes
bool	m_instantiate_global_variables = false
	If true, then the algorithm is allowed to instantiate free variables as a side effect.

bool	m_ignore_conditions = false
	If true, conditions are not evaluated and assumed to be true.

std::map< data::variable, std::size_t >	m_index_of
	Maps process parameters to their index.

const DataRewriter &	R
	The rewriter used by the constelm algorithm.

Protected Attributes inherited from mcrl2::lps::detail::lps_algorithm< Specification >
Specification &	m_spec
	The specification that is processed by the algorithm.

Private Types
using	super = typename lps::detail::lps_algorithm< Specification >

Detailed Description

template<typename DataRewriter, typename Specification = specification>
class mcrl2::lps::constelm_algorithm< DataRewriter, Specification >

Algorithm class for elimination of constant parameters.

Definition at line 22 of file constelm.h.

Member Typedef Documentation

◆ super

template<typename DataRewriter , typename Specification = specification>

using mcrl2::lps::constelm_algorithm< DataRewriter, Specification >::super = typename lps::detail::lps_algorithm<Specification>

private

Definition at line 24 of file constelm.h.

Constructor & Destructor Documentation

◆ constelm_algorithm()

template<typename DataRewriter , typename Specification = specification>

mcrl2::lps::constelm_algorithm< DataRewriter, Specification >::constelm_algorithm	(	Specification &	spec,
		const DataRewriter &	R_
	)

inline

Constructor.

Definition at line 113 of file constelm.h.

Member Function Documentation

◆ compute_constant_parameters()

template<typename DataRewriter , typename Specification = specification>

data::mutable_map_substitution mcrl2::lps::constelm_algorithm< DataRewriter, Specification >::compute_constant_parameters	(	bool	instantiate_global_variables = `false`,
		bool	ignore_conditions = `false`
	)

inline

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.

Definition at line 123 of file constelm.h.

◆ is_constant()

template<typename DataRewriter , typename Specification = specification>

bool mcrl2::lps::constelm_algorithm< DataRewriter, Specification >::is_constant	(	const data::data_expression &	x,
		const std::set< data::variable > &	global_variables
	)		const

inlineprotected

Definition at line 96 of file constelm.h.

◆ LOG_CONDITION()

template<typename DataRewriter , typename Specification = specification>

void mcrl2::lps::constelm_algorithm< DataRewriter, Specification >::LOG_CONDITION	(	const data::data_expression &	cond,
		const data::data_expression &	c_i,
		const data::mutable_map_substitution<> &	sigma,
		const std::string &	msg = `""`
	)

inlineprotected

Definition at line 78 of file constelm.h.

◆ LOG_CONSTANT_PARAMETERS()

template<typename DataRewriter , typename Specification = specification>

void mcrl2::lps::constelm_algorithm< DataRewriter, Specification >::LOG_CONSTANT_PARAMETERS	(	const data::mutable_map_substitution<> &	sigma,
		const std::string &	constant_removed_msg = `""`,
		const std::string &	nothing_removed_msg = `""`
	)

inlineprotected

Definition at line 40 of file constelm.h.

◆ LOG_PARAMETER_CHANGE()

template<typename DataRewriter , typename Specification = specification>

void mcrl2::lps::constelm_algorithm< DataRewriter, Specification >::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 = `""`
	)

inlineprotected

Definition at line 61 of file constelm.h.

◆ remove_parameters()

template<typename DataRewriter , typename Specification = specification>

void mcrl2::lps::constelm_algorithm< DataRewriter, Specification >::remove_parameters ( data::mutable_map_substitution<> & sigma )

inline

Applies the substitution computed by compute_constant_parameters.

Definition at line 232 of file constelm.h.

◆ run()

template<typename DataRewriter , typename Specification = specification>

void mcrl2::lps::constelm_algorithm< DataRewriter, Specification >::run	(	bool	instantiate_global_variables = `false`,
		bool	ignore_conditions = `false`
	)

inline

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.

Definition at line 257 of file constelm.h.

Member Data Documentation

◆ m_ignore_conditions

template<typename DataRewriter , typename Specification = specification>

bool mcrl2::lps::constelm_algorithm< DataRewriter, Specification >::m_ignore_conditions = false

protected

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

Definition at line 32 of file constelm.h.

◆ m_index_of

template<typename DataRewriter , typename Specification = specification>

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

protected

Maps process parameters to their index.

Definition at line 35 of file constelm.h.

◆ m_instantiate_global_variables

template<typename DataRewriter , typename Specification = specification>

bool mcrl2::lps::constelm_algorithm< DataRewriter, Specification >::m_instantiate_global_variables = false

protected

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

Definition at line 29 of file constelm.h.

◆ R

template<typename DataRewriter , typename Specification = specification>

const DataRewriter& mcrl2::lps::constelm_algorithm< DataRewriter, Specification >::R

protected

The rewriter used by the constelm algorithm.

Definition at line 38 of file constelm.h.

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

lps/include/mcrl2/lps/constelm.h

Public Member Functions

Protected Member Functions

Protected Attributes

Private Types

Detailed Description

Member Typedef Documentation

◆ super

Constructor & Destructor Documentation

◆ constelm_algorithm()

Member Function Documentation

◆ compute_constant_parameters()

◆ is_constant()

◆ LOG_CONDITION()

◆ LOG_CONSTANT_PARAMETERS()

◆ LOG_PARAMETER_CHANGE()

◆ remove_parameters()

◆ run()

Member Data Documentation

◆ m_ignore_conditions

◆ m_index_of

◆ m_instantiate_global_variables

◆ R