12#ifndef MCRL2_DATA_DETAIL_SEQUENCE_ALGORITHM_H
13#define MCRL2_DATA_DETAIL_SEQUENCE_ALGORITHM_H
33template <
typename Iterator>
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));
47template <
typename Iterator1,
typename Iterator2>
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();
63template <
typename Iterator,
typename T>
66 for (Iterator i = first; i != last; ++i)
68 if (s.find(*i) == s.end())
79template <
class Container>
82 std::set<
typename Container::value_type> result;
83 std::copy(c.begin(), c.end(), std::inserter(result, result.begin()));
91template <
typename Sequence>
94 for (
typename Sequence::const_iterator i = s1.begin(); i != s1.end(); ++i)
96 if (
std::find(s2.begin(), s2.end(), *i) != s2.end())
bool operator!=(const unprotected_aterm_core &t) const
Inequality operator on two unprotected aterms.
\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
logger(const log_level_t l)
Default constructor.
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.
const data::assignment_list & assignments() const
Returns the sequence of assignments.
LPS summand containing a deadlock.
bool has_time() const
Returns true if time is available.
const data::data_expression & time() const
Returns the time.
\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
A stochastic process initializer.
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.
The main namespace for the aterm++ library.
void syntax_error_fn(struct D_Parser *ap)
Custom syntax error function that prints both the line number and the column.
D_ParseNode * ambiguity_fn(struct D_Parser *, int n, struct D_ParseNode **v)
Function for resolving parser ambiguities.
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()
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_.
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.
Namespace for all data library functionality.
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
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_process_initializer &x)
std::string pp(const lps::stochastic_distribution &x)
std::set< data::variable > find_all_variables(const lps::linear_process &x)
std::set< data::sort_expression > find_sort_expressions(const lps::stochastic_specification &x)
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_with_summand_numbers(const specification &x)
std::string pp(const lps::process_initializer &x)
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)
std::string pp(const lps::stochastic_specification &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(const lps::linear_process &x)
std::string pp(const lps::deadlock &x)
std::set< process::action_label > find_action_labels(const lps::process_initializer &x)
std::string pp(const lps::multi_action &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.
std::string pp(const lps::specification &x)
void normalize_sorts(lps::specification &x, const data::sort_specification &)
std::set< data::variable > find_free_variables(const lps::deadlock &x)
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::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_summand &x)
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_linear_process &x)
std::set< data::variable > find_all_variables(const lps::multi_action &x)
std::set< data::sort_expression > find_sort_expressions(const lps::specification &x)
std::string pp(const lps::stochastic_action_summand &x)
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::string pp(const lps::action_summand &x)
std::set< core::identifier_string > find_identifiers(const lps::specification &x)
std::string pp_with_summand_numbers(const stochastic_specification &x)
std::set< process::action_label > find_action_labels(const lps::specification &x)
The main namespace for the Process library.
atermpp::term_list< action_label > action_label_list
\brief list of action_labels
Wrapper for D_Parser and its corresponding D_ParserTables.
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...
parser(D_ParserTables &tables, D_AmbiguityFn ambiguity_fn=nullptr, D_SyntaxErrorFn syntax_error_fn=nullptr, std::size_t max_error_message_count=1)
unsigned int start_symbol_index(const std::string &name) const
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
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_)
std::size_t operator()(const atermpp::detail::reference_aterm< T > &t) const