mcrl2/lps/symbolic_reachability.h

Include file:

#include "mcrl2/lps/symbolic_reachability.h"

add your file description here.

Classes

Variables

constexpr std::uint32_t mcrl2::lps::relprod_ignore

Functions

std::set<data::function_symbol> mcrl2::lps::add_real_operators(std::set<data::function_symbol> s)
void mcrl2::lps::adjust_read_write_patterns(std::vector<boost::dynamic_bitset<>> &patterns, const Options &options)
sylvan::ldds::ldd mcrl2::lps::alternative_relprev(const sylvan::ldds::ldd &Y, const summand_group &R, const sylvan::ldds::ldd &X)
sylvan::ldds::ldd mcrl2::lps::alternative_relprod(const sylvan::ldds::ldd &todo, const summand_group &R)
void mcrl2::lps::check_enumerator_solution(const EnumeratorElement &p, const summand_group&)
std::vector<boost::dynamic_bitset<>> mcrl2::lps::compute_summand_group_patterns(const std::vector<boost::dynamic_bitset<>> &patterns, const std::vector<std::set<std::size_t>> groups)
std::vector<std::set<std::size_t>> mcrl2::lps::compute_summand_groups(const std::string &text, const std::vector<boost::dynamic_bitset<>> &patterns)
std::vector<std::set<std::size_t>> mcrl2::lps::compute_summand_groups_default(const std::vector<boost::dynamic_bitset<>> &patterns)
std::vector<std::set<std::size_t>> mcrl2::lps::compute_summand_groups_simple(const std::vector<boost::dynamic_bitset<>> &patterns)
std::vector<std::size_t> mcrl2::lps::compute_variable_order(const std::string &text, const std::vector<boost::dynamic_bitset<>> &patterns, bool exclude_first_variable = false)
std::vector<std::size_t> mcrl2::lps::compute_variable_order_default(std::size_t n)
std::vector<std::size_t> mcrl2::lps::compute_variable_order_random(std::size_t n, bool exclude_first_variable = false)
data::rewriter 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)
std::vector<data::data_expression> mcrl2::lps::ldd2state(const std::vector<data_expression_index> &data_index, const std::vector<std::uint32_t> &x)
std::vector<data::data_expression> 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)
void mcrl2::lps::learn_successors_callback(WorkerP *, Task *, std::uint32_t *x, std::size_t, void *context)
std::ostream &mcrl2::lps::operator<<(std::ostream &out, const symbolic_reachability_options &options)
std::ostream &mcrl2::lps::operator<<(std::ostream &out, const data_expression_index &x)
std::ostream &mcrl2::lps::operator<<(std::ostream &out, const summand_group &x)
std::set<std::size_t> mcrl2::lps::parameter_indices(const std::set<data::variable> &parameters, const std::map<data::variable, std::size_t> &index)
std::vector<std::set<std::size_t>> mcrl2::lps::parse_summand_groups(std::string text, std::size_t n)
std::vector<std::size_t> mcrl2::lps::parse_variable_order(std::string text, std::size_t n, bool exclude_first_variable = false)
Container mcrl2::lps::permute_copy(const Container &v, const std::vector<std::size_t> &permutation)
std::string mcrl2::lps::print_read_write_patterns(const std::vector<boost::dynamic_bitset<>> &patterns)
std::string 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)
std::string mcrl2::lps::print_state(const std::vector<data_expression_index> &data_index, const std::vector<std::uint32_t> &x)
std::string 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)
std::string mcrl2::lps::print_states(const std::vector<data_expression_index> &data_index, const sylvan::ldds::ldd &x)
std::string mcrl2::lps::print_states(const std::vector<data_expression_index> &data_index, const sylvan::ldds::ldd &x, const std::vector<std::size_t> &used)
std::string mcrl2::lps::print_transition(const std::vector<data_expression_index> &data_index, const std::vector<std::uint32_t> &xy)
std::string 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)
std::vector<T> mcrl2::lps::project(const std::vector<T> &v, const std::vector<std::size_t> &used)
std::vector<boost::dynamic_bitset<>> mcrl2::lps::reorder_read_write_patterns(const std::vector<boost::dynamic_bitset<>> &patterns, const std::vector<std::size_t> &variable_order)