mcrl2::lps::binary_algorithm

Include file:

#include "mcrl2/lps/binary.h

class mcrl2::lps::binary_algorithm

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 types

type mcrl2::lps::binary_algorithm::action_summand_type

typedef for process_type::action_summand_type

type mcrl2::lps::binary_algorithm::enumerator_element

typedef for data::enumerator_list_element_with_substitution

type mcrl2::lps::binary_algorithm::process_type

typedef for Specification::process_type

type mcrl2::lps::binary_algorithm::super

typedef for detail::lps_algorithm< Specification >

Protected attributes

std::map<data::variable, std::vector<data::data_expression>> mcrl2::lps::binary_algorithm::m_enumerated_elements

Mapping of variables to all values they can be assigned.

data::enumerator_identifier_generator mcrl2::lps::binary_algorithm::m_id_generator

Identifier generator for the enumerator.

data::mutable_map_substitution mcrl2::lps::binary_algorithm::m_if_trees

Mapping of variables to corresponding if-tree.

data::set_identifier_generator mcrl2::lps::binary_algorithm::m_if_trees_generator

Contains the names of variables appearing in rhs of m_if_trees.

std::map<data::variable, std::vector<data::variable>> mcrl2::lps::binary_algorithm::m_new_parameters

Mapping of finite variables to boolean vectors.

const std::string mcrl2::lps::binary_algorithm::m_parameter_selection

DataRewriter mcrl2::lps::binary_algorithm::m_rewriter

Rewriter.

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.

Pre: enumerated_elements.size() <= 2^new_parameters.size()

Returns: if then else tree from enumerated_elements in terms of new_parameters

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.

Pre: 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.

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.

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.

std::set<data::variable> select_parameters(const std::string parameter_selection) const

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

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)

Public member functions

binary_algorithm(Specification &spec, DataRewriter &r, const std::string parameter_selection = "")

Constructor for binary algorithm.

Parameters:

• spec Specification to which the algorithm should be applied
• r a rewriter for data

void run()

Apply the algorithm to the specification passed in the constructor.