mcrl2/modal_formula/state_formula.h

Include file:

#include "mcrl2/modal_formula/state_formula.h"

Add your file description here.

Typedefs

type state_formula_list

typedef for atermpp::term_list< state_formula >

list of state_formulas

type state_formula_vector

typedef for std::vector< state_formula >

vector of state_formulas

Functions

std::set<process::action_label> find_action_labels(const state_formulas::state_formula &x)
std::set<data::variable> find_all_variables(const state_formulas::state_formula &x)
std::set<data::variable> find_free_variables(const state_formulas::state_formula &x)
std::set<core::identifier_string> find_identifiers(const state_formulas::state_formula &x)
bool mcrl2::state_formulas::find_nil(const state_formulas::state_formula &x)
std::set<data::sort_expression> find_sort_expressions(const state_formulas::state_formula &x)
bool is_and(const atermpp::aterm_appl &x)

Test for a and expression.

Parameters:

  • x A term

Returns: True if x is a and expression

bool is_delay(const atermpp::aterm_appl &x)

Test for a delay expression.

Parameters:

  • x A term

Returns: True if x is a delay expression

bool is_delay_timed(const atermpp::aterm_appl &x)

Test for a delay_timed expression.

Parameters:

  • x A term

Returns: True if x is a delay_timed expression

bool is_exists(const atermpp::aterm_appl &x)

Test for a exists expression.

Parameters:

  • x A term

Returns: True if x is a exists expression

bool is_false(const atermpp::aterm_appl &x)

Test for a false expression.

Parameters:

  • x A term

Returns: True if x is a false expression

bool is_forall(const atermpp::aterm_appl &x)

Test for a forall expression.

Parameters:

  • x A term

Returns: True if x is a forall expression

bool is_imp(const atermpp::aterm_appl &x)

Test for a imp expression.

Parameters:

  • x A term

Returns: True if x is a imp expression

bool is_may(const atermpp::aterm_appl &x)

Test for a may expression.

Parameters:

  • x A term

Returns: True if x is a may expression

bool is_mu(const atermpp::aterm_appl &x)

Test for a mu expression.

Parameters:

  • x A term

Returns: True if x is a mu expression

bool is_must(const atermpp::aterm_appl &x)

Test for a must expression.

Parameters:

  • x A term

Returns: True if x is a must expression

bool is_not(const atermpp::aterm_appl &x)

Test for a not expression.

Parameters:

  • x A term

Returns: True if x is a not expression

bool is_nu(const atermpp::aterm_appl &x)

Test for a nu expression.

Parameters:

  • x A term

Returns: True if x is a nu expression

bool is_or(const atermpp::aterm_appl &x)

Test for a or expression.

Parameters:

  • x A term

Returns: True if x is a or expression

bool mcrl2::state_formulas::is_state_formula(const atermpp::aterm_appl &x)

Test for a state_formula expression.

Parameters:

  • x A term

Returns: True if x is a state_formula expression

bool is_true(const atermpp::aterm_appl &x)

Test for a true expression.

Parameters:

  • x A term

Returns: True if x is a true expression

bool is_variable(const atermpp::aterm_appl &x)

Test for a variable expression.

Parameters:

  • x A term

Returns: True if x is a variable expression

bool is_yaled(const atermpp::aterm_appl &x)

Test for a yaled expression.

Parameters:

  • x A term

Returns: True if x is a yaled expression

bool is_yaled_timed(const atermpp::aterm_appl &x)

Test for a yaled_timed expression.

Parameters:

  • x A term

Returns: True if x is a yaled_timed expression

state_formulas::state_formula normalize_sorts(const state_formula &x, const data::sort_specification &sortspec)
std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const state_formula &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const true_ &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const false_ &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const not_ &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const and_ &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const or_ &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const imp &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const forall &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const exists &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const must &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const may &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const yaled &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const yaled_timed &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const delay &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const delay_timed &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const variable &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const nu &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::ostream &mcrl2::state_formulas::operator<<(std::ostream &out, const mu &x)

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

std::string pp(const state_formula &x)
std::string pp(const true_ &x)
std::string pp(const false_ &x)
std::string pp(const not_ &x)
std::string pp(const and_ &x)
std::string pp(const or_ &x)
std::string pp(const imp &x)
std::string pp(const forall &x)
std::string pp(const exists &x)
std::string pp(const must &x)
std::string pp(const may &x)
std::string pp(const yaled &x)
std::string pp(const yaled_timed &x)
std::string pp(const delay &x)
std::string pp(const delay_timed &x)
std::string pp(const variable &x)
std::string pp(const nu &x)
std::string pp(const mu &x)
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.

void mcrl2::state_formulas::swap(state_formula &t1, state_formula &t2)

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

void mcrl2::state_formulas::swap(must &t1, must &t2)

swap overload

void mcrl2::state_formulas::swap(may &t1, may &t2)

swap overload

void mcrl2::state_formulas::swap(yaled &t1, yaled &t2)

swap overload

void mcrl2::state_formulas::swap(yaled_timed &t1, yaled_timed &t2)

swap overload

void mcrl2::state_formulas::swap(delay &t1, delay &t2)

swap overload

void mcrl2::state_formulas::swap(delay_timed &t1, delay_timed &t2)

swap overload

void mcrl2::state_formulas::swap(variable &t1, variable &t2)

swap overload

void mcrl2::state_formulas::swap(nu &t1, nu &t2)

swap overload

void mcrl2::state_formulas::swap(mu &t1, mu &t2)

swap overload

state_formulas::state_formula translate_user_notation(const state_formulas::state_formula &x)

Functions

bool is_timed(const state_formula &x)