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.