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 action_summand_type

typedef for process_type::action_summand_type

type enumerator_element

typedef for data::enumerator_list_element_with_substitution

type process_type

typedef for Specification::process_type

type super

typedef for detail::lps_algorithm< Specification >

Protected attributes

std::map<data::variable, std::vector<data::data_expression>> m_enumerated_elements

Mapping of variables to all values they can be assigned.

data::enumerator_identifier_generator m_id_generator

Identifier generator for the enumerator.

data::mutable_map_substitution m_if_trees

Mapping of variables to corresponding if-tree.

std::set<data::variable> m_if_trees_variables

Variables appearing in rhs of m_if_trees.

std::map<data::variable, std::vector<data::variable>> m_new_parameters

Mapping of finite variables to boolean vectors.

DataRewriter m_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()

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.

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 process_initializer &init)
stochastic_process_initializer update_initial_process(const stochastic_process_initializer &init)

Public member functions

binary_algorithm(Specification &spec, DataRewriter &r)

Constructor for binary algorithm.


  • 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.