mCRL2
Loading...
Searching...
No Matches
mcrl2::pbes_system::absinthe_algorithm Struct Reference

#include <absinthe.h>

Classes

struct  absinthe_data_expression_builder
 
struct  absinthe_sort_expression_builder
 
struct  lift_equation_1_2
 
struct  lift_equation_2_3
 
struct  lift_function_symbol_1_2
 
struct  lift_function_symbol_2_3
 
struct  make_data_expression_set
 
struct  make_set
 
struct  sort_function
 

Public Types

typedef std::map< data::sort_expression, data::sort_expressionsort_expression_substitution_map
 
typedef std::map< data::function_symbol, data::function_symbolfunction_symbol_substitution_map
 
typedef std::map< data::sort_expression, data::function_symbolabstraction_map
 

Public Member Functions

sort_expression_substitution_map parse_sort_expression_mapping (const std::string &text, const data::data_specification &dataspec)
 
void parse_right_hand_sides (const std::string &text, data::data_specification &dataspec)
 
function_symbol_substitution_map parse_function_symbol_mapping (const std::string &text, const data::data_specification &dataspec)
 
abstraction_map parse_abstraction_map (const std::string &text)
 
template<typename Map >
std::string print_mapping (const Map &m)
 
void check_consistency (const data::sort_expression &s, const data::sort_expression &t, const data::function_symbol &f, sort_expression_substitution_map &sigmaS) const
 
void check_consistency (const data::function_symbol &f1, const data::function_symbol &f2, sort_expression_substitution_map &sigmaS) const
 
void lift_data_specification (const pbes &p, const abstraction_map &sigmaH, const sort_expression_substitution_map &sigmaS, function_symbol_substitution_map &sigmaF, data::data_specification &dataspec)
 
void print_fsvec (const data::function_symbol_vector &v, const std::string &msg) const
 
void print_fsmap (const function_symbol_substitution_map &v, const std::string &msg) const
 
void enable_logging ()
 
void run (pbes &p, const std::string &abstraction_text, bool is_over_approximation)
 

Public Attributes

data::set_identifier_generator m_generator
 

Detailed Description

Definition at line 122 of file absinthe.h.

Member Typedef Documentation

◆ abstraction_map

◆ function_symbol_substitution_map

◆ sort_expression_substitution_map

Member Function Documentation

◆ check_consistency() [1/2]

void mcrl2::pbes_system::absinthe_algorithm::check_consistency ( const data::function_symbol f1,
const data::function_symbol f2,
sort_expression_substitution_map sigmaS 
) const
inline

Definition at line 832 of file absinthe.h.

◆ check_consistency() [2/2]

void mcrl2::pbes_system::absinthe_algorithm::check_consistency ( const data::sort_expression s,
const data::sort_expression t,
const data::function_symbol f,
sort_expression_substitution_map sigmaS 
) const
inline

Definition at line 817 of file absinthe.h.

◆ enable_logging()

void mcrl2::pbes_system::absinthe_algorithm::enable_logging ( )
inline

Definition at line 951 of file absinthe.h.

◆ lift_data_specification()

void mcrl2::pbes_system::absinthe_algorithm::lift_data_specification ( const pbes p,
const abstraction_map sigmaH,
const sort_expression_substitution_map sigmaS,
function_symbol_substitution_map sigmaF,
data::data_specification dataspec 
)
inline

Definition at line 864 of file absinthe.h.

◆ parse_abstraction_map()

abstraction_map mcrl2::pbes_system::absinthe_algorithm::parse_abstraction_map ( const std::string &  text)
inline

Definition at line 462 of file absinthe.h.

◆ parse_function_symbol_mapping()

function_symbol_substitution_map mcrl2::pbes_system::absinthe_algorithm::parse_function_symbol_mapping ( const std::string &  text,
const data::data_specification dataspec 
)
inline

Definition at line 441 of file absinthe.h.

◆ parse_right_hand_sides()

void mcrl2::pbes_system::absinthe_algorithm::parse_right_hand_sides ( const std::string &  text,
data::data_specification dataspec 
)
inline

Definition at line 424 of file absinthe.h.

◆ parse_sort_expression_mapping()

sort_expression_substitution_map mcrl2::pbes_system::absinthe_algorithm::parse_sort_expression_mapping ( const std::string &  text,
const data::data_specification dataspec 
)
inline

Definition at line 406 of file absinthe.h.

◆ print_fsmap()

void mcrl2::pbes_system::absinthe_algorithm::print_fsmap ( const function_symbol_substitution_map v,
const std::string &  msg 
) const
inline

Definition at line 942 of file absinthe.h.

◆ print_fsvec()

void mcrl2::pbes_system::absinthe_algorithm::print_fsvec ( const data::function_symbol_vector v,
const std::string &  msg 
) const
inline

Definition at line 933 of file absinthe.h.

◆ print_mapping()

template<typename Map >
std::string mcrl2::pbes_system::absinthe_algorithm::print_mapping ( const Map &  m)
inline

Definition at line 807 of file absinthe.h.

◆ run()

void mcrl2::pbes_system::absinthe_algorithm::run ( pbes p,
const std::string &  abstraction_text,
bool  is_over_approximation 
)
inline

Definition at line 956 of file absinthe.h.

Member Data Documentation

◆ m_generator

data::set_identifier_generator mcrl2::pbes_system::absinthe_algorithm::m_generator

Definition at line 129 of file absinthe.h.


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