mcrl2::pbes_system::pbesinst_lazy_algorithm
===============================================================================


Include file:

.. code-block:: c++

   #include "mcrl2/pbes/pbesinst_lazy.h

.. cpp:class:: mcrl2::pbes_system::pbesinst_lazy_algorithm

  A PBES instantiation algorithm that uses a lazy strategy. 

  

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

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

  

.. cpp:member:: atermpp::indexed_set< propositional_variable_instantiation, true > mcrl2::pbes_system::pbesinst_lazy_algorithm::discovered
  
  The propositional variable instantiations that have been discovered (not necessarily handled). 

  

.. cpp:member:: propositional_variable_instantiation mcrl2::pbes_system::pbesinst_lazy_algorithm::init
  
  The initial value (after rewriting). 

  

.. cpp:member:: pbes_equation_index mcrl2::pbes_system::pbesinst_lazy_algorithm::m_equation_index
  
  A lookup map for PBES equations. 

  

.. cpp:member:: enumerate_quantifiers_rewriter mcrl2::pbes_system::pbesinst_lazy_algorithm::m_global_R
  
  The rewriter. 

  

.. cpp:member:: std::shared_mutex mcrl2::pbes_system::pbesinst_lazy_algorithm::m_graph_access
  
  

  

.. cpp:member:: std::size_t mcrl2::pbes_system::pbesinst_lazy_algorithm::m_iteration_count
  
  

  

.. cpp:member:: bool mcrl2::pbes_system::pbesinst_lazy_algorithm::m_must_abort
  
  

  

.. cpp:member:: const pbessolve_options & mcrl2::pbes_system::pbesinst_lazy_algorithm::m_options
  
  Algorithm options. 

  

.. cpp:member:: pbes mcrl2::pbes_system::pbesinst_lazy_algorithm::m_pbes
  
  A PBES. 

  

.. cpp:member:: std::mutex mcrl2::pbes_system::pbesinst_lazy_algorithm::m_todo_access
  
  

  

.. cpp:member:: pbesinst_lazy_todo mcrl2::pbes_system::pbesinst_lazy_algorithm::todo
  
  The propositional variable instantiations that need to be handled. 

  

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

.. cpp:function:: data::rewriter construct_rewriter(const pbes &pbesspec)
  
  

  

.. cpp:function:: pbes preprocess(const pbes &x) const
  
  

  

.. cpp:function:: virtual std::string status_message(std::size_t equation_count)
  
  

  

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

.. cpp:function:: static void rewrite_true_false(pbes_expression &result, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi)
  
  

  

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

.. cpp:function:: const pbes_equation_index& equation_index() const
  
  

  

.. cpp:function:: void next_todo(propositional_variable_instantiation &result)
  
  

  

.. cpp:function:: virtual void on_discovered_elements(const std::set< propositional_variable_instantiation > &)
  
  This function is called when new elements are added to discovered. 

  

.. cpp:function:: virtual void on_end_while_loop()
  
  This function is called right after the while loop is finished. 

  

.. cpp:function:: virtual void on_report_equation(const std::size_t, std::shared_mutex &, const propositional_variable_instantiation &, const pbes_expression &, std::size_t)
  
  Reports BES equations that are produced by the algorithm. This function is called for every BES equation X = psi with rank k that is produced. By default it does nothing. 

  

.. cpp:function:: pbesinst_lazy_algorithm(const pbessolve_options &options, const pbes &p)
  
  Constructor. 

  
  
  **Parameters:**

  * **p** The pbes used in the exploration algorithm. 

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

  * **search_strategy** The search strategy used to explore the pbes, typically depth or breadth first. 

  * **optimization** An indication of the optimisation level. 



.. cpp:function:: virtual void rewrite_psi(const std::size_t, pbes_expression &result, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi)
  
  

  

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

  

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

  

.. cpp:function:: virtual void run_thread(const std::size_t thread_index, pbesinst_lazy_todo &todo, std::atomic< std::size_t > &number_of_active_processes, data::mutable_indexed_substitution<> sigma, enumerate_quantifiers_rewriter R)
  
  

  

.. cpp:function:: virtual bool solution_found(const propositional_variable_instantiation &) const
  
  

  

.. cpp:function:: const fixpoint_symbol& symbol(std::size_t i) const
  
  

  

.. cpp:function:: virtual ~pbesinst_lazy_algorithm()=default