mcrl2::lps::next_state_generator

Include file:

#include "mcrl2/lps/next_state_generator.h

class mcrl2::lps::next_state_generator

Public types

type mcrl2::lps::next_state_generator::condition_arguments_t

typedef for atermpp::term_appl< data::data_expression >

type mcrl2::lps::next_state_generator::enumerator_iterator_t

typedef for enumerator_t::iterator

type mcrl2::lps::next_state_generator::enumerator_queue_t

typedef for data::enumerator_queue< data::enumerator_list_element_with_substitution<> >

type mcrl2::lps::next_state_generator::enumerator_t

typedef for data::enumerator_algorithm_with_iterator

type mcrl2::lps::next_state_generator::rewriter_t

typedef for data::rewriter

type mcrl2::lps::next_state_generator::state_probability_pair

typedef for mcrl2::lps::state_probability_pair< lps::state, lps::probabilistic_data_expression >

type mcrl2::lps::next_state_generator::substitution_t

typedef for data::rewriter::substitution_type

type mcrl2::lps::next_state_generator::summand_enumeration_t

typedef for std::list< data::data_expression_list >

Protected attributes

summand_subset_t mcrl2::lps::next_state_generator::m_all_summands

substitution_t mcrl2::lps::next_state_generator::m_base_substitution

enumerator_t mcrl2::lps::next_state_generator::m_enumerator

data::enumerator_identifier_generator mcrl2::lps::next_state_generator::m_id_generator

transition_t::state_probability_list mcrl2::lps::next_state_generator::m_initial_states

data::variable_vector mcrl2::lps::next_state_generator::m_process_parameters

rewriter_t mcrl2::lps::next_state_generator::m_rewriter

stochastic_specification mcrl2::lps::next_state_generator::m_specification

substitution_t mcrl2::lps::next_state_generator::m_substitution

std::vector<summand_t> mcrl2::lps::next_state_generator::m_summands

bool mcrl2::lps::next_state_generator::m_use_enumeration_caching

Public member functions

iterator begin(const state &state, enumerator_queue_t *enumeration_queue)

Returns an iterator for generating the successors of the given state.

iterator begin(const state &state, std::size_t summand_index, enumerator_queue_t *enumeration_queue)

Returns an iterator for generating the successors of the given state. Only the successors with respect to the summand with the given index are generated.

iterator begin(const state &state, summand_subset_t &summand_subset, enumerator_queue_t *enumeration_queue)

Returns an iterator for generating the successors of the given state.

const next_state_generator::transition_t::state_probability_list calculate_distribution(const stochastic_distribution &dist, const data::data_expression_vector &state_args, substitution_t &sigma)

iterator end()

Returns an iterator pointing to the end of a next state list.

summand_subset_t &full_subset()

Returns a reference to the summand subset containing all summands.

rewriter_t &get_rewriter()

Returns the rewriter associated with this generator.

const transition_t::state_probability_list &initial_states() const

Gets the initial state.

next_state_generator(const stochastic_specification &spec, const data::rewriter &rewriter, const substitution_t &base_substitution = data::mutable_indexed_substitution<>(), bool use_enumeration_caching = false, bool use_summand_pruning = false)

Constructor.

Parameters:

• spec The process specification.
• rewriter The rewriter used.
• base_substitution A substitution from variables to terms in normal form, used to replace variables occurring the in the specification. The rhs’s in the substitution are assumed to be in normal form. It can be useful to replace closed expressions in the lps by variables, and put there rhs’s in the base_substitution to avoid rewriting these expressions repeatedly.
• use_enumeration_caching Cache intermediate enumeration results.
• use_summand_pruning Preprocess summands using pruning strategy.

~next_state_generator()