mCRL2
Loading...
Searching...
No Matches
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 >:
mcrl2::lps::detail::lps_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
 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

typedef detail::lps_algorithm< Specification > super
 

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 32 of file sumelm.h.

Member Typedef Documentation

◆ super

template<typename Specification = specification>
typedef detail::lps_algorithm<Specification> mcrl2::lps::sumelm_algorithm< Specification >::super
private

Definition at line 34 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
specThe specification to which sum elimination should be applied.
declusterControl whether disjunctive conditions need to be split into multiple summands.

Definition at line 50 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
san action_summand.

Definition at line 84 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 104 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 58 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 42 of file sumelm.h.

◆ m_removed

template<typename Specification = specification>
std::size_t mcrl2::lps::sumelm_algorithm< Specification >::m_removed
protected

Stores the number of summation variables that has been removed.

Definition at line 39 of file sumelm.h.


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