mcrl2::pbes_system::pbesinst_algorithm
===============================================================================


Include file:

.. code-block:: c++

   #include "mcrl2/pbes/pbesinst_algorithm.h

.. cpp:class:: mcrl2::pbes_system::pbesinst_algorithm

  Algorithm class for the pbesinst instantiation algorithm. 

  

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

.. cpp:member:: data::rewriter mcrl2::pbes_system::pbesinst_algorithm::datar
  
  Data rewriter. 

  

.. cpp:member:: std::set< propositional_variable_instantiation > mcrl2::pbes_system::pbesinst_algorithm::done
  
  Propositional variable instantiations that have been handled. 

  

.. cpp:member:: std::vector< std::vector< pbes_equation > > mcrl2::pbes_system::pbesinst_algorithm::E
  
  Data structure for storing the result. E[i] corresponds to the equations generated from the i-th PBES equation. 

  

.. cpp:member:: std::map< core::identifier_string, int > mcrl2::pbes_system::pbesinst_algorithm::equation_index
  
  A lookup map for PBES equations. 

  

.. cpp:member:: propositional_variable_instantiation mcrl2::pbes_system::pbesinst_algorithm::init
  
  The initial value. 

  

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

  

.. cpp:member:: bool mcrl2::pbes_system::pbesinst_algorithm::m_print_equations
  
  Print the equations to standard out. 

  

.. cpp:member:: enumerate_quantifiers_rewriter mcrl2::pbes_system::pbesinst_algorithm::R
  
  The rewriter. 

  

.. cpp:member:: std::set< propositional_variable_instantiation > mcrl2::pbes_system::pbesinst_algorithm::todo
  
  Propositional variable instantiations that need to be handled. 

  

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

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

  

.. cpp:function:: pbes_expression rho(const pbes_expression &x) const
  
  

  

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

.. cpp:function:: pbes get_result()
  
  Returns the computed bes in pbes format. 

  
      
  **Returns:** The computed bes in pbes format 

.. cpp:function:: pbesinst_algorithm(data::data_specification const &data_spec, data::rewriter::strategy rewrite_strategy=data::jitty, bool print_equations=false)
  
  Constructor. 

  
  
  **Parameters:**

  * **data_spec** A data specification. 

  * **rewrite_strategy** A strategy for the data rewriter. 

  * **print_equations** If true, the generated equations are printed. 



.. cpp:function:: bool& print_equations()
  
  Returns the flag for printing the generated bes equations. 

  
      
  **Returns:** The flag for printing the generated bes equations 

.. cpp:function:: enumerate_quantifiers_rewriter& rewriter()
  
  

  

.. cpp:function:: void run(pbes &p)
  
  Runs the algorithm. The result is obtained by calling the function get_result. 

  
  
  **Parameters:**

  * **p** A PBES.