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

#include <lps2pbes_rhs.h>

Inheritance diagram for mcrl2::pbes_system::detail::lps2pbes_parameters:
mcrl2::pbes_system::detail::lps2pbes_counter_example_parameters

Public Member Functions

 lps2pbes_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 >
pbes_expression rhs_may_must (bool is_must, const data::variable_list &y, const pbes_expression &left, const pbes_expression &right, const lps::multi_action &, const data::assignment_list &, 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 lps2pbes_rhs.h.

Constructor & Destructor Documentation

◆ lps2pbes_parameters()

mcrl2::pbes_system::detail::lps2pbes_parameters::lps2pbes_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 lps2pbes_rhs.h.

Member Function Documentation

◆ is_timed()

bool mcrl2::pbes_system::detail::lps2pbes_parameters::is_timed ( ) const
inline

Definition at line 41 of file lps2pbes_rhs.h.

◆ rhs_may_must()

template<typename TermTraits >
pbes_expression mcrl2::pbes_system::detail::lps2pbes_parameters::rhs_may_must ( bool  is_must,
const data::variable_list &  y,
const pbes_expression &  left,
const pbes_expression &  right,
const lps::multi_action &  ,
const data::assignment_list &  ,
TermTraits   
)
inline

Definition at line 47 of file lps2pbes_rhs.h.

Member Data Documentation

◆ id_generator

data::set_identifier_generator& mcrl2::pbes_system::detail::lps2pbes_parameters::id_generator

Definition at line 30 of file lps2pbes_rhs.h.

◆ lps

const lps::stochastic_linear_process& mcrl2::pbes_system::detail::lps2pbes_parameters::lps

Definition at line 29 of file lps2pbes_rhs.h.

◆ phi0

const state_formulas::state_formula& mcrl2::pbes_system::detail::lps2pbes_parameters::phi0

Definition at line 28 of file lps2pbes_rhs.h.

◆ T

const data::variable& mcrl2::pbes_system::detail::lps2pbes_parameters::T

Definition at line 31 of file lps2pbes_rhs.h.

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