mcrl2::lps::detail::make_timed_lps_summand< IdentifierGenerator > Struct Template Reference

Adds a time parameter t to s if needed and returns the result. The time t is chosen such that it doesn't appear in context. More...

#include <make_timed_lps.h>

Public Member Functions
	make_timed_lps_summand (IdentifierGenerator &generator)
void	operator() (deadlock_summand &s) const
	Adds time to the summand s (either an action or a deadlock summand)
void	operator() (action_summand &s) const
	Adds time to the summand s (either an action or a deadlock summand)

Public Attributes
IdentifierGenerator &	m_generator

Detailed Description

template<typename IdentifierGenerator>
struct mcrl2::lps::detail::make_timed_lps_summand< IdentifierGenerator >

Adds a time parameter t to s if needed and returns the result. The time t is chosen such that it doesn't appear in context.

Definition at line 26 of file make_timed_lps.h.

Constructor & Destructor Documentation

make_timed_lps_summand()

template<typename IdentifierGenerator >

mcrl2::lps::detail::make_timed_lps_summand< IdentifierGenerator >::make_timed_lps_summand ( IdentifierGenerator &  generator )

inline

Definition at line 30 of file make_timed_lps.h.

Member Function Documentation

operator()() [1/2]

template<typename IdentifierGenerator >

void mcrl2::lps::detail::make_timed_lps_summand< IdentifierGenerator >::operator() ( action_summand &  s ) const

inline

Adds time to the summand s (either an action or a deadlock summand)

Parameters

s	An action summand

Definition at line 51 of file make_timed_lps.h.

operator()() [2/2]

template<typename IdentifierGenerator >

void mcrl2::lps::detail::make_timed_lps_summand< IdentifierGenerator >::operator() ( deadlock_summand &  s ) const

inline

Adds time to the summand s (either an action or a deadlock summand)

Parameters

s	An action summand

Definition at line 36 of file make_timed_lps.h.

Member Data Documentation

m_generator

template<typename IdentifierGenerator >

IdentifierGenerator& mcrl2::lps::detail::make_timed_lps_summand< IdentifierGenerator >::m_generator

Definition at line 28 of file make_timed_lps.h.

---

The documentation for this struct was generated from the following file:

• lps/include/mcrl2/lps/detail/make_timed_lps.h