mCRL2
|
Class implementing the sum elimination lemma. More...
#include <sumelm.h>
Public Member Functions | |
sumelm_algorithm (Specification &spec, bool decluster=false) | |
Constructor. | |
void | run () |
Apply the sum elimination lemma to all summands in the specification. | |
template<class Summand > | |
void | operator() (Summand &s) |
Apply the sum elimination lemma to summand s. | |
std::size_t | removed () const |
Returns the amount of removed summation variables. | |
![]() | |
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 Attributes | |
std::size_t | m_removed |
Stores the number of summation variables that has been removed. | |
bool | m_decluster |
Whether to decluster disjunctive conditions first. | |
![]() | |
Specification & | m_spec |
The specification that is processed by the algorithm. | |
Private Types | |
typedef detail::lps_algorithm< Specification > | super |
Additional Inherited Members | |
![]() | |
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_) |
Class implementing the sum elimination lemma.
|
private |
|
inline |
|
inline |
Apply the sum elimination lemma to summand s.
s | an action_summand. |
|
inline |
|
inline |
|
protected |
|
protected |