mcrl2::lps::detail::Disjointness_Checker Class Reference

#include <disjointness_checker.h>

Public Member Functions
template<typename LinearProcess >
	Disjointness_Checker (const LinearProcess &a_process_equation)
	Constructor that initializes the sets Disjointness_Checker::f_used_parameters_per_summand and.
bool	disjoint (std::size_t n1, std::size_t n2)
	Indicates whether or not the summands with number n_1 and n_2 are disjoint.

Private Member Functions
void	process_data_expression (std::size_t n, const data::data_expression &x)
	Updates the array Disjointness_Checker::f_used_parameters_per_summand, given the expression a_expression.
void	process_multi_action (std::size_t n, const multi_action &a)
	Updates the array Disjointness_Checker::f_used_parameters_per_summand, given the multiaction a.
void	process_summand (std::size_t n, const action_summand &s)
	Updates the arrays Disjointness_Checker::f_changed_parameters_per_summand and.

Private Attributes
std::size_t	f_number_of_summands
	The number of summands of the LPS passed as argument of the constructor.
std::vector< std::set< data::variable > >	f_used_parameters_per_summand
	A two dimensional array, indicating which parameters a summand uses, for each of the summands.
std::vector< std::set< data::variable > >	f_changed_parameters_per_summand
	A two dimensional array, indicating which parameters a summand changes, for each of the summands.

Detailed Description

Definition at line 38 of file disjointness_checker.h.

Constructor & Destructor Documentation

Disjointness_Checker()

template<typename LinearProcess >

mcrl2::lps::detail::Disjointness_Checker::Disjointness_Checker

(

const LinearProcess &

a_process_equation

)

Constructor that initializes the sets Disjointness_Checker::f_used_parameters_per_summand and.

Disjointness_Checker::f_changed_parameters_per_summand, and the indexed set

Disjointness_Checker::f_parameter_set. precondition: the argument passed as parameter a_process_equations is a specification of process equations in mCRL2 format precondition: the arguments passed as parameters n_1 and n_2 correspond to summands in the proces equations passed as parameter a_process_equations. They lie in the interval from and including 1 upto and including the highest summand number

Definition at line 164 of file disjointness_checker.h.

Member Function Documentation

disjoint()

bool mcrl2::lps::detail::Disjointness_Checker::disjoint ( std::size_t  n1, std::size_t  n2  )

inline

Indicates whether or not the summands with number n_1 and n_2 are disjoint.

Definition at line 183 of file disjointness_checker.h.

process_data_expression()

void mcrl2::lps::detail::Disjointness_Checker::process_data_expression ( std::size_t  n, const data::data_expression &  x  )

inlineprivate

Updates the array Disjointness_Checker::f_used_parameters_per_summand, given the expression a_expression.

Definition at line 77 of file disjointness_checker.h.

process_multi_action()

void mcrl2::lps::detail::Disjointness_Checker::process_multi_action ( std::size_t  n, const multi_action &  a  )

inlineprivate

Updates the array Disjointness_Checker::f_used_parameters_per_summand, given the multiaction a.

Definition at line 123 of file disjointness_checker.h.

process_summand()

void mcrl2::lps::detail::Disjointness_Checker::process_summand ( std::size_t  n, const action_summand &  s  )

inlineprivate

Updates the arrays Disjointness_Checker::f_changed_parameters_per_summand and.

Disjointness_Checker::f_used_parameters_per_summand, given the summand s.

Definition at line 143 of file disjointness_checker.h.

Member Data Documentation

f_changed_parameters_per_summand

std::vector<std::set<data::variable> > mcrl2::lps::detail::Disjointness_Checker::f_changed_parameters_per_summand

private

A two dimensional array, indicating which parameters a summand changes, for each of the summands.

Definition at line 48 of file disjointness_checker.h.

f_number_of_summands

std::size_t mcrl2::lps::detail::Disjointness_Checker::f_number_of_summands

private

The number of summands of the LPS passed as argument of the constructor.

Definition at line 42 of file disjointness_checker.h.

f_used_parameters_per_summand

std::vector<std::set<data::variable> > mcrl2::lps::detail::Disjointness_Checker::f_used_parameters_per_summand

private

A two dimensional array, indicating which parameters a summand uses, for each of the summands.

Definition at line 45 of file disjointness_checker.h.

---

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

• lps/include/mcrl2/lps/disjointness_checker.h