mCRL2
|
The main namespace for the PRES library. More...
Namespaces | |
namespace | accessors |
The namespace for accessor functions on pres expressions. | |
namespace | algorithms |
namespace | detail |
namespace | tools |
Classes | |
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_pres_expressions |
struct | add_sort_expressions |
struct | add_traverser_data_expressions |
struct | add_traverser_identifier_strings |
struct | add_traverser_pres_expressions |
struct | add_traverser_sort_expressions |
struct | add_traverser_variables |
struct | add_variables |
class | and_ |
\brief The and operator for pres expressions More... | |
class | condeq |
\brief Conditional operator with condition smaller than or equal to 0 More... | |
class | condsm |
\brief Conditional operator with condition smaller than 0 More... | |
class | const_multiply |
\brief The multiplication with a positive constant with the constant at the left. More... | |
class | const_multiply_alt |
\brief The multiplication with a positive constant with the constant at the right. More... | |
struct | data_expression_builder |
\brief Builder class More... | |
struct | data_expression_traverser |
\brief Traverser class More... | |
struct | data_rewriter |
A rewriter that applies a data rewriter to data expressions in a term. More... | |
struct | empty_parameter_selection |
Exception that is used to signal an empty parameter selection. More... | |
struct | enumerate_quantifiers_rewriter |
An attempt for improving the efficiency. More... | |
class | eqinf |
\brief The indicator whether the argument is infinite More... | |
class | eqninf |
\brief The indicator whether the argument is -infinite More... | |
struct | identifier_string_traverser |
\brief Traverser class More... | |
class | imp |
\brief The implication operator for pres expressions More... | |
class | infimum |
\brief The infimum over a data type for pres expressions More... | |
class | lps2pres_algorithm |
Algorithm for translating a state formula and a timed stochastic specification to a pres. More... | |
class | lts2pres_algorithm |
Algorithm for translating a state formula and an untimed specification to a pres. More... | |
class | minus |
\brief The not operator for pres expressions More... | |
class | one_point_rule_rewriter |
A rewriter that applies one point rule quantifier elimination to a PRES. More... | |
class | or_ |
\brief The or operator for pres expressions More... | |
class | plus |
\brief The addition operator for pres expressions More... | |
class | pres |
parameterized boolean equation system More... | |
class | pres2res_algorithm |
A simple algorithm that takes a pres, instantiates it into a res, without parameterized variables, and sum, infimum and supremum operators. More... | |
class | pres_constelm_algorithm |
Algorithm class for the constelm algorithm. More... | |
class | pres_equation |
pres equation. More... | |
class | pres_expression |
\brief A pres expression More... | |
struct | pres_expression_builder |
\brief Builder class More... | |
struct | pres_expression_builder_base |
Builder class. More... | |
struct | pres_expression_traverser |
\brief Traverser class More... | |
struct | pres_expression_traverser_base |
Traversal class for pres_expressions. Used as a base class for pres_expression_traverser. More... | |
class | pres_parelm_algorithm |
Algorithm class for the parelm algorithm. More... | |
class | pres_type_checker |
class | presinst_algorithm |
Algorithm class for the presinst instantiation algorithm. More... | |
class | presinst_finite_algorithm |
Algorithm class for the finite presinst algorithm. More... | |
struct | presinst_finite_rename |
Function object for renaming a propositional variable instantiation. More... | |
struct | presinst_rename |
Creates a unique name for a propositional variable instantiation. The propositional variable instantiation must be closed. Originally implemented by Alexander van Dam. More... | |
struct | presinst_rename_long |
Creates a unique name for a propositional variable instantiation. The propositional variable instantiation must be closed. Originally implemented by Alexander van Dam. More... | |
struct | pressolve_options |
class | propositional_variable_instantiation |
\brief A propositional variable instantiation More... | |
class | propositional_variable_substitution |
Substitution function for propositional variables. More... | |
class | quantifiers_inside_rewriter |
A rewriter that pushes quantifiers inside in a PRES expression. More... | |
class | res_conjunctive_disjunctive_normal_form_builder |
class | ressolve_by_gauss_elimination_algorithm |
An algorithm that takes a res, i.e. a pres with propositional variables without parameters and solves it by Gauss elimination. More... | |
class | ressolve_by_numerical_iteration |
class | ressolve_by_numerical_iteration_directed |
struct | simplify_data_rewriter |
A rewriter that simplifies boolean expressions in a term, and rewrites data expressions. More... | |
struct | simplify_quantifiers_data_rewriter |
A rewriter that simplifies boolean expressions and quantifiers, and rewrites data expressions. More... | |
struct | simplify_quantifiers_rewriter |
A rewriter that simplifies boolean expressions and quantifiers. More... | |
struct | simplify_rewriter |
A rewriter that simplifies boolean expressions in a term. More... | |
struct | sort_expression_builder |
\brief Builder class More... | |
struct | sort_expression_traverser |
\brief Traverser class More... | |
struct | stream_printer |
Prints the object x to a stream. More... | |
class | substitute_pres_equation_builder |
A builder that substitutes an expression for a propositional variable instantiation in a pres expression. More... | |
class | sum |
\brief The generic sum operator for pres expressions More... | |
class | supremum |
\brief The supremeum over a data type for pres expressions More... | |
struct | untyped_pres |
struct | variable_builder |
\brief Builder class More... | |
class | variable_replace_builder |
struct | variable_traverser |
\brief Traverser class More... | |
Typedefs | |
typedef pbes_system::fixpoint_symbol | fixpoint_symbol |
typedef atermpp::term_list< pres_equation > | pres_equation_list |
\brief list of pres_equations | |
typedef std::vector< pres_equation > | pres_equation_vector |
\brief vector of pres_equations | |
typedef pbes_system::propositional_variable | propositional_variable |
The propositional variable is taken from a pbes_system. | |
typedef atermpp::term_list< pres_expression > | pres_expression_list |
\brief list of pres_expressions | |
typedef std::vector< pres_expression > | pres_expression_vector |
\brief vector of pres_expressions | |
typedef atermpp::term_list< propositional_variable_instantiation > | propositional_variable_instantiation_list |
\brief list of propositional_variable_instantiations | |
typedef std::vector< propositional_variable_instantiation > | propositional_variable_instantiation_vector |
\brief vector of propositional_variable_instantiations | |
typedef atermpp::term_list< pbes_system::propositional_variable > | propositional_variable_list |
\brief list of propositional_variables | |
typedef std::vector< pbes_system::propositional_variable > | propositional_variable_vector |
\brief vector of propositional_variables | |
typedef std::map< core::identifier_string, std::vector< std::size_t > > | presinst_index_map |
Data structure for storing the indices of the variables that should be expanded by the finite presinst algorithm. | |
typedef std::map< core::identifier_string, std::vector< data::variable > > | presinst_variable_map |
Data structure for storing the variables that should be expanded by the finite presinst algorithm. | |
Enumerations | |
enum | pres_rewriter_type { simplify , quantifier_all , quantifier_finite , quantifier_inside , quantifier_one_point } |
An enumerated type for the available pres rewriters. More... | |
enum | presinst_strategy { presinst_lazy_strategy , presinst_finite_strategy } |
presinst transformation strategies More... | |
enum | solution_algorithm { gauss_elimination , numerical , numerical_directed } |
Functions | |
void | constelm (pres &p, data::rewrite_strategy rewrite_strategy, pres_rewriter_type rewriter_type, bool compute_conditions=false, bool remove_redundant_equations=true, bool check_quantifiers=true) |
Apply the constelm algorithm. | |
std::pair< std::vector< pres_expression >, data::data_specification > | parse_pres_expressions (std::string text, const std::string &data_spec="") |
Parses a sequence of pres expressions. The format of the text is as follows: | |
pres_expression | parse_pres_expression (const std::string &text, const std::string &var_decl="datavar\npredvar\n", const std::string &data_spec="") |
Parses a single pres expression. | |
template<typename SubstitutionFunction > | |
pres_expression | parse_pres_expression (const std::string &expr, const std::string &subst, const pres &p, SubstitutionFunction &sigma) |
Parses a pres expression. | |
atermpp::aterm_ostream & | operator<< (atermpp::aterm_ostream &stream, const pres &pres) |
Writes the pres to a stream. | |
atermpp::aterm_istream & | operator>> (atermpp::aterm_istream &stream, pres &pres) |
Reads a pres from a stream. | |
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) |
template<typename Container , typename OutputIterator > | |
void | find_propositional_variable_instantiations (Container const &container, OutputIterator o) |
Returns all data variables that occur in a range of expressions. | |
template<typename Container > | |
std::set< propositional_variable_instantiation > | find_propositional_variable_instantiations (Container const &container) |
Returns all data variables that occur in a range of expressions. | |
template<typename T > | |
bool | search_variable (const T &x, const data::variable &v) |
Returns true if the term has a given variable as subterm. | |
std::map< data::variable, std::set< data::data_expression > > | find_equalities (const pres_expression &x) |
std::map< data::variable, std::set< data::data_expression > > | find_inequalities (const pres_expression &x) |
const std::vector< utilities::file_format > & | pres_file_formats () |
bool | is_pres_file_format (const utilities::file_format &format) |
const utilities::file_format & | pres_format_internal () |
const utilities::file_format & | pres_format_text () |
const utilities::file_format | guess_format (const std::string &filename) |
void | save_pres (const pres &pres, std::ostream &stream, utilities::file_format format=utilities::file_format()) |
Save a PRES in the format specified. | |
void | load_pres (pres &pres, std::istream &stream, utilities::file_format format, const std::string &source="") |
Load a PRES from file. | |
void | save_pres (const pres &pres, const std::string &filename, utilities::file_format format=utilities::file_format(), bool welltypedness_check=true) |
save_pres Saves a PRES to a file. | |
void | load_pres (pres &pres, const std::string &filename, utilities::file_format format=utilities::file_format()) |
Load pres from file. | |
bool | is_monotonous (pres_expression f) |
Returns true if the pres expression is monotonous. | |
bool | is_monotonous (const pres_equation &e) |
Returns true if the pres equation is monotonous. | |
bool | is_monotonous (const pres &p) |
Returns true if the pres is monotonous. | |
template<typename T > | |
bool | is_res (const T &x) |
Returns true if a PRES object is in BES form. | |
template<typename T > | |
bool | is_res (const T &x, std::string &error_message) |
Returns true if a PRES object is in BES form. | |
template<typename FwdIt > | |
pres_expression | join_or (FwdIt first, FwdIt last) |
Returns or applied to the sequence of pres expressions [first, last) | |
template<typename FwdIt > | |
pres_expression | join_and (FwdIt first, FwdIt last) |
Returns and applied to the sequence of pres expressions [first, last) | |
std::set< pres_expression > | split_or (const pres_expression &expr, bool split_data_expressions=false) |
Splits a disjunction into a sequence of operands Given a pres expression of the form p1 || p2 || .... || pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main function symbol. | |
std::set< pres_expression > | split_and (const pres_expression &expr, bool split_data_expressions=false) |
Splits a conjunction into a sequence of operands Given a pres expression of the form p1 && p2 && .... && pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main function symbol. | |
template<typename FwdIt > | |
pres_expression | optimized_join_or (FwdIt first, FwdIt last) |
Returns or applied to the sequence of pres expressions [first, last) | |
template<typename FwdIt > | |
pres_expression | optimized_join_and (FwdIt first, FwdIt last) |
Returns and applied to the sequence of pres expressions [first, last) | |
pres | lps2pres (const lps::stochastic_specification &lpsspec, const state_formulas::state_formula &formula, bool timed=false, bool structured=false, bool unoptimized=false, bool preprocess_modal_operators=false, bool check_only=false) |
Translates a linear stochastic process specification and a state formula to a PRES. If the solution of the PRES is true, the formula holds for the specification. | |
pres | lps2pres (const lps::stochastic_specification &lpsspec, const state_formulas::state_formula_specification &formspec, bool timed=false, bool structured=false, bool unoptimized=false, bool preprocess_modal_operators=false, bool check_only=false) |
Translates a linear process stochastic_specification and a state formula to a PRES. If the solution of the PRES is true, the formula holds for the stochastic_specification. | |
pres | lps2pres (const std::string &spec_text, const std::string &formula_text, bool timed=false, bool structured=false, bool unoptimized=false, bool preprocess_modal_operators=false, bool check_only=false) |
Applies the lps2pres algorithm. | |
pres | lts2pres (const lts::probabilistic_lts_lts_t &l, const state_formulas::state_formula_specification &formspec, bool preprocess_modal_operators=false) |
Translates an LTS and a modal formula into a PRES that represents the corresponding model checking problem. | |
template<typename T > | |
bool | is_normalized (const T &x) |
Checks if a pres expression is normalized. | |
template<typename T > | |
void | normalize (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr) |
The function normalize brings (embedded) pres expressions into positive normal form, i.e. a formula without any occurrences of ! or =>. | |
template<typename T > | |
T | normalize (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr) |
The function normalize brings (embedded) pres expressions 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 *=nullptr) |
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) |
void | parelm (pres &p) |
Apply the parelm algorithm. | |
pres | parse_pres (std::istream &in) |
std::istream & | operator>> (std::istream &from, pres &result) |
Reads a PRES from an input stream. | |
pres | parse_pres (const std::string &text) |
template<typename VariableContainer > | |
propositional_variable | parse_propositional_variable (const std::string &text, const VariableContainer &variables, const data::data_specification &dataspec=data::data_specification()) |
template<typename VariableContainer , typename PropositionalVariableContainer > | |
pres_expression | parse_pres_expression (const std::string &text, const data::data_specification &dataspec, const VariableContainer &variables, const PropositionalVariableContainer &propositional_variables, bool type_check=true, bool translate_user_notation=true, bool normalize_sorts=true) |
Parse a pres expression. Throws an exception if something went wrong. | |
template<typename VariableContainer > | |
pres_expression | parse_pres_expression (const std::string &text, const pres &presspec, const VariableContainer &variables, bool type_check=true, bool translate_user_notation=true, bool normalize_sorts=true) |
Parse a pres expression. Throws an exception if something went wrong. | |
void | complete_data_specification (pres &p) |
Adds all sorts that appear in the PRES p to the data specification of p. | |
std::string | pp (const pres &x) |
void | normalize_sorts (pres &x, const data::sort_specification &sortspec) |
void | translate_user_notation (pres_system::pres &x) |
std::set< data::sort_expression > | find_sort_expressions (const pres_system::pres &x) |
std::set< data::variable > | find_all_variables (const pres_system::pres &x) |
std::set< data::variable > | find_free_variables (const pres_system::pres &x) |
std::set< data::function_symbol > | find_function_symbols (const pres_system::pres &x) |
bool | is_well_typed_equation (const pres_equation &eqn, const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const data::data_specification &data_spec) |
bool | is_well_typed_pres (const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const std::set< data::variable > &occurring_global_variables, const std::set< propositional_variable > &declared_variables, const std::set< propositional_variable_instantiation > &occ, const propositional_variable_instantiation &init, const data::data_specification &data_spec) |
atermpp::aterm | pres_to_aterm (const pres &p) |
Conversion to atermappl. | |
std::ostream & | operator<< (std::ostream &out, const pres &x) |
bool | operator== (const pres &p1, const pres &p2) |
Equality operator on PRESs. | |
atermpp::aterm | pres_equation_to_aterm (const pres_equation &eqn) |
Conversion to atermaPpl. | |
bool | is_well_typed (const pres_equation &eqn) |
bool | has_propositional_variables (const pres_expression &x) |
std::string | pp (const pres_equation &x) |
std::ostream & | operator<< (std::ostream &out, const pres_equation &x) |
void | swap (pres_equation &t1, pres_equation &t2) |
\brief swap overload | |
bool | operator== (const pres_equation &x, const pres_equation &y) |
bool | operator!= (const pres_equation &x, const pres_equation &y) |
std::string | pp (const propositional_variable &v) |
std::string | pp (const pres_equation_vector &x) |
void | normalize_sorts (pres_equation_vector &x, const data::sort_specification &sortspec) |
std::set< data::variable > | find_free_variables (const pres_system::pres_equation &x) |
bool | is_propositional_variable_instantiation (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_infimum (const atermpp::aterm &x) |
bool | is_supremum (const atermpp::aterm &x) |
bool | is_sum (const atermpp::aterm &x) |
bool | is_eqinf (const atermpp::aterm &x) |
bool | is_eqninf (const atermpp::aterm &x) |
bool | is_condsm (const atermpp::aterm &x) |
bool | is_condeq (const atermpp::aterm &x) |
bool | is_pres_expression (const atermpp::aterm &x) |
std::string | pp (const pres_expression &x) |
std::ostream & | operator<< (std::ostream &out, const pres_expression &x) |
void | swap (pres_expression &t1, pres_expression &t2) |
\brief swap overload | |
template<class... ARGUMENTS> | |
void | make_propositional_variable_instantiation (atermpp::aterm &t, const ARGUMENTS &... args) |
std::string | pp (const propositional_variable_instantiation &x) |
std::ostream & | operator<< (std::ostream &out, const propositional_variable_instantiation &x) |
void | swap (propositional_variable_instantiation &t1, propositional_variable_instantiation &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_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_eqinf (atermpp::aterm &t, const ARGUMENTS &... args) |
std::string | pp (const eqinf &x) |
std::ostream & | operator<< (std::ostream &out, const eqinf &x) |
void | swap (eqinf &t1, eqinf &t2) |
\brief swap overload | |
template<class... ARGUMENTS> | |
void | make_eqninf (atermpp::aterm &t, const ARGUMENTS &... args) |
std::string | pp (const eqninf &x) |
std::ostream & | operator<< (std::ostream &out, const eqninf &x) |
void | swap (eqninf &t1, eqninf &t2) |
\brief swap overload | |
template<class... ARGUMENTS> | |
void | make_condsm (atermpp::aterm &t, const ARGUMENTS &... args) |
std::string | pp (const condsm &x) |
std::ostream & | operator<< (std::ostream &out, const condsm &x) |
void | swap (condsm &t1, condsm &t2) |
\brief swap overload | |
template<class... ARGUMENTS> | |
void | make_condeq (atermpp::aterm &t, const ARGUMENTS &... args) |
std::string | pp (const condeq &x) |
std::ostream & | operator<< (std::ostream &out, const condeq &x) |
void | swap (condeq &t1, condeq &t2) |
\brief swap overload | |
std::string | pp (const pres_expression_list &x) |
std::string | pp (const pres_expression_vector &x) |
std::string | pp (const propositional_variable_instantiation_list &x) |
std::string | pp (const propositional_variable_instantiation_vector &x) |
std::set< pres_system::propositional_variable_instantiation > | find_propositional_variable_instantiations (const pres_system::pres_expression &x) |
std::set< core::identifier_string > | find_identifiers (const pres_system::pres_expression &x) |
std::set< data::variable > | find_free_variables (const pres_system::pres_expression &x) |
bool | search_variable (const pres_system::pres_expression &x, const data::variable &v) |
pres_system::pres_expression | normalize_sorts (const pres_system::pres_expression &x, const data::sort_specification &sortspec) |
pres_system::pres_expression | translate_user_notation (const pres_system::pres_expression &x) |
const pres_expression & | true_ () |
const pres_expression & | false_ () |
bool | is_true (const pres_expression &t) |
Test for the value true. | |
bool | is_false (const pres_expression &t) |
Test for the value false. | |
bool | is_pres_minus (const pres_expression &t) |
Returns true if the term t is a minus expression. | |
bool | is_pres_and (const pres_expression &t) |
Returns true if the term t is an and expression. | |
bool | is_pres_or (const pres_expression &t) |
Returns true if the term t is an or expression. | |
bool | is_pres_imp (const pres_expression &t) |
Returns true if the term t is an imp expression. | |
bool | is_pres_infimum (const pres_expression &t) |
Returns true if the term t is a generalized minus expression. | |
bool | is_pres_supremum (const pres_expression &t) |
Returns true if the term t is a generalized maximum expression. | |
bool | is_universal_and (const pres_expression &t) |
Test for a conjunction. | |
bool | is_universal_or (const pres_expression &t) |
Test for a disjunction. | |
bool | is_data (const pres_expression &t) |
Returns true if the term t is a data expression. | |
pres_expression | make_infimum (const data::variable_list &l, const pres_expression &p) |
Make a generalized minimum. It checks for an empty variable list, which is not allowed. | |
pres_expression | make_supremum (const data::variable_list &l, const pres_expression &p) |
Make an generalized maximum. It checks for an empty variable list, which is not allowed. | |
void | optimized_minus (pres_expression &result, const pres_expression &p) |
Make a negation. | |
void | optimized_and (pres_expression &result, const pres_expression &p, const pres_expression &q) |
Make a conjunction. | |
void | optimized_or (pres_expression &result, const pres_expression &p, const pres_expression &q) |
Make a disjunction. | |
void | optimized_plus (pres_expression &result, const pres_expression &p, const pres_expression &q) |
Make a disjunction. | |
void | optimized_infimum (pres_expression &result, const data::variable_list &l, const pres_expression &p) |
Make an implication. | |
void | optimized_supremum (pres_expression &result, const data::variable_list &l, const pres_expression &p) |
Make a supremum. If l is empty, p is returned. | |
void | optimized_sum (pres_expression &result, const data::variable_list &l, const pres_expression &p, const data::data_specification &data_specification, const data::rewriter &rewr) |
Make an sum quantification. If l is empty, p is returned. | |
void | optimized_condsm (pres_expression &result, const pres_expression &p1, const pres_expression &p2, const pres_expression &p3) |
Make an optimized condsm expression. | |
void | optimized_condeq (pres_expression &result, const pres_expression &p1, const pres_expression &p2, const pres_expression &p3) |
Make an optimized condsm expression. | |
void | optimized_eqinf (pres_expression &result, const pres_expression &p) |
Make an optimized eqinf expression. | |
void | optimized_eqninf (pres_expression &result, const pres_expression &p) |
Make an optimized eqinf expression. | |
void | optimized_const_multiply (pres_expression &result, const data::data_expression &d, const pres_expression &p) |
Make an optimized const_multiply expression. | |
void | optimized_const_multiply_alt (pres_expression &result, const data::data_expression &d, const pres_expression &p) |
Make an optimized const_multiply_alt expression. | |
bool | is_constant (const pres_expression &x) |
data::variable_list | free_variables (const pres_expression &x) |
template<class... ARGUMENTS> | |
void | make_propositional_variable (atermpp::aterm &t, const ARGUMENTS &... args) |
pres_rewriter_type | parse_pres_rewriter_type (const std::string &type) |
Parses a pres rewriter type. | |
std::string | print_pres_rewriter_type (const pres_rewriter_type type) |
Prints a pres rewriter type. | |
std::string | description (const pres_rewriter_type type) |
Returns a description of a pres rewriter. | |
std::istream & | operator>> (std::istream &is, pres_rewriter_type &t) |
Stream operator for rewriter type. | |
std::ostream & | operator<< (std::ostream &os, const pres_rewriter_type t) |
void | make_presinst_substitution (const data::variable_list &v, const data::data_expression_list &e, data::rewriter::substitution_type &sigma) |
Creates a substitution function for the presinst rewriter. | |
bool | presinst_is_constant (const pres_expression &x) |
void | presinst_finite (pres &p, data::rewrite_strategy rewrite_strategy, const std::string &finite_parameter_selection) |
presinst_strategy | parse_presinst_strategy (const std::string &s) |
Parse a presinst transformation strategy. | |
std::istream & | operator>> (std::istream &is, presinst_strategy &s) |
std::string | print_presinst_strategy (const presinst_strategy strategy) |
Returns a string representation of a presinst transformation strategy. | |
std::ostream & | operator<< (std::ostream &os, const presinst_strategy strategy) |
std::string | description (const presinst_strategy strategy) |
Returns a string representation of a presinst transformation strategy. | |
std::ostream & | operator<< (std::ostream &out, const pressolve_options &options) |
constexpr int | precedence (const infimum &) |
constexpr int | precedence (const supremum &) |
constexpr int | precedence (const sum &) |
constexpr int | precedence (const plus &) |
constexpr int | precedence (const imp &) |
constexpr int | precedence (const or_ &) |
constexpr int | precedence (const and_ &) |
constexpr int | precedence (const minus &) |
constexpr int | precedence (const const_multiply &) |
constexpr int | precedence (const const_multiply_alt &) |
int | precedence (const pres_expression &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 pres_expression &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 pres_expression &x) |
template<typename T > | |
std::string | pp (const T &x) |
Returns a string representation of the object x. | |
std::set< propositional_variable > | reachable_variables (const pres &p) |
std::vector< propositional_variable > | remove_unreachable_variables (pres &p) |
Removes equations that are not (syntactically) reachable from the initial state of a PRES. | |
template<typename T > | |
T | remove_parameters (const T &x, const std::vector< std::size_t > &to_be_removed, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr) |
Removes parameters from propositional variable instantiations in a pres expression. | |
template<typename T > | |
void | remove_parameters (T &x, const std::vector< std::size_t > &to_be_removed, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0) |
Removes parameters from propositional variable instantiations in a pres expression. | |
template<typename T > | |
T | remove_parameters (const T &x, const std::map< core::identifier_string, std::vector< std::size_t > > &to_be_removed, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr) |
Removes parameters from propositional variable instantiations in a pres expression. | |
template<typename T > | |
void | remove_parameters (T &x, const std::map< core::identifier_string, std::vector< std::size_t > > &to_be_removed, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr) |
Removes parameters from propositional variable instantiations in a pres expression. | |
template<typename T > | |
T | remove_parameters (const T &x, const std::set< data::variable > &to_be_removed, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0) |
Removes parameters from propositional variable instantiations in a pres expression. | |
template<typename T > | |
void | remove_parameters (T &x, const std::set< data::variable > &to_be_removed, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr) |
Removes parameters from propositional variable instantiations in a pres expression. | |
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_propositional_variables (T &x, const Substitution &sigma, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr) |
Applies a propositional variable substitution. | |
template<typename T , typename Substitution > | |
T | replace_propositional_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr) |
Applies a propositional variable substitution. | |
template<typename T , typename Substitution > | |
void | replace_propositional_variables (T &result, const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr) |
Applies a propositional variable substitution. | |
template<typename T , typename Substitution > | |
void | replace_pres_expressions (T &x, const 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_pres_expressions (const T &x, const 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) |
std::string | print_algorithm (const solution_algorithm alg) |
std::string | description (const solution_algorithm a) |
solution_algorithm | parse_algorithm (const std::string &s) |
Parse an algorithm. | |
std::istream & | operator>> (std::istream &is, solution_algorithm &l) |
std::ostream & | operator<< (std::ostream &os, const solution_algorithm l) |
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) |
template<typename T , typename Rewriter > | |
void | pres_rewrite (T &x, const Rewriter &R, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr) |
Rewrites all embedded pres expressions in an object x. | |
template<typename T , typename Rewriter > | |
T | pres_rewrite (const T &x, const Rewriter &R, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0) |
Rewrites all embedded pres expressions in an object x. | |
template<typename T , typename Rewriter , typename Substitution > | |
void | pres_rewrite (T &x, const Rewriter &R, Substitution sigma, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0) |
Rewrites all embedded pres expressions in an object x, and applies a substitution to variables on the fly. | |
template<typename T , typename Rewriter , typename Substitution > | |
T | pres_rewrite (const T &x, const Rewriter &R, Substitution sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0) |
Rewrites all embedded pres expressions in an object x, and applies a substitution to variables on the fly. | |
std::set< data::variable > | significant_variables (const pres_expression &x) |
void | presrewr (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, data::rewrite_strategy rewrite_strategy, pres_rewriter_type rewriter_type) |
void | presconstelm (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, data::rewrite_strategy rewrite_strategy, pres_rewriter_type rewriter_type, bool compute_conditions, bool remove_redundant_equations, bool check_quantifiers) |
void | presinfo (const std::string &input_filename, const std::string &input_file_message, const utilities::file_format &file_format, bool opt_full) |
void | presparelm (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format) |
void | prespp (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, core::print_format_type format) |
void | txt2pres (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, bool normalize) |
void | lps2pres (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, const std::string &formula_filename, bool timed, bool unoptimized, bool preprocess_modal_operators, bool check_only) |
template<typename T > | |
void | translate_user_notation (T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr) |
template<typename T > | |
T | translate_user_notation (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0) |
pres | txt2pres (std::istream &spec_stream, bool normalize=true) |
Parses a PRES specification from an input stream. | |
pres | txt2pres (const std::string &text, bool normalize=true) |
Parses a PRES specification from a string. | |
void | typecheck_pres (pres &presspec) |
Type check a parsed mCRL2 pres specification. Throws an exception if something went wrong. | |
template<typename VariableContainer > | |
propositional_variable | typecheck_propositional_variable (const propositional_variable &x, const VariableContainer &variables, const data::data_specification &dataspec=data::data_specification()) |
Type check a parsed mCRL2 propositional variable. Throws an exception if something went wrong. | |
template<typename VariableContainer , typename PropositionalVariableContainer > | |
pres_expression | typecheck_pres_expression (pres_expression &x, const VariableContainer &variables, const PropositionalVariableContainer &propositional_variables, const data::data_specification &dataspec=data::data_specification()) |
Type check a parsed mCRL2 pres expression. Throws an exception if something went wrong. | |
static atermpp::aterm | remove_index_impl (const atermpp::aterm &x) |
static atermpp::aterm | add_index_impl (const atermpp::aterm &x) |
atermpp::aterm_ostream & | operator<< (atermpp::aterm_ostream &stream, const pres_equation &equation) |
atermpp::aterm_istream & | operator>> (atermpp::aterm_istream &stream, pres_equation &equation) |
atermpp::aterm | pres_marker () |
std::string | pp (const pres_system::propositional_variable_list &x) |
std::string | pp (const pres_system::propositional_variable_vector &x) |
std::string | pp (const pres_system::fixpoint_symbol &x) |
The main namespace for the PRES library.
Definition at line 25 of file pres_equation.h.
\brief list of pres_equations
Definition at line 134 of file pres_equation.h.
typedef std::vector<pres_equation> mcrl2::pres_system::pres_equation_vector |
\brief vector of pres_equations
Definition at line 137 of file pres_equation.h.
\brief list of pres_expressions
Definition at line 72 of file pres_expression.h.
typedef std::vector<pres_expression> mcrl2::pres_system::pres_expression_vector |
\brief vector of pres_expressions
Definition at line 75 of file pres_expression.h.
typedef std::map<core::identifier_string, std::vector<std::size_t> > mcrl2::pres_system::presinst_index_map |
Data structure for storing the indices of the variables that should be expanded by the finite presinst algorithm.
Definition at line 30 of file presinst_finite_algorithm.h.
typedef std::map<core::identifier_string, std::vector<data::variable> > mcrl2::pres_system::presinst_variable_map |
Data structure for storing the variables that should be expanded by the finite presinst algorithm.
Definition at line 33 of file presinst_finite_algorithm.h.
The propositional variable is taken from a pbes_system.
Definition at line 29 of file pres_expression.h.
typedef atermpp::term_list<propositional_variable_instantiation> mcrl2::pres_system::propositional_variable_instantiation_list |
\brief list of propositional_variable_instantiations
Definition at line 199 of file pres_expression.h.
typedef std::vector<propositional_variable_instantiation> mcrl2::pres_system::propositional_variable_instantiation_vector |
\brief vector of propositional_variable_instantiations
Definition at line 202 of file pres_expression.h.
typedef atermpp::term_list<pbes_system::propositional_variable> mcrl2::pres_system::propositional_variable_list |
\brief list of propositional_variables
Definition at line 1970 of file pres_expression.h.
typedef std::vector<pbes_system::propositional_variable> mcrl2::pres_system::propositional_variable_vector |
\brief vector of propositional_variables
Definition at line 1973 of file pres_expression.h.
An enumerated type for the available pres rewriters.
Enumerator | |
---|---|
simplify | |
quantifier_all | |
quantifier_finite | |
quantifier_inside | |
quantifier_one_point |
Definition at line 23 of file pres_rewriter_type.h.
presinst transformation strategies
Enumerator | |
---|---|
presinst_lazy_strategy | |
presinst_finite_strategy |
Definition at line 23 of file presinst_strategy.h.
Enumerator | |
---|---|
gauss_elimination | |
numerical | |
numerical_directed |
Definition at line 22 of file resalgorithm_type.h.
|
static |
|
inline |
|
inline |
Apply the constelm algorithm.
p | A PRES to which the algorithm is applied |
rewrite_strategy | A data rewrite strategy |
rewriter_type | A PRES rewriter type |
compute_conditions | If true, conditions for the edges of the dependency graph are used N.B. Very inefficient! |
remove_redundant_equations | If true, unreachable equations will be removed. |
Definition at line 1006 of file constelm.h.
|
inline |
Returns a description of a pres rewriter.
Definition at line 83 of file pres_rewriter_type.h.
|
inline |
Returns a string representation of a presinst transformation strategy.
Definition at line 87 of file presinst_strategy.h.
|
inline |
Definition at line 38 of file resalgorithm_type.h.
|
inline |
Definition at line 1315 of file pres_expression.h.
std::set< data::variable > mcrl2::pres_system::find_all_variables | ( | const pres_system::pres & | x | ) |
std::set< data::variable > mcrl2::pres_system::find_all_variables | ( | const T & | x | ) |
void mcrl2::pres_system::find_all_variables | ( | const T & | x, |
OutputIterator | o | ||
) |
|
inline |
Definition at line 130 of file find_equalities.h.
std::set< data::variable > mcrl2::pres_system::find_free_variables | ( | const pres_system::pres & | x | ) |
std::set< data::variable > mcrl2::pres_system::find_free_variables | ( | const pres_system::pres_equation & | x | ) |
std::set< data::variable > mcrl2::pres_system::find_free_variables | ( | const pres_system::pres_expression & | x | ) |
std::set< data::variable > mcrl2::pres_system::find_free_variables | ( | const T & | x | ) |
void mcrl2::pres_system::find_free_variables | ( | const T & | x, |
OutputIterator | o | ||
) |
void mcrl2::pres_system::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::pres_system::find_free_variables_with_bound | ( | const T & | x, |
VariableContainer const & | bound | ||
) |
std::set< data::function_symbol > mcrl2::pres_system::find_function_symbols | ( | const pres_system::pres & | x | ) |
std::set< data::function_symbol > mcrl2::pres_system::find_function_symbols | ( | const T & | x | ) |
void mcrl2::pres_system::find_function_symbols | ( | const T & | x, |
OutputIterator | o | ||
) |
std::set< core::identifier_string > mcrl2::pres_system::find_identifiers | ( | const pres_system::pres_expression & | x | ) |
std::set< core::identifier_string > mcrl2::pres_system::find_identifiers | ( | const T & | x | ) |
void mcrl2::pres_system::find_identifiers | ( | const T & | x, |
OutputIterator | o | ||
) |
|
inline |
Definition at line 140 of file find_equalities.h.
std::set< pres_system::propositional_variable_instantiation > mcrl2::pres_system::find_propositional_variable_instantiations | ( | const pres_system::pres_expression & | x | ) |
std::set< propositional_variable_instantiation > mcrl2::pres_system::find_propositional_variable_instantiations | ( | Container const & | container | ) |
void mcrl2::pres_system::find_propositional_variable_instantiations | ( | Container const & | container, |
OutputIterator | o | ||
) |
std::set< data::sort_expression > mcrl2::pres_system::find_sort_expressions | ( | const pres_system::pres & | x | ) |
std::set< data::sort_expression > mcrl2::pres_system::find_sort_expressions | ( | const T & | x | ) |
void mcrl2::pres_system::find_sort_expressions | ( | const T & | x, |
OutputIterator | o | ||
) |
|
inline |
Definition at line 1955 of file pres_expression.h.
|
inline |
bool mcrl2::pres_system::has_propositional_variables | ( | const pres_expression & | x | ) |
|
inline |
\brief Test for a and expression \param x A term \return True if \a x is a and expression
Definition at line 355 of file pres_expression.h.
|
inline |
\brief Test for a condeq expression \param x A term \return True if \a x is a condeq expression
Definition at line 1267 of file pres_expression.h.
|
inline |
\brief Test for a condsm expression \param x A term \return True if \a x is a condsm expression
Definition at line 1186 of file pres_expression.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 659 of file pres_expression.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 735 of file pres_expression.h.
|
inline |
Definition at line 1935 of file pres_expression.h.
|
inline |
Returns true if the term t is a data expression.
t | A PRES expression |
Definition at line 1413 of file pres_expression.h.
|
inline |
\brief Test for a eqinf expression \param x A term \return True if \a x is a eqinf expression
Definition at line 1034 of file pres_expression.h.
|
inline |
\brief Test for a eqninf expression \param x A term \return True if \a x is a eqninf expression
Definition at line 1105 of file pres_expression.h.
|
inline |
Test for the value false.
t | A PRES expression |
false
Definition at line 1333 of file pres_expression.h.
|
inline |
\brief Test for a imp expression \param x A term \return True if \a x is a imp expression
Definition at line 507 of file pres_expression.h.
|
inline |
\brief Test for a infimum expression \param x A term \return True if \a x is a infimum expression
Definition at line 811 of file pres_expression.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
\brief Test for a minus expression \param x A term \return True if \a x is a minus expression
Definition at line 279 of file pres_expression.h.
|
inline |
Returns true if the pres is monotonous.
Definition at line 184 of file is_monotonous.h.
|
inline |
Returns true if the pres equation is monotonous.
Definition at line 177 of file is_monotonous.h.
|
inline |
Returns true if the pres expression is monotonous.
f | A pres expression. |
Definition at line 27 of file is_monotonous.h.
bool mcrl2::pres_system::is_normalized | ( | const T & | x | ) |
Checks if a pres expression is normalized.
x | A PRES expression |
Definition at line 166 of file normalize.h.
|
inline |
\brief Test for a or expression \param x A term \return True if \a x is a or expression
Definition at line 431 of file pres_expression.h.
|
inline |
\brief Test for a plus expression \param x A term \return True if \a x is a plus expression
Definition at line 583 of file pres_expression.h.
|
inline |
Returns true if the term t is an and expression.
t | A PRES expression |
Definition at line 1349 of file pres_expression.h.
|
inline |
\brief Test for a pres_expression expression \param x A term \return True if \a x is a pres_expression expression
Definition at line 98 of file pres_expression.h.
|
inline |
|
inline |
Returns true if the term t is an imp expression.
t | A PRES expression |
Definition at line 1365 of file pres_expression.h.
|
inline |
Returns true if the term t is a generalized minus expression.
t | A PRES expression |
Definition at line 1373 of file pres_expression.h.
|
inline |
Returns true if the term t is a minus expression.
t | A PRES expression |
Definition at line 1341 of file pres_expression.h.
|
inline |
Returns true if the term t is an or expression.
t | A PRES expression |
Definition at line 1357 of file pres_expression.h.
|
inline |
Returns true if the term t is a generalized maximum expression.
t | A PRES expression |
Definition at line 1381 of file pres_expression.h.
|
inline |
\brief Test for a propositional_variable_instantiation expression \param x A term \return True if \a x is a propositional_variable_instantiation expression
Definition at line 208 of file pres_expression.h.
bool mcrl2::pres_system::is_res | ( | const T & | x | ) |
bool mcrl2::pres_system::is_res | ( | const T & | x, |
std::string & | error_message | ||
) |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
\brief Test for a sum expression \param x A term \return True if \a x is a sum expression
Definition at line 963 of file pres_expression.h.
|
inline |
\brief Test for a supremum expression \param x A term \return True if \a x is a supremum expression
Definition at line 887 of file pres_expression.h.
|
inline |
Test for the value true.
t | A PRES expression |
true
Definition at line 1325 of file pres_expression.h.
|
inline |
Test for a conjunction.
t | A PRES expression or a data expression |
Definition at line 1397 of file pres_expression.h.
|
inline |
Test for a disjunction.
t | A PRES expression or a data expression |
Definition at line 1405 of file pres_expression.h.
bool mcrl2::pres_system::is_well_typed | ( | const pres_equation & | eqn | ) |
bool mcrl2::pres_system::is_well_typed_equation | ( | const pres_equation & | eqn, |
const std::set< data::sort_expression > & | declared_sorts, | ||
const std::set< data::variable > & | declared_global_variables, | ||
const data::data_specification & | data_spec | ||
) |
bool mcrl2::pres_system::is_well_typed_pres | ( | const std::set< data::sort_expression > & | declared_sorts, |
const std::set< data::variable > & | declared_global_variables, | ||
const std::set< data::variable > & | occurring_global_variables, | ||
const std::set< propositional_variable > & | declared_variables, | ||
const std::set< propositional_variable_instantiation > & | occ, | ||
const propositional_variable_instantiation & | init, | ||
const data::data_specification & | data_spec | ||
) |
pres_expression mcrl2::pres_system::join_and | ( | FwdIt | first, |
FwdIt | last | ||
) |
pres_expression mcrl2::pres_system::join_or | ( | FwdIt | first, |
FwdIt | last | ||
) |
void mcrl2::pres_system::load_pres | ( | pres & | pres, |
const std::string & | filename, | ||
utilities::file_format | format = utilities::file_format() |
||
) |
Load pres from file.
pres | The pres to which the result is loaded. |
filename | The file from which to load the PRES. |
format | The format in which the PRES is stored in the file. |
The format of the file in infilename is guessed if format is not given or if it is equal to utilities::file_format().
void mcrl2::pres_system::load_pres | ( | pres & | pres, |
std::istream & | stream, | ||
utilities::file_format | format, | ||
const std::string & | source = "" |
||
) |
Load a PRES from file.
pres | The PRES to which the result is loaded. |
stream | The stream from which to load the PRES. |
format | The format that should be assumed for the file in infilename. If unspecified, or pres_file_unknown is specified, then a default format is chosen. |
source | The source from which the stream originates. Used for error messages. |
|
inline |
Translates a linear stochastic process specification and a state formula to a PRES. If the solution of the PRES is true, the formula holds for the specification.
lpsspec | A linear stochastic process specification. |
formula | A modal formula. |
timed | determines whether the timed or untimed variant of the algorithm is chosen. |
structured | use the 'structured' approach of generating equations. |
unoptimized | if true, the resulting PRES is not simplified, if false (default), the PRES is simplified. |
preprocess_modal_operators | A boolean indicating that the modal operators can be preprocessed to obtain a more compact PRES. |
Definition at line 154 of file lps2pres.h.
|
inline |
Translates a linear process stochastic_specification and a state formula to a PRES. If the solution of the PRES is true, the formula holds for the stochastic_specification.
lpsspec | A linear stochastic process specification. |
formspec | A modal formula specification. |
timed | determines whether the timed or untimed variant of the algorithm is chosen. |
structured | use the 'structured' approach of generating equations. |
unoptimized | if true, the resulting PRES is not simplified, if false (default), the PRES is simplified. |
preprocess_modal_operators | A boolean indicating that the modal operators can be preprocessed to obtain a more compact PRES. |
check_only | If check_only is true, only the formula will be checked, but no PRES is generated |
Definition at line 201 of file lps2pres.h.
void mcrl2::pres_system::lps2pres | ( | const std::string & | input_filename, |
const std::string & | output_filename, | ||
const utilities::file_format & | output_format, | ||
const std::string & | formula_filename, | ||
bool | timed, | ||
bool | unoptimized, | ||
bool | preprocess_modal_operators, | ||
bool | check_only | ||
) |
Definition at line 42 of file lps2pres.h.
|
inline |
Applies the lps2pres algorithm.
spec_text | A string. |
formula_text | A string. |
timed | Determines whether the timed or untimed version of the translation algorithm is used. |
structured | use the 'structured' approach of generating equations. |
unoptimized | if true, the resulting PRES is not simplified, if false (default), the PRES is simplified. |
preprocess_modal_operators | A boolean indicating that the modal operators can be preprocessed to obtain a more compact PRES. |
check_only | If check_only is true, only the formula will be checked, but no PRES is generated |
Definition at line 229 of file lps2pres.h.
|
inline |
Translates an LTS and a modal formula into a PRES that represents the corresponding model checking problem.
l | A labelled transition system. |
formspec | A modal formula specification. |
preprocess_modal_operators | A boolean indicating that modal operators must be preprocessed. |
Definition at line 114 of file lts2pres.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 346 of file pres_expression.h.
|
inline |
\brief Make_condeq constructs a new term into a given address. \
t | The reference into which the new condeq is constructed. |
Definition at line 1258 of file pres_expression.h.
|
inline |
\brief Make_condsm constructs a new term into a given address. \
t | The reference into which the new condsm is constructed. |
Definition at line 1177 of file pres_expression.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 650 of file pres_expression.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 726 of file pres_expression.h.
|
inline |
\brief Make_eqinf constructs a new term into a given address. \
t | The reference into which the new eqinf is constructed. |
Definition at line 1025 of file pres_expression.h.
|
inline |
\brief Make_eqninf constructs a new term into a given address. \
t | The reference into which the new eqninf is constructed. |
Definition at line 1096 of file pres_expression.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 498 of file pres_expression.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 802 of file pres_expression.h.
|
inline |
Make a generalized minimum. It checks for an empty variable list, which is not allowed.
l | A sequence of data variables |
p | A PRES expression |
infimum l.p
Definition at line 1545 of file pres_expression.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 270 of file pres_expression.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 422 of file pres_expression.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 574 of file pres_expression.h.
|
inline |
Creates a substitution function for the presinst rewriter.
v | A sequence of data variables |
e | A sequence of data expressions |
sigma | The substitution that maps the i-th element of v to the i-th element of e |
Definition at line 32 of file presinst_algorithm.h.
|
inline |
\brief Make_propositional_variable constructs a new term into a given address. \
t | The reference into which the new propositional_variable is constructed. |
Definition at line 1964 of file pres_expression.h.
|
inline |
\brief Make_propositional_variable_instantiation constructs a new term into a given address. \
t | The reference into which the new propositional_variable_instantiation is constructed. |
Definition at line 193 of file pres_expression.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 954 of file pres_expression.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 878 of file pres_expression.h.
|
inline |
Make an generalized maximum. It checks for an empty variable list, which is not allowed.
l | A sequence of data variables |
p | A PRES expression |
exists l.p
Definition at line 1560 of file pres_expression.h.
T mcrl2::pres_system::normalize | ( | const T & | x, |
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
The function normalize brings (embedded) pres expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.
x | an object containing pres expressions |
Definition at line 189 of file normalize.h.
void mcrl2::pres_system::normalize | ( | T & | x, |
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
The function normalize brings (embedded) pres expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.
x | an object containing pres expressions |
Definition at line 177 of file normalize.h.
pres_system::pres_expression mcrl2::pres_system::normalize_sorts | ( | const pres_system::pres_expression & | x, |
const data::sort_specification & | sortspec | ||
) |
T mcrl2::pres_system::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 34 of file normalize_sorts.h.
void mcrl2::pres_system::normalize_sorts | ( | pres_system::pres & | x, |
const data::sort_specification & | sortspec | ||
) |
void mcrl2::pres_system::normalize_sorts | ( | pres_system::pres_equation_vector & | x, |
const data::sort_specification & | sortspec | ||
) |
void mcrl2::pres_system::normalize_sorts | ( | T & | x, |
const data::sort_specification & | sortspec, | ||
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
Definition at line 25 of file normalize_sorts.h.
|
inline |
Definition at line 168 of file pres_equation.h.
atermpp::aterm_ostream & mcrl2::pres_system::operator<< | ( | atermpp::aterm_ostream & | stream, |
const pres & | pres | ||
) |
|
inline |
|
inline |
Definition at line 123 of file pres_rewriter_type.h.
|
inline |
Definition at line 79 of file presinst_strategy.h.
|
inline |
Definition at line 93 of file resalgorithm_type.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 368 of file pres_expression.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 1280 of file pres_expression.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 1199 of file pres_expression.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 672 of file pres_expression.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 748 of file pres_expression.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 1047 of file pres_expression.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 1118 of file pres_expression.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 520 of file pres_expression.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 824 of file pres_expression.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 292 of file pres_expression.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 444 of file pres_expression.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 596 of file pres_expression.h.
|
inline |
|
inline |
\brief Outputs the object to a stream \param out An output stream \param x Object x \return The output stream
Definition at line 147 of file pres_equation.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 128 of file pres_expression.h.
|
inline |
Definition at line 34 of file pressolve_options.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 221 of file pres_expression.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 976 of file pres_expression.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 900 of file pres_expression.h.
|
inline |
Definition at line 160 of file pres_equation.h.
atermpp::aterm_istream & mcrl2::pres_system::operator>> | ( | atermpp::aterm_istream & | stream, |
pres & | pres | ||
) |
|
inline |
|
inline |
|
inline |
Stream operator for rewriter type.
is | An input stream |
t | A rewriter type |
Definition at line 107 of file pres_rewriter_type.h.
|
inline |
Definition at line 48 of file presinst_strategy.h.
|
inline |
Definition at line 76 of file resalgorithm_type.h.
|
inline |
Make a conjunction.
p | A PRES expression |
q | A PRES expression |
p && q
Definition at line 1586 of file pres_expression.h.
|
inline |
Make an optimized condsm expression.
p1 | A pres expression |
p2 | A pres expression |
p3 | A pres expression |
Definition at line 1823 of file pres_expression.h.
|
inline |
Make an optimized condsm expression.
p1 | A pres expression |
p2 | A pres expression |
p3 | A pres expression |
Definition at line 1801 of file pres_expression.h.
|
inline |
Make an optimized const_multiply expression.
d | A real data expression, which should be positive. |
p | A pres expression |
Definition at line 1897 of file pres_expression.h.
|
inline |
Make an optimized const_multiply_alt expression.
d | A real data expression, which should be positive. |
p | A pres expression |
Definition at line 1918 of file pres_expression.h.
|
inline |
Make an optimized eqinf expression.
p | A pres expression |
Definition at line 1844 of file pres_expression.h.
|
inline |
Make an optimized eqinf expression.
p | A pres expression |
Definition at line 1870 of file pres_expression.h.
|
inline |
Make an implication.
p | A PRES expression |
q | A PRES expression |
p => q
Make an infimum quantification If l is empty, p is returned.
l | A sequence of data variables |
p | A PRES expression |
inf l.p
Definition at line 1669 of file pres_expression.h.
|
inline |
|
inline |
|
inline |
Make a negation.
p | A PRES expression |
!p
Definition at line 1573 of file pres_expression.h.
|
inline |
Make a disjunction.
p | A PRES expression |
q | A PRES expression |
p || q
Definition at line 1596 of file pres_expression.h.
|
inline |
Make a disjunction.
p | A PRES expression |
q | A PRES expression |
p || q
Definition at line 1606 of file pres_expression.h.
|
inline |
Make an sum quantification. If l is empty, p is returned.
l | A sequence of data variables. |
p | A PRES expression. |
data_specification | A data specification to determine the cardinality of sorts. |
rewr | A rewriter to determine the cardinality of sorts. |
sum l.p
Definition at line 1717 of file pres_expression.h.
|
inline |
Make a supremum. If l is empty, p is returned.
l | A sequence of data variables |
p | A PRES expression |
sup l.p
Definition at line 1692 of file pres_expression.h.
|
inline |
|
inline |
Parse an algorithm.
[in] | s | A string |
Definition at line 53 of file resalgorithm_type.h.
|
inline |
|
inline |
pres_expression mcrl2::pres_system::parse_pres_expression | ( | const std::string & | expr, |
const std::string & | subst, | ||
const pres & | p, | ||
SubstitutionFunction & | sigma | ||
) |
pres_expression mcrl2::pres_system::parse_pres_expression | ( | const std::string & | text, |
const data::data_specification & | dataspec, | ||
const VariableContainer & | variables, | ||
const PropositionalVariableContainer & | propositional_variables, | ||
bool | type_check = true , |
||
bool | translate_user_notation = true , |
||
bool | normalize_sorts = true |
||
) |
Parse a pres expression. Throws an exception if something went wrong.
[in] | text | A string containing a pres expression. |
[in] | variables | A sequence of data variables that may appear in x. |
[in] | propositional_variables | A sequence of propositional variables that may appear in x. |
[in] | dataspec | A data specification. |
[in] | type_check | If true the parsed input is also typechecked. |
pres_expression mcrl2::pres_system::parse_pres_expression | ( | const std::string & | text, |
const pres & | presspec, | ||
const VariableContainer & | variables, | ||
bool | type_check = true , |
||
bool | translate_user_notation = true , |
||
bool | normalize_sorts = true |
||
) |
Parse a pres expression. Throws an exception if something went wrong.
[in] | text | A string containing a pres expression. |
[in] | presspec | A PRES used as context. |
[in] | variables | A sequence of data variables that may appear in x. |
[in] | type_check | If true the parsed input is also typechecked. |
|
inline |
|
inline |
Parses a sequence of pres expressions. The format of the text is as follows:
"datavar"
, followed by a sequence of data variable declarations "predvar"
, followed by a sequence of predicate variable declarations "expressions"
, followed by a sequence of pres expressions separated by newlines An example of this is:
text | A string |
data_spec | A string N.B. A side effect of the data specification is that it determines whether rewrite rules for types like Pos and Nat are generated or not. |
|
inline |
Parses a pres rewriter type.
Definition at line 35 of file pres_rewriter_type.h.
|
inline |
Parse a presinst transformation strategy.
Definition at line 31 of file presinst_strategy.h.
propositional_variable mcrl2::pres_system::parse_propositional_variable | ( | const std::string & | text, |
const VariableContainer & | variables, | ||
const data::data_specification & | dataspec = data::data_specification() |
||
) |
std::string mcrl2::pres_system::pp | ( | const condeq & | x | ) |
std::string mcrl2::pres_system::pp | ( | const condsm & | x | ) |
std::string mcrl2::pres_system::pp | ( | const const_multiply & | x | ) |
std::string mcrl2::pres_system::pp | ( | const const_multiply_alt & | x | ) |
std::string mcrl2::pres_system::pp | ( | const eqinf & | x | ) |
std::string mcrl2::pres_system::pp | ( | const eqninf & | x | ) |
std::string mcrl2::pres_system::pp | ( | const plus & | x | ) |
std::string mcrl2::pres_system::pp | ( | const pres_equation & | x | ) |
std::string mcrl2::pres_system::pp | ( | const pres_equation_vector & | x | ) |
std::string mcrl2::pres_system::pp | ( | const pres_expression & | x | ) |
std::string mcrl2::pres_system::pp | ( | const pres_expression_list & | x | ) |
std::string mcrl2::pres_system::pp | ( | const pres_expression_vector & | x | ) |
std::string mcrl2::pres_system::pp | ( | const pres_system::fixpoint_symbol & | x | ) |
std::string mcrl2::pres_system::pp | ( | const pres_system::propositional_variable_list & | x | ) |
std::string mcrl2::pres_system::pp | ( | const pres_system::propositional_variable_vector & | x | ) |
std::string mcrl2::pres_system::pp | ( | const propositional_variable & | v | ) |
std::string mcrl2::pres_system::pp | ( | const propositional_variable_instantiation & | x | ) |
std::string mcrl2::pres_system::pp | ( | const propositional_variable_instantiation_list & | x | ) |
std::string mcrl2::pres_system::pp | ( | const propositional_variable_instantiation_vector & | x | ) |
std::string mcrl2::pres_system::pp | ( | const T & | x | ) |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inline |
|
inlineconstexpr |
|
inlineconstexpr |
|
inline |
Conversion to atermaPpl.
Definition at line 176 of file pres_equation.h.
const std::vector< utilities::file_format > & mcrl2::pres_system::pres_file_formats | ( | ) |
|
inline |
|
inline |
atermpp::aterm mcrl2::pres_system::pres_marker | ( | ) |
T mcrl2::pres_system::pres_rewrite | ( | const T & | x, |
const Rewriter & | R, | ||
Substitution | sigma, | ||
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type * | = 0 |
||
) |
T mcrl2::pres_system::pres_rewrite | ( | const T & | x, |
const Rewriter & | R, | ||
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type * | = 0 |
||
) |
void mcrl2::pres_system::pres_rewrite | ( | T & | x, |
const Rewriter & | R, | ||
Substitution | sigma, | ||
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type * | = 0 |
||
) |
void mcrl2::pres_system::pres_rewrite | ( | T & | x, |
const Rewriter & | R, | ||
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
atermpp::aterm mcrl2::pres_system::pres_to_aterm | ( | const pres & | p | ) |
void mcrl2::pres_system::presconstelm | ( | const std::string & | input_filename, |
const std::string & | output_filename, | ||
const utilities::file_format & | input_format, | ||
const utilities::file_format & | output_format, | ||
data::rewrite_strategy | rewrite_strategy, | ||
pres_rewriter_type | rewriter_type, | ||
bool | compute_conditions, | ||
bool | remove_redundant_equations, | ||
bool | check_quantifiers | ||
) |
Definition at line 22 of file presconstelm.h.
void mcrl2::pres_system::presinfo | ( | const std::string & | input_filename, |
const std::string & | input_file_message, | ||
const utilities::file_format & | file_format, | ||
bool | opt_full | ||
) |
Definition at line 22 of file presinfo.h.
|
inline |
Definition at line 410 of file presinst_finite_algorithm.h.
|
inline |
Definition at line 44 of file presinst_algorithm.h.
void mcrl2::pres_system::presparelm | ( | const std::string & | input_filename, |
const std::string & | output_filename, | ||
const utilities::file_format & | input_format, | ||
const utilities::file_format & | output_format | ||
) |
Definition at line 22 of file presparelm.h.
void mcrl2::pres_system::prespp | ( | const std::string & | input_filename, |
const std::string & | output_filename, | ||
const utilities::file_format & | input_format, | ||
core::print_format_type | format | ||
) |
void mcrl2::pres_system::presrewr | ( | const std::string & | input_filename, |
const std::string & | output_filename, | ||
const utilities::file_format & | input_format, | ||
const utilities::file_format & | output_format, | ||
data::rewrite_strategy | rewrite_strategy, | ||
pres_rewriter_type | rewriter_type | ||
) |
Definition at line 31 of file presrewr.h.
|
inline |
Definition at line 25 of file resalgorithm_type.h.
|
inline |
Prints a pres rewriter type.
Definition at line 62 of file pres_rewriter_type.h.
|
inline |
Returns a string representation of a presinst transformation strategy.
Definition at line 65 of file presinst_strategy.h.
|
inline |
Definition at line 38 of file remove_equations.h.
|
static |
T mcrl2::pres_system::remove_parameters | ( | const T & | x, |
const std::map< core::identifier_string, std::vector< std::size_t > > & | to_be_removed, | ||
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
Removes parameters from propositional variable instantiations in a pres expression.
x | A PRES library object that derives from atermpp::aterm |
to_be_removed | A mapping that maps propositional variable names to indices of parameters that are removed |
x
with parameters removed according to the mapping to_be_removed
Definition at line 208 of file remove_parameters.h.
T mcrl2::pres_system::remove_parameters | ( | const T & | x, |
const std::set< data::variable > & | to_be_removed, | ||
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type * | = 0 |
||
) |
Removes parameters from propositional variable instantiations in a pres expression.
x | A PRES library object that derives from atermpp::aterm |
to_be_removed | A set of parameters that are to be removed |
x
with parameters removed according to the mapping to_be_removed
Definition at line 318 of file remove_parameters.h.
T mcrl2::pres_system::remove_parameters | ( | const T & | x, |
const std::vector< std::size_t > & | to_be_removed, | ||
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
Removes parameters from propositional variable instantiations in a pres expression.
x | A PRES library object that derives from atermpp::aterm |
to_be_removed | The indices of parameters that are to be removed |
x
with parameters removed according to the mapping to_be_removed
Definition at line 107 of file remove_parameters.h.
void mcrl2::pres_system::remove_parameters | ( | T & | x, |
const std::map< core::identifier_string, std::vector< std::size_t > > & | to_be_removed, | ||
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
Removes parameters from propositional variable instantiations in a pres expression.
x | A PRES library object that does not derive from atermpp::aterm |
to_be_removed | A mapping that maps propositional variable names to a sorted vector of parameter indices that need to be removed |
x
with parameters removed according to the mapping to_be_removed
Definition at line 224 of file remove_parameters.h.
void mcrl2::pres_system::remove_parameters | ( | T & | x, |
const std::set< data::variable > & | to_be_removed, | ||
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
Removes parameters from propositional variable instantiations in a pres expression.
x | A PRES library object that does not derive from atermpp::aterm |
to_be_removed | A set of parameters that are to be removed |
x
with parameters removed according to the mapping to_be_removed
Definition at line 333 of file remove_parameters.h.
void mcrl2::pres_system::remove_parameters | ( | T & | x, |
const std::vector< std::size_t > & | to_be_removed, | ||
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type * | = 0 |
||
) |
Removes parameters from propositional variable instantiations in a pres expression.
x | A PRES library object that does not derive from atermpp::aterm |
to_be_removed | The indices of parameters that are to be removed |
x
with parameters removed according to the mapping to_be_removed
Definition at line 122 of file remove_parameters.h.
|
inline |
Removes equations that are not (syntactically) reachable from the initial state of a PRES.
Definition at line 82 of file remove_equations.h.
T mcrl2::pres_system::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::pres_system::replace_all_variables | ( | T & | x, |
const Substitution & | sigma, | ||
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
T mcrl2::pres_system::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::pres_system::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::pres_system::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::pres_system::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::pres_system::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::pres_system::replace_free_variables | ( | T & | x, |
const Substitution & | sigma, | ||
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
T mcrl2::pres_system::replace_pres_expressions | ( | const T & | x, |
const Substitution & | sigma, | ||
bool | innermost = true , |
||
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
void mcrl2::pres_system::replace_pres_expressions | ( | T & | x, |
const Substitution & | sigma, | ||
bool | innermost = true , |
||
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type * | = 0 |
||
) |
T mcrl2::pres_system::replace_propositional_variables | ( | const T & | x, |
const Substitution & | sigma, | ||
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
void mcrl2::pres_system::replace_propositional_variables | ( | T & | result, |
const T & | x, | ||
const Substitution & | sigma, | ||
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
void mcrl2::pres_system::replace_propositional_variables | ( | T & | x, |
const Substitution & | sigma, | ||
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
T mcrl2::pres_system::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::pres_system::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::pres_system::replace_variables | ( | const T & | x, |
const Substitution & | sigma, | ||
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
void mcrl2::pres_system::replace_variables | ( | T & | x, |
const Substitution & | sigma, | ||
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
T mcrl2::pres_system::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 112 of file replace_capture_avoiding.h.
T mcrl2::pres_system::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 146 of file replace_capture_avoiding.h.
void mcrl2::pres_system::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 97 of file replace_capture_avoiding.h.
void mcrl2::pres_system::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 128 of file replace_capture_avoiding.h.
T mcrl2::pres_system::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 124 of file replace_capture_avoiding_with_an_identifier_generator.h.
void mcrl2::pres_system::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 105 of file replace_capture_avoiding_with_an_identifier_generator.h.
T mcrl2::pres_system::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::pres_system::rewrite | ( | const T & | x, |
Rewriter | R, | ||
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
void mcrl2::pres_system::rewrite | ( | T & | x, |
Rewriter | R, | ||
const Substitution & | sigma, | ||
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
void mcrl2::pres_system::rewrite | ( | T & | x, |
Rewriter | R, | ||
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
void mcrl2::pres_system::save_pres | ( | const pres & | pres, |
const std::string & | filename, | ||
utilities::file_format | format = utilities::file_format() , |
||
bool | welltypedness_check = true |
||
) |
save_pres Saves a PRES to a file.
pres | The PRES to save. |
filename | The file to save the PRES in. |
format | The format in which to save the PRES. |
welltypedness_check | If set to false, skips checking whether pres is well typed before saving it to file. |
The format of the file in infilename is guessed if format is not given or if it is equal to utilities::file_format().
void mcrl2::pres_system::save_pres | ( | const pres & | pres, |
std::ostream & | stream, | ||
utilities::file_format | format = utilities::file_format() |
||
) |
Save a PRES in the format specified.
pres | The PRES to be stored |
stream | The stream to which the output is saved. |
format | Determines the format in which the result is written. If unspecified, or pres_file_unknown is specified, then a default format is chosen. |
bool mcrl2::pres_system::search_variable | ( | const pres_system::pres_expression & | x, |
const data::variable & | v | ||
) |
bool mcrl2::pres_system::search_variable | ( | const T & | x, |
const data::variable & | v | ||
) |
|
inline |
Definition at line 119 of file significant_variables.h.
|
inline |
Splits a conjunction into a sequence of operands Given a pres expression of the form p1 && p2 && .... && pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a && as main function symbol.
expr | A PRES expression |
split_data_expressions | if true, both data and pres conjunctions are split, otherwise only pres conjunctions are split. |
|
inline |
Splits a disjunction into a sequence of operands Given a pres expression of the form p1 || p2 || .... || pn, this will yield a set of the form { p1, p2, ..., pn }, assuming that pi does not have a || as main function symbol.
expr | A PRES expression |
split_data_expressions | if true, both data and pres disjunctions are split, otherwise only pres disjunctions are split. |
\brief swap overload
Definition at line 374 of file pres_expression.h.
\brief swap overload
Definition at line 1286 of file pres_expression.h.
\brief swap overload
Definition at line 1205 of file pres_expression.h.
|
inline |
\brief swap overload
Definition at line 678 of file pres_expression.h.
|
inline |
\brief swap overload
Definition at line 754 of file pres_expression.h.
\brief swap overload
Definition at line 1053 of file pres_expression.h.
\brief swap overload
Definition at line 1124 of file pres_expression.h.
\brief swap overload
Definition at line 526 of file pres_expression.h.
\brief swap overload
Definition at line 830 of file pres_expression.h.
\brief swap overload
Definition at line 298 of file pres_expression.h.
\brief swap overload
Definition at line 450 of file pres_expression.h.
\brief swap overload
Definition at line 602 of file pres_expression.h.
|
inline |
\brief swap overload
Definition at line 153 of file pres_equation.h.
|
inline |
\brief swap overload
Definition at line 134 of file pres_expression.h.
|
inline |
\brief swap overload
Definition at line 227 of file pres_expression.h.
\brief swap overload
Definition at line 982 of file pres_expression.h.
\brief swap overload
Definition at line 906 of file pres_expression.h.
pres_system::pres_expression mcrl2::pres_system::translate_user_notation | ( | const pres_system::pres_expression & | x | ) |
T mcrl2::pres_system::translate_user_notation | ( | const T & | x, |
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type * | = 0 |
||
) |
Definition at line 33 of file translate_user_notation.h.
void mcrl2::pres_system::translate_user_notation | ( | pres_system::pres & | x | ) |
void mcrl2::pres_system::translate_user_notation | ( | T & | x, |
typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type * | = nullptr |
||
) |
Definition at line 25 of file translate_user_notation.h.
|
inline |
Definition at line 1306 of file pres_expression.h.
void mcrl2::pres_system::txt2pres | ( | const std::string & | input_filename, |
const std::string & | output_filename, | ||
const utilities::file_format & | output_format, | ||
bool | normalize | ||
) |
Definition at line 21 of file txt2pres.h.
|
inline |
Parses a PRES specification from a string.
text | A string |
normalize | If true, the resulting PRES is normalized after reading. |
Definition at line 47 of file txt2pres.h.
|
inline |
Parses a PRES specification from an input stream.
spec_stream | A stream from which can be read |
normalize | If true, the resulting PRES is normalized after reading. |
Definition at line 30 of file txt2pres.h.
|
inline |
Type check a parsed mCRL2 pres specification. Throws an exception if something went wrong.
[in] | presspec | A process specification that has not been type checked. |
Definition at line 341 of file typecheck.h.
pres_expression mcrl2::pres_system::typecheck_pres_expression | ( | pres_expression & | x, |
const VariableContainer & | variables, | ||
const PropositionalVariableContainer & | propositional_variables, | ||
const data::data_specification & | dataspec = data::data_specification() |
||
) |
Type check a parsed mCRL2 pres expression. Throws an exception if something went wrong.
[in] | x | A pres expression. |
[in] | variables | A sequence of data variables that may appear in x. |
[in] | propositional_variables | A sequence of propositional variables that may appear in x. |
[in] | dataspec | A data specification. |
Definition at line 394 of file typecheck.h.
propositional_variable mcrl2::pres_system::typecheck_propositional_variable | ( | const propositional_variable & | x, |
const VariableContainer & | variables, | ||
const data::data_specification & | dataspec = data::data_specification() |
||
) |
Type check a parsed mCRL2 propositional variable. Throws an exception if something went wrong.
[in] | x | A propositional variable. |
[in] | variables | A sequence of data variables that may appear in x. |
[in] | dataspec | A data specification. |
Definition at line 362 of file typecheck.h.