mCRL2
Loading...
Searching...
No Matches
translate_user_notation.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/translate_user_notation.h
10/// \brief add your file description here.
11
12#ifndef MCRL2_PROCESS_TRANSLATE_USER_NOTATION_H
13#define MCRL2_PROCESS_TRANSLATE_USER_NOTATION_H
14
15#include "mcrl2/data/translate_user_notation.h"
16#include "mcrl2/process/builder.h"
17
18namespace mcrl2
19{
20
21namespace process
22{
23
24template <typename T>
26 typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type* = nullptr
27 )
28{
29 core::make_update_apply_builder<process::data_expression_builder>(data::detail::translate_user_notation_function()).update(x);
30}
31
32template <typename T>
34 typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type* = nullptr
35 )
36{
37 T result;
38 core::make_update_apply_builder<process::data_expression_builder>(data::detail::translate_user_notation_function()).apply(result, x);
39 return result;
40}
41
42} // namespace process
43
44} // namespace mcrl2
45
46#endif // MCRL2_PROCESS_TRANSLATE_USER_NOTATION_H
term_appl_iterator< aterm > iterator
Iterator used to iterate through an term_appl.
Definition aterm.h:42
bool operator==(const unprotected_aterm_core &t) const
Comparison operator.
Definition aterm_core.h:83
bool operator!=(const unprotected_aterm_core &t) const
Inequality operator on two unprotected aterms.
Definition aterm_core.h:92
parse_node_unexpected_exception(const parser &p, const parse_node &node)
Definition parse.h:78
\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
data_expression & operator=(const data_expression &) noexcept=default
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.
void translate_user_notation()
Translate user notation within the equations of the data specification.
data_specification()
Default constructor. Generate a data specification that contains only booleans and positive numbers.
Rewriter that operates on data expressions.
Definition rewriter.h:81
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
\brief A sort expression
\brief A data variable
Definition variable.h:28
const sort_expression & sort() const
Definition variable.h:43
logger(const log_level_t l)
Default constructor.
Definition logger.h:164
const data::data_expression & condition() const
Returns the condition of the rule.
const process::process_expression & rhs() const
Returns the right hand side of the rule.
data::data_expression & condition()
Returns the condition of the rule.
action_rename_rule(const data::variable_list &variables, const data::data_expression &condition, const process::action &lhs, const process::process_expression &rhs)
Constructor.
process::process_expression m_rhs
right hand side of the rule. Can only be an action, tau or delta.
data::variable_list m_variables
The data variables of the rule.
bool check_that_rhs_is_tau_delta_or_an_action() const
data::variable_list & variables()
Returns the variables of the rule.
process::action m_lhs
The left hand side of the rule.
action_rename_rule(const atermpp::aterm &t)
Constructor.
data::data_expression m_condition
The condition of the rule.
const data::variable_list & variables() const
Returns the variables of the rule.
const process::action & lhs() const
Returns the left hand side of the rule.
Read-only singly linked list of action rename rules.
const std::vector< action_rename_rule > & rules() const
Returns the action rename rules.
data::data_specification m_data
The data specification of the action rename specification.
process::action_label_list & action_labels()
Returns the sequence of action labels.
std::vector< action_rename_rule > m_rules
The action rename rules of the action rename specification.
action_rename_specification(const data::data_specification &data, const process::action_label_list &action_labels, const std::vector< action_rename_rule > &rules)
Constructor.
std::vector< action_rename_rule > & rules()
Returns the action rename rules.
process::action_label_list m_action_labels
The action labels of the action rename specification.
const process::action_label_list & action_labels() const
Returns the sequence of action labels.
action_rename_specification(atermpp::aterm t)
Constructor.
bool is_well_typed() const
Indicates whether the action_rename_specification is well typed.
action_rename_specification operator()(const action_rename_specification &arspec, const stochastic_specification &lpsspec)
Type check an action_rename_specification.
Definition typecheck.h:100
process::detail::action_context m_action_context
Definition typecheck.h:75
action_rename_rule typecheck_action_rename_rule(const action_rename_rule &x, const process::action_label_list &action_labels)
Definition typecheck.h:77
data::data_type_checker m_data_type_checker
Definition typecheck.h:74
action_rename_type_checker()
Default constructor for an action rename type checker.
Definition typecheck.h:91
LPS summand containing a multi-action.
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
const data::assignment_list & assignments() const
Returns the sequence of assignments.
LPS summand containing a deadlock.
Represents a deadlock.
Definition deadlock.h:26
deadlock(data::data_expression time=data::undefined_real())
Constructor.
Definition deadlock.h:36
bool has_time() const
Returns true if time is available.
Definition deadlock.h:42
const data::data_expression & time() const
Returns the time.
Definition deadlock.h:49
data::data_expression & time()
Returns the time.
Definition deadlock.h:56
linear_process(const data::variable_list &process_parameters, const deadlock_summand_vector &deadlock_summands, const action_summand_vector &action_summands)
Constructor.
multi_action_type_checker(const data::data_specification &dataspec=data::data_specification())
Default constructor.
Definition typecheck.h:44
multi_action operator()(const process::untyped_multi_action &x)
Type check a multi action. Throws a mcrl2::runtime_error exception if the expression is not well type...
Definition typecheck.h:53
data::detail::variable_context m_variable_context
Definition typecheck.h:29
process::detail::action_context m_action_context
Definition typecheck.h:28
data::data_type_checker m_data_type_checker
Definition typecheck.h:27
multi_action_type_checker(const data::data_specification &dataspec, const VariableContainer &variables, const ActionLabelContainer &action_labels)
Definition typecheck.h:33
\brief A timed multi-action
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 & operator=(multi_action &&) noexcept=default
const data::data_expression & time() const
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
Linear process specification.
LPS summand containing a multi-action.
\brief A stochastic distribution
stochastic_distribution & operator=(stochastic_distribution &&) noexcept=default
stochastic_distribution()
\brief Default constructor X3.
stochastic_distribution(const data::variable_list &variables, const data::data_expression &distribution)
\brief Constructor Z12.
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.
\brief An action label
const data::sort_expression_list & sorts() const
const core::identifier_string & name() const
action(const action_label &label, const data::data_expression_list &arguments)
\brief Constructor Z14.
const data::data_expression_list & arguments() const
action(const action &) noexcept=default
Move semantics.
const action_label & label() const
\brief The allow operator
\brief The at operator
const data::data_expression & time_stamp() const
const process_expression & operand() const
\brief The block operator
\brief The bounded initialization
\brief The choice operator
const process_expression & left() const
const process_expression & right() const
\brief The communication operator
\brief The value delta
delta()
\brief Default constructor X3.
\brief The hide operator
\brief The if-then-else operator
\brief The if-then operator
const process_expression & then_case() const
const data::data_expression & condition() const
\brief The left merge operator
\brief The merge operator
\brief A process equation
process_equation()
\brief Default constructor X3.
process_equation(const process_equation &) noexcept=default
Move semantics.
const data::variable_list & formal_parameters() const
const process_identifier & identifier() const
const process_expression & expression() const
\brief A process expression
process_expression(const process_expression &) noexcept=default
Move semantics.
const process_identifier & identifier() const
const data::data_expression_list & actual_parameters() const
const process_identifier & identifier() const
Process specification consisting of a data specification, action labels, a sequence of process equati...
const process_expression & init() const
Returns the initialization of the process specification.
const process::action_label_list & action_labels() const
Returns the action label specification.
\brief The rename operator
\brief The sequential composition
const process_expression & right() const
const process_expression & left() const
\brief The distribution operator
const data::variable_list & variables() const
const data::data_expression & distribution() const
\brief The sum operator
const process_expression & operand() const
const data::variable_list & variables() const
\brief The synchronization operator
const process_expression & left() const
const process_expression & right() const
\brief The value tau
tau()
\brief Default constructor X3.
\brief An untyped multi action or data application
untyped_multi_action()
\brief Default constructor X3.
Standard exception class for reporting runtime errors.
Definition exception.h:27
runtime_error(const std::string &message)
Constructor.
Definition exception.h:31
D_ParserTables parser_tables_mcrl2
Definition dparser.cpp:20
#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
void syntax_error_fn(struct D_Parser *ap)
Custom syntax error function that prints both the line number and the column.
Definition dparser.cpp:465
D_ParseNode * ambiguity_fn(struct D_Parser *, int n, struct D_ParseNode **v)
Function for resolving parser ambiguities.
Definition dparser.cpp:334
const atermpp::function_symbol & function_symbol_ActionRenameRule()
bool sequence_empty_intersection(Sequence s1, Sequence s2)
Determines if the unordered sequences s1 and s2 have an empty intersection.
bool sequence_contains_duplicates(Iterator first, Iterator last)
Returns true if the sequence [first, last) contains duplicates.
static data_specification const & default_specification()
Definition parse.h:31
bool sequence_is_subset_of_set(Iterator first, Iterator last, const std::set< T > &s)
Returns true if all elements of the range [first, last) are element of the set s.
bool check_assignment_variables(assignment_list const &assignments, variable_list const &variables)
Returns true if the left hand sides of assignments are contained in variables.
bool sequences_do_overlap(Iterator1 first1, Iterator1 last1, Iterator2 first2, Iterator2 last2)
Returns true if the two sequences [first1, last1) and [first2, last2) have a non empty intersection.
std::set< typename Container::value_type > make_set(const Container &c)
Makes a set of the given container.
Namespace for system defined sort bool_.
Definition bool.h:32
bool is_bool(const sort_expression &e)
Recogniser for sort expression Bool.
Definition bool.h:54
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
Namespace for system defined sort real_.
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real1.h:58
Namespace for all data library functionality.
Definition data.cpp:22
atermpp::term_list< data_expression > data_expression_list
\brief list of data_expressions
atermpp::term_list< variable > variable_list
\brief list of variables
atermpp::term_list< assignment > assignment_list
\brief list of assignments
Definition assignment.h:146
std::string pp(const data::variable_list &x)
Definition data.cpp:31
std::string pp(const data::data_expression &x)
Definition data.cpp:52
@ verbose
Definition logger.h:37
bool is_well_typed(const T &x)
Checks well typedness of an LPS object.
bool check_action_labels(const process::action_list &actions, const std::set< process::action_label > &labels)
Returns true if the labels of the given actions are contained in labels.
multi_action complete_multi_action(process::untyped_multi_action &x, const process::action_label_list &action_decls, const data::data_specification &data_spec=data::detail::default_specification())
Definition lps.cpp:132
process::action_label rename_action_label(const process::action_label &act, const std::regex &matching_regex, const std::string &replacing_fmt)
bool check_action_label_sorts(const process::action_label_list &action_labels, const std::set< data::sort_expression > &sorts)
Returns true if the sorts of the given action labels are contained in sorts.
bool check_well_typedness(const T &x)
Checks well typedness of an LPS object, and will print error messages to stderr.
bool check_action_sorts(const process::action_list &actions, const std::set< data::sort_expression > &sorts)
Returns true if the sorts of the given actions are contained in sorts.
void complete_action_rename_specification(action_rename_specification &x, const lps::stochastic_specification &spec)
Definition lps.cpp:150
process::untyped_multi_action parse_multi_action_new(const std::string &text)
Definition lps.cpp:114
multi_action complete_multi_action(process::untyped_multi_action &x, multi_action_type_checker &typechecker, const data::data_specification &data_spec=data::detail::default_specification())
Definition lps.cpp:124
action_rename_specification parse_action_rename_specification_new(const std::string &text)
Definition lps.cpp:140
The main namespace for the LPS library.
Definition constelm.h:21
std::string pp(const lps::stochastic_process_initializer &x)
Definition lps.cpp:36
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
std::set< data::sort_expression > find_sort_expressions(const lps::stochastic_specification &x)
Definition lps.cpp:43
std::set< process::action_label > find_action_labels(const lps::stochastic_specification &x)
Definition lps.cpp:65
std::set< data::variable > find_free_variables(const lps::stochastic_specification &x)
Definition lps.cpp:53
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
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
std::set< data::variable > find_free_variables(const lps::linear_process &x)
Definition lps.cpp:50
std::string pp(const lps::stochastic_specification &x)
Definition lps.cpp:37
bool check_well_typedness(const linear_process &x)
Definition lps.cpp:92
std::set< data::function_symbol > find_function_symbols(const lps::stochastic_specification &x)
Definition lps.cpp:59
std::string pp(const lps::linear_process &x)
Definition lps.cpp:29
std::vector< deadlock_summand > deadlock_summand_vector
\brief vector of deadlock_summands
lps::stochastic_specification action_rename(const action_rename_specification &action_rename_spec, const lps::stochastic_specification &lps_old_spec, const data::rewriter &rewr, const bool enable_rewriting)
Rename the actions in a linear specification using a given action_rename_spec.
std::string pp(const lps::deadlock &x)
Definition lps.cpp:27
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
multi_action typecheck_multi_action(process::untyped_multi_action &mult_act, const data::data_specification &data_spec, const process::action_label_list &action_decls)
Type check a multi action Throws an exception if something went wrong.
Definition typecheck.h:128
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
std::set< data::variable > find_free_variables(const lps::deadlock &x)
Definition lps.cpp:54
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
std::set< data::variable > find_free_variables(const lps::stochastic_linear_process &x)
Definition lps.cpp:51
multi_action typecheck_multi_action(process::untyped_multi_action &mult_act, multi_action_type_checker &typechecker)
Type check a multi action Throws an exception if something went wrong.
Definition typecheck.h:144
std::set< data::function_symbol > find_function_symbols(const lps::specification &x)
Definition lps.cpp:58
std::set< data::variable > find_free_variables(const lps::stochastic_process_initializer &x)
Definition lps.cpp:57
void normalize_sorts(T &x, const data::sort_specification &sortspec, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
std::set< data::variable > find_free_variables(const lps::multi_action &x)
Definition lps.cpp:55
std::string pp(const lps::deadlock_summand &x)
Definition lps.cpp:28
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
std::string pp(const lps::stochastic_linear_process &x)
Definition lps.cpp:35
atermpp::aterm action_rename_specification_to_aterm(const action_rename_specification &spec)
atermpp::aterm action_rename_rule_to_aterm(const action_rename_rule &rule)
std::set< data::variable > find_all_variables(const lps::multi_action &x)
Definition lps.cpp:49
T normalize_sorts(const T &x, const data::sort_specification &sortspec, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=0)
std::set< data::sort_expression > find_sort_expressions(const lps::specification &x)
Definition lps.cpp:42
std::vector< action_summand > action_summand_vector
\brief vector of action_summands
std::string pp(const lps::stochastic_action_summand &x)
Definition lps.cpp:33
std::set< data::variable > find_all_variables(const lps::specification &x)
Definition lps.cpp:46
stochastic_specification action_rename(const std::regex &matching_regex, const std::string &replacing_fmt, const stochastic_specification &lps_old_spec)
Rename actions in given specification based on a regular expression and a string that specifies how t...
bool check_well_typedness(const stochastic_specification &x)
Definition lps.cpp:107
std::set< data::variable > find_all_variables(const lps::deadlock &x)
Definition lps.cpp:48
action_rename_specification typecheck_action_rename_specification(const action_rename_specification &arspec, const lps::stochastic_specification &lpsspec)
Type checks an action rename specification.
Definition typecheck.h:157
std::set< data::variable > find_all_variables(const lps::stochastic_linear_process &x)
Definition lps.cpp:45
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 check_process_instance_assignment(const process_equation &eq, const process_instance_assignment &inst)
Returns true if the process instance assignment a matches with the process equation eq.
Definition is_linear.h:28
bool is_process(const process_expression &x)
Returns true if the argument is a process instance.
Definition is_linear.h:71
bool is_conditional_deadlock(const process_expression &x)
Returns true if the argument is a conditional deadlock.
Definition is_linear.h:131
bool is_linear_process_term(const process_expression &x)
Returns true if the argument is a linear process.
Definition is_linear.h:157
bool check_process_instance(const process_equation &eq, const process_instance &init)
Returns true if the process instance a matches with the process equation eq.
Definition is_linear.h:49
bool is_alternative(const process_expression &x)
Returns true if the argument is an alternative composition.
Definition is_linear.h:147
bool is_timed_deadlock(const process_expression &x)
Returns true if the argument is a deadlock.
Definition is_linear.h:96
bool is_action_prefix(const process_expression &x)
Returns true if the argument is an action prefix.
Definition is_linear.h:123
bool is_stochastic_process(const process_expression &x)
Returns true if the argument is a process instance, optionally wrapped in a stochastic distribution.
Definition is_linear.h:81
bool is_multiaction(const process_expression &x)
Returns true if the argument is a multi-action.
Definition is_linear.h:105
bool is_conditional_action_prefix(const process_expression &x)
Returns true if the argument is a conditional action prefix.
Definition is_linear.h:139
bool is_timed_multiaction(const process_expression &x)
Returns true if the argument is a multi-action.
Definition is_linear.h:115
The main namespace for the Process library.
bool is_at(const atermpp::aterm &x)
bool is_linear(const process_specification &p, bool verbose=false)
Returns true if the process specification is linear.
Definition is_linear.h:347
std::string pp(const process::comm &x)
Definition process.cpp:43
std::string pp(const process::untyped_multi_action &x)
Definition process.cpp:64
bool is_linear(const process_expression &x, const process_equation &eqn)
Returns true if the process expression is linear.
Definition is_linear.h:392
bool is_process_instance(const atermpp::aterm &x)
std::string pp(const process::block &x)
Definition process.cpp:40
bool is_process_instance_assignment(const atermpp::aterm &x)
bool is_tau(const atermpp::aterm &x)
std::string pp(const process::process_instance &x)
Definition process.cpp:54
bool is_seq(const atermpp::aterm &x)
std::string pp(const process::process_instance_assignment &x)
Definition process.cpp:55
bool is_delta(const atermpp::aterm &x)
bool is_linear(const process_equation &eqn)
Returns true if the process equation is linear.
Definition is_linear.h:382
bool is_sum(const atermpp::aterm &x)
T translate_user_notation(const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
bool is_action(const atermpp::aterm &x)
std::string pp(const process::left_merge &x)
Definition process.cpp:49
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::allow &x)
Definition process.cpp:38
std::string pp(const process::if_then_else &x)
Definition process.cpp:48
atermpp::term_list< action > action_list
\brief list of actions
std::string pp(const process::rename &x)
Definition process.cpp:57
std::string pp(const process::process_expression &x)
Definition process.cpp:52
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 translate_user_notation(T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
bool is_choice(const atermpp::aterm &x)
bool is_stochastic_operator(const atermpp::aterm &x)
std::string pp(const process::if_then &x)
Definition process.cpp:47
bool is_sync(const atermpp::aterm &x)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
core::identifier_string parse_Id(const parse_node &node) const
Definition parse.h:233
Wrapper for D_ParseNode.
Definition dparser.h:86
parse_node child(int i) const
Definition dparser.cpp:43
int child_count() const
Definition dparser.cpp:37
std::string symbol_name(const parse_node &node) const
Definition parse.h:205
const parser & m_parser
Definition parse.h:85
Wrapper for D_Parser and its corresponding D_ParserTables.
Definition dparser.h:148
parse_node parse(const std::string &text, unsigned int start_symbol_index=0, bool partial_parses=false)
Parses a string. N.B. The user is responsible for destruction of the returned value by calling destro...
Definition dparser.cpp:211
parser(D_ParserTables &tables, D_AmbiguityFn ambiguity_fn=nullptr, D_SyntaxErrorFn syntax_error_fn=nullptr, std::size_t max_error_message_count=1)
Definition dparser.cpp:174
unsigned int start_symbol_index(const std::string &name) const
Definition dparser.cpp:206
Substitution that maps data variables to data expressions. The substitution is stored as an assignmen...
assignment_sequence_substitution(const assignment_list &assignments_)
data::data_expression parse_DataExpr(const core::parse_node &node) const
Definition parse_impl.h:211
bool callback_DataSpecElement(const core::parse_node &node, untyped_data_specification &result) const
Definition parse_impl.h:413
normalize_sorts_function(const sort_specification &sort_spec)
std::vector< lps::action_rename_rule > parse_ActionRenameRuleList(const core::parse_node &node) const
Definition parse_impl.h:75
process::action parse_Action_as_action(const core::parse_node &node) const
Definition parse_impl.h:51
bool callback_ActionRenameSpec(const core::parse_node &node, data::untyped_data_specification &dataspec_result, lps::action_rename_specification &result) const
Definition parse_impl.h:91
std::vector< lps::action_rename_rule > parse_ActionRenameRuleSpec(const core::parse_node &node) const
Definition parse_impl.h:80
lps::action_rename_specification parse_ActionRenameSpec(const core::parse_node &node) const
Definition parse_impl.h:123
process::process_expression parse_ActionRenameRuleRHS(const core::parse_node &node) const
Definition parse_impl.h:57
action_rename_actions(const core::parser &parser_)
Definition parse_impl.h:46
lps::action_rename_rule parse_ActionRenameRule(const core::parse_node &node) const
Definition parse_impl.h:65
Function object for applying a substitution to LPS data types.
bool is_well_typed(const linear_process_base< ActionSummand > &p) const
Checks well typedness of a linear process.
bool is_well_typed(const process::action &a) const
Traverses an action.
bool is_well_typed(const action_summand &s) const
Checks well typedness of a summand.
bool check_time(const data::data_expression &t, const std::string &type) const
Checks if the sort of t has type real.
bool is_well_typed(const data::assignment &a) const
Traverses an assignment.
bool check_condition(const data::data_expression &t, const std::string &type) const
Checks if the sort of t has type bool.
bool is_well_typed(const stochastic_specification &spec) const
bool is_well_typed(const data::variable &d) const
Checks well typedness of a variable.
bool check_assignments(const data::assignment_list &l, const std::string &type) const
Checks if the assignments are well typed and have unique left hand sides.
bool is_well_typed(const specification &spec) const
bool is_well_typed(const data::sort_expression &d) const
Checks well typedness of a sort expression.
bool is_well_typed_container(const Container &c) const
Checks well typedness of the elements of a container.
bool is_well_typed(const process::action_label &d) const
Traverses an action label.
bool is_well_typed(const specification_base< LinearProcess, InitialProcessExpression > &spec, const std::set< data::variable > &free_variables) const
Checks well typedness of a linear process specification.
bool is_well_typed(const deadlock &d) const
Checks well typedness of a deadlock.
bool is_well_typed(const data::data_expression &d) const
Checks well typedness of a data expression.
bool is_well_typed(const deadlock_summand &s) const
Checks well typedness of a summand.
bool is_well_typed(const multi_action &a) const
Checks well typedness of a multi-action.
process::untyped_multi_action parse_MultAct(const core::parse_node &node) const
Definition parse_impl.h:33
multi_action_actions(const core::parser &parser_)
Definition parse_impl.h:29
action_actions(const core::parser &parser_)
Definition parse_impl.h:47
Converts a process expression into linear process format. Use the convert member functions for this.
process_expression_traverser< linear_process_conversion_traverser > super
lps::deadlock_summand_vector m_deadlock_summands
The result of the conversion.
process_equation m_equation
The process equation that is checked.
lps::specification convert(const process_specification &p)
Converts a process_specification into a specification. Throws non_linear_process if a non-linear sub-...
void leave(const process::left_merge &x)
Visit left_merge node.
lps::action_summand_vector m_action_summands
The result of the conversion.
void leave(const process::bounded_init &x)
Visit bounded_init node.
void convert(const process_equation &)
Returns true if the process equation e is linear.
void leave(const process::if_then_else &x)
Visit if_then_else node.
Exception that is thrown by linear_process_expression_traverser.
Definition is_linear.h:178
Checks if a process equation is linear. Use the is_linear() member function for this.
Definition is_linear.h:167
process_expression_traverser< linear_process_expression_traverser > super
Definition is_linear.h:168
linear_process_expression_traverser(const process_equation &eqn_=process_equation())
Definition is_linear.h:184
void enter(const process::process_instance &x)
Definition is_linear.h:189
process_equation eqn
The process equation that is checked.
Definition is_linear.h:174
bool is_linear(const process_expression &x, bool verbose=false)
Returns true if the process equation e is linear.
Definition is_linear.h:325
void enter(const process::process_instance_assignment &x)
Definition is_linear.h:197
Converts a process expression into linear process format. Use the convert member functions for this.
void leave(const process::stochastic_operator &x)
Visit stochastic operator node.
void convert(const process_equation &)
Returns true if the process equation e is linear.
lps::stochastic_action_summand_vector m_action_summands
The result of the conversion.
lps::deadlock_summand_vector m_deadlock_summands
The result of the conversion.
process_expression_traverser< stochastic_linear_process_conversion_traverser > super
lps::stochastic_specification convert(const process_specification &p)
Converts a process_specification into a stochastic_specification. Throws non_linear_process if a non-...
std::size_t operator()(const atermpp::detail::reference_aterm< T > &t) const