mCRL2
Loading...
Searching...
No Matches
mcrl2::lps::parelm_algorithm< Specification > Class Template Reference

Algorithm class for elimination of unused parameters from a linear process specification. More...

#include <parelm.h>

Inheritance diagram for mcrl2::lps::parelm_algorithm< Specification >:
mcrl2::lps::detail::lps_algorithm< Specification >

Public Member Functions

 parelm_algorithm (Specification &spec)
 Constructor.
 
void run (bool variant1=true)
 Runs the parelm algorithm.
 
- 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

std::set< data::variabletransition_variables ()
 Returns the data variables that are considered in the parelm algorithm.
 
void report_results (const std::set< data::variable > &to_be_removed) const
 
void parelm1 ()
 First version of parelm1.
 
void parelm2 ()
 Second version of parelm that builds a dependency graph.
 
- 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_)
 

Private Types

typedef lps::detail::lps_algorithm< Specification > super
 

Additional Inherited Members

- Protected Attributes inherited from mcrl2::lps::detail::lps_algorithm< Specification >
Specification & m_spec
 The specification that is processed by the algorithm.
 

Detailed Description

template<typename Specification>
class mcrl2::lps::parelm_algorithm< Specification >

Algorithm class for elimination of unused parameters from a linear process specification.

Definition at line 65 of file parelm.h.

Member Typedef Documentation

◆ super

template<typename Specification >
typedef lps::detail::lps_algorithm<Specification> mcrl2::lps::parelm_algorithm< Specification >::super
private

Definition at line 67 of file parelm.h.

Constructor & Destructor Documentation

◆ parelm_algorithm()

template<typename Specification >
mcrl2::lps::parelm_algorithm< Specification >::parelm_algorithm ( Specification &  spec)
inline

Constructor.

Definition at line 250 of file parelm.h.

Member Function Documentation

◆ parelm1()

template<typename Specification >
void mcrl2::lps::parelm_algorithm< Specification >::parelm1 ( )
inlineprotected

First version of parelm1.

Definition at line 106 of file parelm.h.

◆ parelm2()

template<typename Specification >
void mcrl2::lps::parelm_algorithm< Specification >::parelm2 ( )
inlineprotected

Second version of parelm that builds a dependency graph.

Definition at line 163 of file parelm.h.

◆ report_results()

template<typename Specification >
void mcrl2::lps::parelm_algorithm< Specification >::report_results ( const std::set< data::variable > &  to_be_removed) const
inlineprotected

Definition at line 93 of file parelm.h.

◆ run()

template<typename Specification >
void mcrl2::lps::parelm_algorithm< Specification >::run ( bool  variant1 = true)
inline

Runs the parelm algorithm.

Definition at line 255 of file parelm.h.

◆ transition_variables()

template<typename Specification >
std::set< data::variable > mcrl2::lps::parelm_algorithm< Specification >::transition_variables ( )
inlineprotected

Returns the data variables that are considered in the parelm algorithm.

Returns
The data variables that appear in the condition, action or time of the summands

Definition at line 75 of file parelm.h.


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