mCRL2
Loading...
Searching...
No Matches
mcrl2::state_formulas Namespace Reference

Namespaces

namespace  algorithms
 
namespace  detail
 

Classes

struct  action_label_traverser
 \brief Traverser class More...
 
struct  add_data_expressions
 
struct  add_data_variable_binding
 Maintains a multiset of bound data variables during traversal. More...
 
struct  add_data_variable_builder_binding
 
struct  add_data_variable_traverser_binding
 
struct  add_sort_expressions
 
struct  add_state_formula_expressions
 
struct  add_state_variable_binding
 Maintains a multiset of bound state variables during traversal. More...
 
struct  add_traverser_action_labels
 
struct  add_traverser_data_expressions
 
struct  add_traverser_identifier_strings
 
struct  add_traverser_regular_formula_expressions
 
struct  add_traverser_sort_expressions
 
struct  add_traverser_state_formula_expressions
 
struct  add_traverser_state_variables
 
struct  add_traverser_variables
 
struct  add_variables
 
class  and_
 \brief The and operator for state formulas More...
 
class  const_multiply
 \brief The multiply operator for state formulas with values More...
 
class  const_multiply_alt
 \brief The multiply operator for state formulas with values More...
 
struct  data_expression_builder
 \brief Builder class More...
 
struct  data_expression_traverser
 \brief Traverser class More...
 
class  delay
 \brief The delay operator for state formulas More...
 
class  delay_timed
 \brief The timed delay operator for state formulas More...
 
class  exists
 \brief The existential quantification operator for state formulas More...
 
class  false_
 \brief The value false for state formulas More...
 
class  forall
 \brief The universal quantification operator for state formulas More...
 
struct  identifier_string_traverser
 \brief Traverser class More...
 
class  imp
 \brief The implication operator for state formulas More...
 
class  infimum
 \brief The infimum over a data type for state formulas More...
 
class  may
 \brief The may operator for state formulas More...
 
class  minus
 \brief The minus operator for state formulas More...
 
class  mu
 \brief The mu operator for state formulas More...
 
class  must
 \brief The must operator for state formulas More...
 
class  not_
 \brief The not operator for state formulas More...
 
class  nu
 \brief The nu operator for state formulas More...
 
class  or_
 \brief The or operator for state formulas More...
 
struct  parse_state_formula_options
 
class  plus
 \brief The plus operator for state formulas with values More...
 
struct  regular_formula_traverser
 \brief Traverser class More...
 
struct  sort_expression_builder
 \brief Builder class More...
 
struct  sort_expression_traverser
 \brief Traverser class More...
 
class  state_formula
 \brief A state formula More...
 
struct  state_formula_builder
 \brief Builder class More...
 
struct  state_formula_builder_base
 Builder class for pbes_expressions. Used as a base class for pbes_expression_builder. More...
 
struct  state_formula_predicate_variable_rename_builder
 
class  state_formula_specification
 
struct  state_formula_traverser
 \brief Traverser class More...
 
struct  state_formula_traverser_base
 Traversal class for pbes_expressions. Used as a base class for pbes_expression_traverser. More...
 
class  state_formula_type_checker
 
struct  state_formula_variable_rename_builder
 Visitor that renames variables using the specified identifier generator. Also bound variables are renamed! More...
 
struct  state_variable_traverser
 \brief Traverser class More...
 
class  sum
 \brief The sum over a data type for state formulas More...
 
class  supremum
 \brief The supremum over a data type for state formulas More...
 
class  true_
 \brief The value true for state formulas More...
 
class  variable
 \brief The state formula variable More...
 
struct  variable_builder
 \brief Builder class More...
 
struct  variable_traverser
 \brief Traverser class More...
 
class  yaled
 \brief The yaled operator for state formulas More...
 
class  yaled_timed
 \brief The timed yaled operator for state formulas More...
 

Typedefs

typedef atermpp::term_list< state_formulastate_formula_list
 \brief list of state_formulas
 
typedef std::vector< state_formulastate_formula_vector
 \brief vector of state_formulas
 

Functions

std::size_t count_fixpoints (const state_formula &x)
 Counts the number of fixpoints in a state formula.
 
template<typename T , typename OutputIterator >
void find_all_variables (const T &x, OutputIterator o)
 
template<typename T >
std::set< data::variablefind_all_variables (const T &x)
 
template<typename T , typename OutputIterator >
void find_free_variables (const T &x, OutputIterator o)
 
template<typename T , typename OutputIterator , typename VariableContainer >
void find_free_variables_with_bound (const T &x, OutputIterator o, const VariableContainer &bound)
 
template<typename T >
std::set< data::variablefind_free_variables (const T &x)
 
template<typename T , typename VariableContainer >
std::set< data::variablefind_free_variables_with_bound (const T &x, VariableContainer const &bound)
 
template<typename T , typename OutputIterator >
void find_identifiers (const T &x, OutputIterator o)
 
template<typename T >
std::set< core::identifier_stringfind_identifiers (const T &x)
 
template<typename T , typename OutputIterator >
void find_sort_expressions (const T &x, OutputIterator o)
 
template<typename T >
std::set< data::sort_expressionfind_sort_expressions (const T &x)
 
template<typename T , typename OutputIterator >
void find_function_symbols (const T &x, OutputIterator o)
 
template<typename T >
std::set< data::function_symbolfind_function_symbols (const T &x)
 
std::set< core::identifier_stringfind_state_variable_names (const state_formula &x)
 Returns the names of the state variables that occur in x.
 
template<typename T , typename OutputIterator >
void find_state_variables (const T &x, OutputIterator o)
 Returns all state variables that occur in an object.
 
template<typename T >
std::set< state_formulas::variablefind_state_variables (const T &x)
 Returns all state variables that occur in an object.
 
template<typename T , typename OutputIterator >
void find_free_state_variables (const T &x, OutputIterator o)
 Returns all free state variables that occur in an object.
 
template<typename T >
std::set< state_formulas::variablefind_free_state_variables (const T &x)
 Returns all free state variables that occur in an object.
 
template<typename T , typename OutputIterator >
void find_action_labels (const T &x, OutputIterator o)
 Returns all action labels that occur in an object.
 
template<typename T >
std::set< process::action_labelfind_action_labels (const T &x)
 Returns all action labels that occur in an object.
 
void check_state_variable_name_clashes (const state_formula &x)
 Throws an exception if the formula contains name clashes.
 
bool has_state_variable_name_clashes (const state_formula &x)
 Returns true if the formula contains name clashes.
 
void check_data_variable_name_clashes (const state_formula &x)
 Throws an exception if the formula contains name clashes in the parameters of mu/nu/exists/forall.
 
bool has_data_variable_name_clashes (const state_formula &x)
 Returns true if the formula contains parameter name clashes.
 
bool is_monotonous (const state_formula &f, const std::set< core::identifier_string > &non_negated_variables, const std::set< core::identifier_string > &negated_variables)
 Returns true if the state formula is monotonous.
 
bool is_monotonous (const state_formula &f)
 Returns true if the state formula is monotonous.
 
bool is_timed (const state_formula &x)
 Checks if a state formula is timed.
 
std::set< state_formulas::state_formulamaximal_closed_subformulas (const state_formula &x)
 
state_formula negate_variables (const core::identifier_string &name, bool quantitative, const state_formula &x)
 Negates variable instantiations in a state formula with a given name.
 
template<typename T >
bool is_normalized (const T &x)
 Checks if a state formula is normalized.
 
