mcrl2::lps::next_state_generator::summand_subset_t

Include file:

#include "mcrl2/lps/next_state_generator.h

class mcrl2::lps::next_state_generator::summand_subset_t

Friends

friend class mcrl2::lps::next_state_generator::summand_subset_t::next_state_generator

friend class mcrl2::lps::next_state_generator::summand_subset_t::next_state_generator::iterator

Private attributes

next_state_generator *mcrl2::lps::next_state_generator::summand_subset_t::m_generator

std::vector<std::size_t> mcrl2::lps::next_state_generator::summand_subset_t::m_pruning_parameters

substitution_t mcrl2::lps::next_state_generator::summand_subset_t::m_pruning_substitution

pruning_tree_node_t mcrl2::lps::next_state_generator::summand_subset_t::m_pruning_tree

std::vector<std::size_t> mcrl2::lps::next_state_generator::summand_subset_t::m_summands

bool mcrl2::lps::next_state_generator::summand_subset_t::m_use_summand_pruning

Public member functions

summand_subset_t()

Trivial constructor. Constructs an invalid command subset.

summand_subset_t(next_state_generator *generator, bool use_summand_pruning)

Constructs the full summand subset for the given generator.

summand_subset_t(next_state_generator *generator, const stochastic_action_summand_vector &summands, bool use_summand_pruning)

Constructs the summand subset containing the given commands.

Private static member functions

bool summand_set_contains(const std::set<stochastic_action_summand> &summand_set, const summand_t &summand)

Private member functions

atermpp::detail::shared_subset<next_state_generator::summand_t>::iterator begin(const lps::state &state)

void build_pruning_parameters(const stochastic_action_summand_vector &summands)

bool is_not_false(const summand_t &summand)