mcrl2::lps::explorer

Include file:

#include "mcrl2/lps/explorer-cpp17.h
class mcrl2::lps::explorer

Public types

type state_index_type

typedef for typename std::conditional< Stochastic, std::list< std::size_t >, std::size_t >::type

type state_type

typedef for typename std::conditional< Stochastic, stochastic_state, state >::type

Protected types

type enumerator_element

typedef for data::enumerator_list_element_with_substitution

type enumerator_element

typedef for data::enumerator_list_element_with_substitution<>

public-static-attrib

constexpr bool is_stochastic
constexpr bool is_timed

Protected attributes

std::unordered_map<atermpp::term_appl<data::data_expression>, std::list<data::data_expression_list>> global_cache
std::vector<explorer_summand> m_confluent_summands
std::unordered_map<state, std::size_t> m_discovered
data::enumerator_algorithm m_enumerator
data::enumerator_identifier_generator m_id_generator
lps::stochastic_distribution m_initial_distribution
data::data_expression_list m_initial_state
bool m_must_abort
std::size_t m_n
const explorer_options &m_options
std::vector<data::variable> m_process_parameters
bool m_recursive
std::vector<explorer_summand> m_regular_summands
data::rewriter m_rewr
data::mutable_indexed_substitution m_sigma
std::vector<data::data_expression> timed_state

Protected member functions

std::set<data::function_symbol> add_real_operators(std::set<data::function_symbol> s) const
std::set<data::function_symbol> add_real_operators(std::set<data::function_symbol> s) const
void check_enumerator_solution(const enumerator_element &p, const explorer_summand &summand)
void check_enumerator_solution(const enumerator_element &p, const explorer_summand &summand)
state compute_state(const DataExpressionSequence &v) const
state compute_state(const DataExpressionSequence &v) const
stochastic_state compute_stochastic_state(const stochastic_distribution &distribution, const DataExpressionSequence &next_state) const
stochastic_state compute_stochastic_state(const stochastic_distribution &distribution, const DataExpressionSequence &next_state) const
state find_representative(state &u0, const SummandSequence &summands)
state find_representative(state &u0, const SummandSequence &summands)
std::vector<state> generate_successors(const state &s0, const SummandSequence &summands, const SummandSequence &confluent_summands = SummandSequence())
std::vector<state> generate_successors(const state &s0, const SummandSequence &summands, const SummandSequence &confluent_summands = SummandSequence())
void generate_transitions(const explorer_summand &summand, const SummandSequence &confluent_summands, ReportTransition report_transition = ReportTransition())
void generate_transitions(const explorer_summand &summand, const SummandSequence &confluent_summands, ReportTransition report_transition = ReportTransition())
void generate_untimed_stochastic_transitions(const explorer_summand &summand, ExamineTransition examine_transition = ExamineTransition())
bool less_equal(const data::data_expression &t0, const data::data_expression &t1)
bool less_equal(const data::data_expression &t0, const data::data_expression &t1)
std::unique_ptr<todo_set> make_todo_set(const state &init)
std::unique_ptr<todo_set> make_todo_set(ForwardIterator first, ForwardIterator last)
std::unique_ptr<todo_set> make_todo_set(const state &init)
std::unique_ptr<todo_set> make_todo_set(ForwardIterator first, ForwardIterator last)
Specification preprocess(const Specification &lpsspec)
Specification preprocess(const Specification &lpsspec)
process::timed_multi_action rewrite_action(const process::timed_multi_action &a) const
process::timed_multi_action rewrite_action(const process::timed_multi_action &a) const

Public member functions

void abort() override

Abort the state space generation.

void abort() override

Abort the function generate_state_space.

const std::vector<explorer_summand> &confluent_summands() const
const std::vector<explorer_summand> &confluent_summands() const
explorer(const Specification &lpsspec, const explorer_options &options_)
explorer(const Specification &lpsspec, const explorer_options &options_)
void generate_state_space(bool recursive, const StateType &s0, const SummandSequence &regular_summands, const SummandSequence &confluent_summands, std::unordered_map<state, std::size_t> &discovered, DiscoverState discover_state = DiscoverState(), ExamineTransition examine_transition = ExamineTransition(), StartState start_state = StartState(), FinishState finish_state = FinishState(), DiscoverInitialState discover_initial_state = DiscoverInitialState())
void generate_state_space(bool recursive, DiscoverState discover_state = DiscoverState(), ExamineTransition examine_transition = ExamineTransition(), StartState start_state = StartState(), FinishState finish_state = FinishState(), DiscoverInitialState discover_initial_state = DiscoverInitialState())

Generates the state space, and reports all discovered states and transitions by means of callback functions.

