add your file description here. More...

Classes
struct	mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser

struct	mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser

struct	mcrl2::state_formulas::detail::state_formula_preprocess_nested_modal_operators_builder< IdentifierGenerator >
	Visitor that transforms state formulas. This can be useful if the state formula contains nested modal operators. More...

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.

namespace	mcrl2::state_formulas

namespace	mcrl2::state_formulas::detail

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

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

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.

state_formula	mcrl2::state_formulas::preprocess_nested_modal_operators (const state_formula &x)
	Preprocesses a state formula that contains (nested) modal operators.

state_formulas::state_formula	mcrl2::state_formulas::preprocess_state_formula (const state_formulas::state_formula &formula, const std::set< core::identifier_string > &context_ids, bool preprocess_modal_operators, bool quantitative=false, bool warn_for_modal_operator_nesting=true)
	Renames data variables and predicate variables in the formula `f`, and wraps the formula inside a 'nu' if needed. This is needed as a preprocessing step for the algorithm.

Detailed Description

add your file description here.

Classes