mcrl2::pbes_system::partial_order_reduction_algorithm =============================================================================== Include file: .. code-block:: c++ #include "mcrl2/pbes/partial_order_reduction.h .. cpp:class:: mcrl2::pbes_system::partial_order_reduction_algorithm Protected types ------------------------------------------------------------------------------- .. cpp:type:: mcrl2::pbes_system::partial_order_reduction_algorithm::enumerator_element typedef for :cpp:type:`data::enumerator_list_element_with_substitution\< data::data_expression >` Protected attributes ------------------------------------------------------------------------------- .. cpp:member:: std::vector< summand_set > mcrl2::pbes_system::partial_order_reduction_algorithm::m_dependency_nes .. cpp:member:: data::enumerator_algorithm mcrl2::pbes_system::partial_order_reduction_algorithm::m_enumerator .. cpp:member:: pbes_equation_index mcrl2::pbes_system::partial_order_reduction_algorithm::m_equation_index .. cpp:member:: std::chrono::high_resolution_clock::duration mcrl2::pbes_system::partial_order_reduction_algorithm::m_exploration_duration .. cpp:member:: data::enumerator_identifier_generator mcrl2::pbes_system::partial_order_reduction_algorithm::m_id_generator .. cpp:member:: summand_set mcrl2::pbes_system::partial_order_reduction_algorithm::m_invis .. cpp:member:: std::size_t mcrl2::pbes_system::partial_order_reduction_algorithm::m_largest_equation_size .. cpp:member:: pbespor_options mcrl2::pbes_system::partial_order_reduction_algorithm::m_options .. cpp:member:: std::map< data::variable, std::size_t > mcrl2::pbes_system::partial_order_reduction_algorithm::m_parameter_positions .. cpp:member:: std::vector< data::variable > mcrl2::pbes_system::partial_order_reduction_algorithm::m_parameters .. cpp:member:: srf_pbes mcrl2::pbes_system::partial_order_reduction_algorithm::m_pbes .. cpp:member:: data::rewriter mcrl2::pbes_system::partial_order_reduction_algorithm::m_rewr .. cpp:member:: data::mutable_indexed_substitution mcrl2::pbes_system::partial_order_reduction_algorithm::m_sigma .. cpp:member:: smt::smt_solver * mcrl2::pbes_system::partial_order_reduction_algorithm::m_solver .. cpp:member:: std::chrono::high_resolution_clock::duration mcrl2::pbes_system::partial_order_reduction_algorithm::m_static_analysis_duration .. cpp:member:: std::vector< summand_class > mcrl2::pbes_system::partial_order_reduction_algorithm::m_summand_classes .. cpp:member:: std::unordered_map< summand_equivalence_key, std::size_t > mcrl2::pbes_system::partial_order_reduction_algorithm::m_summand_index .. cpp:member:: summand_set mcrl2::pbes_system::partial_order_reduction_algorithm::m_vis Protected member functions ------------------------------------------------------------------------------- .. cpp:function:: const summand_set& choose_minimal_NES(std::size_t k, const propositional_variable_instantiation &X_e) const .. cpp:function:: void compute_dependency_NES() .. cpp:function:: void compute_deterministic() .. cpp:function:: bool compute_deterministic_data(std::size_t k) .. cpp:function:: bool compute_deterministic_equations(std::size_t k) .. cpp:function:: void compute_DNA_DNL_NES(const std::vector< parameter_info > &info) .. cpp:function:: void compute_NES_DNA_DNL() .. cpp:function:: void compute_nxt() .. cpp:function:: void compute_summand_classes() .. cpp:function:: void compute_vis_invis() .. cpp:function:: bool dependency_permanently_disables(const std::size_t k, const std::size_t k1) const Return true iff k1 can never happen after k happens, as deduced from predicate dependencies. .. cpp:function:: bool depends(std::size_t i, std::size_t k, std::size_t j) const .. cpp:function:: bool depends(std::size_t i, std::size_t k) const .. cpp:function:: const summand_set& DNA(std::size_t k) const .. cpp:function:: summand_set& DNA(std::size_t k) .. cpp:function:: const summand_set& DNL(std::size_t k) const .. cpp:function:: summand_set& DNL(std::size_t k) .. cpp:function:: const summand_set& DNS(std::size_t k) const .. cpp:function:: summand_set& DNS(std::size_t k) .. cpp:function:: const summand_set& DNX(std::size_t k, const summand_set &Twork, const summand_set &Ts, const summand_set &en_X_e) const .. cpp:function:: summand_set en(const propositional_variable_instantiation &X_e) .. cpp:function:: std::set FV(const pbes_expression &x) const .. cpp:function:: summand_set invis(const summand_set &K) .. cpp:function:: bool is_true(data::data_expression expr) .. cpp:function:: tribool left_accords_equations(std::size_t k, std::size_t k1) const .. cpp:function:: const summand_set& NES(std::size_t k) const .. cpp:function:: summand_set& NES(std::size_t k) .. cpp:function:: std::size_t parameter_position(const data::variable &v) const .. cpp:function:: void print_pbes() const .. cpp:function:: void print_summand(const srf_summand &summand, bool is_conjunctive) const .. cpp:function:: void print_summand_classes() const .. cpp:function:: std::string print_variables(const data::variable_list &v) const .. cpp:function:: tribool square_accords_equations(std::size_t k, std::size_t k1) const .. cpp:function:: summand_set stubborn_set(const propositional_variable_instantiation &X_e, const summand_set &en_X_e) .. cpp:function:: std::set succ(const propositional_variable_instantiation &X_e, const summand_set &K) .. cpp:function:: std::size_t summand_index(const srf_summand &summand) const .. cpp:function:: tribool triangle_accords_equations(std::size_t k, std::size_t k1) const Protected static member functions ------------------------------------------------------------------------------- .. cpp:function:: static summand_equivalence_key rename_duplicate_variables(data::set_identifier_generator &id_gen, const summand_equivalence_key &summ) Public member functions ------------------------------------------------------------------------------- .. cpp:function:: void explore(const propositional_variable_instantiation &X_init, EmitNode emit_node=EmitNode(), EmitEdge emit_edge=EmitEdge()) .. cpp:function:: void explore_full(const propositional_variable_instantiation &X_init, EmitNode emit_node=EmitNode(), EmitEdge emit_edge=EmitEdge()) .. cpp:function:: const propositional_variable_instantiation& initial_state() const .. cpp:function:: const std::vector& parameters() const .. cpp:function:: partial_order_reduction_algorithm(const pbes &p, pbespor_options options) .. cpp:function:: void print() const .. cpp:function:: const fixpoint_symbol& symbol(const core::identifier_string &X) const .. cpp:function:: ~partial_order_reduction_algorithm()