mcrl2::lps::lpsreach_algorithm
===============================================================================


Include file:

.. code-block:: c++

   #include "mcrl2/lps/lpsreach.h

.. cpp:class:: mcrl2::lps::lpsreach_algorithm

  

  

Private types
-------------------------------------------------------------------------------

.. cpp:type:: mcrl2::lps::lpsreach_algorithm::enumerator_element

  typedef for :cpp:type:`data::enumerator_list_element_with_substitution\<>`
  
  

  

.. cpp:type:: mcrl2::lps::lpsreach_algorithm::ldd

  typedef for :cpp:type:`sylvan::ldds::ldd`
  
  

  

Protected attributes
-------------------------------------------------------------------------------

.. cpp:member:: std::vector< lps::data_expression_index > mcrl2::lps::lpsreach_algorithm::m_data_index
  
  

  

.. cpp:member:: data::enumerator_algorithm mcrl2::lps::lpsreach_algorithm::m_enumerator
  
  

  

.. cpp:member:: std::vector< boost::dynamic_bitset<> > mcrl2::lps::lpsreach_algorithm::m_group_patterns
  
  

  

.. cpp:member:: data::enumerator_identifier_generator mcrl2::lps::lpsreach_algorithm::m_id_generator
  
  

  

.. cpp:member:: data::data_expression_list mcrl2::lps::lpsreach_algorithm::m_initial_state
  
  

  

.. cpp:member:: std::size_t mcrl2::lps::lpsreach_algorithm::m_n
  
  

  

.. cpp:member:: const lps::symbolic_reachability_options & mcrl2::lps::lpsreach_algorithm::m_options
  
  

  

.. cpp:member:: data::variable_list mcrl2::lps::lpsreach_algorithm::m_process_parameters
  
  

  

.. cpp:member:: data::rewriter mcrl2::lps::lpsreach_algorithm::m_rewr
  
  

  

.. cpp:member:: data::mutable_indexed_substitution mcrl2::lps::lpsreach_algorithm::m_sigma
  
  

  

.. cpp:member:: std::vector< lps_summand_group > mcrl2::lps::lpsreach_algorithm::m_summand_groups
  
  

  

.. cpp:member:: std::vector< boost::dynamic_bitset<> > mcrl2::lps::lpsreach_algorithm::m_summand_patterns
  
  

  

.. cpp:member:: std::vector< std::size_t > mcrl2::lps::lpsreach_algorithm::m_variable_order
  
  

  

Friends
-------------------------------------------------------------------------------

friend void :cpp:type:`mcrl2::lps::lpsreach_algorithm::lps::learn_successors_callback`
  
  

  

Protected member functions
-------------------------------------------------------------------------------

.. cpp:function:: void learn_successors(std::size_t i, summand_group &R, const ldd &X)
  
  

  

.. cpp:function:: Specification preprocess(const Specification &lpsspec)
  
  

  

.. cpp:function:: ldd state2ldd(const data::data_expression_list &x)
  
  

  

Public member functions
-------------------------------------------------------------------------------

.. cpp:function:: lpsreach_algorithm(const lps::specification &lpsspec, const lps::symbolic_reachability_options &options_)
  
  

  

.. cpp:function:: const std::vector<boost::dynamic_bitset<> >& read_write_group_patterns() const
  
  

  

.. cpp:function:: const std::vector<boost::dynamic_bitset<> >& read_write_patterns() const
  
  

  

.. cpp:function:: ldd run()