mcrl2::data::detail::parvalues_algorithm< DataRewriter > Class Template Reference

Algorithm class that can be used to apply the lps_explore_domains algorithm. More...

#include <parvalues.h>

Inheritance diagram for mcrl2::data::detail::parvalues_algorithm< DataRewriter >:

Public Member Functions
	parvalues_algorithm (DataRewriter &r, const data_specification &dataspec, const std::size_t qlimit, const std::size_t maximal_number_of_rounds)
	Constructor for lps_explore_domains algorithm.
void	run ()
	Apply the algorithm to the specification passed in the constructor.

Protected Member Functions
void	propagate_values_qvars (mutable_indexed_substitution<> &sigma, const parameter &v, const variable_vector &qvars, const data_expression &condition, const data_expression &update_expr, const bool used_new_value)
void	propagate_values (mutable_indexed_substitution<> &sigma, const parameter &v, const variable_vector &qvars, const data_expression &condition, const data_expression &update_expr, const bool used_new_value)

Protected Attributes
DataRewriter	m_rewriter
	Rewriter.
const data_specification	m_dataspec
const std::size_t	m_qlimit
const std::size_t	m_maximal_number_of_rounds
data::enumerator_identifier_generator &	m_generator
detail::influence_graph	m_graph

Private Types
using	enumerator_element = data::enumerator_list_element_with_substitution<>

Detailed Description

template<typename DataRewriter>
class mcrl2::data::detail::parvalues_algorithm< DataRewriter >

Algorithm class that can be used to apply the lps_explore_domains algorithm.

All parameter values of the process parameters are enumerated.

Definition at line 268 of file parvalues.h.

Member Typedef Documentation

enumerator_element

template<typename DataRewriter >

using mcrl2::data::detail::parvalues_algorithm< DataRewriter >::enumerator_element = data::enumerator_list_element_with_substitution<>

private

Definition at line 270 of file parvalues.h.

Constructor & Destructor Documentation

parvalues_algorithm()

template<typename DataRewriter >

mcrl2::data::detail::parvalues_algorithm< DataRewriter >::parvalues_algorithm ( DataRewriter &  r, const data_specification &  dataspec, const std::size_t  qlimit, const std::size_t  maximal_number_of_rounds  )

inline

Constructor for lps_explore_domains algorithm.

Parameters

spec	Specification to which the algorithm should be applied
r	a rewriter for data

Definition at line 452 of file parvalues.h.

Member Function Documentation

propagate_values()

template<typename DataRewriter >

void mcrl2::data::detail::parvalues_algorithm< DataRewriter >::propagate_values ( mutable_indexed_substitution<> &  sigma, const parameter &  v, const variable_vector &  qvars, const data_expression &  condition, const data_expression &  update_expr, const bool  used_new_value  )

inlineprotected

Definition at line 386 of file parvalues.h.

propagate_values_qvars()

template<typename DataRewriter >

void mcrl2::data::detail::parvalues_algorithm< DataRewriter >::propagate_values_qvars ( mutable_indexed_substitution<> &  sigma, const parameter &  v, const variable_vector &  qvars, const data_expression &  condition, const data_expression &  update_expr, const bool  used_new_value  )

inlineprotected

Definition at line 283 of file parvalues.h.

run()

template<typename DataRewriter >

void mcrl2::data::detail::parvalues_algorithm< DataRewriter >::run ( )

inline

Apply the algorithm to the specification passed in the constructor.

Definition at line 466 of file parvalues.h.

Member Data Documentation

m_dataspec

template<typename DataRewriter >

const data_specification mcrl2::data::detail::parvalues_algorithm< DataRewriter >::m_dataspec

protected

Definition at line 275 of file parvalues.h.

m_generator

template<typename DataRewriter >

data::enumerator_identifier_generator& mcrl2::data::detail::parvalues_algorithm< DataRewriter >::m_generator

protected

Definition at line 278 of file parvalues.h.

m_graph

template<typename DataRewriter >

detail::influence_graph mcrl2::data::detail::parvalues_algorithm< DataRewriter >::m_graph

protected

Definition at line 280 of file parvalues.h.

m_maximal_number_of_rounds

template<typename DataRewriter >

const std::size_t mcrl2::data::detail::parvalues_algorithm< DataRewriter >::m_maximal_number_of_rounds

protected

Definition at line 277 of file parvalues.h.

m_qlimit

template<typename DataRewriter >

const std::size_t mcrl2::data::detail::parvalues_algorithm< DataRewriter >::m_qlimit

protected

Definition at line 276 of file parvalues.h.

m_rewriter

template<typename DataRewriter >

DataRewriter mcrl2::data::detail::parvalues_algorithm< DataRewriter >::m_rewriter

protected

Rewriter.

Definition at line 274 of file parvalues.h.

---

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

• data/include/mcrl2/data/detail/parvalues.h