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

#include <lts2pbes_rhs.h>

Inheritance diagram for mcrl2::pbes_system::detail::lts2pbes_counter_example_parameters:
mcrl2::pbes_system::detail::lts2pbes_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
 
 lts2pbes_counter_example_parameters (const state_formulas::state_formula &phi0, const lts::lts_lts_t &lts0, const lts2pbes_lts &lts1, data::set_identifier_generator &id_generator, utilities::progress_meter &pm)
 
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 pbes_expression &left, const pbes_expression &right, std::size_t i, const lps::multi_action &a, lts2pbes_state_type s, lts2pbes_state_type t, TermTraits)
 
- Public Member Functions inherited from mcrl2::pbes_system::detail::lts2pbes_parameters
 lts2pbes_parameters (const state_formulas::state_formula &phi0_, const lts::lts_lts_t &lts0_, const lts2pbes_lts &lts1_, data::set_identifier_generator &id_generator_, utilities::progress_meter &pm_)
 
template<typename TermTraits >
pbes_expression rhs_may_must (bool is_must, const pbes_expression &left, const pbes_expression &right, std::size_t, const lps::multi_action &, lts2pbes_state_type, lts2pbes_state_type, TermTraits)
 

Public Attributes

std::vector< propositional_variable > Zpos
 
std::vector< propositional_variable > Zneg
 
data::variable_list s_list
 
data::variable_list t_list
 
- Public Attributes inherited from mcrl2::pbes_system::detail::lts2pbes_parameters
const state_formulas::state_formula & phi0
 
const lts::lts_lts_t & lts0
 
const lts2pbes_lts & lts1
 
data::set_identifier_generator & id_generator
 
utilities::progress_meter & pm
 

Detailed Description

Definition at line 76 of file lts2pbes_rhs.h.

Constructor & Destructor Documentation

◆ lts2pbes_counter_example_parameters()

mcrl2::pbes_system::detail::lts2pbes_counter_example_parameters::lts2pbes_counter_example_parameters ( const state_formulas::state_formula &  phi0,
const lts::lts_lts_t &  lts0,
const lts2pbes_lts &  lts1,
data::set_identifier_generator &  id_generator,
utilities::progress_meter &  pm 
)
inline

Definition at line 137 of file lts2pbes_rhs.h.

Member Function Documentation

◆ action_expressions()

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

Definition at line 99 of file lts2pbes_rhs.h.

◆ action_variables()

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

Definition at line 84 of file lts2pbes_rhs.h.

◆ equal_to()

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

Definition at line 165 of file lts2pbes_rhs.h.

◆ equations()

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

Definition at line 111 of file lts2pbes_rhs.h.

◆ multi_action_name()

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

Definition at line 127 of file lts2pbes_rhs.h.

◆ rhs_may_must()

template<typename TermTraits >
pbes_expression mcrl2::pbes_system::detail::lts2pbes_counter_example_parameters::rhs_may_must ( bool  is_must,
const pbes_expression &  left,
const pbes_expression &  right,
std::size_t  i,
const lps::multi_action &  a,
lts2pbes_state_type  s,
lts2pbes_state_type  t,
TermTraits   
)
inline

Definition at line 178 of file lts2pbes_rhs.h.

Member Data Documentation

◆ s_list

data::variable_list mcrl2::pbes_system::detail::lts2pbes_counter_example_parameters::s_list

Definition at line 80 of file lts2pbes_rhs.h.

◆ t_list

data::variable_list mcrl2::pbes_system::detail::lts2pbes_counter_example_parameters::t_list

Definition at line 81 of file lts2pbes_rhs.h.

◆ Zneg

std::vector<propositional_variable> mcrl2::pbes_system::detail::lts2pbes_counter_example_parameters::Zneg

Definition at line 79 of file lts2pbes_rhs.h.

◆ Zpos

std::vector<propositional_variable> mcrl2::pbes_system::detail::lts2pbes_counter_example_parameters::Zpos

Definition at line 78 of file lts2pbes_rhs.h.

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