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

#include <lts2pbes_rhs.h>

Inheritance diagram for mcrl2::pbes_system::detail::lts2pbes_parameters:
mcrl2::pbes_system::detail::lts2pbes_counter_example_parameters

Public Member Functions

 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

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 35 of file lts2pbes_rhs.h.

Constructor & Destructor Documentation

◆ lts2pbes_parameters()

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_ 
)
inline

Definition at line 43 of file lts2pbes_rhs.h.

Member Function Documentation

◆ rhs_may_must()

template<typename TermTraits >
pbes_expression mcrl2::pbes_system::detail::lts2pbes_parameters::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   
)
inline

Definition at line 53 of file lts2pbes_rhs.h.

Member Data Documentation

◆ id_generator

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

Definition at line 40 of file lts2pbes_rhs.h.

◆ lts0

const lts::lts_lts_t& mcrl2::pbes_system::detail::lts2pbes_parameters::lts0

Definition at line 38 of file lts2pbes_rhs.h.

◆ lts1

const lts2pbes_lts& mcrl2::pbes_system::detail::lts2pbes_parameters::lts1

Definition at line 39 of file lts2pbes_rhs.h.

◆ phi0

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

Definition at line 37 of file lts2pbes_rhs.h.

◆ pm

utilities::progress_meter& mcrl2::pbes_system::detail::lts2pbes_parameters::pm

Definition at line 41 of file lts2pbes_rhs.h.

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