mcrl2::lps::suminst_algorithm

Include file:

#include "mcrl2/lps/suminst.h

class mcrl2::lps::suminst_algorithm

Private types

type mcrl2::lps::suminst_algorithm::action_summand_type

typedef for process_type::action_summand_type

type mcrl2::lps::suminst_algorithm::action_summand_vector_type

typedef for std::vector< action_summand_type >

type mcrl2::lps::suminst_algorithm::enumerator_element

typedef for data::enumerator_list_element_with_substitution

type mcrl2::lps::suminst_algorithm::process_type

typedef for Specification::process_type

type mcrl2::lps::suminst_algorithm::super

typedef for detail::lps_algorithm< Specification >

Protected attributes

std::size_t mcrl2::lps::suminst_algorithm::m_added

std::size_t mcrl2::lps::suminst_algorithm::m_deleted

data::enumerator_algorithm mcrl2::lps::suminst_algorithm::m_enumerator

data::enumerator_identifier_generator mcrl2::lps::suminst_algorithm::m_id_generator

std::size_t mcrl2::lps::suminst_algorithm::m_processed

Statistiscs for verbose output.

DataRewriter mcrl2::lps::suminst_algorithm::m_rewriter

Rewriter.

std::set<data::sort_expression> mcrl2::lps::suminst_algorithm::m_sorts

Sorts to be instantiated.

bool mcrl2::lps::suminst_algorithm::m_tau_summands_only

Only instantiate tau summands.

Protected member functions

std::size_t instantiate_summand(const SummandType &s, Container &result)

bool must_instantiate(const action_summand_type &summand)

bool must_instantiate(const deadlock_summand&)

void run(const SummandListType &list, Container &result)

Public member functions

void run()

suminst_algorithm(Specification &spec, DataRewriter &r, std::set<data::sort_expression> sorts = std::set<data::sort_expression>(), bool tau_summands_only = false)