template<typename T >
void normalize (T &x, bool quantitative=false, bool negated=false, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 The function normalize brings (embedded) state formulas into positive normal form, i.e. a formula without any occurrences of ! or =>.
 
template<typename T >
normalize (const T &x, bool quantitative=false, bool negated=false, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 The function normalize brings (embedded) state formulas into positive normal form, i.e. a formula without any occurrences of ! or =>.
 
template<typename T >
void normalize_sorts (T &x, const data::sort_specification &sortspec, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename T >
normalize_sorts (const T &x, const data::sort_specification &sortspec, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
state_formula post_process_state_formula (const state_formula &formula, parse_state_formula_options options=parse_state_formula_options())
 
state_formula parse_state_formula (const std::string &text, lps::stochastic_specification &lpsspec, const bool formula_is_quantitative, parse_state_formula_options options=parse_state_formula_options())
 Parses a state formula from an input stream.
 
state_formula parse_state_formula (const std::string &text, lps::specification &lpsspec, const bool formula_is_quantitative, parse_state_formula_options options=parse_state_formula_options())
 Parses a state formula from an input stream.
 
state_formula parse_state_formula (std::istream &in, lps::stochastic_specification &lpsspec, const bool formula_is_quantitative, parse_state_formula_options options=parse_state_formula_options())
 Parses a state formula from an input stream.
 
state_formula parse_state_formula (std::istream &in, lps::specification &lpsspec, const bool formula_is_quantitative, parse_state_formula_options options=parse_state_formula_options())
 Parses a state formula from an input stream.
 
state_formula_specification parse_state_formula_specification (const std::string &text, const bool formula_is_quantitative, parse_state_formula_options options=parse_state_formula_options())
 Parses a state formula specification from a string.
 
state_formula_specification parse_state_formula_specification (std::istream &in, const bool formula_is_quantitative, parse_state_formula_options options=parse_state_formula_options())
 Parses a state formula specification from an input stream.
 
state_formula_specification parse_state_formula_specification (const std::string &text, lps::stochastic_specification &lpsspec, const bool formula_is_quantitative, parse_state_formula_options options=parse_state_formula_options())
 Parses a state formula specification from a string.
 
state_formula_specification parse_state_formula_specification (const std::string &text, lps::specification &lpsspec, const bool formula_is_quantitative, parse_state_formula_options options=parse_state_formula_options())
 Parses a state formula specification from a string.
 
state_formula_specification parse_state_formula_specification (std::istream &in, lps::stochastic_specification &lpsspec, const bool formula_is_quantitative, parse_state_formula_options options=parse_state_formula_options())
 Parses a state formula specification from an input stream.
 
state_formula_specification parse_state_formula_specification (std::istream &in, lps::specification &lpsspec, const bool formula_is_quantitative, parse_state_formula_options options=parse_state_formula_options())
 Parses a state formula specification from an input stream.
 
state_formula preprocess_nested_modal_operators (const state_formula &x)
 Preprocesses a state formula that contains (nested) modal operators.
 
state_formulas::state_formula preprocess_state_formula (const state_formulas::state_formula &formula, const std::set< core::identifier_string > &context_ids, bool preprocess_modal_operators, bool quantitative=false, 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.
 
constexpr int precedence (const mu &)
 
constexpr int precedence (const nu &)
 
constexpr int precedence (const forall &)
 
constexpr int precedence (const exists &)
 
constexpr int precedence (const infimum &)
 
constexpr int precedence (const supremum &)
 
constexpr int precedence (const sum &)
 
constexpr int precedence (const imp &)
 
constexpr int precedence (const or_ &)
 
constexpr int precedence (const and_ &)
 
constexpr int precedence (const plus &)
 
constexpr int precedence (const const_multiply &)
 
constexpr int precedence (const const_multiply_alt &)
 
constexpr int precedence (const must &)
 
constexpr int precedence (const may &)
 
constexpr int precedence (const not_ &)
 
constexpr int precedence (const minus &)
 
int precedence (const state_formula &x)
 
bool is_left_associative (const imp &)
 
bool is_left_associative (const or_ &)
 
bool is_left_associative (const and_ &)
 
bool is_left_associative (const plus &)
 
bool is_left_associative (const const_multiply &)
 
bool is_left_associative (const const_multiply_alt &)
 
bool is_left_associative (const state_formula &x)
 
bool is_right_associative (const imp &)
 
bool is_right_associative (const or_ &)
 
bool is_right_associative (const and_ &)
 
bool is_right_associative (const plus &)
 
bool is_right_associative (const const_multiply &)
 
bool is_right_associative (const const_multiply_alt &)
 
bool is_right_associative (const state_formula &x)
 
template<typename T >
void pp (const T &t, std::ostream &out)
 Prints the object t to a stream.
 
template<typename T >
std::string pp (const T &t)
 Returns a string representation of the object t.
 
template<typename T , typename Substitution >
void replace_sort_expressions (T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_sort_expressions (const T &x, const Substitution &sigma, bool innermost, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_data_expressions (T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_data_expressions (const T &x, const Substitution &sigma, bool innermost, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_all_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_all_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_free_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_free_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution , typename VariableContainer >
void replace_free_variables (T &x, const Substitution &sigma, const VariableContainer &bound_variables, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution , typename VariableContainer >
replace_free_variables (const T &x, const Substitution &sigma, const VariableContainer &bound_variables, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_state_formulas (T &x, Substitution sigma, bool innermost=true, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename T , typename Substitution >
replace_state_formulas (const T &x, Substitution sigma, bool innermost=true, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_variables_capture_avoiding (T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_variables_capture_avoiding (const T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_variables_capture_avoiding (T &x, Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_variables_capture_avoiding (const T &x, Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution , typename IdentifierGenerator >
void replace_variables_capture_avoiding_with_an_identifier_generator (T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution , typename IdentifierGenerator >
replace_variables_capture_avoiding_with_an_identifier_generator (const T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
state_formula resolve_state_variable_name_clashes (const state_formula &x)
 Resolves name clashes in state variables of formula x.
 
state_formula resolve_state_formula_data_variable_name_clashes (const state_formula &x, const std::set< core::identifier_string > &context_ids=std::set< core::identifier_string >())
 Resolves name clashes in data variables of formula x.
 
template<typename T , typename Rewriter >
void rewrite (T &x, Rewriter R, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Rewriter >
rewrite (const T &x, Rewriter R, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Rewriter , typename Substitution >
void rewrite (T &x, Rewriter R, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Rewriter , typename Substitution >
rewrite (const T &x, Rewriter R, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
bool is_true (const atermpp::aterm &x)
 
bool is_false (const atermpp::aterm &x)
 
bool is_not (const atermpp::aterm &x)
 
bool is_minus (const atermpp::aterm &x)
 
bool is_and (const atermpp::aterm &x)
 
bool is_or (const atermpp::aterm &x)
 
bool is_imp (const atermpp::aterm &x)
 
bool is_plus (const atermpp::aterm &x)
 
bool is_const_multiply (const atermpp::aterm &x)
 
bool is_const_multiply_alt (const atermpp::aterm &x)
 
bool is_forall (const atermpp::aterm &x)
 
bool is_exists (const atermpp::aterm &x)
 
bool is_infimum (const atermpp::aterm &x)
 
bool is_supremum (const atermpp::aterm &x)
 
bool is_sum (const atermpp::aterm &x)
 
bool is_must (const atermpp::aterm &x)
 
bool is_may (const atermpp::aterm &x)
 
bool is_yaled (const atermpp::aterm &x)
 
bool is_yaled_timed (const atermpp::aterm &x)
 
bool is_delay (const atermpp::aterm &x)
 
bool is_delay_timed (const atermpp::aterm &x)
 
bool is_variable (const atermpp::aterm &x)
 
bool is_nu (const atermpp::aterm &x)
 
bool is_mu (const atermpp::aterm &x)
 
bool is_state_formula (const atermpp::aterm &x)
 
std::string pp (const state_formula &x)
 
std::ostream & operator<< (std::ostream &out, const state_formula &x)
 
void swap (state_formula &t1, state_formula &t2)
 \brief swap overload
 
std::string pp (const true_ &x)
 
std::ostream & operator<< (std::ostream &out, const true_ &x)
 
void swap (true_ &t1, true_ &t2)
 \brief swap overload
 
std::string pp (const false_ &x)
 
std::ostream & operator<< (std::ostream &out, const false_ &x)
 
void swap (false_ &t1, false_ &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_not_ (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const not_ &x)
 
std::ostream & operator<< (std::ostream &out, const not_ &x)
 
void swap (not_ &t1, not_ &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_minus (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const minus &x)
 
std::ostream & operator<< (std::ostream &out, const minus &x)
 
void swap (minus &t1, minus &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_and_ (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const and_ &x)
 
std::ostream & operator<< (std::ostream &out, const and_ &x)
 
void swap (and_ &t1, and_ &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_or_ (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const or_ &x)
 
std::ostream & operator<< (std::ostream &out, const or_ &x)
 
void swap (or_ &t1, or_ &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_imp (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const imp &x)
 
std::ostream & operator<< (std::ostream &out, const imp &x)
 
void swap (imp &t1, imp &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_plus (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const plus &x)
 
std::ostream & operator<< (std::ostream &out, const plus &x)
 
void swap (plus &t1, plus &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_const_multiply (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const const_multiply &x)
 
std::ostream & operator<< (std::ostream &out, const const_multiply &x)
 
void swap (const_multiply &t1, const_multiply &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_const_multiply_alt (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const const_multiply_alt &x)
 
std::ostream & operator<< (std::ostream &out, const const_multiply_alt &x)
 
void swap (const_multiply_alt &t1, const_multiply_alt &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_forall (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const forall &x)
 
std::ostream & operator<< (std::ostream &out, const forall &x)
 
void swap (forall &t1, forall &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_exists (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const exists &x)
 
std::ostream & operator<< (std::ostream &out, const exists &x)
 
void swap (exists &t1, exists &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_infimum (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const infimum &x)
 
std::ostream & operator<< (std::ostream &out, const infimum &x)
 
void swap (infimum &t1, infimum &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_supremum (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const supremum &x)
 
std::ostream & operator<< (std::ostream &out, const supremum &x)
 
void swap (supremum &t1, supremum &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_sum (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const sum &x)
 
std::ostream & operator<< (std::ostream &out, const sum &x)
 
void swap (sum &t1, sum &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_must (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const must &x)
 
std::ostream & operator<< (std::ostream &out, const must &x)
 
void swap (must &t1, must &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_may (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const may &x)
 
std::ostream & operator<< (std::ostream &out, const may &x)
 
void swap (may &t1, may &t2)
 \brief swap overload
 
std::string pp (const yaled &x)
 
std::ostream & operator<< (std::ostream &out, const yaled &x)
 
void swap (yaled &t1, yaled &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_yaled_timed (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const yaled_timed &x)
 
std::ostream & operator<< (std::ostream &out, const yaled_timed &x)
 
void swap (yaled_timed &t1, yaled_timed &t2)
 \brief swap overload
 
std::string pp (const delay &x)
 
std::ostream & operator<< (std::ostream &out, const delay &x)
 
void swap (delay &t1, delay &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_delay_timed (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const delay_timed &x)
 
std::ostream & operator<< (std::ostream &out, const delay_timed &x)
 
void swap (delay_timed &t1, delay_timed &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_variable (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const variable &x)
 
std::ostream & operator<< (std::ostream &out, const variable &x)
 
void swap (variable &t1, variable &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_nu (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const nu &x)
 
std::ostream & operator<< (std::ostream &out, const nu &x)
 
void swap (nu &t1, nu &t2)
 \brief swap overload
 
template<class... ARGUMENTS>
void make_mu (atermpp::aterm &t, const ARGUMENTS &... args)
 
std::string pp (const mu &x)
 
std::ostream & operator<< (std::ostream &out, const mu &x)
 
void swap (mu &t1, mu &t2)
 \brief swap overload
 
state_formula normalize_sorts (const state_formula &x, const data::sort_specification &sortspec)
 
state_formulas::state_formula translate_user_notation (const state_formulas::state_formula &x)
 
std::set< data::sort_expressionfind_sort_expressions (const state_formulas::state_formula &x)
 
std::set< data::variablefind_all_variables (const state_formulas::state_formula &x)
 
std::set< data::variablefind_free_variables (const state_formulas::state_formula &x)
 
std::set< core::identifier_stringfind_identifiers (const state_formulas::state_formula &x)
 
std::set< process::action_labelfind_action_labels (const state_formulas::state_formula &x)
 
bool find_nil (const state_formulas::state_formula &x)
 
template<typename IdentifierGenerator >
state_formula_predicate_variable_rename_builder< IdentifierGenerator > make_state_formula_predicate_variable_rename_builder (IdentifierGenerator &generator)
 Utility function for creating a state_formula_predicate_variable_rename_builder.
 
template<typename IdentifierGenerator >
state_formula rename_predicate_variables (const state_formula &f, IdentifierGenerator &generator)
 Renames predicate variables of the formula f using the specified identifier generator.
 
state_formula rename_variables (const state_formula &f, const std::set< core::identifier_string > &forbidden_identifiers)
 Renames all data variables in the formula f such that the forbidden identifiers are not used.
 
std::string pp (const state_formula_specification &x)
 
std::ostream & operator<< (std::ostream &out, const state_formula_specification &x)
 
state_formula translate_regular_formulas (const state_formula &x)
 Translates regular formulas appearing in f into action formulas.
 
template<typename T >
void translate_user_notation (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
 
template<typename T >
translate_user_notation (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename VariableContainer , typename ActionLabelContainer >
state_formula typecheck_state_formula (const state_formula &x, const bool formula_is_quantitative, const data::data_specification &dataspec=data::data_specification(), const ActionLabelContainer &action_labels=ActionLabelContainer(), const VariableContainer &variables=VariableContainer())
 Type check a state formula. Throws an exception if something went wrong.
 
state_formula typecheck_state_formula (const state_formula &x, const lps::stochastic_specification &lpsspec, const bool formula_is_quantitative)
 Type check a state formula. Throws an exception if something went wrong.
 
void typecheck_state_formula_specification (state_formula_specification &formspec, const bool formula_is_quantitative)
 Typecheck the state formula specification formspec. It is assumed that the formula is self contained, i.e. all actions and sorts must be declared.
 
void typecheck_state_formula_specification (state_formula_specification &formspec, const lps::stochastic_specification &lpsspec, const bool formula_is_quantitative)
 Typecheck the state formula specification formspec. It is assumed that the formula is not self contained, i.e. some of the actions and sorts may be declared in lpsspec.
 

Typedef Documentation

◆ state_formula_list

◆ state_formula_vector

\brief vector of state_formulas

Definition at line 67 of file state_formula.h.

Function Documentation

◆ check_data_variable_name_clashes()

void mcrl2::state_formulas::check_data_variable_name_clashes ( const state_formula x)
inline

Throws an exception if the formula contains name clashes in the parameters of mu/nu/exists/forall.

Definition at line 192 of file has_name_clashes.h.

◆ check_state_variable_name_clashes()

void mcrl2::state_formulas::check_state_variable_name_clashes ( const state_formula x)
inline

Throws an exception if the formula contains name clashes.

Definition at line 169 of file has_name_clashes.h.

◆ count_fixpoints()

std::size_t mcrl2::state_formulas::count_fixpoints ( const state_formula x)
inline

Counts the number of fixpoints in a state formula.

Parameters
xA state formula
Returns
The number of fixpoints in a state formula

Definition at line 57 of file count_fixpoints.h.

◆ find_action_labels() [1/3]

std::set< process::action_label > mcrl2::state_formulas::find_action_labels ( const state_formulas::state_formula x)

Definition at line 123 of file modal_formula.cpp.

◆ find_action_labels() [2/3]

template<typename T >
std::set< process::action_label > mcrl2::state_formulas::find_action_labels ( const T &  x)

Returns all action labels that occur in an object.

Parameters
[in]xan object containing action labels
Returns
All action labels that occur in the object x

Definition at line 587 of file find.h.

◆ find_action_labels() [3/3]

template<typename T , typename OutputIterator >
void mcrl2::state_formulas::find_action_labels ( const T &  x,
OutputIterator  o 
)

Returns all action labels that occur in an object.

Parameters
[in]xan object containing action labels
[in,out]oan output iterator to which all action labels occurring in x are written.
Returns
All action labels that occur in the term x

Definition at line 578 of file find.h.

◆ find_all_variables() [1/3]

std::set< data::variable > mcrl2::state_formulas::find_all_variables ( const state_formulas::state_formula x)

Definition at line 120 of file modal_formula.cpp.

◆ find_all_variables() [2/3]

template<typename T >
std::set< data::variable > mcrl2::state_formulas::find_all_variables ( const T &  x)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \return All variables that occur in the object x

Definition at line 310 of file find.h.

◆ find_all_variables() [3/3]

template<typename T , typename OutputIterator >
void mcrl2::state_formulas::find_all_variables ( const T &  x,
OutputIterator  o 
)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are written. \return All variables that occur in the term x

Definition at line 301 of file find.h.

◆ find_free_state_variables() [1/2]

template<typename T >
std::set< state_formulas::variable > mcrl2::state_formulas::find_free_state_variables ( const T &  x)

Returns all free state variables that occur in an object.

Parameters
[in]xan object containing variables
Returns
All state variables that occur in the object x

Definition at line 566 of file find.h.

◆ find_free_state_variables() [2/2]

template<typename T , typename OutputIterator >
void mcrl2::state_formulas::find_free_state_variables ( const T &  x,
OutputIterator  o 
)

Returns all free state variables that occur in an object.

Parameters
[in]xan object containing state variables
[in,out]oan output iterator to which all state variables occurring in x are added.
Returns
All free state variables that occur in the object x

Definition at line 557 of file find.h.

◆ find_free_variables() [1/3]

std::set< data::variable > mcrl2::state_formulas::find_free_variables ( const state_formulas::state_formula x)

Definition at line 121 of file modal_formula.cpp.

◆ find_free_variables() [2/3]

template<typename T >
std::set< data::variable > mcrl2::state_formulas::find_free_variables ( const T &  x)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \return All free variables that occur in the object x

Definition at line 342 of file find.h.

◆ find_free_variables() [3/3]

template<typename T , typename OutputIterator >
void mcrl2::state_formulas::find_free_variables ( const T &  x,
OutputIterator  o 
)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are added. \return All free variables that occur in the object x

Definition at line 322 of file find.h.

◆ find_free_variables_with_bound() [1/2]

template<typename T , typename OutputIterator , typename VariableContainer >
void mcrl2::state_formulas::find_free_variables_with_bound ( const T &  x,
OutputIterator  o,
const VariableContainer &  bound 
)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in,out] o an output iterator to which all variables occurring in x are written. \param[in] bound a container of variables \return All free variables that occur in the object x

Definition at line 333 of file find.h.

◆ find_free_variables_with_bound() [2/2]

template<typename T , typename VariableContainer >
std::set< data::variable > mcrl2::state_formulas::find_free_variables_with_bound ( const T &  x,
VariableContainer const &  bound 
)

\brief Returns all variables that occur in an object \param[in] x an object containing variables \param[in] bound a bound a container of variables \return All free variables that occur in the object x

Definition at line 354 of file find.h.

◆ find_function_symbols() [1/2]

template<typename T >
std::set< data::function_symbol > mcrl2::state_formulas::find_function_symbols ( const T &  x)

\brief Returns all function symbols that occur in an object \param[in] x an object containing function symbols \return All function symbols that occur in the object x

Definition at line 417 of file find.h.

◆ find_function_symbols() [2/2]

template<typename T , typename OutputIterator >
void mcrl2::state_formulas::find_function_symbols ( const T &  x,
OutputIterator  o 
)

\brief Returns all function symbols that occur in an object \param[in] x an object containing function symbols \param[in,out] o an output iterator to which all function symbols occurring in x are written. \return All function symbols that occur in the term x

Definition at line 408 of file find.h.

◆ find_identifiers() [1/3]

std::set< core::identifier_string > mcrl2::state_formulas::find_identifiers ( const state_formulas::state_formula x)

Definition at line 122 of file modal_formula.cpp.

◆ find_identifiers() [2/3]

template<typename T >
std::set< core::identifier_string > mcrl2::state_formulas::find_identifiers ( const T &  x)

\brief Returns all identifiers that occur in an object \param[in] x an object containing identifiers \return All identifiers that occur in the object x

Definition at line 375 of file find.h.

◆ find_identifiers() [3/3]

template<typename T , typename OutputIterator >
void mcrl2::state_formulas::find_identifiers ( const T &  x,
OutputIterator  o 
)

\brief Returns all identifiers that occur in an object \param[in] x an object containing identifiers \param[in,out] o an output iterator to which all identifiers occurring in x are written. \return All identifiers that occur in the term x

Definition at line 366 of file find.h.

◆ find_nil()

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

◆ find_sort_expressions() [1/3]

std::set< data::sort_expression > mcrl2::state_formulas::find_sort_expressions ( const state_formulas::state_formula x)

Definition at line 119 of file modal_formula.cpp.

◆ find_sort_expressions() [2/3]

template<typename T >
std::set< data::sort_expression > mcrl2::state_formulas::find_sort_expressions ( const T &  x)

\brief Returns all sort expressions that occur in an object \param[in] x an object containing sort expressions \return All sort expressions that occur in the object x

Definition at line 396 of file find.h.

◆ find_sort_expressions() [3/3]

template<typename T , typename OutputIterator >
void mcrl2::state_formulas::find_sort_expressions ( const T &  x,
OutputIterator  o 
)

\brief Returns all sort expressions that occur in an object \param[in] x an object containing sort expressions \param[in,out] o an output iterator to which all sort expressions occurring in x are written. \return All sort expressions that occur in the term x

Definition at line 387 of file find.h.

◆ find_state_variable_names()

std::set< core::identifier_string > mcrl2::state_formulas::find_state_variable_names ( const state_formula x)
inline

Returns the names of the state variables that occur in x.

Parameters
[in]xA state formula

Definition at line 524 of file find.h.

◆ find_state_variables() [1/2]

template<typename T >
std::set< state_formulas::variable > mcrl2::state_formulas::find_state_variables ( const T &  x)

Returns all state variables that occur in an object.

Parameters
[in]xan object containing variables
Returns
All state variables that occur in the object x

Definition at line 545 of file find.h.

◆ find_state_variables() [2/2]

template<typename T , typename OutputIterator >
void mcrl2::state_formulas::find_state_variables ( const T &  x,
OutputIterator  o 
)

Returns all state variables that occur in an object.

Parameters
[in]xan object containing state variables
[in,out]oan output iterator to which all state variables occurring in x are written.
Returns
All variables that occur in the term x

Definition at line 536 of file find.h.

◆ has_data_variable_name_clashes()

bool mcrl2::state_formulas::has_data_variable_name_clashes ( const state_formula x)
inline

Returns true if the formula contains parameter name clashes.

Definition at line 200 of file has_name_clashes.h.

◆ has_state_variable_name_clashes()

bool mcrl2::state_formulas::has_state_variable_name_clashes ( const state_formula x)
inline

Returns true if the formula contains name clashes.

Definition at line 177 of file has_name_clashes.h.

◆ is_and()

bool mcrl2::state_formulas::is_and ( const atermpp::aterm x)
inline

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

Definition at line 448 of file state_formula.h.

◆ is_const_multiply()

bool mcrl2::state_formulas::is_const_multiply ( const atermpp::aterm x)
inline

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

Definition at line 752 of file state_formula.h.

◆ is_const_multiply_alt()

bool mcrl2::state_formulas::is_const_multiply_alt ( const atermpp::aterm x)
inline

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

Definition at line 828 of file state_formula.h.

◆ is_delay()

bool mcrl2::state_formulas::is_delay ( const atermpp::aterm x)
inline

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

Definition at line 1537 of file state_formula.h.

◆ is_delay_timed()

bool mcrl2::state_formulas::is_delay_timed ( const atermpp::aterm x)
inline

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

Definition at line 1608 of file state_formula.h.

◆ is_exists()

bool mcrl2::state_formulas::is_exists ( const atermpp::aterm x)
inline

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

Definition at line 980 of file state_formula.h.

◆ is_false()

bool mcrl2::state_formulas::is_false ( const atermpp::aterm x)
inline

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

Definition at line 230 of file state_formula.h.

◆ is_forall()

bool mcrl2::state_formulas::is_forall ( const atermpp::aterm x)
inline

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

Definition at line 904 of file state_formula.h.

◆ is_imp()

bool mcrl2::state_formulas::is_imp ( const atermpp::aterm x)
inline

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

Definition at line 600 of file state_formula.h.

◆ is_infimum()

bool mcrl2::state_formulas::is_infimum ( const atermpp::aterm x)
inline

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

Definition at line 1056 of file state_formula.h.

◆ is_left_associative() [1/7]

bool mcrl2::state_formulas::is_left_associative ( const and_ )
inline

Definition at line 340 of file print.h.

◆ is_left_associative() [2/7]

bool mcrl2::state_formulas::is_left_associative ( const const_multiply )
inline

Definition at line 342 of file print.h.

◆ is_left_associative() [3/7]

bool mcrl2::state_formulas::is_left_associative ( const const_multiply_alt )
inline

Definition at line 343 of file print.h.

◆ is_left_associative() [4/7]

bool mcrl2::state_formulas::is_left_associative ( const imp )
inline

Definition at line 338 of file print.h.

◆ is_left_associative() [5/7]

bool mcrl2::state_formulas::is_left_associative ( const or_ )
inline

Definition at line 339 of file print.h.

◆ is_left_associative() [6/7]

bool mcrl2::state_formulas::is_left_associative ( const plus )
inline

Definition at line 341 of file print.h.

◆ is_left_associative() [7/7]

bool mcrl2::state_formulas::is_left_associative ( const state_formula x)
inline

Definition at line 344 of file print.h.

◆ is_may()

bool mcrl2::state_formulas::is_may ( const atermpp::aterm x)
inline

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

Definition at line 1360 of file state_formula.h.

◆ is_minus()

bool mcrl2::state_formulas::is_minus ( const atermpp::aterm x)
inline

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

Definition at line 372 of file state_formula.h.

◆ is_monotonous() [1/2]

bool mcrl2::state_formulas::is_monotonous ( const state_formula f)
inline

Returns true if the state formula is monotonous.

Parameters
fA modal formula
Returns
True if the state formula is monotonous.

Definition at line 169 of file is_monotonous.h.

◆ is_monotonous() [2/2]

bool mcrl2::state_formulas::is_monotonous ( const state_formula f,
const std::set< core::identifier_string > &  non_negated_variables,
const std::set< core::identifier_string > &  negated_variables 
)
inline

Returns true if the state formula is monotonous.

Parameters
fA modal formula.
non_negated_variablesNames of state variables that occur positively in the current scope.
negated_variablesNames of state variables that occur negatively in the current scope.
Returns
True if the state formula is monotonous.

Definition at line 30 of file is_monotonous.h.

◆ is_mu()

bool mcrl2::state_formulas::is_mu ( const atermpp::aterm x)
inline

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

Definition at line 1861 of file state_formula.h.

◆ is_must()

bool mcrl2::state_formulas::is_must ( const atermpp::aterm x)
inline

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

Definition at line 1284 of file state_formula.h.

◆ is_normalized()

template<typename T >
bool mcrl2::state_formulas::is_normalized ( const T &  x)

Checks if a state formula is normalized.

Parameters
xA PBES expression.
Returns
True if the state formula is normalized.

Definition at line 411 of file normalize.h.

◆ is_not()

bool mcrl2::state_formulas::is_not ( const atermpp::aterm x)
inline

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

Definition at line 301 of file state_formula.h.

◆ is_nu()

bool mcrl2::state_formulas::is_nu ( const atermpp::aterm x)
inline

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

Definition at line 1775 of file state_formula.h.

◆ is_or()

bool mcrl2::state_formulas::is_or ( const atermpp::aterm x)
inline

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

Definition at line 524 of file state_formula.h.

◆ is_plus()

bool mcrl2::state_formulas::is_plus ( const atermpp::aterm x)
inline

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

Definition at line 676 of file state_formula.h.

◆ is_right_associative() [1/7]

bool mcrl2::state_formulas::is_right_associative ( const and_ )
inline

Definition at line 357 of file print.h.

◆ is_right_associative() [2/7]

bool mcrl2::state_formulas::is_right_associative ( const const_multiply )
inline

Definition at line 359 of file print.h.

◆ is_right_associative() [3/7]

bool mcrl2::state_formulas::is_right_associative ( const const_multiply_alt )
inline

Definition at line 360 of file print.h.

◆ is_right_associative() [4/7]

bool mcrl2::state_formulas::is_right_associative ( const imp )
inline

Definition at line 355 of file print.h.

◆ is_right_associative() [5/7]

bool mcrl2::state_formulas::is_right_associative ( const or_ )
inline

Definition at line 356 of file print.h.

◆ is_right_associative() [6/7]

bool mcrl2::state_formulas::is_right_associative ( const plus )
inline

Definition at line 358 of file print.h.

◆ is_right_associative() [7/7]

bool mcrl2::state_formulas::is_right_associative ( const state_formula x)
inline

Definition at line 361 of file print.h.

◆ is_state_formula()

bool mcrl2::state_formulas::is_state_formula ( const atermpp::aterm x)
inline

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

Definition at line 99 of file state_formula.h.

◆ is_sum()

bool mcrl2::state_formulas::is_sum ( const atermpp::aterm x)
inline

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

Definition at line 1208 of file state_formula.h.

◆ is_supremum()

bool mcrl2::state_formulas::is_supremum ( const atermpp::aterm x)
inline

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

Definition at line 1132 of file state_formula.h.

◆ is_timed()

bool mcrl2::state_formulas::is_timed ( const state_formula x)
inline

Checks if a state formula is timed.

Parameters
xA state formula
Returns
True if a state formula is timed

Definition at line 60 of file is_timed.h.

◆ is_true()

bool mcrl2::state_formulas::is_true ( const atermpp::aterm x)
inline

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

Definition at line 177 of file state_formula.h.

◆ is_variable()

bool mcrl2::state_formulas::is_variable ( const atermpp::aterm x)
inline

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

Definition at line 1689 of file state_formula.h.

◆ is_yaled()

bool mcrl2::state_formulas::is_yaled ( const atermpp::aterm x)
inline

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

Definition at line 1413 of file state_formula.h.

◆ is_yaled_timed()

bool mcrl2::state_formulas::is_yaled_timed ( const atermpp::aterm x)
inline

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

Definition at line 1484 of file state_formula.h.

◆ make_and_()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_and_ ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_and_ constructs a new term into a given address. \

Parameters
tThe reference into which the new and_ is constructed.

Definition at line 439 of file state_formula.h.

◆ make_const_multiply()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_const_multiply ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_const_multiply constructs a new term into a given address. \

Parameters
tThe reference into which the new const_multiply is constructed.

Definition at line 743 of file state_formula.h.

◆ make_const_multiply_alt()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_const_multiply_alt ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_const_multiply_alt constructs a new term into a given address. \

Parameters
tThe reference into which the new const_multiply_alt is constructed.

Definition at line 819 of file state_formula.h.

◆ make_delay_timed()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_delay_timed ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_delay_timed constructs a new term into a given address. \

Parameters
tThe reference into which the new delay_timed is constructed.

Definition at line 1599 of file state_formula.h.

◆ make_exists()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_exists ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_exists constructs a new term into a given address. \

Parameters
tThe reference into which the new exists is constructed.

Definition at line 971 of file state_formula.h.

◆ make_forall()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_forall ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_forall constructs a new term into a given address. \

Parameters
tThe reference into which the new forall is constructed.

Definition at line 895 of file state_formula.h.

◆ make_imp()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_imp ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_imp constructs a new term into a given address. \

Parameters
tThe reference into which the new imp is constructed.

Definition at line 591 of file state_formula.h.

◆ make_infimum()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_infimum ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_infimum constructs a new term into a given address. \

Parameters
tThe reference into which the new infimum is constructed.

Definition at line 1047 of file state_formula.h.

◆ make_may()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_may ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_may constructs a new term into a given address. \

Parameters
tThe reference into which the new may is constructed.

Definition at line 1351 of file state_formula.h.

◆ make_minus()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_minus ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_minus constructs a new term into a given address. \

Parameters
tThe reference into which the new minus is constructed.

Definition at line 363 of file state_formula.h.

◆ make_mu()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_mu ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_mu constructs a new term into a given address. \

Parameters
tThe reference into which the new mu is constructed.

Definition at line 1852 of file state_formula.h.

◆ make_must()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_must ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_must constructs a new term into a given address. \

Parameters
tThe reference into which the new must is constructed.

Definition at line 1275 of file state_formula.h.

◆ make_not_()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_not_ ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_not_ constructs a new term into a given address. \

Parameters
tThe reference into which the new not_ is constructed.

Definition at line 292 of file state_formula.h.

◆ make_nu()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_nu ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_nu constructs a new term into a given address. \

Parameters
tThe reference into which the new nu is constructed.

Definition at line 1766 of file state_formula.h.

◆ make_or_()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_or_ ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_or_ constructs a new term into a given address. \

Parameters
tThe reference into which the new or_ is constructed.

Definition at line 515 of file state_formula.h.

◆ make_plus()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_plus ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_plus constructs a new term into a given address. \

Parameters
tThe reference into which the new plus is constructed.

Definition at line 667 of file state_formula.h.

◆ make_state_formula_predicate_variable_rename_builder()

template<typename IdentifierGenerator >
state_formula_predicate_variable_rename_builder< IdentifierGenerator > mcrl2::state_formulas::make_state_formula_predicate_variable_rename_builder ( IdentifierGenerator &  generator)

Utility function for creating a state_formula_predicate_variable_rename_builder.

Parameters
generatorA generator for fresh identifiers
Returns
a state_formula_predicate_variable_rename_builder

Definition at line 111 of file state_formula_rename.h.

◆ make_sum()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_sum ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_sum constructs a new term into a given address. \

Parameters
tThe reference into which the new sum is constructed.

Definition at line 1199 of file state_formula.h.

◆ make_supremum()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_supremum ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_supremum constructs a new term into a given address. \

Parameters
tThe reference into which the new supremum is constructed.

Definition at line 1123 of file state_formula.h.

◆ make_variable()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_variable ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_variable constructs a new term into a given address. \

Parameters
tThe reference into which the new variable is constructed.

Definition at line 1680 of file state_formula.h.

◆ make_yaled_timed()

template<class... ARGUMENTS>
void mcrl2::state_formulas::make_yaled_timed ( atermpp::aterm t,
const ARGUMENTS &...  args 
)
inline

\brief Make_yaled_timed constructs a new term into a given address. \

Parameters
tThe reference into which the new yaled_timed is constructed.

Definition at line 1475 of file state_formula.h.

◆ maximal_closed_subformulas()

std::set< state_formulas::state_formula > mcrl2::state_formulas::maximal_closed_subformulas ( const state_formula x)
inline

Definition at line 247 of file maximal_closed_subformula.h.

◆ negate_variables()

state_formula mcrl2::state_formulas::negate_variables ( const core::identifier_string name,
bool  quantitative,
const state_formula x 
)
inline

Negates variable instantiations in a state formula with a given name.

Parameters
nameThe name of the variables that should be negated.
xThe state formula.

Definition at line 69 of file negate_variables.h.

◆ normalize() [1/2]

template<typename T >
T mcrl2::state_formulas::normalize ( const T &  x,
bool  quantitative = false,
bool  negated = false,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

The function normalize brings (embedded) state formulas into positive normal form, i.e. a formula without any occurrences of ! or =>.

Parameters
xan object containing state formulas
quantitativeIndication whether the formula is a quantitative boolean formula.
negatedIndication whether the formula must be interpreted as being negated.

Definition at line 436 of file normalize.h.

◆ normalize() [2/2]

template<typename T >
void mcrl2::state_formulas::normalize ( T &  x,
bool  quantitative = false,
bool  negated = false,
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

The function normalize brings (embedded) state formulas into positive normal form, i.e. a formula without any occurrences of ! or =>.

Parameters
xan object containing state formulas.
quantitativeIndication whether the formula is a quantitative boolean formula.
negatedIndication whether the formula must be interpreted as being negated.

Definition at line 424 of file normalize.h.

◆ normalize_sorts() [1/3]

state_formulas::state_formula mcrl2::state_formulas::normalize_sorts ( const state_formula x,
const data::sort_specification sortspec 
)

Definition at line 117 of file modal_formula.cpp.

◆ normalize_sorts() [2/3]

template<typename T >
T mcrl2::state_formulas::normalize_sorts ( const T &  x,
const data::sort_specification sortspec,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 84 of file normalize_sorts.h.

◆ normalize_sorts() [3/3]

template<typename T >
void mcrl2::state_formulas::normalize_sorts ( T &  x,
const data::sort_specification sortspec,
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *  = 0 
)

Definition at line 75 of file normalize_sorts.h.

◆ operator<<() [1/26]

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

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

Definition at line 461 of file state_formula.h.

◆ operator<<() [2/26]

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

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

Definition at line 765 of file state_formula.h.

◆ operator<<() [3/26]

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

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

Definition at line 841 of file state_formula.h.

◆ operator<<() [4/26]

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

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

Definition at line 1550 of file state_formula.h.

◆ operator<<() [5/26]

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

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

Definition at line 1621 of file state_formula.h.

◆ operator<<() [6/26]

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

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

Definition at line 993 of file state_formula.h.

◆ operator<<() [7/26]

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

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

Definition at line 243 of file state_formula.h.

◆ operator<<() [8/26]

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

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

Definition at line 917 of file state_formula.h.

◆ operator<<() [9/26]

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

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

Definition at line 613 of file state_formula.h.

◆ operator<<() [10/26]

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

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

Definition at line 1069 of file state_formula.h.

◆ operator<<() [11/26]

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

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

Definition at line 1373 of file state_formula.h.

◆ operator<<() [12/26]

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

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

Definition at line 385 of file state_formula.h.

◆ operator<<() [13/26]

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

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

Definition at line 1874 of file state_formula.h.

◆ operator<<() [14/26]

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

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

Definition at line 1297 of file state_formula.h.

◆ operator<<() [15/26]

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

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

Definition at line 314 of file state_formula.h.

◆ operator<<() [16/26]

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

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

Definition at line 1788 of file state_formula.h.

◆ operator<<() [17/26]

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

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

Definition at line 537 of file state_formula.h.

◆ operator<<() [18/26]

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

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

Definition at line 689 of file state_formula.h.

◆ operator<<() [19/26]

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

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

Definition at line 137 of file state_formula.h.

◆ operator<<() [20/26]

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

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

Definition at line 97 of file state_formula_specification.h.

◆ operator<<() [21/26]

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

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

Definition at line 1221 of file state_formula.h.

◆ operator<<() [22/26]

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

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

Definition at line 1145 of file state_formula.h.

◆ operator<<() [23/26]

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

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

Definition at line 190 of file state_formula.h.

◆ operator<<() [24/26]

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

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

Definition at line 1702 of file state_formula.h.

◆ operator<<() [25/26]

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

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

Definition at line 1426 of file state_formula.h.

◆ operator<<() [26/26]

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

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

Definition at line 1497 of file state_formula.h.

◆ parse_state_formula() [1/4]

state_formula mcrl2::state_formulas::parse_state_formula ( const std::string &  text,
lps::specification lpsspec,
const bool  formula_is_quantitative,
parse_state_formula_options  options = parse_state_formula_options() 
)
inline

Parses a state formula from an input stream.

Parameters
textA string.
lpsspecA linear process specification used as context. The data specification of lpsspec is extended with sorts appearing in the formula.
formula_is_quantitativeIf true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
optionsA set of options guiding parsing.
Returns
The parse result.

Definition at line 166 of file parse.h.

◆ parse_state_formula() [2/4]

state_formula mcrl2::state_formulas::parse_state_formula ( const std::string &  text,
lps::stochastic_specification lpsspec,
const bool  formula_is_quantitative,
parse_state_formula_options  options = parse_state_formula_options() 
)
inline

Parses a state formula from an input stream.

Parameters
textA string.
lpsspecA stochastic linear process specification used as context. The data specification of lpsspec is extended with sorts appearing in the formula.
formula_is_quantitativeIf true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
optionsA set of options guiding parsing.
Returns
The parse result.

Definition at line 144 of file parse.h.

◆ parse_state_formula() [3/4]

state_formula mcrl2::state_formulas::parse_state_formula ( std::istream &  in,
lps::specification lpsspec,
const bool  formula_is_quantitative,
parse_state_formula_options  options = parse_state_formula_options() 
)
inline

Parses a state formula from an input stream.

Parameters
inA stream.
lpsspecA linear process specification used as context. The data specification of lpsspec is extended with sorts appearing in the formula.
formula_is_quantitativeIf true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
optionsA set of options guiding parsing.
Returns
The parse result.

Definition at line 202 of file parse.h.

◆ parse_state_formula() [4/4]

state_formula mcrl2::state_formulas::parse_state_formula ( std::istream &  in,
lps::stochastic_specification lpsspec,
const bool  formula_is_quantitative,
parse_state_formula_options  options = parse_state_formula_options() 
)
inline

Parses a state formula from an input stream.

Parameters
inA stream.
lpsspecA stochastic linear process specification used as context. The data specification of lpsspec is extended with sorts appearing in the formula.
formula_is_quantitativeIf true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
optionsA set of options guiding parsing.
Returns
The parse result.

Definition at line 185 of file parse.h.

◆ parse_state_formula_specification() [1/6]

state_formula_specification mcrl2::state_formulas::parse_state_formula_specification ( const std::string &  text,
const bool  formula_is_quantitative,
parse_state_formula_options  options = parse_state_formula_options() 
)
inline

Parses a state formula specification from a string.

Parameters
textA string.
formula_is_quantitativeIf true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
optionsA set of options guiding parsing.
Returns
The parse result.

Definition at line 220 of file parse.h.

◆ parse_state_formula_specification() [2/6]

state_formula_specification mcrl2::state_formulas::parse_state_formula_specification ( const std::string &  text,
lps::specification lpsspec,
const bool  formula_is_quantitative,
parse_state_formula_options  options = parse_state_formula_options() 
)
inline

Parses a state formula specification from a string.

Parameters
textA string
lpsspecA linear process containing data and action declarations necessary to type check the state formula.
formula_is_quantitativeIf true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
optionsA set of options guiding parsing.
Returns
The parse result

Definition at line 291 of file parse.h.

◆ parse_state_formula_specification() [3/6]

state_formula_specification mcrl2::state_formulas::parse_state_formula_specification ( const std::string &  text,
lps::stochastic_specification lpsspec,
const bool  formula_is_quantitative,
parse_state_formula_options  options = parse_state_formula_options() 
)
inline

Parses a state formula specification from a string.

Parameters
textA string
lpsspecA linear process containing data and action declarations necessary to type check the state formula.
formula_is_quantitativeIf true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
optionsA set of options guiding parsing.
Returns
The parse result

Definition at line 258 of file parse.h.

◆ parse_state_formula_specification() [4/6]

state_formula_specification mcrl2::state_formulas::parse_state_formula_specification ( std::istream &  in,
const bool  formula_is_quantitative,
parse_state_formula_options  options = parse_state_formula_options() 
)
inline

Parses a state formula specification from an input stream.

Parameters
inAn input stream.
formula_is_quantitativeIf true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
optionsA set of options guiding parsing.
Returns
The parse result.

Definition at line 241 of file parse.h.

◆ parse_state_formula_specification() [5/6]

state_formula_specification mcrl2::state_formulas::parse_state_formula_specification ( std::istream &  in,
lps::specification lpsspec,
const bool  formula_is_quantitative,
parse_state_formula_options  options = parse_state_formula_options() 
)
inline

Parses a state formula specification from an input stream.

Parameters
inAn input stream.
lpsspecA linear process containing data and action declarations necessary to type check the state formula.
formula_is_quantitativeIf true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
optionsA set of options guiding parsing.
Returns
The parse result.

Definition at line 326 of file parse.h.

◆ parse_state_formula_specification() [6/6]

state_formula_specification mcrl2::state_formulas::parse_state_formula_specification ( std::istream &  in,
lps::stochastic_specification lpsspec,
const bool  formula_is_quantitative,
parse_state_formula_options  options = parse_state_formula_options() 
)
inline

Parses a state formula specification from an input stream.

Parameters
inAn input stream.
lpsspecA stochastic linear process containing data and action declarations necessary to type check the state formula.
formula_is_quantitativeIf true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula.
optionsA set of options guiding parsing.
Returns
The parse result.

Definition at line 310 of file parse.h.

◆ post_process_state_formula()

state_formula mcrl2::state_formulas::post_process_state_formula ( const state_formula formula,
parse_state_formula_options  options = parse_state_formula_options() 
)
inline

Definition at line 108 of file parse.h.

◆ pp() [1/28]

std::string mcrl2::state_formulas::pp ( const and_ x)

Definition at line 91 of file modal_formula.cpp.

◆ pp() [2/28]

std::string mcrl2::state_formulas::pp ( const const_multiply x)

Definition at line 92 of file modal_formula.cpp.

◆ pp() [3/28]

std::string mcrl2::state_formulas::pp ( const const_multiply_alt x)

Definition at line 93 of file modal_formula.cpp.

◆ pp() [4/28]

std::string mcrl2::state_formulas::pp ( const delay x)

Definition at line 94 of file modal_formula.cpp.

◆ pp() [5/28]

std::string mcrl2::state_formulas::pp ( const delay_timed x)

Definition at line 95 of file modal_formula.cpp.

◆ pp() [6/28]

std::string mcrl2::state_formulas::pp ( const exists x)

Definition at line 96 of file modal_formula.cpp.

◆ pp() [7/28]

std::string mcrl2::state_formulas::pp ( const false_ x)

Definition at line 97 of file modal_formula.cpp.

◆ pp() [8/28]

std::string mcrl2::state_formulas::pp ( const forall x)

Definition at line 98 of file modal_formula.cpp.

◆ pp() [9/28]

std::string mcrl2::state_formulas::pp ( const imp x)

Definition at line 99 of file modal_formula.cpp.

◆ pp() [10/28]

std::string mcrl2::state_formulas::pp ( const infimum x)

Definition at line 100 of file modal_formula.cpp.

◆ pp() [11/28]

std::string mcrl2::state_formulas::pp ( const may x)

Definition at line 101 of file modal_formula.cpp.

◆ pp() [12/28]

std::string mcrl2::state_formulas::pp ( const minus x)

Definition at line 102 of file modal_formula.cpp.

◆ pp() [13/28]

std::string mcrl2::state_formulas::pp ( const mu x)

Definition at line 103 of file modal_formula.cpp.

◆ pp() [14/28]

std::string mcrl2::state_formulas::pp ( const must x)

Definition at line 104 of file modal_formula.cpp.

◆ pp() [15/28]

std::string mcrl2::state_formulas::pp ( const not_ x)

Definition at line 105 of file modal_formula.cpp.

◆ pp() [16/28]

std::string mcrl2::state_formulas::pp ( const nu x)

Definition at line 106 of file modal_formula.cpp.

◆ pp() [17/28]

std::string mcrl2::state_formulas::pp ( const or_ x)

Definition at line 107 of file modal_formula.cpp.

◆ pp() [18/28]

std::string mcrl2::state_formulas::pp ( const plus x)

Definition at line 108 of file modal_formula.cpp.

◆ pp() [19/28]

std::string mcrl2::state_formulas::pp ( const state_formula x)

Definition at line 109 of file modal_formula.cpp.

◆ pp() [20/28]

std::string mcrl2::state_formulas::pp ( const state_formula_specification x)

Definition at line 110 of file modal_formula.cpp.

◆ pp() [21/28]

std::string mcrl2::state_formulas::pp ( const sum x)

Definition at line 111 of file modal_formula.cpp.

◆ pp() [22/28]

std::string mcrl2::state_formulas::pp ( const supremum x)

Definition at line 112 of file modal_formula.cpp.

◆ pp() [23/28]

template<typename T >
std::string mcrl2::state_formulas::pp ( const T &  t)

Returns a string representation of the object t.

Definition at line 676 of file print.h.

◆ pp() [24/28]

template<typename T >
void mcrl2::state_formulas::pp ( const T &  t,
std::ostream &  out 
)

Prints the object t to a stream.

Definition at line 668 of file print.h.

◆ pp() [25/28]

std::string mcrl2::state_formulas::pp ( const true_ x)

Definition at line 113 of file modal_formula.cpp.

◆ pp() [26/28]

std::string mcrl2::state_formulas::pp ( const variable x)

Definition at line 114 of file modal_formula.cpp.

◆ pp() [27/28]

std::string mcrl2::state_formulas::pp ( const yaled x)

Definition at line 115 of file modal_formula.cpp.

◆ pp() [28/28]

std::string mcrl2::state_formulas::pp ( const yaled_timed x)

Definition at line 116 of file modal_formula.cpp.

◆ precedence() [1/18]

constexpr int mcrl2::state_formulas::precedence ( const and_ )
inlineconstexpr

Definition at line 307 of file print.h.

◆ precedence() [2/18]

constexpr int mcrl2::state_formulas::precedence ( const const_multiply )
inlineconstexpr

Definition at line 309 of file print.h.

◆ precedence() [3/18]

constexpr int mcrl2::state_formulas::precedence ( const const_multiply_alt )
inlineconstexpr

Definition at line 310 of file print.h.

◆ precedence() [4/18]

constexpr int mcrl2::state_formulas::precedence ( const exists )
inlineconstexpr

Definition at line 301 of file print.h.

◆ precedence() [5/18]

constexpr int mcrl2::state_formulas::precedence ( const forall )
inlineconstexpr

Definition at line 300 of file print.h.

◆ precedence() [6/18]

constexpr int mcrl2::state_formulas::precedence ( const imp )
inlineconstexpr

Definition at line 305 of file print.h.

◆ precedence() [7/18]

constexpr int mcrl2::state_formulas::precedence ( const infimum )
inlineconstexpr

Definition at line 302 of file print.h.

◆ precedence() [8/18]

constexpr int mcrl2::state_formulas::precedence ( const may )
inlineconstexpr

Definition at line 312 of file print.h.

◆ precedence() [9/18]

constexpr int mcrl2::state_formulas::precedence ( const minus )
inlineconstexpr

Definition at line 314 of file print.h.

◆ precedence() [10/18]

constexpr int mcrl2::state_formulas::precedence ( const mu )
inlineconstexpr

Definition at line 298 of file print.h.

◆ precedence() [11/18]

constexpr int mcrl2::state_formulas::precedence ( const must )
inlineconstexpr

Definition at line 311 of file print.h.

◆ precedence() [12/18]

constexpr int mcrl2::state_formulas::precedence ( const not_ )
inlineconstexpr

Definition at line 313 of file print.h.

◆ precedence() [13/18]

constexpr int mcrl2::state_formulas::precedence ( const nu )
inlineconstexpr

Definition at line 299 of file print.h.

◆ precedence() [14/18]

constexpr int mcrl2::state_formulas::precedence ( const or_ )
inlineconstexpr

Definition at line 306 of file print.h.

◆ precedence() [15/18]

constexpr int mcrl2::state_formulas::precedence ( const plus )
inlineconstexpr

Definition at line 308 of file print.h.

◆ precedence() [16/18]

int mcrl2::state_formulas::precedence ( const state_formula x)
inline

Definition at line 315 of file print.h.

◆ precedence() [17/18]

constexpr int mcrl2::state_formulas::precedence ( const sum )
inlineconstexpr

Definition at line 304 of file print.h.

◆ precedence() [18/18]

constexpr int mcrl2::state_formulas::precedence ( const supremum )
inlineconstexpr

Definition at line 303 of file print.h.

◆ preprocess_nested_modal_operators()

state_formula mcrl2::state_formulas::preprocess_nested_modal_operators ( const state_formula x)
inline

Preprocesses a state formula that contains (nested) modal operators.

Parameters
xA modal formula

Definition at line 330 of file preprocess_state_formula.h.

◆ preprocess_state_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  quantitative = false,
bool  warn_for_modal_operator_nesting = true 
)
inline

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
formulaA modal formula.
context_idsA set of identifier strings.
preprocess_modal_operatorsA boolean indicating that dummy fixed point symbols can be inserted which makes subsequent handling easier.
warn_for_modal_operator_nestingA boolean enabling warnings for modal operator nesting.
Returns
The preprocessed formula.

Definition at line 350 of file preprocess_state_formula.h.

◆ rename_predicate_variables()

template<typename IdentifierGenerator >
state_formula mcrl2::state_formulas::rename_predicate_variables ( const state_formula f,
IdentifierGenerator &  generator 
)

Renames predicate variables of the formula f using the specified identifier generator.

Postcondition
predicate variables within the same scope have different names
Parameters
fA modal formula
generatorA generator for fresh identifiers
Returns
The rename result

Definition at line 122 of file state_formula_rename.h.

◆ rename_variables()

state_formula mcrl2::state_formulas::rename_variables ( const state_formula f,
const std::set< core::identifier_string > &  forbidden_identifiers 
)
inline

Renames all data variables in the formula f such that the forbidden identifiers are not used.

Parameters
fA modal formula.
forbidden_identifiersSet of identifiers strings, which are renamed.
Returns
The rename result.

Definition at line 193 of file state_formula_rename.h.

◆ replace_all_variables() [1/2]

template<typename T , typename Substitution >
T mcrl2::state_formulas::replace_all_variables ( const T &  x,
const Substitution &  sigma,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 392 of file replace.h.

◆ replace_all_variables() [2/2]

template<typename T , typename Substitution >
void mcrl2::state_formulas::replace_all_variables ( T &  x,
const Substitution &  sigma,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 383 of file replace.h.

◆ replace_data_expressions() [1/2]

template<typename T , typename Substitution >
T mcrl2::state_formulas::replace_data_expressions ( const T &  x,
const Substitution &  sigma,
bool  innermost,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 350 of file replace.h.

◆ replace_data_expressions() [2/2]

template<typename T , typename Substitution >
void mcrl2::state_formulas::replace_data_expressions ( T &  x,
const Substitution &  sigma,
bool  innermost,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 340 of file replace.h.

◆ replace_free_variables() [1/4]

template<typename T , typename Substitution , typename VariableContainer >
T mcrl2::state_formulas::replace_free_variables ( const T &  x,
const Substitution &  sigma,
const VariableContainer &  bound_variables,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 444 of file replace.h.

◆ replace_free_variables() [2/4]

template<typename T , typename Substitution >
T mcrl2::state_formulas::replace_free_variables ( const T &  x,
const Substitution &  sigma,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

\brief Applies the substitution sigma to x. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 417 of file replace.h.

◆ replace_free_variables() [3/4]

template<typename T , typename Substitution , typename VariableContainer >
void mcrl2::state_formulas::replace_free_variables ( T &  x,
const Substitution &  sigma,
const VariableContainer &  bound_variables,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 431 of file replace.h.

◆ replace_free_variables() [4/4]

template<typename T , typename Substitution >
void mcrl2::state_formulas::replace_free_variables ( T &  x,
const Substitution &  sigma,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

\brief Applies the substitution sigma to x. \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }

Definition at line 405 of file replace.h.

◆ replace_sort_expressions() [1/2]

template<typename T , typename Substitution >
T mcrl2::state_formulas::replace_sort_expressions ( const T &  x,
const Substitution &  sigma,
bool  innermost,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 328 of file replace.h.

◆ replace_sort_expressions() [2/2]

template<typename T , typename Substitution >
void mcrl2::state_formulas::replace_sort_expressions ( T &  x,
const Substitution &  sigma,
bool  innermost,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 318 of file replace.h.

◆ replace_state_formulas() [1/2]

template<typename T , typename Substitution >
T mcrl2::state_formulas::replace_state_formulas ( const T &  x,
Substitution  sigma,
bool  innermost = true,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 513 of file replace.h.

◆ replace_state_formulas() [2/2]

template<typename T , typename Substitution >
void mcrl2::state_formulas::replace_state_formulas ( T &  x,
Substitution  sigma,
bool  innermost = true,
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *  = 0 
)

Definition at line 503 of file replace.h.

◆ replace_variables() [1/2]

template<typename T , typename Substitution >
T mcrl2::state_formulas::replace_variables ( const T &  x,
const Substitution &  sigma,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 372 of file replace.h.

◆ replace_variables() [2/2]

template<typename T , typename Substitution >
void mcrl2::state_formulas::replace_variables ( T &  x,
const Substitution &  sigma,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 363 of file replace.h.

◆ replace_variables_capture_avoiding() [1/4]

template<typename T , typename Substitution >
T mcrl2::state_formulas::replace_variables_capture_avoiding ( const T &  x,
Substitution &  sigma,
data::set_identifier_generator id_generator,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the substiution is applied. \param sigma A substitution. \param id_generator An identifier generator that generates names that do not appear in x and sigma

Definition at line 293 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding() [2/4]

template<typename T , typename Substitution >
T mcrl2::state_formulas::replace_variables_capture_avoiding ( const T &  x,
Substitution &  sigma,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the substiution is applied. \param sigma A substitution.

Definition at line 327 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding() [3/4]

template<typename T , typename Substitution >
void mcrl2::state_formulas::replace_variables_capture_avoiding ( T &  x,
Substitution &  sigma,
data::set_identifier_generator id_generator,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the subsitution is applied. \param sigma A substitution. \param id_generator An identifier generator that generates names that do not appear in x and sigma

Definition at line 278 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding() [4/4]

template<typename T , typename Substitution >
void mcrl2::state_formulas::replace_variables_capture_avoiding ( T &  x,
Substitution &  sigma,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

\brief Applies sigma as a capture avoiding substitution to x. \param x The object to which the subsitution is applied. \param sigma A substitution.

Definition at line 309 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding_with_an_identifier_generator() [1/2]

template<typename T , typename Substitution , typename IdentifierGenerator >
T mcrl2::state_formulas::replace_variables_capture_avoiding_with_an_identifier_generator ( const T &  x,
Substitution &  sigma,
IdentifierGenerator &  id_generator,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

\brief Applies sigma as a capture avoiding substitution to x using an identifier generator.. \details This substitution function is much faster than replace_variables_capture_avoiding, but it requires an identifier generator that generates strings for fresh variables. These strings must be unique in the sense that they have not been used for other variables. \param x The object to which the substiution is applied. \param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its right hand side. The class maintain_variables_in_rhs is useful for this purpose. \param id_generator A generator that generates unique strings, not yet used as variable names. \return The result is the term x to which sigma has been applied.

Definition at line 265 of file replace_capture_avoiding_with_an_identifier_generator.h.

◆ replace_variables_capture_avoiding_with_an_identifier_generator() [2/2]

template<typename T , typename Substitution , typename IdentifierGenerator >
void mcrl2::state_formulas::replace_variables_capture_avoiding_with_an_identifier_generator ( T &  x,
Substitution &  sigma,
IdentifierGenerator &  id_generator,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

\brief Applies sigma as a capture avoiding substitution to x using an identifier generator. \details This substitution function is much faster than replace_variables_capture_avoiding, but it requires an identifier generator that generates strings for fresh variables. These strings must be unique in the sense that they have not been used for other variables. \param x The object to which the subsitution is applied. \param sigma A mutable substitution of which it can efficiently be checked whether a variable occurs in its right hand side. The class maintain_variables_in_rhs is useful for this purpose. \param id_generator A generator that generates unique strings, not yet used as variable names.

Definition at line 246 of file replace_capture_avoiding_with_an_identifier_generator.h.

◆ resolve_state_formula_data_variable_name_clashes()

state_formula mcrl2::state_formulas::resolve_state_formula_data_variable_name_clashes ( const state_formula x,
const std::set< core::identifier_string > &  context_ids = std::set<core::identifier_string>() 
)
inline

Resolves name clashes in data variables of formula x.

Definition at line 323 of file resolve_name_clashes.h.

◆ resolve_state_variable_name_clashes()

state_formula mcrl2::state_formulas::resolve_state_variable_name_clashes ( const state_formula x)
inline

Resolves name clashes in state variables of formula x.

Definition at line 314 of file resolve_name_clashes.h.

◆ rewrite() [1/4]

template<typename T , typename Rewriter , typename Substitution >
T mcrl2::state_formulas::rewrite ( const T &  x,
Rewriter  R,
const Substitution &  sigma,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

\brief Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly \param x an object containing expressions \param R a rewriter \param sigma a substitution \return the rewrite result

Definition at line 198 of file rewrite.h.

◆ rewrite() [2/4]

template<typename T , typename Rewriter >
T mcrl2::state_formulas::rewrite ( const T &  x,
Rewriter  R,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

\brief Rewrites all embedded expressions in an object x \param x an object containing expressions \param R a rewriter \return the rewrite result

Definition at line 168 of file rewrite.h.

◆ rewrite() [3/4]

template<typename T , typename Rewriter , typename Substitution >
void mcrl2::state_formulas::rewrite ( T &  x,
Rewriter  R,
const Substitution &  sigma,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

\brief Rewrites all embedded expressions in an object x, and applies a substitution to variables on the fly \param x an object containing expressions \param R a rewriter \param sigma a substitution

Definition at line 183 of file rewrite.h.

◆ rewrite() [4/4]

template<typename T , typename Rewriter >
void mcrl2::state_formulas::rewrite ( T &  x,
Rewriter  R,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

\brief Rewrites all embedded expressions in an object x \param x an object containing expressions \param R a rewriter

Definition at line 155 of file rewrite.h.

◆ swap() [1/25]

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

\brief swap overload

Definition at line 467 of file state_formula.h.

◆ swap() [2/25]

void mcrl2::state_formulas::swap ( const_multiply t1,
const_multiply t2 
)
inline

\brief swap overload

Definition at line 771 of file state_formula.h.

◆ swap() [3/25]

void mcrl2::state_formulas::swap ( const_multiply_alt t1,
const_multiply_alt t2 
)
inline

\brief swap overload

Definition at line 847 of file state_formula.h.

◆ swap() [4/25]

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

\brief swap overload

Definition at line 1556 of file state_formula.h.

◆ swap() [5/25]

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

\brief swap overload

Definition at line 1627 of file state_formula.h.

◆ swap() [6/25]

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

\brief swap overload

Definition at line 999 of file state_formula.h.

◆ swap() [7/25]

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

\brief swap overload

Definition at line 249 of file state_formula.h.

◆ swap() [8/25]

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

\brief swap overload

Definition at line 923 of file state_formula.h.

◆ swap() [9/25]

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

\brief swap overload

Definition at line 619 of file state_formula.h.

◆ swap() [10/25]

void mcrl2::state_formulas::swap ( infimum t1,
infimum t2 
)
inline

\brief swap overload

Definition at line 1075 of file state_formula.h.

◆ swap() [11/25]

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

\brief swap overload

Definition at line 1379 of file state_formula.h.

◆ swap() [12/25]

void mcrl2::state_formulas::swap ( minus t1,
minus t2 
)
inline

\brief swap overload

Definition at line 391 of file state_formula.h.

◆ swap() [13/25]

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

\brief swap overload

Definition at line 1880 of file state_formula.h.

◆ swap() [14/25]

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

\brief swap overload

Definition at line 1303 of file state_formula.h.

◆ swap() [15/25]

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

\brief swap overload

Definition at line 320 of file state_formula.h.

◆ swap() [16/25]

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

\brief swap overload

Definition at line 1794 of file state_formula.h.

◆ swap() [17/25]

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

\brief swap overload

Definition at line 543 of file state_formula.h.

◆ swap() [18/25]

void mcrl2::state_formulas::swap ( plus t1,
plus t2 
)
inline

\brief swap overload

Definition at line 695 of file state_formula.h.

◆ swap() [19/25]

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

\brief swap overload

Definition at line 143 of file state_formula.h.

◆ swap() [20/25]

void mcrl2::state_formulas::swap ( sum t1,
sum t2 
)
inline

\brief swap overload

Definition at line 1227 of file state_formula.h.

◆ swap() [21/25]

void mcrl2::state_formulas::swap ( supremum t1,
supremum t2 
)
inline

\brief swap overload

Definition at line 1151 of file state_formula.h.

◆ swap() [22/25]

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

\brief swap overload

Definition at line 196 of file state_formula.h.

◆ swap() [23/25]

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

\brief swap overload

Definition at line 1708 of file state_formula.h.

◆ swap() [24/25]

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

\brief swap overload

Definition at line 1432 of file state_formula.h.

◆ swap() [25/25]

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

\brief swap overload

Definition at line 1503 of file state_formula.h.

◆ translate_regular_formulas()

state_formula mcrl2::state_formulas::translate_regular_formulas ( const state_formula x)
inline

Translates regular formulas appearing in f into action formulas.

Parameters
xA state formula

Definition at line 41 of file translate_regular_formulas.h.

◆ translate_user_notation() [1/3]

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

Definition at line 118 of file modal_formula.cpp.

◆ translate_user_notation() [2/3]

template<typename T >
T mcrl2::state_formulas::translate_user_notation ( const T &  x,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 79 of file translate_user_notation.h.

◆ translate_user_notation() [3/3]

template<typename T >
void mcrl2::state_formulas::translate_user_notation ( T &  x,
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *  = 0 
)

Definition at line 71 of file translate_user_notation.h.

◆ typecheck_state_formula() [1/2]

template<typename VariableContainer , typename ActionLabelContainer >
state_formula mcrl2::state_formulas::typecheck_state_formula ( const state_formula x,
const bool  formula_is_quantitative,
const data::data_specification dataspec = data::data_specification(),
const ActionLabelContainer &  action_labels = ActionLabelContainer(),
const VariableContainer &  variables = VariableContainer() 
)

Type check a state formula. Throws an exception if something went wrong.

Parameters
[in]xA state formula that has not been type checked.
[in]dataspecThe data specification against which the formulas is checked.
[in]action_labelsA declaration of action labels that can be used in the state formulas.
[in]variablesA container with global data variables.
Postcondition
formula is type checked.

Definition at line 784 of file typecheck.h.

◆ typecheck_state_formula() [2/2]

state_formula mcrl2::state_formulas::typecheck_state_formula ( const state_formula x,
const lps::stochastic_specification lpsspec,
const bool  formula_is_quantitative 
)
inline

Type check a state formula. Throws an exception if something went wrong.

Parameters
[in]xA state formula that has not been type checked.
[in]lpsspecA linear process specifications containing data, action and global variable declarations to be used when typechecking the formula.
Postcondition
formula is type checked.

Definition at line 810 of file typecheck.h.

◆ typecheck_state_formula_specification() [1/2]

void mcrl2::state_formulas::typecheck_state_formula_specification ( state_formula_specification formspec,
const bool  formula_is_quantitative 
)
inline

Typecheck the state formula specification formspec. It is assumed that the formula is self contained, i.e. all actions and sorts must be declared.

Definition at line 821 of file typecheck.h.

◆ typecheck_state_formula_specification() [2/2]

void mcrl2::state_formulas::typecheck_state_formula_specification ( state_formula_specification formspec,
const lps::stochastic_specification lpsspec,
const bool  formula_is_quantitative 
)
inline

Typecheck the state formula specification formspec. It is assumed that the formula is not self contained, i.e. some of the actions and sorts may be declared in lpsspec.

Definition at line 842 of file typecheck.h.