mcrl2::lps::sumelm_algorithm< Specification > Class Template Reference

Class implementing the sum elimination lemma. More...

#include <sumelm.h>

Inheritance diagram for mcrl2::lps::sumelm_algorithm< Specification >:

Public Member Functions
	sumelm_algorithm (Specification &spec, bool decluster=false)
	Constructor.
void	run ()
	Apply the sum elimination lemma to all summands in the specification.
template<class Summand >
void	operator() (Summand &s)
	Apply the sum elimination lemma to summand s.
std::size_t	removed () const
	Returns the amount of removed summation variables.
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 Attributes
std::size_t	m_removed = 0
	Stores the number of summation variables that has been removed.
bool	m_decluster
	Whether to decluster disjunctive conditions first.
Protected Attributes inherited from mcrl2::lps::detail::lps_algorithm< Specification >
Specification &	m_spec
	The specification that is processed by the algorithm.

Private Types
using	super = typename detail::lps_algorithm< Specification >

Additional Inherited Members
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
template<typename SummandType >
void	summand_remove_unused_summand_variables (SummandType &summand_)

Detailed Description

template<typename Specification = specification>
class mcrl2::lps::sumelm_algorithm< Specification >

Class implementing the sum elimination lemma.

Definition at line 30 of file sumelm.h.

Member Typedef Documentation

super

template<typename Specification = specification>

using mcrl2::lps::sumelm_algorithm< Specification >::super = typename detail::lps_algorithm<Specification>

private

Definition at line 32 of file sumelm.h.

Constructor & Destructor Documentation

sumelm_algorithm()

template<typename Specification = specification>

mcrl2::lps::sumelm_algorithm< Specification >::sumelm_algorithm ( Specification &  spec, bool  decluster = false  )

inline

Constructor.

Parameters

spec	The specification to which sum elimination should be applied.
decluster	Control whether disjunctive conditions need to be split into multiple summands.

Definition at line 48 of file sumelm.h.

Member Function Documentation

operator()()

template<typename Specification = specification>

template<class Summand >

void mcrl2::lps::sumelm_algorithm< Specification >::operator() ( Summand &  s )

inline

Apply the sum elimination lemma to summand s.

Parameters

s	an action_summand.

Definition at line 82 of file sumelm.h.

removed()

template<typename Specification = specification>

std::size_t mcrl2::lps::sumelm_algorithm< Specification >::removed ( ) const

inline

Returns the amount of removed summation variables.

Definition at line 102 of file sumelm.h.

run()

template<typename Specification = specification>

void mcrl2::lps::sumelm_algorithm< Specification >::run ( )

inline

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

Definition at line 56 of file sumelm.h.

Member Data Documentation

m_decluster

template<typename Specification = specification>

bool mcrl2::lps::sumelm_algorithm< Specification >::m_decluster

protected

Whether to decluster disjunctive conditions first.

Definition at line 40 of file sumelm.h.

m_removed

template<typename Specification = specification>

std::size_t mcrl2::lps::sumelm_algorithm< Specification >::m_removed = 0

protected

Stores the number of summation variables that has been removed.

Definition at line 37 of file sumelm.h.

---

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

• lps/include/mcrl2/lps/sumelm.h