#include <decluster.h>

Inheritance diagram for mcrl2::lps::decluster_algorithm< Specification >:

Public Member Functions
	decluster_algorithm (Specification &spec)

void	run ()

Public Member Functions inherited from mcrl2::lps::detail::lps_algorithm< Specification >
	lps_algorithm (Specification &spec)
	Constructor.

bool	verbose () const
	Flag for verbose output.

data::data_expression	next_state (const action_summand &s, const data::variable &v) const
	Applies the next state substitution to the variable v.

void	instantiate_free_variables ()
	Attempts to eliminate the free variables of the specification, by substituting a constant value for them. If no constant value is found for one of the variables, an exception is thrown.

void	remove_parameters (const std::set< data::variable > &to_be_removed)
	Removes formal parameters from the specification.

void	remove_singleton_sorts ()
	Removes parameters with a singleton sort.

void	remove_trivial_summands ()
	Removes summands with condition equal to false.

void	remove_unused_summand_variables ()
	Removes unused summand variables.

Protected Member Functions
template<typename SummandType , typename OutIter >
void	decluster_summand (const SummandType &summand, OutIter &out)

Protected Member Functions inherited from mcrl2::lps::detail::lps_algorithm< Specification >
void	sumelm_find_variables (const action_summand &s, std::set< data::variable > &result) const

void	sumelm_find_variables (const deadlock_summand &s, std::set< data::variable > &result) const

void	summand_remove_unused_summand_variables (SummandType &summand_)

Private Types
using	super = typename detail::lps_algorithm< Specification >

using	process_type = typename Specification::process_type

using	action_summand_type = typename process_type::action_summand_type

using	action_summand_vector_type = std::vector< action_summand_type >

Additional Inherited Members
Protected Attributes inherited from mcrl2::lps::detail::lps_algorithm< Specification >
Specification &	m_spec
	The specification that is processed by the algorithm.

Detailed Description

template<typename Specification>
class mcrl2::lps::decluster_algorithm< Specification >

Definition at line 22 of file decluster.h.