mcrl2/modal_formula/preprocess_state_formula.h

Include file:

#include "mcrl2/modal_formula/preprocess_state_formula.h"

add your file description here.

Classes

  • mcrl2::state_formulas::detail::count_modal_operator_nesting_traverser
  • mcrl2::state_formulas::detail::has_unscoped_modal_formula_traverser
  • mcrl2::state_formulas::detail::state_formula_preprocess_nested_modal_operators_builder

Functions

state_formula mcrl2::state_formulas::preprocess_nested_modal_operators(const state_formula &x)

Preprocesses a state formula that contains (nested) modal operators.

Parameters:

  • x A modal formula
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 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.

Parameters:

  • formula A modal formula.
  • context_ids A set of identifier strings.
  • preprocess_modal_operators A boolean indicating that dummy fixed point symbols can be inserted which makes subsequent handling easier.
  • warn_for_modal_operator_nesting A boolean enabling warnings for modal operator nesting.

Returns: The preprocessed formula.

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