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
21{
22
23namespace data
24{
25
26namespace detail
27{
28
29/// \brief Returns true if the sequence [first, last) contains duplicates.
30/// \param first Start of a sequence
31/// \param last End of a sequence
32/// \return True if the sequence [first, last) contains duplicates.
33template <typename Iterator>
34bool sequence_contains_duplicates(Iterator first, Iterator last)
35{
36 // TODO: this implementation is not particularly efficient
37 std::set<typename std::iterator_traits<Iterator>::value_type> s(first, last);
38 return s.size() < static_cast <std::size_t>(std::distance(first, last));
39}
40
41/// \brief Returns true if the two sequences [first1, last1) and [first2, last2) have a non empty intersection.
42/// \param first1 Start of a sequence
43/// \param last1 End of a sequence
44/// \param first2 Start of a sequence
45/// \param last2 End of a sequence
46/// \return True if the two sequences [first1, last1) and [first2, last2) have a non empty intersection.
47template <typename Iterator1, typename Iterator2>
48bool sequences_do_overlap(Iterator1 first1, Iterator1 last1, Iterator2 first2, Iterator2 last2)
49{
50 typedef typename std::iterator_traits<Iterator1>::value_type value_type;
51 std::set<value_type> s1(first1, last1);
52 std::set<value_type> s2(first2, last2);
53 std::vector<value_type> intersection;
54 std::set_intersection(s1.begin(), s1.end(), s2.begin(), s2.end(), std::back_inserter(intersection));
55 return !intersection.empty();
56}
57
58/// \brief Returns true if all elements of the range [first, last) are element of the set s.
59/// \param first Start of a sequence
60/// \param last End of a sequence
61/// \param s A set
62/// \return True if all elements of the range [first, last) are element of the set s.
63template <typename Iterator, typename T>
64bool sequence_is_subset_of_set(Iterator first, Iterator last, const std::set<T>& s)
65{
66 for (Iterator i = first; i != last; ++i)
67 {
68 if (s.find(*i) == s.end())
69 {
70 return false;
71 }
72 }
73 return true;
74}
75
76/// \brief Makes a set of the given container.
77/// \param c A container
78/// \return A set containing the elements of the container
79template <class Container>
81{
82 std::set<typename Container::value_type> result;
83 std::copy(c.begin(), c.end(), std::inserter(result, result.begin()));
84 return result;
85}
86
87/// \brief Determines if the unordered sequences s1 and s2 have an empty intersection
88/// \param s1 A sequence
89/// \param s2 A sequence
90/// \return True if the intersection of s1 and s2 is empty
91template <typename Sequence>
92bool sequence_empty_intersection(Sequence s1, Sequence s2)
93{
94 for (typename Sequence::const_iterator i = s1.begin(); i != s1.end(); ++i)
95 {
96 if (std::find(s2.begin(), s2.end(), *i) != s2.end())
97 {
98 return false;
99 }
100 }
101 return true;
102}
103
104} // namespace detail
105
106} // namespace data
107
108} // namespace mcrl2
109
110#endif // MCRL2_DATA_DETAIL_SEQUENCE_ALGORITHM_H
bool operator!=(const unprotected_aterm_core &t) const
Inequality operator on two unprotected aterms.
Definition aterm_core.h:92
\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
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
\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
Read-only singly linked list of action rename rules.
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:68
const data::assignment_list & assignments() const
Returns the sequence of assignments.
LPS summand containing a deadlock.
Represents a deadlock.
Definition deadlock.h:26
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
\brief A timed multi-action
bool has_time() const
Returns true if time is available.
const process::action_list & actions() const
multi_action & operator=(multi_action &&) noexcept=default
const data::data_expression & time() const
Linear process specification.
LPS summand containing a multi-action.
\brief A stochastic distribution
\brief An action label
\brief An untyped multi action or data application
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
void syntax_error_fn(struct D_Parser *ap)
Custom syntax error function that prints both the line number and the column.
Definition dparser.cpp:463
D_ParseNode * ambiguity_fn(struct D_Parser *, int n, struct D_ParseNode **v)
Function for resolving parser ambiguities.
Definition dparser.cpp:332
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
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
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:132
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: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::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::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
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
std::set< data::variable > find_all_variables(const lps::multi_action &x)
Definition lps.cpp:49
std::set< data::sort_expression > find_sort_expressions(const lps::specification &x)
Definition lps.cpp:42
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
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
The main namespace for the Process library.
atermpp::term_list< action_label > action_label_list
\brief list of action_labels
Wrapper for D_ParseNode.
Definition dparser.h:86
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:209
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:204
Substitution that maps data variables to data expressions. The substitution is stored as an assignmen...
assignment_sequence_substitution(const assignment_list &assignments_)
lps::action_rename_specification parse_ActionRenameSpec(const core::parse_node &node) const
Definition parse_impl.h:123
action_rename_actions(const core::parser &parser_)
Definition parse_impl.h:46
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
std::size_t operator()(const atermpp::detail::reference_aterm< T > &t) const