|
| state_formula | parse_state_formula (const std::string &text) |
| |
| state_formula_specification | parse_state_formula_specification (const std::string &text) |
| |
| 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) |
| |
| std::size_t | count_modal_operator_nesting (const state_formula &x) |
| |
| bool | has_unscoped_modal_formulas (const state_formula &x) |
| | Checks whether a state formula contains an unscoped modal operator. A modal operator (must '[a]' or may '') is unscoped when, on the path from the root of the formula to that operator, it is not preceded by a fixpoint operator (mu or nu). In other words, the modal operator is not contained in the scope of any fixpoint. For example '[a]true' and 'true => true' contain an unscoped modal operator, whereas in 'mu X. [a]true' both modal operators are scoped by the surrounding 'mu 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) |
| |
| bool mcrl2::state_formulas::detail::has_unscoped_modal_formulas |
( |
const state_formula & |
x | ) |
|
|
inline |
Checks whether a state formula contains an unscoped modal operator. A modal operator (must '[a]' or may '') is unscoped when, on the path from the root of the formula to that operator, it is not preceded by a fixpoint operator (mu or nu). In other words, the modal operator is not contained in the scope of any fixpoint. For example '[a]true' and 'true => true' contain an unscoped modal operator, whereas in 'mu X. [a]true' both modal operators are scoped by the surrounding 'mu X'.
Definition at line 205 of file preprocess_state_formula.h.
1.9.7