12#ifndef MCRL2_PROCESS_DETAIL_PROCESS_CONTEXT_H
13#define MCRL2_PROCESS_DETAIL_PROCESS_CONTEXT_H
35 if (std::find_if(parameters.
begin(), parameters.
end(), [&](
const data::variable& v) { return a.lhs() == v.name(); }) == parameters.
end())
47 std::set<core::identifier_string> parameter_names;
50 parameter_names.insert(param.name());
53 assert(i != assignments.
end());
63 template <
typename ProcessIdentifierContainer>
79 for (
auto i = range.first; i != range.second; ++i)
91 sort_typechecker(v.sort());
110 std::vector<process_identifier> result;
111 for (
auto k = range.first; k != range.second; ++k)
116 result.push_back(
id);
121 std::string detailed_message;
124 if (std::distance(range.first, range.second) == 1)
128 detailed_message =
"Missing parameter: " +
core::pp(a.
lhs()) +
'\n';
132 if (result.size() > 1)
136 return result.front();
143 for (
auto k = range.first; k != range.second; ++k)
158 for (
auto k = range.first; k != range.second; ++k)
161 if (
id.variables().size() == parameters.
size())
add your file description here.
Term containing a string.
size_type size() const
Returns the size of the term_list.
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
\brief Assignment of a data expression to a string
const core::identifier_string & lhs() const
bool is_declared(const core::identifier_string &name) const
bool is_matching_assignment(const data::untyped_identifier_assignment_list &assignments, const data::variable_list ¶meters) const
bool is_declared(const core::identifier_string &name) const
data::sorts_list matching_process_sorts(const core::identifier_string &name, const data::data_expression_list ¶meters) const
process_instance make_process_instance(const core::identifier_string &name, const data::sort_expression_list &formal_parameters, const data::data_expression_list &actual_parameters) const
std::multimap< core::identifier_string, process_identifier > m_process_identifiers
process_identifier match_untyped_process_instance_assignment(const untyped_process_assignment &x) const
data::untyped_identifier_assignment find_violating_assignment(const data::untyped_identifier_assignment_list &assignments, const data::variable_list ¶meters) const
void add_process_identifiers(const ProcessIdentifierContainer &ids, const action_context &action_ctx, const data::sort_type_checker &sort_typechecker)
\brief A process identifier
\brief An untyped process assginment
const data::untyped_identifier_assignment_list & assignments() const
const core::identifier_string & name() const
Standard exception class for reporting runtime errors.
Add your file description here.
term_list< Term > reverse(const term_list< Term > &l)
Returns the list with the elements in reversed order.
std::string pp(const identifier_string &x)
data::sort_expression_list parameter_sorts(const Container ¶meters)
Returns the sorts of a sequence of parameters.
bool unique_names(const VariableContainer &variables)
Returns true if the names of the given variables are unique.
std::string pp(const abstraction &x)
std::string pp(const action_label &x)
bool contains(const atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable > &c, const typename atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable >::key_type &v, const std::size_t thread_index=0)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
add your file description here.