mcrl2::action_formulas Namespace Reference

Namespaces
namespace	detail

Classes
class	action_formula
	\brief An action formula More...
struct	action_formula_builder
	\brief Builder class More...
struct	action_formula_builder_base
	Base class for action_formula_builder. More...
struct	action_formula_traverser
	\brief Traverser class More...
struct	action_formula_traverser_base
	Base class for action_formula_traverser. More...
struct	action_label_traverser
	\brief Traverser class More...
struct	add_action_formula_expressions
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_sort_expressions
struct	add_traverser_action_formula_expressions
struct	add_traverser_action_labels
struct	add_traverser_data_expressions
struct	add_traverser_identifier_strings
struct	add_traverser_sort_expressions
struct	add_traverser_variables
struct	add_variables
class	and_
	\brief The and operator for action formulas More...
class	at
	\brief The at operator for action formulas More...
struct	data_expression_builder
	\brief Builder class More...
struct	data_expression_traverser
	\brief Traverser class More...
class	exists
	\brief The existential quantification operator for action formulas More...
class	false_
	\brief The value false for action formulas More...
class	forall
	\brief The universal quantification operator for action formulas More...
struct	identifier_string_traverser
	\brief Traverser class More...
class	imp
	\brief The implication operator for action formulas More...
class	multi_action
	\brief The multi action for action formulas More...
class	not_
	\brief The not operator for action formulas More...
class	or_
	\brief The or operator for action formulas More...
struct	sort_expression_builder
	\brief Builder class More...
struct	sort_expression_traverser
	\brief Traverser class More...
class	true_
	\brief The value true for action formulas More...
struct	variable_builder
	\brief Builder class More...
struct	variable_traverser
	\brief Traverser class More...

Typedefs
using	action_formula_list = atermpp::term_list< action_formula >
	\brief list of action_formulas
using	action_formula_vector = std::vector< action_formula >
	\brief vector of action_formulas

Functions
std::string	pp (const action_formulas::action_formula &x, bool arg0)
std::string	pp (const action_formulas::and_ &x, bool arg0)
std::string	pp (const action_formulas::at &x, bool arg0)
std::string	pp (const action_formulas::exists &x, bool arg0)
std::string	pp (const action_formulas::false_ &x, bool arg0)
std::string	pp (const action_formulas::forall &x, bool arg0)
std::string	pp (const action_formulas::imp &x, bool arg0)
std::string	pp (const action_formulas::multi_action &x, bool arg0)
std::string	pp (const action_formulas::not_ &x, bool arg0)
std::string	pp (const action_formulas::or_ &x, bool arg0)
std::string	pp (const action_formulas::true_ &x, bool arg0)
std::set< data::variable >	find_all_variables (const action_formulas::action_formula &x)
template<typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable>>
action_formula	parse_action_formula (const std::string &text, const data::data_specification &dataspec, const VariableContainer &variables, const ActionLabelContainer &actions)
action_formula	parse_action_formula (const std::string &text, const lps::stochastic_specification &lpsspec)
constexpr int	precedence (const forall &)
constexpr int	precedence (const exists &)
constexpr int	precedence (const imp &)
constexpr int	precedence (const or_ &)
constexpr int	precedence (const and_ &)
constexpr int	precedence (const at &)
constexpr int	precedence (const not_ &)
int	precedence (const action_formula &x)
bool	is_left_associative (const imp &)
bool	is_left_associative (const or_ &)
bool	is_left_associative (const and_ &)
bool	is_left_associative (const action_formula &x)
bool	is_right_associative (const imp &)
bool	is_right_associative (const or_ &)
bool	is_right_associative (const and_ &)
bool	is_right_associative (const action_formula &x)
template<typename T >
void	pp (const T &t, std::ostream &out, bool precendence_aware)
	Prints the object t to a stream.
template<typename T >
std::string	pp (const T &t, bool precendence_aware=true)
	Returns a string representation of the object t.
