mCRL2
|
Algorithm class that can be used to apply the binary algorithm. More...
#include <binary.h>
Public Member Functions | |
binary_algorithm (Specification &spec, DataRewriter &r, const std::string parameter_selection="") | |
Constructor for binary algorithm. | |
void | run () |
Apply the algorithm to the specification passed in the constructor. | |
![]() | |
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 | |
data::data_expression | make_if_tree (data::variable_vector new_parameters, const data::data_expression_vector &enumerated_elements) |
Build an if-then-else tree of enumerated elements in terms of new parameters. | |
std::set< data::variable > | select_parameters (const std::string parameter_selection) const |
Determine which variables should be replaced, based on parameter_selection. | |
void | replace_enumerated_parameters (const std::set< data::variable > &selected_params) |
Take a specification and calculate a vector of boolean variables for each process parameter in selected_params. A mapping variable -> vector of booleans is stored in new_parameters_table a mapping variable -> enumerated elements is stored in enumerated_elements_table. | |
data::data_expression_list | replace_enumerated_parameters_in_initial_expressions (const data::variable_list &vl, const data::data_expression_list &el) |
Replace expressions in v that are of a finite sort with a vector of assignments to Boolean variables. | |
data::assignment_list | replace_enumerated_parameters_in_assignments (data::assignment_list v) |
Replace assignments in v that are of a finite sort with a vector of assignments to Boolean variables. | |
void | update_action_summand (action_summand &s) |
Update an action summand with the new Boolean parameters. | |
void | update_action_summand (stochastic_action_summand &s) |
Update an action summand with the new Boolean parameters. | |
void | update_deadlock_summand (deadlock_summand &s) |
Update a deadlock summand with the new Boolean parameters. | |
process_initializer | update_initial_process (const data::variable_list ¶meters, const process_initializer &init) |
stochastic_process_initializer | update_initial_process (const data::variable_list ¶meters, const stochastic_process_initializer &init) |
![]() | |
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 | |
DataRewriter | m_rewriter |
Rewriter. | |
const std::string | m_parameter_selection |
std::map< data::variable, std::vector< data::variable > > | m_new_parameters |
Mapping of finite variables to boolean vectors. | |
std::map< data::variable, std::vector< data::data_expression > > | m_enumerated_elements |
Mapping of variables to all values they can be assigned. | |
data::mutable_map_substitution | m_if_trees |
Mapping of variables to corresponding if-tree. | |
data::set_identifier_generator | m_if_trees_generator |
Contains the names of variables appearing in rhs of m_if_trees. | |
data::enumerator_identifier_generator | m_id_generator |
Identifier generator for the enumerator. | |
![]() | |
Specification & | m_spec |
The specification that is processed by the algorithm. | |
Private Types | |
typedef data::enumerator_list_element_with_substitution | enumerator_element |
typedef detail::lps_algorithm< Specification > | super |
typedef Specification::process_type | process_type |
typedef process_type::action_summand_type | action_summand_type |
Algorithm class that can be used to apply the binary algorithm.
All parameters of finite data types are replaced with a vector of booleans.
|
private |
|
private |
|
private |
|
private |
|
inline |
|
inlineprotected |
|
inlineprotected |
Take a specification and calculate a vector of boolean variables for each process parameter in selected_params. A mapping variable -> vector of booleans is stored in new_parameters_table a mapping variable -> enumerated elements is stored in enumerated_elements_table.
|
inlineprotected |
|
inlineprotected |
|
inline |
|
inlineprotected |
|
inlineprotected |
|
inlineprotected |
|
inlineprotected |
|
inlineprotected |
|
inlineprotected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |