Include file:
#include "mcrl2/modal_formula/state_formula.h"
Add your file description here.
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
mcrl2::state_formulas::
state_formula_list
¶typedef for atermpp::term_list< state_formula >
list of state_formulas
mcrl2::state_formulas::
state_formula_vector
¶typedef for std::vector< state_formula >
vector of state_formulas
mcrl2::state_formulas::
find_nil
(const state_formulas::state_formula &x)¶is_and
(const atermpp::aterm_appl &x)Test for a and expression.
Parameters:
Returns: True if x is a and expression
is_delay
(const atermpp::aterm_appl &x)¶Test for a delay expression.
Parameters:
Returns: True if x is a delay expression
is_delay_timed
(const atermpp::aterm_appl &x)¶Test for a delay_timed expression.
Parameters:
Returns: True if x is a delay_timed expression
is_exists
(const atermpp::aterm_appl &x)Test for a exists expression.
Parameters:
Returns: True if x is a exists expression
is_false
(const atermpp::aterm_appl &x)Test for a false expression.
Parameters:
Returns: True if x is a false expression
is_forall
(const atermpp::aterm_appl &x)Test for a forall expression.
Parameters:
Returns: True if x is a forall expression
is_imp
(const atermpp::aterm_appl &x)Test for a imp expression.
Parameters:
Returns: True if x is a imp expression
is_may
(const atermpp::aterm_appl &x)¶Test for a may expression.
Parameters:
Returns: True if x is a may expression
is_mu
(const atermpp::aterm_appl &x)¶Test for a mu expression.
Parameters:
Returns: True if x is a mu expression
is_must
(const atermpp::aterm_appl &x)¶Test for a must expression.
Parameters:
Returns: True if x is a must expression
is_not
(const atermpp::aterm_appl &x)Test for a not expression.
Parameters:
Returns: True if x is a not expression
is_nu
(const atermpp::aterm_appl &x)¶Test for a nu expression.
Parameters:
Returns: True if x is a nu expression
is_or
(const atermpp::aterm_appl &x)Test for a or expression.
Parameters:
Returns: True if x is a or expression
mcrl2::state_formulas::
is_state_formula
(const atermpp::aterm_appl &x)¶Test for a state_formula expression.
Parameters:
Returns: True if x is a state_formula expression
is_true
(const atermpp::aterm_appl &x)Test for a true expression.
Parameters:
Returns: True if x is a true expression
is_variable
(const atermpp::aterm_appl &x)¶Test for a variable expression.
Parameters:
Returns: True if x is a variable expression
is_yaled
(const atermpp::aterm_appl &x)¶Test for a yaled expression.
Parameters:
Returns: True if x is a yaled expression
is_yaled_timed
(const atermpp::aterm_appl &x)¶Test for a yaled_timed expression.
Parameters:
Returns: True if x is a yaled_timed expression
mcrl2::state_formulas::
operator<<
(std::ostream &out, const and_ &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const delay &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const delay_timed &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const exists &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const false_ &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const forall &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const imp &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const may &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const mu &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const must &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const not_ &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const nu &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const or_ &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const state_formula &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const true_ &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const variable &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const yaled &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
operator<<
(std::ostream &out, const yaled_timed &x)¶Outputs the object to a stream.
Parameters:
Returns: The output stream
mcrl2::state_formulas::
preprocess_nested_modal_operators
(const state_formula &x)Preprocesses a state formula that contains (nested) modal operators.
Parameters:
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:
Returns: The preprocessed formula.
mcrl2::state_formulas::
swap
(delay_timed &t1, delay_timed &t2)¶swap overload
mcrl2::state_formulas::
swap
(state_formula &t1, state_formula &t2)¶swap overload
mcrl2::state_formulas::
swap
(yaled_timed &t1, yaled_timed &t2)¶swap overload