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 >

list of state_formulas

type mcrl2::state_formulas::state_formula_vector

typedef for std::vector< state_formula >

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)

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

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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 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 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 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 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 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 mu &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 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 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 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 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 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 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

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)

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

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

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

swap overload

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(variable &t1, variable &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