No Matches
state_formula.h File Reference

Add your file description here. More...

Go to the source code of this file.


class  mcrl2::state_formulas::state_formula
 \brief A state formula More...
class  mcrl2::state_formulas::true_
 \brief The value true for state formulas More...
class  mcrl2::state_formulas::false_
 \brief The value false for state formulas More...
class  mcrl2::state_formulas::not_
 \brief The not operator for state formulas More...
class  mcrl2::state_formulas::minus
 \brief The minus operator for state formulas More...
class  mcrl2::state_formulas::and_
 \brief The and operator for state formulas More...
class  mcrl2::state_formulas::or_
 \brief The or operator for state formulas More...
class  mcrl2::state_formulas::imp
 \brief The implication operator for state formulas More...
class  mcrl2::state_formulas::plus
 \brief The plus operator for state formulas with values More...
class  mcrl2::state_formulas::const_multiply
 \brief The multiply operator for state formulas with values More...
class  mcrl2::state_formulas::const_multiply_alt
 \brief The multiply operator for state formulas with values More...
class  mcrl2::state_formulas::forall
 \brief The universal quantification operator for state formulas More...
class  mcrl2::state_formulas::exists
 \brief The existential quantification operator for state formulas More...
class  mcrl2::state_formulas::infimum
 \brief The infimum over a data type for state formulas More...
class  mcrl2::state_formulas::supremum
 \brief The supremum over a data type for state formulas More...
class  mcrl2::state_formulas::sum
 \brief The sum over a data type for state formulas More...
class  mcrl2::state_formulas::must
 \brief The must operator for state formulas More...
class  mcrl2::state_formulas::may
 \brief The may operator for state formulas More...
class  mcrl2::state_formulas::yaled
 \brief The yaled operator for state formulas More...
class  mcrl2::state_formulas::yaled_timed
 \brief The timed yaled operator for state formulas More...
class  mcrl2::state_formulas::delay
 \brief The delay operator for state formulas More...
class  mcrl2::state_formulas::delay_timed
 \brief The timed delay operator for state formulas More...
class  mcrl2::state_formulas::variable
 \brief The state formula variable More...
class  mcrl2::state_formulas::nu
 \brief The nu operator for state formulas More...
class  mcrl2::state_formulas::mu
 \brief The mu operator for state formulas More...


namespace  mcrl2
 A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace  mcrl2::state_formulas
namespace  mcrl2::state_formulas::algorithms


typedef atermpp::term_list< state_formulamcrl2::state_formulas::state_formula_list
 \brief list of state_formulas
typedef std::vector< state_formulamcrl2::state_formulas::state_formula_vector
 \brief vector of state_formulas


bool mcrl2::state_formulas::is_true (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_false (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_not (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_minus (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_and (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_or (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_imp (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_plus (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_const_multiply (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_const_multiply_alt (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_forall (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_exists (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_infimum (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_supremum (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_sum (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_must (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_may (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_yaled (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_yaled_timed (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_delay (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_delay_timed (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_variable (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_nu (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_mu (const atermpp::aterm &x)
bool mcrl2::state_formulas::is_state_formula (const atermpp::aterm &x)
std::string mcrl2::state_formulas::pp (const state_formula &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const state_formula &x)
void mcrl2::state_formulas::swap (state_formula &t1, state_formula &t2)
 \brief swap overload
std::string mcrl2::state_formulas::pp (const true_ &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const true_ &x)
void mcrl2::state_formulas::swap (true_ &t1, true_ &t2)
 \brief swap overload
std::string mcrl2::state_formulas::pp (const false_ &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const false_ &x)
void mcrl2::state_formulas::swap (false_ &t1, false_ &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_not_ (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const not_ &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const not_ &x)
void mcrl2::state_formulas::swap (not_ &t1, not_ &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_minus (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const minus &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const minus &x)
void mcrl2::state_formulas::swap (minus &t1, minus &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_and_ (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const and_ &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const and_ &x)
void mcrl2::state_formulas::swap (and_ &t1, and_ &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_or_ (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const or_ &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const or_ &x)
void mcrl2::state_formulas::swap (or_ &t1, or_ &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_imp (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const imp &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const imp &x)
void mcrl2::state_formulas::swap (imp &t1, imp &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_plus (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const plus &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const plus &x)
void mcrl2::state_formulas::swap (plus &t1, plus &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_const_multiply (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const const_multiply &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const const_multiply &x)
void mcrl2::state_formulas::swap (const_multiply &t1, const_multiply &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_const_multiply_alt (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const const_multiply_alt &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const const_multiply_alt &x)
void mcrl2::state_formulas::swap (const_multiply_alt &t1, const_multiply_alt &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_forall (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const forall &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const forall &x)
void mcrl2::state_formulas::swap (forall &t1, forall &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_exists (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const exists &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const exists &x)
void mcrl2::state_formulas::swap (exists &t1, exists &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_infimum (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const infimum &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const infimum &x)
void mcrl2::state_formulas::swap (infimum &t1, infimum &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_supremum (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const supremum &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const supremum &x)
void mcrl2::state_formulas::swap (supremum &t1, supremum &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_sum (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const sum &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const sum &x)
void mcrl2::state_formulas::swap (sum &t1, sum &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_must (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const must &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const must &x)
void mcrl2::state_formulas::swap (must &t1, must &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_may (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const may &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const may &x)
void mcrl2::state_formulas::swap (may &t1, may &t2)
 \brief swap overload
std::string mcrl2::state_formulas::pp (const yaled &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const yaled &x)
void mcrl2::state_formulas::swap (yaled &t1, yaled &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_yaled_timed (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const yaled_timed &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const yaled_timed &x)
void mcrl2::state_formulas::swap (yaled_timed &t1, yaled_timed &t2)
 \brief swap overload
std::string mcrl2::state_formulas::pp (const delay &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const delay &x)
void mcrl2::state_formulas::swap (delay &t1, delay &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_delay_timed (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const delay_timed &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const delay_timed &x)
void mcrl2::state_formulas::swap (delay_timed &t1, delay_timed &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_variable (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const variable &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const variable &x)
void mcrl2::state_formulas::swap (variable &t1, variable &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_nu (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const nu &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const nu &x)
void mcrl2::state_formulas::swap (nu &t1, nu &t2)
 \brief swap overload
template<class... ARGUMENTS>
void mcrl2::state_formulas::make_mu (atermpp::aterm &t, const ARGUMENTS &... args)
std::string mcrl2::state_formulas::pp (const mu &x)
std::ostream & mcrl2::state_formulas::operator<< (std::ostream &out, const mu &x)
void mcrl2::state_formulas::swap (mu &t1, mu &t2)
 \brief swap overload
bool mcrl2::state_formulas::algorithms::is_timed (const state_formula &x)
state_formula mcrl2::state_formulas::normalize_sorts (const state_formula &x, const data::sort_specification &sortspec)
state_formulas::state_formula mcrl2::state_formulas::translate_user_notation (const state_formulas::state_formula &x)
std::set< data::sort_expressionmcrl2::state_formulas::find_sort_expressions (const state_formulas::state_formula &x)
std::set< data::variablemcrl2::state_formulas::find_all_variables (const state_formulas::state_formula &x)
std::set< data::variablemcrl2::state_formulas::find_free_variables (const state_formulas::state_formula &x)
std::set< core::identifier_stringmcrl2::state_formulas::find_identifiers (const state_formulas::state_formula &x)
std::set< process::action_labelmcrl2::state_formulas::find_action_labels (const state_formulas::state_formula &x)
bool mcrl2::state_formulas::find_nil (const state_formulas::state_formula &x)

Detailed Description

Add your file description here.

Definition in file state_formula.h.