mcrl2::pbes_system::detail::pre_srf_summand< allow_ce > Class Template Reference

#include <srf_pbes.h>

Public Member Functions
	pre_srf_summand (data::variable_list parameters, const pbes_expression &condition, propositional_variable_instantiation X)
const data::variable_list &	parameters () const
data::variable_list &	parameters ()
const condition_type &	condition () const
condition_type &	condition ()
const propositional_variable_instantiation &	variable () const
propositional_variable_instantiation &	variable ()
void	add_variables (const data::variable_list &variables)
void	add_condition (const pbes_expression &f)
pbes_expression	to_pbes (bool conjunctive) const

Protected Attributes
data::variable_list	m_parameters
condition_type	m_condition
propositional_variable_instantiation	m_X

Private Types
using	condition_type = std::conditional_t< allow_ce, pbes_expression, data::data_expression >

Detailed Description

template<bool allow_ce>
class mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >

A summand in a srf equation, if allow_ce is true then counter example information is allowed in the condition. This means that the condition contains propositional variables.

Definition at line 114 of file srf_pbes.h.

Member Typedef Documentation

condition_type

template<bool allow_ce>

using mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >::condition_type = std::conditional_t<allow_ce, pbes_expression, data::data_expression>

private

Definition at line 116 of file srf_pbes.h.

Constructor & Destructor Documentation

pre_srf_summand()

template<bool allow_ce>

mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >::pre_srf_summand ( data::variable_list  parameters, const pbes_expression &  condition, propositional_variable_instantiation  X  )

inline

Definition at line 123 of file srf_pbes.h.

Member Function Documentation

add_condition()

template<bool allow_ce>

void mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >::add_condition ( const pbes_expression &  f )

inline

Definition at line 153 of file srf_pbes.h.

add_variables()

template<bool allow_ce>

void mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >::add_variables ( const data::variable_list &  variables )

inline

Definition at line 151 of file srf_pbes.h.

condition() [1/2]

template<bool allow_ce>

condition_type & mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >::condition ( )

inline

Definition at line 145 of file srf_pbes.h.

condition() [2/2]

template<bool allow_ce>

const condition_type & mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >::condition ( ) const

inline

Definition at line 143 of file srf_pbes.h.

parameters() [1/2]

template<bool allow_ce>

data::variable_list & mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >::parameters ( )

inline

Definition at line 141 of file srf_pbes.h.

parameters() [2/2]

template<bool allow_ce>

const data::variable_list & mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >::parameters ( ) const

inline

Definition at line 139 of file srf_pbes.h.

to_pbes()

template<bool allow_ce>

pbes_expression mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >::to_pbes ( bool  conjunctive ) const

inline

Definition at line 165 of file srf_pbes.h.

variable() [1/2]

template<bool allow_ce>

propositional_variable_instantiation & mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >::variable ( )

inline

Definition at line 149 of file srf_pbes.h.

variable() [2/2]

template<bool allow_ce>

const propositional_variable_instantiation & mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >::variable ( ) const

inline

Definition at line 147 of file srf_pbes.h.

Member Data Documentation

m_condition

template<bool allow_ce>

condition_type mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >::m_condition

protected

Definition at line 119 of file srf_pbes.h.

m_parameters

template<bool allow_ce>

data::variable_list mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >::m_parameters

protected

Definition at line 118 of file srf_pbes.h.

m_X

template<bool allow_ce>

propositional_variable_instantiation mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >::m_X

protected

Definition at line 120 of file srf_pbes.h.

---

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

• pbes/include/mcrl2/pbes/srf_pbes.h