mCRL2
Loading...
Searching...
No Matches
mcrl2::lps::constelm_algorithm< DataRewriter, Specification > Class Template Reference

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

#include <constelm.h>

Inheritance diagram for mcrl2::lps::constelm_algorithm< DataRewriter, Specification >:
mcrl2::lps::detail::lps_algorithm< 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
 If true, then the algorithm is allowed to instantiate free variables as a side effect.
 
bool m_ignore_conditions
 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

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

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 25 of file constelm.h.

Member Typedef Documentation

◆ super

template<typename DataRewriter , typename Specification = specification>
typedef lps::detail::lps_algorithm<Specification> mcrl2::lps::constelm_algorithm< DataRewriter, Specification >::super
private

Definition at line 27 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 114 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_variablesIf true, the algorithm is allowed to instantiate free variables as a side effect
ignore_conditionsIf true, the algorithm is allowed to ignore the conditions in the LPS.

Definition at line 125 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 97 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 79 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 43 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 62 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 234 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_variablesIf true, the algorithm is allowed to instantiate free variables as a side effect
ignore_conditionsIf true, the algorithm is allowed to ignore the conditions in the LPS.

Definition at line 259 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
protected

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

Definition at line 35 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 38 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
protected

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

Definition at line 32 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 41 of file constelm.h.


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