mcrl2::pbes_system::symbolic_pbessolve_algorithm

Include file:

#include "mcrl2/pbes/symbolic_pbessolve.h
class mcrl2::pbes_system::symbolic_pbessolve_algorithm

Protected attributes

ldd mcrl2::pbes_system::symbolic_pbessolve_algorithm::m_all_nodes
const std::vector<lps::data_expression_index> &mcrl2::pbes_system::symbolic_pbessolve_algorithm::m_data_index
bool mcrl2::pbes_system::symbolic_pbessolve_algorithm::m_no_relprod
std::map<std::size_t, ldd> mcrl2::pbes_system::symbolic_pbessolve_algorithm::m_rank_map
const std::vector<summand_group> &mcrl2::pbes_system::symbolic_pbessolve_algorithm::m_summand_groups
ldd mcrl2::pbes_system::symbolic_pbessolve_algorithm::m_V

Public member functions

ldd attractor(const ldd &U, std::size_t alpha, const ldd &V)
std::pair<std::size_t, ldd> get_min_rank(const ldd &V)
ldd predecessors(const ldd &U, const ldd &V)
bool solve(const ldd &V, const ldd &initial_vertex)
symbolic_pbessolve_algorithm(const ldd &V, const std::vector<summand_group> &summand_groups, const std::map<std::size_t, std::pair<std::size_t, bool>> &equation_info, bool no_relprod, const std::vector<lps::data_expression_index> &data_index)
std::pair<ldd, ldd> zielonka(const ldd &V)