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

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_equationpres_equation_list
 \brief list of pres_equations
 
typedef std::vector< pres_equationpres_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_expressionpres_expression_list
 \brief list of pres_expressions
 
typedef std::vector< pres_expressionpres_expression_vector
 \brief vector of pres_expressions
 
typedef atermpp::term_list< propositional_variable_instantiationpropositional_variable_instantiation_list
 \brief list of propositional_variable_instantiations
 
typedef std::vector< propositional_variable_instantiationpropositional_variable_instantiation_vector
 \brief vector of propositional_variable_instantiations
 
typedef atermpp::term_list< pbes_system::propositional_variablepropositional_variable_list
 \brief list of propositional_variables
 
typedef std::vector< pbes_system::propositional_variablepropositional_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_specificationparse_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_ostreamoperator<< (atermpp::aterm_ostream &stream, const pres &pres)
 Writes the pres to a stream.
 
atermpp::aterm_istreamoperator>> (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::variablefind_all_variables (const T &x)
 
template<typename T , typename OutputIterator >
void find_free_variables (const T &x, OutputIterator o)
 
template<typename T , typename OutputIterator , typename VariableContainer >
void find_free_variables_with_bound (const T &x, OutputIterator o, const VariableContainer &bound)
 
template<typename T >
std::set< data::variablefind_free_variables (const T &x)
 
template<typename T , typename VariableContainer >
std::set< data::variablefind_free_variables_with_bound (const T &x, VariableContainer const &bound)
 
template<typename T , typename OutputIterator >
void find_identifiers (const T &x, OutputIterator o)
 
template<typename T >
std::set< core::identifier_stringfind_identifiers (const T &x)
 
template<typename T , typename OutputIterator >
void find_sort_expressions (const T &x, OutputIterator o)
 
template<typename T >
std::set< data::sort_expressionfind_sort_expressions (const T &x)
 
template<typename T , typename OutputIterator >
void find_function_symbols (const T &x, OutputIterator o)
 
template<typename T >
std::set< data::function_symbolfind_function_symbols (const T &x)
 
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_instantiationfind_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_formatpres_format_internal ()
 
const utilities::file_formatpres_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_expressionsplit_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_expressionsplit_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 >
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 >
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_expressionfind_sort_expressions (const pres_system::pres &x)
 
std::set< data::variablefind_all_variables (const pres_system::pres &x)
 
std::set< data::variablefind_free_variables (const pres_system::pres &x)
 
std::set< data::function_symbolfind_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::variablefind_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_instantiationfind_propositional_variable_instantiations (const pres_system::pres_expression &x)
 
std::set< core::identifier_stringfind_identifiers (const pres_system::pres_expression &x)
 
std::set< data::variablefind_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_expressiontrue_ ()
 
const pres_expressionfalse_ ()
 
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_variablereachable_variables (const pres &p)
 
std::vector< propositional_variableremove_unreachable_variables (pres &p)
 Removes equations that are not (syntactically) reachable from the initial state of a PRES.
 
template<typename 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 >
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 >
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 >
replace_sort_expressions (const T &x, const Substitution &sigma, bool innermost, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_data_expressions (T &x, const Substitution &sigma, bool innermost, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_data_expressions (const T &x, const Substitution &sigma, bool innermost, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_all_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_all_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_free_variables (T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_free_variables (const T &x, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution , typename VariableContainer >
void replace_free_variables (T &x, const Substitution &sigma, const VariableContainer &bound_variables, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution , typename VariableContainer >
replace_free_variables (const T &x, const Substitution &sigma, const VariableContainer &bound_variables, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_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 >
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 >
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 >
replace_variables_capture_avoiding (const T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
void replace_variables_capture_avoiding (T &x, Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution >
replace_variables_capture_avoiding (const T &x, Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution , typename IdentifierGenerator >
void replace_variables_capture_avoiding_with_an_identifier_generator (T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Substitution , typename IdentifierGenerator >
replace_variables_capture_avoiding_with_an_identifier_generator (const T &x, Substitution &sigma, IdentifierGenerator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
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 >
rewrite (const T &x, Rewriter R, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Rewriter , typename Substitution >
void rewrite (T &x, Rewriter R, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T , typename Rewriter , typename Substitution >
rewrite (const T &x, Rewriter R, const Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
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 >
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 >
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::variablesignificant_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 >
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_ostreamoperator<< (atermpp::aterm_ostream &stream, const pres_equation &equation)
 
atermpp::aterm_istreamoperator>> (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)
 

Detailed Description

The main namespace for the PRES library.

Typedef Documentation

◆ fixpoint_symbol

◆ pres_equation_list

\brief list of pres_equations

Definition at line 134 of file pres_equation.h.

◆ pres_equation_vector

\brief vector of pres_equations

Definition at line 137 of file pres_equation.h.

◆ pres_expression_list

\brief list of pres_expressions

Definition at line 72 of file pres_expression.h.

◆ pres_expression_vector

\brief vector of pres_expressions

Definition at line 75 of file pres_expression.h.

◆ presinst_index_map

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.

◆ 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.

◆ propositional_variable

The propositional variable is taken from a pbes_system.

Definition at line 29 of file pres_expression.h.

◆ propositional_variable_instantiation_list

\brief list of propositional_variable_instantiations

Definition at line 199 of file pres_expression.h.

◆ propositional_variable_instantiation_vector

\brief vector of propositional_variable_instantiations

Definition at line 202 of file pres_expression.h.

◆ propositional_variable_list

\brief list of propositional_variables

Definition at line 1970 of file pres_expression.h.

◆ propositional_variable_vector

\brief vector of propositional_variables

Definition at line 1973 of file pres_expression.h.

Enumeration Type Documentation

◆ pres_rewriter_type

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_strategy

presinst transformation strategies

Enumerator
presinst_lazy_strategy 
presinst_finite_strategy 

Definition at line 23 of file presinst_strategy.h.

◆ solution_algorithm

Enumerator
gauss_elimination 
numerical 
numerical_directed 

Definition at line 22 of file resalgorithm_type.h.

Function Documentation

◆ add_index_impl()

static atermpp::aterm mcrl2::pres_system::add_index_impl ( const atermpp::aterm x)
static

Definition at line 177 of file io.cpp.

◆ complete_data_specification()

void mcrl2::pres_system::complete_data_specification ( pres p)
inline

Adds all sorts that appear in the PRES p to the data specification of p.

Parameters
pa PRES.

Definition at line 320 of file pres.h.

◆ constelm()

void mcrl2::pres_system::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 
)
inline

Apply the constelm algorithm.

Parameters
pA PRES to which the algorithm is applied
rewrite_strategyA data rewrite strategy
rewriter_typeA PRES rewriter type
compute_conditionsIf true, conditions for the edges of the dependency graph are used N.B. Very inefficient!
remove_redundant_equationsIf true, unreachable equations will be removed.

Definition at line 1006 of file constelm.h.

◆ description() [1/3]

std::string mcrl2::pres_system::description ( const pres_rewriter_type  type)
inline

Returns a description of a pres rewriter.

Definition at line 83 of file pres_rewriter_type.h.

◆ description() [2/3]

std::string mcrl2::pres_system::description ( const presinst_strategy  strategy)
inline

Returns a string representation of a presinst transformation strategy.

Definition at line 87 of file presinst_strategy.h.

◆ description() [3/3]

std::string mcrl2::pres_system::description ( const solution_algorithm  a)
inline

Definition at line 38 of file resalgorithm_type.h.

◆ false_()

const pres_expression & mcrl2::pres_system::false_ ( )
inline
Returns
Returns the value false

Definition at line 1315 of file pres_expression.h.

◆ find_all_variables() [1/3]

std::set< data::variable > mcrl2::pres_system::find_all_variables ( const pres_system::pres x)

Definition at line 56 of file pres.cpp.

◆ find_all_variables() [2/3]

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

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

Definition at line 75 of file find.h.

◆ find_all_variables() [3/3]

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

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

Definition at line 66 of file find.h.

◆ find_equalities()

std::map< data::variable, std::set< data::data_expression > > mcrl2::pres_system::find_equalities ( const pres_expression x)
inline

Definition at line 130 of file find_equalities.h.

◆ find_free_variables() [1/5]

std::set< data::variable > mcrl2::pres_system::find_free_variables ( const pres_system::pres x)

Definition at line 57 of file pres.cpp.

◆ find_free_variables() [2/5]

std::set< data::variable > mcrl2::pres_system::find_free_variables ( const pres_system::pres_equation x)

Definition at line 59 of file pres.cpp.

◆ find_free_variables() [3/5]

std::set< data::variable > mcrl2::pres_system::find_free_variables ( const pres_system::pres_expression x)

Definition at line 58 of file pres.cpp.

◆ find_free_variables() [4/5]

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

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

Definition at line 107 of file find.h.

◆ find_free_variables() [5/5]

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

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

Definition at line 87 of file find.h.

◆ find_free_variables_with_bound() [1/2]

template<typename T , typename OutputIterator , typename VariableContainer >
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

Definition at line 98 of file find.h.

◆ find_free_variables_with_bound() [2/2]

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

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

Definition at line 119 of file find.h.

◆ find_function_symbols() [1/3]

std::set< data::function_symbol > mcrl2::pres_system::find_function_symbols ( const pres_system::pres x)

Definition at line 60 of file pres.cpp.

◆ find_function_symbols() [2/3]

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

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

Definition at line 182 of file find.h.

◆ find_function_symbols() [3/3]

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

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

Definition at line 173 of file find.h.

◆ find_identifiers() [1/3]

std::set< core::identifier_string > mcrl2::pres_system::find_identifiers ( const pres_system::pres_expression x)

Definition at line 62 of file pres.cpp.

◆ find_identifiers() [2/3]

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

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

Definition at line 140 of file find.h.

◆ find_identifiers() [3/3]

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

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

Definition at line 131 of file find.h.

◆ find_inequalities()

std::map< data::variable, std::set< data::data_expression > > mcrl2::pres_system::find_inequalities ( const pres_expression x)
inline

Definition at line 140 of file find_equalities.h.

◆ find_propositional_variable_instantiations() [1/3]

std::set< pres_system::propositional_variable_instantiation > mcrl2::pres_system::find_propositional_variable_instantiations ( const pres_system::pres_expression x)

Definition at line 61 of file pres.cpp.

◆ find_propositional_variable_instantiations() [2/3]

template<typename Container >
std::set< propositional_variable_instantiation > mcrl2::pres_system::find_propositional_variable_instantiations ( Container const &  container)

Returns all data variables that occur in a range of expressions.

Parameters
[in]containera container with expressions
Returns
All data variables that occur in the term t

Definition at line 205 of file find.h.

◆ find_propositional_variable_instantiations() [3/3]

template<typename Container , typename OutputIterator >
void mcrl2::pres_system::find_propositional_variable_instantiations ( Container const &  container,
OutputIterator  o 
)

Returns all data variables that occur in a range of expressions.

Parameters
[in]containera container with expressions
[in,out]oan output iterator to which all data variables occurring in t are added.
Returns
All data variables that occur in the term t

Definition at line 196 of file find.h.

◆ find_sort_expressions() [1/3]

std::set< data::sort_expression > mcrl2::pres_system::find_sort_expressions ( const pres_system::pres x)

Definition at line 55 of file pres.cpp.

◆ find_sort_expressions() [2/3]

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

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

Definition at line 161 of file find.h.

◆ find_sort_expressions() [3/3]

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

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

Definition at line 152 of file find.h.

◆ free_variables()

data::variable_list mcrl2::pres_system::free_variables ( const pres_expression x)
inline

Definition at line 1955 of file pres_expression.h.

◆ guess_format()

const utilities::file_format mcrl2::pres_system::guess_format ( const std::string &  filename)
inline

Definition at line 45 of file io.h.

◆ has_propositional_variables()

bool mcrl2::pres_system::has_propositional_variables ( const pres_expression x)

◆ is_and()

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

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

Definition at line 355 of file pres_expression.h.

◆ is_condeq()

bool mcrl2::pres_system::is_condeq ( const atermpp::aterm x)
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.

◆ is_condsm()

bool mcrl2::pres_system::is_condsm ( const atermpp::aterm x)
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.

◆ is_const_multiply()

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

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

Definition at line 659 of file pres_expression.h.

◆ is_const_multiply_alt()

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

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

Definition at line 735 of file pres_expression.h.

◆ is_constant()

bool mcrl2::pres_system::is_constant ( const pres_expression x)
inline

Definition at line 1935 of file pres_expression.h.

◆ is_data()

bool mcrl2::pres_system::is_data ( const pres_expression t)
inline

Returns true if the term t is a data expression.

Parameters
tA PRES expression
Returns
True if the term t is a data expression

Definition at line 1413 of file pres_expression.h.

◆ is_eqinf()

bool mcrl2::pres_system::is_eqinf ( const atermpp::aterm x)
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.

◆ is_eqninf()

bool mcrl2::pres_system::is_eqninf ( const atermpp::aterm x)
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.

◆ is_false()

bool mcrl2::pres_system::is_false ( const pres_expression t)
inline

Test for the value false.

Parameters
tA PRES expression
Returns
True if it is the value false

Definition at line 1333 of file pres_expression.h.

◆ is_imp()

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

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

Definition at line 507 of file pres_expression.h.

◆ is_infimum()

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

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

Definition at line 811 of file pres_expression.h.

◆ is_left_associative() [1/7]

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

Definition at line 50 of file print.h.

◆ is_left_associative() [2/7]

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

Definition at line 52 of file print.h.

◆ is_left_associative() [3/7]

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

Definition at line 53 of file print.h.

◆ is_left_associative() [4/7]

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

Definition at line 48 of file print.h.

◆ is_left_associative() [5/7]

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

Definition at line 49 of file print.h.

◆ is_left_associative() [6/7]

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

Definition at line 51 of file print.h.

◆ is_left_associative() [7/7]

bool mcrl2::pres_system::is_left_associative ( const pres_expression x)
inline

Definition at line 54 of file print.h.

◆ is_minus()

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

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

Definition at line 279 of file pres_expression.h.

◆ is_monotonous() [1/3]

bool mcrl2::pres_system::is_monotonous ( const pres p)
inline

Returns true if the pres is monotonous.

Definition at line 184 of file is_monotonous.h.

◆ is_monotonous() [2/3]

bool mcrl2::pres_system::is_monotonous ( const pres_equation e)
inline

Returns true if the pres equation is monotonous.

Definition at line 177 of file is_monotonous.h.

◆ is_monotonous() [3/3]

bool mcrl2::pres_system::is_monotonous ( pres_expression  f)
inline

Returns true if the pres expression is monotonous.

Parameters
fA pres expression.
Returns
True if the pres expression is monotonous.

Definition at line 27 of file is_monotonous.h.

◆ is_normalized()

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

Checks if a pres expression is normalized.

Parameters
xA PRES expression
Returns
True if the pres expression is normalized

Definition at line 166 of file normalize.h.

◆ is_or()

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

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

Definition at line 431 of file pres_expression.h.

◆ is_plus()

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

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

Definition at line 583 of file pres_expression.h.

◆ is_pres_and()

bool mcrl2::pres_system::is_pres_and ( const pres_expression t)
inline

Returns true if the term t is an and expression.

Parameters
tA PRES expression
Returns
True if the term t is an and expression

Definition at line 1349 of file pres_expression.h.

◆ is_pres_expression()

bool mcrl2::pres_system::is_pres_expression ( const atermpp::aterm x)
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.

◆ is_pres_file_format()

bool mcrl2::pres_system::is_pres_file_format ( const utilities::file_format format)
inline

Definition at line 27 of file io.h.

◆ is_pres_imp()

bool mcrl2::pres_system::is_pres_imp ( const pres_expression t)
inline

Returns true if the term t is an imp expression.

Parameters
tA PRES expression
Returns
True if the term t is an imp expression

Definition at line 1365 of file pres_expression.h.

◆ is_pres_infimum()

bool mcrl2::pres_system::is_pres_infimum ( const pres_expression t)
inline

Returns true if the term t is a generalized minus expression.

Parameters
tA PRES expression
Returns
True if the term t is a generalized minus expression

Definition at line 1373 of file pres_expression.h.

◆ is_pres_minus()

bool mcrl2::pres_system::is_pres_minus ( const pres_expression t)
inline

Returns true if the term t is a minus expression.

Parameters
tA PRES expression
Returns
True if the term t is a minus expression

Definition at line 1341 of file pres_expression.h.

◆ is_pres_or()

bool mcrl2::pres_system::is_pres_or ( const pres_expression t)
inline

Returns true if the term t is an or expression.

Parameters
tA PRES expression
Returns
True if the term t is an or expression

Definition at line 1357 of file pres_expression.h.

◆ is_pres_supremum()

bool mcrl2::pres_system::is_pres_supremum ( const pres_expression t)
inline

Returns true if the term t is a generalized maximum expression.

Parameters
tA PRES expression
Returns
True if the term t is a generalized maximum expression

Definition at line 1381 of file pres_expression.h.

◆ is_propositional_variable_instantiation()

bool mcrl2::pres_system::is_propositional_variable_instantiation ( const atermpp::aterm x)
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.

◆ is_res() [1/2]

template<typename T >
bool mcrl2::pres_system::is_res ( const T &  x)

Returns true if a PRES object is in BES form.

Parameters
xa PRES object

Definition at line 84 of file is_res.h.

◆ is_res() [2/2]

template<typename T >
bool mcrl2::pres_system::is_res ( const T &  x,
std::string &  error_message 
)

Returns true if a PRES object is in BES form.

Parameters
xa PRES object

Definition at line 94 of file is_res.h.

◆ is_right_associative() [1/7]

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

Definition at line 67 of file print.h.

◆ is_right_associative() [2/7]

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

Definition at line 69 of file print.h.

◆ is_right_associative() [3/7]

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

Definition at line 70 of file print.h.

◆ is_right_associative() [4/7]

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

Definition at line 65 of file print.h.

◆ is_right_associative() [5/7]

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

Definition at line 66 of file print.h.

◆ is_right_associative() [6/7]

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

Definition at line 68 of file print.h.

◆ is_right_associative() [7/7]

bool mcrl2::pres_system::is_right_associative ( const pres_expression x)
inline

Definition at line 71 of file print.h.

◆ is_sum()

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

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

Definition at line 963 of file pres_expression.h.

◆ is_supremum()

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

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

Definition at line 887 of file pres_expression.h.

◆ is_true()

bool mcrl2::pres_system::is_true ( const pres_expression t)
inline

Test for the value true.

Parameters
tA PRES expression
Returns
True if it is the value true

Definition at line 1325 of file pres_expression.h.

◆ is_universal_and()

bool mcrl2::pres_system::is_universal_and ( const pres_expression t)
inline

Test for a conjunction.

Parameters
tA PRES expression or a data expression
Returns
True if it is a conjunction

Definition at line 1397 of file pres_expression.h.

◆ is_universal_or()

bool mcrl2::pres_system::is_universal_or ( const pres_expression t)
inline

Test for a disjunction.

Parameters
tA PRES expression or a data expression
Returns
True if it is a disjunction

Definition at line 1405 of file pres_expression.h.

◆ is_well_typed()

bool mcrl2::pres_system::is_well_typed ( const pres_equation eqn)

Definition at line 80 of file pres.cpp.

◆ is_well_typed_equation()

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 
)

Definition at line 85 of file pres.cpp.

◆ is_well_typed_pres()

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 
)

Definition at line 94 of file pres.cpp.

◆ join_and()

template<typename FwdIt >
pres_expression mcrl2::pres_system::join_and ( FwdIt  first,
FwdIt  last 
)

Returns and applied to the sequence of pres expressions [first, last)

Parameters
firstStart of a sequence of pres expressions
lastEnd of a sequence of of pres expressions
Returns
And applied to the sequence of pres expressions [first, last)

Definition at line 36 of file join.h.

◆ join_or()

template<typename FwdIt >
pres_expression mcrl2::pres_system::join_or ( FwdIt  first,
FwdIt  last 
)

Returns or applied to the sequence of pres expressions [first, last)

Parameters
firstStart of a sequence of pres expressions
lastEnd of a sequence of of pres expressions
Returns
Or applied to the sequence of pres expressions [first, last)

Definition at line 26 of file join.h.

◆ load_pres() [1/2]

void mcrl2::pres_system::load_pres ( pres pres,
const std::string &  filename,
utilities::file_format  format = utilities::file_format() 
)

Load pres from file.

Parameters
presThe pres to which the result is loaded.
filenameThe file from which to load the PRES.
formatThe 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().

Definition at line 139 of file io.cpp.

◆ load_pres() [2/2]

void mcrl2::pres_system::load_pres ( pres pres,
std::istream &  stream,
utilities::file_format  format,
const std::string &  source = "" 
)

Load a PRES from file.

Parameters
presThe PRES to which the result is loaded.
streamThe stream from which to load the PRES.
formatThe format that should be assumed for the file in infilename. If unspecified, or pres_file_unknown is specified, then a default format is chosen.
sourceThe source from which the stream originates. Used for error messages.

Definition at line 73 of file io.cpp.

◆ lps2pres() [1/4]

pres mcrl2::pres_system::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 
)
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.

Parameters
lpsspecA linear stochastic process specification.
formulaA modal formula.
timeddetermines whether the timed or untimed variant of the algorithm is chosen.
structureduse the 'structured' approach of generating equations.
unoptimizedif true, the resulting PRES is not simplified, if false (default), the PRES is simplified.
preprocess_modal_operatorsA boolean indicating that the modal operators can be preprocessed to obtain a more compact PRES.
Returns
The resulting pres.

Definition at line 154 of file lps2pres.h.

◆ lps2pres() [2/4]

pres mcrl2::pres_system::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 
)
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.

Parameters
lpsspecA linear stochastic process specification.
formspecA modal formula specification.
timeddetermines whether the timed or untimed variant of the algorithm is chosen.
structureduse the 'structured' approach of generating equations.
unoptimizedif true, the resulting PRES is not simplified, if false (default), the PRES is simplified.
preprocess_modal_operatorsA boolean indicating that the modal operators can be preprocessed to obtain a more compact PRES.
check_onlyIf check_only is true, only the formula will be checked, but no PRES is generated
Returns
The resulting pres.

Definition at line 201 of file lps2pres.h.

◆ lps2pres() [3/4]

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.

◆ lps2pres() [4/4]

pres mcrl2::pres_system::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 
)
inline

Applies the lps2pres algorithm.

Parameters
spec_textA string.
formula_textA string.
timedDetermines whether the timed or untimed version of the translation algorithm is used.
structureduse the 'structured' approach of generating equations.
unoptimizedif true, the resulting PRES is not simplified, if false (default), the PRES is simplified.
preprocess_modal_operatorsA boolean indicating that the modal operators can be preprocessed to obtain a more compact PRES.
check_onlyIf check_only is true, only the formula will be checked, but no PRES is generated
Returns
The result of the algorithm

Definition at line 229 of file lps2pres.h.

◆ lts2pres()

pres mcrl2::pres_system::lts2pres ( const lts::probabilistic_lts_lts_t l,
const state_formulas::state_formula_specification formspec,
bool  preprocess_modal_operators = false 
)
inline

Translates an LTS and a modal formula into a PRES that represents the corresponding model checking problem.

Parameters
lA labelled transition system.
formspecA modal formula specification.
preprocess_modal_operatorsA boolean indicating that modal operators must be preprocessed.

Definition at line 114 of file lts2pres.h.

◆ make_and_()

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

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

Parameters
tThe reference into which the new and_ is constructed.

Definition at line 346 of file pres_expression.h.

◆ make_condeq()

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

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

Parameters
tThe reference into which the new condeq is constructed.

Definition at line 1258 of file pres_expression.h.

◆ make_condsm()

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

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

Parameters
tThe reference into which the new condsm is constructed.

Definition at line 1177 of file pres_expression.h.

◆ make_const_multiply()

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

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

Parameters
tThe reference into which the new const_multiply is constructed.

Definition at line 650 of file pres_expression.h.

◆ make_const_multiply_alt()

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

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

Parameters
tThe reference into which the new const_multiply_alt is constructed.

Definition at line 726 of file pres_expression.h.

◆ make_eqinf()

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

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

Parameters
tThe reference into which the new eqinf is constructed.

Definition at line 1025 of file pres_expression.h.

◆ make_eqninf()

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

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

Parameters
tThe reference into which the new eqninf is constructed.

Definition at line 1096 of file pres_expression.h.

◆ make_imp()

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

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

Parameters
tThe reference into which the new imp is constructed.

Definition at line 498 of file pres_expression.h.

◆ make_infimum() [1/2]

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

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

Parameters
tThe reference into which the new infimum is constructed.

Definition at line 802 of file pres_expression.h.

◆ make_infimum() [2/2]

pres_expression mcrl2::pres_system::make_infimum ( const data::variable_list l,
const pres_expression p 
)
inline

Make a generalized minimum. It checks for an empty variable list, which is not allowed.

Parameters
lA sequence of data variables
pA PRES expression
Returns
The value infimum l.p

Definition at line 1545 of file pres_expression.h.

◆ make_minus()

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

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

Parameters
tThe reference into which the new minus is constructed.

Definition at line 270 of file pres_expression.h.

◆ make_or_()

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

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

Parameters
tThe reference into which the new or_ is constructed.

Definition at line 422 of file pres_expression.h.

◆ make_plus()

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

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

Parameters
tThe reference into which the new plus is constructed.

Definition at line 574 of file pres_expression.h.

◆ make_presinst_substitution()

void mcrl2::pres_system::make_presinst_substitution ( const data::variable_list v,
const data::data_expression_list e,
data::rewriter::substitution_type sigma 
)
inline

Creates a substitution function for the presinst rewriter.

Parameters
vA sequence of data variables
eA sequence of data expressions
sigmaThe 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.

◆ make_propositional_variable()

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

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

Parameters
tThe reference into which the new propositional_variable is constructed.

Definition at line 1964 of file pres_expression.h.

◆ make_propositional_variable_instantiation()

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

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

Parameters
tThe reference into which the new propositional_variable_instantiation is constructed.

Definition at line 193 of file pres_expression.h.

◆ make_sum()

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

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

Parameters
tThe reference into which the new sum is constructed.

Definition at line 954 of file pres_expression.h.

◆ make_supremum() [1/2]

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

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

Parameters
tThe reference into which the new supremum is constructed.

Definition at line 878 of file pres_expression.h.

◆ make_supremum() [2/2]

pres_expression mcrl2::pres_system::make_supremum ( const data::variable_list l,
const pres_expression p 
)
inline

Make an generalized maximum. It checks for an empty variable list, which is not allowed.

Parameters
lA sequence of data variables
pA PRES expression
Returns
The value exists l.p

Definition at line 1560 of file pres_expression.h.

◆ normalize() [1/2]

template<typename T >
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 =>.

Parameters
xan object containing pres expressions

Definition at line 189 of file normalize.h.

◆ normalize() [2/2]

template<typename T >
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 =>.

Parameters
xan object containing pres expressions

Definition at line 177 of file normalize.h.

◆ normalize_sorts() [1/5]

pres_system::pres_expression mcrl2::pres_system::normalize_sorts ( const pres_system::pres_expression x,
const data::sort_specification sortspec 
)

Definition at line 52 of file pres.cpp.

◆ normalize_sorts() [2/5]

template<typename T >
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.

◆ normalize_sorts() [3/5]

void mcrl2::pres_system::normalize_sorts ( pres_system::pres x,
const data::sort_specification sortspec 
)

Definition at line 51 of file pres.cpp.

◆ normalize_sorts() [4/5]

void mcrl2::pres_system::normalize_sorts ( pres_system::pres_equation_vector x,
const data::sort_specification sortspec 
)

Definition at line 50 of file pres.cpp.

◆ normalize_sorts() [5/5]

template<typename T >
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.

◆ operator!=()

bool mcrl2::pres_system::operator!= ( const pres_equation x,
const pres_equation y 
)
inline

Definition at line 168 of file pres_equation.h.

◆ operator<<() [1/24]

atermpp::aterm_ostream & mcrl2::pres_system::operator<< ( atermpp::aterm_ostream stream,
const pres pres 
)

Writes the pres to a stream.

Definition at line 225 of file io.cpp.

◆ operator<<() [2/24]

atermpp::aterm_ostream & mcrl2::pres_system::operator<< ( atermpp::aterm_ostream stream,
const pres_equation equation 
)
inline

Definition at line 197 of file io.cpp.

◆ operator<<() [3/24]

std::ostream & mcrl2::pres_system::operator<< ( std::ostream &  os,
const pres_rewriter_type  t 
)
inline

Definition at line 123 of file pres_rewriter_type.h.

◆ operator<<() [4/24]

std::ostream & mcrl2::pres_system::operator<< ( std::ostream &  os,
const presinst_strategy  strategy 
)
inline

Definition at line 79 of file presinst_strategy.h.

◆ operator<<() [5/24]

std::ostream & mcrl2::pres_system::operator<< ( std::ostream &  os,
const solution_algorithm  l 
)
inline

Definition at line 93 of file resalgorithm_type.h.

◆ operator<<() [6/24]

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

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

Definition at line 368 of file pres_expression.h.

◆ operator<<() [7/24]

std::ostream & mcrl2::pres_system::operator<< ( std::ostream &  out,
const condeq x 
)
inline

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

Definition at line 1280 of file pres_expression.h.

◆ operator<<() [8/24]

std::ostream & mcrl2::pres_system::operator<< ( std::ostream &  out,
const condsm x 
)
inline

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

Definition at line 1199 of file pres_expression.h.

◆ operator<<() [9/24]

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

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

Definition at line 672 of file pres_expression.h.

◆ operator<<() [10/24]

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

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

Definition at line 748 of file pres_expression.h.

◆ operator<<() [11/24]

std::ostream & mcrl2::pres_system::operator<< ( std::ostream &  out,
const eqinf x 
)
inline

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

Definition at line 1047 of file pres_expression.h.

◆ operator<<() [12/24]

std::ostream & mcrl2::pres_system::operator<< ( std::ostream &  out,
const eqninf x 
)
inline

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

Definition at line 1118 of file pres_expression.h.

◆ operator<<() [13/24]

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

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

Definition at line 520 of file pres_expression.h.

◆ operator<<() [14/24]

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

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

Definition at line 824 of file pres_expression.h.

◆ operator<<() [15/24]

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

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

Definition at line 292 of file pres_expression.h.

◆ operator<<() [16/24]

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

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

Definition at line 444 of file pres_expression.h.

◆ operator<<() [17/24]

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

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

Definition at line 596 of file pres_expression.h.

◆ operator<<() [18/24]

std::ostream & mcrl2::pres_system::operator<< ( std::ostream &  out,
const pres x 
)
inline

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

Definition at line 310 of file pres.h.

◆ operator<<() [19/24]

std::ostream & mcrl2::pres_system::operator<< ( std::ostream &  out,
const pres_equation x 
)
inline

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

Definition at line 147 of file pres_equation.h.

◆ operator<<() [20/24]

std::ostream & mcrl2::pres_system::operator<< ( std::ostream &  out,
const pres_expression x 
)
inline

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

Definition at line 128 of file pres_expression.h.

◆ operator<<() [21/24]

std::ostream & mcrl2::pres_system::operator<< ( std::ostream &  out,
const pressolve_options options 
)
inline

Definition at line 34 of file pressolve_options.h.

◆ operator<<() [22/24]

std::ostream & mcrl2::pres_system::operator<< ( std::ostream &  out,
const propositional_variable_instantiation x 
)
inline

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

Definition at line 221 of file pres_expression.h.

◆ operator<<() [23/24]

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

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

Definition at line 976 of file pres_expression.h.

◆ operator<<() [24/24]

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

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

Definition at line 900 of file pres_expression.h.

◆ operator==() [1/2]

bool mcrl2::pres_system::operator== ( const pres p1,
const pres p2 
)
inline

Equality operator on PRESs.

Returns
True if the PRESs have exactly the same internal representation. Note that this is in general not a very useful test.

Definition at line 333 of file pres.h.

◆ operator==() [2/2]

bool mcrl2::pres_system::operator== ( const pres_equation x,
const pres_equation y 
)
inline

Definition at line 160 of file pres_equation.h.

◆ operator>>() [1/6]

atermpp::aterm_istream & mcrl2::pres_system::operator>> ( atermpp::aterm_istream stream,
pres pres 
)

Reads a pres from a stream.

Definition at line 238 of file io.cpp.

◆ operator>>() [2/6]

atermpp::aterm_istream & mcrl2::pres_system::operator>> ( atermpp::aterm_istream stream,
pres_equation equation 
)
inline

Definition at line 205 of file io.cpp.

◆ operator>>() [3/6]

std::istream & mcrl2::pres_system::operator>> ( std::istream &  from,
pres result 
)
inline

Reads a PRES from an input stream.

Parameters
fromAn input stream
resultA PRES
Returns
The input stream

Definition at line 52 of file parse.h.

◆ operator>>() [4/6]

std::istream & mcrl2::pres_system::operator>> ( std::istream &  is,
pres_rewriter_type t 
)
inline

Stream operator for rewriter type.

Parameters
isAn input stream
tA rewriter type
Returns
The input stream

Definition at line 107 of file pres_rewriter_type.h.

◆ operator>>() [5/6]

std::istream & mcrl2::pres_system::operator>> ( std::istream &  is,
presinst_strategy s 
)
inline

Definition at line 48 of file presinst_strategy.h.

◆ operator>>() [6/6]

std::istream & mcrl2::pres_system::operator>> ( std::istream &  is,
solution_algorithm l 
)
inline

Definition at line 76 of file resalgorithm_type.h.

◆ optimized_and()

void mcrl2::pres_system::optimized_and ( pres_expression result,
const pres_expression p,
const pres_expression q 
)
inline

Make a conjunction.

Parameters
pA PRES expression
qA PRES expression
Returns
The value p && q

Definition at line 1586 of file pres_expression.h.

◆ optimized_condeq()

void mcrl2::pres_system::optimized_condeq ( pres_expression result,
const pres_expression p1,
const pres_expression p2,
const pres_expression p3 
)
inline

Make an optimized condsm expression.

Parameters
p1A pres expression
p2A pres expression
p3A pres expression
Returns
An optimized representation of condsm(p1, p2, p3)

Definition at line 1823 of file pres_expression.h.

◆ optimized_condsm()

void mcrl2::pres_system::optimized_condsm ( pres_expression result,
const pres_expression p1,
const pres_expression p2,
const pres_expression p3 
)
inline

Make an optimized condsm expression.

Parameters
p1A pres expression
p2A pres expression
p3A pres expression
Returns
An optimized representation of condsm(p1, p2, p3)

Definition at line 1801 of file pres_expression.h.

◆ optimized_const_multiply()

void mcrl2::pres_system::optimized_const_multiply ( pres_expression result,
const data::data_expression d,
const pres_expression p 
)
inline

Make an optimized const_multiply expression.

Parameters
dA real data expression, which should be positive.
pA pres expression
Returns
An optimized representation of eqinf(p)

Definition at line 1897 of file pres_expression.h.

◆ optimized_const_multiply_alt()

void mcrl2::pres_system::optimized_const_multiply_alt ( pres_expression result,
const data::data_expression d,
const pres_expression p 
)
inline

Make an optimized const_multiply_alt expression.

Parameters
dA real data expression, which should be positive.
pA pres expression
Returns
An optimized representation of eqinf(p)

Definition at line 1918 of file pres_expression.h.

◆ optimized_eqinf()

void mcrl2::pres_system::optimized_eqinf ( pres_expression result,
const pres_expression p 
)
inline

Make an optimized eqinf expression.

Parameters
pA pres expression
Returns
An optimized representation of eqinf(p)

Definition at line 1844 of file pres_expression.h.

◆ optimized_eqninf()

void mcrl2::pres_system::optimized_eqninf ( pres_expression result,
const pres_expression p 
)
inline

Make an optimized eqinf expression.

Parameters
pA pres expression
Returns
An optimized representation of eqinf(p)

Definition at line 1870 of file pres_expression.h.

◆ optimized_infimum()

void mcrl2::pres_system::optimized_infimum ( pres_expression result,
const data::variable_list l,
const pres_expression p 
)
inline

Make an implication.

Parameters
pA PRES expression
qA PRES expression
Returns
The value p => q

Make an infimum quantification If l is empty, p is returned.

Parameters
lA sequence of data variables
pA PRES expression
Returns
The value inf l.p

Definition at line 1669 of file pres_expression.h.

◆ optimized_join_and()

template<typename FwdIt >
pres_expression mcrl2::pres_system::optimized_join_and ( FwdIt  first,
FwdIt  last 
)
inline

Returns and applied to the sequence of pres expressions [first, last)

Parameters
firstStart of a sequence of pres expressions
lastEnd of a sequence of pres expressions
Returns
And applied to the sequence of pres expressions [first, last)

Definition at line 116 of file join.h.

◆ optimized_join_or()

template<typename FwdIt >
pres_expression mcrl2::pres_system::optimized_join_or ( FwdIt  first,
FwdIt  last 
)
inline

Returns or applied to the sequence of pres expressions [first, last)

Parameters
firstStart of a sequence of pres expressions
lastEnd of a sequence of pres expressions
Returns
Or applied to the sequence of pres expressions [first, last)

Definition at line 98 of file join.h.

◆ optimized_minus()

void mcrl2::pres_system::optimized_minus ( pres_expression result,
const pres_expression p 
)
inline

Make a negation.

Parameters
pA PRES expression
Returns
The value !p

Definition at line 1573 of file pres_expression.h.

◆ optimized_or()

void mcrl2::pres_system::optimized_or ( pres_expression result,
const pres_expression p,
const pres_expression q 
)
inline

Make a disjunction.

Parameters
pA PRES expression
qA PRES expression
Returns
The value p || q

Definition at line 1596 of file pres_expression.h.

◆ optimized_plus()

void mcrl2::pres_system::optimized_plus ( pres_expression result,
const pres_expression p,
const pres_expression q 
)
inline

Make a disjunction.

Parameters
pA PRES expression
qA PRES expression
Returns
The value p || q

Definition at line 1606 of file pres_expression.h.

◆ optimized_sum()

void mcrl2::pres_system::optimized_sum ( pres_expression result,
const data::variable_list l,
const pres_expression p,
const data::data_specification data_specification,
const data::rewriter rewr 
)
inline

Make an sum quantification. If l is empty, p is returned.

Parameters
lA sequence of data variables.
pA PRES expression.
data_specificationA data specification to determine the cardinality of sorts.
rewrA rewriter to determine the cardinality of sorts.
Returns
The value sum l.p

Definition at line 1717 of file pres_expression.h.

◆ optimized_supremum()

void mcrl2::pres_system::optimized_supremum ( pres_expression result,
const data::variable_list l,
const pres_expression p 
)
inline

Make a supremum. If l is empty, p is returned.

Parameters
lA sequence of data variables
pA PRES expression
Returns
The value sup l.p

Definition at line 1692 of file pres_expression.h.

◆ parelm()

void mcrl2::pres_system::parelm ( pres p)
inline

Apply the parelm algorithm.

Parameters
pA PRES to which the algorithm is applied

Definition at line 326 of file parelm.h.

◆ parse_algorithm()

solution_algorithm mcrl2::pres_system::parse_algorithm ( const std::string &  s)
inline

Parse an algorithm.

Parameters
[in]sA string
Returns
The algorithm represented by s

Definition at line 53 of file resalgorithm_type.h.

◆ parse_pres() [1/2]

pres mcrl2::pres_system::parse_pres ( const std::string &  text)
inline

Definition at line 59 of file parse.h.

◆ parse_pres() [2/2]

pres mcrl2::pres_system::parse_pres ( std::istream &  in)
inline

Definition at line 39 of file parse.h.

◆ parse_pres_expression() [1/4]

template<typename SubstitutionFunction >
pres_expression mcrl2::pres_system::parse_pres_expression ( const std::string &  expr,
const std::string &  subst,
const pres p,
SubstitutionFunction &  sigma 
)

Parses a pres expression.

Parameters
exprA string
substA string
pA PRES
sigmaA substitution function
Returns
The parsed expression

Definition at line 189 of file parse.h.

◆ parse_pres_expression() [2/4]

template<typename VariableContainer , typename PropositionalVariableContainer >
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.

Parameters
[in]textA string containing a pres expression.
[in]variablesA sequence of data variables that may appear in x.
[in]propositional_variablesA sequence of propositional variables that may appear in x.
[in]dataspecA data specification.
[in]type_checkIf true the parsed input is also typechecked.
Returns
The parsed PRES expression.

Definition at line 85 of file parse.h.

◆ parse_pres_expression() [3/4]

template<typename VariableContainer >
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.

Parameters
[in]textA string containing a pres expression.
[in]presspecA PRES used as context.
[in]variablesA sequence of data variables that may appear in x.
[in]type_checkIf true the parsed input is also typechecked.
Returns
The parsed PRES expression.

Definition at line 119 of file parse.h.

◆ parse_pres_expression() [4/4]

pres_expression mcrl2::pres_system::parse_pres_expression ( const std::string &  text,
const std::string &  var_decl = "datavar\npredvar\n",
const std::string &  data_spec = "" 
)
inline

Parses a single pres expression.

Parameters
textA string
var_declA string with their types.
An example of this is:
datavar
n: Nat;
predvar
X: Pos;
Y: Nat, Bool;
data_specA string
Returns
The parsed expression

Definition at line 177 of file parse.h.

◆ parse_pres_expressions()

std::pair< std::vector< pres_expression >, data::data_specification > mcrl2::pres_system::parse_pres_expressions ( std::string  text,
const std::string &  data_spec = "" 
)
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:

datavar
n: Nat;
predvar
X: Pos;
Y: Nat, Bool;
Parameters
textA string
data_specA 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.
Returns
The parsed expression and the data specification that was used.

Definition at line 42 of file parse.h.

◆ parse_pres_rewriter_type()

pres_rewriter_type mcrl2::pres_system::parse_pres_rewriter_type ( const std::string &  type)
inline

Parses a pres rewriter type.

Definition at line 35 of file pres_rewriter_type.h.

◆ parse_presinst_strategy()

presinst_strategy mcrl2::pres_system::parse_presinst_strategy ( const std::string &  s)
inline

Parse a presinst transformation strategy.

Definition at line 31 of file presinst_strategy.h.

◆ parse_propositional_variable()

template<typename VariableContainer >
propositional_variable mcrl2::pres_system::parse_propositional_variable ( const std::string &  text,
const VariableContainer &  variables,
const data::data_specification dataspec = data::data_specification() 
)

Definition at line 66 of file parse.h.

◆ pp() [1/28]

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

Definition at line 35 of file pres.cpp.

◆ pp() [2/28]

std::string mcrl2::pres_system::pp ( const condeq x)

◆ pp() [3/28]

std::string mcrl2::pres_system::pp ( const condsm x)

◆ pp() [4/28]

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

Definition at line 43 of file pres.cpp.

◆ pp() [5/28]

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

Definition at line 44 of file pres.cpp.

◆ pp() [6/28]

std::string mcrl2::pres_system::pp ( const eqinf x)

◆ pp() [7/28]

std::string mcrl2::pres_system::pp ( const eqninf x)

◆ pp() [8/28]

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

Definition at line 41 of file pres.cpp.

◆ pp() [9/28]

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

Definition at line 39 of file pres.cpp.

◆ pp() [10/28]

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

Definition at line 42 of file pres.cpp.

◆ pp() [11/28]

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

Definition at line 36 of file pres.cpp.

◆ pp() [12/28]

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

◆ pp() [13/28]

std::string mcrl2::pres_system::pp ( const pres x)

Definition at line 45 of file pres.cpp.

◆ pp() [14/28]

std::string mcrl2::pres_system::pp ( const pres_equation x)

Definition at line 46 of file pres.cpp.

◆ pp() [15/28]

std::string mcrl2::pres_system::pp ( const pres_equation_vector x)

Definition at line 28 of file pres.cpp.

◆ pp() [16/28]

std::string mcrl2::pres_system::pp ( const pres_expression x)

Definition at line 47 of file pres.cpp.

◆ pp() [17/28]

std::string mcrl2::pres_system::pp ( const pres_expression_list x)

Definition at line 29 of file pres.cpp.

◆ pp() [18/28]

std::string mcrl2::pres_system::pp ( const pres_expression_vector x)

Definition at line 30 of file pres.cpp.

◆ pp() [19/28]

std::string mcrl2::pres_system::pp ( const pres_system::fixpoint_symbol x)

Definition at line 38 of file pres.cpp.

◆ pp() [20/28]

std::string mcrl2::pres_system::pp ( const pres_system::propositional_variable_list x)

Definition at line 31 of file pres.cpp.

◆ pp() [21/28]

std::string mcrl2::pres_system::pp ( const pres_system::propositional_variable_vector x)

Definition at line 32 of file pres.cpp.

◆ pp() [22/28]

std::string mcrl2::pres_system::pp ( const propositional_variable v)

Definition at line 48 of file pres.cpp.

◆ pp() [23/28]

std::string mcrl2::pres_system::pp ( const propositional_variable_instantiation x)

Definition at line 49 of file pres.cpp.

◆ pp() [24/28]

std::string mcrl2::pres_system::pp ( const propositional_variable_instantiation_list x)

Definition at line 33 of file pres.cpp.

◆ pp() [25/28]

std::string mcrl2::pres_system::pp ( const propositional_variable_instantiation_vector x)

Definition at line 34 of file pres.cpp.

◆ pp() [26/28]

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

Definition at line 40 of file pres.cpp.

◆ pp() [27/28]

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

Definition at line 37 of file pres.cpp.

◆ pp() [28/28]

template<typename T >
std::string mcrl2::pres_system::pp ( const T &  x)

Returns a string representation of the object x.

Definition at line 355 of file print.h.

◆ precedence() [1/11]

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

Definition at line 28 of file print.h.

◆ precedence() [2/11]

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

Definition at line 30 of file print.h.

◆ precedence() [3/11]

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

Definition at line 31 of file print.h.

◆ precedence() [4/11]

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

Definition at line 26 of file print.h.

◆ precedence() [5/11]

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

Definition at line 22 of file print.h.

◆ precedence() [6/11]

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

Definition at line 29 of file print.h.

◆ precedence() [7/11]

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

Definition at line 27 of file print.h.

◆ precedence() [8/11]

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

Definition at line 25 of file print.h.

◆ precedence() [9/11]

int mcrl2::pres_system::precedence ( const pres_expression x)
inline

Definition at line 32 of file print.h.

◆ precedence() [10/11]

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

Definition at line 24 of file print.h.

◆ precedence() [11/11]

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

Definition at line 23 of file print.h.

◆ pres_equation_to_aterm()

atermpp::aterm mcrl2::pres_system::pres_equation_to_aterm ( const pres_equation eqn)
inline

Conversion to atermaPpl.

Returns
The specification converted to aterm format.

Definition at line 176 of file pres_equation.h.

◆ pres_file_formats()

const std::vector< utilities::file_format > & mcrl2::pres_system::pres_file_formats ( )

Definition at line 24 of file io.cpp.

◆ pres_format_internal()

const utilities::file_format & mcrl2::pres_system::pres_format_internal ( )
inline

Definition at line 40 of file io.h.

◆ pres_format_text()

const utilities::file_format & mcrl2::pres_system::pres_format_text ( )
inline

Definition at line 42 of file io.h.

◆ pres_marker()

atermpp::aterm mcrl2::pres_system::pres_marker ( )

Definition at line 220 of file io.cpp.

◆ pres_rewrite() [1/4]

template<typename T , typename Rewriter , typename Substitution >
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 
)

Rewrites all embedded pres expressions in an object x, and applies a substitution to variables on the fly.

Parameters
xan object containing expressions
Ra pres rewriter
sigmaa substitution
Returns
the rewrite result

Definition at line 199 of file rewrite.h.

◆ pres_rewrite() [2/4]

template<typename T , typename Rewriter >
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 
)

Rewrites all embedded pres expressions in an object x.

Parameters
xan object containing expressions
Ra pres rewriter
Returns
the rewrite result

Definition at line 169 of file rewrite.h.

◆ pres_rewrite() [3/4]

template<typename T , typename Rewriter , typename Substitution >
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 
)

Rewrites all embedded pres expressions in an object x, and applies a substitution to variables on the fly.

Parameters
xan object containing expressions
Ra pres rewriter
sigmaa substitution

Definition at line 184 of file rewrite.h.

◆ pres_rewrite() [4/4]

template<typename T , typename Rewriter >
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 
)

Rewrites all embedded pres expressions in an object x.

Parameters
xan object containing expressions
Ra pres rewriter

Definition at line 156 of file rewrite.h.

◆ pres_to_aterm()

atermpp::aterm mcrl2::pres_system::pres_to_aterm ( const pres p)

Conversion to atermappl.

Returns
The PRES converted to aterm format.

Definition at line 319 of file io.cpp.

◆ presconstelm()

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.

◆ presinfo()

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.

◆ presinst_finite()

void mcrl2::pres_system::presinst_finite ( pres p,
data::rewrite_strategy  rewrite_strategy,
const std::string &  finite_parameter_selection 
)
inline

Definition at line 410 of file presinst_finite_algorithm.h.

◆ presinst_is_constant()

bool mcrl2::pres_system::presinst_is_constant ( const pres_expression x)
inline

Definition at line 44 of file presinst_algorithm.h.

◆ presparelm()

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.

◆ prespp()

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 
)

Definition at line 21 of file prespp.h.

◆ presrewr()

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.

◆ print_algorithm()

std::string mcrl2::pres_system::print_algorithm ( const solution_algorithm  alg)
inline

Definition at line 25 of file resalgorithm_type.h.

◆ print_pres_rewriter_type()

std::string mcrl2::pres_system::print_pres_rewriter_type ( const pres_rewriter_type  type)
inline

Prints a pres rewriter type.

Definition at line 62 of file pres_rewriter_type.h.

◆ print_presinst_strategy()

std::string mcrl2::pres_system::print_presinst_strategy ( const presinst_strategy  strategy)
inline

Returns a string representation of a presinst transformation strategy.

Definition at line 65 of file presinst_strategy.h.

◆ reachable_variables()

std::set< propositional_variable > mcrl2::pres_system::reachable_variables ( const pres p)
inline

Definition at line 38 of file remove_equations.h.

◆ remove_index_impl()

static atermpp::aterm mcrl2::pres_system::remove_index_impl ( const atermpp::aterm x)
static

Definition at line 165 of file io.cpp.

◆ remove_parameters() [1/6]

template<typename T >
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.

Parameters
xA PRES library object that derives from atermpp::aterm
to_be_removedA mapping that maps propositional variable names to indices of parameters that are removed
Returns
The expression x with parameters removed according to the mapping to_be_removed

Definition at line 208 of file remove_parameters.h.

◆ remove_parameters() [2/6]

template<typename T >
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.

Parameters
xA PRES library object that derives from atermpp::aterm
to_be_removedA set of parameters that are to be removed
Returns
The expression x with parameters removed according to the mapping to_be_removed

Definition at line 318 of file remove_parameters.h.

◆ remove_parameters() [3/6]

template<typename T >
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.

Parameters
xA PRES library object that derives from atermpp::aterm
to_be_removedThe indices of parameters that are to be removed
Returns
The expression x with parameters removed according to the mapping to_be_removed

Definition at line 107 of file remove_parameters.h.

◆ remove_parameters() [4/6]

template<typename T >
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.

Parameters
xA PRES library object that does not derive from atermpp::aterm
to_be_removedA mapping that maps propositional variable names to a sorted vector of parameter indices that need to be removed
Returns
The expression x with parameters removed according to the mapping to_be_removed

Definition at line 224 of file remove_parameters.h.

◆ remove_parameters() [5/6]

template<typename T >
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.

Parameters
xA PRES library object that does not derive from atermpp::aterm
to_be_removedA set of parameters that are to be removed
Returns
The expression x with parameters removed according to the mapping to_be_removed

Definition at line 333 of file remove_parameters.h.

◆ remove_parameters() [6/6]

template<typename T >
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.

Parameters
xA PRES library object that does not derive from atermpp::aterm
to_be_removedThe indices of parameters that are to be removed
Returns
The expression x with parameters removed according to the mapping to_be_removed

Definition at line 122 of file remove_parameters.h.

◆ remove_unreachable_variables()

std::vector< propositional_variable > mcrl2::pres_system::remove_unreachable_variables ( pres p)
inline

Removes equations that are not (syntactically) reachable from the initial state of a PRES.

Returns
The removed variables

Definition at line 82 of file remove_equations.h.

◆ replace_all_variables() [1/2]

template<typename T , typename Substitution >
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 
)

Definition at line 169 of file replace.h.

◆ replace_all_variables() [2/2]

template<typename T , typename Substitution >
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 
)

Definition at line 160 of file replace.h.

◆ replace_data_expressions() [1/2]

template<typename T , typename Substitution >
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 
)

Definition at line 127 of file replace.h.

◆ replace_data_expressions() [2/2]

template<typename T , typename Substitution >
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 
)

Definition at line 117 of file replace.h.

◆ replace_free_variables() [1/4]

template<typename T , typename Substitution , typename VariableContainer >
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 
)

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

