Namespaces
namespace	detail

Classes
struct	action_label_traverser
	\brief Traverser class More...

struct	add_data_expressions

struct	add_data_variable_binding
	Maintains a multiset of bound data variables during traversal. More...

struct	add_data_variable_builder_binding

struct	add_data_variable_traverser_binding

struct	add_regular_formula_expressions

struct	add_sort_expressions

struct	add_traverser_action_labels

struct	add_traverser_data_expressions

struct	add_traverser_identifier_strings

struct	add_traverser_regular_formula_expressions

struct	add_traverser_sort_expressions

struct	add_traverser_variables

struct	add_variables

class	alt
	\brief The alt operator for regular formulas More...

struct	data_expression_builder
	\brief Builder class More...

struct	data_expression_traverser
	\brief Traverser class More...

struct	identifier_string_traverser
	\brief Traverser class More...

class	regular_formula
	\brief A regular formula More...

struct	regular_formula_builder
	\brief Builder class More...

struct	regular_formula_builder_base
	Builder class for regular_formula_builder. Used as a base class for pbes_expression_builder. More...

struct	regular_formula_traverser
	\brief Traverser class More...

struct	regular_formula_traverser_base
	Traversal class for regular_formula_traverser. Used as a base class for pbes_expression_traverser. More...

class	seq
	\brief The seq operator for regular formulas More...

struct	sort_expression_builder
	\brief Builder class More...

struct	sort_expression_traverser
	\brief Traverser class More...

class	trans
	\brief The trans operator for regular formulas More...

class	trans_or_nil
	\brief The 'trans or nil' operator for regular formulas More...

class	untyped_regular_formula
	\brief An untyped regular formula or action formula More...

struct	variable_builder
	\brief Builder class More...

struct	variable_traverser
	\brief Traverser class More...

Typedefs
typedef atermpp::term_list< regular_formula >	regular_formula_list
	\brief list of regular_formulas

typedef std::vector< regular_formula >	regular_formula_vector
	\brief vector of regular_formulas

Functions
template<typename T , typename OutputIterator >
void	find_all_variables (const T &x, OutputIterator o)

template<typename T >
std::set< data::variable >	find_all_variables (const T &x)

template<typename T , typename OutputIterator >
void	find_free_variables (const T &x, OutputIterator o)

template<typename T , typename OutputIterator , typename VariableContainer >
void	find_free_variables_with_bound (const T &x, OutputIterator o, const VariableContainer &bound)

template<typename T >
std::set< data::variable >	find_free_variables (const T &x)

template<typename T , typename VariableContainer >
std::set< data::variable >	find_free_variables_with_bound (const T &x, VariableContainer const &bound)

template<typename T , typename OutputIterator >
void	find_identifiers (const T &x, OutputIterator o)

template<typename T >
std::set< core::identifier_string >	find_identifiers (const T &x)

template<typename T , typename OutputIterator >
void	find_sort_expressions (const T &x, OutputIterator o)

template<typename T >
std::set< data::sort_expression >	find_sort_expressions (const T &x)

template<typename T , typename OutputIterator >
void	find_function_symbols (const T &x, OutputIterator o)

template<typename T >
std::set< data::function_symbol >	find_function_symbols (const T &x)

template<typename T >
void	normalize_sorts (T &x, const data::sort_specification &sortspec, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)

