Include file:
#include "mcrl2/lps/sumelm.h
mcrl2::lps::
sumelm_algorithm
¶Class implementing the sum elimination lemma.
mcrl2::lps::sumelm_algorithm::
super
¶typedef for detail::lps_algorithm< Specification >
mcrl2::lps::sumelm_algorithm::
m_decluster
¶Whether to decluster disjunctive conditions first.
mcrl2::lps::sumelm_algorithm::
m_removed
¶Stores the number of summation variables that has been removed.
compute_substitutions
(const summand_base &s, data::mutable_map_substitution<> &substitutions)¶is_summand_variable
(const summand_base &s, const data::data_expression &x)¶Returns true if x is a summand variable of summand s.
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.
swap
(T &x, T &y)¶operator()
(action_summand &s)¶Apply the sum elimination lemma to summand s.
Parameters:
operator()
(deadlock_summand &s)¶Apply the sum elimination lemma to summand s.
Parameters:
removed
() const¶Returns the amount of removed summation variables.
run
()Apply the sum elimination lemma to all summands in the specification.
sumelm_algorithm
(Specification &spec, bool decluster = false)¶Constructor.
Parameters: