mCRL2
|
#include <suminst.h>
Public Member Functions | |
suminst_algorithm (Specification &spec, DataRewriter &r, std::set< data::sort_expression > sorts=std::set< data::sort_expression >(), bool tau_summands_only=false) | |
void | run () |
![]() | |
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 | |
template<typename SummandType , typename Container > | |
std::size_t | instantiate_summand (const SummandType &s, Container &result) |
bool | must_instantiate (const action_summand_type &summand) |
bool | must_instantiate (const deadlock_summand &) |
template<typename SummandListType , typename Container > | |
void | run (const SummandListType &list, Container &result) |
![]() | |
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_) |
Protected Attributes | |
std::set< data::sort_expression > | m_sorts |
Sorts to be instantiated. | |
bool | m_tau_summands_only |
Only instantiate tau summands. | |
DataRewriter | m_rewriter |
Rewriter. | |
data::enumerator_algorithm | m_enumerator |
data::enumerator_identifier_generator | m_id_generator |
std::size_t | m_processed |
Statistiscs for verbose output. | |
std::size_t | m_deleted |
std::size_t | m_added |
![]() | |
Specification & | m_spec |
The specification that is processed by the algorithm. | |
Private Types | |
typedef detail::lps_algorithm< Specification > | super |
typedef data::enumerator_list_element_with_substitution | enumerator_element |
typedef Specification::process_type | process_type |
typedef process_type::action_summand_type | action_summand_type |
typedef std::vector< action_summand_type > | action_summand_vector_type |
|
private |
|
private |
|
private |
|
private |
|
private |
|
inline |
|
inlineprotected |
|
inlineprotected |
|
inlineprotected |
|
inline |
|
inlineprotected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |