mCRL2
Loading...
Searching...
No Matches
rename_expression.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
9/// \file mcrl2/process/rename_expression.h
10/// \brief add your file description here.
11
12#ifndef MCRL2_PROCESS_RENAME_EXPRESSION_H
13#define MCRL2_PROCESS_RENAME_EXPRESSION_H
14
15#include "mcrl2/core/detail/default_values.h"
16#include "mcrl2/core/detail/soundness_checks.h"
17
18namespace mcrl2
19{
20
21namespace process
22{
23
24//--- start generated class rename_expression ---//
25/// \\brief A rename expression
27{
28 public:
29 /// \\brief Default constructor X3.
32 {}
33
34 /// \\brief Constructor Z9.
35 /// \\param term A term
36 explicit rename_expression(const atermpp::aterm& term)
37 : atermpp::aterm(term)
38 {
39 assert(core::detail::check_term_RenameExpr(*this));
40 }
41
42 /// \\brief Constructor Z12.
45 {}
46
47 /// \\brief Constructor Z1.
48 rename_expression(const std::string& source, const std::string& target)
50 {}
51
52 /// Move semantics
53 rename_expression(const rename_expression&) noexcept = default;
54 rename_expression(rename_expression&&) noexcept = default;
55 rename_expression& operator=(const rename_expression&) noexcept = default;
57
59 {
60 return atermpp::down_cast<core::identifier_string>((*this)[0]);
61 }
62
64 {
65 return atermpp::down_cast<core::identifier_string>((*this)[1]);
66 }
67};
68
69/// \\brief Make_rename_expression constructs a new term into a given address.
70/// \\ \param t The reference into which the new rename_expression is constructed.
71template <class... ARGUMENTS>
72inline void make_rename_expression(atermpp::aterm& t, const ARGUMENTS&... args)
73{
74 atermpp::make_term_appl(t, core::detail::function_symbol_RenameExpr(), args...);
75}
76
77/// \\brief list of rename_expressions
79
80/// \\brief vector of rename_expressions
82
83/// \\brief Test for a rename_expression expression
84/// \\param x A term
85/// \\return True if \\a x is a rename_expression expression
86inline
88{
90}
91
92// prototype declaration
93std::string pp(const rename_expression& x);
94
95/// \\brief Outputs the object to a stream
96/// \\param out An output stream
97/// \\param x Object x
98/// \\return The output stream
99inline
100std::ostream& operator<<(std::ostream& out, const rename_expression& x)
101{
102 return out << process::pp(x);
103}
104
105/// \\brief swap overload
107{
108 t1.swap(t2);
109}
110//--- end generated class rename_expression ---//
111
112} // namespace process
113
114} // namespace mcrl2
115
116#endif // MCRL2_PROCESS_RENAME_EXPRESSION_H
aterm_string(const std::string &s)
Constructor that allows construction from a string.
aterm_string & operator=(const aterm_string &t) noexcept=default
const aterm & operator[](const size_type i) const
Returns the i-th argument.
Definition aterm.h:187
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
Definition aterm.h:144
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
bool operator==(const function_symbol &f) const
Equality test.
A list of aterm objects.
Definition aterm_list.h:24
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
Definition aterm_core.h:152
bool operator<(const unprotected_aterm_core &t) const
Comparison operator for two unprotected aterms.
Definition aterm_core.h:104
bool operator==(const unprotected_aterm_core &t) const
Comparison operator.
Definition aterm_core.h:83
bool defined() const
Returns true if this term is not equal to the term assigned by the default constructor of aterms,...
Definition aterm_core.h:143
bool operator!=(const unprotected_aterm_core &t) const
Inequality operator on two unprotected aterms.
Definition aterm_core.h:92
An abstraction expression.
Definition abstraction.h:26
const variable_list & variables() const
Definition abstraction.h:63
const data_expression & body() const
Definition abstraction.h:68
const binder_type & binding_operator() const
Definition abstraction.h:58
\brief A sort alias
Definition alias.h:26
alias(const basic_sort &name, const sort_expression &reference)
\brief Constructor Z12.
Definition alias.h:42
\brief Assignment of a data expression to a variable
Definition assignment.h:91
const data_expression & rhs() const
Definition assignment.h:122
const variable & lhs() const
Definition assignment.h:117
\brief A basic sort
Definition basic_sort.h:26
data_expression & operator=(const data_expression &) noexcept=default
data_expression()
\brief Default constructor X3.
data_expression & operator=(data_expression &&) noexcept=default
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
data_expression(const data_expression &) noexcept=default
Move semantics.
const function_symbol_vector & constructors(const sort_expression &s, const bool do_not_normalize=false) const
Gets all constructors of a sort including those that are system defined.
void add_consistent_inequality_set(const std::vector< linear_inequality > &inequalities_in_)
inequality_consistency_cache & operator=(const inequality_consistency_cache &)=delete
inequality_consistency_cache(const inequality_consistency_cache &)=delete
inequality_inconsistency_cache_base * m_cache
bool is_consistent(const std::vector< linear_inequality > &inequalities_in_) const
inequality_inconsistency_cache_base & operator=(const inequality_inconsistency_cache_base &)=delete
inequality_inconsistency_cache_base(const node_type node, const linear_inequality &inequality, inequality_inconsistency_cache_base *present_branch, inequality_inconsistency_cache_base *non_present_branch)
inequality_inconsistency_cache_base(const inequality_inconsistency_cache_base &)=delete
bool is_inconsistent(const std::vector< linear_inequality > &inequalities_in_) const
inequality_inconsistency_cache & operator=(const inequality_consistency_cache &)=delete
inequality_inconsistency_cache(const inequality_inconsistency_cache &)=delete
void add_inconsistent_inequality_set(const std::vector< linear_inequality > &inequalities_in_)
lhs_t(const aterm &t)
Constructor from an aterm.
const data_expression & operator[](const variable &v) const
Give the factor of variable v.
data_expression transform_to_data_expression() const
lhs_t erase(const variable &v) const
Erase a variable and its factor.
std::size_t count(const variable &v) const
Give the factor of variable v.
lhs_t(const ITERATOR begin, const ITERATOR end, TRANSFORMER f)
Constructor.
data_expression evaluate(const SubstitutionFunction &beta, const rewriter &r) const
Evaluate the variables in this lhs_t according to the subsitution function.
lhs_t::const_iterator find(const variable &v) const
Give an iterator of the factor/variable pair for v, or end() if v does not occur.
lhs_t(const ITERATOR begin, const ITERATOR end)
Constructor.
variable_with_a_rational_factor(const variable &v, const data_expression &f)
\brief A function sort
\brief A function symbol
function_symbol & operator=(function_symbol &&) noexcept=default
function_symbol()
Default constructor.
const detail::lhs_t & lhs() const
linear_inequality invert(const rewriter &r)
bool typical_pair(data_expression &lhs_expression, data_expression &rhs_expression, detail::comparison_t &comparison_operator, const rewriter &r) const
Return this inequality as a typical pair of terms of the form <x1+c2 x2+...+cn xn,...
linear_inequality()
Constructor yielding an inconsistent inequality.
bool is_true(const rewriter &r) const
void add_variables(std::set< variable > &variable_set) const
bool is_false(const rewriter &r) const
linear_inequality(const data_expression &e, const rewriter &r)
Constructor that constructs a linear inequality out of a data expression.
linear_inequality(const data_expression &lhs, const data_expression &rhs, const detail::comparison_t comparison, const rewriter &r, const bool negate=false)
constructor.
data_expression transform_to_data_expression() const
static void parse_and_store_expression(const data_expression &e, detail::map_based_lhs_t &new_lhs, data_expression &new_rhs, const rewriter &r, const bool negate=false, const data_expression &factor=real_one())
linear_inequality(const detail::lhs_t &lhs, const data_expression &r, detail::comparison_t t)
Basic constructor.
detail::lhs_t::const_iterator lhs_begin() const
detail::lhs_t::const_iterator lhs_end() const
linear_inequality(const detail::lhs_t &lhs, const data_expression &rhs, detail::comparison_t comparison, const rewriter &r)
constructor.
const data_expression & rhs() const
data_expression get_factor_for_a_variable(const variable &x)
detail::comparison_t comparison() const
Wrapper class for internal storage and substitution updates using operator()
assignment(const variable_type &v, Substitution &sigma, std::multiset< variable_type > &variables_in_rhs, std::set< variable_type > &scratch_set)
Constructor.
void operator=(const expression_type &e)
Actual assignment.
Wrapper that extends any substitution to a substitution maintaining the vars in its rhs.
bool variable_occurs_in_a_rhs(const variable_type &v)
Indicates whether a variable occurs in some rhs of this substitution.
assignment operator[](variable_type const &v)
Assigment operator.
const std::multiset< variable > & variables_in_rhs()
Provides a set of variables that occur in the right hand sides of the assignments.
std::multiset< variable_type > m_variables_in_rhs
Components for generating an arbitrary element of a sort.
data_expression operator()(const sort_expression &sort)
Returns a representative of a sort.
Rewriter that operates on data expressions.
Definition rewriter.h:81
data_expression operator()(const data_expression &d) const
Rewrites a data expression.
Definition rewriter.h:158
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
void add_identifier(const core::identifier_string &s) override
Adds the identifier s to the context.
\brief A sort expression
sort_expression & operator=(const sort_expression &) noexcept=default
\brief An argument of a constructor of a structured sort
\brief A constructor for a structured sort
function_symbol constructor_function(const sort_expression &s) const
Returns the constructor function for this constructor, assuming it is internally represented with sor...
function_symbol recogniser_function(const sort_expression &s) const
Returns the function corresponding to the recogniser of this constructor, such that it is usable in t...
\brief A data variable
Definition variable.h:28
variable(const std::string &name, const sort_expression &sort)
Constructor.
Definition variable.h:69
const core::identifier_string & name() const
Definition variable.h:38
variable & operator=(variable &&) noexcept=default
const sort_expression & sort() const
Definition variable.h:43
variable & operator=(const variable &) noexcept=default
\brief A where expression
where_clause(const atermpp::aterm &term)
logger(const log_level_t l)
Default constructor.
Definition logger.h:164
LPS summand containing a multi-action.
lps::multi_action m_multi_action
The summation variables of the summand.
action_summand(const action_summand &) noexcept=default
Move semantics.
data::assignment_list & assignments()
Returns the sequence of assignments.
void swap(action_summand &other)
Swaps the contents.
data::data_expression_list next_state(const data::variable_list &process_parameters) const
Returns the next state corresponding to this summand.
Definition lps.cpp:68
action_summand(const data::variable_list &summation_variables, const data::data_expression &condition, const lps::multi_action &action, const data::assignment_list &assignments)
Constructor.
bool has_time() const
Returns true if time is available.
bool is_tau() const
Returns true if the multi-action corresponding to this summand is equal to tau.
summand_base super
The super class.
action_summand & operator=(const action_summand &) noexcept=default
action_summand & operator=(action_summand &&) noexcept=default
action_summand(action_summand &&) noexcept=default
const data::assignment_list & assignments() const
Returns the sequence of assignments.
data::assignment_list m_assignments
The assignments of the next state.
Algorithm class for elimination of constant parameters.
Definition constelm.h:26
void LOG_PARAMETER_CHANGE(const data::data_expression &d_j, const data::data_expression &Rd_j, const data::data_expression &Rg_ij, const data::mutable_map_substitution<> &sigma, const std::string &msg="")
Definition constelm.h:62
lps::detail::lps_algorithm< Specification > super
Definition constelm.h:27
bool is_constant(const data::data_expression &x, const std::set< data::variable > &global_variables) const
Definition constelm.h:97
void remove_parameters(data::mutable_map_substitution<> &sigma)
Applies the substitution computed by compute_constant_parameters.
Definition constelm.h:234
const DataRewriter & R
The rewriter used by the constelm algorithm.
Definition constelm.h:41
void LOG_CONSTANT_PARAMETERS(const data::mutable_map_substitution<> &sigma, const std::string &constant_removed_msg="", const std::string &nothing_removed_msg="")
Definition constelm.h:43
bool m_ignore_conditions
If true, conditions are not evaluated and assumed to be true.
Definition constelm.h:35
constelm_algorithm(Specification &spec, const DataRewriter &R_)
Constructor.
Definition constelm.h:114
void LOG_CONDITION(const data::data_expression &cond, const data::data_expression &c_i, const data::mutable_map_substitution<> &sigma, const std::string &msg="")
Definition constelm.h:79
void run(bool instantiate_global_variables=false, bool ignore_conditions=false)
Runs the constelm algorithm.
Definition constelm.h:259
std::map< data::variable, std::size_t > m_index_of
Maps process parameters to their index.
Definition constelm.h:38
data::mutable_map_substitution compute_constant_parameters(bool instantiate_global_variables=false, bool ignore_conditions=false)
Computes constant parameters.
Definition constelm.h:125
bool m_instantiate_global_variables
If true, then the algorithm is allowed to instantiate free variables as a side effect.
Definition constelm.h:32
LPS summand containing a deadlock.
deadlock_summand(const data::variable_list &summation_variables, const data::data_expression &condition, const lps::deadlock &delta)
Constructor.
Represents a deadlock.
Definition deadlock.h:26
deadlock(data::data_expression time=data::undefined_real())
Constructor.
Definition deadlock.h:36
data::data_expression & time()
Returns the time.
Definition deadlock.h:56
Algorithm class for algorithms on linear process specifications. It can be instantiated with lps::spe...
void remove_parameters(const std::set< data::variable > &to_be_removed)
Removes formal parameters from the specification.
void remove_unused_summand_variables()
Removes unused summand variables.
void sumelm_find_variables(const action_summand &s, std::set< data::variable > &result) const
void summand_remove_unused_summand_variables(SummandType &summand_)
void sumelm_find_variables(const deadlock_summand &s, std::set< data::variable > &result) const
data::data_expression next_state(const action_summand &s, const data::variable &v) const
Applies the next state substitution to the variable v.
bool verbose() const
Flag for verbose output.
void remove_singleton_sorts()
Removes parameters with a singleton sort.
void remove_trivial_summands()
Removes summands with condition equal to false.
void instantiate_free_variables()
Attempts to eliminate the free variables of the specification, by substituting a constant value for t...
lps_algorithm(Specification &spec)
Constructor.
Specification & m_spec
The specification that is processed by the algorithm.
data_expression & constraint()
Obtain a reference to the constraint.
deadlock_summand_vector & deadlock_summands()
Returns the sequence of deadlock summands.
const std::vector< ActionSummand > & action_summands() const
Returns the sequence of action summands.
deadlock_summand_vector m_deadlock_summands
The deadlock summands of the process.
linear_process_base()=default
Constructor.
data::variable_list m_process_parameters
The process parameters of the process.
linear_process_base(const data::variable_list &process_parameters, const deadlock_summand_vector &deadlock_summands, const std::vector< ActionSummand > &action_summands)
Constructor.
bool has_time() const
Returns true if time is available in at least one of the summands.
data::variable_list & process_parameters()
Returns the sequence of process parameters.
std::vector< ActionSummand > m_action_summands
The action summands of the process.
ActionSummand action_summand_type
The action summand type.
linear_process_base(const atermpp::aterm &lps, bool stochastic_distributions_allowed=true)
Constructor.
const deadlock_summand_vector & deadlock_summands() const
Returns the sequence of deadlock summands.
std::vector< ActionSummand > & action_summands()
Returns the sequence of action summands.
std::size_t summand_count() const
Returns the number of LPS summands.
const data::variable_list & process_parameters() const
Returns the sequence of process parameters.
linear_process(const data::variable_list &process_parameters, const deadlock_summand_vector &deadlock_summands, const action_summand_vector &action_summands)
Constructor.
linear_process(const atermpp::aterm &lps, bool=false)
Constructor.
linear_process()=default
Constructor.
linear_process_base< action_summand > super
\brief A timed multi-action
multi_action(const multi_action &) noexcept=default
Move semantics.
multi_action(const atermpp::aterm &term)
Constructor.
bool has_time() const
Returns true if time is available.
const process::action_list & actions() const
multi_action(const process::action &l)
Constructor.
multi_action operator+(const multi_action &other) const
Joins the actions of both multi actions.
multi_action sort_actions() const
Returns the multiaction in which the list of actions is sorted.
multi_action & operator=(multi_action &&) noexcept=default
const data::data_expression & time() const
multi_action & operator=(const multi_action &) noexcept=default
multi_action(multi_action &&) noexcept=default
multi_action(const process::action_list &actions=process::action_list(), data::data_expression time=data::undefined_real())
Constructor.
process_initializer & operator=(process_initializer &&) noexcept=default
process_initializer(process_initializer &&) noexcept=default
process_initializer(const process_initializer &) noexcept=default
Move semantics.
process_initializer(const data::data_expression_list &expressions)
Constructor.
process_initializer(const atermpp::aterm &term, bool check_distribution=true)
Constructor.
data::data_expression_list expressions() const
process_initializer & operator=(const process_initializer &) noexcept=default
process_initializer()
Default constructor.
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the LPS.
LinearProcess & process()
Returns a reference to the linear process of the specification.
process::action_label_list m_action_labels
The action specification of the specification.
specification_base(const data::data_specification &data, const process::action_label_list &action_labels, const std::set< data::variable > &global_variables, const LinearProcess &lps, const InitialProcessExpression &initial_process)
Constructor.
const process::action_label_list & action_labels() const
Returns a sequence of action labels. This sequence contains all action labels occurring in the specif...
const InitialProcessExpression & initial_process() const
Returns the initial process.
const LinearProcess & process() const
Returns the linear process of the specification.
process::action_label_list & action_labels()
Returns a sequence of action labels. This sequence contains all action labels occurring in the specif...
std::set< data::variable > m_global_variables
The set of global variables.
LinearProcess process_type
The process type.
InitialProcessExpression & initial_process()
Returns a reference to the initial process.
InitialProcessExpression initial_process_type
The initial process type.
LinearProcess m_process
The linear process of the specification.
std::set< data::variable > & global_variables()
Returns the declared free variables of the LPS.
data::data_specification m_data
The data specification of the specification.
InitialProcessExpression m_initial_process
The initial state of the specification.
Linear process specification.
specification()=default
Constructor.
specification_base< linear_process, process_initializer > super
specification(const data::data_specification &data, const process::action_label_list &action_labels, const std::set< data::variable > &global_variables, const linear_process &lps, const process_initializer &initial_process)
Constructor.
LPS summand containing a multi-action.
stochastic_action_summand(const data::variable_list &summation_variables, const data::data_expression &condition, const lps::multi_action &action, const data::assignment_list &assignments, const stochastic_distribution &distribution)
Constructor.
stochastic_distribution & distribution()
Returns the distribution of this summand.
\brief A stochastic distribution
stochastic_distribution & operator=(stochastic_distribution &&) noexcept=default
stochastic_distribution(stochastic_distribution &&) noexcept=default
stochastic_distribution()
\brief Default constructor X3.
stochastic_distribution(const stochastic_distribution &) noexcept=default
Move semantics.
const data::variable_list & variables() const
bool is_defined() const
Returns true if the distribution is defined, i.e. it contains a valid distribution....
stochastic_distribution(const data::variable_list &variables, const data::data_expression &distribution)
\brief Constructor Z12.
stochastic_distribution & operator=(const stochastic_distribution &) noexcept=default
stochastic_distribution(const atermpp::aterm &term)
const data::data_expression & distribution() const
stochastic_linear_process(const data::variable_list &process_parameters, const deadlock_summand_vector &deadlock_summands, const stochastic_action_summand_vector &action_summands)
Constructor.
stochastic_process_initializer(const data::data_expression_list &expressions, const stochastic_distribution &distribution)
Constructor.
const stochastic_distribution & distribution() const
stochastic_specification(const specification &other)
Constructor. This constructor is explicit as implicit conversions of this kind is a source of bugs.
specification_base< stochastic_linear_process, stochastic_process_initializer > super
stochastic_specification(const data::data_specification &data, const process::action_label_list &action_labels, const std::set< data::variable > &global_variables, const stochastic_linear_process &lps, const stochastic_process_initializer &initial_process)
Constructor.
Base class for LPS summands.
Definition summand.h:25
const data::data_expression & condition() const
Returns the condition expression.
Definition summand.h:60
void swap(summand_base &other)
Swaps the contents.
Definition summand.h:73
summand_base(const data::variable_list &summation_variables, const data::data_expression &condition)
Constructor.
Definition summand.h:39
\brief An action label
const data::sort_expression_list & sorts() const
action_label()
\brief Default constructor X3.
action_label(const atermpp::aterm &term)
action_label & operator=(action_label &&) noexcept=default
action_label(const std::string &name, const data::sort_expression_list &sorts)
\brief Constructor Z1.
action_label(action_label &&) noexcept=default
const core::identifier_string & name() const
action_label & operator=(const action_label &) noexcept=default
action_label(const action_label &) noexcept=default
Move semantics.
action_label(const core::identifier_string &name, const data::sort_expression_list &sorts)
\brief Constructor Z12.
\brief A multiset of action names
action_name_multiset & operator=(action_name_multiset &&) noexcept=default
const core::identifier_string_list & names() const
action_name_multiset()
\brief Default constructor X3.
action_name_multiset & operator=(const action_name_multiset &) noexcept=default
action_name_multiset(const atermpp::aterm &term)
action_name_multiset(const action_name_multiset &) noexcept=default
Move semantics.
action_name_multiset(action_name_multiset &&) noexcept=default
action_name_multiset(const core::identifier_string_list &names)
\brief Constructor Z12.
action(const action_label &label, const data::data_expression_list &arguments)
\brief Constructor Z14.
action & operator=(action &&) noexcept=default
action()
\brief Default constructor X3.
action(const atermpp::aterm &term)
action(action &&) noexcept=default
action & operator=(const action &) noexcept=default
const data::data_expression_list & arguments() const
action(const action &) noexcept=default
Move semantics.
const action_label & label() const
\brief The allow operator
allow(const allow &) noexcept=default
Move semantics.
allow()
\brief Default constructor X3.
allow(const atermpp::aterm &term)
const process_expression & operand() const
allow(const action_name_multiset_list &allow_set, const process_expression &operand)
\brief Constructor Z14.
allow(allow &&) noexcept=default
const action_name_multiset_list & allow_set() const
allow & operator=(allow &&) noexcept=default
allow & operator=(const allow &) noexcept=default
\brief The at operator
at(at &&) noexcept=default
at(const atermpp::aterm &term)
at(const at &) noexcept=default
Move semantics.
at()
\brief Default constructor X3.
at & operator=(const at &) noexcept=default
at(const process_expression &operand, const data::data_expression &time_stamp)
\brief Constructor Z14.
const data::data_expression & time_stamp() const
at & operator=(at &&) noexcept=default
const process_expression & operand() const
\brief The block operator
block & operator=(block &&) noexcept=default
block & operator=(const block &) noexcept=default
const process_expression & operand() const
block(block &&) noexcept=default
block(const block &) noexcept=default
Move semantics.
block(const atermpp::aterm &term)
block()
\brief Default constructor X3.
block(const core::identifier_string_list &block_set, const process_expression &operand)
\brief Constructor Z14.
const core::identifier_string_list & block_set() const
\brief The bounded initialization
bounded_init(const bounded_init &) noexcept=default
Move semantics.
bounded_init & operator=(const bounded_init &) noexcept=default
const process_expression & right() const
bounded_init(bounded_init &&) noexcept=default
bounded_init(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
bounded_init(const atermpp::aterm &term)
const process_expression & left() const
bounded_init()
\brief Default constructor X3.
bounded_init & operator=(bounded_init &&) noexcept=default
\brief The choice operator
choice(const atermpp::aterm &term)
choice & operator=(const choice &) noexcept=default
choice(const choice &) noexcept=default
Move semantics.
choice()
\brief Default constructor X3.
const process_expression & left() const
choice(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
choice(choice &&) noexcept=default
const process_expression & right() const
choice & operator=(choice &&) noexcept=default
\brief The communication operator
comm & operator=(const comm &) noexcept=default
comm(const atermpp::aterm &term)
comm(comm &&) noexcept=default
comm & operator=(comm &&) noexcept=default
comm(const comm &) noexcept=default
Move semantics.
const communication_expression_list & comm_set() const
comm(const communication_expression_list &comm_set, const process_expression &operand)
\brief Constructor Z14.
const process_expression & operand() const
comm()
\brief Default constructor X3.
const core::identifier_string & name() const
communication_expression()
\brief Default constructor X3.
communication_expression & operator=(const communication_expression &) noexcept=default
communication_expression(const action_name_multiset &action_name, const std::string &name)
\brief Constructor Z1.
communication_expression(const communication_expression &) noexcept=default
Move semantics.
communication_expression(communication_expression &&) noexcept=default
communication_expression & operator=(communication_expression &&) noexcept=default
communication_expression(const action_name_multiset &action_name, const core::identifier_string &name)
\brief Constructor Z12.
const action_name_multiset & action_name() const
\brief The value delta
delta & operator=(const delta &) noexcept=default
delta()
\brief Default constructor X3.
delta(const atermpp::aterm &term)
delta(delta &&) noexcept=default
delta(const delta &) noexcept=default
Move semantics.
delta & operator=(delta &&) noexcept=default
\brief The hide operator
hide(hide &&) noexcept=default
hide(const atermpp::aterm &term)
hide(const core::identifier_string_list &hide_set, const process_expression &operand)
\brief Constructor Z14.
const core::identifier_string_list & hide_set() const
hide & operator=(const hide &) noexcept=default
const process_expression & operand() const
hide(const hide &) noexcept=default
Move semantics.
hide & operator=(hide &&) noexcept=default
hide()
\brief Default constructor X3.
\brief The if-then-else operator
const process_expression & else_case() const
if_then_else(if_then_else &&) noexcept=default
const process_expression & then_case() const
if_then_else(const atermpp::aterm &term)
if_then_else()
\brief Default constructor X3.
if_then_else & operator=(const if_then_else &) noexcept=default
if_then_else(const if_then_else &) noexcept=default
Move semantics.
const data::data_expression & condition() const
if_then_else & operator=(if_then_else &&) noexcept=default
if_then_else(const data::data_expression &condition, const process_expression &then_case, const process_expression &else_case)
\brief Constructor Z14.
\brief The if-then operator
const process_expression & then_case() const
if_then & operator=(const if_then &) noexcept=default
if_then(const data::data_expression &condition, const process_expression &then_case)
\brief Constructor Z14.
if_then(const atermpp::aterm &term)
const data::data_expression & condition() const
if_then(const if_then &) noexcept=default
Move semantics.
if_then & operator=(if_then &&) noexcept=default
if_then(if_then &&) noexcept=default
if_then()
\brief Default constructor X3.
\brief The left merge operator
left_merge(left_merge &&) noexcept=default
const process_expression & right() const
left_merge & operator=(left_merge &&) noexcept=default
left_merge(const atermpp::aterm &term)
left_merge & operator=(const left_merge &) noexcept=default
left_merge(const left_merge &) noexcept=default
Move semantics.
left_merge(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
const process_expression & left() const
left_merge()
\brief Default constructor X3.
\brief The merge operator
merge(const atermpp::aterm &term)
const process_expression & right() const
const process_expression & left() const
merge & operator=(const merge &) noexcept=default
merge(const merge &) noexcept=default
Move semantics.
merge(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
merge & operator=(merge &&) noexcept=default
merge(merge &&) noexcept=default
merge()
\brief Default constructor X3.
\brief A process expression
process_expression & operator=(const process_expression &) noexcept=default
process_expression(const process_expression &) noexcept=default
Move semantics.
process_expression()
\brief Default constructor X3.
process_expression(const data::untyped_data_parameter &x)
\brief Constructor Z6.
process_expression(process_expression &&) noexcept=default
process_expression(const atermpp::aterm &term)
process_expression & operator=(process_expression &&) noexcept=default
\brief A process identifier
process_identifier(const process_identifier &) noexcept=default
Move semantics.
const data::variable_list & variables() const
process_identifier & operator=(const process_identifier &) noexcept=default
process_identifier(process_identifier &&) noexcept=default
process_identifier(const core::identifier_string &name, const data::variable_list &variables)
Constructor.
const core::identifier_string & name() const
process_identifier & operator=(process_identifier &&) noexcept=default
process_identifier(const std::string &name, const data::variable_list &variables)
Constructor.
process_identifier(const atermpp::aterm &term)
Constructor.
process_instance_assignment(const process_instance_assignment &) noexcept=default
Move semantics.
process_instance_assignment()
\brief Default constructor X3.
process_instance_assignment(const process_identifier &identifier, const data::assignment_list &assignments)
\brief Constructor Z14.
process_instance_assignment & operator=(const process_instance_assignment &) noexcept=default
process_instance_assignment(process_instance_assignment &&) noexcept=default
const data::assignment_list & assignments() const
process_instance_assignment(const atermpp::aterm &term)
process_instance_assignment & operator=(process_instance_assignment &&) noexcept=default
const process_identifier & identifier() const
const data::data_expression_list & actual_parameters() const
process_instance(const process_identifier &identifier, const data::data_expression_list &actual_parameters)
\brief Constructor Z14.
process_instance & operator=(const process_instance &) noexcept=default
process_instance & operator=(process_instance &&) noexcept=default
const process_identifier & identifier() const
process_instance(process_instance &&) noexcept=default
process_instance()
\brief Default constructor X3.
process_instance(const atermpp::aterm &term)
process_instance(const process_instance &) noexcept=default
Move semantics.
Process specification consisting of a data specification, action labels, a sequence of process equati...
process_expression & init()
Returns the initialization of the process specification.
process::action_label_list & action_labels()
Returns the action label specification.
\brief A rename expression
const core::identifier_string & source() const
rename_expression()
\brief Default constructor X3.
rename_expression & operator=(rename_expression &&) noexcept=default
rename_expression & operator=(const rename_expression &) noexcept=default
rename_expression(core::identifier_string &source, core::identifier_string &target)
\brief Constructor Z12.
const core::identifier_string & target() const
rename_expression(const atermpp::aterm &term)
rename_expression(rename_expression &&) noexcept=default
rename_expression(const std::string &source, const std::string &target)
\brief Constructor Z1.
rename_expression(const rename_expression &) noexcept=default
Move semantics.
\brief The rename operator
rename(const atermpp::aterm &term)
rename & operator=(const rename &) noexcept=default
rename(const rename &) noexcept=default
Move semantics.
rename()
\brief Default constructor X3.
const process_expression & operand() const
rename & operator=(rename &&) noexcept=default
rename(rename &&) noexcept=default
rename(const rename_expression_list &rename_set, const process_expression &operand)
\brief Constructor Z14.
const rename_expression_list & rename_set() const
\brief The sequential composition
seq & operator=(seq &&) noexcept=default
const process_expression & right() const
seq(const atermpp::aterm &term)
seq()
\brief Default constructor X3.
seq & operator=(const seq &) noexcept=default
const process_expression & left() const
seq(seq &&) noexcept=default
seq(const seq &) noexcept=default
Move semantics.
seq(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
\brief The distribution operator
const data::variable_list & variables() const
const data::data_expression & distribution() const
stochastic_operator & operator=(stochastic_operator &&) noexcept=default
stochastic_operator()
\brief Default constructor X3.
stochastic_operator(const atermpp::aterm &term)
stochastic_operator(stochastic_operator &&) noexcept=default
stochastic_operator(const stochastic_operator &) noexcept=default
Move semantics.
stochastic_operator & operator=(const stochastic_operator &) noexcept=default
const process_expression & operand() const
stochastic_operator(const data::variable_list &variables, const data::data_expression &distribution, const process_expression &operand)
\brief Constructor Z14.
\brief The sum operator
const process_expression & operand() const
sum(const data::variable_list &variables, const process_expression &operand)
\brief Constructor Z14.
sum(const atermpp::aterm &term)
sum & operator=(sum &&) noexcept=default
sum()
\brief Default constructor X3.
const data::variable_list & variables() const
sum(sum &&) noexcept=default
sum(const sum &) noexcept=default
Move semantics.
sum & operator=(const sum &) noexcept=default
\brief The synchronization operator
sync & operator=(const sync &) noexcept=default
sync(sync &&) noexcept=default
sync(const sync &) noexcept=default
Move semantics.
const process_expression & left() const
sync()
\brief Default constructor X3.
sync & operator=(sync &&) noexcept=default
sync(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
const process_expression & right() const
sync(const atermpp::aterm &term)
\brief The value tau
tau(const tau &) noexcept=default
Move semantics.
tau()
\brief Default constructor X3.
tau(const atermpp::aterm &term)
tau & operator=(tau &&) noexcept=default
tau & operator=(const tau &) noexcept=default
tau(tau &&) noexcept=default
\brief An untyped process assginment
untyped_process_assignment & operator=(untyped_process_assignment &&) noexcept=default
const data::untyped_identifier_assignment_list & assignments() const
untyped_process_assignment(const core::identifier_string &name, const data::untyped_identifier_assignment_list &assignments)
\brief Constructor Z14.
untyped_process_assignment(const atermpp::aterm &term)
const core::identifier_string & name() const
untyped_process_assignment()
\brief Default constructor X3.
untyped_process_assignment & operator=(const untyped_process_assignment &) noexcept=default
untyped_process_assignment(untyped_process_assignment &&) noexcept=default
untyped_process_assignment(const untyped_process_assignment &) noexcept=default
Move semantics.
Standard exception class for reporting runtime errors.
Definition exception.h:27
process_expression processbody
objectdatatype(const objectdatatype &o)=default
process_expression representedprocess
variable_list old_parameters
bool free_variables_defined
~objectdatatype()=default
process::action_label_list multi_action_names
processstatustype processstatus
identifier_string objectname
objectdatatype()=default
objectdatatype & operator=(const objectdatatype &o)=default
objecttype object
std::set< variable > free_variables
process_identifier process_representing_action
variable_list parameters
enumeratedtype(const enumeratedtype &e)
enumeratedtype(const std::size_t n, specification_basic_type &spec)
void operator=(const enumeratedtype &e)
enumtype(const enumtype &)=delete
enumtype & operator=(const enumtype &)=delete
enumtype(std::size_t n, const sort_expression_list &fsorts, const sort_expression_list &gsorts, specification_basic_type &spec)
process_pid_pair & operator=(const process_pid_pair &other)=default
const process_expression & process_body() const
const process_identifier & process_id() const
process_pid_pair(const process_pid_pair &other)=default
process_pid_pair & operator=(process_pid_pair &&other)=default
process_pid_pair(const process_expression &process_body, const process_identifier &pid)
process_pid_pair(process_pid_pair &&other)=default
static stackoperations * find_suitable_stack_operations(const variable_list &parameters, stackoperations *stack_operations_list)
stacklisttype & operator=(const stacklisttype &)=delete
stacklisttype(const variable_list &parlist, specification_basic_type &spec, const bool regular, const std::set< process_identifier > &pCRLprocs, const bool singlecontrolstate)
Constructor.
stacklisttype(const stacklisttype &)=delete
stackoperations & operator=(const stackoperations &)=delete
stackoperations(const stackoperations &)=delete
stackoperations(const variable_list &pl, specification_basic_type &spec)
process_expression procstorealGNFbody(const process_expression &body, variableposition v, std::vector< process_identifier > &todo, const bool regular, processstatustype mode, const variable_list &freevars, const std::set< variable > &variables_bound_in_sum)
data_expression construct_binary_case_tree(std::size_t n, const variable_list &sums, data_expression_list terms, const sort_expression &termsort, const enumtype &e)
data::maintain_variables_in_rhs< data::mutable_map_substitution<> > make_unique_variables(const variable_list &var_list, const std::string &hint)
variable_list parscollect(const process_expression &oldbody, process_expression &newbody)
action_list linMergeMultiActionList(const action_list &ma1, const action_list &ma2)
const objectdatatype & objectIndex(const aterm &o) const
void generateLPEpCRL(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process_identifier &procId, const bool containstime, const bool regular, variable_list &parameters, data_expression_list &init, stochastic_distribution &initial_stochastic_distribution)
variable get_fresh_variable(const std::string &s, const sort_expression &sort, const int reuse_index=-1)
process_expression distributeActionOverConditions(const process_expression &act, const data_expression &condition, const process_expression &restterm, const variable_list &freevars, const std::set< variable > &variables_bound_in_sum)
data_expression construct_binary_case_tree_rec(std::size_t n, const variable_list &sums, data_expression_list &terms, const sort_expression &termsort, const enumtype &e)
static void complete_proc_identifier_map(std::map< process_identifier, process_identifier > &identifier_identifier_map)
process_expression to_regular_form(const process_expression &t, std::vector< process_identifier > &todo, const variable_list &freevars, const std::set< variable > &variables_bound_in_sum)
void collectsumlistterm(const process_identifier &procId, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process_expression &body, const variable_list &pars, const stacklisttype &stack, const bool regular, const bool singlestate, const std::set< process_identifier > &pCRLprocs)
data_expression_list findarguments(const variable_list &pars, const variable_list &parlist, const assignment_list &args, const data_expression_list &t2, const stacklisttype &stack, const variable_list &vars, const std::set< variable > &free_variables_in_body, const variable_list &stochastic_variables)
void calculate_communication_merge(const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const stochastic_action_summand_vector &action_summands2, const deadlock_summand_vector &deadlock_summands2, const action_name_multiset_list &allowlist, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)
void insertvariable(const variable &var, const bool mustbenew)
process_identifier storeinit(const process_expression &init)
static action_list to_sorted_action_list(const process_expression &p)
Convert the process expression to a sorted action list.
process_expression guarantee_that_parameters_have_unique_type_body(const process_expression &t, std::set< process_identifier > &visited_processes, std::set< identifier_string > &used_variable_names, maintain_variables_in_rhs< mutable_map_substitution<> > &parameter_mapping, std::set< variable > &variables_in_lhs_of_parameter_mapping)
static action_list hide_(const identifier_string_list &hidelist, const action_list &multiaction)
process_expression pCRLrewrite(const process_expression &t)
data_expression_list pushdummy_regular_data_expressions(const variable_list &pars, const stacklisttype &stack)
void define_equations_for_case_function(const std::size_t index, const data::function_symbol &functionname, const sort_expression &sort)
void alphaconvert(variable_list &sumvars, MutableSubstitution &sigma, const variable_list &occurvars, const data_expression_list &occurterms)
bool canterminatebody(const process_expression &t)
data_expression transform_matching_list(const variable_list &matchinglist)
void add_summands(const process_identifier &procId, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, process_expression summandterm, const std::set< process_identifier > &pCRLprocs, const stacklisttype &stack, const bool regular, const bool singlestate, const variable_list &process_parameters)
bool isDeltaAtZero(const process_expression &t)
data::function_symbol find_case_function(std::size_t index, const sort_expression &sort) const
data_expression_list make_initialstate(const process_identifier &initialProcId, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const bool regular, const bool singlecontrolstate, const stochastic_distribution &initial_stochastic_distribution)
static bool summandsCanBeClustered(const stochastic_action_summand &summand1, const stochastic_action_summand &summand2)
static sort_expression_list getActionSorts(const action_list &actionlist)
void filter_vars_by_multiaction(const action_list &multiaction, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
stochastic_action_summand collect_sum_arg_arg_cond(const enumtype &e, std::size_t n, const stochastic_action_summand_vector &action_summands, const variable_list &parameters)
static process_identifier get_last(const process_identifier &id, const std::map< process_identifier, process_identifier > &identifier_identifier_map)
static bool check_real_variable_occurrence(const variable_list &sumvars, const data_expression &actiontime, const data_expression &condition)
process_identifier newprocess(const variable_list &parameters, const process_expression &body, const processstatustype ps, const bool canterminate, const bool containstime)
void make_pCRL_procs(const process_identifier &id, std::set< process_identifier > &reachable_process_identifiers)
void filter_vars_by_term(const data_expression &t, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
data_expression_list pushdummy_stack(const variable_list &parameters, const stacklisttype &stack, const variable_list &stochastic_variables)
void procstorealGNFrec(const process_identifier &procIdDecl, const variableposition v, std::vector< process_identifier > &todo, const bool regular)
static action_label_list getnames(const process_expression &multiAction)
variable_list getparameters_rec(const process_expression &multiAction, std::set< variable > &occurs_set)
static int match_sequence(const std::vector< process_instance_assignment > &s1, const std::vector< process_instance_assignment > &s2, const bool regular2)
void detail_check_objectdata(const aterm &o) const
assignment_list argscollect_regular2(const process_expression &t, variable_list &vl)
void guarantee_that_parameters_have_unique_type(const process_identifier &procId, std::set< process_identifier > &visited_processes, std::set< identifier_string > &used_variable_names, maintain_variables_in_rhs< mutable_map_substitution<> > &parameter_mapping, std::set< variable > &variables_in_lhs_of_parameter_mapping)
void calculate_left_merge_action(const lps::detail::ultimate_delay &ultimate_delay_condition, const stochastic_action_summand_vector &action_summands1, const action_name_multiset_list &allowlist, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands)
process_expression split_body(const process_expression &t, std::map< process_identifier, process_identifier > &visited_id, std::map< process_expression, process_expression > &visited_proc, const variable_list &parameters)
void parallelcomposition(const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const variable_list &pars1, const data_expression_list &init1, const stochastic_distribution &initial_stochastic_distribution1, const lps::detail::ultimate_delay &ultimate_delay_condition1, const stochastic_action_summand_vector &action_summands2, const deadlock_summand_vector &deadlock_summands2, const variable_list &pars2, const data_expression_list &init2, const stochastic_distribution &initial_stochastic_distribution2, const lps::detail::ultimate_delay &ultimate_delay_condition2, const action_name_multiset_list &allowlist1, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, variable_list &pars_result, data_expression_list &init_result, stochastic_distribution &initial_stochastic_distribution, lps::detail::ultimate_delay &ultimate_delay_condition)
bool occursintermlist(const variable &var, const assignment_list &r, const process_identifier &proc_name) const
void transform_process_arguments(const process_identifier &procId)
objectdatatype & insert_process_declaration(const process_identifier &procId, const variable_list &parameters, const process_expression &body, processstatustype s, const bool canterminate, const bool containstime)
static void set_proc_identifier_map(std::map< process_identifier, process_identifier > &identifier_identifier_map, const process_identifier &id1_, const process_identifier &id2_, const process_identifier &initial_process)
bool canterminate_rec(const process_identifier &procId, bool &stable, std::set< process_identifier > &visited)
set_identifier_generator fresh_identifier_generator
std::set< process_identifier > remove_stochastic_operators_from_front(const std::set< process_identifier > &reachable_process_identifiers, process_identifier &initial_process_id, stochastic_distribution &initial_stochastic_distribution)
void filter_vars_by_termlist(Iterator begin, const Iterator &end, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
bool searchProcDeclaration(const variable_list &parameters, const process_expression &body, const processstatustype s, const bool canterminate, const bool containstime, process_identifier &p) const
process_identifier splitmCRLandpCRLprocsAndAddTerminatedAction(const process_identifier &procId)
action_list linMergeMultiActionListProcess(const process_expression &ma1, const process_expression &ma2)
void guarantee_that_parameters_have_unique_type(const process_identifier &procId)
std::vector< process_equation > procs
action_list adapt_multiaction_to_stack(const action_list &multiAction, const stacklisttype &stack, const variable_list &vars)
void determinewhetherprocessescanterminate(const process_identifier &procId)
process_expression distribute_condition(const process_expression &body1, const data_expression &condition)
bool containstime_rec(const process_identifier &procId, bool *stable, std::set< process_identifier > &visited, bool &contains_if_then)
void collectsumlist(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const std::set< process_identifier > &pCRLprocs, const variable_list &pars, const stacklisttype &stack, bool regular, bool singlestate)
data_expression correctstatecond(const process_identifier &procId, const std::set< process_identifier > &pCRLproc, const stacklisttype &stack, int regular)
void calculate_communication_merge_action_summands(const stochastic_action_summand_vector &action_summands1, const stochastic_action_summand_vector &action_summands2, const action_name_multiset_list &allowlist, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands)
processstatustype determine_process_statusterm(const process_expression &body, const processstatustype status)
void calculate_communication_merge_action_deadlock_summands(const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)
data_expression getvar(const variable &var, const stacklisttype &stack) const
variable_list initdatavars
void find_free_variables_process(const process_expression &p, std::set< variable > &free_variables_in_p)
lps::detail::ultimate_delay combine_ultimate_delays(const lps::detail::ultimate_delay &delay1, const lps::detail::ultimate_delay &delay2)
Returns the conjunction of the two delay conditions and the join of the variables,...
process_expression distributeTime(const process_expression &body, const data_expression &time, const variable_list &freevars, data_expression &timecondition)
data_expression_list pushdummyrec_stack(const variable_list &totalpars, const variable_list &pars, const stacklisttype &stack, const variable_list &stochastic_variables)
static action_list to_action_list(const process_expression &p)
void combine_summand_lists(const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const lps::detail::ultimate_delay &ultimate_delay_condition1, const stochastic_action_summand_vector &action_summands2, const deadlock_summand_vector &deadlock_summands2, const lps::detail::ultimate_delay &ultimate_delay_condition2, const variable_list &par1, const variable_list &par3, const action_name_multiset_list &allowlist1, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)
process_expression cut_off_unreachable_tail(const process_expression &t)
std::vector< enumeratedtype > enumeratedtypes
data_expression find_(const variable &s, const assignment_list &args, const stacklisttype &stack, const variable_list &vars, const std::set< variable > &free_variables_in_body, const variable_list &stochastic_variables)
process::action_label_list acts
assignment_list make_procargs_regular(const process_expression &t, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const bool singlestate, const variable_list &stochastic_variables)
static void hidecomposition(const identifier_string_list &hidelist, stochastic_action_summand_vector &action_summands)
std::size_t create_enumeratedtype(const std::size_t n)
void generateLPEmCRL(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process_identifier &procIdDecl, const bool regular, variable_list &pars, data_expression_list &init, stochastic_distribution &initial_stochastic_distribution, lps::detail::ultimate_delay &ultimate_delay_condition)
process_instance_assignment expand_process_instance_assignment(const process_instance_assignment &t)
static process_expression delta_at_zero()
assignment_list rewrite_assignments(const assignment_list &t)
assignment_list push_regular(const process_identifier &procId, const assignment_list &args, const stacklisttype &stack, const std::set< process_identifier > &pCRLprocs, bool singlestate, const variable_list &stochastic_variables)
void transform_process_arguments(const process_identifier &procId, std::set< process_identifier > &visited_processes)
std::set< process_identifier > minimize_set_of_reachable_process_identifiers(const std::set< process_identifier > &reachable_process_identifiers, const process_identifier &initial_process)
void collectPcrlProcesses(const process_identifier &procDecl, std::vector< process_identifier > &pcrlprocesses, std::set< process_identifier > &visited)
variable_list make_binary_sums(std::size_t n, const sort_expression &enumtypename, data_expression &condition, const variable_list &tail)
variable_list SieveProcDataVarsAssignments(const std::set< variable > &vars, const data_expression_list &initial_state_expressions)
data_expression_list extend_conditions(const variable &var, const data_expression_list &conditionlist)
bool check_valid_process_instance_assignment(const process_identifier &id, const assignment_list &assignments)
static variable_list joinparameters(const variable_list &par1, const variable_list &par2)
void calculate_left_merge_deadlock(const lps::detail::ultimate_delay &ultimate_delay_condition, const deadlock_summand_vector &deadlock_summands1, const bool is_allow, const bool is_block, const stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)
void addString(const identifier_string &str)
void procstovarheadGNF(const std::vector< process_identifier > &procs)
static process_expression action_list_to_process(const action_list &ma)
process_expression distribute_sum_over_a_stochastic_operator(const variable_list &sumvars, const variable_list &stochastic_variables, const data_expression &distribution, const process_expression &body)
variable_list collectparameterlist(const std::set< process_identifier > &pCRLprocs)
void alphaconvertprocess(variable_list &sumvars, MutableSubstitution &sigma, const process_expression &p)
process_expression obtain_initial_distribution_term(const process_expression &t)
data_expression push_stack(const process_identifier &procId, const assignment_list &args, const data_expression_list &t2, const stacklisttype &stack, const std::set< process_identifier > &pCRLprocs, const variable_list &vars, const variable_list &stochastic_variables)
void calculate_left_merge(const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const lps::detail::ultimate_delay &ultimate_delay_condition2, const action_name_multiset_list &allowlist, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)
void declare_control_state(const std::set< process_identifier > &pCRLprocs)
void create_case_function_on_enumeratedtype(const sort_expression &sort, const std::size_t enumeratedtype_index)
variable_list SieveProcDataVarsSummands(const std::set< variable > &vars, const stochastic_action_summand_vector &action_summands, const deadlock_summand_vector &deadlock_summands, const variable_list &parameters)
static data_expression_list extend(const data_expression &c, const data_expression_list &cl)
specification_basic_type & operator=(const specification_basic_type &)=delete
static bool occursinvarandremove(const variable &var, variable_list &vl)
process_expression bodytovarheadGNF(const process_expression &body, const state s, const variable_list &freevars, const variableposition v, const std::set< variable > &variables_bound_in_sum)
process_identifier terminatedProcId
process_expression distribute_sum(const variable_list &sumvars, const process_expression &body1)
data_expression variables_are_equal_to_default_values(const variable_list &vl)
void procstorealGNF(const process_identifier &procsIdDecl, const bool regular)
static bool check_assignment_list(const assignment_list &assignments, const variable_list &parameters)
data_expression RewriteTerm(const data_expression &t)
void alphaconversion(const process_identifier &procId, const variable_list &parameters)
bool all_equal(const atermpp::term_list< T > &l)
static bool alreadypresent(variable &var, const variable_list &vl)
void cluster_actions(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const variable_list &pars)
process_expression transform_initial_distribution_term(const process_expression &t, const std::map< process_identifier, process_pid_pair > &processes_with_initial_distribution)
process_expression create_regular_invocation(process_expression sequence, std::vector< process_identifier > &todo, const variable_list &freevars, const std::set< variable > &variables_bound_in_sum)
process_expression transform_process_arguments_body(const process_expression &t, const std::set< variable > &bound_variables, std::set< process_identifier > &visited_processes)
static assignment_list parameters_to_assignment_list(const variable_list &parameters, const std::set< variable > &variables_bound_in_sum)
assignment_list dummyparameterlist(const stacklisttype &stack, const bool singlestate)
mcrl2::data::rewriter rewr
void make_pCRL_procs(const process_expression &t, std::set< process_identifier > &reachable_process_identifiers)
stackoperations * stack_operations_list
process_expression wraptime(const process_expression &body, const data_expression &time, const variable_list &freevars)
process_identifier split_process(const process_identifier &procId, std::map< process_identifier, process_identifier > &visited_id, std::map< process_expression, process_expression > &visited_proc)
bool mergeoccursin(variable &var, const variable_list &v, variable_list &matchinglist, variable_list &pars, data_expression_list &args, const variable_list &process_parameters)
static bool occursintermlist(const variable &var, const data_expression_list &r)
bool exists_variable_for_sequence(const std::vector< process_instance_assignment > &process_names, process_identifier &result)
std::set< variable > find_free_variables_process(const process_expression &p)
process_expression alphaconversionterm(const process_expression &t, const variable_list &parameters, maintain_variables_in_rhs< mutable_map_substitution<> > sigma)
process_expression putbehind(const process_expression &body1, const process_expression &body2)
std::vector< std::vector< process_instance_assignment > > representedprocesses
assignment_list substitute_assignmentlist(const assignment_list &assignments, const variable_list &parameters, const bool replacelhs, const bool replacerhs, Substitution &sigma)
process_instance_assignment transform_process_instance_to_process_instance_assignment(const process_instance &procId, const std::set< variable > &bound_variables=std::set< variable >())
process_instance_assignment RewriteProcess(const process_instance_assignment &t)
process_identifier delta_process
objectdatatype & objectIndex(const aterm &o)
void insert_summand(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const variable_list &sumvars, const data_expression &condition, const action_list &multiAction, const data_expression &actTime, const stochastic_distribution &distribution, const assignment_list &procargs, const bool has_time, const bool is_deadlock_summand)
variable_list parameters_that_occur_in_body(const variable_list &parameters, const process_expression &body)
process_expression enumerate_distribution_and_sums(const variable_list &sumvars, const variable_list &stochvars, const data_expression &distribution, const process_expression &body)
bool containstimebody(const process_expression &t)
assignment_list make_procargs(const process_expression &t, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const variable_list &vars, const bool regular, const bool singlestate, const variable_list &stochastic_variables)
data_expression adapt_term_to_stack(const data_expression &t, const stacklisttype &stack, const variable_list &vars, const variable_list &stochastic_variables)
data_expression_list processencoding(std::size_t i, const data_expression_list &t1, const stacklisttype &stack)
process_expression RewriteMultAct(const process_expression &t)
void generateLPEmCRLterm(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process_expression &t, const bool regular, const bool rename_variables, variable_list &pars, data_expression_list &init, stochastic_distribution &initial_stochastic_distribution, lps::detail::ultimate_delay &ultimate_delay_condition)
Linearise a process indicated by procIdDecl.
variable_list make_pars(const sort_expression_list &sortlist)
specification_basic_type(const specification_basic_type &)=delete
static data_expression real_times_optimized(const data_expression &r1, const data_expression &r2)
bool occursinpCRLterm(const variable &var, const process_expression &p, const bool strict)
void collectPcrlProcesses(const process_identifier &procDecl, std::vector< process_identifier > &pcrlprocesses)
static std::size_t upperpowerof2(std::size_t i)
void extract_names(const process_expression &sequence, std::vector< process_instance_assignment > &result)
std::map< aterm, objectdatatype > objectdata
action RewriteAction(const action &t)
data_expression_vector adapt_termlist_to_stack(Iterator begin, const Iterator &end, const stacklisttype &stack, const variable_list &vars, const variable_list &stochastic_variables)
data_expression make_procargs_stack(const process_expression &t, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const variable_list &vars, const variable_list &stochastic_variables)
specification_basic_type(const process::action_label_list &as, const std::vector< process_equation > &ps, const variable_list &idvs, const data_specification &ds, const std::set< data::variable > &glob_vars, const t_lin_options &opt, const process_specification &procspec)
variable_list getparameters(const process_expression &multiAction)
data_expression makesingleultimatedelaycondition(const variable_list &sumvars, const variable_list &freevars, const data_expression &condition, const bool has_time, const variable &timevariable, const data_expression &actiontime, variable_list &used_sumvars)
void collectPcrlProcesses_term(const process_expression &body, std::vector< process_identifier > &pcrlprocesses, std::set< process_identifier > &visited)
data_expression representative_generator_internal(const sort_expression &s, const bool allow_dont_care_var=true)
assignment_list processencoding(std::size_t i, const assignment_list &t1, const stacklisttype &stack)
objectdatatype & addMultiAction(const process_expression &multiAction, bool &isnew)
void storeprocs(const std::vector< process_equation > &procs)
process_expression substitute_pCRLproc(const process_expression &p, Substitution &sigma)
void make_parameters_and_sum_variables_unique(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, variable_list &pars, lps::detail::ultimate_delay &ultimate_delay_condition, const std::string &hint="")
const std::set< variable > & get_free_variables(objectdatatype &object)
std::set< variable > global_variables
static data_expression getRHSassignment(const variable &var, const assignment_list &as)
variable_list construct_renaming(const variable_list &pars1, const variable_list &pars2, variable_list &pars3, variable_list &pars4, const bool unique=true)
void determine_process_status(const process_identifier &procDecl, const processstatustype status)
static action_list makemultiaction(const process::action_label_list &actionIds, const data_expression_list &args)
void insertvariables(const variable_list &vars, const bool mustbenew)
data_expression_list RewriteTermList(const data_expression_list &t)
data_specification data
variable_list make_parameters_rec(const data_expression_list &l, std::set< variable > &occurs_set)
static assignment_list filter_assignments(const assignment_list &assignments, const variable_list &parameters)
variable_list merge_var(const variable_list &v1, const variable_list &v2, std::vector< variable_list > &renamings_pars, std::vector< data_expression_list > &renamings_args, data_expression_list &conditionlist, const variable_list &process_parameters)
bool containstimebody(const process_expression &t, bool *stable, std::set< process_identifier > &visited, bool allowrecursion, bool &contains_if_then)
static assignment_list sort_assignments(const assignment_list &ass, const variable_list &parameters)
assignment_list find_dummy_arguments(const variable_list &parlist, const assignment_list &args, const std::set< variable > &free_variables_in_body, const variable_list &stochastic_variables)
process_identifier tau_process
static sort_expression_list get_sorts(const List &l)
std::vector< process_identifier > seq_varnames
void storeact(const process::action_label_list &acts)
bool is_global_variable(const data_expression &d) const
static bool occursin(const variable &name, const variable_list &pars)
bool canterminatebody(const process_expression &t, bool &stable, std::set< process_identifier > &visited, const bool allowrecursion)
void AddTerminationActionIfNecessary(const stochastic_action_summand_vector &summands)
bool determinewhetherprocessescontaintime(const process_identifier &procId)
void filter_vars_by_assignmentlist(const assignment_list &assignments, const variable_list &parameters, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
data_expression_list addcondition(const variable_list &matchinglist, const data_expression_list &conditionlist)
void calculate_communication_merge_deadlock_summands(const deadlock_summand_vector &deadlock_summands1, const deadlock_summand_vector &deadlock_summands2, const stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)
void transform(const process_identifier &init, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, variable_list &parameters, data_expression_list &initial_state, stochastic_distribution &initial_stochastic_distribution)
process_expression obtain_initial_distribution(const process_identifier &procId)
objectdatatype & insertAction(const action_label &actionId)
Expression replace_variables_capture_avoiding_alt(const Expression &e, Substitution &sigma)
process_instance_assignment expand_process_instance_assignment(const process_instance_assignment &t, std::set< process_identifier > &visited_processes)
assignment_list pushdummy_regular(const variable_list &pars, const stacklisttype &stack, const variable_list &stochastic_variables)
std::set< data::variable > sigma_variables(const SUBSTITUTION &sigma)
assignment_list argscollect_regular(const process_expression &t, const variable_list &vl, const std::set< variable > &variables_bound_in_sum)
static data_expression_list getarguments(const action_list &multiAction)
lps::detail::ultimate_delay getUltimateDelayCondition(const stochastic_action_summand_vector &action_summands, const deadlock_summand_vector &deadlock_summands, const variable_list &freevars)
@ multiAction
Definition linearise.cpp:76
@ GNFalpha
Definition linearise.cpp:78
@ mCRLbusy
Definition linearise.cpp:73
@ mCRL
Definition linearise.cpp:71
@ GNF
Definition linearise.cpp:77
@ mCRLlin
Definition linearise.cpp:74
@ pCRL
Definition linearise.cpp:75
@ mCRLdone
Definition linearise.cpp:72
@ GNFbusy
Definition linearise.cpp:79
@ unknown
Definition linearise.cpp:70
@ error
Definition linearise.cpp:80
@ func
Definition linearise.cpp:89
@ act
Definition linearise.cpp:90
@ sorttype
Definition linearise.cpp:93
@ multiact
Definition linearise.cpp:94
@ proc
Definition linearise.cpp:91
@ _map
Definition linearise.cpp:88
@ none
Definition linearise.cpp:87
@ variable_
Definition linearise.cpp:92
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
The main namespace for the aterm++ library.
Definition algorithm.h:21
term_list< aterm > aterm_list
A term_list with elements of type aterm.
Definition aterm_list.h:497
const atermpp::function_symbol & function_symbol_TimedMultAct()
const atermpp::function_symbol & function_symbol_BInit()
const atermpp::function_symbol & function_symbol_Choice()
const atermpp::function_symbol & function_symbol_UntypedProcessAssignment()
const atermpp::function_symbol & function_symbol_Allow()
const atermpp::function_symbol & function_symbol_Merge()
const atermpp::function_symbol & function_symbol_Rename()
const atermpp::function_symbol & function_symbol_ActId()
const atermpp::function_symbol & function_symbol_Block()
const atermpp::function_symbol & function_symbol_Sum()
const atermpp::function_symbol & function_symbol_AtTime()
const atermpp::function_symbol & function_symbol_GlobVarSpec()
const atermpp::function_symbol & function_symbol_Comm()
const atermpp::function_symbol & function_symbol_Action()
const atermpp::function_symbol & function_symbol_Distribution()
const atermpp::function_symbol & function_symbol_LinearProcessInit()
const atermpp::function_symbol & function_symbol_RenameExpr()
const atermpp::function_symbol & function_symbol_MultActName()
const atermpp::function_symbol & function_symbol_Process()
const atermpp::function_symbol & function_symbol_IfThenElse()
const atermpp::function_symbol & function_symbol_CommExpr()
const atermpp::function_symbol & function_symbol_Sync()
const atermpp::function_symbol & function_symbol_Seq()
const atermpp::function_symbol & function_symbol_ProcVarId()
const atermpp::function_symbol & function_symbol_LinProcSpec()
const atermpp::function_symbol & function_symbol_ProcessAssignment()
const atermpp::function_symbol & function_symbol_IfThen()
const atermpp::function_symbol & function_symbol_LinearProcessSummand()
const atermpp::function_symbol & function_symbol_Hide()
const atermpp::function_symbol & function_symbol_StochasticOperator()
const atermpp::function_symbol & function_symbol_ActSpec()
const atermpp::function_symbol & function_symbol_LMerge()
atermpp::term_list< identifier_string > identifier_string_list
\brief list of identifier_strings
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
atermpp::function_symbol linear_inequality_equal()
const lhs_t map_to_lhs_type(const map_based_lhs_t &lhs)
void optimized_forall(typename TermTraits::term_type &result, const typename TermTraits::variable_sequence_type &v, const typename TermTraits::term_type &arg, bool remove_variables, bool empty_domain_allowed, TermTraits)
Make a universal quantification.
void split_condition(const data_expression &e, std::vector< data_expression_list > &real_conditions, std::vector< data_expression > &non_real_conditions)
This function first splits the given condition e into real conditions and non real conditions....
const lhs_t remove_variable_and_divide(const lhs_t &lhs, const variable &v, const data_expression &f, const rewriter &r)
data_expression negate_inequality(const data_expression &e)
const lhs_t subtract(const lhs_t &argument, const lhs_t &e, const rewriter &r)
const lhs_t map_to_lhs_type(const map_based_lhs_t &lhs, const data_expression &factor, const rewriter &r)
void optimized_exists(typename TermTraits::term_type &result, const typename TermTraits::variable_sequence_type &v, const typename TermTraits::term_type &arg, bool remove_variables, bool empty_domain_allowed, TermTraits)
Make an existential quantification.
void optimized_or(typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits)
Make a disjunction.
atermpp::function_symbol linear_inequality_less()
void emplace_back_if_not_zero(std::vector< detail::variable_with_a_rational_factor > &r, const variable &v, const data_expression &f)
std::string pp(const detail::comparison_t t)
variable_list set_intersection(const variable_list &x, const variable_list &y)
Returns the intersection of two unordered sets, that are stored in ATerm lists.
lhs_t set_factor_for_a_variable(const lhs_t &lhs, const variable &x, const data_expression &e)
void optimized_imp(typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits t)
Make an implication.
const lhs_t add(const data_expression &v, const lhs_t &argument, const rewriter &r)
const data_expression & else_part(const data_expression &e)
bool is_well_formed(const lhs_t &lhs)
bool is_inequality(const data_expression &e)
Determine whether a data expression is an inequality.
detail::comparison_t negate(const detail::comparison_t t)
const data_expression & condition_part(const data_expression &e)
std::map< variable, data_expression > map_based_lhs_t
const lhs_t add(const lhs_t &argument, const lhs_t &e, const rewriter &r)
atermpp::aterm data_specification_to_aterm(const data_specification &s)
Definition data_io.cpp:44
atermpp::function_symbol linear_inequality_less_equal()
lhs_t meta_operation_lhs(const lhs_t &argument1, const lhs_t &argument2, OPERATION operation, const rewriter &r)
const lhs_t subtract(const lhs_t &argument, const data_expression &v, const rewriter &r)
std::string pp(const detail::lhs_t &lhs)
const lhs_t meta_operation_constant(const lhs_t &argument, const data_expression &v, const rewriter &r)
const data_expression & then_part(const data_expression &e)
void optimized_not(typename TermTraits::term_type &result, const typename TermTraits::term_type &arg, TermTraits)
static bool split_condition_aux(const data_expression &e, std::vector< data_expression_list > &real_conditions, std::vector< data_expression_list > &non_real_conditions, const bool negate=false)
Splits a condition in expressions ranging over reals and the others.
void set_factor_for_a_variable(detail::map_based_lhs_t &new_lhs, const variable &x, const data_expression &e)
variable_list set_difference(const variable_list &x, const variable_list &y)
Returns the difference of two unordered sets, that are stored in aterm lists.
void optimized_and(typename TermTraits::term_type &result, const typename TermTraits::term_type &left, const typename TermTraits::term_type &right, TermTraits)
Make a conjunction and optimize it if possible.
const lhs_t multiply(const lhs_t &argument, const data_expression &v, const rewriter &r)
atermpp::function_symbol f_variable_with_a_rational_factor()
const lhs_t divide(const lhs_t &argument, const data_expression &v, const rewriter &r)
A collection of utilities for lazy expression construction.
data_expression and_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p or q.
data_expression or_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p and q.
Namespace for system defined sort bool_.
Definition bool.h:32
bool is_or_application(const atermpp::aterm &e)
Recogniser for application of ||.
Definition bool.h:345
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition bool.h:493
bool is_implies_application(const atermpp::aterm &e)
Recogniser for application of =>.
Definition bool.h:409
application not_(const data_expression &arg0)
Application of function symbol !.
Definition bool.h:197
application or_(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ||.
Definition bool.h:324
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
bool is_and_application(const atermpp::aterm &e)
Recogniser for application of &&.
Definition bool.h:281
bool is_not_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition bool.h:217
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition bool.h:481
Namespace for system defined sort int_.
bool is_cint_application(const atermpp::aterm &e)
Recogniser for application of @cInt.
Definition int1.h:124
Namespace for system defined sort nat.
bool is_natural_constant(const data_expression &n)
Determines whether n is a natural constant.
Namespace for system defined sort pos.
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:45
Namespace for system defined sort real_.
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1059
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1237
bool is_zero(const atermpp::aterm &e)
function_symbol divides(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1407
data_expression & real_one()
bool is_one(const atermpp::aterm &e)
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
Definition real1.h:1136
data_expression & real_zero()
bool is_creal_application(const atermpp::aterm &e)
Recogniser for application of @cReal.
Definition real1.h:153
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1152
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:48
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real1.h:58
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
Definition real1.h:1285
bool is_larger_zero(const atermpp::aterm &e)
Functions that returns true if e is a closed real number larger than zero.
function_symbol abs(const sort_expression &s0)
Definition real1.h:735
bool is_times_application(const atermpp::aterm &e)
Recogniser for application of *.
Definition real1.h:1306
function_symbol negate(const sort_expression &s0)
Definition real1.h:810
bool is_negate_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:877
bool is_minus_application(const atermpp::aterm &e)
Recogniser for application of -.
Definition real1.h:1221
Namespace for all data library functionality.
Definition data.cpp:22
linear_inequality subtract(const linear_inequality &e1, const linear_inequality &e2, const data_expression &f1, const data_expression &f2, const rewriter &r)
Subtract the given equality, multiplied by f1/f2. The result is e1-(f1/f2)e2,.
std::vector< assignment > assignment_vector
\brief vector of assignments
Definition assignment.h:149
application real_times(const data_expression &arg0, const data_expression &arg1)
const data::data_expression & undefined_real()
Returns a data expression of type Real that corresponds to 'undefined'.
Definition undefined.h:66
data_expression & real_one()
void optimized_exists_no_empty_domain(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make an existential quantification.
void optimized_exists(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make an existential quantification.
bool is_closed_real_number(const data_expression &e)
bool is_application(const data_expression &t)
Returns true if the term t is an application.
application real_plus(const data_expression &arg0, const data_expression &arg1)
atermpp::term_list< function_symbol > function_symbol_list
\brief list of function_symbols
data_expression & real_minus_one()
bool is_simple_substitution(const map_substitution< AssociativeContainer > &sigma)
void optimized_or(Term &result, const Term &p, const Term &q)
Make a conjunction, and optimize if possible.
bool is_positive(const data_expression &e, const rewriter &r)
bool is_where_clause(const atermpp::aterm &x)
Returns true if the term t is a where clause.
application less_equal(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <=.
Definition standard.h:295
std::string pp(const data::variable &x)
Definition data.cpp:81
application real_abs(const data_expression &arg)
void count_occurrences(const std::vector< linear_inequality > &inequalities, std::map< variable, std::size_t > &nr_positive_occurrences, std::map< variable, std::size_t > &nr_negative_occurrences, const rewriter &r)
application less(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <.
Definition standard.h:258
std::set< data::variable > substitution_variables(const map_substitution< AssociativeContainer > &sigma)
std::string pp_vector(const TYPE &inequalities)
Print the vector of inequalities to stderr in readable form.
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
std::vector< variable > variable_vector
\brief vector of variables
Definition variable.h:89
application if_(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol if.
Definition standard.h:219
void remove_redundant_inequalities(const std::vector< linear_inequality > &inequalities, std::vector< linear_inequality > &resulting_inequalities, const rewriter &r)
Remove every redundant inequality from a vector of inequalities.
application real_minus(const data_expression &arg0, const data_expression &arg1)
atermpp::term_list< sort_expression > sort_expression_list
\brief list of sort_expressions
std::vector< data_expression > data_expression_vector
\brief vector of data_expressions
static void pivot_and_update(const variable &xi, const variable &xj, const data_expression &v, const data_expression &v_delta_correction, std::map< variable, data_expression > &beta, std::map< variable, data_expression > &beta_delta_correction, std::set< variable > &basic_variables, std::map< variable, detail::lhs_t > &working_equalities, const rewriter &r)
map_substitution< AssociativeContainer > make_map_substitution(const AssociativeContainer &m)
Utility function for creating a map_substitution.
void fourier_motzkin(const data_expression &e_in, const variable_list &vars_in, data_expression &e_out, variable_list &vars_out, const rewriter &r)
Eliminate variables from a data expression using Gauss elimination and Fourier-Motzkin elimination.
bool is_simple_substitution(const assignment_sequence_substitution &sigma)
std::string pp(const linear_inequality &l)
application real_divides(const data_expression &arg0, const data_expression &arg1)
std::set< variable > gauss_elimination(const std::vector< linear_inequality > &inequalities, std::vector< linear_inequality > &resulting_equalities, std::vector< linear_inequality > &resulting_inequalities, Variable_iterator variables_begin, Variable_iterator variables_end, const rewriter &r)
Try to eliminate variables from a system of inequalities using Gauss elimination.
void optimized_imp(Term &result, const Term &p, const Term &q)
Make an implication.
std::vector< structured_sort_constructor > structured_sort_constructor_vector
\brief vector of structured_sort_constructors
bool is_zero(const data_expression &e)
bool is_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
void fourier_motzkin(const std::vector< linear_inequality > &inequalities_in, Data_variable_iterator variables_begin, Data_variable_iterator variables_end, std::vector< linear_inequality > &resulting_inequalities, const rewriter &r)
atermpp::term_list< data_expression > data_expression_list
\brief list of data_expressions
data_expression rewrite_with_memory(const data_expression &t, const rewriter &r)
data_expression & real_zero()
bool is_a_redundant_inequality(const std::vector< linear_inequality > &inequalities, const std::vector< linear_inequality > ::iterator i, const rewriter &r)
Indicate whether an inequality from a set of inequalities is redundant.
application greater(const data_expression &arg0, const data_expression &arg1)
Application of function symbol >
Definition standard.h:332
bool is_untyped_data_parameter(const atermpp::aterm &x)
void optimized_forall_no_empty_domain(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make a universal quantification.
atermpp::term_list< variable > variable_list
\brief list of variables
bool is_exists(const atermpp::aterm &x)
Returns true if the term t is an existential quantification.
application real_negate(const data_expression &arg)
atermpp::term_list< assignment > assignment_list
\brief list of assignments
Definition assignment.h:146
bool is_inconsistent(const std::vector< linear_inequality > &inequalities_in, const rewriter &r, const bool use_cache=true)
Determine whether a list of data expressions is inconsistent.
std::string pp(const data::sort_expression &x)
Definition data.cpp:69
data_expression max(const data_expression &e1, const data_expression &e2, const rewriter &)
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
bool is_negative(const data_expression &e, const rewriter &r)
const data_expression_list & variable_list_to_data_expression_list(const variable_list &l)
Transform a variable_list into a data_expression_list.
application equal_to(const data_expression &arg0, const data_expression &arg1)
Application of function symbol ==.
Definition standard.h:144
void optimized_not(Term &result, const Term &arg)
Make a negation.
void optimized_and(Term &result, const Term &p, const Term &q)
Make a conjunction, and optimize if possible.
data_expression min(const data_expression &e1, const data_expression &e2, const rewriter &)
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
atermpp::term_list< untyped_identifier_assignment > untyped_identifier_assignment_list
\brief list of untyped_identifier_assignments
Definition assignment.h:242
std::vector< structured_sort_constructor_argument > structured_sort_constructor_argument_vector
\brief vector of structured_sort_constructor_arguments
void optimized_forall(Term &result, const VariableSequence &l, const Term &p, bool remove_variables=false)
Make a universal quantification.
std::string pp(const data::data_expression &x)
Definition data.cpp:52
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
atermpp::term_list< structured_sort_constructor > structured_sort_constructor_list
\brief list of structured_sort_constructors
@ warning
Definition logger.h:34
@ verbose
Definition logger.h:37
bool mCRL2logEnabled(const log_level_t level)
Definition logger.h:383
void replace_global_variables(Specification &lpsspec, const data::mutable_map_substitution<> &sigma)
Applies a global variable substitution to an LPS.
data::mutable_map_substitution instantiate_global_variables(Specification &lpsspec)
Eliminates the global variables of an LPS, by substituting a constant value for them....
Summand make_action_summand(const data::variable_list &, const data::data_expression &, const multi_action &, const data::assignment_list &, const stochastic_distribution &)
The main namespace for the LPS library.
Definition constelm.h:21
std::vector< multi_action > multi_action_vector
\brief vector of multi_actions
std::string pp(const lps::stochastic_distribution &x)
Definition lps.cpp:34
std::set< data::variable > find_all_variables(const lps::linear_process &x)
Definition lps.cpp:44
void make_stochastic_distribution(atermpp::aterm &t, const ARGUMENTS &... args)
std::set< data::sort_expression > find_sort_expressions(const lps::stochastic_specification &x)
Definition lps.cpp:43
std::set< data::variable > find_free_variables(const lps::stochastic_specification &x)
Definition lps.cpp:53
void complete_data_specification(stochastic_specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
std::vector< stochastic_action_summand > stochastic_action_summand_vector
\brief vector of stochastic_action_summands
std::string pp_with_summand_numbers(const specification &x)
Definition lps.cpp:74
std::string pp(const lps::process_initializer &x)
Definition lps.cpp:31
bool operator!=(const stochastic_specification &spec1, const stochastic_specification &spec2)
Inequality operator.
std::set< data::variable > find_all_variables(const lps::stochastic_specification &x)
Definition lps.cpp:47
bool check_well_typedness(const specification &x)
Definition lps.cpp:102
void swap(stochastic_distribution &t1, stochastic_distribution &t2)
\brief swap overload
void complete_data_specification(specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
std::set< data::variable > find_free_variables(const lps::linear_process &x)
Definition lps.cpp:50
bool is_specification(const atermpp::aterm &x)
Test for a specification expression.
atermpp::term_list< process_initializer > process_initializer_list
\brief list of process_initializers
std::string pp(const lps::stochastic_specification &x)
Definition lps.cpp:37
bool check_well_typedness(const linear_process &x)
Definition lps.cpp:92
atermpp::term_list< action_summand > action_summand_list
\brief list of action_summands
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)
std::set< data::function_symbol > find_function_symbols(const lps::stochastic_specification &x)
Definition lps.cpp:59
bool occursinterm(const data::data_expression &t, const data::variable &var)
std::string pp(const lps::linear_process &x)
Definition lps.cpp:29
std::vector< deadlock_summand > deadlock_summand_vector
\brief vector of deadlock_summands
void remove_parameters(Object &x, const std::set< data::variable > &to_be_removed)
Rewrites an LPS data type.
Definition remove.h:190
void replace_variables_capture_avoiding(T &x, Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
atermpp::aterm specification_to_aterm(const specification_base< LinearProcess, InitialProcessExpression > &spec)
Conversion to aterm.
std::set< process::action_label > find_action_labels(const lps::process_initializer &x)
Definition lps.cpp:63
std::string pp(const lps::multi_action &x)
Definition lps.cpp:30
std::set< data::variable > find_free_variables(const lps::specification &x)
Definition lps.cpp:52
void constelm(Specification &spec, const DataRewriter &R, bool instantiate_global_variables=false)
Removes zero or more constant parameters from the specification spec.
Definition constelm.h:271
atermpp::term_list< multi_action > multi_action_list
\brief list of multi_actions
std::string pp(const lps::specification &x)
Definition lps.cpp:32
void normalize_sorts(lps::specification &x, const data::sort_specification &)
Definition lps.cpp:39
bool operator==(const specification &spec1, const specification &spec2)
Equality operator.
std::set< process::action_label > find_action_labels(const lps::linear_process &x)
Definition lps.cpp:62
lps::multi_action normalize_sorts(const lps::multi_action &x, const data::sort_specification &sortspec)
Definition lps.cpp:38
void swap(process_initializer &t1, process_initializer &t2)
\brief swap overload
std::set< data::function_symbol > find_function_symbols(const lps::specification &x)
Definition lps.cpp:58
atermpp::term_list< stochastic_distribution > stochastic_distribution_list
\brief list of stochastic_distributions
bool operator==(const stochastic_specification &spec1, const stochastic_specification &spec2)
std::set< data::variable > find_free_variables(const lps::multi_action &x)
Definition lps.cpp:55
void swap(action_summand &t1, action_summand &t2)
\brief swap overload
T replace_variables_capture_avoiding(const T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
void remove_redundant_assignments(Specification &lpsspec)
Removes redundant assignments of the form x = x from an LPS specification.
Definition remove.h:247
void swap(multi_action &t1, multi_action &t2)
\brief swap overload
bool operator!=(const specification &spec1, const specification &spec2)
Inequality operator.
void normalize_sorts(lps::stochastic_specification &x, const data::sort_specification &)
Definition lps.cpp:40
std::set< data::variable > find_free_variables(const lps::process_initializer &x)
Definition lps.cpp:56
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....
bool is_stochastic_distribution(const atermpp::aterm &x)
specification remove_stochastic_operators(const stochastic_specification &spec)
Converts a stochastic specification to a specification. Throws an exception if non-empty distribution...
bool operator==(const action_summand &x, const action_summand &y)
Equality operator of action summands.
stochastic_distribution replace_variables_capture_avoiding(const stochastic_distribution &x, data::data_expression_list &pars, Substitution &sigma, data::set_identifier_generator &id_generator)
bool is_process_initializer(const atermpp::aterm &x)
void remove_singleton_sorts(Specification &spec)
Removes parameters with a singleton sort from a linear process specification.
Definition remove.h:211
bool check_well_typedness(const Object &o)
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...
Definition remove.h:229
mcrl2::lps::stochastic_specification linearise(const mcrl2::process::process_specification &type_checked_spec, const mcrl2::lps::t_lin_options &lin_options=t_lin_options())
Linearises a process specification.
void rename(const process::rename_expression_list &renamings, lps::stochastic_action_summand_vector &action_summands)
std::vector< process_initializer > process_initializer_vector
\brief vector of process_initializers
std::set< data::variable > find_all_variables(const lps::multi_action &x)
Definition lps.cpp:49
atermpp::aterm linear_process_to_aterm(const linear_process_base< ActionSummand > &p)
Conversion to aterm.
std::set< data::sort_expression > find_sort_expressions(const lps::specification &x)
Definition lps.cpp:42
void make_process_initializer(atermpp::aterm &t, EXPRESSION_LIST args)
void make_multi_action(atermpp::aterm &t, const ARGUMENTS &... args)
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 equ...
std::vector< action_summand > action_summand_vector
\brief vector of action_summands
void remove_trivial_summands(Specification &spec)
Removes summands with condition equal to false from a linear process specification.
Definition remove.h:199
bool operator<(const action_summand &x, const action_summand &y)
Comparison operator for action summands.
T replace_variables_capture_avoiding(const T &x, Substitution &sigma, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
std::vector< stochastic_distribution > stochastic_distribution_vector
\brief vector of stochastic_distributions
std::set< data::variable > find_all_variables(const lps::specification &x)
Definition lps.cpp:46
bool check_well_typedness(const stochastic_specification &x)
Definition lps.cpp:107
atermpp::aterm action_summand_to_aterm(const action_summand &s)
Conversion to aterm.
stochastic_distribution replace_variables_capture_avoiding(const stochastic_distribution &x, data::data_expression_list &pars, Substitution &sigma)
bool check_well_typedness(const stochastic_linear_process &x)
Definition lps.cpp:97
lps::multi_action translate_user_notation(const lps::multi_action &x)
Definition lps.cpp:41
std::set< core::identifier_string > find_identifiers(const lps::stochastic_specification &x)
Definition lps.cpp:61
std::string pp(const lps::action_summand &x)
Definition lps.cpp:26
std::set< core::identifier_string > find_identifiers(const lps::specification &x)
Definition lps.cpp:60
std::string pp_with_summand_numbers(const stochastic_specification &x)
Definition lps.cpp:83
std::set< process::action_label > find_action_labels(const lps::specification &x)
Definition lps.cpp:64
bool is_multi_action(const atermpp::aterm &x)
bool is_linear_process(const atermpp::aterm &x)
Test for a linear_process expression.
The main namespace for the Process library.
bool is_at(const atermpp::aterm &x)
void swap(delta &t1, delta &t2)
\brief swap overload
std::string pp(const process::comm &x)
Definition process.cpp:43
void swap(process_instance &t1, process_instance &t2)
\brief swap overload
void make_allow(atermpp::aterm &t, const ARGUMENTS &... args)
process::action normalize_sorts(const process::action &x, const data::sort_specification &sortspec)
Definition process.cpp:66
void normalize_sorts(process::process_equation_vector &x, const data::sort_specification &sortspec)
Definition process.cpp:68
std::set< data::variable > find_free_variables(const process::action &x)
Definition process.cpp:78
std::string pp(const process::action_vector &x)
Definition process.cpp:26
void make_choice(atermpp::aterm &t, const ARGUMENTS &... args)
std::vector< process_expression > process_expression_vector
\brief vector of process_expressions
void swap(action_label &t1, action_label &t2)
\brief swap overload
void make_process_identifier(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_process_instance(const atermpp::aterm &x)
std::string pp(const process::block &x)
Definition process.cpp:40
void swap(hide &t1, hide &t2)
\brief swap overload
process::action_label_list normalize_sorts(const process::action_label_list &x, const data::sort_specification &sortspec)
Definition process.cpp:67
std::string pp(const process::untyped_process_assignment &x)
Definition process.cpp:65
std::string pp(const process::at &x)
Definition process.cpp:39
void make_merge(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const process::stochastic_operator &x)
Definition process.cpp:60
void make_at(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_process_expression(const atermpp::aterm &x)
bool is_process_instance_assignment(const atermpp::aterm &x)
void swap(sync &t1, sync &t2)
\brief swap overload
void swap(communication_expression &t1, communication_expression &t2)
\brief swap overload
bool is_tau(const atermpp::aterm &x)
std::string pp(const process::process_instance &x)
Definition process.cpp:54
void swap(merge &t1, merge &t2)
\brief swap overload
void make_action(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const process::action_label_list &x)
Definition process.cpp:27
bool is_seq(const atermpp::aterm &x)
void make_sync(atermpp::aterm &t, const ARGUMENTS &... args)
std::vector< rename_expression > rename_expression_vector
\brief vector of rename_expressions
bool is_merge(const atermpp::aterm &x)
std::string pp(const process::choice &x)
Definition process.cpp:42
std::string pp(const process::process_instance_assignment &x)
Definition process.cpp:55
std::set< data::sort_expression > find_sort_expressions(const process::action_label_list &x)
Definition process.cpp:73
void make_if_then_else(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_action_label(const atermpp::aterm &x)
std::string pp(const process::rename_expression &x)
Definition process.cpp:58
void make_hide(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(choice &t1, choice &t2)
\brief swap overload
bool is_communication_expression(const atermpp::aterm &x)
bool is_allow(const atermpp::aterm &x)
atermpp::term_list< rename_expression > rename_expression_list
\brief list of rename_expressions
std::vector< communication_expression > communication_expression_vector
\brief vector of communication_expressions
void swap(if_then &t1, if_then &t2)
\brief swap overload
void swap(rename &t1, rename &t2)
\brief swap overload
std::string pp(const process::process_identifier &x)
Definition process.cpp:53
std::string pp(const process::action &x)
Definition process.cpp:35
void make_if_then(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(comm &t1, comm &t2)
\brief swap overload
void swap(tau &t1, tau &t2)
\brief swap overload
bool is_bounded_init(const atermpp::aterm &x)
std::string pp(const process::seq &x)
Definition process.cpp:59
bool is_delta(const atermpp::aterm &x)
std::set< data::sort_expression > find_sort_expressions(const process::process_expression &x)
Definition process.cpp:75
void swap(left_merge &t1, left_merge &t2)
\brief swap overload
void make_block(atermpp::aterm &t, const ARGUMENTS &... args)
process::process_expression translate_user_notation(const process::process_expression &x)
Definition process.cpp:71
bool is_sum(const atermpp::aterm &x)
void swap(bounded_init &t1, bounded_init &t2)
\brief swap overload
std::string pp(const process::delta &x)
Definition process.cpp:45
bool is_process_identifier(const atermpp::aterm &x)
bool is_block(const atermpp::aterm &x)
void swap(stochastic_operator &t1, stochastic_operator &t2)
\brief swap overload
void swap(sum &t1, sum &t2)
\brief swap overload
bool is_if_then_else(const atermpp::aterm &x)
atermpp::term_list< process_expression > process_expression_list
\brief list of process_expressions
void make_action_label(atermpp::aterm &t, const ARGUMENTS &... args)
process::action translate_user_notation(const process::action &x)
Definition process.cpp:70
bool is_comm(const atermpp::aterm &x)
void alphabet_reduce(process_specification &procspec, std::size_t duplicate_equation_limit=(std::numeric_limits< size_t >::max)())
Applies alphabet reduction to a process specification.
Definition process.cpp:83
bool is_action(const atermpp::aterm &x)
std::string pp(const process::left_merge &x)
Definition process.cpp:49
std::string pp(const process::communication_expression &x)
Definition process.cpp:44
void swap(allow &t1, allow &t2)
\brief swap overload
bool is_left_merge(const atermpp::aterm &x)
std::string pp(const process::hide &x)
Definition process.cpp:46
atermpp::term_list< action_label > action_label_list
\brief list of action_labels
std::string pp(const process::process_identifier_list &x)
Definition process.cpp:29
void make_communication_expression(atermpp::aterm &t, const ARGUMENTS &... args)
std::vector< action > action_vector
\brief vector of actions
void swap(seq &t1, seq &t2)
\brief swap overload
void make_stochastic_operator(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_action_name_multiset(const atermpp::aterm &x)
std::string pp(const process::sum &x)
Definition process.cpp:61
std::string pp(const process::allow &x)
Definition process.cpp:38
std::string pp(const process::if_then_else &x)
Definition process.cpp:48
std::string pp(const process::process_expression_list &x)
Definition process.cpp:31
atermpp::term_list< action > action_list
\brief list of actions
std::string pp(const process::rename &x)
Definition process.cpp:57
void swap(process_expression &t1, process_expression &t2)
\brief swap overload
void make_process_instance(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const process::action_name_multiset &x)
Definition process.cpp:37
std::string pp(const process::tau &x)
Definition process.cpp:63
bool is_hide(const atermpp::aterm &x)
std::string pp(const process::process_expression &x)
Definition process.cpp:52
void swap(if_then_else &t1, if_then_else &t2)
\brief swap overload
void swap(block &t1, block &t2)
\brief swap overload
bool is_if_then(const atermpp::aterm &x)
std::string pp(const process::merge &x)
Definition process.cpp:50
std::string pp(const process::bounded_init &x)
Definition process.cpp:41
void make_untyped_process_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
void make_process_instance_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_choice(const atermpp::aterm &x)
void make_comm(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const process::action_list &x)
Definition process.cpp:25
bool is_stochastic_operator(const atermpp::aterm &x)
void swap(process_instance_assignment &t1, process_instance_assignment &t2)
\brief swap overload
void swap(process_identifier &t1, process_identifier &t2)
\brief swap overload
atermpp::term_list< process_identifier > process_identifier_list
\brief list of process_identifiers
void swap(action_name_multiset &t1, action_name_multiset &t2)
\brief swap overload
void make_bounded_init(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_rename_expression(const atermpp::aterm &x)
std::vector< action_name_multiset > action_name_multiset_vector
\brief vector of action_name_multisets
atermpp::term_list< communication_expression > communication_expression_list
\brief list of communication_expressions
void make_rename_expression(atermpp::aterm &t, const ARGUMENTS &... args)
void make_action_name_multiset(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(rename_expression &t1, rename_expression &t2)
\brief swap overload
atermpp::term_list< action_name_multiset > action_name_multiset_list
\brief list of action_name_multisets
std::set< data::variable > find_all_variables(const process::action &x)
Definition process.cpp:77
bool is_rename(const atermpp::aterm &x)
std::vector< action_label > action_label_vector
\brief vector of action_labels
bool is_untyped_process_assignment(const atermpp::aterm &x)
void make_rename(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const process::if_then &x)
Definition process.cpp:47
void make_seq(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_sync(const atermpp::aterm &x)
void make_sum(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const process::action_label &x)
Definition process.cpp:36
std::string pp(const process::sync &x)
Definition process.cpp:62
bool equal_signatures(const action &a, const action &b)
Compares the signatures of two actions.
void swap(at &t1, at &t2)
\brief swap overload
void swap(action &t1, action &t2)
\brief swap overload
std::vector< process_identifier > process_identifier_vector
\brief vector of process_identifiers
void swap(untyped_process_assignment &t1, untyped_process_assignment &t2)
\brief swap overload
void make_left_merge(atermpp::aterm &t, const ARGUMENTS &... args)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
void swap(atermpp::aterm &t1, atermpp::aterm &t2) noexcept
Swaps two term_applss.
Definition aterm.h:475
static const atermpp::aterm Delta
static const atermpp::aterm UntypedProcessAssignment
static const atermpp::aterm Distribution
static const atermpp::aterm Allow
static const atermpp::aterm RenameExpr
static const atermpp::aterm Tau
static const atermpp::aterm ActId
static const atermpp::aterm Hide
static const atermpp::aterm LinearProcessInit
static const atermpp::aterm Rename
static const atermpp::aterm Process
static const atermpp::aterm IfThen
static const atermpp::aterm StochasticOperator
static const atermpp::aterm BInit
static const atermpp::aterm Merge
static const atermpp::aterm Action
static const atermpp::aterm MultActName
static const atermpp::aterm AtTime
static const atermpp::aterm Choice
static const atermpp::aterm Comm
static const atermpp::aterm ProcessAssignment
static const atermpp::aterm Sync
static const atermpp::aterm LMerge
static const atermpp::aterm ProcVarId
static const atermpp::aterm ProcExpr
static const atermpp::aterm Seq
static const atermpp::aterm Sum
static const atermpp::aterm Block
static const atermpp::aterm CommExpr
static const atermpp::aterm IfThenElse
static const atermpp::function_symbol Rename
static const atermpp::function_symbol Allow
static const atermpp::function_symbol Delta
static const atermpp::function_symbol ProcessAssignment
static const atermpp::function_symbol IfThenElse
static const atermpp::function_symbol Hide
static const atermpp::function_symbol UntypedProcessAssignment
static const atermpp::function_symbol ActId
static const atermpp::function_symbol TimedMultAct
static const atermpp::function_symbol ProcVarId
static const atermpp::function_symbol BInit
static const atermpp::function_symbol RenameExpr
static const atermpp::function_symbol StochasticOperator
static const atermpp::function_symbol LinProcSpec
static const atermpp::function_symbol Choice
static const atermpp::function_symbol Sync
static const atermpp::function_symbol Sum
static const atermpp::function_symbol Action
static const atermpp::function_symbol CommExpr
static const atermpp::function_symbol Comm
static const atermpp::function_symbol AtTime
static const atermpp::function_symbol MultActName
static const atermpp::function_symbol LinearProcess
static const atermpp::function_symbol Process
static const atermpp::function_symbol Merge
static const atermpp::function_symbol LinearProcessInit
static const atermpp::function_symbol Block
static const atermpp::function_symbol Seq
static const atermpp::function_symbol IfThen
static const atermpp::function_symbol Distribution
static const atermpp::function_symbol LMerge
static const atermpp::function_symbol Tau
Contains type information for terms.
Definition term_traits.h:24
Substitution that maps data variables to data expressions. The substitution is stored as an assignmen...
assignment_sequence_substitution(const assignment_list &assignments_)
const data_expression & operator()(const variable &v) const
A unary function that can be used in combination with replace_data_expressions to eliminate real numb...
fourier_motzkin_sigma(const rewriter &rewr_)
const data_expression operator()(const data_expression &d) const
const data_expression apply(const abstraction &d, bool negate) const
Generic substitution function. The substitution is stored as a mapping of variables to expressions.
const expression_type operator()(const variable_type &v) const
const AssociativeContainer & m_map
map_substitution(const AssociativeContainer &m)
AssociativeContainer::mapped_type expression_type
AssociativeContainer::key_type variable_type
void update(lps::action_summand &x)
Definition builder.h:230
void apply(T &result, const lps::stochastic_process_initializer &x)
Definition builder.h:318
void update(lps::linear_process &x)
Definition builder.h:254
void apply(T &result, const lps::multi_action &x)
Definition builder.h:212
void apply(T &result, const lps::stochastic_distribution &x)
Definition builder.h:273
void update(lps::specification &x)
Definition builder.h:262
void update(lps::deadlock &x)
Definition builder.h:202
void update(lps::stochastic_linear_process &x)
Definition builder.h:299
void apply(T &result, const lps::process_initializer &x)
Definition builder.h:246
void update(lps::stochastic_action_summand &x)
Definition builder.h:281
void update(lps::deadlock_summand &x)
Definition builder.h:220
void update(lps::stochastic_specification &x)
Definition builder.h:307
Builder< Derived > super
Definition builder.h:196
void update(lps::deadlock &x)
Definition builder.h:35
void update(lps::stochastic_specification &x)
Definition builder.h:159
void update(lps::specification &x)
Definition builder.h:104
void apply(T &result, const lps::process_initializer &x)
Definition builder.h:85
void apply(T &result, const lps::stochastic_process_initializer &x)
Definition builder.h:174
void update(lps::action_summand &x)
Definition builder.h:66
Builder< Derived > super
Definition builder.h:29
void apply(T &result, const lps::stochastic_distribution &x)
Definition builder.h:119
void update(lps::stochastic_linear_process &x)
Definition builder.h:148
void update(lps::stochastic_action_summand &x)
Definition builder.h:127
void apply(T &result, const lps::multi_action &x)
Definition builder.h:45
void update(lps::linear_process &x)
Definition builder.h:93
void update(lps::deadlock_summand &x)
Definition builder.h:53
Builder< Derived > super
Definition builder.h:339
void update(lps::action_summand &x)
Definition builder.h:376
void update(lps::deadlock &x)
Definition builder.h:345
void apply(T &result, const lps::multi_action &x)
Definition builder.h:355
void apply(T &result, const lps::stochastic_process_initializer &x)
Definition builder.h:478
void update(lps::specification &x)
Definition builder.h:414
void apply(T &result, const lps::stochastic_distribution &x)
Definition builder.h:426
void update(lps::linear_process &x)
Definition builder.h:403
void update(lps::stochastic_action_summand &x)
Definition builder.h:434
void update(lps::stochastic_specification &x)
Definition builder.h:466
void apply(T &result, const lps::process_initializer &x)
Definition builder.h:395
void update(lps::stochastic_linear_process &x)
Definition builder.h:455
void update(lps::deadlock_summand &x)
Definition builder.h:363
process::detail::add_capture_avoiding_replacement< Builder, Derived, Substitution > super
void apply(T &result, const stochastic_distribution &x, data::data_expression_list &pars)
In the code below, it is essential that the assignments are also updated. They are passed by referenc...
void apply(T &result, const stochastic_distribution &x, data::assignment_list &assignments)
In the code below, it is essential that the assignments are also updated. They are passed by referenc...
void do_action_summand(ActionSummand &x, const data::variable_list &v)
add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater< Substitution > &sigma)
Function object that checks if a sort is a singleton sort. Note that it is an approximation,...
Definition remove.h:39
is_singleton_sort(const data::data_specification &data_spec)
Definition remove.h:42
bool operator()(const data::sort_expression &s) const
Definition remove.h:46
const data::data_specification & m_data_spec
Definition remove.h:40
Function object that checks if a summand has a false condition.
Definition remove.h:28
bool operator()(const summand_base &s) const
Definition remove.h:29
Traverser for removing parameters from LPS data types. These parameters can be either process paramet...
Definition remove.h:61
void apply(atermpp::term_list< T > &result, const data::assignment_list &x)
Removes parameters from a list of assignments. Assignments to removed parameters are removed.
Definition remove.h:104
void apply(T &result, const stochastic_process_initializer &x)
Definition remove.h:159
void apply(T &result, const process_initializer &x)
Definition remove.h:152
void update(std::set< data::variable > &x)
Removes parameters from a set container.
Definition remove.h:76
const std::set< data::variable > & to_be_removed
Definition remove.h:68
void apply(atermpp::term_list< T > &result, const data::variable_list &x)
Removes parameters from a list of variables.
Definition remove.h:86
void update(linear_process &x)
Removes parameters from a linear_process.
Definition remove.h:114
data_expression_builder< remove_parameters_builder > super
Definition remove.h:62
data::data_expression_list remove_expressions(const data::data_expression_list &e)
Removes expressions from e at the corresponding positions of process_parameters.
Definition remove.h:133
void update(stochastic_specification &x)
Removes parameters from a linear process specification.
Definition remove.h:178
void update(specification &x)
Removes parameters from a linear process specification.
Definition remove.h:169
remove_parameters_builder(const std::set< data::variable > &to_be_removed_)
Definition remove.h:71
void update(stochastic_linear_process &x)
Removes parameters from a linear_process.
Definition remove.h:124
Options for linearisation.
Definition linearise.h:28
t_lin_method lin_method
Definition linearise.h:29
\brief Builder class
Definition builder.h:491
make_substitution(const std::map< process_identifier, process_identifier > &map)
process_identifier operator()(const process_identifier &id) const
const std::map< process_identifier, process_identifier > & m_map
std::size_t operator()(const atermpp::aterm &t) const
Definition aterm.h:483
std::size_t operator()(const atermpp::detail::reference_aterm< T > &t) const
std::size_t operator()(const mcrl2::lps::multi_action &ma) const
std::size_t operator()(const mcrl2::process::action &t) const