mcrl2::pbes_system::pbesreach_algorithm

Include file:

#include "mcrl2/pbes/pbesreach.h

class mcrl2::pbes_system::pbesreach_algorithm

Private types

type mcrl2::pbes_system::pbesreach_algorithm::enumerator_element

typedef for data::enumerator_list_element_with_substitution<>

Protected types

type mcrl2::pbes_system::pbesreach_algorithm::ldd

typedef for sylvan::ldds::ldd

Protected attributes

std::vector<lps::data_expression_index> mcrl2::pbes_system::pbesreach_algorithm::m_data_index

ldd mcrl2::pbes_system::pbesreach_algorithm::m_deadlocks

data::enumerator_algorithm mcrl2::pbes_system::pbesreach_algorithm::m_enumerator

std::vector<boost::dynamic_bitset<>> mcrl2::pbes_system::pbesreach_algorithm::m_group_patterns

data::enumerator_identifier_generator mcrl2::pbes_system::pbesreach_algorithm::m_id_generator

data::data_expression_list mcrl2::pbes_system::pbesreach_algorithm::m_initial_state

ldd mcrl2::pbes_system::pbesreach_algorithm::m_initial_vertex

std::size_t mcrl2::pbes_system::pbesreach_algorithm::m_n

const symbolic_reachability_options &mcrl2::pbes_system::pbesreach_algorithm::m_options

pbes_system::srf_pbes mcrl2::pbes_system::pbesreach_algorithm::m_pbes

data::variable_list mcrl2::pbes_system::pbesreach_algorithm::m_process_parameters

data::rewriter mcrl2::pbes_system::pbesreach_algorithm::m_rewr

data::mutable_indexed_substitution mcrl2::pbes_system::pbesreach_algorithm::m_sigma

std::vector<summand_group> mcrl2::pbes_system::pbesreach_algorithm::m_summand_groups

std::vector<boost::dynamic_bitset<>> mcrl2::pbes_system::pbesreach_algorithm::m_summand_patterns

ldd mcrl2::pbes_system::pbesreach_algorithm::m_todo

std::vector<std::size_t> mcrl2::pbes_system::pbesreach_algorithm::m_variable_order

ldd mcrl2::pbes_system::pbesreach_algorithm::m_visited

Friends

friend void mcrl2::pbes_system::pbesreach_algorithm::lps::learn_successors_callback

Protected member functions

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

Updates R.L := R.L U {(x,y) in R | x in X}.

pbes_system::srf_pbes preprocess(pbes_system::pbes pbesspec, bool make_total)

ldd state2ldd(const data::data_expression_list &x)

Public member functions

const std::vector<lps::data_expression_index> &data_index() const

ldd deadlocks()

Returns: The set of deadlock states.

ldd initial_state()

virtual void on_end_while_loop()

This function is called right after the while loop is finished.

const srf_pbes &pbes() const

pbesreach_algorithm(const pbes_system::pbes &pbesspec, const symbolic_reachability_options &options_)

const data::variable_list &process_parameters() const

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

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

ldd relprod_impl(const ldd &U, const summand_group &group, std::size_t i)

Computes relprod(U, group).

ldd run(bool report_states = false)

virtual bool solution_found() const

Returns: True iff the solution for the initial state is true.

std::tuple<ldd, ldd, ldd> step(const ldd &visited, const ldd &todo, bool learn_transitions = true, bool detect_deadlocks = false)

Perform a single breadth first step.

Returns: The tuple <visited, todo, deadlocks>

const std::vector<summand_group> &summand_groups() const

virtual sylvan::ldds::ldd W0() const

Returns: True iff the vertex is won by even and nothing if the solution has not been determined.

virtual sylvan::ldds::ldd W1() const

virtual ~pbesreach_algorithm()