Definition at line 221 of file replace.h.

◆ replace_free_variables() [2/4]

template<typename T , typename Substitution >
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 
)

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

Definition at line 194 of file replace.h.

◆ replace_free_variables() [3/4]

template<typename T , typename Substitution , typename VariableContainer >
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 
)

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

Definition at line 208 of file replace.h.

◆ replace_free_variables() [4/4]

template<typename T , typename Substitution >
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 
)

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

Definition at line 182 of file replace.h.

◆ replace_pres_expressions() [1/2]

template<typename T , typename Substitution >
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 
)

Definition at line 278 of file replace.h.

◆ replace_pres_expressions() [2/2]

template<typename T , typename Substitution >
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 
)

Definition at line 268 of file replace.h.

◆ replace_propositional_variables() [1/3]

template<typename T , typename Substitution >
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 
)

Applies a propositional variable substitution.

Definition at line 246 of file replace.h.

◆ replace_propositional_variables() [2/3]

template<typename T , typename Substitution >
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 
)

Applies a propositional variable substitution.

Definition at line 258 of file replace.h.

◆ replace_propositional_variables() [3/3]

template<typename T , typename Substitution >
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 
)

Applies a propositional variable substitution.

Definition at line 236 of file replace.h.

◆ replace_sort_expressions() [1/2]

template<typename T , typename Substitution >
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 
)

Definition at line 105 of file replace.h.

◆ replace_sort_expressions() [2/2]

template<typename T , typename Substitution >
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 
)

Definition at line 95 of file replace.h.

◆ replace_variables() [1/2]

template<typename T , typename Substitution >
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 
)

Definition at line 149 of file replace.h.

◆ replace_variables() [2/2]

template<typename T , typename Substitution >
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 
)

Definition at line 140 of file replace.h.

◆ replace_variables_capture_avoiding() [1/4]

template<typename T , typename Substitution >
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.

◆ replace_variables_capture_avoiding() [2/4]

template<typename T , typename Substitution >
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.

◆ replace_variables_capture_avoiding() [3/4]

template<typename T , typename Substitution >
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.

◆ replace_variables_capture_avoiding() [4/4]

template<typename T , typename Substitution >
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.

◆ replace_variables_capture_avoiding_with_an_identifier_generator() [1/2]

template<typename T , typename Substitution , typename IdentifierGenerator >
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.

◆ replace_variables_capture_avoiding_with_an_identifier_generator() [2/2]

template<typename T , typename Substitution , typename IdentifierGenerator >
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.

◆ rewrite() [1/4]

template<typename T , typename Rewriter , typename Substitution >
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 
)

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

Definition at line 140 of file rewrite.h.

◆ rewrite() [2/4]

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

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

Definition at line 110 of file rewrite.h.

◆ rewrite() [3/4]

template<typename T , typename Rewriter , typename Substitution >
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 
)

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

Definition at line 125 of file rewrite.h.

◆ rewrite() [4/4]

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

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

Definition at line 97 of file rewrite.h.

◆ save_pres() [1/2]

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.

Parameters
presThe PRES to save.
filenameThe file to save the PRES in.
formatThe format in which to save the PRES.
welltypedness_checkIf 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().

Definition at line 104 of file io.cpp.

◆ save_pres() [2/2]

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.

Parameters
presThe PRES to be stored
streamThe stream to which the output is saved.
formatDetermines the format in which the result is written. If unspecified, or pres_file_unknown is specified, then a default format is chosen.

Definition at line 43 of file io.cpp.

◆ search_variable() [1/2]

bool mcrl2::pres_system::search_variable ( const pres_system::pres_expression x,
const data::variable v 
)

Definition at line 63 of file pres.cpp.

◆ search_variable() [2/2]

template<typename T >
bool mcrl2::pres_system::search_variable ( const T &  x,
const data::variable v 
)

Returns true if the term has a given variable as subterm.

Parameters
[in]xan expression
[in]va variable
Returns
True if v occurs in x.

Definition at line 217 of file find.h.

◆ significant_variables()

std::set< data::variable > mcrl2::pres_system::significant_variables ( const pres_expression x)
inline

Definition at line 119 of file significant_variables.h.

◆ split_and()

std::set< pres_expression > mcrl2::pres_system::split_and ( const pres_expression expr,
bool  split_data_expressions = false 
)
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.

Parameters
exprA PRES expression
split_data_expressionsif true, both data and pres conjunctions are split, otherwise only pres conjunctions are split.
Returns
A sequence of operands

Definition at line 76 of file join.h.

◆ split_or()

std::set< pres_expression > mcrl2::pres_system::split_or ( const pres_expression expr,
bool  split_data_expressions = false 
)
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.

Parameters
exprA PRES expression
split_data_expressionsif true, both data and pres disjunctions are split, otherwise only pres disjunctions are split.
Returns
A sequence of operands

Definition at line 50 of file join.h.

◆ swap() [1/17]

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

\brief swap overload

Definition at line 374 of file pres_expression.h.

◆ swap() [2/17]

void mcrl2::pres_system::swap ( condeq t1,
condeq t2 
)
inline

\brief swap overload

Definition at line 1286 of file pres_expression.h.

◆ swap() [3/17]

void mcrl2::pres_system::swap ( condsm t1,
condsm t2 
)
inline

