mCRL2
|
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_formula > | state_formula_list |
\brief list of state_formulas | |
typedef std::vector< state_formula > | state_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::variable > | find_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::variable > | find_free_variables (const T &x) |
template<typename T , typename VariableContainer > | |
std::set< data::variable > | find_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_string > | find_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_expression > | find_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_symbol > | find_function_symbols (const T &x) |
std::set< core::identifier_string > | find_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::variable > | find_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::variable > | find_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_label > | find_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_formula > | maximal_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 > | |
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 > | |
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 > | |
T | 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 > | |
T | 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 > | |
T | 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 > | |
T | 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 > | |
T | 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 > | |
T | 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 > | |
T | 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 > | |
T | 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 > | |
T | 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 > | |
T | 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 > | |
T | 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 > | |
T | 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_expression > | find_sort_expressions (const state_formulas::state_formula &x) |
std::set< data::variable > | find_all_variables (const state_formulas::state_formula &x) |
std::set< data::variable > | find_free_variables (const state_formulas::state_formula &x) |
std::set< core::identifier_string > | find_identifiers (const state_formulas::state_formula &x) |
std::set< process::action_label > | find_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 > | |
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. | |
\brief list of state_formulas
Definition at line 64 of file state_formula.h.
typedef std::vector<state_formula> mcrl2::state_formulas::state_formula_vector |
\brief vector of state_formulas
Definition at line 67 of file state_formula.h.
|
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.
|
inline |
Throws an exception if the formula contains name clashes.
Definition at line 169 of file has_name_clashes.h.
|
inline |
Counts the number of fixpoints in a state formula.
x | A state formula |
Definition at line 57 of file count_fixpoints.h.
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.
std::set< process::action_label > mcrl2::state_formulas::find_action_labels | ( | const T & | x | ) |
void mcrl2::state_formulas::find_action_labels | ( | const T & | x, |
OutputIterator | o | ||
) |
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.
std::set< data::variable > mcrl2::state_formulas::find_all_variables | ( | const T & | x | ) |
void mcrl2::state_formulas::find_all_variables | ( | const T & | x, |
OutputIterator | o | ||
) |
std::set< state_formulas::variable > mcrl2::state_formulas::find_free_state_variables | ( | const T & | x | ) |
void mcrl2::state_formulas::find_free_state_variables | ( | const T & | x, |
OutputIterator | o | ||
) |
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.
std::set< data::variable > mcrl2::state_formulas::find_free_variables | ( | const T & | x | ) |
void mcrl2::state_formulas::find_free_variables | ( | const T & | x, |
OutputIterator | o | ||
) |
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
std::set< data::variable > mcrl2::state_formulas::find_free_variables_with_bound | ( | const T & | x, |
VariableContainer const & | bound | ||
) |
std::set< data::function_symbol > mcrl2::state_formulas::find_function_symbols | ( | const T & | x | ) |
void mcrl2::state_formulas::find_function_symbols | ( | const T & | x, |
OutputIterator | o | ||
) |
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.
std::set< core::identifier_string > mcrl2::state_formulas::find_identifiers | ( | const T & | x | ) |
void mcrl2::state_formulas::find_identifiers | ( | const T & | x, |
OutputIterator | o | ||
) |
bool mcrl2::state_formulas::find_nil | ( | const state_formulas::state_formula & | x | ) |
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.
std::set< data::sort_expression > mcrl2::state_formulas::find_sort_expressions | ( | const T & | x | ) |
void mcrl2::state_formulas::find_sort_expressions | ( | const T & | x, |
OutputIterator | o | ||
) |
|
inline |
std::set< state_formulas::variable > mcrl2::state_formulas::find_state_variables | ( | const T & | x | ) |
void mcrl2::state_formulas::find_state_variables | ( | const T & | x, |
OutputIterator | o | ||
) |
|
inline |
Returns true if the formula contains parameter name clashes.
Definition at line 200 of file has_name_clashes.h.
|
inline |
Returns true if the formula contains name clashes.
Definition at line 177 of file has_name_clashes.h.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
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.
|
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.
|
inline |
Returns true if the state formula is monotonous.
f | A modal formula |
Definition at line 169 of file is_monotonous.h.
|
inline |
Returns true if the state formula is monotonous.
f | A modal formula. |
non_negated_variables | Names of state variables that occur positively in the current scope. |
negated_variables | Names of state variables that occur negatively in the current scope. |
Definition at line 30 of file is_monotonous.h.
|
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.
|
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.
bool mcrl2::state_formulas::is_normalized | ( | const T & | x | ) |
Checks if a state formula is normalized.
x | A PBES expression. |
Definition at line 411 of file normalize.h.
|
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.
|
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.
|
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.
|
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.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
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.
|
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.
|
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.
|
inline |
Checks if a state formula is timed.
x | A state formula |
Definition at line 60 of file is_timed.h.
|
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.
|
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.
|
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.
|
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.
|
inline |
\brief Make_and_ constructs a new term into a given address. \
t | The reference into which the new and_ is constructed. |
Definition at line 439 of file state_formula.h.
|
inline |
\brief Make_const_multiply constructs a new term into a given address. \
t | The reference into which the new const_multiply is constructed. |
Definition at line 743 of file state_formula.h.
|
inline |
\brief Make_const_multiply_alt constructs a new term into a given address. \
t | The reference into which the new const_multiply_alt is constructed. |
Definition at line 819 of file state_formula.h.
|
inline |
\brief Make_delay_timed constructs a new term into a given address. \
t | The reference into which the new delay_timed is constructed. |
Definition at line 1599 of file state_formula.h.
|
inline |
\brief Make_exists constructs a new term into a given address. \
t | The reference into which the new exists is constructed. |
Definition at line 971 of file state_formula.h.
|
inline |
\brief Make_forall constructs a new term into a given address. \
t | The reference into which the new forall is constructed. |
Definition at line 895 of file state_formula.h.
|
inline |
\brief Make_imp constructs a new term into a given address. \
t | The reference into which the new imp is constructed. |
Definition at line 591 of file state_formula.h.
|
inline |
\brief Make_infimum constructs a new term into a given address. \
t | The reference into which the new infimum is constructed. |
Definition at line 1047 of file state_formula.h.
|
inline |
\brief Make_may constructs a new term into a given address. \
t | The reference into which the new may is constructed. |
Definition at line 1351 of file state_formula.h.
|
inline |
\brief Make_minus constructs a new term into a given address. \
t | The reference into which the new minus is constructed. |
Definition at line 363 of file state_formula.h.
|
inline |
\brief Make_mu constructs a new term into a given address. \
t | The reference into which the new mu is constructed. |
Definition at line 1852 of file state_formula.h.
|
inline |
\brief Make_must constructs a new term into a given address. \
t | The reference into which the new must is constructed. |
Definition at line 1275 of file state_formula.h.
|
inline |
\brief Make_not_ constructs a new term into a given address. \
t | The reference into which the new not_ is constructed. |
Definition at line 292 of file state_formula.h.
|
inline |
\brief Make_nu constructs a new term into a given address. \
t | The reference into which the new nu is constructed. |
Definition at line 1766 of file state_formula.h.
|
inline |
\brief Make_or_ constructs a new term into a given address. \
t | The reference into which the new or_ is constructed. |
Definition at line 515 of file state_formula.h.
|
inline |
\brief Make_plus constructs a new term into a given address. \
t | The reference into which the new plus is constructed. |
Definition at line 667 of file state_formula.h.
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.
generator | A generator for fresh identifiers |
Definition at line 111 of file state_formula_rename.h.
|
inline |
\brief Make_sum constructs a new term into a given address. \
t | The reference into which the new sum is constructed. |
Definition at line 1199 of file state_formula.h.
|
inline |
\brief Make_supremum constructs a new term into a given address. \
t | The reference into which the new supremum is constructed. |
Definition at line 1123 of file state_formula.h.
|
inline |
\brief Make_variable constructs a new term into a given address. \
t | The reference into which the new variable is constructed. |
Definition at line 1680 of file state_formula.h.
|
inline |
\brief Make_yaled_timed constructs a new term into a given address. \
t | The reference into which the new yaled_timed is constructed. |
Definition at line 1475 of file state_formula.h.
|
inline |
Definition at line 247 of file maximal_closed_subformula.h.
|
inline |
Negates variable instantiations in a state formula with a given name.
name | The name of the variables that should be negated. |
x | The state formula. |
Definition at line 69 of file negate_variables.h.
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 =>.
x | an object containing state formulas |
quantitative | Indication whether the formula is a quantitative boolean formula. |
negated | Indication whether the formula must be interpreted as being negated. |
Definition at line 436 of file normalize.h.
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 =>.
x | an object containing state formulas. |
quantitative | Indication whether the formula is a quantitative boolean formula. |
negated | Indication whether the formula must be interpreted as being negated. |
Definition at line 424 of file normalize.h.
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.
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.
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
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.
|
inline |
Parses a state formula from an input stream.
text | A string. |
lpsspec | A linear process specification used as context. The data specification of lpsspec is extended with sorts appearing in the formula. |
formula_is_quantitative | If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula. |
options | A set of options guiding parsing. |
|
inline |
Parses a state formula from an input stream.
text | A string. |
lpsspec | A stochastic linear process specification used as context. The data specification of lpsspec is extended with sorts appearing in the formula. |
formula_is_quantitative | If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula. |
options | A set of options guiding parsing. |
|
inline |
Parses a state formula from an input stream.
in | A stream. |
lpsspec | A linear process specification used as context. The data specification of lpsspec is extended with sorts appearing in the formula. |
formula_is_quantitative | If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula. |
options | A set of options guiding parsing. |
|
inline |
Parses a state formula from an input stream.
in | A stream. |
lpsspec | A stochastic linear process specification used as context. The data specification of lpsspec is extended with sorts appearing in the formula. |
formula_is_quantitative | If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula. |
options | A set of options guiding parsing. |
|
inline |
Parses a state formula specification from a string.
text | A string. |
formula_is_quantitative | If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula. |
options | A set of options guiding parsing. |
|
inline |
Parses a state formula specification from a string.
text | A string |
lpsspec | A linear process containing data and action declarations necessary to type check the state formula. |
formula_is_quantitative | If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula. |
options | A set of options guiding parsing. |
|
inline |
Parses a state formula specification from a string.
text | A string |
lpsspec | A linear process containing data and action declarations necessary to type check the state formula. |
formula_is_quantitative | If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula. |
options | A set of options guiding parsing. |
|
inline |
Parses a state formula specification from an input stream.
in | An input stream. |
formula_is_quantitative | If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula. |
options | A set of options guiding parsing. |
|
inline |
Parses a state formula specification from an input stream.
in | An input stream. |
lpsspec | A linear process containing data and action declarations necessary to type check the state formula. |
formula_is_quantitative | If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula. |
options | A set of options guiding parsing. |
|
inline |
Parses a state formula specification from an input stream.
in | An input stream. |
lpsspec | A stochastic linear process containing data and action declarations necessary to type check the state formula. |
formula_is_quantitative | If true the formula is interpreted as a quantitative modal formula, instead of a classical boolean modal formula. |
options | A set of options guiding parsing. |
|
inline |
std::string mcrl2::state_formulas::pp | ( | const and_ & | x | ) |
Definition at line 91 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const const_multiply & | x | ) |
Definition at line 92 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const const_multiply_alt & | x | ) |
Definition at line 93 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const delay & | x | ) |
Definition at line 94 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const delay_timed & | x | ) |
Definition at line 95 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const exists & | x | ) |
Definition at line 96 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const false_ & | x | ) |
Definition at line 97 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const forall & | x | ) |
Definition at line 98 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const imp & | x | ) |
Definition at line 99 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const infimum & | x | ) |
Definition at line 100 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const may & | x | ) |
Definition at line 101 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const minus & | x | ) |
Definition at line 102 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const mu & | x | ) |
Definition at line 103 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const must & | x | ) |
Definition at line 104 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const not_ & | x | ) |
Definition at line 105 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const nu & | x | ) |
Definition at line 106 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const or_ & | x | ) |
Definition at line 107 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const plus & | x | ) |
Definition at line 108 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const state_formula & | x | ) |
Definition at line 109 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const state_formula_specification & | x | ) |
Definition at line 110 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const sum & | x | ) |
Definition at line 111 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const supremum & | x | ) |
Definition at line 112 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const T & | t | ) |
void mcrl2::state_formulas::pp | ( | const T & | t, |
std::ostream & | out | ||
) |
std::string mcrl2::state_formulas::pp | ( | const true_ & | x | ) |
Definition at line 113 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const variable & | x | ) |
Definition at line 114 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const yaled & | x | ) |
Definition at line 115 of file modal_formula.cpp.
std::string mcrl2::state_formulas::pp | ( | const yaled_timed & | x | ) |
Definition at line 116 of file modal_formula.cpp.
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inline |
|
inlineconstexpr |
|
inlineconstexpr |
|
inline |
Preprocesses a state formula that contains (nested) modal operators.
x | A modal formula |
Definition at line 330 of file preprocess_state_formula.h.
|
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.
formula | A modal formula. |
context_ids | A set of identifier strings. |
preprocess_modal_operators | A boolean indicating that dummy fixed point symbols can be inserted which makes subsequent handling easier. |
warn_for_modal_operator_nesting | A boolean enabling warnings for modal operator nesting. |
Definition at line 350 of file preprocess_state_formula.h.
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.
f | A modal formula |
generator | A generator for fresh identifiers |
Definition at line 122 of file state_formula_rename.h.
|
inline |
Renames all data variables in the formula f such that the forbidden identifiers are not used.
f | A modal formula. |
forbidden_identifiers | Set of identifiers strings, which are renamed. |
Definition at line 193 of file state_formula_rename.h.
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 |
||
) |
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 |
||
) |
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 |
||
) |
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 |
||
) |
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 |
||
) |
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 |
||
) |
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 |
||
) |
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 |
||
) |
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 |
||
) |
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 |
||
) |
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 |
||
) |
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 |
||
) |
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 |
||
) |
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 |
||
) |
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.
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.
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.
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.
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.
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.
|
inline |
Resolves name clashes in data variables of formula x.
Definition at line 323 of file resolve_name_clashes.h.
|
inline |
Resolves name clashes in state variables of formula x.
Definition at line 314 of file resolve_name_clashes.h.
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 |
||
) |
T mcrl2::state_formulas::rewrite | ( | const T & | x, |
Rewriter | R, | ||
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
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 |
||
) |
void mcrl2::state_formulas::rewrite | ( | T & | x, |
Rewriter | R, | ||
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
\brief swap overload
Definition at line 467 of file state_formula.h.
|
inline |
\brief swap overload
Definition at line 771 of file state_formula.h.
|
inline |
\brief swap overload
Definition at line 847 of file state_formula.h.
\brief swap overload
Definition at line 1556 of file state_formula.h.
|
inline |
\brief swap overload
Definition at line 1627 of file state_formula.h.
\brief swap overload
Definition at line 999 of file state_formula.h.
\brief swap overload
Definition at line 249 of file state_formula.h.
\brief swap overload
Definition at line 923 of file state_formula.h.
\brief swap overload
Definition at line 619 of file state_formula.h.
\brief swap overload
Definition at line 1075 of file state_formula.h.
\brief swap overload
Definition at line 1379 of file state_formula.h.
\brief swap overload
Definition at line 391 of file state_formula.h.
\brief swap overload
Definition at line 1880 of file state_formula.h.
\brief swap overload
Definition at line 1303 of file state_formula.h.
\brief swap overload
Definition at line 320 of file state_formula.h.
\brief swap overload
Definition at line 1794 of file state_formula.h.
\brief swap overload
Definition at line 543 of file state_formula.h.
\brief swap overload
Definition at line 695 of file state_formula.h.
|
inline |
\brief swap overload
Definition at line 143 of file state_formula.h.
\brief swap overload
Definition at line 1227 of file state_formula.h.
\brief swap overload
Definition at line 1151 of file state_formula.h.
\brief swap overload
Definition at line 196 of file state_formula.h.
\brief swap overload
Definition at line 1708 of file state_formula.h.
\brief swap overload
Definition at line 1432 of file state_formula.h.
|
inline |
\brief swap overload
Definition at line 1503 of file state_formula.h.
|
inline |
Translates regular formulas appearing in f into action formulas.
x | A state formula |
Definition at line 41 of file translate_regular_formulas.h.
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.
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.
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.
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.
[in] | x | A state formula that has not been type checked. |
[in] | dataspec | The data specification against which the formulas is checked. |
[in] | action_labels | A declaration of action labels that can be used in the state formulas. |
[in] | variables | A container with global data variables. |
Definition at line 784 of file typecheck.h.
|
inline |
Type check a state formula. Throws an exception if something went wrong.
[in] | x | A state formula that has not been type checked. |
[in] | lpsspec | A linear process specifications containing data, action and global variable declarations to be used when typechecking the formula. |
Definition at line 810 of file typecheck.h.
|
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.
|
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.