Parameters:

  • discover_state Is invoked when a state is encountered for the first time.
  • examine_transition Is invoked on every transition.
  • start_state Is invoked on a state right before its outgoing transitions are being explored.
  • finish_state Is invoked on a state after all of its outgoing transitions have been explored.
void generate_state_space(bool timed, bool recursive, const state &d0, const SummandSequence &regular_summands, const SummandSequence &confluent_summands, std::unordered_map<state, std::size_t> &discovered, DiscoverState discover_state = DiscoverState(), ExamineTransition examine_transition = ExamineTransition(), StartState start_state = StartState(), FinishState finish_state = FinishState())
void generate_state_space(bool timed, bool recursive, DiscoverState discover_state = DiscoverState(), ExamineTransition examine_transition = ExamineTransition(), StartState start_state = StartState(), FinishState finish_state = FinishState())

Generates the state space, and reports all discovered states and transitions by means of callback functions.

Parameters:

  • discover_state Is invoked when a state is encountered for the first time.
  • examine_transition Is invoked on every transition.
  • start_state Is invoked on a state right before its outgoing transitions are being explored.
  • finish_state Is invoked on a state after all of its outgoing transitions have been explored.
void generate_stochastic_state_space(bool recursive, DiscoverState discover_state = DiscoverState(), ExamineTransition examine_transition = ExamineTransition(), StartState start_state = StartState(), FinishState finish_state = FinishState(), DiscoverInitialState discover_initial_state = DiscoverInitialState())

Generates the state space, and reports all discovered states and transitions by means of callback functions.

Parameters:

  • discover_state Is invoked when a state is encountered for the first time.
  • examine_transition Is invoked on every transition.
  • start_state Is invoked on a state right before its outgoing transitions are being explored.
  • finish_state Is invoked on a state after all of its outgoing transitions have been explored.
void generate_timed_state_space(bool recursive, const state &d0, const SummandSequence &regular_summands, const SummandSequence &confluent_summands, std::unordered_map<state, std::size_t> &discovered, DiscoverState discover_state = DiscoverState(), ExamineTransition examine_transition = ExamineTransition(), StartState start_state = StartState(), FinishState finish_state = FinishState())
std::vector<std::pair<lps::multi_action, state_type>> generate_transitions(const state &d0)

Generates outgoing transitions for a given state.

std::vector<std::pair<lps::multi_action, state>> generate_transitions(const data::data_expression_list &init)

Generates outgoing transitions for a given state.

std::vector<std::pair<lps::multi_action, state_type>> generate_transitions(const data::data_expression_list &init, std::size_t i)

Generates outgoing transitions for a given state, reachable via the summand with index i.

std::vector<std::pair<lps::multi_action, state>> generate_transitions(const state &d0)

Generates outgoing transitions for a given state.

std::vector<std::pair<lps::multi_action, state>> generate_transitions(const data::data_expression_list &init)

Generates outgoing transitions for a given state.

std::vector<std::pair<lps::multi_action, state>> generate_transitions(const data::data_expression_list &init, std::size_t i)

Generates outgoing transitions for a given state, reachable via the summand with index i.

void generate_untimed_state_space(bool recursive, const state &d0, const SummandSequence &regular_summands, const SummandSequence &confluent_summands, std::unordered_map<state, std::size_t> &discovered, DiscoverState discover_state = DiscoverState(), ExamineTransition examine_transition = ExamineTransition(), StartState start_state = StartState(), FinishState finish_state = FinishState())
void generate_untimed_stochastic_state_space(bool recursive, const stochastic_state &s0_, const SummandSequence &regular_summands, std::unordered_map<state, std::size_t> &discovered, DiscoverState discover_state = DiscoverState(), ExamineTransition examine_transition = ExamineTransition(), StartState start_state = StartState(), FinishState finish_state = FinishState(), DiscoverInitialState discover_initial_state = DiscoverInitialState())
state_type make_state(const state &s) const
const state_type &make_state(const stochastic_state &s) const
state make_timed_state(const state &s, const data::data_expression &t)
state make_timed_state(const state &s, const data::data_expression &t)
data::data_expression_list process_parameter_values() const
data::data_expression_list process_parameter_values() const
const std::vector<data::variable> &process_parameters() const
const std::vector<data::variable> &process_parameters() const
const std::vector<explorer_summand> &regular_summands() const
const std::vector<explorer_summand> &regular_summands() const
void set_process_parameter_values(const data::data_expression_list &values)
void set_process_parameter_values(const data::data_expression_list &values)
const std::unordered_map<state, std::size_t> &state_map() const

Returns a mapping containing all discovered states.

const std::unordered_map<state, std::size_t> &state_map() const

Returns a mapping containing all discovered states.

~explorer() = default
~explorer() = default