mcrl2/modal_formula/state_formula.h

Include file:

#include "mcrl2/modal_formula/state_formula.h"

Add your file description here.

Classes

• mcrl2::state_formulas::and_
• mcrl2::state_formulas::delay
• mcrl2::state_formulas::delay_timed
• mcrl2::state_formulas::exists
• mcrl2::state_formulas::false_
• mcrl2::state_formulas::forall
• mcrl2::state_formulas::imp
• mcrl2::state_formulas::may
• mcrl2::state_formulas::mu
• mcrl2::state_formulas::must
• mcrl2::state_formulas::not_
• mcrl2::state_formulas::nu
• mcrl2::state_formulas::or_
• mcrl2::state_formulas::state_formula
• mcrl2::state_formulas::true_
• mcrl2::state_formulas::variable
• mcrl2::state_formulas::yaled
• mcrl2::state_formulas::yaled_timed

Typedefs

type mcrl2::state_formulas::state_formula_list

typedef for atermpp::term_list< state_formula >

brief list of state_formulas

type mcrl2::state_formulas::state_formula_vector

typedef for std::vector< state_formula >

brief vector of state_formulas

Functions

bool mcrl2::state_formulas::find_nil(const state_formulas::state_formula &x)

bool is_and(const atermpp::aterm_appl &x)

brief Test for a and expression param x A term return True if a x is a and expression

bool is_delay(const atermpp::aterm_appl &x)

brief Test for a delay expression param x A term return True if a x is a delay expression

bool is_delay_timed(const atermpp::aterm_appl &x)

brief Test for a delay_timed expression param x A term return True if a x is a delay_timed expression

bool is_exists(const atermpp::aterm_appl &x)

brief Test for a exists expression param x A term return True if a x is a exists expression

bool is_false(const atermpp::aterm_appl &x)

brief Test for a false expression param x A term return True if a x is a false expression

bool is_forall(const atermpp::aterm_appl &x)

brief Test for a forall expression param x A term return True if a x is a forall expression

bool is_imp(const atermpp::aterm_appl &x)

brief Test for a imp expression param x A term return True if a x is a imp expression

bool is_may(const atermpp::aterm_appl &x)

brief Test for a may expression param x A term return True if a x is a may expression

bool is_mu(const atermpp::aterm_appl &x)

brief Test for a mu expression param x A term return True if a x is a mu expression

bool is_must(const atermpp::aterm_appl &x)

brief Test for a must expression param x A term return True if a x is a must expression

bool is_not(const atermpp::aterm_appl &x)

brief Test for a not expression param x A term return True if a x is a not expression

bool is_nu(const atermpp::aterm_appl &x)

brief Test for a nu expression param x A term return True if a x is a nu expression

bool is_or(const atermpp::aterm_appl &x)

brief Test for a or expression param x A term return True if a x is a or expression

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

brief Test for a state_formula expression param x A term return True if a x is a state_formula expression

bool is_true(const atermpp::aterm_appl &x)

brief Test for a true expression param x A term return True if a x is a true expression

bool is_variable(const atermpp::aterm_appl &x)

brief Test for a variable expression param x A term return True if a x is a variable expression

bool is_yaled(const atermpp::aterm_appl &x)

brief Test for a yaled expression param x A term return True if a x is a yaled expression

bool is_yaled_timed(const atermpp::aterm_appl &x)

brief Test for a yaled_timed expression param x A term return True if a x is a yaled_timed expression

void mcrl2::state_formulas::make_and_(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_and_ constructs a new term into a given address.

Parameters:

• t The reference into which the new and_ is constructed.

void mcrl2::state_formulas::make_delay_timed(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_delay_timed constructs a new term into a given address.

Parameters:

• t The reference into which the new delay_timed is constructed.

void mcrl2::state_formulas::make_exists(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_exists constructs a new term into a given address.

Parameters:

• t The reference into which the new exists is constructed.

void mcrl2::state_formulas::make_forall(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_forall constructs a new term into a given address.

Parameters:

• t The reference into which the new forall is constructed.

void mcrl2::state_formulas::make_imp(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_imp constructs a new term into a given address.

Parameters:

• t The reference into which the new imp is constructed.

void mcrl2::state_formulas::make_may(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_may constructs a new term into a given address.

Parameters:

• t The reference into which the new may is constructed.

void mcrl2::state_formulas::make_mu(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_mu constructs a new term into a given address.

Parameters:

• t The reference into which the new mu is constructed.

void mcrl2::state_formulas::make_must(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_must constructs a new term into a given address.

Parameters:

• t The reference into which the new must is constructed.

void mcrl2::state_formulas::make_not_(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_not_ constructs a new term into a given address.

Parameters:

• t The reference into which the new not_ is constructed.

void mcrl2::state_formulas::make_nu(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_nu constructs a new term into a given address.

Parameters:

• t The reference into which the new nu is constructed.

void mcrl2::state_formulas::make_or_(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_or_ constructs a new term into a given address.

Parameters:

• t The reference into which the new or_ is constructed.

void mcrl2::state_formulas::make_variable(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_variable constructs a new term into a given address.

Parameters:

• t The reference into which the new variable is constructed.

void mcrl2::state_formulas::make_yaled_timed(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_yaled_timed constructs a new term into a given address.

Parameters:

• t The reference into which the new yaled_timed is constructed.

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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(and_ &t1, and_ &t2)

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload

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

brief swap overload