mcrl2::pbes_system::pbesbddsolve
===============================================================================


Include file:

.. code-block:: c++

   #include "mcrl2/pbes/pbesbddsolve1.h

.. cpp:class:: mcrl2::pbes_system::pbesbddsolve

  

  

Private attributes
-------------------------------------------------------------------------------

.. cpp:member:: bdd_granularity mcrl2::pbes_system::pbesbddsolve::m_granularity
  
  

  

.. cpp:member:: const srf_pbes & mcrl2::pbes_system::pbesbddsolve::m_pbes
  
  

  

.. cpp:member:: pbes_equation_index mcrl2::pbes_system::pbesbddsolve::m_pbes_index
  
  

  

.. cpp:member:: utilities::execution_timer * mcrl2::pbes_system::pbesbddsolve::m_timer
  
  

  

.. cpp:member:: bool mcrl2::pbes_system::pbesbddsolve::m_unary_encoding
  
  

  

.. cpp:member:: variable_manager mcrl2::pbes_system::pbesbddsolve::m_variable_manager
  
  

  

Private member functions
-------------------------------------------------------------------------------

.. cpp:function:: std::vector<bdd> compute_edge_relation(const std::vector< srf_equation > &equations, const std::vector< bdd > &equation_ids, const std::vector< bdd > &equation_ids_next, const std::vector< bdd > &parameters_next) const
  
  

  

.. cpp:function:: std::vector<data::variable> compute_id_variables(std::size_t n, bool unary_encoding)
  
  

  

.. cpp:function:: bdd compute_initial_state(const std::vector< bdd > &ids) const
  
  

  

.. cpp:function:: std::vector<bdd> compute_nodes(std::size_t equation_count, const std::vector< bdd > &id_variables, bool unary_encoding)
  
  

  

.. cpp:function:: std::tuple< bdd, bdd, bdd, bdd_substitution, bdd_substitution, bdd, std::vector<bdd>, bdd, bdd, bdd, std::map<std::uint32_t, bdd> > compute_parity_game()
  
  

  

.. cpp:function:: std::map<std::size_t, std::vector<bdd> > compute_priority_map(const std::vector< bdd > &equation_ids) const
  
  

  

.. cpp:function:: void finish_timer(const std::string &msg) const
  
  

  

.. cpp:function:: std::vector<bdd> make_bdd_variables(const std::vector< data::variable > &v)
  
  

  

.. cpp:function:: bdd parameter_updates(const std::vector< bdd > &parameters, const std::vector< bdd > &values) const
  
  

  

.. cpp:function:: void start_timer(const std::string &msg) const
  
  

  

.. cpp:function:: bdd to_bdd(const data::variable &x) const
  
  

  

.. cpp:function:: bdd to_bdd(const data::data_expression &x) const
  
  

  

.. cpp:function:: std::vector<bdd> to_bdd(const data::data_expression_list &v) const
  
  

  

.. cpp:function:: std::vector<bdd> to_bdd(const data::variable_list &v) const
  
  

  

.. cpp:function:: std::vector<bdd> to_bdd(const std::vector< data::variable > &v) const
  
  

  

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

.. cpp:function:: pbesbddsolve(const srf_pbes &p, bool unary_encoding=false, bdd_granularity granularity=bdd_granularity::per_pbes, utilities::execution_timer *timer=nullptr)
  
  

  

.. cpp:function:: bool run(bool use_sylvan_optimization=true, bool remove_unreachable_vertices=true)