mcrl2::lps::explorer

Include file:

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

Public types

type mcrl2::lps::explorer::indexed_set_for_states_type

typedef for atermpp::indexed_set< state, atermpp::detail::GlobalThreadSafe >

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

summand_cache_map mcrl2::lps::explorer::global_cache
std::vector<explorer_summand> mcrl2::lps::explorer::m_confluent_summands
indexed_set_for_states_type mcrl2::lps::explorer::m_discovered
std::mutex mcrl2::lps::explorer::m_exclusive_state_access
data::enumerator_algorithm mcrl2::lps::explorer::m_global_enumerator
data::enumerator_identifier_generator mcrl2::lps::explorer::m_global_id_generator
Specification mcrl2::lps::explorer::m_global_lpsspec
data::rewriter mcrl2::lps::explorer::m_global_rewr
data::mutable_indexed_substitution mcrl2::lps::explorer::m_global_sigma
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
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 data::data_expression &p_expression, const explorer_summand &summand, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr) const
void compute_state(state &result, const DataExpressionSequence &v, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr) const
void compute_stochastic_state(stochastic_state &result, const stochastic_distribution &distribution, const DataExpressionSequence &next_state, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::enumerator_algorithm<> &enumerator) const
data::rewriter construct_rewriter(const Specification &lpsspec, bool remove_unused_rewrite_rules)
state find_representative(state &u0, const SummandSequence &summands, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator)
std::vector<state> generate_successors(const state &s0, const SummandSequence &summands, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator, const SummandSequence &confluent_summands = SummandSequence())
void generate_transitions(const explorer_summand &summand, const SummandSequence &confluent_summands, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::data_expression &condition, state_type &s1, atermpp::term_appl<data::data_expression> &key, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator, ReportTransition report_transition = ReportTransition())
bool is_confluent_tau(const multi_action &a)
bool less_equal(const data::data_expression &t0, const data::data_expression &t1, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr) 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, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator)
Specification preprocess(const Specification &lpsspec)
lps::multi_action rewrite_action(const lps::multi_action &a, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr) const

Rewrite action a, and put it back in place.

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, indexed_set_for_states_type &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(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_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_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())
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_thread(std::unique_ptr<todo_set> &todo, const std::size_t thread_index, std::atomic<std::size_t> &number_of_active_processes, std::atomic<std::size_t> &number_of_idle_processes, const SummandSequence &regular_summands, const SummandSequence &confluent_summands, indexed_set_for_states_type &discovered, DiscoverState discover_state, ExamineTransition examine_transition, StartState start_state, FinishState finish_state, data::rewriter thread_rewr, data::mutable_indexed_substitution<> thread_sigma)
std::vector<std::pair<lps::multi_action, state>> generate_transitions(const data::data_expression_list &init, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr)

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, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::data_expression &condition, state_type &d0, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator)

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

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

Generates outgoing transitions for a given state, using the global substitution, rewriter, enumerator and id_generator.

This function is not suitable to be used in parallel threads, but can only be used for pre or post processing.

std::vector<std::pair<lps::multi_action, state_type>> generate_transitions(const state &d0, data::mutable_indexed_substitution<> &sigma, data::rewriter &rewr, data::enumerator_algorithm<> &enumerator, data::enumerator_identifier_generator &id_generator)

Generates outgoing transitions for a given state.

state_type make_state(const state &s) const
const state_type &make_state(const stochastic_state &s) const
void make_timed_state(state &result, const state &s, const data::data_expression &t) const
data::data_expression_list process_parameter_values() const

Process parameter values for use in a single thread.

data::data_expression_list process_parameter_values(data::mutable_indexed_substitution<> &sigma) 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)
void set_process_parameter_values(const data::data_expression_list &values, data::mutable_indexed_substitution<> &sigma)
const indexed_set_for_states_type &state_map() const

Returns a mapping containing all discovered states.

~explorer() = default