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


Include file:

.. code-block:: c++

   #include "mcrl2/lps/disjointness_checker.h

.. cpp:class:: mcrl2::lps::detail::Disjointness_Checker

  

  

Private attributes
-------------------------------------------------------------------------------

.. cpp:member:: 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. 

  

.. cpp:member:: 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. 

  

.. cpp:member:: 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
-------------------------------------------------------------------------------

.. cpp:function:: 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. 

  

.. cpp:function:: 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. 

  

.. cpp:function:: 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
-------------------------------------------------------------------------------

.. cpp:function:: 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. 

  

.. cpp:function:: 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