mcrl2::lps::lpsreach_algorithm

Include file:

#include "mcrl2/lps/lpsreach.h

class mcrl2::lps::lpsreach_algorithm

Private types

type mcrl2::lps::lpsreach_algorithm::enumerator_element

typedef for data::enumerator_list_element_with_substitution<>

type mcrl2::lps::lpsreach_algorithm::ldd

typedef for sylvan::ldds::ldd

Protected attributes

std::vector<lps::data_expression_index> mcrl2::lps::lpsreach_algorithm::m_data_index

data::enumerator_algorithm mcrl2::lps::lpsreach_algorithm::m_enumerator

std::vector<boost::dynamic_bitset<>> mcrl2::lps::lpsreach_algorithm::m_group_patterns

data::enumerator_identifier_generator mcrl2::lps::lpsreach_algorithm::m_id_generator

data::data_expression_list mcrl2::lps::lpsreach_algorithm::m_initial_state

std::size_t mcrl2::lps::lpsreach_algorithm::m_n

const lps::symbolic_reachability_options &mcrl2::lps::lpsreach_algorithm::m_options

data::variable_list mcrl2::lps::lpsreach_algorithm::m_process_parameters

data::rewriter mcrl2::lps::lpsreach_algorithm::m_rewr

data::mutable_indexed_substitution mcrl2::lps::lpsreach_algorithm::m_sigma

std::vector<lps_summand_group> mcrl2::lps::lpsreach_algorithm::m_summand_groups

std::vector<boost::dynamic_bitset<>> mcrl2::lps::lpsreach_algorithm::m_summand_patterns

std::vector<std::size_t> mcrl2::lps::lpsreach_algorithm::m_variable_order

Friends

friend void mcrl2::lps::lpsreach_algorithm::lps::learn_successors_callback

Protected member functions

void learn_successors(std::size_t i, summand_group &R, const ldd &X)

Specification preprocess(const Specification &lpsspec)

ldd state2ldd(const data::data_expression_list &x)

Public member functions

lpsreach_algorithm(const lps::specification &lpsspec, const lps::symbolic_reachability_options &options_)

const std::vector<boost::dynamic_bitset<>> &read_write_group_patterns() const

const std::vector<boost::dynamic_bitset<>> &read_write_patterns() const

ldd run()