mCRL2
Loading...
Searching...
No Matches
mcrl2::lps::binary_algorithm< DataRewriter, Specification > Class Template Reference

Algorithm class that can be used to apply the binary algorithm. More...

#include <binary.h>

Inheritance diagram for mcrl2::lps::binary_algorithm< DataRewriter, Specification >:
mcrl2::lps::detail::lps_algorithm< Specification >

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.
 
- Public Member Functions inherited from mcrl2::lps::detail::lps_algorithm< Specification >
 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::variableselect_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 &parameters, const process_initializer &init)
 
stochastic_process_initializer update_initial_process (const data::variable_list &parameters, const stochastic_process_initializer &init)
 
- Protected Member Functions inherited from mcrl2::lps::detail::lps_algorithm< Specification >
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.
 
- Protected Attributes inherited from mcrl2::lps::detail::lps_algorithm< Specification >
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
 

Detailed Description

template<typename DataRewriter, typename Specification>
class mcrl2::lps::binary_algorithm< DataRewriter, Specification >

Algorithm class that can be used to apply the binary algorithm.

All parameters of finite data types are replaced with a vector of booleans.

Definition at line 44 of file binary.h.

Member Typedef Documentation

◆ action_summand_type

template<typename DataRewriter , typename Specification >
typedef process_type::action_summand_type mcrl2::lps::binary_algorithm< DataRewriter, Specification >::action_summand_type
private

Definition at line 49 of file binary.h.

◆ enumerator_element

template<typename DataRewriter , typename Specification >
typedef data::enumerator_list_element_with_substitution mcrl2::lps::binary_algorithm< DataRewriter, Specification >::enumerator_element
private

Definition at line 46 of file binary.h.

◆ process_type

template<typename DataRewriter , typename Specification >
typedef Specification::process_type mcrl2::lps::binary_algorithm< DataRewriter, Specification >::process_type
private

Definition at line 48 of file binary.h.

◆ super

template<typename DataRewriter , typename Specification >
typedef detail::lps_algorithm<Specification> mcrl2::lps::binary_algorithm< DataRewriter, Specification >::super
private

Definition at line 47 of file binary.h.

Constructor & Destructor Documentation

◆ binary_algorithm()

template<typename DataRewriter , typename Specification >
mcrl2::lps::binary_algorithm< DataRewriter, Specification >::binary_algorithm ( Specification &  spec,
DataRewriter &  r,
const std::string  parameter_selection = "" 
)
inline

Constructor for binary algorithm.

Parameters
specSpecification to which the algorithm should be applied
ra rewriter for data

Definition at line 395 of file binary.h.

Member Function Documentation

◆ make_if_tree()

template<typename DataRewriter , typename Specification >
data::data_expression mcrl2::lps::binary_algorithm< DataRewriter, Specification >::make_if_tree ( data::variable_vector  new_parameters,
const data::data_expression_vector enumerated_elements 
)
inlineprotected

Build an if-then-else tree of enumerated elements in terms of new parameters.

Precondition
enumerated_elements.size() <= 2^new_parameters.size()
Returns
if then else tree from enumerated_elements in terms of new_parameters

Definition at line 77 of file binary.h.

◆ replace_enumerated_parameters()

template<typename DataRewriter , typename Specification >
void mcrl2::lps::binary_algorithm< DataRewriter, Specification >::replace_enumerated_parameters ( const std::set< data::variable > &  selected_params)
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.

