Function object that computes the condition for commutative confluence. More...

#include <confluence.h>

Public Member Functions
	commutative_confluence_condition (const data::variable_list &process_parameters_, data::mutable_indexed_substitution<> &sigma_, data::set_identifier_generator &generator_)

data::variable_list	make_fresh_variables (const data::variable_list &e) const

data::data_expression	operator() (const confluence_summand &summand_i, const confluence_summand &summand_j) const

Public Attributes
const data::variable_list &	process_parameters

data::mutable_indexed_substitution &	sigma

data::set_identifier_generator &	generator

Detailed Description

Function object that computes the condition for commutative confluence.

Parameters

summand_i	An arbitrary action summand
summand_j	A tau summand

Definition at line 204 of file confluence.h.

Constructor & Destructor Documentation

mcrl2::lps::commutative_confluence_condition::commutative_confluence_condition	(	const data::variable_list &	process_parameters_,
		data::mutable_indexed_substitution<> &	sigma_,
		data::set_identifier_generator &	generator_
	)

inline

Definition at line 210 of file confluence.h.

data::variable_list mcrl2::lps::commutative_confluence_condition::make_fresh_variables ( const data::variable_list & e ) const

inline

Definition at line 214 of file confluence.h.

data::data_expression mcrl2::lps::commutative_confluence_condition::operator()	(	const confluence_summand &	summand_i,
		const confluence_summand &	summand_j
	)		const

inline

Definition at line 219 of file confluence.h.

data::set_identifier_generator& mcrl2::lps::commutative_confluence_condition::generator

Definition at line 208 of file confluence.h.

const data::variable_list& mcrl2::lps::commutative_confluence_condition::process_parameters

Definition at line 206 of file confluence.h.

data::mutable_indexed_substitution& mcrl2::lps::commutative_confluence_condition::sigma

Definition at line 207 of file confluence.h.

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