mCRL2
|
Algorithm class for elimination of constant parameters. More...
#include <constelm.h>
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. | |
![]() | |
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 ¬hing_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 |
![]() | |
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. | |
![]() | |
Specification & | m_spec |
The specification that is processed by the algorithm. | |
Private Types | |
typedef lps::detail::lps_algorithm< Specification > | super |
Algorithm class for elimination of constant parameters.
Definition at line 25 of file constelm.h.
|
private |
Definition at line 27 of file constelm.h.
|
inline |
Constructor.
Definition at line 114 of file constelm.h.
|
inline |
Computes constant 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 125 of file constelm.h.
|
inlineprotected |
Definition at line 97 of file constelm.h.
|
inlineprotected |
Definition at line 79 of file constelm.h.
|
inlineprotected |
Definition at line 43 of file constelm.h.
|
inlineprotected |
Definition at line 62 of file constelm.h.
|
inline |
Applies the substitution computed by compute_constant_parameters.
Definition at line 234 of file constelm.h.
|
inline |
Runs the constelm algorithm.
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 259 of file constelm.h.
|
protected |
If true, conditions are not evaluated and assumed to be true.
Definition at line 35 of file constelm.h.
|
protected |
Maps process parameters to their index.
Definition at line 38 of file constelm.h.
|
protected |
If true, then the algorithm is allowed to instantiate free variables as a side effect.
Definition at line 32 of file constelm.h.
|
protected |
The rewriter used by the constelm algorithm.
Definition at line 41 of file constelm.h.