\brief swap overload

Definition at line 1205 of file pres_expression.h.

◆ swap() [4/17]

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

\brief swap overload

Definition at line 678 of file pres_expression.h.

◆ swap() [5/17]

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

\brief swap overload

Definition at line 754 of file pres_expression.h.

◆ swap() [6/17]

void mcrl2::pres_system::swap ( eqinf t1,
eqinf t2 
)
inline

\brief swap overload

Definition at line 1053 of file pres_expression.h.

◆ swap() [7/17]

void mcrl2::pres_system::swap ( eqninf t1,
eqninf t2 
)
inline

\brief swap overload

Definition at line 1124 of file pres_expression.h.

◆ swap() [8/17]

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

\brief swap overload

Definition at line 526 of file pres_expression.h.

◆ swap() [9/17]

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

\brief swap overload

Definition at line 830 of file pres_expression.h.

◆ swap() [10/17]

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

\brief swap overload

Definition at line 298 of file pres_expression.h.

◆ swap() [11/17]

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

\brief swap overload

Definition at line 450 of file pres_expression.h.

◆ swap() [12/17]

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

\brief swap overload

Definition at line 602 of file pres_expression.h.

◆ swap() [13/17]

void mcrl2::pres_system::swap ( pres_equation t1,
pres_equation t2 
)
inline

