Visitor that applies a propositional variable substitution to a pbes expression. More...

#include <pbesinst_finite_algorithm.h>

Inheritance diagram for mcrl2::pbes_system::detail::pbesinst_finite_builder< DataRewriter, SubstitutionFunction >:

Public Types
using	super = pbes_system::detail::data_rewriter_builder< pbesinst_finite_builder, DataRewriter, SubstitutionFunction >

Public Types inherited from mcrl2::pbes_system::detail::data_rewriter_builder< pbesinst_finite_builder< DataRewriter, SubstitutionFunction >, DataRewriter, SubstitutionFunction >
using	super = add_data_rewriter< pbes_system::pbes_expression_builder, pbesinst_finite_builder< DataRewriter, SubstitutionFunction >, DataRewriter, SubstitutionFunction >

Public Types inherited from mcrl2::pbes_system::detail::add_data_rewriter< Builder, Derived, DataRewriter, SubstitutionFunction >
using	super = Builder< Derived >

Public Member Functions
	pbesinst_finite_builder (const DataRewriter &R, SubstitutionFunction &sigma, const pbesinst_finite_rename &rho, const data::data_specification &data_spec, const pbesinst_index_map &index_map, const pbesinst_variable_map &variable_map)

std::string	print_parameters (const std::vector< data::data_expression > &finite_parameters, const std::vector< data::data_expression > &infinite_parameters) const

template<typename VariableContainer , typename ExpressionContainer >
data::data_expression	make_condition (const VariableContainer &variables, const ExpressionContainer &expressions) const
	Computes the condition 'for all i: variables[i] == expressions[i]'.

template<typename DataExpressionContainer >
data::data_expression_list	rewrite_container (const DataExpressionContainer &v, const data::rewriter &rewr)

template<typename DataExpressionContainer >
data::data_expression_list	rewrite_container (const DataExpressionContainer &v, const data::rewriter &rewr, const data::mutable_indexed_substitution<> &sigma)

template<class T >
void	apply (T &result, const propositional_variable_instantiation &x)

propositional_variable_instantiation	visit_initial_state (const propositional_variable_instantiation &init)

Public Member Functions inherited from mcrl2::pbes_system::detail::data_rewriter_builder< pbesinst_finite_builder< DataRewriter, SubstitutionFunction >, DataRewriter, SubstitutionFunction >
	data_rewriter_builder (const DataRewriter &R, SubstitutionFunction &sigma)

Public Member Functions inherited from mcrl2::pbes_system::detail::add_data_rewriter< Builder, Derived, DataRewriter, SubstitutionFunction >
	add_data_rewriter (const DataRewriter &R_, SubstitutionFunction &sigma_)

template<atermpp::IsATerm T>
void	apply (T &result, const data::data_expression &x)

template<class T >
void	apply (T &result, const propositional_variable_instantiation &x)

Public Attributes
const pbesinst_finite_rename &	m_rename

const data::data_specification &	m_data_spec

const pbesinst_index_map &	m_index_map

const pbesinst_variable_map &	m_variable_map

Public Attributes inherited from mcrl2::pbes_system::detail::add_data_rewriter< Builder, Derived, DataRewriter, SubstitutionFunction >
const DataRewriter &	R

SubstitutionFunction &	sigma

Detailed Description

template<typename DataRewriter, typename SubstitutionFunction>
struct mcrl2::pbes_system::detail::pbesinst_finite_builder< DataRewriter, SubstitutionFunction >

Visitor that applies a propositional variable substitution to a pbes expression.

Definition at line 125 of file pbesinst_finite_algorithm.h.

Member Typedef Documentation

◆ super

template<typename DataRewriter , typename SubstitutionFunction >

using mcrl2::pbes_system::detail::pbesinst_finite_builder< DataRewriter, SubstitutionFunction >::super = pbes_system::detail::data_rewriter_builder<pbesinst_finite_builder, DataRewriter, SubstitutionFunction>

Definition at line 127 of file pbesinst_finite_algorithm.h.

Constructor & Destructor Documentation

◆ pbesinst_finite_builder()

template<typename DataRewriter , typename SubstitutionFunction >

mcrl2::pbes_system::detail::pbesinst_finite_builder< DataRewriter, SubstitutionFunction >::pbesinst_finite_builder	(	const DataRewriter &	R,
		SubstitutionFunction &	sigma,
		const pbesinst_finite_rename &	rho,
		const data::data_specification &	data_spec,
		const pbesinst_index_map &	index_map,
		const pbesinst_variable_map &	variable_map
	)

inline

Definition at line 136 of file pbesinst_finite_algorithm.h.

Member Function Documentation

◆ apply()

template<typename DataRewriter , typename SubstitutionFunction >

template<class T >

void mcrl2::pbes_system::detail::pbesinst_finite_builder< DataRewriter, SubstitutionFunction >::apply	(	T &	result,
		const propositional_variable_instantiation &	x
	)

inline

Definition at line 203 of file pbesinst_finite_algorithm.h.

◆ make_condition()

template<typename DataRewriter , typename SubstitutionFunction >

template<typename VariableContainer , typename ExpressionContainer >

data::data_expression mcrl2::pbes_system::detail::pbesinst_finite_builder< DataRewriter, SubstitutionFunction >::make_condition	(	const VariableContainer &	variables,
		const ExpressionContainer &	expressions
	)		const

inline

Computes the condition 'for all i: variables[i] == expressions[i]'.

Definition at line 171 of file pbesinst_finite_algorithm.h.

◆ print_parameters()

template<typename DataRewriter , typename SubstitutionFunction >

std::string mcrl2::pbes_system::detail::pbesinst_finite_builder< DataRewriter, SubstitutionFunction >::print_parameters	(	const std::vector< data::data_expression > &	finite_parameters,
		const std::vector< data::data_expression > &	infinite_parameters
	)		const

inline

Definition at line 150 of file pbesinst_finite_algorithm.h.

◆ rewrite_container() [1/2]

template<typename DataRewriter , typename SubstitutionFunction >

template<typename DataExpressionContainer >

data::data_expression_list mcrl2::pbes_system::detail::pbesinst_finite_builder< DataRewriter, SubstitutionFunction >::rewrite_container	(	const DataExpressionContainer &	v,
		const data::rewriter &	rewr
	)

inline

Definition at line 191 of file pbesinst_finite_algorithm.h.

◆ rewrite_container() [2/2]

template<typename DataRewriter , typename SubstitutionFunction >

template<typename DataExpressionContainer >

data::data_expression_list mcrl2::pbes_system::detail::pbesinst_finite_builder< DataRewriter, SubstitutionFunction >::rewrite_container	(	const DataExpressionContainer &	v,
		const data::rewriter &	rewr,
		const data::mutable_indexed_substitution<> &	sigma
	)

inline

Definition at line 197 of file pbesinst_finite_algorithm.h.

◆ visit_initial_state()

template<typename DataRewriter , typename SubstitutionFunction >

propositional_variable_instantiation mcrl2::pbes_system::detail::pbesinst_finite_builder< DataRewriter, SubstitutionFunction >::visit_initial_state ( const propositional_variable_instantiation & init )