mCRL2
Loading...
Searching...
No Matches
mcrl2::core Namespace Reference

Namespaces

namespace  detail
 

Classes

class  add_binding
 Traverser that defines functions for maintaining bound variables. More...
 
class  apply_builder
 
class  apply_builder_arg1
 
class  apply_builder_arg2
 
struct  apply_traverser
 
struct  builder
 expression builder that visits all sub expressions More...
 
struct  default_parser_actions
 
struct  parse_node
 Wrapper for D_ParseNode. More...
 
class  parse_node_exception
 
class  parse_node_unexpected_exception
 
struct  parser
 Wrapper for D_Parser and its corresponding D_ParserTables. More...
 
struct  parser_actions
 
struct  parser_table
 Wrapper for D_ParserTables. More...
 
struct  stream_printer
 Prints the object x to a stream. More...
 
struct  term_traits
 Contains type information for terms. More...
 
struct  term_traits< data::data_expression >
 Contains type information for data expressions. More...
 
struct  term_traits< pbes_system::pbes_expression >
 Contains type information for pbes expressions. More...
 
struct  term_traits< pres_system::pres_expression >
 Contains type information for pres expressions. More...
 
struct  term_traits_optimized
 Contains type information for terms. More...
 
struct  term_traits_optimized< pbes_system::pbes_expression >
 Contains type information for pbes expressions. More...
 
struct  term_traits_optimized< pres_system::pres_expression >
 Contains type information for pres expressions. More...
 
struct  traverser
 expression traverser that visits all sub expressions More...
 
struct  update_apply_builder
 
class  update_apply_builder_arg1
 

Typedefs

typedef atermpp::aterm_string identifier_string
 String type of the LPS library. Identifier strings are represented internally as ATerms.
 
typedef atermpp::term_list< identifier_stringidentifier_string_list
 \brief list of identifier_strings
 
typedef std::vector< identifier_stringidentifier_string_vector
 \brief vector of identifier_strings
 

Enumerations

enum  print_format_type { print_default , print_internal }
 print_format_type represents the available pretty print formats More...
 

Functions

void msg (const std::string &)
 
template<template< class > class Builder>
apply_builder< Builder > make_apply_builder ()
 
template<template< class > class Builder, class Arg1 >
apply_builder_arg1< Builder, Arg1 > make_apply_builder_arg1 (const Arg1 &arg1)
 
template<template< class > class Builder, class Arg1 , class Arg2 >
apply_builder_arg2< Builder, Arg1, Arg2 > make_apply_builder_arg2 (const Arg1 &arg1, const Arg2 &arg2)
 
template<template< class > class Builder, class Function >
update_apply_builder< Builder, Function > make_update_apply_builder (const Function &f)
 
template<template< class > class Builder, class Function , class Arg1 >
update_apply_builder_arg1< Builder, Function, Arg1 > make_update_apply_builder_arg1 (const Function &f)
 
std::string pp (const identifier_string &x)
 
std::ostream & operator<< (std::ostream &out, const identifier_string &x)
 
void swap (identifier_string &t1, identifier_string &t2)
 \brief swap overload
 
bool is_identifier_string (const atermpp::aterm &t)
 Tests if a term is an identifier string.
 
identifier_string empty_identifier_string ()
 Provides the empty identifier string.
 
atermpp::aterm load_aterm (std::istream &stream, bool binary=true, const std::string &format="aterm", const std::string &source="", atermpp::aterm_transformer transformer=atermpp::identity)
 Attempts to read an aterm from a stream.
 
template<typename T >
void print_aterm (const T &)
 
template<>
void print_aterm (const atermpp::aterm_appl &x)
 
identifier_string parse_identifier (const std::string &text)
 Parse an identifier.
 
bool is_user_identifier (std::string const &s)
 
void warn_and_or (const parse_node &)
 Prints a warning for each occurrence of 'x && y || z' in the parse tree.
 
void warn_left_merge_merge (const parse_node &)
 Prints a warning for each occurrence of 'x ||_ y || z' in the parse tree.
 
template<typename T >
std::string pp (const T &x)
 Returns a string representation of the object x.
 
std::string pp_format_to_string (const print_format_type pp_format)
 Print string representation of pretty print format.
 
std::ostream & operator<< (std::ostream &os, const print_format_type &pp_format)
 
print_format_type parse_pp_format (const std::string &s)
 
std::istream & operator>> (std::istream &is, print_format_type &f)
 
template<template< class > class Traverser>
apply_traverser< Traverser > make_apply_traverser ()
 

Typedef Documentation

◆ identifier_string

String type of the LPS library. Identifier strings are represented internally as ATerms.

Definition at line 26 of file identifier_string.h.

◆ identifier_string_list

\brief list of identifier_strings

Definition at line 30 of file identifier_string.h.

◆ identifier_string_vector

\brief vector of identifier_strings

Definition at line 33 of file identifier_string.h.

Enumeration Type Documentation

◆ print_format_type

print_format_type represents the available pretty print formats

Enumerator
print_default 
print_internal 

Definition at line 23 of file print_format.h.

Function Documentation

◆ empty_identifier_string()

identifier_string mcrl2::core::empty_identifier_string ( )
inline

Provides the empty identifier string.

Returns
The empty identifier string.

Definition at line 67 of file identifier_string.h.

◆ is_identifier_string()

bool mcrl2::core::is_identifier_string ( const atermpp::aterm t)
inline

Tests if a term is an identifier string.

Parameters
[in]tA term
Returns
Whether t is an identifier string.

Definition at line 59 of file identifier_string.h.

◆ is_user_identifier()

bool mcrl2::core::is_user_identifier ( std::string const &  s)
inline

Definition at line 274 of file parse.h.

◆ load_aterm()

atermpp::aterm mcrl2::core::load_aterm ( std::istream &  stream,
bool  binary = true,
const std::string &  format = "aterm",
const std::string &  source = "",
atermpp::aterm_transformer  transformer = atermpp::identity 
)
inline

Attempts to read an aterm from a stream.

Parameters
[in]streamThe stream from which the term is read.
[in]binaryA boolean indicating whether the stream is in binary of textual format.
[in]formatThe format that is being read (for example "LPS" or "PBES").
[in]sourceThe source from which the stream originates (the empty string is used for an unknown source).
[in]transformerA funtion that is applied to every subterm of the read term.
Exceptions
Throwsa mcrl2 runtime error when an error occurs when reading the term.

Definition at line 44 of file load_aterm.h.

◆ make_apply_builder()

template<template< class > class Builder>
apply_builder< Builder > mcrl2::core::make_apply_builder ( )

Definition at line 116 of file builder.h.

◆ make_apply_builder_arg1()

template<template< class > class Builder, class Arg1 >
apply_builder_arg1< Builder, Arg1 > mcrl2::core::make_apply_builder_arg1 ( const Arg1 &  arg1)

Definition at line 140 of file builder.h.

◆ make_apply_builder_arg2()

template<template< class > class Builder, class Arg1 , class Arg2 >
apply_builder_arg2< Builder, Arg1, Arg2 > mcrl2::core::make_apply_builder_arg2 ( const Arg1 &  arg1,
const Arg2 &  arg2 
)

Definition at line 164 of file builder.h.

◆ make_apply_traverser()

template<template< class > class Traverser>
apply_traverser< Traverser > mcrl2::core::make_apply_traverser ( )

Definition at line 79 of file traverser.h.

◆ make_update_apply_builder()

template<template< class > class Builder, class Function >
update_apply_builder< Builder, Function > mcrl2::core::make_update_apply_builder ( const Function &  f)

Definition at line 199 of file builder.h.

◆ make_update_apply_builder_arg1()

template<template< class > class Builder, class Function , class Arg1 >
update_apply_builder_arg1< Builder, Function, Arg1 > mcrl2::core::make_update_apply_builder_arg1 ( const Function &  f)

Definition at line 233 of file builder.h.

◆ msg()

void mcrl2::core::msg ( const std::string &  )
inline

Definition at line 29 of file builder.h.

◆ operator<<() [1/2]

std::ostream & mcrl2::core::operator<< ( std::ostream &  os,
const print_format_type pp_format 
)
inline

Definition at line 45 of file print_format.h.

◆ operator<<() [2/2]

std::ostream & mcrl2::core::operator<< ( std::ostream &  out,
const identifier_string x 
)
inline

\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream

Definition at line 43 of file identifier_string.h.

◆ operator>>()

std::istream & mcrl2::core::operator>> ( std::istream &  is,
print_format_type f 
)
inline

Definition at line 69 of file print_format.h.

◆ parse_identifier()

identifier_string mcrl2::core::parse_identifier ( const std::string &  text)
inline

Parse an identifier.

Definition at line 263 of file parse.h.

◆ parse_pp_format()

print_format_type mcrl2::core::parse_pp_format ( const std::string &  s)
inline

Definition at line 52 of file print_format.h.

◆ pp() [1/2]

std::string mcrl2::core::pp ( const identifier_string x)

Definition at line 26 of file core.cpp.

◆ pp() [2/2]

template<typename T >
std::string mcrl2::core::pp ( const T &  x)

Returns a string representation of the object x.

Definition at line 241 of file print.h.

◆ pp_format_to_string()

std::string mcrl2::core::pp_format_to_string ( const print_format_type  pp_format)
inline

Print string representation of pretty print format.

Parameters
pp_formata pretty print format
Returns
string representation of the pretty print format
Exceptions
mcrl2::runtimeerror if an unknown pretty print format is passed into the function.

Definition at line 31 of file print_format.h.

◆ print_aterm() [1/2]

template<>
void mcrl2::core::print_aterm ( const atermpp::aterm_appl x)
inline

Definition at line 256 of file parse.h.

◆ print_aterm() [2/2]

template<typename T >
void mcrl2::core::print_aterm ( const T &  )

Definition at line 250 of file parse.h.

◆ swap()

void mcrl2::core::swap ( identifier_string t1,
identifier_string t2 
)
inline

\brief swap overload

Definition at line 49 of file identifier_string.h.

◆ warn_and_or()

void mcrl2::core::warn_and_or ( const parse_node )
inline

Prints a warning for each occurrence of 'x && y || z' in the parse tree.

Definition at line 216 of file parser_utility.h.

◆ warn_left_merge_merge()

void mcrl2::core::warn_left_merge_merge ( const parse_node )
inline

Prints a warning for each occurrence of 'x ||_ y || z' in the parse tree.

Definition at line 223 of file parser_utility.h.