mcrl2::state_formulas::detail Namespace Reference

Classes
struct	add_capture_avoiding_replacement
struct	add_capture_avoiding_replacement_with_an_identifier_generator
struct	apply_maximal_closed_subformula_traverser
struct	bottom_up_traverser
struct	count_modal_operator_nesting_traverser
struct	find_free_state_variables_traverser
struct	find_state_variables_traverser
struct	free_variables_node
struct	has_unscoped_modal_formula_traverser
struct	is_timed_traverser
	Function that determines if a state formula is time dependent. More...
struct	maximal_closed_subformula_node
struct	maximal_closed_subformula_traverser
struct	printer
struct	state_formula_actions
class	state_formula_data_variable_name_clash_checker
	Traverser that checks for name clashes in parameters of nested mu's/nu's and forall/exists. More...
class	state_formula_data_variable_name_clash_resolver
struct	state_formula_preprocess_nested_modal_operators_builder
	Visitor that transforms state formulas. This can be useful if the state formula contains nested modal operators. More...
class	state_variable_context
class	state_variable_name_clash_checker
	Traverser that checks for name clashes in nested mu's/nu's. More...
class	state_variable_name_clash_resolver
struct	state_variable_name_traverser
struct	state_variable_negator
	Visitor that negates propositional variable instantiations with a given name. More...
struct	typecheck_builder
struct	untyped_state_formula_specification

Functions
template<template< class > class Traverser, class OutputIterator >
find_state_variables_traverser< Traverser, OutputIterator >	make_find_state_variables_traverser (OutputIterator out)
template<template< class > class Traverser, template< template< class > class, class > class Binder, class OutputIterator >
find_free_state_variables_traverser< Traverser, Binder, OutputIterator >	make_find_free_state_variables_traverser (OutputIterator out)
template<template< class > class Traverser, template< template< class > class, class > class Binder, class OutputIterator , class VariableContainer >
find_free_state_variables_traverser< Traverser, Binder, OutputIterator >	make_find_free_state_variables_traverser (OutputIterator out, const VariableContainer &v)
std::size_t	child_count (const state_formula &x)
std::ostream &	operator<< (std::ostream &out, const maximal_closed_subformula_node &node)
state_formula	parse_state_formula (const std::string &text)
state_formula_specification	parse_state_formula_specification (const std::string &text)
std::size_t	count_modal_operator_nesting (const state_formula &x)
bool	has_unscoped_modal_formulas (const state_formula &x)
template<typename IdentifierGenerator >
state_formula_preprocess_nested_modal_operators_builder< IdentifierGenerator >	make_state_formula_preprocess_nested_modal_operators_builder (IdentifierGenerator &generator)
	Utility function for creating a state_formula_preprocess_nested_modal_operators_builder.
template<template< class > class Builder, class Substitution , class IdentifierGenerator >
add_capture_avoiding_replacement_with_an_identifier_generator< Builder, class Derived, Substitution, IdentifierGenerator >	make_add_capture_avoiding_replacement_with_an_identifier_generator (Substitution &sigma, IdentifierGenerator &id_generator)
typecheck_builder	make_typecheck_builder (data::data_type_checker &data_typechecker, const data::detail::variable_context &variable_context, const process::detail::action_context &action_context, const detail::state_variable_context &state_variable_context, const bool formula_is_quantitative)

Function Documentation

child_count()

std::size_t mcrl2::state_formulas::detail::child_count ( const state_formula &  x )

inline

Definition at line 24 of file maximal_closed_subformula.h.

count_modal_operator_nesting()

std::size_t mcrl2::state_formulas::detail::count_modal_operator_nesting ( const state_formula &  x )

inline

Definition at line 134 of file preprocess_state_formula.h.

has_unscoped_modal_formulas()

bool mcrl2::state_formulas::detail::has_unscoped_modal_formulas ( const state_formula &  x )

inline

Definition at line 203 of file preprocess_state_formula.h.

make_add_capture_avoiding_replacement_with_an_identifier_generator()

template<template< class > class Builder, class Substitution , class IdentifierGenerator >

add_capture_avoiding_replacement_with_an_identifier_generator< Builder, class Derived, Substitution, IdentifierGenerator > mcrl2::state_formulas::detail::make_add_capture_avoiding_replacement_with_an_identifier_generator	(	Substitution &	sigma,
		IdentifierGenerator &	id_generator
	)

Definition at line 228 of file replace_capture_avoiding_with_an_identifier_generator.h.

make_find_free_state_variables_traverser() [1/2]

template<template< class > class Traverser, template< template< class > class, class > class Binder, class OutputIterator >

find_free_state_variables_traverser< Traverser, Binder, OutputIterator > mcrl2::state_formulas::detail::make_find_free_state_variables_traverser

(

OutputIterator

out

)

Definition at line 507 of file find.h.

make_find_free_state_variables_traverser() [2/2]

template<template< class > class Traverser, template< template< class > class, class > class Binder, class OutputIterator , class VariableContainer >

find_free_state_variables_traverser< Traverser, Binder, OutputIterator > mcrl2::state_formulas::detail::make_find_free_state_variables_traverser	(	OutputIterator	out,
		const VariableContainer &	v
	)

Definition at line 514 of file find.h.

make_find_state_variables_traverser()

template<template< class > class Traverser, class OutputIterator >

find_state_variables_traverser< Traverser, OutputIterator > mcrl2::state_formulas::detail::make_find_state_variables_traverser

(

OutputIterator

out

)

Definition at line 465 of file find.h.

make_state_formula_preprocess_nested_modal_operators_builder()

template<typename IdentifierGenerator >

state_formula_preprocess_nested_modal_operators_builder< IdentifierGenerator > mcrl2::state_formulas::detail::make_state_formula_preprocess_nested_modal_operators_builder

(

IdentifierGenerator &

generator

)

Utility function for creating a state_formula_preprocess_nested_modal_operators_builder.

Parameters

generator

A generator for fresh identifiers

Returns

a state_formula_preprocess_nested_modal_operators_builder

Definition at line 320 of file preprocess_state_formula.h.

make_typecheck_builder()

typecheck_builder mcrl2::state_formulas::detail::make_typecheck_builder ( data::data_type_checker &  data_typechecker, const data::detail::variable_context &  variable_context, const process::detail::action_context &  action_context, const detail::state_variable_context &  state_variable_context, const bool  formula_is_quantitative  )

inline

Definition at line 716 of file typecheck.h.

operator<<()

std::ostream & mcrl2::state_formulas::detail::operator<<	(	std::ostream &	out,
		const maximal_closed_subformula_node &	node
	)

Definition at line 136 of file maximal_closed_subformula.h.

parse_state_formula()

state_formula mcrl2::state_formulas::detail::parse_state_formula

(

const std::string &

text

)

Definition at line 128 of file modal_formula.cpp.

parse_state_formula_specification()

state_formula_specification mcrl2::state_formulas::detail::parse_state_formula_specification

(

const std::string &

text

)

Definition at line 139 of file modal_formula.cpp.