\brief swap overload

Definition at line 153 of file pres_equation.h.

◆ swap() [14/17]

void mcrl2::pres_system::swap ( pres_expression t1,
pres_expression t2 
)
inline

\brief swap overload

Definition at line 134 of file pres_expression.h.

◆ swap() [15/17]

void mcrl2::pres_system::swap ( propositional_variable_instantiation t1,
propositional_variable_instantiation t2 
)
inline

\brief swap overload

Definition at line 227 of file pres_expression.h.

◆ swap() [16/17]

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

\brief swap overload

Definition at line 982 of file pres_expression.h.

◆ swap() [17/17]

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

\brief swap overload

Definition at line 906 of file pres_expression.h.

◆ translate_user_notation() [1/4]

pres_system::pres_expression mcrl2::pres_system::translate_user_notation ( const pres_system::pres_expression x)

Definition at line 54 of file pres.cpp.

◆ translate_user_notation() [2/4]

template<typename T >
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.

◆ translate_user_notation() [3/4]

void mcrl2::pres_system::translate_user_notation ( pres_system::pres x)

Definition at line 53 of file pres.cpp.

◆ translate_user_notation() [4/4]

template<typename T >
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.

◆ true_()

const pres_expression & mcrl2::pres_system::true_ ( )
inline
Returns
Returns the value true