template<typename T , typename Substitution > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_sort_expressions (T &x, const Substitution &sigma, bool innermost)
template<typename T , typename Substitution > requires std::is_base_of_v<atermpp::aterm, T>
T	replace_sort_expressions (const T &x, const Substitution &sigma, bool innermost)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_data_expressions (T &x, const Substitution &sigma, bool innermost)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_data_expressions (const T &x, const Substitution &sigma, bool innermost)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables (T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables (const T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_all_variables (T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_all_variables (const T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_free_variables (T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_free_variables (const T &x, const Substitution &sigma)
template<typename T , data::IsSubstitution Substitution, typename VariableContainer > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_free_variables (T &x, const Substitution &sigma, const VariableContainer &bound_variables)
template<typename T , data::IsSubstitution Substitution, typename VariableContainer > requires std::is_base_of_v<atermpp::aterm, T>
T	replace_free_variables (const T &x, const Substitution &sigma, const VariableContainer &bound_variables)
bool	is_true (const atermpp::aterm &x)
bool	is_false (const atermpp::aterm &x)
bool	is_not (const atermpp::aterm &x)
bool	is_and (const atermpp::aterm &x)
bool	is_or (const atermpp::aterm &x)
bool	is_imp (const atermpp::aterm &x)
bool	is_forall (const atermpp::aterm &x)
bool	is_exists (const atermpp::aterm &x)
bool	is_at (const atermpp::aterm &x)
bool	is_multi_action (const atermpp::aterm &x)
bool	is_action_formula (const atermpp::aterm &x)
std::ostream &	operator<< (std::ostream &out, const action_formula &x)
void	swap (action_formula &t1, action_formula &t2) noexcept
	\brief swap overload
std::ostream &	operator<< (std::ostream &out, const true_ &x)
void	swap (true_ &t1, true_ &t2) noexcept
	\brief swap overload
std::ostream &	operator<< (std::ostream &out, const false_ &x)
void	swap (false_ &t1, false_ &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_not (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const not_ &x)
void	swap (not_ &t1, not_ &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_and (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const and_ &x)
void	swap (and_ &t1, and_ &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_or (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const or_ &x)
void	swap (or_ &t1, or_ &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_imp (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const imp &x)
void	swap (imp &t1, imp &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_forall (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const forall &x)
void	swap (forall &t1, forall &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_exists (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const exists &x)
void	swap (exists &t1, exists &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_at (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const at &x)
void	swap (at &t1, at &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	make_multi_action (atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream &	operator<< (std::ostream &out, const multi_action &x)
void	swap (multi_action &t1, multi_action &t2) noexcept
	\brief swap overload
template<typename T , typename OutputIterator >
void	find_all_variables (const T &x, OutputIterator o)
	Writes all variables that occur in an object to an output iterator.
template<typename T >
std::set< data::variable >	find_all_variables (const T &x)
	Returns all variables that occur in an object.
template<typename T , typename OutputIterator >
void	find_free_variables (const T &x, OutputIterator o)
	Writes all free variables that occur in an object to an output iterator.
template<typename T , typename OutputIterator , typename VariableContainer >
void	find_free_variables_with_bound (const T &x, OutputIterator o, const VariableContainer &bound)
	Writes all free variables that occur in an object to an output iterator.
template<typename T >
std::set< data::variable >	find_free_variables (const T &x)
	Returns all free variables that occur in an object.
template<typename T , typename VariableContainer >
std::set< data::variable >	find_free_variables_with_bound (const T &x, VariableContainer const &bound)
	Returns all free variables that occur in an object.
template<typename T , typename OutputIterator >
void	find_identifiers (const T &x, OutputIterator o)
	Writes all identifiers that occur in an object to an output iterator.
template<typename T >
std::set< core::identifier_string >	find_identifiers (const T &x)
	Returns all identifiers that occur in an object.
template<typename T , typename OutputIterator >
void	find_sort_expressions (const T &x, OutputIterator o)
	Writes all sort expressions that occur in an object to an output iterator.
template<typename T >
std::set< data::sort_expression >	find_sort_expressions (const T &x)
	Returns all sort expressions that occur in an object.
template<typename T , typename OutputIterator >
void	find_function_symbols (const T &x, OutputIterator o)
	Writes all function symbols that occur in an object to an output iterator.
template<typename T >
std::set< data::function_symbol >	find_function_symbols (const T &x)
	Returns all function symbols that occur in an object.
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	normalize_sorts (T &x, const data::sort_specification &sortspec)
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	normalize_sorts (const T &x, const data::sort_specification &sortspec)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables_capture_avoiding (T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
template<typename T , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables_capture_avoiding (T &x, Substitution &sigma)
template<typename T , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables_capture_avoiding (const T &x, Substitution &sigma)
template<typename T , data::IsSubstitution Substitution, typename IdentifierGenerator > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	replace_variables_capture_avoiding_with_an_identifier_generator (T &x, Substitution &sigma, IdentifierGenerator &id_generator)
template<typename T , data::IsSubstitution Substitution, typename IdentifierGenerator > requires std::is_base_of_v<atermpp::aterm, T>
T	replace_variables_capture_avoiding_with_an_identifier_generator (const T &x, Substitution &sigma, IdentifierGenerator &id_generator)
template<typename T , typename Rewriter > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	rewrite (T &x, Rewriter R)
template<typename T , typename Rewriter > requires std::is_base_of_v<atermpp::aterm, T>
T	rewrite (const T &x, Rewriter R)
template<typename T , typename Rewriter , data::IsSubstitution Substitution> requires (!std::is_base_of_v<atermpp::aterm, T>)
void	rewrite (T &x, Rewriter R, const Substitution &sigma)
template<typename T , typename Rewriter , data::IsSubstitution Substitution> requires std::is_base_of_v<atermpp::aterm, T>
T	rewrite (const T &x, Rewriter R, const Substitution &sigma)
template<typename T > requires (!std::is_base_of_v<atermpp::aterm, T>)
void	translate_user_notation (T &x)
template<typename T > requires (std::is_base_of_v<atermpp::aterm, T>)
T	translate_user_notation (const T &x)
template<typename ActionLabelContainer = std::vector<state_formulas::variable>, typename VariableContainer = std::vector<data::variable>>
action_formula	typecheck_action_formula (const action_formula &x, const data::data_specification &dataspec, const VariableContainer &variables, const ActionLabelContainer &actions)
action_formula	typecheck_action_formula (const action_formula &x, const lps::stochastic_specification &lpsspec)

Typedef Documentation

action_formula_list

using mcrl2::action_formulas::action_formula_list = typedef atermpp::term_list<action_formula>

\brief list of action_formulas

Definition at line 62 of file action_formula.h.

action_formula_vector

using mcrl2::action_formulas::action_formula_vector = typedef std::vector<action_formula>

\brief vector of action_formulas

Definition at line 65 of file action_formula.h.

Function Documentation

find_all_variables() [1/3]

std::set< data::variable > mcrl2::action_formulas::find_all_variables

(

const action_formulas::action_formula &

x

)

Definition at line 38 of file modal_formula.cpp.

find_all_variables() [2/3]

template<typename T >

std::set< data::variable > mcrl2::action_formulas::find_all_variables

(

const T &

x

)

Returns all variables that occur in an object.

Parameters

[in]

x

an object containing variables

Returns

All variables that occur in the object x

Definition at line 39 of file find.h.

find_all_variables() [3/3]

template<typename T , typename OutputIterator >

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

Writes all variables that occur in an object to an output iterator.

Parameters

[in]	x	an object containing variables
[in,out]	o	an output iterator to which all variables occurring in x are written.

Definition at line 30 of file find.h.

find_free_variables() [1/2]

template<typename T >

std::set< data::variable > mcrl2::action_formulas::find_free_variables

(

const T &

x

)

Returns all free variables that occur in an object.

Parameters

[in]

x

an object containing variables

Returns

All free variables that occur in the object x

Definition at line 69 of file find.h.

find_free_variables() [2/2]

template<typename T , typename OutputIterator >

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

Writes all free variables that occur in an object to an output iterator.

Parameters

[in]	x	an object containing variables
[in,out]	o	an output iterator to which all variables occurring in x are added.

Definition at line 50 of file find.h.

find_free_variables_with_bound() [1/2]

template<typename T , typename OutputIterator , typename VariableContainer >

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

Writes all free variables that occur in an object to an output iterator.

Parameters

[in]	x	an object containing variables
[in,out]	o	an output iterator to which all variables occurring in x are written.
[in]	bound	a container of variables

Definition at line 60 of file find.h.

find_free_variables_with_bound() [2/2]

template<typename T , typename VariableContainer >

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

Returns all free variables that occur in an object.

Parameters

[in]	x	an object containing variables
[in]	bound	a container of variables

Returns

All free variables that occur in the object x

Definition at line 81 of file find.h.

find_function_symbols() [1/2]

template<typename T >

std::set< data::function_symbol > mcrl2::action_formulas::find_function_symbols

(

const T &

x

)

Returns all function symbols that occur in an object.

Parameters

[in]

x

an object containing function symbols

Returns

All function symbols that occur in the object x

Definition at line 141 of file find.h.

find_function_symbols() [2/2]

template<typename T , typename OutputIterator >

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

Writes all function symbols that occur in an object to an output iterator.

Parameters

[in]	x	an object containing function symbols
[in,out]	o	an output iterator to which all function symbols occurring in x are written.

Definition at line 132 of file find.h.

find_identifiers() [1/2]

template<typename T >

std::set< core::identifier_string > mcrl2::action_formulas::find_identifiers

(

const T &

x

)

Returns all identifiers that occur in an object.

Parameters

[in]

x

an object containing identifiers

Returns

All identifiers that occur in the object x

Definition at line 101 of file find.h.

find_identifiers() [2/2]

template<typename T , typename OutputIterator >

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

Writes all identifiers that occur in an object to an output iterator.

Parameters

[in]	x	an object containing identifiers
[in,out]	o	an output iterator to which all identifiers occurring in x are written.

Definition at line 92 of file find.h.

find_sort_expressions() [1/2]

template<typename T >

std::set< data::sort_expression > mcrl2::action_formulas::find_sort_expressions

(

const T &

x

)

Returns all sort expressions that occur in an object.

Parameters

[in]

x

an object containing sort expressions

Returns

All sort expressions that occur in the object x

Definition at line 121 of file find.h.

find_sort_expressions() [2/2]

template<typename T , typename OutputIterator >

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

Writes all sort expressions that occur in an object to an output iterator.

Parameters

[in]	x	an object containing sort expressions
[in,out]	o	an output iterator to which all sort expressions occurring in x are written.

Definition at line 112 of file find.h.

is_action_formula()

bool mcrl2::action_formulas::is_action_formula ( const atermpp::aterm &  x )

inline

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

Definition at line 83 of file action_formula.h.

is_and()

bool mcrl2::action_formulas::is_and ( const atermpp::aterm &  x )

inline

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

Definition at line 348 of file action_formula.h.

is_at()

bool mcrl2::action_formulas::is_at ( const atermpp::aterm &  x )

inline

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

Definition at line 728 of file action_formula.h.

is_exists()

bool mcrl2::action_formulas::is_exists ( const atermpp::aterm &  x )

inline

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

Definition at line 652 of file action_formula.h.

is_false()

bool mcrl2::action_formulas::is_false ( const atermpp::aterm &  x )

inline

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

Definition at line 201 of file action_formula.h.

is_forall()

bool mcrl2::action_formulas::is_forall ( const atermpp::aterm &  x )

inline

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

Definition at line 576 of file action_formula.h.

is_imp()

bool mcrl2::action_formulas::is_imp ( const atermpp::aterm &  x )

inline

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

Definition at line 500 of file action_formula.h.

is_left_associative() [1/4]

bool mcrl2::action_formulas::is_left_associative ( const action_formula &  x )

inline

Definition at line 45 of file print.h.

is_left_associative() [2/4]

bool mcrl2::action_formulas::is_left_associative ( const and_ &  )

inline

Definition at line 44 of file print.h.

is_left_associative() [3/4]

bool mcrl2::action_formulas::is_left_associative ( const imp &  )

inline

Definition at line 42 of file print.h.

is_left_associative() [4/4]

bool mcrl2::action_formulas::is_left_associative ( const or_ &  )

inline

Definition at line 43 of file print.h.

is_multi_action()

bool mcrl2::action_formulas::is_multi_action ( const atermpp::aterm &  x )

inline

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

Definition at line 799 of file action_formula.h.

is_not()

bool mcrl2::action_formulas::is_not ( const atermpp::aterm &  x )

inline

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

Definition at line 272 of file action_formula.h.

is_or()

bool mcrl2::action_formulas::is_or ( const atermpp::aterm &  x )

inline

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

Definition at line 424 of file action_formula.h.

is_right_associative() [1/4]

bool mcrl2::action_formulas::is_right_associative ( const action_formula &  x )

inline

Definition at line 56 of file print.h.

is_right_associative() [2/4]

bool mcrl2::action_formulas::is_right_associative ( const and_ &  )

inline

Definition at line 55 of file print.h.

is_right_associative() [3/4]

bool mcrl2::action_formulas::is_right_associative ( const imp &  )

inline

Definition at line 53 of file print.h.

is_right_associative() [4/4]

bool mcrl2::action_formulas::is_right_associative ( const or_ &  )

inline

Definition at line 54 of file print.h.

is_true()

bool mcrl2::action_formulas::is_true ( const atermpp::aterm &  x )

inline

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

Definition at line 148 of file action_formula.h.

make_and()

template<class... ARGUMENTS>

void mcrl2::action_formulas::make_and ( atermpp::aterm &  t, const ARGUMENTS &...  args  )

inline

\brief The function make_and constructs a new term into a given address. \

Parameters

t	The reference into which the new and is constructed.

Definition at line 339 of file action_formula.h.

make_at()

template<class... ARGUMENTS>

void mcrl2::action_formulas::make_at ( atermpp::aterm &  t, const ARGUMENTS &...  args  )

inline

\brief The function make_at constructs a new term into a given address. \

Parameters

t	The reference into which the new at is constructed.

Definition at line 719 of file action_formula.h.

make_exists()

template<class... ARGUMENTS>

void mcrl2::action_formulas::make_exists ( atermpp::aterm &  t, const ARGUMENTS &...  args  )

inline

\brief The function make_exists constructs a new term into a given address. \

Parameters

t	The reference into which the new exists is constructed.

Definition at line 643 of file action_formula.h.

make_forall()

template<class... ARGUMENTS>

void mcrl2::action_formulas::make_forall ( atermpp::aterm &  t, const ARGUMENTS &...  args  )

inline

\brief The function make_forall constructs a new term into a given address. \

Parameters

t	The reference into which the new forall is constructed.

Definition at line 567 of file action_formula.h.

make_imp()

template<class... ARGUMENTS>

void mcrl2::action_formulas::make_imp ( atermpp::aterm &  t, const ARGUMENTS &...  args  )

inline

\brief The function make_imp constructs a new term into a given address. \

Parameters

t	The reference into which the new imp is constructed.

Definition at line 491 of file action_formula.h.

make_multi_action()

template<class... ARGUMENTS>

void mcrl2::action_formulas::make_multi_action ( atermpp::aterm &  t, const ARGUMENTS &...  args  )

inline

\brief The function make_multi_action constructs a new term into a given address. \

Parameters

t	The reference into which the new multi_action is constructed.

Definition at line 790 of file action_formula.h.

make_not()

template<class... ARGUMENTS>

void mcrl2::action_formulas::make_not ( atermpp::aterm &  t, const ARGUMENTS &...  args  )

inline

\brief The function make_not constructs a new term into a given address. \

Parameters

t	The reference into which the new not is constructed.

Definition at line 263 of file action_formula.h.

make_or()

template<class... ARGUMENTS>

void mcrl2::action_formulas::make_or ( atermpp::aterm &  t, const ARGUMENTS &...  args  )

inline

\brief The function make_or constructs a new term into a given address. \

Parameters

t	The reference into which the new or is constructed.

Definition at line 415 of file action_formula.h.

normalize_sorts() [1/2]

template<typename T >
requires (std::is_base_of_v<atermpp::aterm, T>)

T mcrl2::action_formulas::normalize_sorts	(	const T &	x,
		const data::sort_specification &	sortspec
	)

Definition at line 34 of file normalize_sorts.h.

normalize_sorts() [2/2]

template<typename T >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::action_formulas::normalize_sorts	(	T &	x,
		const data::sort_specification &	sortspec
	)

Definition at line 26 of file normalize_sorts.h.

operator<<() [1/11]

std::ostream & mcrl2::action_formulas::operator<< ( std::ostream &  out, const action_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 108 of file action_formula.h.

operator<<() [2/11]

std::ostream & mcrl2::action_formulas::operator<< ( std::ostream &  out, const and_ &  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 361 of file action_formula.h.

operator<<() [3/11]

std::ostream & mcrl2::action_formulas::operator<< ( std::ostream &  out, const at &  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 741 of file action_formula.h.

operator<<() [4/11]

std::ostream & mcrl2::action_formulas::operator<< ( std::ostream &  out, const exists &  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 665 of file action_formula.h.

operator<<() [5/11]

std::ostream & mcrl2::action_formulas::operator<< ( std::ostream &  out, const false_ &  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 214 of file action_formula.h.

operator<<() [6/11]

std::ostream & mcrl2::action_formulas::operator<< ( std::ostream &  out, const forall &  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 589 of file action_formula.h.

operator<<() [7/11]

std::ostream & mcrl2::action_formulas::operator<< ( std::ostream &  out, const imp &  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 513 of file action_formula.h.

operator<<() [8/11]

std::ostream & mcrl2::action_formulas::operator<< ( std::ostream &  out, const multi_action &  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 812 of file action_formula.h.

operator<<() [9/11]

std::ostream & mcrl2::action_formulas::operator<< ( std::ostream &  out, const not_ &  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 285 of file action_formula.h.

operator<<() [10/11]

std::ostream & mcrl2::action_formulas::operator<< ( std::ostream &  out, const or_ &  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 437 of file action_formula.h.

operator<<() [11/11]

std::ostream & mcrl2::action_formulas::operator<< ( std::ostream &  out, const true_ &  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 161 of file action_formula.h.

parse_action_formula() [1/2]

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

action_formula mcrl2::action_formulas::parse_action_formula	(	const std::string &	text,
		const data::data_specification &	dataspec,
		const VariableContainer &	variables,
		const ActionLabelContainer &	actions
	)

Definition at line 37 of file parse.h.

parse_action_formula() [2/2]

action_formula mcrl2::action_formulas::parse_action_formula ( const std::string &  text, const lps::stochastic_specification &  lpsspec  )

inline

Definition at line 50 of file parse.h.

pp() [1/13]

std::string mcrl2::action_formulas::pp	(	const action_formulas::action_formula &	x,
		bool	arg0 = true
	)

Definition at line 27 of file modal_formula.cpp.

pp() [2/13]

std::string mcrl2::action_formulas::pp	(	const action_formulas::and_ &	x,
		bool	arg0 = true
	)

Definition at line 28 of file modal_formula.cpp.

pp() [3/13]

std::string mcrl2::action_formulas::pp	(	const action_formulas::at &	x,
		bool	arg0 = true
	)

Definition at line 29 of file modal_formula.cpp.

pp() [4/13]

std::string mcrl2::action_formulas::pp	(	const action_formulas::exists &	x,
		bool	arg0 = true
	)

Definition at line 30 of file modal_formula.cpp.

pp() [5/13]

std::string mcrl2::action_formulas::pp	(	const action_formulas::false_ &	x,
		bool	arg0 = true
	)

Definition at line 31 of file modal_formula.cpp.

pp() [6/13]

std::string mcrl2::action_formulas::pp	(	const action_formulas::forall &	x,
		bool	arg0 = true
	)

Definition at line 32 of file modal_formula.cpp.

pp() [7/13]

std::string mcrl2::action_formulas::pp	(	const action_formulas::imp &	x,
		bool	arg0 = true
	)

Definition at line 33 of file modal_formula.cpp.

pp() [8/13]

std::string mcrl2::action_formulas::pp	(	const action_formulas::multi_action &	x,
		bool	arg0 = true
	)

Definition at line 34 of file modal_formula.cpp.

pp() [9/13]

std::string mcrl2::action_formulas::pp	(	const action_formulas::not_ &	x,
		bool	arg0 = true
	)

Definition at line 35 of file modal_formula.cpp.

pp() [10/13]

std::string mcrl2::action_formulas::pp	(	const action_formulas::or_ &	x,
		bool	arg0 = true
	)

Definition at line 36 of file modal_formula.cpp.

pp() [11/13]

std::string mcrl2::action_formulas::pp	(	const action_formulas::true_ &	x,
		bool	arg0 = true
	)

Definition at line 37 of file modal_formula.cpp.

pp() [12/13]

template<typename T >

std::string mcrl2::action_formulas::pp	(	const T &	t,
		bool	precendence_aware = true
	)

Returns a string representation of the object t.

Definition at line 175 of file print.h.

pp() [13/13]

template<typename T >

void mcrl2::action_formulas::pp	(	const T &	t,
		std::ostream &	out,
		bool	precendence_aware
	)

Prints the object t to a stream.

Definition at line 167 of file print.h.

precedence() [1/8]

int mcrl2::action_formulas::precedence ( const action_formula &  x )

inline

Definition at line 29 of file print.h.

precedence() [2/8]

constexpr int mcrl2::action_formulas::precedence ( const and_ &  )

inlineconstexpr

Definition at line 26 of file print.h.

precedence() [3/8]

constexpr int mcrl2::action_formulas::precedence ( const at &  )

inlineconstexpr

Definition at line 27 of file print.h.

precedence() [4/8]

constexpr int mcrl2::action_formulas::precedence ( const exists &  )

inlineconstexpr

Definition at line 23 of file print.h.

precedence() [5/8]

constexpr int mcrl2::action_formulas::precedence ( const forall &  )

inlineconstexpr

Definition at line 22 of file print.h.

precedence() [6/8]

constexpr int mcrl2::action_formulas::precedence ( const imp &  )

inlineconstexpr

Definition at line 24 of file print.h.

precedence() [7/8]

constexpr int mcrl2::action_formulas::precedence ( const not_ &  )

inlineconstexpr

Definition at line 28 of file print.h.

precedence() [8/8]

constexpr int mcrl2::action_formulas::precedence ( const or_ &  )

inlineconstexpr

Definition at line 25 of file print.h.

replace_all_variables() [1/2]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::action_formulas::replace_all_variables	(	const T &	x,
		const Substitution &	sigma
	)

Definition at line 101 of file replace.h.

replace_all_variables() [2/2]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::action_formulas::replace_all_variables	(	T &	x,
		const Substitution &	sigma
	)

Definition at line 92 of file replace.h.

replace_data_expressions() [1/2]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::action_formulas::replace_data_expressions	(	const T &	x,
		const Substitution &	sigma,
		bool	innermost
	)

Definition at line 58 of file replace.h.

replace_data_expressions() [2/2]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::action_formulas::replace_data_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost
	)

Definition at line 48 of file replace.h.

replace_free_variables() [1/4]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::action_formulas::replace_free_variables	(	const T &	x,
		const Substitution &	sigma
	)

\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 126 of file replace.h.

replace_free_variables() [2/4]

template<typename T , data::IsSubstitution Substitution, typename VariableContainer >
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::action_formulas::replace_free_variables	(	const T &	x,
		const Substitution &	sigma,
		const VariableContainer &	bound_variables
	)

\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 153 of file replace.h.

replace_free_variables() [3/4]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::action_formulas::replace_free_variables	(	T &	x,
		const Substitution &	sigma
	)

\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 114 of file replace.h.

replace_free_variables() [4/4]

template<typename T , data::IsSubstitution Substitution, typename VariableContainer >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::action_formulas::replace_free_variables	(	T &	x,
		const Substitution &	sigma,
		const VariableContainer &	bound_variables
	)

\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 140 of file replace.h.

replace_sort_expressions() [1/2]

template<typename T , typename Substitution >
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::action_formulas::replace_sort_expressions	(	const T &	x,
		const Substitution &	sigma,
		bool	innermost
	)

Definition at line 36 of file replace.h.

replace_sort_expressions() [2/2]

template<typename T , typename Substitution >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::action_formulas::replace_sort_expressions	(	T &	x,
		const Substitution &	sigma,
		bool	innermost
	)

Definition at line 26 of file replace.h.

replace_variables() [1/2]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::action_formulas::replace_variables	(	const T &	x,
		const Substitution &	sigma
	)

Definition at line 80 of file replace.h.

replace_variables() [2/2]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::action_formulas::replace_variables	(	T &	x,
		const Substitution &	sigma
	)

Definition at line 71 of file replace.h.

replace_variables_capture_avoiding() [1/4]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::action_formulas::replace_variables_capture_avoiding	(	const T &	x,
		Substitution &	sigma
	)

\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 116 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [2/4]

template<typename T , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::action_formulas::replace_variables_capture_avoiding	(	const T &	x,
		Substitution &	sigma,
		data::set_identifier_generator &	id_generator
	)

\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 82 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [3/4]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::action_formulas::replace_variables_capture_avoiding	(	T &	x,
		Substitution &	sigma
	)

\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 98 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [4/4]

template<typename T , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::action_formulas::replace_variables_capture_avoiding	(	T &	x,
		Substitution &	sigma,
		data::set_identifier_generator &	id_generator
	)

\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 67 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding_with_an_identifier_generator() [1/2]

template<typename T , data::IsSubstitution Substitution, typename IdentifierGenerator >
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::action_formulas::replace_variables_capture_avoiding_with_an_identifier_generator	(	const T &	x,
		Substitution &	sigma,
		IdentifierGenerator &	id_generator
	)

\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 93 of file replace_capture_avoiding_with_an_identifier_generator.h.

replace_variables_capture_avoiding_with_an_identifier_generator() [2/2]

template<typename T , data::IsSubstitution Substitution, typename IdentifierGenerator >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::action_formulas::replace_variables_capture_avoiding_with_an_identifier_generator	(	T &	x,
		Substitution &	sigma,
		IdentifierGenerator &	id_generator
	)

\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 74 of file replace_capture_avoiding_with_an_identifier_generator.h.

rewrite() [1/4]

template<typename T , typename Rewriter >
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::action_formulas::rewrite	(	const T &	x,
		Rewriter	R
	)

\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 40 of file rewrite.h.

rewrite() [2/4]

template<typename T , typename Rewriter , data::IsSubstitution Substitution>
requires std::is_base_of_v<atermpp::aterm, T>

T mcrl2::action_formulas::rewrite	(	const T &	x,
		Rewriter	R,
		const Substitution &	sigma
	)

\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 70 of file rewrite.h.

rewrite() [3/4]

template<typename T , typename Rewriter >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::action_formulas::rewrite	(	T &	x,
		Rewriter	R
	)

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

Definition at line 27 of file rewrite.h.

rewrite() [4/4]

template<typename T , typename Rewriter , data::IsSubstitution Substitution>
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::action_formulas::rewrite	(	T &	x,
		Rewriter	R,
		const Substitution &	sigma
	)

\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 55 of file rewrite.h.

swap() [1/11]

void mcrl2::action_formulas::swap ( action_formula &  t1, action_formula &  t2  )

inlinenoexcept

\brief swap overload

Definition at line 114 of file action_formula.h.

swap() [2/11]

void mcrl2::action_formulas::swap ( and_ &  t1, and_ &  t2  )

inlinenoexcept

\brief swap overload

Definition at line 367 of file action_formula.h.

swap() [3/11]

void mcrl2::action_formulas::swap ( at &  t1, at &  t2  )

inlinenoexcept

\brief swap overload

Definition at line 747 of file action_formula.h.

swap() [4/11]

void mcrl2::action_formulas::swap ( exists &  t1, exists &  t2  )

inlinenoexcept

\brief swap overload

Definition at line 671 of file action_formula.h.

swap() [5/11]

void mcrl2::action_formulas::swap ( false_ &  t1, false_ &  t2  )

inlinenoexcept

\brief swap overload

Definition at line 220 of file action_formula.h.

swap() [6/11]

void mcrl2::action_formulas::swap ( forall &  t1, forall &  t2  )

inlinenoexcept

\brief swap overload

Definition at line 595 of file action_formula.h.

swap() [7/11]

void mcrl2::action_formulas::swap ( imp &  t1, imp &  t2  )

inlinenoexcept

\brief swap overload

Definition at line 519 of file action_formula.h.

swap() [8/11]

void mcrl2::action_formulas::swap ( multi_action &  t1, multi_action &  t2  )

inlinenoexcept

\brief swap overload

Definition at line 818 of file action_formula.h.

swap() [9/11]

void mcrl2::action_formulas::swap ( not_ &  t1, not_ &  t2  )

inlinenoexcept

\brief swap overload

Definition at line 291 of file action_formula.h.

swap() [10/11]

void mcrl2::action_formulas::swap ( or_ &  t1, or_ &  t2  )

inlinenoexcept

\brief swap overload

Definition at line 443 of file action_formula.h.

swap() [11/11]

void mcrl2::action_formulas::swap ( true_ &  t1, true_ &  t2  )

inlinenoexcept

\brief swap overload

Definition at line 167 of file action_formula.h.

translate_user_notation() [1/2]

template<typename T >
requires (std::is_base_of_v<atermpp::aterm, T>)

T mcrl2::action_formulas::translate_user_notation

(

const T &

x

)

Definition at line 33 of file translate_user_notation.h.

translate_user_notation() [2/2]

template<typename T >
requires (!std::is_base_of_v<atermpp::aterm, T>)

void mcrl2::action_formulas::translate_user_notation

(

T &

x

)

Definition at line 26 of file translate_user_notation.h.

typecheck_action_formula() [1/2]

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

action_formula mcrl2::action_formulas::typecheck_action_formula	(	const action_formula &	x,
		const data::data_specification &	dataspec,
		const VariableContainer &	variables,
		const ActionLabelContainer &	actions
	)

Definition at line 143 of file typecheck.h.

typecheck_action_formula() [2/2]

action_formula mcrl2::action_formulas::typecheck_action_formula ( const action_formula &  x, const lps::stochastic_specification &  lpsspec  )

inline

Definition at line 161 of file typecheck.h.