Precondition
all elements in selected_params should not be of type Bool and should have a finite type
Returns
data variable list with the new process parameters (i.e. with all variables of a finite type != bool replaced by a vector of boolean variables.

Definition at line 160 of file binary.h.

◆ replace_enumerated_parameters_in_assignments()

template<typename DataRewriter , typename Specification >
data::assignment_list mcrl2::lps::binary_algorithm< DataRewriter, Specification >::replace_enumerated_parameters_in_assignments ( data::assignment_list  v)
inlineprotected

Replace assignments in v that are of a finite sort with a vector of assignments to Boolean variables.

Definition at line 298 of file binary.h.

◆ replace_enumerated_parameters_in_initial_expressions()

template<typename DataRewriter , typename Specification >
data::data_expression_list mcrl2::lps::binary_algorithm< DataRewriter, Specification >::replace_enumerated_parameters_in_initial_expressions ( const data::variable_list vl,
const data::data_expression_list el 
)
inlineprotected

Replace expressions in v that are of a finite sort with a vector of assignments to Boolean variables.

Definition at line 236 of file binary.h.

◆ run()

template<typename DataRewriter , typename Specification >
void mcrl2::lps::binary_algorithm< DataRewriter, Specification >::run ( )
inline

Apply the algorithm to the specification passed in the constructor.

Definition at line 405 of file binary.h.

◆ select_parameters()

template<typename DataRewriter , typename Specification >
std::set< data::variable > mcrl2::lps::binary_algorithm< DataRewriter, Specification >::select_parameters ( const std::string  parameter_selection) const
inlineprotected

Determine which variables should be replaced, based on parameter_selection.

Returns
A subset of the process parameters, with a finite sort that is not Bool

Definition at line 119 of file binary.h.

◆ update_action_summand() [1/2]

template<typename DataRewriter , typename Specification >
void mcrl2::lps::binary_algorithm< DataRewriter, Specification >::update_action_summand ( action_summand s)
inlineprotected

Update an action summand with the new Boolean parameters.

Definition at line 355 of file binary.h.

◆ update_action_summand() [2/2]

template<typename DataRewriter , typename Specification >
void mcrl2::lps::binary_algorithm< DataRewriter, Specification >::update_action_summand ( stochastic_action_summand s)
inlineprotected

Update an action summand with the new Boolean parameters.

Definition at line 363 of file binary.h.

◆ update_deadlock_summand()

template<typename DataRewriter , typename Specification >
void mcrl2::lps::binary_algorithm< DataRewriter, Specification >::update_deadlock_summand ( deadlock_summand s)
inlineprotected

Update a deadlock summand with the new Boolean parameters.

Definition at line 370 of file binary.h.

◆ update_initial_process() [1/2]

template<typename DataRewriter , typename Specification >
process_initializer mcrl2::lps::binary_algorithm< DataRewriter, Specification >::update_initial_process ( const data::variable_list parameters,
const process_initializer init 
)
inlineprotected

Definition at line 376 of file binary.h.

◆ update_initial_process() [2/2]

template<typename DataRewriter , typename Specification >
stochastic_process_initializer mcrl2::lps::binary_algorithm< DataRewriter, Specification >::update_initial_process ( const data::variable_list parameters,
const stochastic_process_initializer init 
)
inlineprotected

Definition at line 381 of file binary.h.

Member Data Documentation

◆ m_enumerated_elements

template<typename DataRewriter , typename Specification >
std::map<data::variable, std::vector<data::data_expression> > mcrl2::lps::binary_algorithm< DataRewriter, Specification >::m_enumerated_elements
protected

Mapping of variables to all values they can be assigned.

Definition at line 62 of file binary.h.

◆ m_id_generator

template<typename DataRewriter , typename Specification >
data::enumerator_identifier_generator mcrl2::lps::binary_algorithm< DataRewriter, Specification >::m_id_generator
protected

Identifier generator for the enumerator.

Definition at line 71 of file binary.h.

◆ m_if_trees

template<typename DataRewriter , typename Specification >
data::mutable_map_substitution mcrl2::lps::binary_algorithm< DataRewriter, Specification >::m_if_trees
protected

Mapping of variables to corresponding if-tree.

Definition at line 65 of file binary.h.

◆ m_if_trees_generator

template<typename DataRewriter , typename Specification >
data::set_identifier_generator mcrl2::lps::binary_algorithm< DataRewriter, Specification >::m_if_trees_generator
protected

Contains the names of variables appearing in rhs of m_if_trees.

Definition at line 68 of file binary.h.

◆ m_new_parameters

template<typename DataRewriter , typename Specification >
std::map<data::variable, std::vector<data::variable> > mcrl2::lps::binary_algorithm< DataRewriter, Specification >::m_new_parameters
protected

Mapping of finite variables to boolean vectors.

Definition at line 59 of file binary.h.

◆ m_parameter_selection

template<typename DataRewriter , typename Specification >
const std::string mcrl2::lps::binary_algorithm< DataRewriter, Specification >::m_parameter_selection
protected

Definition at line 56 of file binary.h.

◆ m_rewriter

template<typename DataRewriter , typename Specification >
DataRewriter mcrl2::lps::binary_algorithm< DataRewriter, Specification >::m_rewriter
protected

Rewriter.

Definition at line 54 of file binary.h.


The documentation for this class was generated from the following file: