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_string >	identifier_string_list
	\brief list of identifier_strings

typedef std::vector< identifier_string >	identifier_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 &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

typedef atermpp::aterm_string mcrl2::core::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

typedef atermpp::term_list<identifier_string> mcrl2::core::identifier_string_list

\brief list of identifier_strings

Definition at line 30 of file identifier_string.h.

◆ identifier_string_vector

typedef std::vector<identifier_string> mcrl2::core::identifier_string_vector

\brief vector of identifier_strings

Definition at line 33 of file identifier_string.h.

Enumeration Type Documentation

◆ print_format_type

enum mcrl2::core::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] t A 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]	stream	The stream from which the term is read.
[in]	binary	A boolean indicating whether the stream is in binary of textual format.
[in]	format	The format that is being read (for example "LPS" or "PBES").
[in]	source	The source from which the stream originates (the empty string is used for an unknown source).
[in]	transformer	A funtion that is applied to every subterm of the read term.

Exceptions

Throws a 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 226 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_format a pretty print format

Returns: string representation of the pretty print format

Exceptions

mcrl2::runtime error 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 & 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.

Namespaces

Classes

Typedefs

Enumerations

Functions

Typedef Documentation

◆ identifier_string

◆ identifier_string_list

◆ identifier_string_vector

Enumeration Type Documentation

◆ print_format_type

Function Documentation

◆ empty_identifier_string()

◆ is_identifier_string()

◆ is_user_identifier()

◆ load_aterm()

◆ make_apply_builder()

◆ make_apply_builder_arg1()

◆ make_apply_builder_arg2()

◆ make_apply_traverser()

◆ make_update_apply_builder()

◆ make_update_apply_builder_arg1()

◆ msg()

◆ operator<<() [1/2]

◆ operator<<() [2/2]

◆ operator>>()

◆ parse_identifier()

◆ parse_pp_format()

◆ pp() [1/2]

◆ pp() [2/2]

◆ pp_format_to_string()

◆ print_aterm() [1/2]

◆ print_aterm() [2/2]

◆ swap()

◆ warn_and_or()

◆ warn_left_merge_merge()