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:: std::unordered_set< propositional_variable_instantiation > 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:: std::size_t mcrl2::pbes_system::pbesinst_lazy_algorithm::m_iteration_count .. 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:: enumerate_quantifiers_rewriter mcrl2::pbes_system::pbesinst_lazy_algorithm::R The rewriter. .. 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 pbes_expression rewrite_true_false(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:: propositional_variable_instantiation next_todo() .. 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 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 pbes_expression rewrite_psi(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 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