mCRL2
Loading...
Searching...
No Matches
Public Member Functions | Public Attributes | List of all members
mcrl2::pres_system::detail::lps2pres_parameters Struct Reference

#include <lps2pres_rhs.h>

Public Member Functions

 lps2pres_parameters (const state_formulas::state_formula &phi0_, const lps::stochastic_linear_process &lps_, data::set_identifier_generator &id_generator_, const data::variable &T_)
 
bool is_timed () const
 
template<typename TermTraits >
pres_expression rhs_may_must (bool is_must, const data::variable_list &y, const pres_expression &left, const pres_expression &right, const lps::multi_action &, const data::assignment_list &, const lps::stochastic_distribution &dist, TermTraits)
 

Public Attributes

const state_formulas::state_formula & phi0
 
const lps::stochastic_linear_process & lps
 
data::set_identifier_generator & id_generator
 
const data::variable & T
 

Detailed Description

Definition at line 26 of file lps2pres_rhs.h.

Constructor & Destructor Documentation

◆ lps2pres_parameters()

mcrl2::pres_system::detail::lps2pres_parameters::lps2pres_parameters ( const state_formulas::state_formula &  phi0_,
const lps::stochastic_linear_process &  lps_,
data::set_identifier_generator &  id_generator_,
const data::variable &  T_ 
)
inline

Definition at line 33 of file lps2pres_rhs.h.

Member Function Documentation

◆ is_timed()

bool mcrl2::pres_system::detail::lps2pres_parameters::is_timed ( ) const
inline

Definition at line 41 of file lps2pres_rhs.h.

◆ rhs_may_must()

template<typename TermTraits >
pres_expression mcrl2::pres_system::detail::lps2pres_parameters::rhs_may_must ( bool  is_must,
const data::variable_list &  y,
const pres_expression &  left,
const pres_expression &  right,
const lps::multi_action &  ,
const data::assignment_list &  ,
const lps::stochastic_distribution &  dist,
TermTraits   
)
inline

Definition at line 47 of file lps2pres_rhs.h.

Member Data Documentation

◆ id_generator

data::set_identifier_generator& mcrl2::pres_system::detail::lps2pres_parameters::id_generator

Definition at line 30 of file lps2pres_rhs.h.

◆ lps

const lps::stochastic_linear_process& mcrl2::pres_system::detail::lps2pres_parameters::lps

Definition at line 29 of file lps2pres_rhs.h.

◆ phi0

const state_formulas::state_formula& mcrl2::pres_system::detail::lps2pres_parameters::phi0

Definition at line 28 of file lps2pres_rhs.h.

◆ T

const data::variable& mcrl2::pres_system::detail::lps2pres_parameters::T

Definition at line 31 of file lps2pres_rhs.h.

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