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
using	identifier_string = atermpp::aterm_string
	String type of the LPS library. Identifier strings are represented internally as ATerms.

using	identifier_string_list = atermpp::term_list< identifier_string >
	\brief list of identifier_strings

using	identifier_string_vector = std::vector< identifier_string >
	\brief vector of identifier_strings

using	print_format_type = enum { print_default, print_internal }
	print_format_type represents the available pretty print formats

Functions
std::string	pp (const core::identifier_string &x, bool arg0)

template<typename T >
std::string	pp (const T &x, bool precedence_aware=true)
	Returns a string representation of the object x.

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<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::ostream &	operator<< (std::ostream &out, const identifier_string &x)

void	swap (identifier_string &t1, identifier_string &t2) noexcept
	\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.

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.

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

using mcrl2::core::identifier_string = typedef atermpp::aterm_string

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

Definition at line 23 of file identifier_string.h.

◆ identifier_string_list

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

\brief list of identifier_strings

Definition at line 27 of file identifier_string.h.

◆ identifier_string_vector

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

\brief vector of identifier_strings

Definition at line 30 of file identifier_string.h.

◆ print_format_type

using mcrl2::core::print_format_type = typedef enum { print_default, print_internal }

print_format_type represents the available pretty print formats

Definition at line 22 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 64 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 56 of file identifier_string.h.

◆ is_user_identifier()

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

inline

Definition at line 272 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 43 of file load_aterm.h.

◆ make_apply_builder()

template<template< class > class Builder>

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

Definition at line 103 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 127 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 151 of file builder.h.

◆ make_apply_traverser()

template<template< class > class Traverser>

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

Definition at line 78 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 186 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 220 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 48 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 40 of file identifier_string.h.

◆ operator>>()

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

inline

Definition at line 72 of file print_format.h.

◆ parse_identifier()

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

inline

Parse an identifier.

Definition at line 261 of file parse.h.

◆ parse_pp_format()

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

inline

Definition at line 55 of file print_format.h.

◆ pp() [1/2]

std::string mcrl2::core::pp	(	const core::identifier_string &	x,
		bool	arg0 = `true`
	)

Definition at line 26 of file core.cpp.

◆ pp() [2/2]

template<typename T >

std::string mcrl2::core::pp	(	const T &	x,
		bool	precedence_aware = `true`
	)

Returns a string representation of the object x.

Definition at line 228 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 34 of file print_format.h.

◆ print_aterm() [1/2]

template<>

void mcrl2::core::print_aterm ( const atermpp::aterm & x )

inline

Definition at line 254 of file parse.h.

◆ print_aterm() [2/2]

template<typename T >

void mcrl2::core::print_aterm ( const T & )

Definition at line 248 of file parse.h.

◆ swap()

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

inlinenoexcept

\brief swap overload

Definition at line 46 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 215 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 221 of file parser_utility.h.

Namespaces

Classes

Typedefs

Functions

Typedef Documentation

◆ identifier_string

◆ identifier_string_list

◆ identifier_string_vector

◆ 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()

◆ 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()