template<typename T >
T	normalize_sorts (const T &x, const data::sort_specification &sortspec, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable>>
regular_formula	parse_regular_formula (const std::string &text, const data::data_specification &dataspec, const VariableContainer &variables, const ActionLabelContainer &actions)

regular_formula	parse_regular_formula (const std::string &text, const lps::stochastic_specification &lpsspec)

constexpr int	precedence (const seq &)

constexpr int	precedence (const alt &)

constexpr int	precedence (const trans &)

constexpr int	precedence (const trans_or_nil &)

int	precedence (const regular_formula &x)

bool	is_left_associative (const seq &)

bool	is_left_associative (const alt &)

bool	is_left_associative (const regular_formula &x)

bool	is_right_associative (const seq &)

bool	is_right_associative (const alt &)

bool	is_right_associative (const regular_formula &x)

template<typename T >
void	pp (const T &t, std::ostream &out)
	Prints the object t to a stream.

template<typename T >
std::string	pp (const T &t)
	Returns a string representation of the object t.

bool	is_seq (const atermpp::aterm &x)

bool	is_alt (const atermpp::aterm &x)

bool	is_trans (const atermpp::aterm &x)

bool	is_trans_or_nil (const atermpp::aterm &x)

bool	is_untyped_regular_formula (const atermpp::aterm &x)

bool	is_regular_formula (const atermpp::aterm &x)

std::string	pp (const regular_formula &x)

std::ostream &	operator<< (std::ostream &out, const regular_formula &x)

void	swap (regular_formula &t1, regular_formula &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_seq (atermpp::aterm &t, const ARGUMENTS &... args)

std::string	pp (const seq &x)

std::ostream &	operator<< (std::ostream &out, const seq &x)

void	swap (seq &t1, seq &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_alt (atermpp::aterm &t, const ARGUMENTS &... args)

std::string	pp (const alt &x)

std::ostream &	operator<< (std::ostream &out, const alt &x)

void	swap (alt &t1, alt &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_trans (atermpp::aterm &t, const ARGUMENTS &... args)

std::string	pp (const trans &x)

std::ostream &	operator<< (std::ostream &out, const trans &x)

void	swap (trans &t1, trans &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_trans_or_nil (atermpp::aterm &t, const ARGUMENTS &... args)

std::string	pp (const trans_or_nil &x)

std::ostream &	operator<< (std::ostream &out, const trans_or_nil &x)

void	swap (trans_or_nil &t1, trans_or_nil &t2)
	\brief swap overload

template<class... ARGUMENTS>
void	make_untyped_regular_formula (atermpp::aterm &t, const ARGUMENTS &... args)

std::string	pp (const untyped_regular_formula &x)

std::ostream &	operator<< (std::ostream &out, const untyped_regular_formula &x)

void	swap (untyped_regular_formula &t1, untyped_regular_formula &t2)
	\brief swap overload

template<typename T , typename Substitution >
void	replace_sort_expressions (T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
T	replace_sort_expressions (const T &x, const Substitution &sigma, bool innermost, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
void	replace_data_expressions (T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
T	replace_data_expressions (const T &x, const Substitution &sigma, bool innermost, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
void	replace_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
T	replace_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
void	replace_all_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
T	replace_all_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
void	replace_free_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
T	replace_free_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution , typename VariableContainer >
void	replace_free_variables (T &x, const Substitution &sigma, const VariableContainer &bound_variables, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution , typename VariableContainer >
T	replace_free_variables (const T &x, const Substitution &sigma, const VariableContainer &bound_variables, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
void	replace_variables_capture_avoiding (T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
void	replace_variables_capture_avoiding (T &x, Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution >
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution , typename IdentifierGenerator >
void	replace_variables_capture_avoiding_with_an_identifier_generator (T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Substitution , typename IdentifierGenerator >
T	replace_variables_capture_avoiding_with_an_identifier_generator (const T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Rewriter >
void	rewrite (T &x, Rewriter R, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Rewriter >
T	rewrite (const T &x, Rewriter R, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Rewriter , typename Substitution >
void	rewrite (T &x, Rewriter R, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T , typename Rewriter , typename Substitution >
T	rewrite (const T &x, Rewriter R, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename T >
void	translate_user_notation (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)

template<typename T >
T	translate_user_notation (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)

template<typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable>>
regular_formula	typecheck_regular_formula (const regular_formula &x, const data::data_specification &dataspec, const VariableContainer &variables, const ActionLabelContainer &actions)

regular_formula	typecheck_regular_formula (const regular_formula &x, const lps::stochastic_specification &lpsspec)

Typedef Documentation

◆ regular_formula_list

typedef atermpp::term_list<regular_formula> mcrl2::regular_formulas::regular_formula_list

\brief list of regular_formulas

Definition at line 59 of file regular_formula.h.

◆ regular_formula_vector

typedef std::vector<regular_formula> mcrl2::regular_formulas::regular_formula_vector

\brief vector of regular_formulas

Definition at line 62 of file regular_formula.h.

Function Documentation

◆ find_all_variables() [1/2]

template<typename T >

std::set< data::variable > mcrl2::regular_formulas::find_all_variables ( const T & x )

\brief Returns all variables that occur in an object \param[in] x an object containing variables \return All variables that occur in the object x

Definition at line 175 of file find.h.

◆ find_all_variables() [2/2]

template<typename T , typename OutputIterator >

void mcrl2::regular_formulas::find_all_variables	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are written. \return All variables that occur in the term x

Definition at line 166 of file find.h.

◆ find_free_variables() [1/2]

template<typename T >

std::set< data::variable > mcrl2::regular_formulas::find_free_variables ( const T & x )

\brief Returns all variables that occur in an object \param[in] x an object containing variables \return All free variables that occur in the object x

Definition at line 207 of file find.h.

◆ find_free_variables() [2/2]

template<typename T , typename OutputIterator >

void mcrl2::regular_formulas::find_free_variables	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are added. \return All free variables that occur in the object x

Definition at line 187 of file find.h.

◆ find_free_variables_with_bound() [1/2]

template<typename T , typename OutputIterator , typename VariableContainer >

void mcrl2::regular_formulas::find_free_variables_with_bound	(	const T &	x,
		OutputIterator	o,
		const VariableContainer &	bound
	)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are written. \param[in] bound a container of variables \return All free variables that occur in the object x

Definition at line 198 of file find.h.

◆ find_free_variables_with_bound() [2/2]

template<typename T , typename VariableContainer >

std::set< data::variable > mcrl2::regular_formulas::find_free_variables_with_bound	(	const T &	x,
		VariableContainer const &	bound
	)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in] bound a bound a container of variables \return All free variables that occur in the object x

Definition at line 219 of file find.h.

◆ find_function_symbols() [1/2]

template<typename T >

std::set< data::function_symbol > mcrl2::regular_formulas::find_function_symbols ( const T & x )

\brief Returns all function symbols that occur in an object \param[in] x an object containing function symbols \return All function symbols that occur in the object x

Definition at line 282 of file find.h.

◆ find_function_symbols() [2/2]

template<typename T , typename OutputIterator >

void mcrl2::regular_formulas::find_function_symbols	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all function symbols that occur in an object \param[in] x an object containing function symbols \param[in,out] o an output iterator to which all function symbols occurring in x are written. \return All function symbols that occur in the term x

Definition at line 273 of file find.h.

◆ find_identifiers() [1/2]

template<typename T >

std::set< core::identifier_string > mcrl2::regular_formulas::find_identifiers ( const T & x )

\brief Returns all identifiers that occur in an object \param[in] x an object containing identifiers \return All identifiers that occur in the object x

Definition at line 240 of file find.h.

◆ find_identifiers() [2/2]

template<typename T , typename OutputIterator >

void mcrl2::regular_formulas::find_identifiers	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all identifiers that occur in an object \param[in] x an object containing identifiers \param[in,out] o an output iterator to which all identifiers occurring in x are written. \return All identifiers that occur in the term x

Definition at line 231 of file find.h.

◆ find_sort_expressions() [1/2]

template<typename T >

std::set< data::sort_expression > mcrl2::regular_formulas::find_sort_expressions ( const T & x )

\brief Returns all sort expressions that occur in an object \param[in] x an object containing sort expressions \return All sort expressions that occur in the object x

Definition at line 261 of file find.h.

◆ find_sort_expressions() [2/2]

template<typename T , typename OutputIterator >

void mcrl2::regular_formulas::find_sort_expressions	(	const T &	x,
		OutputIterator	o
	)

\brief Returns all sort expressions that occur in an object \param[in] x an object containing sort expressions \param[in,out] o an output iterator to which all sort expressions occurring in x are written. \return All sort expressions that occur in the term x

Definition at line 252 of file find.h.

◆ is_alt()

bool mcrl2::regular_formulas::is_alt ( const atermpp::aterm & x )

inline

\brief Test for a alt expression \param x A term \return True if \a x is a alt expression

Definition at line 233 of file regular_formula.h.

◆ is_left_associative() [1/3]

bool mcrl2::regular_formulas::is_left_associative ( const alt & )

inline

Definition at line 201 of file print.h.

◆ is_left_associative() [2/3]

bool mcrl2::regular_formulas::is_left_associative ( const regular_formula & x )

inline

Definition at line 202 of file print.h.

◆ is_left_associative() [3/3]

bool mcrl2::regular_formulas::is_left_associative ( const seq & )

inline

Definition at line 200 of file print.h.

◆ is_regular_formula()

bool mcrl2::regular_formulas::is_regular_formula ( const atermpp::aterm & x )

inline

\brief Test for a regular_formula expression \param x A term \return True if \a x is a regular_formula expression

Definition at line 75 of file regular_formula.h.

◆ is_right_associative() [1/3]

bool mcrl2::regular_formulas::is_right_associative ( const alt & )

inline

Definition at line 210 of file print.h.

◆ is_right_associative() [2/3]

bool mcrl2::regular_formulas::is_right_associative ( const regular_formula & x )

inline

Definition at line 211 of file print.h.

◆ is_right_associative() [3/3]

bool mcrl2::regular_formulas::is_right_associative ( const seq & )

inline

Definition at line 209 of file print.h.

◆ is_seq()

bool mcrl2::regular_formulas::is_seq ( const atermpp::aterm & x )

inline

\brief Test for a seq expression \param x A term \return True if \a x is a seq expression

Definition at line 157 of file regular_formula.h.

◆ is_trans()

bool mcrl2::regular_formulas::is_trans ( const atermpp::aterm & x )

inline

\brief Test for a trans expression \param x A term \return True if \a x is a trans expression

Definition at line 304 of file regular_formula.h.

◆ is_trans_or_nil()

bool mcrl2::regular_formulas::is_trans_or_nil ( const atermpp::aterm & x )

inline

\brief Test for a trans_or_nil expression \param x A term \return True if \a x is a trans_or_nil expression

Definition at line 375 of file regular_formula.h.

◆ is_untyped_regular_formula()

bool mcrl2::regular_formulas::is_untyped_regular_formula ( const atermpp::aterm & x )

inline

\brief Test for a untyped_regular_formula expression \param x A term \return True if \a x is a untyped_regular_formula expression

Definition at line 461 of file regular_formula.h.

◆ make_alt()

template<class... ARGUMENTS>

void mcrl2::regular_formulas::make_alt	(	atermpp::aterm &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_alt constructs a new term into a given address. \

Parameters

t	The reference into which the new alt is constructed.

Definition at line 224 of file regular_formula.h.

◆ make_seq()

template<class... ARGUMENTS>

void mcrl2::regular_formulas::make_seq	(	atermpp::aterm &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_seq constructs a new term into a given address. \

Parameters

t	The reference into which the new seq is constructed.

Definition at line 148 of file regular_formula.h.

◆ make_trans()

template<class... ARGUMENTS>

void mcrl2::regular_formulas::make_trans	(	atermpp::aterm &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_trans constructs a new term into a given address. \

Parameters

t	The reference into which the new trans is constructed.

Definition at line 295 of file regular_formula.h.

◆ make_trans_or_nil()

template<class... ARGUMENTS>

void mcrl2::regular_formulas::make_trans_or_nil	(	atermpp::aterm &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_trans_or_nil constructs a new term into a given address. \

Parameters

t	The reference into which the new trans_or_nil is constructed.

Definition at line 366 of file regular_formula.h.

◆ make_untyped_regular_formula()

template<class... ARGUMENTS>

void mcrl2::regular_formulas::make_untyped_regular_formula	(	atermpp::aterm &	t,
		const ARGUMENTS &...	args
	)

inline

\brief Make_untyped_regular_formula constructs a new term into a given address. \

Parameters

t	The reference into which the new untyped_regular_formula is constructed.

Definition at line 452 of file regular_formula.h.

◆ normalize_sorts() [1/2]

template<typename T >

T mcrl2::regular_formulas::normalize_sorts	(	const T &	x,
		const data::sort_specification &	sortspec,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 59 of file normalize_sorts.h.

◆ normalize_sorts() [2/2]

template<typename T >

void mcrl2::regular_formulas::normalize_sorts	(	T &	x,
		const data::sort_specification &	sortspec,
		typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *	= `0`
	)

Definition at line 50 of file normalize_sorts.h.

◆ operator<<() [1/6]

std::ostream & mcrl2::regular_formulas::operator<<	(	std::ostream &	out,
		const alt &	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 246 of file regular_formula.h.

◆ operator<<() [2/6]

std::ostream & mcrl2::regular_formulas::operator<<	(	std::ostream &	out,
		const regular_formula &	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 94 of file regular_formula.h.

◆ operator<<() [3/6]

std::ostream & mcrl2::regular_formulas::operator<<	(	std::ostream &	out,
		const seq &	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 170 of file regular_formula.h.

◆ operator<<() [4/6]

std::ostream & mcrl2::regular_formulas::operator<<	(	std::ostream &	out,
		const trans &	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 317 of file regular_formula.h.

◆ operator<<() [5/6]

std::ostream & mcrl2::regular_formulas::operator<<	(	std::ostream &	out,
		const trans_or_nil &	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 388 of file regular_formula.h.

◆ operator<<() [6/6]

std::ostream & mcrl2::regular_formulas::operator<<	(	std::ostream &	out,
		const untyped_regular_formula &	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 474 of file regular_formula.h.

◆ parse_regular_formula() [1/2]

template<typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable>>

regular_formula mcrl2::regular_formulas::parse_regular_formula	(	const std::string &	text,
		const data::data_specification &	dataspec,
		const VariableContainer &	variables,
		const ActionLabelContainer &	actions
	)

Definition at line 68 of file parse.h.

◆ parse_regular_formula() [2/2]

regular_formula mcrl2::regular_formulas::parse_regular_formula	(	const std::string &	text,
		const lps::stochastic_specification &	lpsspec
	)

inline

Definition at line 81 of file parse.h.

◆ pp() [1/8]

std::string mcrl2::regular_formulas::pp ( const alt & x )

Definition at line 62 of file modal_formula.cpp.

◆ pp() [2/8]

std::string mcrl2::regular_formulas::pp ( const regular_formula & x )

Definition at line 63 of file modal_formula.cpp.

◆ pp() [3/8]

std::string mcrl2::regular_formulas::pp ( const seq & x )

Definition at line 64 of file modal_formula.cpp.

◆ pp() [4/8]

template<typename T >

std::string mcrl2::regular_formulas::pp ( const T & t )

Returns a string representation of the object t.

Definition at line 287 of file print.h.

◆ pp() [5/8]

template<typename T >

void mcrl2::regular_formulas::pp	(	const T &	t,
		std::ostream &	out
	)

Prints the object t to a stream.

Definition at line 279 of file print.h.

◆ pp() [6/8]

std::string mcrl2::regular_formulas::pp ( const trans & x )

Definition at line 65 of file modal_formula.cpp.

◆ pp() [7/8]

std::string mcrl2::regular_formulas::pp ( const trans_or_nil & x )

Definition at line 66 of file modal_formula.cpp.

◆ pp() [8/8]

std::string mcrl2::regular_formulas::pp ( const untyped_regular_formula & x )

Definition at line 67 of file modal_formula.cpp.

◆ precedence() [1/5]

constexpr int mcrl2::regular_formulas::precedence ( const alt & )

inlineconstexpr

Definition at line 187 of file print.h.

◆ precedence() [2/5]

int mcrl2::regular_formulas::precedence ( const regular_formula & x )

inline

Definition at line 190 of file print.h.

◆ precedence() [3/5]

constexpr int mcrl2::regular_formulas::precedence ( const seq & )

inlineconstexpr

Definition at line 186 of file print.h.

◆ precedence() [4/5]

constexpr int mcrl2::regular_formulas::precedence ( const trans & )

inlineconstexpr

Definition at line 188 of file print.h.

◆ precedence() [5/5]

constexpr int mcrl2::regular_formulas::precedence ( const trans_or_nil & )

inlineconstexpr

Definition at line 189 of file print.h.

◆ replace_all_variables() [1/2]

template<typename T , typename Substitution >

T mcrl2::regular_formulas::replace_all_variables	(	const T &	x,
		const Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 246 of file replace.h.

◆ replace_all_variables() [2/2]

template<typename T , typename Substitution >

void mcrl2::regular_formulas::replace_all_variables	(	T &	x,
		const Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 237 of file replace.h.

◆ replace_data_expressions() [1/2]

template<typename T , typename Substitution >

T mcrl2::regular_formulas::replace_data_expressions	(	const T &	x,
		const Substitution &	sigma,
		bool	innermost,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 204 of file replace.h.

◆ replace_data_expressions() [2/2]

template<typename T , typename Substitution >

void mcrl2::regular_formulas::replace_data_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 194 of file replace.h.

◆ replace_free_variables() [1/4]

template<typename T , typename Substitution , typename VariableContainer >

T mcrl2::regular_formulas::replace_free_variables	(	const T &	x,
		const Substitution &	sigma,
		const VariableContainer &	bound_variables,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 298 of file replace.h.

◆ replace_free_variables() [2/4]

template<typename T , typename Substitution >

T mcrl2::regular_formulas::replace_free_variables	(	const T &	x,
		const Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies the substitution sigma to x. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 271 of file replace.h.

◆ replace_free_variables() [3/4]

template<typename T , typename Substitution , typename VariableContainer >

void mcrl2::regular_formulas::replace_free_variables	(	T &	x,
		const Substitution &	sigma,
		const VariableContainer &	bound_variables,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 285 of file replace.h.

◆ replace_free_variables() [4/4]

template<typename T , typename Substitution >

void mcrl2::regular_formulas::replace_free_variables	(	T &	x,
		const Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies the substitution sigma to x. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 259 of file replace.h.

◆ replace_sort_expressions() [1/2]

template<typename T , typename Substitution >

T mcrl2::regular_formulas::replace_sort_expressions	(	const T &	x,
		const Substitution &	sigma,
		bool	innermost,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 182 of file replace.h.

◆ replace_sort_expressions() [2/2]

template<typename T , typename Substitution >

void mcrl2::regular_formulas::replace_sort_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 172 of file replace.h.

◆ replace_variables() [1/2]

template<typename T , typename Substitution >

T mcrl2::regular_formulas::replace_variables	(	const T &	x,
		const Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 226 of file replace.h.

◆ replace_variables() [2/2]

template<typename T , typename Substitution >

void mcrl2::regular_formulas::replace_variables	(	T &	x,
		const Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 217 of file replace.h.

◆ replace_variables_capture_avoiding() [1/4]

template<typename T , typename Substitution >

T mcrl2::regular_formulas::replace_variables_capture_avoiding	(	const T &	x,
		Substitution &	sigma,
		data::set_identifier_generator &	id_generator,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the substiution is applied. \param sigma A substitution. \param id_generator An identifier generator that generates names that do not appear in x and sigma

Definition at line 180 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding() [2/4]

template<typename T , typename Substitution >

T mcrl2::regular_formulas::replace_variables_capture_avoiding	(	const T &	x,
		Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the substiution is applied. \param sigma A substitution.

Definition at line 214 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding() [3/4]

template<typename T , typename Substitution >

void mcrl2::regular_formulas::replace_variables_capture_avoiding	(	T &	x,
		Substitution &	sigma,
		data::set_identifier_generator &	id_generator,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the subsitution is applied. \param sigma A substitution. \param id_generator An identifier generator that generates names that do not appear in x and sigma

Definition at line 165 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding() [4/4]

template<typename T , typename Substitution >

void mcrl2::regular_formulas::replace_variables_capture_avoiding	(	T &	x,
		Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the subsitution is applied. \param sigma A substitution.

Definition at line 196 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding_with_an_identifier_generator() [1/2]

template<typename T , typename Substitution , typename IdentifierGenerator >

T mcrl2::regular_formulas::replace_variables_capture_avoiding_with_an_identifier_generator	(	const T &	x,
		Substitution &	sigma,
		IdentifierGenerator &	id_generator,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies sigma as a capture avoiding substitution to x using an identifier generator.. \details This substitution function is much faster than replace_variables_capture_avoiding, but it requires an identifier generator that generates strings for fresh variables. These strings must be unique in the sense that they have not been used for other variables. \param x The object to which the substiution is applied. \param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its right hand side. The class maintain_variables_in_rhs is useful for this purpose. \param id_generator A generator that generates unique strings, not yet used as variable names. \return The result is the term x to which sigma has been applied.

Definition at line 170 of file replace_capture_avoiding_with_an_identifier_generator.h.

◆ replace_variables_capture_avoiding_with_an_identifier_generator() [2/2]

template<typename T , typename Substitution , typename IdentifierGenerator >

void mcrl2::regular_formulas::replace_variables_capture_avoiding_with_an_identifier_generator	(	T &	x,
		Substitution &	sigma,
		IdentifierGenerator &	id_generator,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Applies sigma as a capture avoiding substitution to x using an identifier generator. \details This substitution function is much faster than replace_variables_capture_avoiding, but it requires an identifier generator that generates strings for fresh variables. These strings must be unique in the sense that they have not been used for other variables. \param x The object to which the subsitution is applied. \param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its right hand side. The class maintain_variables_in_rhs is useful for this purpose. \param id_generator A generator that generates unique strings, not yet used as variable names.

Definition at line 151 of file replace_capture_avoiding_with_an_identifier_generator.h.

◆ rewrite() [1/4]

template<typename T , typename Rewriter , typename Substitution >

T mcrl2::regular_formulas::rewrite	(	const T &	x,
		Rewriter	R,
		const Substitution &	sigma,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly \param x an object containing expressions \param R a rewriter \param sigma a substitution \return the rewrite result

Definition at line 134 of file rewrite.h.

◆ rewrite() [2/4]

template<typename T , typename Rewriter >

T mcrl2::regular_formulas::rewrite	(	const T &	x,
		Rewriter	R,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Rewrites all embedded expressions in an object x \param x an object containing expressions \param R a rewriter \return the rewrite result

Definition at line 104 of file rewrite.h.

◆ rewrite() [3/4]

template<typename T , typename Rewriter , typename Substitution >

void mcrl2::regular_formulas::rewrite	(	T &	x,
		Rewriter	R,
		const Substitution &	sigma,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly \param x an object containing expressions \param R a rewriter \param sigma a substitution

Definition at line 119 of file rewrite.h.

◆ rewrite() [4/4]

template<typename T , typename Rewriter >

void mcrl2::regular_formulas::rewrite	(	T &	x,
		Rewriter	R,
		typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

\brief Rewrites all embedded expressions in an object x \param x an object containing expressions \param R a rewriter

Definition at line 91 of file rewrite.h.

◆ swap() [1/6]

void mcrl2::regular_formulas::swap	(	alt &	t1,
		alt &	t2
	)

inline

\brief swap overload

Definition at line 252 of file regular_formula.h.

◆ swap() [2/6]

void mcrl2::regular_formulas::swap	(	regular_formula &	t1,
		regular_formula &	t2
	)

inline

\brief swap overload

Definition at line 100 of file regular_formula.h.

◆ swap() [3/6]

void mcrl2::regular_formulas::swap	(	seq &	t1,
		seq &	t2
	)

inline

\brief swap overload

Definition at line 176 of file regular_formula.h.

◆ swap() [4/6]

void mcrl2::regular_formulas::swap	(	trans &	t1,
		trans &	t2
	)

inline

\brief swap overload

Definition at line 323 of file regular_formula.h.

◆ swap() [5/6]

void mcrl2::regular_formulas::swap	(	trans_or_nil &	t1,
		trans_or_nil &	t2
	)

inline

\brief swap overload

Definition at line 394 of file regular_formula.h.

◆ swap() [6/6]

void mcrl2::regular_formulas::swap	(	untyped_regular_formula &	t1,
		untyped_regular_formula &	t2
	)

inline

\brief swap overload

Definition at line 480 of file regular_formula.h.

◆ translate_user_notation() [1/2]

template<typename T >

T mcrl2::regular_formulas::translate_user_notation	(	const T &	x,
		typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *	= `nullptr`
	)

Definition at line 56 of file translate_user_notation.h.

◆ translate_user_notation() [2/2]

template<typename T >

void mcrl2::regular_formulas::translate_user_notation	(	T &	x,
		typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *	= `0`
	)

Definition at line 48 of file translate_user_notation.h.

◆ typecheck_regular_formula() [1/2]

template<typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable>>

regular_formula mcrl2::regular_formulas::typecheck_regular_formula	(	const regular_formula &	x,
		const data::data_specification &	dataspec,
		const VariableContainer &	variables,
		const ActionLabelContainer &	actions
	)

Definition at line 315 of file typecheck.h.

◆ typecheck_regular_formula() [2/2]

regular_formula mcrl2::regular_formulas::typecheck_regular_formula	(	const regular_formula &	x,
		const lps::stochastic_specification &	lpsspec
	)

inline

Definition at line 333 of file typecheck.h.

Namespaces

Classes

Typedefs

Functions

Typedef Documentation

◆ regular_formula_list

◆ regular_formula_vector

Function Documentation

◆ find_all_variables() [1/2]

◆ find_all_variables() [2/2]

◆ find_free_variables() [1/2]

◆ find_free_variables() [2/2]

◆ find_free_variables_with_bound() [1/2]

◆ find_free_variables_with_bound() [2/2]

◆ find_function_symbols() [1/2]

◆ find_function_symbols() [2/2]

◆ find_identifiers() [1/2]

◆ find_identifiers() [2/2]

◆ find_sort_expressions() [1/2]

◆ find_sort_expressions() [2/2]

◆ is_alt()

◆ is_left_associative() [1/3]

◆ is_left_associative() [2/3]

◆ is_left_associative() [3/3]

◆ is_regular_formula()

◆ is_right_associative() [1/3]

◆ is_right_associative() [2/3]

◆ is_right_associative() [3/3]

◆ is_seq()

◆ is_trans()

◆ is_trans_or_nil()

◆ is_untyped_regular_formula()

◆ make_alt()

◆ make_seq()

◆ make_trans()

◆ make_trans_or_nil()

◆ make_untyped_regular_formula()

◆ normalize_sorts() [1/2]

◆ normalize_sorts() [2/2]

◆ operator<<() [1/6]

◆ operator<<() [2/6]

◆ operator<<() [3/6]

◆ operator<<() [4/6]

◆ operator<<() [5/6]

◆ operator<<() [6/6]

◆ parse_regular_formula() [1/2]

◆ parse_regular_formula() [2/2]

◆ pp() [1/8]

◆ pp() [2/8]

◆ pp() [3/8]

◆ pp() [4/8]

◆ pp() [5/8]

◆ pp() [6/8]

◆ pp() [7/8]

◆ pp() [8/8]

◆ precedence() [1/5]

◆ precedence() [2/5]

◆ precedence() [3/5]

◆ precedence() [4/5]

◆ precedence() [5/5]

◆ replace_all_variables() [1/2]

◆ replace_all_variables() [2/2]

◆ replace_data_expressions() [1/2]

◆ replace_data_expressions() [2/2]

◆ replace_free_variables() [1/4]

◆ replace_free_variables() [2/4]

◆ replace_free_variables() [3/4]

◆ replace_free_variables() [4/4]

◆ replace_sort_expressions() [1/2]

◆ replace_sort_expressions() [2/2]

◆ replace_variables() [1/2]

◆ replace_variables() [2/2]

◆ replace_variables_capture_avoiding() [1/4]

◆ replace_variables_capture_avoiding() [2/4]

◆ replace_variables_capture_avoiding() [3/4]

◆ replace_variables_capture_avoiding() [4/4]

◆ replace_variables_capture_avoiding_with_an_identifier_generator() [1/2]

◆ replace_variables_capture_avoiding_with_an_identifier_generator() [2/2]

◆ rewrite() [1/4]

◆ rewrite() [2/4]