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 next_state_generator

friend class next_state_generator::iterator

Private attributes

next_state_generator *m_generator
std::vector<std::size_t> m_pruning_parameters
substitution_t m_pruning_substitution
pruning_tree_node_t m_pruning_tree
std::vector<std::size_t> m_summands
bool 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)