mcrl2::lps::sumelm_algorithm

Include file:

#include "mcrl2/lps/sumelm.h

class mcrl2::lps::sumelm_algorithm

Class implementing the sum elimination lemma.

Private types

type mcrl2::lps::sumelm_algorithm::super

typedef for detail::lps_algorithm< Specification >

Protected attributes

bool mcrl2::lps::sumelm_algorithm::m_decluster

Whether to decluster disjunctive conditions first.

std::size_t mcrl2::lps::sumelm_algorithm::m_removed

Stores the number of summation variables that has been removed.

Protected member functions

data::data_expression compute_substitutions(const summand_base &s, data::mutable_map_substitution<> &substitutions)

bool is_summand_variable(const summand_base &s, const data::data_expression &x)

Returns true if x is a summand variable of summand s.

void sumelm_add_replacement(data::mutable_map_substitution<> &replacements, const data::variable &lhs, const data::data_expression &rhs)

Adds replacement lhs := rhs to the specified map of replacements. All replacements that have lhs as a right hand side will be changed to have rhs as a right hand side.

void swap(T &x, T &y)

Public member functions

void operator()(action_summand &s)

Apply the sum elimination lemma to summand s.

Parameters:

• s an action_summand.

void operator()(deadlock_summand &s)

Apply the sum elimination lemma to summand s.

Parameters:

• s a deadlock_summand.

std::size_t removed() const

Returns the amount of removed summation variables.

void run()

Apply the sum elimination lemma to all summands in the specification.

sumelm_algorithm(Specification &spec, bool decluster = false)

Constructor.

Parameters:

• spec The specification to which sum elimination should be applied.

• decluster Control whether disjunctive conditions need to be split into multiple summands.