mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm =============================================================================== Include file: .. code-block:: c++ #include "mcrl2/pbes/pbesinst_alternative_lazy_algorithm.h .. cpp:class:: mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm An alternative lazy algorithm for instantiating a PBES, ported from bes_deprecated.h. Public types ------------------------------------------------------------------------------- .. cpp:type:: mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::pbes_expression_pair typedef for :cpp:type:`std::pair\< pbes_expression, pbes_expression >` Protected attributes ------------------------------------------------------------------------------- .. cpp:member:: std::unordered_map< propositional_variable_instantiation, pbes_expression > mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::equation Map a variable instantiation to its right hand side. .. cpp:member:: std::unordered_map< core::identifier_string, std::size_t > mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::equation_index A lookup map for PBES equations. .. cpp:member:: propositional_variable_instantiation mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::init The initial value. .. cpp:member:: std::vector< std::vector< propositional_variable_instantiation > > mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::instantiations instantiations[i] contains all instantiations of the variable of the i-th equation in the PBES. .. cpp:member:: const bool mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_approximate_true The variable m_approximimate_true indicates whether boolean variables that cannot be dealt with as the todo buffer would otherwise exceeds m_maximum_todo_size are set to true or to false .. cpp:member:: const data::data_specification & mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_data_spec .. cpp:member:: const data::rewriter & mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_datar Data rewriter. .. cpp:member:: std::size_t mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_elements_not_stored_in_todo_buffer When the todo buffer is limited, due to m_maximum_todo_size, then the variable below counts how many elements are dropped out of the todo buffer. .. cpp:member:: const mcrl2::bes::remove_level mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_erase_unused_bes_variables Indicate to which extent explored bes equations that turn out not to reachable can be thrown away. Values are: none, some or all. .. cpp:member:: const std::size_t mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_maximum_todo_size The maximum size that the todo buffer is allowed to have. .. cpp:member:: search_strategy mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_search_strategy The search strategy to use when exploring the state space. .. cpp:member:: transformation_strategy mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::m_transformation_strategy Transformation strategy. .. cpp:member:: std::unordered_map< propositional_variable_instantiation, std::unordered_set< propositional_variable_instantiation > > mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::occurrence Map a variable instantiation to a set of other variable instantiations on whose right hand sides it appears. .. cpp:member:: enumerate_quantifiers_rewriter mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::R The rewriter. .. cpp:member:: std::vector< std::size_t > mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::ranks ranks[i] contains the rank of the i-th equation in the PBES. .. cpp:member:: std::vector< fixpoint_symbol > mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::symbols symbols[i] contains the fixedpoint symbol of the i-th equation in the PBES. .. cpp:member:: std::deque< propositional_variable_instantiation > mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::todo Propositional variable instantiations that need to be handled. .. cpp:member:: std::unordered_set< propositional_variable_instantiation > mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::todo_set The content of todo as a set. .. cpp:member:: std::unordered_map< propositional_variable_instantiation, pbes_expression > mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::trivial Map a variable instantiations to its right hand side when the latter is trivial (either true or false). Protected static attributes ------------------------------------------------------------------------------- .. cpp:member:: const std::size_t mcrl2::pbes_system::pbesinst_alternative_lazy_algorithm::regeneration_count_init Initial value for regeneration_period. Protected member functions ------------------------------------------------------------------------------- .. cpp:function:: void print_equation_count(const std::size_t nr_of_processed_variables, const std::size_t nr_of_generated_variables, const std::size_t todo_size) const Prints a log message for every 1000-th equation. Public member functions ------------------------------------------------------------------------------- .. cpp:function:: void add_todo(const propositional_variable_instantiation &X) .. cpp:function:: bool find_loop(pbes_expression expr, propositional_variable_instantiation X) .. cpp:function:: bool find_loop_rec(const pbes_expression &expr, propositional_variable_instantiation X, std::size_t rank, std::unordered_map< propositional_variable_instantiation, bool > &visited) .. cpp:function:: std::size_t get_rank(const propositional_variable_instantiation &X) .. cpp:function:: pbes get_result(bool short_rename_scheme=true) Returns the computed bes in pbes format. **Returns:** The computed bes in pbes format .. cpp:function:: propositional_variable_instantiation next_todo() .. cpp:function:: pbesinst_alternative_lazy_algorithm(const data::data_specification &data_spec, const data::rewriter &datar, search_strategy search_strategy=breadth_first, transformation_strategy transformation_strategy=lazy, const mcrl2::bes::remove_level erase_unused_bes_variables=mcrl2::bes::none, const std::size_t maximum_todo_size=std::numeric_limits< std::size_t >::max(), const bool approximate_true=true) Constructor. **Parameters:** * **data_spec** A data specification. * **datar** A data rewriter. * **search_strategy** A search strategy (e.g. breadth_first). * **transformation_strategy** A strategy to transform the PBES into a BES. * **erase_unused_bes_variables** An indicator how often unreachable variables must be garbage collected. * **maximum_todo_size** An indication of the maximal size of the stack with explorable BES variables. If the stack exceeds this size, the ignored variable is set to true or false, depending on the parameter approximate_true. * **approximate_true** If true BES variables that are not investigated are set to false. If false these variables are set to true. .. cpp:function:: void regenerate_states() .. 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 .. cpp:function:: pbes_expression_pair simplify_pbes_expression(const pbes_expression &p, const std::unordered_map< propositional_variable_instantiation, pbes_expression > &trivial)