mCRL2
Loading...
Searching...
No Matches
Public Member Functions | Protected Attributes | List of all members
mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce > Class Template Reference

#include <srf_pbes.h>

Public Member Functions

 pre_srf_pbes ()=default
 
 pre_srf_pbes (const data::data_specification &dataspec, std::set< data::variable > global_variables, std::vector< pre_srf_equation< allow_ce > > equations, propositional_variable_instantiation initial_state)
 
const std::vector< pre_srf_equation< allow_ce > > & equations () const
 
std::vector< pre_srf_equation< allow_ce > > & equations ()
 
const propositional_variable_instantiation & initial_state () const
 
propositional_variable_instantiation & initial_state ()
 
const data::data_specification & data () const
 
data::data_specification & data ()
 
const std::set< data::variable > & global_variables () const
 
std::set< data::variable > & global_variables ()
 
pbes to_pbes () const
 
void make_total ()
 

Protected Attributes

data::data_specification m_dataspec
 
std::set< data::variable > m_global_variables
 
std::vector< pre_srf_equation< allow_ce > > m_equations
 
propositional_variable_instantiation m_initial_state
 

Detailed Description

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

explicit representation of a pbes in SRF format

If allow_ce is true, then counter example expressions are allowed in the PBES. We refer to this as kind of pre_srf. When the counter example information is replaced by true or false in every condition, we obtain a srf.

Definition at line 792 of file srf_pbes.h.

Constructor & Destructor Documentation

◆ pre_srf_pbes() [1/2]

template<bool allow_ce>
mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::pre_srf_pbes ( )
default

◆ pre_srf_pbes() [2/2]

template<bool allow_ce>
mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::pre_srf_pbes ( const data::data_specification &  dataspec,
std::set< data::variable >  global_variables,
std::vector< pre_srf_equation< allow_ce > >  equations,
propositional_variable_instantiation  initial_state 
)
inline

Definition at line 803 of file srf_pbes.h.

Member Function Documentation

◆ data() [1/2]

template<bool allow_ce>
data::data_specification & mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::data ( )
inline

Definition at line 823 of file srf_pbes.h.

◆ data() [2/2]

template<bool allow_ce>
const data::data_specification & mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::data ( ) const
inline

Definition at line 821 of file srf_pbes.h.

◆ equations() [1/2]

template<bool allow_ce>
std::vector< pre_srf_equation< allow_ce > > & mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::equations ( )
inline

Definition at line 815 of file srf_pbes.h.

◆ equations() [2/2]

template<bool allow_ce>
const std::vector< pre_srf_equation< allow_ce > > & mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::equations ( ) const
inline

Definition at line 813 of file srf_pbes.h.

◆ global_variables() [1/2]

template<bool allow_ce>
std::set< data::variable > & mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::global_variables ( )
inline

Definition at line 827 of file srf_pbes.h.

◆ global_variables() [2/2]

template<bool allow_ce>
const std::set< data::variable > & mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::global_variables ( ) const
inline

Definition at line 825 of file srf_pbes.h.

◆ initial_state() [1/2]

template<bool allow_ce>
propositional_variable_instantiation & mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::initial_state ( )
inline

Definition at line 819 of file srf_pbes.h.

◆ initial_state() [2/2]

template<bool allow_ce>
const propositional_variable_instantiation & mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::initial_state ( ) const
inline

Definition at line 817 of file srf_pbes.h.

◆ make_total()

template<bool allow_ce>
void mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::make_total ( )
inline

Definition at line 841 of file srf_pbes.h.

◆ to_pbes()

template<bool allow_ce>
pbes mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::to_pbes ( ) const
inline

Definition at line 829 of file srf_pbes.h.

Member Data Documentation

◆ m_dataspec

template<bool allow_ce>
data::data_specification mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::m_dataspec
protected

Definition at line 795 of file srf_pbes.h.

◆ m_equations

template<bool allow_ce>
std::vector<pre_srf_equation<allow_ce> > mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::m_equations
protected

Definition at line 797 of file srf_pbes.h.

◆ m_global_variables

template<bool allow_ce>
std::set<data::variable> mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::m_global_variables
protected

Definition at line 796 of file srf_pbes.h.

◆ m_initial_state

template<bool allow_ce>
propositional_variable_instantiation mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >::m_initial_state
protected

Definition at line 798 of file srf_pbes.h.

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