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
typedef atermpp::term_list< action_formula >	action_formula_list
	\brief list of action_formulas
typedef std::vector< action_formula >	action_formula_vector
	\brief vector of action_formulas

Functions
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::string	pp (const action_formula &x)
std::ostream &	operator<< (std::ostream &out, const action_formula &x)
void	swap (action_formula &t1, action_formula &t2)
	\brief swap overload
std::string	pp (const true_ &x)
std::ostream &	operator<< (std::ostream &out, const true_ &x)
void	swap (true_ &t1, true_ &t2)
	\brief swap overload
std::string	pp (const false_ &x)
std::ostream &	operator<< (std::ostream &out, const false_ &x)
void	swap (false_ &t1, false_ &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_not_ (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const not_ &x)
std::ostream &	operator<< (std::ostream &out, const not_ &x)
void	swap (not_ &t1, not_ &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_and_ (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const and_ &x)
std::ostream &	operator<< (std::ostream &out, const and_ &x)
void	swap (and_ &t1, and_ &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_or_ (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const or_ &x)
std::ostream &	operator<< (std::ostream &out, const or_ &x)
void	swap (or_ &t1, or_ &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_imp (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const imp &x)
std::ostream &	operator<< (std::ostream &out, const imp &x)
void	swap (imp &t1, imp &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_forall (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const forall &x)
std::ostream &	operator<< (std::ostream &out, const forall &x)
void	swap (forall &t1, forall &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_exists (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const exists &x)
std::ostream &	operator<< (std::ostream &out, const exists &x)
void	swap (exists &t1, exists &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_at (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const at &x)
std::ostream &	operator<< (std::ostream &out, const at &x)
void	swap (at &t1, at &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	make_multi_action (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	pp (const multi_action &x)
std::ostream &	operator<< (std::ostream &out, const multi_action &x)
void	swap (multi_action &t1, multi_action &t2)
	\brief swap overload
std::set< data::variable >	find_all_variables (const action_formulas::action_formula &x)
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>>
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)
	Prints the object t to a stream.
template<typename T >
std::string	pp (const T &t)
	Returns a string representation of the object t.
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>>
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

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

\brief list of action_formulas

Definition at line 65 of file action_formula.h.

action_formula_vector

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

\brief vector of action_formulas

Definition at line 68 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

)

\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 40 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
	)

\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 31 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

)

\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 72 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
	)

\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 52 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
	)

\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 63 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
	)

\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 84 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

)

\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 147 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
	)

\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 138 of file find.h.

find_identifiers() [1/2]

template<typename T >

std::set< core::identifier_string > mcrl2::action_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 105 of file find.h.

find_identifiers() [2/2]

template<typename T , typename OutputIterator >

void mcrl2::action_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 96 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

)

\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 126 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
	)

\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 117 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 86 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 351 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 731 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 655 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 204 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 579 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 503 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 802 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 275 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 427 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 151 of file action_formula.h.

make_and_()

template<class... ARGUMENTS>

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

inline

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

Parameters

t	The reference into which the new and_ is constructed.

Definition at line 342 of file action_formula.h.

make_at()

template<class... ARGUMENTS>

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

inline

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

Parameters

t	The reference into which the new at is constructed.

Definition at line 722 of file action_formula.h.

make_exists()

template<class... ARGUMENTS>

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

inline

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

Parameters

t	The reference into which the new exists is constructed.

Definition at line 646 of file action_formula.h.

make_forall()

template<class... ARGUMENTS>

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

inline

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

Parameters

t	The reference into which the new forall is constructed.

Definition at line 570 of file action_formula.h.

make_imp()

template<class... ARGUMENTS>

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

inline

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

Parameters

t	The reference into which the new imp is constructed.

Definition at line 494 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 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 793 of file action_formula.h.

make_not_()

template<class... ARGUMENTS>

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

inline

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

Parameters

t	The reference into which the new not_ is constructed.

Definition at line 266 of file action_formula.h.

make_or_()

template<class... ARGUMENTS>

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

inline

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

Parameters

t	The reference into which the new or_ is constructed.

Definition at line 418 of file action_formula.h.

normalize_sorts() [1/2]

template<typename T >

T mcrl2::action_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 34 of file normalize_sorts.h.

normalize_sorts() [2/2]

template<typename T >

void mcrl2::action_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 25 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 111 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 364 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 744 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 668 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 217 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 592 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 516 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 815 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 288 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 440 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 164 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_formula &

x

)

Definition at line 27 of file modal_formula.cpp.

pp() [2/13]

std::string mcrl2::action_formulas::pp

(

const and_ &

x

)

Definition at line 28 of file modal_formula.cpp.

pp() [3/13]

std::string mcrl2::action_formulas::pp

(

const at &

x

)

Definition at line 29 of file modal_formula.cpp.

pp() [4/13]

std::string mcrl2::action_formulas::pp

(

const exists &

x

)

Definition at line 30 of file modal_formula.cpp.

pp() [5/13]

std::string mcrl2::action_formulas::pp

(

const false_ &

x

)

Definition at line 31 of file modal_formula.cpp.

