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

#include <lps2pbes_rhs.h>

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

Public Member Functions

data::variable_list action_variables (const process::action_list &actions) const
 
data::data_expression_list action_expressions (const process::action_list &actions) const
 
std::vector< pbes_equation > equations () const
 
std::string multi_action_name (const lps::multi_action &a) const
 
 lps2pbes_counter_example_parameters (const state_formulas::state_formula &phi0, const lps::stochastic_linear_process &lps, data::set_identifier_generator &id_generator, const data::variable &T)
 
data::data_expression equal_to (const data::variable_list &d, const data::data_expression_list &e) 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 &ai, const data::assignment_list &gi, TermTraits)
 
- Public Member Functions inherited from 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_)
 
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

data::variable_list d1
 
data::mutable_map_substitution sigma
 
std::map< lps::multi_action, propositional_variable > Zpos
 
std::map< lps::multi_action, propositional_variable > Zneg
 
- Public Attributes inherited from mcrl2::pbes_system::detail::lps2pbes_parameters
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 68 of file lps2pbes_rhs.h.

Constructor & Destructor Documentation

◆ lps2pbes_counter_example_parameters()

mcrl2::pbes_system::detail::lps2pbes_counter_example_parameters::lps2pbes_counter_example_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 129 of file lps2pbes_rhs.h.

Member Function Documentation

◆ action_expressions()

data::data_expression_list mcrl2::pbes_system::detail::lps2pbes_counter_example_parameters::action_expressions ( const process::action_list &  actions) const
inline

Definition at line 91 of file lps2pbes_rhs.h.

◆ action_variables()

data::variable_list mcrl2::pbes_system::detail::lps2pbes_counter_example_parameters::action_variables ( const process::action_list &  actions) const
inline

Definition at line 76 of file lps2pbes_rhs.h.

◆ equal_to()

data::data_expression mcrl2::pbes_system::detail::lps2pbes_counter_example_parameters::equal_to ( const data::variable_list &  d,
const data::data_expression_list &  e 
) const
inline

Definition at line 153 of file lps2pbes_rhs.h.

◆ equations()

std::vector< pbes_equation > mcrl2::pbes_system::detail::lps2pbes_counter_example_parameters::equations ( ) const
inline

Definition at line 103 of file lps2pbes_rhs.h.

◆ multi_action_name()

std::string mcrl2::pbes_system::detail::lps2pbes_counter_example_parameters::multi_action_name ( const lps::multi_action &  a) const
inline

Definition at line 119 of file lps2pbes_rhs.h.

◆ rhs_may_must()

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

Definition at line 166 of file lps2pbes_rhs.h.

Member Data Documentation

◆ d1

data::variable_list mcrl2::pbes_system::detail::lps2pbes_counter_example_parameters::d1

Definition at line 70 of file lps2pbes_rhs.h.

◆ sigma

data::mutable_map_substitution mcrl2::pbes_system::detail::lps2pbes_counter_example_parameters::sigma

Definition at line 71 of file lps2pbes_rhs.h.

◆ Zneg

std::map<lps::multi_action, propositional_variable> mcrl2::pbes_system::detail::lps2pbes_counter_example_parameters::Zneg

Definition at line 73 of file lps2pbes_rhs.h.

◆ Zpos

std::map<lps::multi_action, propositional_variable> mcrl2::pbes_system::detail::lps2pbes_counter_example_parameters::Zpos

Definition at line 72 of file lps2pbes_rhs.h.

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