12#ifndef MCRL2_DATA_DETAIL_SEQUENCE_ALGORITHM_H
13#define MCRL2_DATA_DETAIL_SEQUENCE_ALGORITHM_H
27template <
typename Iterator>
28bool sequence_contains_duplicates(Iterator first, Iterator last)
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));
41template <
typename Iterator1,
typename Iterator2>
42bool sequences_do_overlap(Iterator1 first1, Iterator1 last1, Iterator2 first2, Iterator2 last2)
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();
57template <
typename Iterator,
typename T>
58bool sequence_is_subset_of_set(Iterator first, Iterator last,
const std::set<T>& s)
60 for (Iterator i = first; i != last; ++i)
62 if (s.find(*i) == s.end())
73template <
class Container>
74std::set<
typename Container::value_type> make_set(
const Container& c)
76 std::set<
typename Container::value_type> result;
77 std::copy(c.begin(), c.end(), std::inserter(result, result.begin()));
85template <
typename Sequence>
86bool sequence_empty_intersection(Sequence s1, Sequence s2)
88 for (
typename Sequence::const_iterator i = s1.begin(); i != s1.end(); ++i)
90 if (std::find(s2.begin(), s2.end(), *i) != s2.end())
\brief Assignment of a data expression to a variable
const data_expression & rhs() const
const variable & lhs() const
sort_expression sort() const
Returns the sort of the data expression.
const sort_expression & sort() const
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.
LPS summand containing a deadlock.
bool has_time() const
Returns true if time is available.
\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.
Linear process specification.
\brief An untyped multi action or data application
D_ParserTables parser_tables_mcrl2
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
static data_specification const & default_specification()
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_.
bool is_bool(const sort_expression &e)
Recogniser for sort expression Bool.
Namespace for system defined sort real_.
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
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())
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)
process::untyped_multi_action parse_multi_action_new(const std::string &text)
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())
action_rename_specification parse_action_rename_specification_new(const std::string &text)
The main namespace for the LPS library.
std::string pp(const lps::stochastic_specification &x, bool arg0)
std::set< data::variable > find_all_variables(const lps::linear_process &x)
std::string pp(const lps::specification &x, bool arg0)
std::set< data::sort_expression > find_sort_expressions(const lps::stochastic_specification &x)
std::string pp_extended(const lps::stochastic_specification &x, const std::string &process_name, bool precedence_aware=true)
std::set< process::action_label > find_action_labels(const lps::stochastic_specification &x)
std::set< data::variable > find_free_variables(const lps::stochastic_specification &x)
std::string pp(const lps::stochastic_distribution &x, bool arg0)
std::string pp_extended(const stochastic_specification &x, const std::string &process_name, bool precedence_aware, bool summand_numbers)
std::set< data::variable > find_all_variables(const lps::multi_action &x)
Returns all variables inside a multi-action.
std::set< data::variable > find_all_variables(const lps::stochastic_specification &x)
bool check_well_typedness(const specification &x)
std::set< data::variable > find_free_variables(const lps::linear_process &x)
bool check_well_typedness(const linear_process &x)
std::set< data::function_symbol > find_function_symbols(const lps::stochastic_specification &x)
std::string pp_extended(const specification &x, const std::string &process_name, bool precedence_aware, bool summand_numbers)
std::set< process::action_label > find_action_labels(const lps::process_initializer &x)
std::set< data::variable > find_free_variables(const lps::specification &x)
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.
void normalize_sorts(lps::specification &x, const data::sort_specification &)
std::set< data::variable > find_free_variables(const lps::deadlock &x)
std::string pp(const lps::deadlock_summand &x, bool arg0)
std::set< process::action_label > find_action_labels(const lps::linear_process &x)
lps::multi_action normalize_sorts(const lps::multi_action &x, const data::sort_specification &sortspec)
std::set< data::variable > find_free_variables(const lps::stochastic_linear_process &x)
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.
std::set< data::function_symbol > find_function_symbols(const lps::specification &x)
std::string pp(const lps::stochastic_linear_process &x, bool arg0)
std::set< data::variable > find_free_variables(const lps::stochastic_process_initializer &x)
std::set< data::variable > find_free_variables(const lps::multi_action &x)
std::string pp(const lps::deadlock &x, bool arg0)
void normalize_sorts(lps::stochastic_specification &x, const data::sort_specification &)
std::set< data::variable > find_free_variables(const lps::process_initializer &x)
std::string pp(const lps::stochastic_action_summand &x, bool arg0)
std::string pp(const lps::stochastic_process_initializer &x, bool arg0)
std::string pp(const lps::linear_process &x, bool arg0)
std::string pp(const lps::multi_action &x, bool arg0)
std::set< data::sort_expression > find_sort_expressions(const lps::specification &x)
std::string pp(const lps::action_summand &x, bool arg0)
std::set< data::variable > find_all_variables(const lps::specification &x)
bool check_well_typedness(const stochastic_specification &x)
std::set< data::variable > find_all_variables(const lps::deadlock &x)
action_rename_specification typecheck_action_rename_specification(const action_rename_specification &arspec, const lps::stochastic_specification &lpsspec)
Type checks an action rename specification.
std::set< data::variable > find_all_variables(const lps::stochastic_linear_process &x)
bool check_well_typedness(const stochastic_linear_process &x)
lps::multi_action translate_user_notation(const lps::multi_action &x)
std::set< core::identifier_string > find_identifiers(const lps::stochastic_specification &x)
std::set< core::identifier_string > find_identifiers(const lps::specification &x)
std::set< process::action_label > find_action_labels(const lps::specification &x)
std::string pp(const lps::process_initializer &x, bool arg0)
The main namespace for the Process library.
lps::action_rename_specification parse_ActionRenameSpec(const core::parse_node &node) const
action_rename_actions(const core::parser &parser_)
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 operator()(const Term &t) const
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
multi_action_actions(const core::parser &parser_)