mCRL2
Loading...
Searching...
No Matches
sequence_algorithm.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/data/detail/sequence_algorithm.h
10/// \brief Add your file description here.
11
12#ifndef MCRL2_DATA_DETAIL_SEQUENCE_ALGORITHM_H
13#define MCRL2_DATA_DETAIL_SEQUENCE_ALGORITHM_H
14
15#include <algorithm>
16#include <iterator>
17#include <set>
18#include <vector>
19
20namespace mcrl2::data::detail
21{
22
23/// \brief Returns true if the sequence [first, last) contains duplicates.
24/// \param first Start of a sequence
25/// \param last End of a sequence
26/// \return True if the sequence [first, last) contains duplicates.
27template <typename Iterator>
28bool sequence_contains_duplicates(Iterator first, Iterator last)
29{
30 // TODO: this implementation is not particularly efficient
31 std::set<typename std::iterator_traits<Iterator>::value_type> s(first, last);
32 return s.size() < static_cast <std::size_t>(std::distance(first, last));
33}
34
35/// \brief Returns true if the two sequences [first1, last1) and [first2, last2) have a non empty intersection.
36/// \param first1 Start of a sequence
37/// \param last1 End of a sequence
38/// \param first2 Start of a sequence
39/// \param last2 End of a sequence
40/// \return True if the two sequences [first1, last1) and [first2, last2) have a non empty intersection.
41template <typename Iterator1, typename Iterator2>
42bool sequences_do_overlap(Iterator1 first1, Iterator1 last1, Iterator2 first2, Iterator2 last2)
43{
44 using value_type = typename std::iterator_traits<Iterator1>::value_type;
45 std::set<value_type> s1(first1, last1);
46 std::set<value_type> s2(first2, last2);
47 std::vector<value_type> intersection;
48 std::set_intersection(s1.begin(), s1.end(), s2.begin(), s2.end(), std::back_inserter(intersection));
49 return !intersection.empty();
50}
51
52/// \brief Returns true if all elements of the range [first, last) are element of the set s.
53/// \param first Start of a sequence
54/// \param last End of a sequence
55/// \param s A set
56/// \return True if all elements of the range [first, last) are element of the set s.
57template <typename Iterator, typename T>
58bool sequence_is_subset_of_set(Iterator first, Iterator last, const std::set<T>& s)
59{
60 for (Iterator i = first; i != last; ++i)
61 {
62 if (s.find(*i) == s.end())
63 {
64 return false;
65 }
66 }
67 return true;
68}
69
70/// \brief Makes a set of the given container.
71/// \param c A container
72/// \return A set containing the elements of the container
73template <class Container>
74std::set<typename Container::value_type> make_set(const Container& c)
75{
76 std::set<typename Container::value_type> result;
77 std::copy(c.begin(), c.end(), std::inserter(result, result.begin()));
78 return result;
79}
80
81/// \brief Determines if the unordered sequences s1 and s2 have an empty intersection
82/// \param s1 A sequence
83/// \param s2 A sequence
84/// \return True if the intersection of s1 and s2 is empty
85template <typename Sequence>
86bool sequence_empty_intersection(Sequence s1, Sequence s2)
87{
88 for (typename Sequence::const_iterator i = s1.begin(); i != s1.end(); ++i)
89 {
90 if (std::find(s2.begin(), s2.end(), *i) != s2.end())
91 {
92 return false;
93 }
94 }
95 return true;
96}
97
98} // namespace mcrl2::data::detail
99
100#endif // MCRL2_DATA_DETAIL_SEQUENCE_ALGORITHM_H
\brief Assignment of a data expression to a variable
Definition assignment.h:88
const data_expression & rhs() const
Definition assignment.h:119
const variable & lhs() const
Definition assignment.h:114
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:107
\brief A sort expression
\brief A data variable
Definition variable.h:25
const sort_expression & sort() const
Definition variable.h:40
Action rename specification.
process::action_label_list & action_labels()
Returns the sequence of action labels.
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:71
LPS summand containing a deadlock.
Represents a deadlock.
Definition deadlock.h:23
bool has_time() const
Returns true if time is available.
Definition deadlock.h:39
\brief A timed multi-action
bool has_time() const
Returns true if time is available.
multi_action & operator=(multi_action &&) noexcept=default
Linear process specification.
\brief An action label
\brief An untyped multi action or data application
D_ParserTables parser_tables_mcrl2
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:393
static data_specification const & default_specification()
Definition parse.h:28
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.
Namespace for system defined sort bool_.
Definition bool.h:29
bool is_bool(const sort_expression &e)
Recogniser for sort expression Bool.
Definition bool.h:51
Namespace for system defined sort real_.
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real1.h:55
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
bool is_well_typed(const T &x)
Checks well typedness of an LPS object.
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:148
bool check_well_typedness(const T &x)
Checks well typedness of an LPS object, and will print error messages to stderr.
void complete_action_rename_specification(action_rename_specification &x, const lps::stochastic_specification &spec)
Definition lps.cpp:166
process::untyped_multi_action parse_multi_action_new(const std::string &text)
Definition lps.cpp:130
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:140
action_rename_specification parse_action_rename_specification_new(const std::string &text)
Definition lps.cpp:156
The main namespace for the LPS library.
Definition constelm.h:18
std::string pp(const lps::stochastic_specification &x, bool arg0)
Definition lps.cpp:40
std::set< data::variable > find_all_variables(const lps::linear_process &x)
Definition lps.cpp:47
std::string pp(const lps::specification &x, bool arg0)
Definition lps.cpp:35
std::set< data::sort_expression > find_sort_expressions(const lps::stochastic_specification &x)
Definition lps.cpp:46
std::string pp_extended(const lps::stochastic_specification &x, const std::string &process_name, bool precedence_aware=true)
Definition lps.cpp:79
std::set< process::action_label > find_action_labels(const lps::stochastic_specification &x)
Definition lps.cpp:68
std::set< data::variable > find_free_variables(const lps::stochastic_specification &x)
Definition lps.cpp:56
std::string pp(const lps::stochastic_distribution &x, bool arg0)
Definition lps.cpp:37
std::string pp_extended(const stochastic_specification &x, const std::string &process_name, bool precedence_aware, bool summand_numbers)
Definition lps.cpp:98
std::set< data::variable > find_all_variables(const lps::multi_action &x)
Returns all variables inside a multi-action.
Definition lps.cpp:52
std::set< data::variable > find_all_variables(const lps::stochastic_specification &x)
Definition lps.cpp:50
bool check_well_typedness(const specification &x)
Definition lps.cpp:118
std::set< data::variable > find_free_variables(const lps::linear_process &x)
Definition lps.cpp:53
bool check_well_typedness(const linear_process &x)
Definition lps.cpp:108
std::set< data::function_symbol > find_function_symbols(const lps::stochastic_specification &x)
Definition lps.cpp:62
std::string pp_extended(const specification &x, const std::string &process_name, bool precedence_aware, bool summand_numbers)
Definition lps.cpp:88
std::set< process::action_label > find_action_labels(const lps::process_initializer &x)
Definition lps.cpp:66
std::set< data::variable > find_free_variables(const lps::specification &x)
Definition lps.cpp:55
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:125
void normalize_sorts(lps::specification &x, const data::sort_specification &)
Definition lps.cpp:42
std::set< data::variable > find_free_variables(const lps::deadlock &x)
Definition lps.cpp:57
std::string pp(const lps::deadlock_summand &x, bool arg0)
Definition lps.cpp:31
std::set< process::action_label > find_action_labels(const lps::linear_process &x)
Definition lps.cpp:65
lps::multi_action normalize_sorts(const lps::multi_action &x, const data::sort_specification &sortspec)
Definition lps.cpp:41
std::set< data::variable > find_free_variables(const lps::stochastic_linear_process &x)
Definition lps.cpp:54
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:141
std::set< data::function_symbol > find_function_symbols(const lps::specification &x)
Definition lps.cpp:61
std::string pp(const lps::stochastic_linear_process &x, bool arg0)
Definition lps.cpp:38
std::set< data::variable > find_free_variables(const lps::stochastic_process_initializer &x)
Definition lps.cpp:60
std::set< data::variable > find_free_variables(const lps::multi_action &x)
Definition lps.cpp:58
std::string pp(const lps::deadlock &x, bool arg0)
Definition lps.cpp:30
void normalize_sorts(lps::stochastic_specification &x, const data::sort_specification &)
Definition lps.cpp:43
std::set< data::variable > find_free_variables(const lps::process_initializer &x)
Definition lps.cpp:59
std::string pp(const lps::stochastic_action_summand &x, bool arg0)
Definition lps.cpp:36
std::string pp(const lps::stochastic_process_initializer &x, bool arg0)
Definition lps.cpp:39
std::string pp(const lps::linear_process &x, bool arg0)
Definition lps.cpp:32
std::string pp(const lps::multi_action &x, bool arg0)
Definition lps.cpp:33
std::set< data::sort_expression > find_sort_expressions(const lps::specification &x)
Definition lps.cpp:45
std::string pp(const lps::action_summand &x, bool arg0)
Definition lps.cpp:29
std::set< data::variable > find_all_variables(const lps::specification &x)
Definition lps.cpp:49
bool check_well_typedness(const stochastic_specification &x)
Definition lps.cpp:123
std::set< data::variable > find_all_variables(const lps::deadlock &x)
Definition lps.cpp:51
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:154
std::set< data::variable > find_all_variables(const lps::stochastic_linear_process &x)
Definition lps.cpp:48
bool check_well_typedness(const stochastic_linear_process &x)
Definition lps.cpp:113
lps::multi_action translate_user_notation(const lps::multi_action &x)
Definition lps.cpp:44
std::set< core::identifier_string > find_identifiers(const lps::stochastic_specification &x)
Definition lps.cpp:64
std::set< core::identifier_string > find_identifiers(const lps::specification &x)
Definition lps.cpp:63
std::set< process::action_label > find_action_labels(const lps::specification &x)
Definition lps.cpp:67
std::string pp(const lps::process_initializer &x, bool arg0)
Definition lps.cpp:34
The main namespace for the Process library.
lps::action_rename_specification parse_ActionRenameSpec(const core::parse_node &node) const
Definition parse_impl.h:119
action_rename_actions(const core::parser &parser_)
Definition parse_impl.h:42
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:29
multi_action_actions(const core::parser &parser_)
Definition parse_impl.h:25