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

The main namespace for the LPS library. More...

Namespaces

namespace  detail
 
namespace  tools
 

Classes

struct  abortable
 
class  action_label_data_type
 Models the mapping of mCRL2 action labels to integers. More...
 
struct  action_label_traverser
 \brief Traverser class More...
 
class  action_rename_rule
 Action rename rule. More...
 
class  action_rename_specification
 Read-only singly linked list of action rename rules. More...
 
class  action_rename_type_checker
 
class  action_summand
 LPS summand containing a multi-action. More...
 
struct  add_data_expressions
 
struct  add_data_variable_binding
 Maintains a multiset of bound data variables during traversal. More...
 
struct  add_data_variable_builder_binding
 
struct  add_data_variable_traverser_binding
 
struct  add_sort_expressions
 
struct  add_traverser_action_labels
 
struct  add_traverser_data_expressions
 
struct  add_traverser_identifier_strings
 
struct  add_traverser_sort_expressions
 
struct  add_traverser_variables
 
struct  add_variables
 
class  binary_algorithm
 Algorithm class that can be used to apply the binary algorithm. More...
 
class  breadth_first_todo_set
 
struct  commutative_confluence_condition
 Function object that computes the condition for commutative confluence. More...
 
class  confluence_checker
 
struct  confluence_summand
 
class  constelm_algorithm
 Algorithm class for elimination of constant parameters. 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...
 
class  deadlock
 Represents a deadlock. More...
 
class  deadlock_summand
 LPS summand containing a deadlock. More...
 
class  decluster_algorithm
 
class  depth_first_todo_set
 
class  explorer
 
struct  explorer_options
 
struct  explorer_summand
 
class  highway_todo_set
 
struct  identifier_string_traverser
 \brief Traverser class More...
 
class  invelm_algorithm
 
class  linear_process
 linear process. More...
 
class  linear_process_base
 
class  lpsparunfold
 
class  multi_action
 \brief A timed multi-action More...
 
class  multi_action_type_checker
 
class  parelm_algorithm
 Algorithm class for elimination of unused parameters from a linear process specification. More...
 
struct  parunfold_replacement
 
class  pins
 
class  pins_data_type
 Models a pins data type. A pins data type maintains a mapping between known values of a data type and integers. More...
 
class  probabilistic_data_expression
 This class contains labels for probabilistic transistions, consisting of a numerator and a denumerator. More...
 
class  process_initializer
 A process initializer. More...
 
class  simulation
 Simulation process. More...
 
struct  sort_expression_builder
 \brief Builder class More...
 
struct  sort_expression_traverser
 \brief Traverser class More...
 
class  specification
 Linear process specification. More...
 
class  specification_base
 
struct  square_confluence_condition
 Function object that computes the condition for square confluence. More...
 
class  state_data_type
 Models the mapping of mCRL2 state values to integers. More...
 
class  state_probability_pair
 
class  stochastic_action_summand
 LPS summand containing a multi-action. More...
 
class  stochastic_distribution
 \brief A stochastic distribution More...
 
class  stochastic_linear_process
 linear process. More...
 
class  stochastic_process_initializer
 A stochastic process initializer. More...
 
class  stochastic_specification
 Linear process specification. More...
 
struct  stochastic_state
 
struct  stream_printer
 Prints the object x to a stream. More...
 
class  sumelm_algorithm
 Class implementing the sum elimination lemma. More...
 
class  suminst_algorithm
 
class  summand_base
 Base class for LPS summands. More...
 
struct  t_lin_options
 Options for linearisation. More...
 
class  todo_set
 
struct  triangular_confluence_condition
 Function object that computes the condition for triangular confluence. More...
 
struct  trivial_confluence_condition
 Function object that computes the condition for triangular confluence. More...
 
struct  unfold_cache_element
 Element in the cache that keeps track of the information for a single unfolded sort, say s. More...
 
class  untime_algorithm
 
struct  variable_builder
 \brief Builder class More...
 
struct  variable_traverser
 \brief Traverser class More...
 

Typedefs

typedef atermpp::term_list< action_summandaction_summand_list
 \brief list of action_summands
 
typedef std::vector< action_summandaction_summand_vector
 \brief vector of action_summands
 
typedef atermpp::term_list< deadlockdeadlock_list
 \brief list of deadlocks
 
typedef std::vector< deadlockdeadlock_vector
 \brief vector of deadlocks
 
typedef atermpp::term_list< deadlock_summanddeadlock_summand_list
 \brief list of deadlock_summands
 
typedef std::vector< deadlock_summanddeadlock_summand_vector
 \brief vector of deadlock_summands
 
typedef atermpp::utilities::unordered_map< atermpp::term_appl< data::data_expression >, atermpp::term_list< data::data_expression_list >, detail::cache_hash, detail::cache_equality, std::allocator< std::pair< atermpp::term_appl< data::data_expression >, atermpp::term_list< data::data_expression_list > > >, true > summand_cache_map
 
typedef atermpp::term_list< multi_actionmulti_action_list
 \brief list of multi_actions
 
typedef std::vector< multi_actionmulti_action_vector
 \brief vector of multi_actions
 
typedef atermpp::term_list< process_initializerprocess_initializer_list
 \brief list of process_initializers
 
typedef std::vector< process_initializerprocess_initializer_vector
 \brief vector of process_initializers
 
typedef atermpp::term_balanced_tree< data::data_expressionstate
 
typedef atermpp::term_list< stochastic_action_summandstochastic_action_summand_list
 \brief list of stochastic_action_summands
 
typedef std::vector< stochastic_action_summandstochastic_action_summand_vector
 \brief vector of stochastic_action_summands
 
typedef atermpp::term_list< stochastic_distributionstochastic_distribution_list
 \brief list of stochastic_distributions
 
typedef std::vector< stochastic_distributionstochastic_distribution_vector
 \brief vector of stochastic_distributions
 
typedef atermpp::term_list< stochastic_process_initializerstochastic_process_initializer_list
 \brief list of stochastic_process_initializers
 
typedef std::vector< stochastic_process_initializerstochastic_process_initializer_vector
 \brief vector of stochastic_process_initializers
 

Enumerations

enum  exploration_strategy {
  es_none , es_breadth , es_depth , es_random ,
  es_value_prioritized , es_value_random_prioritized , es_highway
}
 
enum class  caching { none , local , global }
 
enum  t_lin_method { lmStack , lmRegular , lmRegular2 }
 The available linearisation methods. More...
 
enum  lps_rewriter_type { simplify , quantifier_one_point , condition_one_point }
 An enumerated type for the available lps rewriters. More...
 

Functions

atermpp::aterm_appl action_rename_rule_to_aterm (const action_rename_rule &rule)
 
atermpp::aterm_appl action_rename_specification_to_aterm (const action_rename_specification &spec)
 
lps::stochastic_specification action_rename (const action_rename_specification &action_rename_spec, const lps::stochastic_specification &lps_old_spec, const data::rewriter &rewr, const bool enable_rewriting)
 Rename the actions in a linear specification using a given action_rename_spec.
 
stochastic_specification action_rename (const std::regex &matching_regex, const std::string &replacing_fmt, const stochastic_specification &lps_old_spec)
 Rename actions in given specification based on a regular expression and a string that specifies how the replacement should be formatted.
 
std::string pp (const action_summand &x)
 
std::ostream & operator<< (std::ostream &out, const action_summand &x)
 
void swap (action_summand &t1, action_summand &t2)
 \brief swap overload
 
bool operator< (const action_summand &x, const action_summand &y)
 Comparison operator for action summands.
 
bool operator== (const action_summand &x, const action_summand &y)
 Equality operator of action summands.
 
atermpp::aterm_appl action_summand_to_aterm (const action_summand &s)
 Conversion to aterm_appl.
 
std::size_t nr_of_booleans_for_elements (std::size_t n)
 
template<typename Summand >
const stochastic_distributionsummand_distribution (const Summand &)
 
template<>
const stochastic_distributionsummand_distribution (const lps::stochastic_action_summand &summand)
 
std::set< data::variableused_read_variables (const action_summand &summand)
 
std::set< data::variablechanged_variables (const action_summand &summand)
 
data::assignment_list make_assignment_list (const data::variable_list &variables, const data::data_expression_list &expressions)
 
std::string print_confluence_summand (const confluence_summand &summand, const data::variable_list &process_parameters)
 
bool disjoint (const confluence_summand &summand1, const confluence_summand &summand2)
 Indicates whether or not two summands are disjoint.
 
process::action_label make_ctau_act_id ()
 Creates an identifier for the ctau action.
 
process::action make_ctau_action ()
 Creates the ctau action.
 
template<typename Specification >
bool has_ctau_action (const Specification &lpsspec)
 
template<typename DataRewriter , typename Specification >
void constelm (Specification &spec, const DataRewriter &R, bool instantiate_global_variables=false)
 Removes zero or more constant parameters from the specification spec.
 
std::string pp (const deadlock &x)
 
std::ostream & operator<< (std::ostream &out, const deadlock &x)
 
void swap (deadlock &t1, deadlock &t2)
 \brief swap overload
 
std::set< data::variablefind_all_variables (const lps::deadlock &x)
 
std::set< data::variablefind_free_variables (const lps::deadlock &x)
 
std::string pp (const deadlock_summand &x)
 
std::ostream & operator<< (std::ostream &out, const deadlock_summand &x)
 
void swap (deadlock_summand &t1, deadlock_summand &t2)
 \brief swap overload
 
atermpp::aterm_appl deadlock_summand_to_aterm (const deadlock_summand &s)
 Conversion to atermappl.
 
exploration_strategy parse_exploration_strategy (const std::string &s)
 
std::string print_exploration_strategy (const exploration_strategy es)
 
std::istream & operator>> (std::istream &is, exploration_strategy &strat)
 
std::ostream & operator<< (std::ostream &os, const exploration_strategy strat)
 
std::string description (const exploration_strategy strat)
 
std::ostream & operator<< (std::ostream &os, caching c)
 
std::vector< data::data_expressionmake_data_expression_vector (const data::data_expression_list &v)
 
template<>
const stochastic_distributionsummand_distribution (const lps::stochastic_action_summand &summand)
 
const stochastic_distributioninitial_distribution (const lps::specification &)
 
const stochastic_distributioninitial_distribution (const lps::stochastic_specification &lpsspec)
 
std::ostream & operator<< (std::ostream &out, const explorer_summand &summand)
 
std::ostream & operator<< (std::ostream &out, const explorer_options &options)
 
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 T >
bool search_free_variable (const T &x, const data::variable &v)
 Returns true if the term has a given free variable as subterm.
 
template<typename T , typename OutputIterator >
void find_action_labels (const T &x, OutputIterator o)
 Returns all action labels that occur in an object.
 
template<typename T >
std::set< process::action_labelfind_action_labels (const T &x)
 Returns all action labels that occur in an object.
 
template<typename Node , typename GenerateSuccessors >
Node find_representative (Node &u0, GenerateSuccessors generate_successors)
 Search for a unique representative in a graph.
 
