mCRL2
Loading...
Searching...
No Matches
mcrl2::lps::suminst_algorithm< DataRewriter, Specification > Class Template Reference

#include <suminst.h>

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

Public Member Functions

 suminst_algorithm (Specification &spec, DataRewriter &r, std::set< data::sort_expression > sorts=std::set< data::sort_expression >(), bool tau_summands_only=false)
 
void run ()
 
- 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 Member Functions

template<typename SummandType , typename Container >
std::size_t instantiate_summand (const SummandType &s, Container &result)
 
bool must_instantiate (const action_summand_type &summand)
 
bool must_instantiate (const deadlock_summand &)
 
template<typename SummandListType , typename Container >
void run (const SummandListType &list, Container &result)
 
- 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
 
void summand_remove_unused_summand_variables (SummandType &summand_)
 

Protected Attributes

std::set< data::sort_expressionm_sorts
 Sorts to be instantiated.
 
bool m_tau_summands_only
 Only instantiate tau summands.
 
DataRewriter m_rewriter
 Rewriter.
 
data::enumerator_algorithm m_enumerator
 
data::enumerator_identifier_generator m_id_generator
 
std::size_t m_processed
 Statistiscs for verbose output.
 
std::size_t m_deleted
 
std::size_t m_added
 
- 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
 
typedef data::enumerator_list_element_with_substitution enumerator_element
 
typedef Specification::process_type process_type
 
typedef process_type::action_summand_type action_summand_type
 
typedef std::vector< action_summand_typeaction_summand_vector_type
 

Detailed Description

template<typename DataRewriter, typename Specification>
class mcrl2::lps::suminst_algorithm< DataRewriter, Specification >

Definition at line 44 of file suminst.h.

Member Typedef Documentation

◆ action_summand_type

template<typename DataRewriter , typename Specification >
typedef process_type::action_summand_type mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::action_summand_type
private

Definition at line 49 of file suminst.h.

◆ action_summand_vector_type

template<typename DataRewriter , typename Specification >
typedef std::vector<action_summand_type> mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::action_summand_vector_type
private

Definition at line 50 of file suminst.h.

◆ enumerator_element

template<typename DataRewriter , typename Specification >
typedef data::enumerator_list_element_with_substitution mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::enumerator_element
private

Definition at line 47 of file suminst.h.

◆ process_type

template<typename DataRewriter , typename Specification >
typedef Specification::process_type mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::process_type
private

Definition at line 48 of file suminst.h.

◆ super

template<typename DataRewriter , typename Specification >
typedef detail::lps_algorithm<Specification> mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::super
private

Definition at line 46 of file suminst.h.

Constructor & Destructor Documentation

◆ suminst_algorithm()

template<typename DataRewriter , typename Specification >
mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::suminst_algorithm ( Specification &  spec,
DataRewriter &  r,
std::set< data::sort_expression sorts = std::set<data::sort_expression>(),
bool  tau_summands_only = false 
)
inline

Definition at line 181 of file suminst.h.

Member Function Documentation

◆ instantiate_summand()

template<typename DataRewriter , typename Specification >
template<typename SummandType , typename Container >
std::size_t mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::instantiate_summand ( const SummandType &  s,
Container &  result 
)
inlineprotected

Definition at line 71 of file suminst.h.

◆ must_instantiate() [1/2]

template<typename DataRewriter , typename Specification >
bool mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::must_instantiate ( const action_summand_type summand)
inlineprotected

Definition at line 143 of file suminst.h.

◆ must_instantiate() [2/2]

template<typename DataRewriter , typename Specification >
bool mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::must_instantiate ( const deadlock_summand )
inlineprotected

Definition at line 148 of file suminst.h.

◆ run() [1/2]

template<typename DataRewriter , typename Specification >
void mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::run ( )
inline

Definition at line 201 of file suminst.h.

◆ run() [2/2]

template<typename DataRewriter , typename Specification >
template<typename SummandListType , typename Container >
void mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::run ( const SummandListType &  list,
Container &  result 
)
inlineprotected

Definition at line 154 of file suminst.h.

Member Data Documentation

◆ m_added

template<typename DataRewriter , typename Specification >
std::size_t mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::m_added
protected

Definition at line 68 of file suminst.h.

◆ m_deleted

template<typename DataRewriter , typename Specification >
std::size_t mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::m_deleted
protected

Definition at line 67 of file suminst.h.

◆ m_enumerator

template<typename DataRewriter , typename Specification >
data::enumerator_algorithm mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::m_enumerator
protected

Definition at line 62 of file suminst.h.

◆ m_id_generator

template<typename DataRewriter , typename Specification >
data::enumerator_identifier_generator mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::m_id_generator
protected

Definition at line 63 of file suminst.h.

◆ m_processed

template<typename DataRewriter , typename Specification >
std::size_t mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::m_processed
protected

Statistiscs for verbose output.

Definition at line 66 of file suminst.h.

◆ m_rewriter

template<typename DataRewriter , typename Specification >
DataRewriter mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::m_rewriter
protected

Rewriter.

Definition at line 61 of file suminst.h.

◆ m_sorts

template<typename DataRewriter , typename Specification >
std::set<data::sort_expression> mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::m_sorts
protected

Sorts to be instantiated.

Definition at line 55 of file suminst.h.

◆ m_tau_summands_only

template<typename DataRewriter , typename Specification >
bool mcrl2::lps::suminst_algorithm< DataRewriter, Specification >::m_tau_summands_only
protected

Only instantiate tau summands.

Definition at line 58 of file suminst.h.


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