mcrl2::lps::detail::Disjointness_Checker

Include file:

#include "mcrl2/lps/disjointness_checker.h

class mcrl2::lps::detail::Disjointness_Checker

Private attributes

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

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

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

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

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

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

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.

Disjointness_Checker::f_used_parameters_per_summand, given the summand s.

Public member functions

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.

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 setDisjointness_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