template<typename T >
void if_rewrite (T &x, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 Applies the one point rule rewriter to all embedded data expressions in an object x.
 
template<typename T >
if_rewrite (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 Applies the one point rule rewriter to all embedded data expressions in an object x.
 
atermpp::aterm_ostreamoperator<< (atermpp::aterm_ostream &stream, const specification &spec)
 Writes LPS to the stream.
 
atermpp::aterm_ostreamoperator<< (atermpp::aterm_ostream &stream, const stochastic_specification &spec)
 
atermpp::aterm_istreamoperator>> (atermpp::aterm_istream &stream, specification &spec)
 Reads LPS from the stream.
 
atermpp::aterm_istreamoperator>> (atermpp::aterm_istream &stream, stochastic_specification &spec)
 
template<typename Specification >
void save_lps (const Specification &spec, std::ostream &stream, const std::string &target="")
 Save an LPS in the format specified.
 
template<typename Specification >
void load_lps (Specification &spec, std::istream &stream, const std::string &source="")
 Load LPS from file.
 
template<typename Specification >
void save_lps (const Specification &spec, const std::string &filename)
 Saves an LPS to a file.
 
template<typename Specification >
void load_lps (Specification &spec, const std::string &filename)
 Load LPS from file.
 
template<typename T >
bool is_stochastic (const T &x)
 Returns true if the LPS object x contains a stochastic distribution in one of its attributes.
 
bool check_well_typedness (const linear_process &x)
 
bool check_well_typedness (const stochastic_linear_process &x)
 
template<typename ActionSummand >
atermpp::aterm_appl linear_process_to_aterm (const linear_process_base< ActionSummand > &p)
 Conversion to aterm_appl.
 
std::string pp (const linear_process &x)
 
std::ostream & operator<< (std::ostream &out, const linear_process &x)
 
bool is_linear_process (const atermpp::aterm_appl &x)
 Test for a linear_process expression.
 
std::set< data::variablefind_all_variables (const lps::linear_process &x)
 
std::set< data::variablefind_free_variables (const lps::linear_process &x)
 
std::set< process::action_labelfind_action_labels (const lps::linear_process &x)
 
std::string print_lin_method (const t_lin_method lin_method)
 String representation of a linearisation method.
 
std::string description (const t_lin_method lin_method)
 
t_lin_method parse_lin_method (const std::string &s)
 Parse a linearisation method.
 
std::istream & operator>> (std::istream &is, t_lin_method &l)
 
std::ostream & operator<< (std::ostream &os, const t_lin_method l)
 
mcrl2::lps::stochastic_specification linearise (const mcrl2::process::process_specification &type_checked_spec, mcrl2::lps::t_lin_options lin_options=t_lin_options())
 Linearises a process specification.
 
mcrl2::lps::stochastic_specification linearise (const std::string &text, mcrl2::lps::t_lin_options lin_options=t_lin_options())
 Linearises a process specification from a textual specification.
 
lps_rewriter_type parse_lps_rewriter_type (const std::string &type)
 Parses a lps rewriter type.
 
std::string print_lps_rewriter_type (const lps_rewriter_type type)
 Prints a lps rewriter type.
 
std::string description (const lps_rewriter_type type)
 Returns a description of a lps rewriter.
 
std::istream & operator>> (std::istream &is, lps_rewriter_type &t)
 Stream operator for rewriter type.
 
std::ostream & operator<< (std::ostream &os, const lps_rewriter_type t)
 
template<template< class > class Builder, template< template< class > class, class, class > class Binder>
parunfold_replacement< Builder, Binder > apply_parunfold_replacement_builder (const lpsparunfold::case_func_replacement &case_funcs, data::set_identifier_generator &id_generator)
 
template<typename T >
void insert_case_functions (T &x, const lpsparunfold::case_func_replacement &cfv, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
template<typename T >
void insert_case_functions (T &x, const lpsparunfold::case_func_replacement &cfv, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 
std::vector< std::string > generate_values (const data::data_specification &dataspec, const data::sort_expression &s, std::size_t max_size=1000)
 Generates possible values of the data type (at most max_size).
 
bool is_multi_action (const atermpp::aterm_appl &x)
 
template<class... ARGUMENTS>
void make_multi_action (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
std::string pp (const multi_action &x)
 
std::ostream & operator<< (std::ostream &out, const multi_action &x)
 
void swap (multi_action &t1, multi_action &t2)
 \brief swap overload
 
lps::multi_action normalize_sorts (const multi_action &x, const data::sort_specification &sortspec)
 
lps::multi_action translate_user_notation (const lps::multi_action &x)
 
std::set< data::variablefind_all_variables (const lps::multi_action &x)
 
std::set< data::variablefind_free_variables (const lps::multi_action &x)
 
data::data_expression equal_multi_actions (const multi_action &a, const multi_action &b)
 Returns a data expression that expresses under which conditions the multi actions a and b are equal. The multi actions may contain free variables.
 
data::data_expression not_equal_multi_actions (const multi_action &a, const multi_action &b)
 Returns a pbes expression that expresses under which conditions the multi actions a and b are not equal. The multi actions may contain free variables.
 
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 *=0)
 
template<typename T >
void one_point_rule_rewrite (T &x, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 Applies the one point rule rewriter to all embedded data expressions in an object x.
 
template<typename T >
one_point_rule_rewrite (const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 Applies the one point rule rewriter to all embedded data expressions in an object x.
 
template<typename Specification >
void order_summand_variables (Specification &lpsspec)
 Order summand variables to make enumeration over these variables more efficient.
 
template<typename Specification >
void parelm (Specification &spec, bool variant1=true)
 Removes unused parameters from a linear process specification.
 
multi_action parse_multi_action (std::stringstream &in, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
 Parses a multi_action from an input stream.
 
multi_action parse_multi_action (std::stringstream &in, multi_action_type_checker &typechecker, const data::data_specification &data_spec=data::detail::default_specification())
 Parses a multi_action from an input stream.
 
multi_action parse_multi_action (const std::string &text, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
 Parses a multi_action from a string.
 
multi_action parse_multi_action (const std::string &text, multi_action_type_checker &typechecker, const data::data_specification &data_spec=data::detail::default_specification())
 Parses a multi_action from a string.
 
action_rename_specification parse_action_rename_specification (std::istream &in, const lps::stochastic_specification &spec)
 Parses a process specification from an input stream.
 
action_rename_specification parse_action_rename_specification (const std::string &spec_string, const lps::stochastic_specification &spec)
 Parses an action rename specification. Parses an acion rename specification. If the action rename specification contains data types that are not present in the data specification of spec they are added to it.
 
specification parse_linear_process_specification (std::istream &spec_stream)
 Parses a linear process specification from an input stream.
 
specification parse_linear_process_specification (const std::string &text)
 Parses a linear process specification from a string.
 
template<typename Specification >
void parse_lps (std::istream &, Specification &)
 
template<>
void parse_lps< specification > (std::istream &from, specification &result)
 
template<>
void parse_lps< stochastic_specification > (std::istream &from, stochastic_specification &result)
 Parses a stochastic linear process specification from an input stream.
 
template<typename Specification >
void parse_lps (const std::string &text, Specification &result)
 
process::action parse_action (const std::string &text, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
 Parses an action from a string.
 
template<typename T >
std::string pp (const T &x)
 Returns a string representation of the object x.
 
std::string pp (const probabilistic_data_expression &l)
 
std::ostream & operator<< (std::ostream &out, const probabilistic_data_expression &x)
 Pretty print to an outstream.
 
template<class EXPRESSION_LIST >
void make_process_initializer (atermpp::aterm_appl &t, EXPRESSION_LIST args)
 
bool is_process_initializer (const atermpp::aterm_appl &x)
 
std::string pp (const process_initializer &x)
 
std::ostream & operator<< (std::ostream &out, const process_initializer &x)
 
void swap (process_initializer &t1, process_initializer &t2)
 \brief swap overload
 
std::set< data::variablefind_free_variables (const lps::process_initializer &x)
 
std::set< process::action_labelfind_action_labels (const lps::process_initializer &x)
 
template<typename Object >
void remove_parameters (Object &x, const std::set< data::variable > &to_be_removed)
 Rewrites an LPS data type.
 
template<typename Specification >
void remove_trivial_summands (Specification &spec)
 Removes summands with condition equal to false from a linear process specification.
 
template<typename Specification >
void remove_singleton_sorts (Specification &spec)
 Removes parameters with a singleton sort from a linear process specification.
 
data::assignment_list remove_redundant_assignments (const data::assignment_list &assignments, const data::variable_list &do_not_remove)
 Removes assignments of the form x := x from v for variables x that are not contained in do_not_remove.
 
template<typename Specification >
void remove_redundant_assignments (Specification &lpsspec)
 Removes redundant assignments of the form x = x from an LPS specification.
 
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 Substitution >
stochastic_distribution replace_variables_capture_avoiding (const stochastic_distribution &x, data::data_expression_list &pars, Substitution &sigma, data::set_identifier_generator &id_generator)
 
template<typename Substitution >
stochastic_distribution replace_variables_capture_avoiding (const stochastic_distribution &x, data::data_expression_list &pars, Substitution &sigma)
 
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)
 
template<typename T >
void replace_constants_by_variables (T &x, const data::rewriter &r, data::mutable_indexed_substitution<> &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 Replace each constant data application c in x by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times.
 
template<typename T >
replace_constants_by_variables (const T &x, const data::rewriter &r, data::mutable_indexed_substitution<> &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 Replace each constant data application c in x by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times.
 
template<typename Specification >
void resolve_summand_variable_name_clashes (Specification &spec)
 Renames summand variables such that there are no name clashes between summand variables and process parameters.
 
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 DataRewriter >
void one_point_condition_rewrite (T &x, const DataRewriter &R, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 Applies the one point condition rewriter to all embedded data expressions in an object x.
 
template<typename T , typename DataRewriter >
one_point_condition_rewrite (const T &x, const DataRewriter &R, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
 Applies the one point condition rewriter to all embedded data expressions in an object x.
 
template<typename Object >
bool check_well_typedness (const Object &o)
 
template<typename LinearProcess , typename InitialProcessExpression >
atermpp::aterm_appl specification_to_aterm (const specification_base< LinearProcess, InitialProcessExpression > &spec)
 Conversion to aterm_appl.
 
void complete_data_specification (specification &spec)
 Adds all sorts that appear in the process of l to the data specification of l.
 
bool check_well_typedness (const specification &x)
 
void normalize_sorts (lps::specification &x, const data::sort_specification &sortspec)
 
bool is_specification (const atermpp::aterm_appl &x)
 Test for a specification expression.
 
std::string pp (const specification &x)
 
std::ostream & operator<< (std::ostream &out, const specification &x)
 
std::string pp_with_summand_numbers (const specification &x)
 
std::set< data::sort_expressionfind_sort_expressions (const lps::specification &x)
 
std::set< data::variablefind_all_variables (const lps::specification &x)
 
std::set< data::variablefind_free_variables (const lps::specification &x)
 
std::set< data::function_symbolfind_function_symbols (const lps::specification &x)
 
std::set< core::identifier_stringfind_identifiers (const lps::specification &x)
 
std::set< process::action_labelfind_action_labels (const lps::specification &x)
 
bool operator== (const specification &spec1, const specification &spec2)
 Equality operator.
 
bool operator!= (const specification &spec1, const specification &spec2)
 Inequality operator.
 
template<class ForwardTraversalIterator , class Transformer >
void make_state (state &result, ForwardTraversalIterator p, const std::size_t size, Transformer transformer)
 
template<class ForwardTraversalIterator >
void make_state (state &result, ForwardTraversalIterator p, const std::size_t size)
 
std::string pp (const lps::state &x)
 
std::string pp (const stochastic_action_summand &x)
 
std::ostream & operator<< (std::ostream &out, const stochastic_action_summand &x)
 
void swap (stochastic_action_summand &t1, stochastic_action_summand &t2)
 \brief swap overload
 
bool operator< (const stochastic_action_summand &x, const stochastic_action_summand &y)
 Comparison operator for action summands.
 
bool operator== (const stochastic_action_summand &x, const stochastic_action_summand &y)
 Equality operator of stochastic action summands.
 
atermpp::aterm_appl action_summand_to_aterm (const stochastic_action_summand &s)
 Conversion to aterm_appl.
 
template<class... ARGUMENTS>
void make_stochastic_distribution (atermpp::aterm_appl &t, const ARGUMENTS &... args)
 
bool is_stochastic_distribution (const atermpp::aterm_appl &x)
 
std::string pp (const stochastic_distribution &x)
 
std::ostream & operator<< (std::ostream &out, const stochastic_distribution &x)
 
void swap (stochastic_distribution &t1, stochastic_distribution &t2)
 \brief swap overload
 
std::string pp (const stochastic_linear_process &x)
 
std::ostream & operator<< (std::ostream &out, const stochastic_linear_process &x)
 
std::set< data::variablefind_all_variables (const lps::stochastic_linear_process &x)
 
std::set< data::variablefind_free_variables (const lps::stochastic_linear_process &x)
 
template<class... ARGUMENTS>
void make_stochastic_process_initializer (atermpp::aterm_appl &t, ARGUMENTS... args)
 
bool is_stochastic_process_initializer (const atermpp::aterm_appl &x)
 
std::string pp (const stochastic_process_initializer &x)
 
std::ostream & operator<< (std::ostream &out, const stochastic_process_initializer &x)
 
void swap (stochastic_process_initializer &t1, stochastic_process_initializer &t2)
 \brief swap overload
 
std::set< data::variablefind_free_variables (const lps::stochastic_process_initializer &x)
 
void complete_data_specification (stochastic_specification &spec)
 Adds all sorts that appear in the process of l to the data specification of l.
 
std::set< data::sort_expressionfind_sort_expressions (const lps::stochastic_specification &x)
 
std::set< data::variablefind_all_variables (const lps::stochastic_specification &x)
 
std::set< data::variablefind_free_variables (const lps::stochastic_specification &x)
 
std::set< data::function_symbolfind_function_symbols (const lps::stochastic_specification &x)
 
std::set< core::identifier_stringfind_identifiers (const lps::stochastic_specification &x)
 
bool check_well_typedness (const stochastic_specification &x)
 
void normalize_sorts (stochastic_specification &x, const data::sort_specification &sortspec)
 
std::string pp (const stochastic_specification &x)
 
std::ostream & operator<< (std::ostream &out, const stochastic_specification &x)
 
bool operator== (const stochastic_specification &spec1, const stochastic_specification &spec2)
 
bool operator!= (const stochastic_specification &spec1, const stochastic_specification &spec2)
 Inequality operator.
 
std::string pp_with_summand_numbers (const stochastic_specification &x)
 
specification remove_stochastic_operators (const stochastic_specification &spec)
 Converts a stochastic specification to a specification. Throws an exception if non-empty distributions are encountered.
 
std::string print_probability (const data::data_expression &x)
 
void check_probability (const data::data_expression &x, const data::rewriter &rewr)
 
void check_stochastic_state (const stochastic_state &s, const data::rewriter &rewr)
 
bool sumelm (action_summand &s)
 Apply the sum elimination lemma to summand s.
 
bool sumelm (stochastic_action_summand &s)
 Apply the sum elimination lemma to summand s.
 
bool sumelm (deadlock_summand &s)
 Apply the sum elimination lemma to summand s.
 
std::set< data::sort_expressionfinite_sorts (const data::data_specification &s)
 Return a set with all finite sorts in data specification s.
 
void lpsbinary (const std::string &input_filename, const std::string &output_filename, const std::string &parameter_selection)
 
void lpsconstelm (const std::string &input_filename, const std::string &output_filename, data::rewriter::strategy rewrite_strategy, bool instantiate_free_variables, bool ignore_conditions, bool remove_trivial_summands, bool remove_singleton_sorts)
 
void lpsinfo (const std::string &input_filename, const std::string &input_file_message)
 
bool lpsinvelm (const std::string &input_filename, const std::string &output_filename, const std::string &invariant_filename, const std::string &dot_file_name, data::rewriter::strategy rewrite_strategy, data::detail::smt_solver_type solver_type, const bool no_check, const bool no_elimination, const bool simplify_all, const bool all_violations, const bool counter_example, const bool path_eliminator, const bool apply_induction, const int time_limit)
 
void lpsparelm (const std::string &input_filename, const std::string &output_filename)
 
void lpspp (const std::string &input_filename, const std::string &output_filename, bool print_summand_numbers, core::print_format_type format)
 
void lpsrewr (const std::string &input_filename, const std::string &output_filename, const data::rewriter::strategy rewrite_strategy, const lps::lps_rewriter_type rewriter_type)
 
void lpssumelm (const std::string &input_filename, const std::string &output_filename, const bool decluster)
 
void lpssuminst (const std::string &input_filename, const std::string &output_filename, const data::rewriter::strategy rewrite_strategy, const std::string &sorts_string, const bool finite_sorts_only, const bool tau_summands_only)
 
void lpsuntime (const std::string &input_filename, const std::string &output_filename, const bool add_invariants, const bool apply_fourier_motzkin, const data::rewriter::strategy rewrite_strategy)
 
void txt2lps (const std::string &input_filename, const std::string &output_filename)
 
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)
 
multi_action typecheck_multi_action (process::untyped_multi_action &mult_act, const data::data_specification &data_spec, const process::action_label_list &action_decls)
 Type check a multi action Throws an exception if something went wrong.
 
multi_action typecheck_multi_action (process::untyped_multi_action &mult_act, multi_action_type_checker &typechecker)
 Type check a multi action Throws an exception if something went wrong.
 
action_rename_specification typecheck_action_rename_specification (const action_rename_specification &arspec, const lps::stochastic_specification &lpsspec)
 Type checks an action rename specification.
 
std::set< process::action_labelfind_action_labels (const lps::stochastic_specification &x)
 
atermpp::aterm linear_process_specification_marker ()
 
atermpp::aterm_ostreamoperator<< (atermpp::aterm_ostream &stream, const multi_action &action)
 
atermpp::aterm_istreamoperator>> (atermpp::aterm_istream &stream, multi_action &action)
 
atermpp::aterm_ostreamoperator<< (atermpp::aterm_ostream &stream, const deadlock_summand &summand)
 
atermpp::aterm_istreamoperator>> (atermpp::aterm_istream &stream, deadlock_summand &summand)
 
atermpp::aterm_ostreamoperator<< (atermpp::aterm_ostream &stream, const stochastic_action_summand &summand)
 
atermpp::aterm_istreamoperator>> (atermpp::aterm_istream &stream, stochastic_action_summand &summand)
 
template<typename ActionSummand >
atermpp::aterm_ostreamoperator<< (atermpp::aterm_ostream &stream, const linear_process_base< ActionSummand > &lps)
 
template<typename ActionSummand >
atermpp::aterm_istreamoperator>> (atermpp::aterm_istream &stream, linear_process_base< ActionSummand > &lps)
 
static void write_spec (atermpp::aterm_ostream &stream, const stochastic_specification &spec)
 
static void read_spec (atermpp::aterm_istream &stream, stochastic_specification &spec)
 

Detailed Description

The main namespace for the LPS library.

Typedef Documentation

◆ action_summand_list

\brief list of action_summands

Definition at line 116 of file action_summand.h.

◆ action_summand_vector

\brief vector of action_summands

Definition at line 119 of file action_summand.h.

◆ deadlock_list

\brief list of deadlocks

Definition at line 89 of file deadlock.h.

◆ deadlock_summand_list

\brief list of deadlock_summands

Definition at line 81 of file deadlock_summand.h.

◆ deadlock_summand_vector

\brief vector of deadlock_summands

Definition at line 84 of file deadlock_summand.h.

◆ deadlock_vector

typedef std::vector<deadlock> mcrl2::lps::deadlock_vector

\brief vector of deadlocks

Definition at line 92 of file deadlock.h.

◆ multi_action_list

\brief list of multi_actions

Definition at line 109 of file multi_action.h.

◆ multi_action_vector

\brief vector of multi_actions

Definition at line 112 of file multi_action.h.

◆ process_initializer_list

\brief list of process_initializers

Definition at line 77 of file process_initializer.h.

◆ process_initializer_vector

\brief vector of process_initializers

Definition at line 80 of file process_initializer.h.

◆ state

◆ stochastic_action_summand_list

\brief list of stochastic_action_summands

Definition at line 73 of file stochastic_action_summand.h.

◆ stochastic_action_summand_vector

\brief vector of stochastic_action_summands

Definition at line 76 of file stochastic_action_summand.h.

◆ stochastic_distribution_list

\brief list of stochastic_distributions

Definition at line 78 of file stochastic_distribution.h.

◆ stochastic_distribution_vector

\brief vector of stochastic_distributions

Definition at line 81 of file stochastic_distribution.h.

◆ stochastic_process_initializer_list

\brief list of stochastic_process_initializers

Definition at line 60 of file stochastic_process_initializer.h.

◆ stochastic_process_initializer_vector

\brief vector of stochastic_process_initializers

Definition at line 63 of file stochastic_process_initializer.h.

◆ summand_cache_map

Enumeration Type Documentation

◆ caching

enum class mcrl2::lps::caching
strong
Enumerator
none 
local 
global 

Definition at line 38 of file explorer.h.

◆ exploration_strategy

Enumerator
es_none 
es_breadth 
es_depth 
es_random 
es_value_prioritized 
es_value_random_prioritized 
es_highway 

Definition at line 21 of file exploration_strategy.h.

◆ lps_rewriter_type

An enumerated type for the available lps rewriters.

Enumerator
simplify 
quantifier_one_point 
condition_one_point 

Definition at line 23 of file lps_rewriter_type.h.

◆ t_lin_method

The available linearisation methods.

Enumerator
lmStack 
lmRegular 
lmRegular2 

Definition at line 24 of file linearisation_method.h.

Function Documentation

◆ action_rename() [1/2]

lps::stochastic_specification mcrl2::lps::action_rename ( const action_rename_specification action_rename_spec,
const lps::stochastic_specification lps_old_spec,
const data::rewriter rewr,
const bool  enable_rewriting 
)
inline

Rename the actions in a linear specification using a given action_rename_spec.

The actions in a linear specification are renamed according to a given action rename specification. Note that the rules are applied in the order they appear in the specification. This yield quite elaborate conditions in the resulting lps, as a latter rule can only be applied if an earlier rule is not applicable. Note also that there is always a default summand, where the action is not renamed. Using sum elimination and rewriting a substantial reduction of the conditions that are generated can be obtained, often allowing many summands to be removed.

Parameters
action_rename_specThe action_rename_specification to be used.
lps_old_specThe input linear specification.
rewrA data rewriter.
Returns
The lps_old_spec where all actions have been renamed according to action_rename_spec.

Definition at line 442 of file action_rename.h.

◆ action_rename() [2/2]

stochastic_specification mcrl2::lps::action_rename ( const std::regex &  matching_regex,
const std::string &  replacing_fmt,
const stochastic_specification lps_old_spec 
)
inline

Rename actions in given specification based on a regular expression and a string that specifies how the replacement should be formatted.

Definition at line 801 of file action_rename.h.

◆ action_rename_rule_to_aterm()

atermpp::aterm_appl mcrl2::lps::action_rename_rule_to_aterm ( const action_rename_rule rule)
inline

Definition at line 267 of file action_rename.h.

◆ action_rename_specification_to_aterm()

atermpp::aterm_appl mcrl2::lps::action_rename_specification_to_aterm ( const action_rename_specification spec)
inline

Definition at line 273 of file action_rename.h.

◆ action_summand_to_aterm() [1/2]

atermpp::aterm_appl mcrl2::lps::action_summand_to_aterm ( const action_summand s)
inline

Conversion to aterm_appl.

Definition at line 172 of file action_summand.h.

◆ action_summand_to_aterm() [2/2]

atermpp::aterm_appl mcrl2::lps::action_summand_to_aterm ( const stochastic_action_summand s)
inline

Conversion to aterm_appl.

Definition at line 118 of file stochastic_action_summand.h.

◆ apply_parunfold_replacement_builder()

template<template< class > class Builder, template< template< class > class, class, class > class Binder>
parunfold_replacement< Builder, Binder > mcrl2::lps::apply_parunfold_replacement_builder ( const lpsparunfold::case_func_replacement case_funcs,
data::set_identifier_generator id_generator 
)

Definition at line 753 of file lpsparunfoldlib.h.

◆ changed_variables()

std::set< data::variable > mcrl2::lps::changed_variables ( const action_summand summand)
inline

Definition at line 101 of file confluence.h.

◆ check_probability()

void mcrl2::lps::check_probability ( const data::data_expression x,
const data::rewriter rewr 
)
inline

Definition at line 81 of file stochastic_state.h.

◆ check_stochastic_state()

void mcrl2::lps::check_stochastic_state ( const stochastic_state s,
const data::rewriter rewr 
)
inline

Definition at line 103 of file stochastic_state.h.

◆ check_well_typedness() [1/5]

bool mcrl2::lps::check_well_typedness ( const linear_process x)

Definition at line 92 of file lps.cpp.

◆ check_well_typedness() [2/5]

template<typename Object >
bool mcrl2::lps::check_well_typedness ( const Object &  o)

◆ check_well_typedness() [3/5]

bool mcrl2::lps::check_well_typedness ( const specification x)

Definition at line 102 of file lps.cpp.

◆ check_well_typedness() [4/5]

bool mcrl2::lps::check_well_typedness ( const stochastic_linear_process x)

Definition at line 97 of file lps.cpp.

◆ check_well_typedness() [5/5]

bool mcrl2::lps::check_well_typedness ( const stochastic_specification x)

Definition at line 107 of file lps.cpp.

◆ complete_data_specification() [1/2]

void mcrl2::lps::complete_data_specification ( specification spec)
inline

Adds all sorts that appear in the process of l to the data specification of l.

Parameters
specA linear process specification

Definition at line 256 of file specification.h.

◆ complete_data_specification() [2/2]

void mcrl2::lps::complete_data_specification ( stochastic_specification spec)
inline

Adds all sorts that appear in the process of l to the data specification of l.

Parameters
specA linear process specification

Definition at line 104 of file stochastic_specification.h.

◆ constelm()

template<typename DataRewriter , typename Specification >
void mcrl2::lps::constelm ( Specification &  spec,
const DataRewriter &  R,
bool  instantiate_global_variables = false 
)

Removes zero or more constant parameters from the specification spec.

Parameters
specA linear process specification
RA data rewriter
instantiate_global_variablesIf true, free variables may be instantiated as a side effect of the algorithm

Definition at line 264 of file constelm.h.

◆ deadlock_summand_to_aterm()

atermpp::aterm_appl mcrl2::lps::deadlock_summand_to_aterm ( const deadlock_summand s)
inline

Conversion to atermappl.

Returns
The deadlock summand converted to aterm format.

Definition at line 109 of file deadlock_summand.h.

◆ description() [1/3]

std::string mcrl2::lps::description ( const exploration_strategy  strat)
inline

Definition at line 105 of file exploration_strategy.h.

◆ description() [2/3]

std::string mcrl2::lps::description ( const lps_rewriter_type  type)
inline

Returns a description of a lps rewriter.

Definition at line 68 of file lps_rewriter_type.h.

◆ description() [3/3]

std::string mcrl2::lps::description ( const t_lin_method  lin_method)
inline

Definition at line 42 of file linearisation_method.h.

◆ disjoint()

bool mcrl2::lps::disjoint ( const confluence_summand summand1,
const confluence_summand summand2 
)
inline

Indicates whether or not two summands are disjoint.

Definition at line 172 of file confluence.h.

◆ equal_multi_actions()

data::data_expression mcrl2::lps::equal_multi_actions ( const multi_action a,
const multi_action b 
)
inline

Returns a data expression that expresses under which conditions the multi actions a and b are equal. The multi actions may contain free variables.

Parameters
aA sequence of actions
bA sequence of actions
Returns
Necessary conditions for the equality of a and b

Definition at line 311 of file multi_action.h.

◆ find_action_labels() [1/6]

std::set< process::action_label > mcrl2::lps::find_action_labels ( const lps::linear_process x)

Definition at line 62 of file lps.cpp.

◆ find_action_labels() [2/6]

std::set< process::action_label > mcrl2::lps::find_action_labels ( const lps::process_initializer x)

Definition at line 63 of file lps.cpp.

◆ find_action_labels() [3/6]

std::set< process::action_label > mcrl2::lps::find_action_labels ( const lps::specification x)

Definition at line 64 of file lps.cpp.

◆ find_action_labels() [4/6]

std::set< process::action_label > mcrl2::lps::find_action_labels ( const lps::stochastic_specification x)

Definition at line 65 of file lps.cpp.

◆ find_action_labels() [5/6]

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

Returns all action labels that occur in an object.

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

Definition at line 181 of file find.h.

◆ find_action_labels() [6/6]

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

Returns all action labels that occur in an object.

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

Definition at line 172 of file find.h.

◆ find_all_variables() [1/8]

std::set< data::variable > mcrl2::lps::find_all_variables ( const lps::deadlock x)

Definition at line 48 of file lps.cpp.

◆ find_all_variables() [2/8]

std::set< data::variable > mcrl2::lps::find_all_variables ( const lps::linear_process x)

Definition at line 44 of file lps.cpp.

◆ find_all_variables() [3/8]

std::set< data::variable > mcrl2::lps::find_all_variables ( const lps::multi_action x)

Definition at line 49 of file lps.cpp.

◆ find_all_variables() [4/8]

std::set< data::variable > mcrl2::lps::find_all_variables ( const lps::specification x)

Definition at line 46 of file lps.cpp.

◆ find_all_variables() [5/8]

std::set< data::variable > mcrl2::lps::find_all_variables ( const lps::stochastic_linear_process x)

Definition at line 45 of file lps.cpp.

◆ find_all_variables() [6/8]

std::set< data::variable > mcrl2::lps::find_all_variables ( const lps::stochastic_specification x)

Definition at line 47 of file lps.cpp.

◆ find_all_variables() [7/8]

template<typename T >
std::set< data::variable > mcrl2::lps::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 40 of file find.h.

◆ find_all_variables() [8/8]

template<typename T , typename OutputIterator >
void mcrl2::lps::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 31 of file find.h.

◆ find_free_variables() [1/10]

std::set< data::variable > mcrl2::lps::find_free_variables ( const lps::deadlock x)

Definition at line 54 of file lps.cpp.

◆ find_free_variables() [2/10]

std::set< data::variable > mcrl2::lps::find_free_variables ( const lps::linear_process x)

Definition at line 50 of file lps.cpp.

◆ find_free_variables() [3/10]

std::set< data::variable > mcrl2::lps::find_free_variables ( const lps::multi_action x)

Definition at line 55 of file lps.cpp.

◆ find_free_variables() [4/10]

std::set< data::variable > mcrl2::lps::find_free_variables ( const lps::process_initializer x)

Definition at line 56 of file lps.cpp.

◆ find_free_variables() [5/10]

std::set< data::variable > mcrl2::lps::find_free_variables ( const lps::specification x)

Definition at line 52 of file lps.cpp.

◆ find_free_variables() [6/10]

std::set< data::variable > mcrl2::lps::find_free_variables ( const lps::stochastic_linear_process x)

Definition at line 51 of file lps.cpp.

◆ find_free_variables() [7/10]

std::set< data::variable > mcrl2::lps::find_free_variables ( const lps::stochastic_process_initializer x)

Definition at line 57 of file lps.cpp.

◆ find_free_variables() [8/10]

std::set< data::variable > mcrl2::lps::find_free_variables ( const lps::stochastic_specification x)

Definition at line 53 of file lps.cpp.

◆ find_free_variables() [9/10]

template<typename T >
std::set< data::variable > mcrl2::lps::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 72 of file find.h.

◆ find_free_variables() [10/10]

template<typename T , typename OutputIterator >
void mcrl2::lps::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 52 of file find.h.

◆ find_free_variables_with_bound() [1/2]

template<typename T , typename OutputIterator , typename VariableContainer >
void mcrl2::lps::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 63 of file find.h.

◆ find_free_variables_with_bound() [2/2]

template<typename T , typename VariableContainer >
std::set< data::variable > mcrl2::lps::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 84 of file find.h.

◆ find_function_symbols() [1/4]

std::set< data::function_symbol > mcrl2::lps::find_function_symbols ( const lps::specification x)

Definition at line 58 of file lps.cpp.

◆ find_function_symbols() [2/4]

std::set< data::function_symbol > mcrl2::lps::find_function_symbols ( const lps::stochastic_specification x)

Definition at line 59 of file lps.cpp.

◆ find_function_symbols() [3/4]

template<typename T >
std::set< data::function_symbol > mcrl2::lps::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 147 of file find.h.

◆ find_function_symbols() [4/4]

template<typename T , typename OutputIterator >
void mcrl2::lps::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 138 of file find.h.

◆ find_identifiers() [1/4]

std::set< core::identifier_string > mcrl2::lps::find_identifiers ( const lps::specification x)

Definition at line 60 of file lps.cpp.

◆ find_identifiers() [2/4]

std::set< core::identifier_string > mcrl2::lps::find_identifiers ( const lps::stochastic_specification x)

Definition at line 61 of file lps.cpp.

◆ find_identifiers() [3/4]

template<typename T >
std::set< core::identifier_string > mcrl2::lps::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 105 of file find.h.

◆ find_identifiers() [4/4]

template<typename T , typename OutputIterator >
void mcrl2::lps::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 96 of file find.h.

◆ find_representative()

template<typename Node , typename GenerateSuccessors >
Node mcrl2::lps::find_representative ( Node &  u0,
GenerateSuccessors  generate_successors 
)

Search for a unique representative in a graph.

Parameters
u0The root of the graph.
generate_successorsA function that generates successors of a node.

This function is based on an iterative version of Tarjan's strongly connected components algorithm. It returns the smallest node of the first SCC that is detected. The first SCC is a TSCC, meaning that it has no outgoing edges. In a confluent tau graph there is only one TSCC, so this should guarantee a unique representative. N.B. The implementation is based on https://llbit.se/?p=3379

Definition at line 32 of file find_representative.h.

◆ find_sort_expressions() [1/4]

std::set< data::sort_expression > mcrl2::lps::find_sort_expressions ( const lps::specification x)

Definition at line 42 of file lps.cpp.

◆ find_sort_expressions() [2/4]

std::set< data::sort_expression > mcrl2::lps::find_sort_expressions ( const lps::stochastic_specification x)

Definition at line 43 of file lps.cpp.

◆ find_sort_expressions() [3/4]

template<typename T >
std::set< data::sort_expression > mcrl2::lps::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 126 of file find.h.

◆ find_sort_expressions() [4/4]

template<typename T , typename OutputIterator >
void mcrl2::lps::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 117 of file find.h.

◆ finite_sorts()

std::set< data::sort_expression > mcrl2::lps::finite_sorts ( const data::data_specification s)
inline

Return a set with all finite sorts in data specification s.

Definition at line 28 of file suminst.h.

◆ generate_values()

std::vector< std::string > mcrl2::lps::generate_values ( const data::data_specification dataspec,
const data::sort_expression s,
std::size_t  max_size = 1000 
)
inline

Generates possible values of the data type (at most max_size).

Definition at line 41 of file ltsmin.h.

◆ has_ctau_action()

template<typename Specification >
bool mcrl2::lps::has_ctau_action ( const Specification &  lpsspec)

Definition at line 195 of file confluence.h.

◆ if_rewrite() [1/2]

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

Applies the one point rule rewriter to all embedded data expressions in an object x.

Parameters
xan object containing data expressions
Returns
the rewrite result

Definition at line 54 of file if_rewrite.h.

◆ if_rewrite() [2/2]

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

Applies the one point rule rewriter to all embedded data expressions in an object x.

Parameters
xan object containing data expressions

Definition at line 44 of file if_rewrite.h.

◆ initial_distribution() [1/2]

const stochastic_distribution & mcrl2::lps::initial_distribution ( const lps::specification )
inline

Definition at line 256 of file explorer.h.

◆ initial_distribution() [2/2]

const stochastic_distribution & mcrl2::lps::initial_distribution ( const lps::stochastic_specification lpsspec)
inline

Definition at line 263 of file explorer.h.

◆ insert_case_functions() [1/2]

template<typename T >
void mcrl2::lps::insert_case_functions ( T &  x,
const lpsparunfold::case_func_replacement cfv,
data::set_identifier_generator id_generator,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 760 of file lpsparunfoldlib.h.

◆ insert_case_functions() [2/2]

template<typename T >
void mcrl2::lps::insert_case_functions ( T &  x,
const lpsparunfold::case_func_replacement cfv,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Definition at line 770 of file lpsparunfoldlib.h.

◆ is_linear_process()

bool mcrl2::lps::is_linear_process ( const atermpp::aterm_appl x)
inline

Test for a linear_process expression.

Parameters
xA term
Returns
True if x is a linear process expression

Definition at line 266 of file linear_process.h.

◆ is_multi_action()

bool mcrl2::lps::is_multi_action ( const atermpp::aterm_appl x)
inline

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

Definition at line 118 of file multi_action.h.

◆ is_process_initializer()

bool mcrl2::lps::is_process_initializer ( const atermpp::aterm_appl x)
inline

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

Definition at line 86 of file process_initializer.h.

◆ is_specification()

bool mcrl2::lps::is_specification ( const atermpp::aterm_appl x)
inline

Test for a specification expression.

Parameters
xA term
Returns
True if x is a specification expression

Definition at line 44 of file specification.h.

◆ is_stochastic()

template<typename T >
bool mcrl2::lps::is_stochastic ( const T &  x)

Returns true if the LPS object x contains a stochastic distribution in one of its attributes.

Definition at line 50 of file is_stochastic.h.

◆ is_stochastic_distribution()

bool mcrl2::lps::is_stochastic_distribution ( const atermpp::aterm_appl x)
inline

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

Definition at line 87 of file stochastic_distribution.h.

◆ is_stochastic_process_initializer()

bool mcrl2::lps::is_stochastic_process_initializer ( const atermpp::aterm_appl x)
inline

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

Definition at line 69 of file stochastic_process_initializer.h.

◆ linear_process_specification_marker()

atermpp::aterm mcrl2::lps::linear_process_specification_marker ( )

Definition at line 18 of file lps_io.cpp.

◆ linear_process_to_aterm()

template<typename ActionSummand >
atermpp::aterm_appl mcrl2::lps::linear_process_to_aterm ( const linear_process_base< ActionSummand > &  p)

Conversion to aterm_appl.

Returns
The action summand converted to aterm format.

Definition at line 227 of file linear_process.h.

◆ linearise() [1/2]

mcrl2::lps::stochastic_specification mcrl2::lps::linearise ( const mcrl2::process::process_specification type_checked_spec,
mcrl2::lps::t_lin_options  lin_options = t_lin_options() 
)

Linearises a process specification.

Parameters
[in]type_checked_specA process specification
[in]lin_optionsoptions that should be used during linearisation
Returns
An LPS equivalent to spec, which is linearised using lin_options
Exceptions
mcrl2::runtime_errorLinearisation failed

Definition at line 11250 of file linearise.cpp.

◆ linearise() [2/2]

mcrl2::lps::stochastic_specification mcrl2::lps::linearise ( const std::string &  text,
mcrl2::lps::t_lin_options  lin_options = t_lin_options() 
)
inline

Linearises a process specification from a textual specification.

Parameters
[in]textA string containing a process specification
[in]lin_optionsoptions that should be used during linearisation
Returns
An LPS equivalent to the specification representing text, which is linearised using lin_options
Exceptions
mcrl2::runtime_errorLinearisation failed

Definition at line 79 of file linearise.h.

◆ load_lps() [1/2]

template<typename Specification >
void mcrl2::lps::load_lps ( Specification &  spec,
const std::string &  filename 
)

Load LPS from file.

Parameters
specThe LPS to which the result is loaded.
filenameThe file from which to load the LPS. If empty, the file is read from stdin.

Definition at line 85 of file io.h.

◆ load_lps() [2/2]

template<typename Specification >
void mcrl2::lps::load_lps ( Specification &  spec,
std::istream &  stream,
const std::string &  source = "" 
)

Load LPS from file.

Parameters
specThe LPS to which the result is loaded.
streamThe stream from which to load the LPS (it is assumed to have been opened in the right mode).
sourceThe source from which the stream originates. Used for error messages.

Definition at line 54 of file io.h.

◆ lpsbinary()

void mcrl2::lps::lpsbinary ( const std::string &  input_filename,
const std::string &  output_filename,
const std::string &  parameter_selection 
)

Definition at line 31 of file tools.cpp.

◆ lpsconstelm()

void mcrl2::lps::lpsconstelm ( const std::string &  input_filename,
const std::string &  output_filename,
data::rewriter::strategy  rewrite_strategy,
bool  instantiate_free_variables,
bool  ignore_conditions,
bool  remove_trivial_summands,
bool  remove_singleton_sorts 
)

Definition at line 43 of file tools.cpp.

◆ lpsinfo()

void mcrl2::lps::lpsinfo ( const std::string &  input_filename,
const std::string &  input_file_message 
)

Definition at line 75 of file tools.cpp.

◆ lpsinvelm()

bool mcrl2::lps::lpsinvelm ( const std::string &  input_filename,
const std::string &  output_filename,
const std::string &  invariant_filename,
const std::string &  dot_file_name,
data::rewriter::strategy  rewrite_strategy,
data::detail::smt_solver_type  solver_type,
const bool  no_check,
const bool  no_elimination,
const bool  simplify_all,
const bool  all_violations,
const bool  counter_example,
const bool  path_eliminator,
const bool  apply_induction,
const int  time_limit 
)

Definition at line 86 of file tools.cpp.

◆ lpsparelm()

void mcrl2::lps::lpsparelm ( const std::string &  input_filename,
const std::string &  output_filename 
)

Definition at line 161 of file tools.cpp.

◆ lpspp()

void mcrl2::lps::lpspp ( const std::string &  input_filename,
const std::string &  output_filename,
bool  print_summand_numbers,
core::print_format_type  format 
)

Definition at line 171 of file tools.cpp.

◆ lpsrewr()

void mcrl2::lps::lpsrewr ( const std::string &  input_filename,
const std::string &  output_filename,
const data::rewriter::strategy  rewrite_strategy,
const lps::lps_rewriter_type  rewriter_type 
)

Definition at line 213 of file tools.cpp.

◆ lpssumelm()

void mcrl2::lps::lpssumelm ( const std::string &  input_filename,
const std::string &  output_filename,
const bool  decluster 
)

Definition at line 246 of file tools.cpp.

◆ lpssuminst()

void mcrl2::lps::lpssuminst ( const std::string &  input_filename,
const std::string &  output_filename,
const data::rewriter::strategy  rewrite_strategy,
const std::string &  sorts_string,
const bool  finite_sorts_only,
const bool  tau_summands_only 
)

Definition at line 259 of file tools.cpp.

◆ lpsuntime()

void mcrl2::lps::lpsuntime ( const std::string &  input_filename,
const std::string &  output_filename,
const bool  add_invariants,
const bool  apply_fourier_motzkin,
const data::rewriter::strategy  rewrite_strategy 
)

Definition at line 296 of file tools.cpp.

◆ make_assignment_list()

data::assignment_list mcrl2::lps::make_assignment_list ( const data::variable_list variables,
const data::data_expression_list expressions 
)
inline

Definition at line 113 of file confluence.h.

◆ make_ctau_act_id()

process::action_label mcrl2::lps::make_ctau_act_id ( )
inline

Creates an identifier for the ctau action.

Definition at line 181 of file confluence.h.

◆ make_ctau_action()

process::action mcrl2::lps::make_ctau_action ( )
inline

Creates the ctau action.

Definition at line 188 of file confluence.h.

◆ make_data_expression_vector()

std::vector< data::data_expression > mcrl2::lps::make_data_expression_vector ( const data::data_expression_list v)
inline

Definition at line 54 of file explorer.h.

◆ make_multi_action()

template<class... ARGUMENTS>
void mcrl2::lps::make_multi_action ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

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

Parameters
tThe reference into which the new multi_action is constructed.

Definition at line 103 of file multi_action.h.

◆ make_process_initializer()

template<class EXPRESSION_LIST >
void mcrl2::lps::make_process_initializer ( atermpp::aterm_appl t,
EXPRESSION_LIST  args 
)
inline

Definition at line 69 of file process_initializer.h.

◆ make_state() [1/2]

template<class ForwardTraversalIterator >
void mcrl2::lps::make_state ( state result,
ForwardTraversalIterator  p,
const std::size_t  size 
)

Definition at line 37 of file state.h.

◆ make_state() [2/2]

template<class ForwardTraversalIterator , class Transformer >
void mcrl2::lps::make_state ( state result,
ForwardTraversalIterator  p,
const std::size_t  size,
Transformer  transformer 
)

Definition at line 27 of file state.h.

◆ make_stochastic_distribution()

template<class... ARGUMENTS>
void mcrl2::lps::make_stochastic_distribution ( atermpp::aterm_appl t,
const ARGUMENTS &...  args 
)
inline

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

Parameters
tThe reference into which the new stochastic_distribution is constructed.

Definition at line 72 of file stochastic_distribution.h.

◆ make_stochastic_process_initializer()

template<class... ARGUMENTS>
void mcrl2::lps::make_stochastic_process_initializer ( atermpp::aterm_appl t,
ARGUMENTS...  args 
)
inline

Definition at line 52 of file stochastic_process_initializer.h.

◆ normalize_sorts() [1/5]

lps::multi_action mcrl2::lps::normalize_sorts ( const multi_action x,
const data::sort_specification sortspec 
)

Definition at line 38 of file lps.cpp.

◆ normalize_sorts() [2/5]

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

Definition at line 34 of file normalize_sorts.h.

◆ normalize_sorts() [3/5]

void mcrl2::lps::normalize_sorts ( lps::specification x,
const data::sort_specification sortspec 
)

Definition at line 39 of file lps.cpp.

◆ normalize_sorts() [4/5]

void mcrl2::lps::normalize_sorts ( lps::stochastic_specification x,
const data::sort_specification sortspec 
)

Definition at line 40 of file lps.cpp.

◆ normalize_sorts() [5/5]

template<typename T >
void mcrl2::lps::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.

◆ not_equal_multi_actions()

data::data_expression mcrl2::lps::not_equal_multi_actions ( const multi_action a,
const multi_action b 
)
inline

Returns a pbes expression that expresses under which conditions the multi actions a and b are not equal. The multi actions may contain free variables.

Parameters
aA sequence of actions
bA sequence of actions
Returns
Necessary conditions for the inequality of a and b

Definition at line 359 of file multi_action.h.

◆ nr_of_booleans_for_elements()

std::size_t mcrl2::lps::nr_of_booleans_for_elements ( std::size_t  n)
inline

Definition at line 27 of file binary.h.

◆ one_point_condition_rewrite() [1/2]

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

Applies the one point condition rewriter to all embedded data expressions in an object x.

Parameters
xan object containing data expressions
Returns
the rewrite result

Definition at line 175 of file one_point_condition_rewrite.h.

◆ one_point_condition_rewrite() [2/2]

template<typename T , typename DataRewriter >
void mcrl2::lps::one_point_condition_rewrite ( T &  x,
const DataRewriter &  R,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Applies the one point condition rewriter to all embedded data expressions in an object x.

Parameters
xan object containing data expressions

Definition at line 165 of file one_point_condition_rewrite.h.

◆ one_point_rule_rewrite() [1/2]

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

Applies the one point rule rewriter to all embedded data expressions in an object x.

Parameters
xan object containing data expressions
Returns
the rewrite result

Definition at line 56 of file one_point_rule_rewrite.h.

◆ one_point_rule_rewrite() [2/2]

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

Applies the one point rule rewriter to all embedded data expressions in an object x.

Parameters
xan object containing data expressions

Definition at line 46 of file one_point_rule_rewrite.h.

◆ operator!=() [1/2]

bool mcrl2::lps::operator!= ( const specification spec1,
const specification spec2 
)
inline

Inequality operator.

Definition at line 248 of file specification.h.

◆ operator!=() [2/2]

bool mcrl2::lps::operator!= ( const stochastic_specification spec1,
const stochastic_specification spec2 
)
inline

Inequality operator.

Definition at line 94 of file stochastic_specification.h.

◆ operator<() [1/2]

bool mcrl2::lps::operator< ( const action_summand x,
const action_summand y 
)
inline

Comparison operator for action summands.

Definition at line 143 of file action_summand.h.

◆ operator<() [2/2]

bool mcrl2::lps::operator< ( const stochastic_action_summand x,
const stochastic_action_summand y 
)
inline

Comparison operator for action summands.

Definition at line 100 of file stochastic_action_summand.h.

◆ operator<<() [1/25]

atermpp::aterm_ostream & mcrl2::lps::operator<< ( atermpp::aterm_ostream stream,
const deadlock_summand summand 
)

Definition at line 42 of file lps_io.cpp.

◆ operator<<() [2/25]

template<typename ActionSummand >
atermpp::aterm_ostream & mcrl2::lps::operator<< ( atermpp::aterm_ostream stream,
const linear_process_base< ActionSummand > &  lps 
)

Definition at line 97 of file lps_io.cpp.

◆ operator<<() [3/25]

atermpp::aterm_ostream & mcrl2::lps::operator<< ( atermpp::aterm_ostream stream,
const multi_action action 
)

Definition at line 23 of file lps_io.cpp.

◆ operator<<() [4/25]

atermpp::aterm_ostream & mcrl2::lps::operator<< ( atermpp::aterm_ostream stream,
const specification spec 
)

Writes LPS to the stream.

Definition at line 171 of file lps_io.cpp.

◆ operator<<() [5/25]

atermpp::aterm_ostream & mcrl2::lps::operator<< ( atermpp::aterm_ostream stream,
const stochastic_action_summand summand 
)

Definition at line 64 of file lps_io.cpp.

◆ operator<<() [6/25]

atermpp::aterm_ostream & mcrl2::lps::operator<< ( atermpp::aterm_ostream stream,
const stochastic_specification spec 
)

Definition at line 177 of file lps_io.cpp.

◆ operator<<() [7/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  os,
caching  c 
)
inline

Definition at line 41 of file explorer.h.

◆ operator<<() [8/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  os,
const exploration_strategy  strat 
)
inline

Definition at line 99 of file exploration_strategy.h.

◆ operator<<() [9/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  os,
const lps_rewriter_type  t 
)
inline

Definition at line 103 of file lps_rewriter_type.h.

◆ operator<<() [10/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  os,
const t_lin_method  l 
)
inline

Definition at line 96 of file linearisation_method.h.

◆ operator<<() [11/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const action_summand 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 129 of file action_summand.h.

◆ operator<<() [12/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const deadlock 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 102 of file deadlock.h.

◆ operator<<() [13/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const deadlock_summand 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 94 of file deadlock_summand.h.

◆ operator<<() [14/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const explorer_options options 
)
inline

Definition at line 75 of file explorer_options.h.

◆ operator<<() [15/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const explorer_summand summand 
)
inline

Definition at line 429 of file explorer.h.

◆ operator<<() [16/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const linear_process 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 256 of file linear_process.h.

◆ operator<<() [17/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const multi_action 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 131 of file multi_action.h.

◆ operator<<() [18/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const probabilistic_data_expression x 
)
inline

Pretty print to an outstream.

Definition at line 228 of file probabilistic_data_expression.h.

◆ operator<<() [19/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const process_initializer 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 99 of file process_initializer.h.

◆ operator<<() [20/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const specification x 
)
inline

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

Definition at line 209 of file specification.h.

◆ operator<<() [21/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const stochastic_action_summand 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 86 of file stochastic_action_summand.h.

◆ operator<<() [22/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const stochastic_distribution 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 100 of file stochastic_distribution.h.

◆ operator<<() [23/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const stochastic_linear_process 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 88 of file stochastic_linear_process.h.

◆ operator<<() [24/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const stochastic_process_initializer 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 82 of file stochastic_process_initializer.h.

◆ operator<<() [25/25]

std::ostream & mcrl2::lps::operator<< ( std::ostream &  out,
const stochastic_specification x 
)
inline

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

Definition at line 80 of file stochastic_specification.h.

◆ operator==() [1/4]

bool mcrl2::lps::operator== ( const action_summand x,
const action_summand y 
)
inline

Equality operator of action summands.

Definition at line 162 of file action_summand.h.

◆ operator==() [2/4]

bool mcrl2::lps::operator== ( const specification spec1,
const specification spec2 
)
inline

Equality operator.

Definition at line 241 of file specification.h.

◆ operator==() [3/4]

bool mcrl2::lps::operator== ( const stochastic_action_summand x,
const stochastic_action_summand y 
)
inline

Equality operator of stochastic action summands.

Definition at line 111 of file stochastic_action_summand.h.

◆ operator==() [4/4]

bool mcrl2::lps::operator== ( const stochastic_specification spec1,
const stochastic_specification spec2 
)
inline

Definition at line 87 of file stochastic_specification.h.

◆ operator>>() [1/9]

atermpp::aterm_istream & mcrl2::lps::operator>> ( atermpp::aterm_istream stream,
deadlock_summand summand 
)

Definition at line 50 of file lps_io.cpp.

◆ operator>>() [2/9]

template<typename ActionSummand >
atermpp::aterm_istream & mcrl2::lps::operator>> ( atermpp::aterm_istream stream,
linear_process_base< ActionSummand > &  lps 
)

Definition at line 107 of file lps_io.cpp.

◆ operator>>() [3/9]

atermpp::aterm_istream & mcrl2::lps::operator>> ( atermpp::aterm_istream stream,
multi_action action 
)

Definition at line 30 of file lps_io.cpp.

◆ operator>>() [4/9]

atermpp::aterm_istream & mcrl2::lps::operator>> ( atermpp::aterm_istream stream,
lps::specification spec 
)

Reads LPS from the stream.

Definition at line 183 of file lps_io.cpp.

◆ operator>>() [5/9]

atermpp::aterm_istream & mcrl2::lps::operator>> ( atermpp::aterm_istream stream,
stochastic_action_summand summand 
)

Definition at line 74 of file lps_io.cpp.

◆ operator>>() [6/9]

atermpp::aterm_istream & mcrl2::lps::operator>> ( atermpp::aterm_istream stream,
lps::stochastic_specification spec 
)

Definition at line 191 of file lps_io.cpp.

◆ operator>>() [7/9]

std::istream & mcrl2::lps::operator>> ( std::istream &  is,
exploration_strategy strat 
)
inline

Definition at line 83 of file exploration_strategy.h.

◆ operator>>() [8/9]

std::istream & mcrl2::lps::operator>> ( std::istream &  is,
lps_rewriter_type t 
)
inline

Stream operator for rewriter type.

Parameters
isAn input stream
tA rewriter type
Returns
The input stream

Definition at line 87 of file lps_rewriter_type.h.

◆ operator>>() [9/9]

std::istream & mcrl2::lps::operator>> ( std::istream &  is,
t_lin_method l 
)
inline

Definition at line 79 of file linearisation_method.h.

◆ order_summand_variables()

template<typename Specification >
void mcrl2::lps::order_summand_variables ( Specification &  lpsspec)

Order summand variables to make enumeration over these variables more efficient.

Definition at line 23 of file order_summand_variables.h.

◆ parelm()

template<typename Specification >
void mcrl2::lps::parelm ( Specification &  spec,
bool  variant1 = true 
)

Removes unused parameters from a linear process specification.

Parameters
specA linear process specification
variant1If true the default variant of parelm is used, otherwise an alternative implementation is chosen.

Definition at line 273 of file parelm.h.

◆ parse_action()

process::action mcrl2::lps::parse_action ( const std::string &  text,
const process::action_label_list action_decls,
const data::data_specification data_spec = data::detail::default_specification() 
)
inline

Parses an action from a string.

Parameters
textA string containing an action
action_declsAn action declaration
[in]data_specA data specification used for sort normalization
Returns
An action
Exceptions
mcrl2::runtime_errorwhen the input does not match the syntax of an action.

Definition at line 211 of file parse.h.

◆ parse_action_rename_specification() [1/2]

action_rename_specification mcrl2::lps::parse_action_rename_specification ( const std::string &  spec_string,
const lps::stochastic_specification spec 
)
inline

Parses an action rename specification. Parses an acion rename specification. If the action rename specification contains data types that are not present in the data specification of spec they are added to it.

Parameters
spec_stringA string containing an action rename specification.
specA linear process specification
Returns
An action rename specification

Definition at line 110 of file parse.h.

◆ parse_action_rename_specification() [2/2]

action_rename_specification mcrl2::lps::parse_action_rename_specification ( std::istream &  in,
const lps::stochastic_specification spec 
)
inline

Parses a process specification from an input stream.

Parameters
inAn input stream
specA linear process specification.
Returns
The parse result

Definition at line 94 of file parse.h.

◆ parse_exploration_strategy()

exploration_strategy mcrl2::lps::parse_exploration_strategy ( const std::string &  s)
inline

Definition at line 31 of file exploration_strategy.h.

◆ parse_lin_method()

t_lin_method mcrl2::lps::parse_lin_method ( const std::string &  s)
inline

Parse a linearisation method.

Parameters
[in]sA string
Returns
The linearisation method represented by s

Definition at line 57 of file linearisation_method.h.

◆ parse_linear_process_specification() [1/2]

specification mcrl2::lps::parse_linear_process_specification ( const std::string &  text)
inline

Parses a linear process specification from a string.

Parameters
textA string containing a linear process specification
Returns
The parsed specification
Exceptions
non_linear_processif a non-linear sub-expression is encountered.
mcrl2::runtime_errorin the following cases:
  • The number of equations is not equal to one
  • The initial process is not a process instance, or it does not match with the equation
  • A sequential process is found with a right hand side that is not a process instance, or it doesn't match the equation

Definition at line 152 of file parse.h.

◆ parse_linear_process_specification() [2/2]

specification mcrl2::lps::parse_linear_process_specification ( std::istream &  spec_stream)
inline

Parses a linear process specification from an input stream.

Parameters
spec_streamAn input stream containing a linear process specification
Returns
The parsed specification
Exceptions
non_linear_processif a non-linear sub-expression is encountered.
mcrl2::runtime_errorin the following cases:
  • The number of equations is not equal to one
  • The initial process is not a process instance, or it does not match with the equation
  • A sequential process is found with a right hand side that is not a process instance, or it doesn't match the equation

Definition at line 128 of file parse.h.

◆ parse_lps() [1/2]

template<typename Specification >
void mcrl2::lps::parse_lps ( const std::string &  text,
Specification &  result 
)

Definition at line 197 of file parse.h.

◆ parse_lps() [2/2]

template<typename Specification >
void mcrl2::lps::parse_lps ( std::istream &  ,
Specification &   
)

Definition at line 159 of file parse.h.

◆ parse_lps< specification >()

template<>
void mcrl2::lps::parse_lps< specification > ( std::istream &  from,
specification result 
)
inline

Definition at line 166 of file parse.h.

◆ parse_lps< stochastic_specification >()

template<>
void mcrl2::lps::parse_lps< stochastic_specification > ( std::istream &  from,
stochastic_specification result 
)
inline

Parses a stochastic linear process specification from an input stream.

Parameters
fromAn input stream containing a linear process specification.
resultAn output parameter in which the parsed stochastic process is put.
Returns
The parsed specification.
Exceptions
non_linear_processif a non-linear sub-expression is encountered.
mcrl2::runtime_errorin the following cases:
  • The number of equations is not equal to one.
  • The initial process is not a process instance, or it does not match with the equation.
  • A sequential process is found with a right hand side that is not a process instance, or it doesn't match the equation.

Definition at line 183 of file parse.h.

◆ parse_lps_rewriter_type()

lps_rewriter_type mcrl2::lps::parse_lps_rewriter_type ( const std::string &  type)
inline

Parses a lps rewriter type.

Definition at line 32 of file lps_rewriter_type.h.

◆ parse_multi_action() [1/4]

multi_action mcrl2::lps::parse_multi_action ( const std::string &  text,
const process::action_label_list action_decls,
const data::data_specification data_spec = data::detail::default_specification() 
)
inline

Parses a multi_action from a string.

Parameters
textA string containing a multi_action
[in]action_declsA list of allowed action labels that is used for type checking.
[in]data_specThe data specification that is used for type checking.
Returns
The parsed multi_action
Exceptions
mcrl2::runtime_errorwhen the input does not match the syntax of a multi action.

Definition at line 70 of file parse.h.

◆ parse_multi_action() [2/4]

multi_action mcrl2::lps::parse_multi_action ( const std::string &  text,
multi_action_type_checker typechecker,
const data::data_specification data_spec = data::detail::default_specification() 
)
inline

Parses a multi_action from a string.

Parameters
textA string containing a multi_action
[in]typecheckerTypechecker used to check the action.
[in]data_specThe data specification that is used for type checking.
Returns
The parsed multi_action
Exceptions
mcrl2::runtime_errorwhen the input does not match the syntax of a multi action.

Definition at line 83 of file parse.h.

◆ parse_multi_action() [3/4]

multi_action mcrl2::lps::parse_multi_action ( std::stringstream &  in,
const process::action_label_list action_decls,
const data::data_specification data_spec = data::detail::default_specification() 
)
inline

Parses a multi_action from an input stream.

Parameters
inAn input stream containing a multi_action
[in]action_declsA list of allowed action labels that is used for type checking.
[in]data_specThe data specification that is used for type checking.
Returns
The parsed multi_action
Exceptions
mcrl2::runtime_errorwhen the input does not match the syntax of a multi action.

Definition at line 42 of file parse.h.

◆ parse_multi_action() [4/4]

multi_action mcrl2::lps::parse_multi_action ( std::stringstream &  in,
multi_action_type_checker typechecker,
const data::data_specification data_spec = data::detail::default_specification() 
)
inline

Parses a multi_action from an input stream.

Parameters
inAn input stream containing a multi_action
[in]typecheckerTypechecker used to check the action.
[in]data_specThe data specification that is used for type checking.
Returns
The parsed multi_action
Exceptions
mcrl2::runtime_errorwhen the input does not match the syntax of a multi action.

Definition at line 56 of file parse.h.

◆ pp() [1/15]

std::string mcrl2::lps::pp ( const action_summand x)

Definition at line 26 of file lps.cpp.

◆ pp() [2/15]

std::string mcrl2::lps::pp ( const deadlock x)

Definition at line 27 of file lps.cpp.

◆ pp() [3/15]

std::string mcrl2::lps::pp ( const deadlock_summand x)

Definition at line 28 of file lps.cpp.

◆ pp() [4/15]

std::string mcrl2::lps::pp ( const linear_process x)

Definition at line 29 of file lps.cpp.

◆ pp() [5/15]

std::string mcrl2::lps::pp ( const lps::state x)
inline

Definition at line 49 of file state.h.

◆ pp() [6/15]

std::string mcrl2::lps::pp ( const multi_action x)

Definition at line 30 of file lps.cpp.

◆ pp() [7/15]

std::string mcrl2::lps::pp ( const probabilistic_data_expression l)
inline

Definition at line 220 of file probabilistic_data_expression.h.

◆ pp() [8/15]

std::string mcrl2::lps::pp ( const process_initializer x)

Definition at line 31 of file lps.cpp.

◆ pp() [9/15]

std::string mcrl2::lps::pp ( const specification x)

Definition at line 32 of file lps.cpp.

◆ pp() [10/15]

std::string mcrl2::lps::pp ( const stochastic_action_summand x)

Definition at line 33 of file lps.cpp.

◆ pp() [11/15]

std::string mcrl2::lps::pp ( const stochastic_distribution x)

Definition at line 34 of file lps.cpp.

◆ pp() [12/15]

std::string mcrl2::lps::pp ( const stochastic_linear_process x)

Definition at line 35 of file lps.cpp.

◆ pp() [13/15]

std::string mcrl2::lps::pp ( const stochastic_process_initializer x)

Definition at line 36 of file lps.cpp.

◆ pp() [14/15]

std::string mcrl2::lps::pp ( const stochastic_specification x)

Definition at line 37 of file lps.cpp.

◆ pp() [15/15]

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

Returns a string representation of the object x.

Definition at line 331 of file print.h.

◆ pp_with_summand_numbers() [1/2]

std::string mcrl2::lps::pp_with_summand_numbers ( const specification x)

Definition at line 74 of file lps.cpp.

◆ pp_with_summand_numbers() [2/2]

std::string mcrl2::lps::pp_with_summand_numbers ( const stochastic_specification x)

Definition at line 83 of file lps.cpp.

◆ print_confluence_summand()

std::string mcrl2::lps::print_confluence_summand ( const confluence_summand summand,
const data::variable_list process_parameters 
)
inline

Definition at line 157 of file confluence.h.

◆ print_exploration_strategy()

std::string mcrl2::lps::print_exploration_strategy ( const exploration_strategy  es)
inline

Definition at line 61 of file exploration_strategy.h.

◆ print_lin_method()

std::string mcrl2::lps::print_lin_method ( const t_lin_method  lin_method)
inline

String representation of a linearisation method.

Parameters
[in]lin_methodA linerisation method
Returns
String representation of lin_method

Definition at line 30 of file linearisation_method.h.

◆ print_lps_rewriter_type()

std::string mcrl2::lps::print_lps_rewriter_type ( const lps_rewriter_type  type)
inline

Prints a lps rewriter type.

Definition at line 51 of file lps_rewriter_type.h.

◆ print_probability()

std::string mcrl2::lps::print_probability ( const data::data_expression x)
inline

Definition at line 74 of file stochastic_state.h.

◆ read_spec()

static void mcrl2::lps::read_spec ( atermpp::aterm_istream stream,
stochastic_specification spec 
)
static

Definition at line 136 of file lps_io.cpp.

◆ remove_parameters()

template<typename Object >
void mcrl2::lps::remove_parameters ( Object &  x,
const std::set< data::variable > &  to_be_removed 
)

Rewrites an LPS data type.

Definition at line 190 of file remove.h.

◆ remove_redundant_assignments() [1/2]

data::assignment_list mcrl2::lps::remove_redundant_assignments ( const data::assignment_list assignments,
const data::variable_list do_not_remove 
)
inline

Removes assignments of the form x := x from v for variables x that are not contained in do_not_remove.

Definition at line 229 of file remove.h.

◆ remove_redundant_assignments() [2/2]

template<typename Specification >
void mcrl2::lps::remove_redundant_assignments ( Specification &  lpsspec)

Removes redundant assignments of the form x = x from an LPS specification.

Parameters
lpsspecA linear process specification

Definition at line 247 of file remove.h.

◆ remove_singleton_sorts()

template<typename Specification >
void mcrl2::lps::remove_singleton_sorts ( Specification &  spec)

Removes parameters with a singleton sort from a linear process specification.

Parameters
specA linear process specification

Definition at line 211 of file remove.h.

◆ remove_stochastic_operators()

specification mcrl2::lps::remove_stochastic_operators ( const stochastic_specification spec)
inline

Converts a stochastic specification to a specification. Throws an exception if non-empty distributions are encountered.

Definition at line 113 of file stochastic_specification.h.

◆ remove_trivial_summands()

template<typename Specification >
void mcrl2::lps::remove_trivial_summands ( Specification &  spec)

Removes summands with condition equal to false from a linear process specification.

Parameters
specA linear process specification

Definition at line 199 of file remove.h.

◆ replace_constants_by_variables() [1/2]

template<typename T >
T mcrl2::lps::replace_constants_by_variables ( const T &  x,
const data::rewriter r,
data::mutable_indexed_substitution<> &  sigma,
typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Replace each constant data application c in x by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times.

Definition at line 55 of file replace_constants_by_variables.h.

◆ replace_constants_by_variables() [2/2]

template<typename T >
void mcrl2::lps::replace_constants_by_variables ( T &  x,
const data::rewriter r,
data::mutable_indexed_substitution<> &  sigma,
typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *  = nullptr 
)

Replace each constant data application c in x by a fresh variable v, and add extend the substitution sigma with the assignment v := r(c). This can be used in rewriting, to avoid that c is rewritten by the rewriter multiple times.

Definition at line 41 of file replace_constants_by_variables.h.

◆ replace_variables_capture_avoiding() [1/6]

template<typename Substitution >
stochastic_distribution mcrl2::lps::replace_variables_capture_avoiding ( const stochastic_distribution x,
data::data_expression_list pars,
Substitution &  sigma 
)

\brief Applies sigma as a capture avoiding substitution to a stochastic_distribution and a list of parameters. \param x The object to which the substiution is applied. \param pars The parameters of which the variables are bound. This list is changed if necessary. \param sigma A substitution.

Definition at line 277 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding() [2/6]

template<typename Substitution >
stochastic_distribution mcrl2::lps::replace_variables_capture_avoiding ( const stochastic_distribution x,
data::data_expression_list pars,
Substitution &  sigma,
data::set_identifier_generator id_generator 
)

\brief Applies sigma as a capture avoiding substitution to x with x a distribution.. \details The capture avoiding substitution must also be applied to the expression to which the distribution is applied. \param x The object to which the substiution is applied. \param pars The parameter list to which the distribution 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 259 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding() [3/6]

template<typename T , typename Substitution >
T mcrl2::lps::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 203 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding() [4/6]

template<typename T , typename Substitution >
T mcrl2::lps::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 237 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding() [5/6]

template<typename T , typename Substitution >
void mcrl2::lps::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 188 of file replace_capture_avoiding.h.

◆ replace_variables_capture_avoiding() [6/6]

template<typename T , typename Substitution >
void mcrl2::lps::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 219 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::lps::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 158 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::lps::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 139 of file replace_capture_avoiding_with_an_identifier_generator.h.

◆ resolve_summand_variable_name_clashes()

template<typename Specification >
void mcrl2::lps::resolve_summand_variable_name_clashes ( Specification &  spec)

Renames summand variables such that there are no name clashes between summand variables and process parameters.

Definition at line 136 of file resolve_name_clashes.h.

◆ rewrite() [1/4]

template<typename T , typename Rewriter , typename Substitution >
T mcrl2::lps::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 70 of file rewrite.h.

◆ rewrite() [2/4]

template<typename T , typename Rewriter >
T mcrl2::lps::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 40 of file rewrite.h.

◆ rewrite() [3/4]

template<typename T , typename Rewriter , typename Substitution >
void mcrl2::lps::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 55 of file rewrite.h.

◆ rewrite() [4/4]

template<typename T , typename Rewriter >
void mcrl2::lps::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 27 of file rewrite.h.

◆ save_lps() [1/2]

template<typename Specification >
void mcrl2::lps::save_lps ( const Specification &  spec,
const std::string &  filename 
)

Saves an LPS to a file.

Parameters
specThe LPS to save.
filenameThe file to save the LPS in. If empty, the file is written to stdout.

Definition at line 64 of file io.h.

◆ save_lps() [2/2]

template<typename Specification >
void mcrl2::lps::save_lps ( const Specification &  spec,
std::ostream &  stream,
const std::string &  target = "" 
)

Save an LPS in the format specified.

Parameters
specThe LPS to be stored
streamThe stream to which the output is written.
targetA string indicating the target stream, used to print information. utilities::file_format::unknown() is specified, then a default format is chosen.

Definition at line 42 of file io.h.

◆ search_free_variable()

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

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

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

Definition at line 160 of file find.h.

◆ specification_to_aterm()

template<typename LinearProcess , typename InitialProcessExpression >
atermpp::aterm_appl mcrl2::lps::specification_to_aterm ( const specification_base< LinearProcess, InitialProcessExpression > &  spec)

Conversion to aterm_appl.

Returns
The specification converted to aterm format.

Definition at line 228 of file specification.h.

◆ sumelm() [1/3]

bool mcrl2::lps::sumelm ( action_summand s)
inline

Apply the sum elimination lemma to summand s.

Parameters
san action summand
Returns
true if any summation variables have been removed, or false otherwise.

Definition at line 114 of file sumelm.h.

◆ sumelm() [2/3]

bool mcrl2::lps::sumelm ( deadlock_summand s)
inline

Apply the sum elimination lemma to summand s.

Parameters
sa deadlock summand
Returns
true if any summation variables have been removed, or false otherwise.

Definition at line 138 of file sumelm.h.

◆ sumelm() [3/3]

bool mcrl2::lps::sumelm ( stochastic_action_summand s)
inline

Apply the sum elimination lemma to summand s.

Parameters
sa stochastic action summand
Returns
true if any summation variables have been removed, or false otherwise.

Definition at line 126 of file sumelm.h.

◆ summand_distribution() [1/3]

template<>
const stochastic_distribution & mcrl2::lps::summand_distribution ( const lps::stochastic_action_summand summand)

Definition at line 79 of file confluence.h.

◆ summand_distribution() [2/3]

template<>
const stochastic_distribution & mcrl2::lps::summand_distribution ( const lps::stochastic_action_summand summand)
inline

Definition at line 250 of file explorer.h.

◆ summand_distribution() [3/3]

template<typename Summand >
const stochastic_distribution & mcrl2::lps::summand_distribution ( const Summand &  )
inline

Definition at line 71 of file confluence.h.

◆ swap() [1/8]

void mcrl2::lps::swap ( action_summand t1,
action_summand t2 
)
inline

\brief swap overload

Definition at line 135 of file action_summand.h.

◆ swap() [2/8]

void mcrl2::lps::swap ( deadlock t1,
deadlock t2 
)
inline

\brief swap overload

Definition at line 108 of file deadlock.h.

◆ swap() [3/8]

void mcrl2::lps::swap ( deadlock_summand t1,
deadlock_summand t2 
)
inline

\brief swap overload

Definition at line 100 of file deadlock_summand.h.

◆ swap() [4/8]

void mcrl2::lps::swap ( multi_action t1,
multi_action t2 
)
inline

\brief swap overload

Definition at line 137 of file multi_action.h.

◆ swap() [5/8]

void mcrl2::lps::swap ( process_initializer t1,
process_initializer t2 
)
inline

\brief swap overload

Definition at line 105 of file process_initializer.h.

◆ swap() [6/8]

void mcrl2::lps::swap ( stochastic_action_summand t1,
stochastic_action_summand t2 
)
inline

\brief swap overload

Definition at line 92 of file stochastic_action_summand.h.

◆ swap() [7/8]

void mcrl2::lps::swap ( stochastic_distribution t1,
stochastic_distribution t2 
)
inline

\brief swap overload

Definition at line 106 of file stochastic_distribution.h.

◆ swap() [8/8]

void mcrl2::lps::swap ( stochastic_process_initializer t1,
stochastic_process_initializer t2 
)
inline

\brief swap overload

Definition at line 88 of file stochastic_process_initializer.h.

◆ translate_user_notation() [1/3]

lps::multi_action mcrl2::lps::translate_user_notation ( const lps::multi_action x)

Definition at line 41 of file lps.cpp.

◆ translate_user_notation() [2/3]

template<typename T >
T mcrl2::lps::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/3]

template<typename T >
void mcrl2::lps::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.

◆ txt2lps()

void mcrl2::lps::txt2lps ( const std::string &  input_filename,
const std::string &  output_filename 
)

Definition at line 310 of file tools.cpp.

◆ typecheck_action_rename_specification()

action_rename_specification mcrl2::lps::typecheck_action_rename_specification ( const action_rename_specification arspec,
const lps::stochastic_specification lpsspec 
)
inline

Type checks an action rename specification.

Parameters
arspecAn action rename specifition.
lpsspecA linear process specification, used for the datatypes and action declarations.
Returns
A type checked rename specification.

Definition at line 157 of file typecheck.h.

◆ typecheck_multi_action() [1/2]

multi_action mcrl2::lps::typecheck_multi_action ( process::untyped_multi_action mult_act,
const data::data_specification data_spec,
const process::action_label_list action_decls 
)
inline

Type check a multi action Throws an exception if something went wrong.

Parameters
[in]mult_actA multi action that has not been type checked.
[in]data_specA data specification to use as context.
[in]action_declsA list of action declarations to use as context.
Postcondition
mult_action is type checked and sorts have been added when necessary.

Definition at line 128 of file typecheck.h.

◆ typecheck_multi_action() [2/2]

multi_action mcrl2::lps::typecheck_multi_action ( process::untyped_multi_action mult_act,
multi_action_type_checker typechecker 
)
inline

Type check a multi action Throws an exception if something went wrong.

Parameters
[in]mult_actA multi action that has not been type checked.
[in]typecheckerChecker that will be used to check multi_act
Postcondition
mult_action is type checked and sorts have been added when necessary.

Definition at line 144 of file typecheck.h.

◆ used_read_variables()

std::set< data::variable > mcrl2::lps::used_read_variables ( const action_summand summand)
inline

Definition at line 85 of file confluence.h.

◆ write_spec()

static void mcrl2::lps::write_spec ( atermpp::aterm_ostream stream,
const stochastic_specification spec 
)
static

Definition at line 122 of file lps_io.cpp.