mCRL2
|
Algorithm class for elimination of unused parameters from a linear process specification. More...
#include <parelm.h>
Public Member Functions | |
parelm_algorithm (Specification &spec) | |
Constructor. | |
void | run (bool variant1=true) |
Runs the parelm 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 | |
std::set< data::variable > | transition_variables () |
Returns the data variables that are considered in the parelm algorithm. | |
void | report_results (const std::set< data::variable > &to_be_removed) const |
void | parelm1 () |
First version of parelm1. | |
void | parelm2 () |
Second version of parelm that builds a dependency graph. | |
![]() | |
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 |
void | summand_remove_unused_summand_variables (SummandType &summand_) |
Private Types | |
typedef lps::detail::lps_algorithm< Specification > | super |
Additional Inherited Members | |
![]() | |
Specification & | m_spec |
The specification that is processed by the algorithm. | |
Algorithm class for elimination of unused parameters from a linear process specification.
|
private |
|
inline |
|
inlineprotected |
|
inlineprotected |
|
inlineprotected |
|
inline |
|
inlineprotected |