mCRL2
Loading...
Searching...
No Matches
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
mcrl2::lps::detail::lps_algorithm< Specification > Class Template Reference

Algorithm class for algorithms on linear process specifications. It can be instantiated with lps::specification and lps::stochastic_specification. More...

#include <lps_algorithm.h>

Inheritance diagram for mcrl2::lps::detail::lps_algorithm< Specification >:
mcrl2::lps::constelm_algorithm< DataRewriter, Specification > mcrl2::lps::sumelm_algorithm< Specification >

Public Member Functions

 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 Member Functions

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_)
 

Protected Attributes

Specification & m_spec
 The specification that is processed by the algorithm.
 

Detailed Description

template<typename Specification = specification>
class mcrl2::lps::detail::lps_algorithm< Specification >

Algorithm class for algorithms on linear process specifications. It can be instantiated with lps::specification and lps::stochastic_specification.

Definition at line 31 of file lps_algorithm.h.

Constructor & Destructor Documentation

◆ lps_algorithm()

template<typename Specification = specification>
mcrl2::lps::detail::lps_algorithm< Specification >::lps_algorithm ( Specification &  spec)
inline

Constructor.

Definition at line 80 of file lps_algorithm.h.

Member Function Documentation

◆ instantiate_free_variables()

template<typename Specification = specification>
void mcrl2::lps::detail::lps_algorithm< Specification >::instantiate_free_variables ( )
inline

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.

Definition at line 106 of file lps_algorithm.h.

◆ next_state()

template<typename Specification = specification>
data::data_expression mcrl2::lps::detail::lps_algorithm< Specification >::next_state ( const action_summand &  s,
const data::variable &  v 
) const
inline

Applies the next state substitution to the variable v.

Definition at line 91 of file lps_algorithm.h.

◆ remove_parameters()

template<typename Specification = specification>
void mcrl2::lps::detail::lps_algorithm< Specification >::remove_parameters ( const std::set< data::variable > &  to_be_removed)
inline

Removes formal parameters from the specification.

Definition at line 112 of file lps_algorithm.h.

◆ remove_singleton_sorts()

template<typename Specification = specification>
void mcrl2::lps::detail::lps_algorithm< Specification >::remove_singleton_sorts ( )
inline

Removes parameters with a singleton sort.

Definition at line 118 of file lps_algorithm.h.

◆ remove_trivial_summands()

template<typename Specification = specification>
void mcrl2::lps::detail::lps_algorithm< Specification >::remove_trivial_summands ( )
inline

Removes summands with condition equal to false.

Definition at line 124 of file lps_algorithm.h.

◆ remove_unused_summand_variables()

template<typename Specification = specification>
void mcrl2::lps::detail::lps_algorithm< Specification >::remove_unused_summand_variables ( )
inline

Removes unused summand variables.

Definition at line 130 of file lps_algorithm.h.

◆ sumelm_find_variables() [1/2]

template<typename Specification = specification>
void mcrl2::lps::detail::lps_algorithm< Specification >::sumelm_find_variables ( const action_summand &  s,
std::set< data::variable > &  result 
) const
inlineprotected

Definition at line 37 of file lps_algorithm.h.

◆ sumelm_find_variables() [2/2]

template<typename Specification = specification>
void mcrl2::lps::detail::lps_algorithm< Specification >::sumelm_find_variables ( const deadlock_summand &  s,
std::set< data::variable > &  result 
) const
inlineprotected

Definition at line 51 of file lps_algorithm.h.

◆ summand_remove_unused_summand_variables()

template<typename Specification = specification>
template<typename SummandType >
void mcrl2::lps::detail::lps_algorithm< Specification >::summand_remove_unused_summand_variables ( SummandType &  summand_)
inlineprotected

Definition at line 63 of file lps_algorithm.h.

◆ verbose()

template<typename Specification = specification>
bool mcrl2::lps::detail::lps_algorithm< Specification >::verbose ( ) const
inline

Flag for verbose output.

Definition at line 85 of file lps_algorithm.h.

Member Data Documentation

◆ m_spec

template<typename Specification = specification>
Specification& mcrl2::lps::detail::lps_algorithm< Specification >::m_spec
protected

The specification that is processed by the algorithm.

Definition at line 35 of file lps_algorithm.h.

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