pp() [6/13]

std::string mcrl2::action_formulas::pp

(

const forall &

x

)

Definition at line 32 of file modal_formula.cpp.

pp() [7/13]

std::string mcrl2::action_formulas::pp

(

const imp &

x

)

Definition at line 33 of file modal_formula.cpp.

pp() [8/13]

std::string mcrl2::action_formulas::pp

(

const multi_action &

x

)

Definition at line 34 of file modal_formula.cpp.

pp() [9/13]

std::string mcrl2::action_formulas::pp

(

const not_ &

x

)

Definition at line 35 of file modal_formula.cpp.

pp() [10/13]

std::string mcrl2::action_formulas::pp

(

const or_ &

x

)

Definition at line 36 of file modal_formula.cpp.

pp() [11/13]

template<typename T >

std::string mcrl2::action_formulas::pp

(

const T &

t

)

Returns a string representation of the object t.

Definition at line 175 of file print.h.

pp() [12/13]

template<typename T >

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

Prints the object t to a stream.

Definition at line 167 of file print.h.

pp() [13/13]

std::string mcrl2::action_formulas::pp

(

const true_ &

x

)

Definition at line 37 of file modal_formula.cpp.

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 , typename Substitution >

T mcrl2::action_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 100 of file replace.h.

replace_all_variables() [2/2]

template<typename T , typename Substitution >

void mcrl2::action_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 91 of file replace.h.

replace_data_expressions() [1/2]

template<typename T , typename Substitution >

T mcrl2::action_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 58 of file replace.h.

replace_data_expressions() [2/2]

template<typename T , typename Substitution >

void mcrl2::action_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 48 of file replace.h.

replace_free_variables() [1/4]

template<typename T , typename Substitution , typename VariableContainer >

T mcrl2::action_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 152 of file replace.h.

replace_free_variables() [2/4]

template<typename T , typename Substitution >

T mcrl2::action_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 125 of file replace.h.

replace_free_variables() [3/4]

template<typename T , typename Substitution , typename VariableContainer >

void mcrl2::action_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 139 of file replace.h.

replace_free_variables() [4/4]

template<typename T , typename Substitution >

void mcrl2::action_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 113 of file replace.h.

replace_sort_expressions() [1/2]

template<typename T , typename Substitution >

T mcrl2::action_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 36 of file replace.h.

replace_sort_expressions() [2/2]

template<typename T , typename Substitution >

void mcrl2::action_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 26 of file replace.h.

replace_variables() [1/2]

template<typename T , typename Substitution >

T mcrl2::action_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 80 of file replace.h.

replace_variables() [2/2]

template<typename T , typename Substitution >

void mcrl2::action_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 71 of file replace.h.

replace_variables_capture_avoiding() [1/4]

template<typename T , typename Substitution >

T mcrl2::action_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 83 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [2/4]

template<typename T , typename Substitution >

T mcrl2::action_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 117 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [3/4]

template<typename T , typename Substitution >

void mcrl2::action_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 68 of file replace_capture_avoiding.h.

replace_variables_capture_avoiding() [4/4]

template<typename T , typename Substitution >

void mcrl2::action_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 99 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::action_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 93 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::action_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 74 of file replace_capture_avoiding_with_an_identifier_generator.h.

rewrite() [1/4]

template<typename T , typename Rewriter , typename Substitution >

T mcrl2::action_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 70 of file rewrite.h.

rewrite() [2/4]

template<typename T , typename Rewriter >

T mcrl2::action_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 40 of file rewrite.h.

rewrite() [3/4]

template<typename T , typename Rewriter , typename Substitution >

void mcrl2::action_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 55 of file rewrite.h.

rewrite() [4/4]

template<typename T , typename Rewriter >

void mcrl2::action_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 27 of file rewrite.h.

swap() [1/11]

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

inline

\brief swap overload

Definition at line 117 of file action_formula.h.

swap() [2/11]

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

inline

\brief swap overload

Definition at line 370 of file action_formula.h.

swap() [3/11]

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

inline

\brief swap overload

Definition at line 750 of file action_formula.h.

swap() [4/11]

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

inline

\brief swap overload

Definition at line 674 of file action_formula.h.

swap() [5/11]

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

inline

\brief swap overload

Definition at line 223 of file action_formula.h.

swap() [6/11]

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

inline

\brief swap overload

Definition at line 598 of file action_formula.h.

swap() [7/11]

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

inline

\brief swap overload

Definition at line 522 of file action_formula.h.

swap() [8/11]

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

inline

\brief swap overload

Definition at line 821 of file action_formula.h.

swap() [9/11]

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

inline

\brief swap overload

Definition at line 294 of file action_formula.h.

swap() [10/11]

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

inline

\brief swap overload

Definition at line 446 of file action_formula.h.

swap() [11/11]

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

inline

\brief swap overload

Definition at line 170 of file action_formula.h.

translate_user_notation() [1/2]

template<typename T >

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

Definition at line 33 of file translate_user_notation.h.

translate_user_notation() [2/2]

template<typename T >

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

Definition at line 25 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 142 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 160 of file typecheck.h.