Include file:
#include "mcrl2/lps/symbolic_reachability.h"
add your file description here.
mcrl2::lps::summand_group::summand
mcrl2::lps::summand_group
mcrl2::lps::symbolic_reachability_options
mcrl2::lps::
add_real_operators
(std::set<data::function_symbol> s)¶mcrl2::lps::
adjust_read_write_patterns
(std::vector<boost::dynamic_bitset<>> &patterns, const Options &options)¶mcrl2::lps::
alternative_relprev
(const sylvan::ldds::ldd &Y, const summand_group &R, const sylvan::ldds::ldd &X)¶mcrl2::lps::
alternative_relprod
(const sylvan::ldds::ldd &todo, const summand_group &R)¶mcrl2::lps::
check_enumerator_solution
(const EnumeratorElement &p, const summand_group&)¶mcrl2::lps::
compute_summand_group_patterns
(const std::vector<boost::dynamic_bitset<>> &patterns, const std::vector<std::set<std::size_t>> groups)¶mcrl2::lps::
compute_summand_groups
(const std::string &text, const std::vector<boost::dynamic_bitset<>> &patterns)¶mcrl2::lps::
compute_summand_groups_default
(const std::vector<boost::dynamic_bitset<>> &patterns)¶mcrl2::lps::
compute_summand_groups_simple
(const std::vector<boost::dynamic_bitset<>> &patterns)¶mcrl2::lps::
compute_variable_order
(const std::string &text, const std::vector<boost::dynamic_bitset<>> &patterns, bool exclude_first_variable = false)¶mcrl2::lps::
compute_variable_order_default
(std::size_t n)¶mcrl2::lps::
compute_variable_order_random
(std::size_t n, bool exclude_first_variable = false)¶mcrl2::lps::
construct_rewriter
(const data::data_specification &dataspec, data::rewrite_strategy rewrite_strategy, const std::set<data::function_symbol> &function_symbols, bool remove_unused_rewrite_rules)¶mcrl2::lps::
ldd2state
(const std::vector<data_expression_index> &data_index, const std::vector<std::uint32_t> &x)¶mcrl2::lps::
ldd2state
(const std::vector<data_expression_index> &data_index, const std::vector<std::uint32_t> &x, const std::vector<std::size_t> &used)¶mcrl2::lps::
learn_successors_callback
(WorkerP *, Task *, std::uint32_t *x, std::size_t, void *context)¶mcrl2::lps::
operator<<
(std::ostream &out, const symbolic_reachability_options &options)¶mcrl2::lps::
operator<<
(std::ostream &out, const data_expression_index &x)¶mcrl2::lps::
operator<<
(std::ostream &out, const summand_group &x)¶mcrl2::lps::
parameter_indices
(const std::set<data::variable> ¶meters, const std::map<data::variable, std::size_t> &index)¶mcrl2::lps::
parse_summand_groups
(std::string text, std::size_t n)¶mcrl2::lps::
parse_variable_order
(std::string text, std::size_t n, bool exclude_first_variable = false)¶mcrl2::lps::
permute_copy
(const Container &v, const std::vector<std::size_t> &permutation)¶mcrl2::lps::
print_read_write_patterns
(const std::vector<boost::dynamic_bitset<>> &patterns)¶mcrl2::lps::
print_relation
(const std::vector<data_expression_index> &data_index, const sylvan::ldds::ldd &R, const std::vector<std::size_t> &read, const std::vector<std::size_t> &write)¶mcrl2::lps::
print_state
(const std::vector<data_expression_index> &data_index, const std::vector<std::uint32_t> &x)¶mcrl2::lps::
print_state
(const std::vector<data_expression_index> &data_index, const std::vector<std::uint32_t> &x, const std::vector<std::size_t> &used)¶mcrl2::lps::
print_states
(const std::vector<data_expression_index> &data_index, const sylvan::ldds::ldd &x)¶mcrl2::lps::
print_states
(const std::vector<data_expression_index> &data_index, const sylvan::ldds::ldd &x, const std::vector<std::size_t> &used)¶mcrl2::lps::
print_transition
(const std::vector<data_expression_index> &data_index, const std::vector<std::uint32_t> &xy)¶mcrl2::lps::
print_transition
(const std::vector<data_expression_index> &data_index, const std::uint32_t *xy, const std::vector<std::size_t> &read, const std::vector<std::size_t> &write)¶mcrl2::lps::
project
(const std::vector<T> &v, const std::vector<std::size_t> &used)¶mcrl2::lps::
reorder_read_write_patterns
(const std::vector<boost::dynamic_bitset<>> &patterns, const std::vector<std::size_t> &variable_order)¶