mcrl2::lps::explorer

Include file:

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

Public types

type mcrl2::lps::explorer::state_index_type

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

type mcrl2::lps::explorer::state_type

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

Protected types

type mcrl2::lps::explorer::enumerator_element

typedef for data::enumerator_list_element_with_substitution<>

public-static-attrib

constexpr bool mcrl2::lps::explorer::is_stochastic
constexpr bool mcrl2::lps::explorer::is_timed

Protected attributes

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

Protected member functions

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)
state compute_state(const DataExpressionSequence &v) const
stochastic_state compute_stochastic_state(const stochastic_distribution &distribution, const DataExpressionSequence &next_state) const
state find_representative(state &u0, const SummandSequence &summands)
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())
bool less_equal(const data::data_expression &t0, const data::data_expression &t1) const
std::unique_ptr<todo_set> make_todo_set(const state &init)
std::unique_ptr<todo_set> make_todo_set(ForwardIterator first, ForwardIterator last)
std::list<transition> out_edges(const state &s, const SummandSequence &regular_summands, const SummandSequence &confluent_summands)
Specification preprocess(const Specification &lpsspec)
process::timed_multi_action rewrite_action(const process::timed_multi_action &a) const

Public member functions

void abort() override

Abort the state space generation.

const std::vector<explorer_summand> &confluent_summands() const
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, utilities::indexed_set<state> &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_dfs_iterative(const state &s0, std::unordered_set<state> &discovered, const SummandSequence &regular_summands, const SummandSequence &confluent_summands, DiscoverState discover_state = DiscoverState(), ExamineTransition examine_transition = ExamineTransition(), TreeEdge tree_edge = TreeEdge(), BackEdge back_edge = BackEdge(), ForwardOrCrossEdge forward_or_cross_edge = ForwardOrCrossEdge(), FinishState finish_state = FinishState())
void generate_state_space_dfs_iterative(bool recursive, DiscoverState discover_state = DiscoverState(), ExamineTransition examine_transition = ExamineTransition(), TreeEdge tree_edge = TreeEdge(), BackEdge back_edge = BackEdge(), ForwardOrCrossEdge forward_or_cross_edge = ForwardOrCrossEdge(), FinishState finish_state = FinishState())
void generate_state_space_dfs_recursive(const state &s0, std::unordered_set<state> gray, std::unordered_set<state> &discovered, const SummandSequence &regular_summands, const SummandSequence &confluent_summands, DiscoverState discover_state = DiscoverState(), ExamineTransition examine_transition = ExamineTransition(), TreeEdge tree_edge = TreeEdge(), BackEdge back_edge = BackEdge(), ForwardOrCrossEdge forward_or_cross_edge = ForwardOrCrossEdge(), FinishState finish_state = FinishState())
void generate_state_space_dfs_recursive(bool recursive, DiscoverState discover_state = DiscoverState(), ExamineTransition examine_transition = ExamineTransition(), TreeEdge tree_edge = TreeEdge(), BackEdge back_edge = BackEdge(), ForwardOrCrossEdge forward_or_cross_edge = ForwardOrCrossEdge(), 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.

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) const
data::data_expression_list process_parameter_values() const
const std::vector<data::variable> &process_parameters() const
const std::vector<explorer_summand> &regular_summands() const
void set_process_parameter_values(const data::data_expression_list &values)
const utilities::indexed_set<state> &state_map() const

Returns a mapping containing all discovered states.

~explorer() = default