Definition at line 1306 of file pres_expression.h.

◆ txt2pres() [1/3]

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.

◆ txt2pres() [2/3]

pres mcrl2::pres_system::txt2pres ( const std::string &  text,
bool  normalize = true 
)
inline

Parses a PRES specification from a string.

Parameters
textA string
normalizeIf true, the resulting PRES is normalized after reading.
Returns
The parsed PRES

Definition at line 47 of file txt2pres.h.

◆ txt2pres() [3/3]

pres mcrl2::pres_system::txt2pres ( std::istream &  spec_stream,
bool  normalize = true 
)
inline

Parses a PRES specification from an input stream.

Parameters
spec_streamA stream from which can be read
normalizeIf true, the resulting PRES is normalized after reading.
Returns
The parsed PRES

Definition at line 30 of file txt2pres.h.

◆ typecheck_pres()

void mcrl2::pres_system::typecheck_pres ( pres presspec)
inline

Type check a parsed mCRL2 pres specification. Throws an exception if something went wrong.

Parameters
[in]presspecA process specification that has not been type checked.
Postcondition
presspec is type checked.

Definition at line 341 of file typecheck.h.

◆ typecheck_pres_expression()

template<typename VariableContainer , typename PropositionalVariableContainer >
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.

Parameters
[in]xA pres expression.
[in]variablesA sequence of data variables that may appear in x.
[in]propositional_variablesA sequence of propositional variables that may appear in x.
[in]dataspecA data specification.
Returns
the type checked expression

Definition at line 394 of file typecheck.h.

◆ typecheck_propositional_variable()

template<typename VariableContainer >
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.

Parameters
[in]xA propositional variable.
[in]variablesA sequence of data variables that may appear in x.
[in]dataspecA data specification.
Returns
the type checked expression

Definition at line 362 of file typecheck.h.