Include file:
#include "mcrl2/pbes/pbesreach.h
mcrl2::pbes_system::
pbesreach_algorithm
¶mcrl2::pbes_system::pbesreach_algorithm::
enumerator_element
¶typedef for data::enumerator_list_element_with_substitution<>
mcrl2::pbes_system::pbesreach_algorithm::
ldd
¶typedef for sylvan::ldds::ldd
mcrl2::pbes_system::pbesreach_algorithm::
m_data_index
¶mcrl2::pbes_system::pbesreach_algorithm::
m_enumerator
¶mcrl2::pbes_system::pbesreach_algorithm::
m_group_patterns
¶mcrl2::pbes_system::pbesreach_algorithm::
m_id_generator
¶mcrl2::pbes_system::pbesreach_algorithm::
m_initial_state
¶mcrl2::pbes_system::pbesreach_algorithm::
m_n
¶mcrl2::pbes_system::pbesreach_algorithm::
m_options
¶mcrl2::pbes_system::pbesreach_algorithm::
m_pbes
¶mcrl2::pbes_system::pbesreach_algorithm::
m_process_parameters
¶mcrl2::pbes_system::pbesreach_algorithm::
m_rewr
¶mcrl2::pbes_system::pbesreach_algorithm::
m_sigma
¶mcrl2::pbes_system::pbesreach_algorithm::
m_summand_groups
¶mcrl2::pbes_system::pbesreach_algorithm::
m_summand_patterns
¶mcrl2::pbes_system::pbesreach_algorithm::
m_variable_order
¶friend void mcrl2::pbes_system::pbesreach_algorithm::lps::learn_successors_callback
learn_successors
(std::size_t i, summand_group &R, const ldd &X)preprocess
(pbes_system::pbes pbesspec, bool make_total)¶state2ldd
(const data::data_expression_list &x)data_index
() const¶initial_state
()pbesreach_algorithm
(const pbes_system::pbes &pbesspec, const symbolic_reachability_options &options_)¶process_parameters
() constread_write_group_patterns
() constread_write_patterns
() construn
(bool report_states = false)summand_groups
() const¶