mcrl2::lps::next_state_generator

Include file:

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

Public types

type condition_arguments_t

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

type enumerator_iterator_t

typedef for enumerator_t::iterator

type enumerator_queue_t

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

type enumerator_t

typedef for data::enumerator_algorithm_with_iterator

type rewriter_t

typedef for data::rewriter

type state_probability_pair

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

type substitution_t

typedef for data::rewriter::substitution_type

type summand_enumeration_t

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

Protected attributes

summand_subset_t m_all_summands
substitution_t m_base_substitution
enumerator_t m_enumerator
data::enumerator_identifier_generator m_id_generator
transition_t::state_probability_list m_initial_states
data::variable_vector m_process_parameters
rewriter_t m_rewriter
stochastic_specification m_specification
substitution_t m_substitution
std::vector<summand_t> m_summands
bool 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, summand_subset_t &summand_subset, 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.

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()