mcrl2::pbes_system::pbesinst_finite_algorithm
===============================================================================


Include file:

.. code-block:: c++

   #include "mcrl2/pbes/pbesinst_finite_algorithm.h

.. cpp:class:: mcrl2::pbes_system::pbesinst_finite_algorithm

  Algorithm class for the finite pbesinst algorithm. 

  

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

.. cpp:member:: std::size_t mcrl2::pbes_system::pbesinst_finite_algorithm::m_equation_count
  
  The number of generated equations. 

  

.. cpp:member:: data::enumerator_identifier_generator mcrl2::pbes_system::pbesinst_finite_algorithm::m_id_generator
  
  Identifier generator for the enumerator. 

  

.. cpp:member:: data::rewriter::strategy mcrl2::pbes_system::pbesinst_finite_algorithm::m_rewriter_strategy
  
  The strategy of the data rewriter. 

  

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

.. cpp:function:: void compute_index_map(const std::vector< pbes_equation > &equations, const pbesinst_variable_map &variable_map, pbesinst_index_map &index_map)
  
  Returns true if the container contains the given element. 

  

.. cpp:function:: std::string print_equation_count(std::size_t size) const
  
  Prints a message for every 1000-th equation. 

  

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

.. cpp:function:: pbesinst_finite_algorithm(data::rewriter::strategy rewriter_strategy=data::jitty)
  
  Constructor. 

  
  
  **Parameters:**

  * **rewriter_strategy** Strategy to be used for the data rewriter. 



.. cpp:function:: void run(pbes &pbesspec, const pbesinst_variable_map &variable_map)
  
  Runs the algorithm. 

  
  
  **Parameters:**

  * **pbesspec** A PBES 

  * **variable_map** A map containing the finite parameters that should be expanded by the algorithm. 



.. cpp:function:: void run(pbes &p)
  
  Runs the algorithm. 

  
  
  **Parameters:**

  * **p** A PBES