mCRL2
Loading...
Searching...
No Matches
iota.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/utilities/detail/iota.h
10/// \brief The iota function.
11
12#ifndef MCRL2_UTILITIES_DETAIL_IOTA_H
13#define MCRL2_UTILITIES_DETAIL_IOTA_H
14
15namespace mcrl2
16{
17
18namespace utilities
19{
20
21namespace detail
22{
23
24/// \brief Generates the sequence value, value + 1, ... and writes it to the sequence [first, last)
25/// \param first Start of a sequence
26/// \param last End of a sequence
27/// \param value A value
28template <class Iter, class T>
29void iota(Iter first, Iter last, T value)
30{
31 while (first != last)
32 {
33 *first++ = value++;
34 }
35}
36
37} // namespace detail
38
39} // namespace utilities
40
41} // namespace mcrl2
42
43#endif // MCRL2_UTILITIES_DETAIL_IOTA_H
aterm_string(const std::string &s)
Constructor that allows construction from a string.
bool operator==(const unprotected_aterm_core &t) const
Comparison operator.
Definition aterm_core.h:83
bool defined() const
Returns true if this term is not equal to the term assigned by the default constructor of aterms,...
Definition aterm_core.h:143
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
data_expression & operator=(const data_expression &) noexcept=default
The class BDD2Dot offers the ability to write binary decision diagrams to dot files....
Definition bdd2dot.h:30
std::ofstream f_dot_file
The file the output is written to.
Definition bdd2dot.h:36
std::map< atermpp::aterm, atermpp::aterm_int > f_visited
A table containing all the visited nodes. It maps these nodes to the corresponding node numbers.
Definition bdd2dot.h:39
void aux_output_bdd(const data_expression &a_bdd)
Writes the BDD it receives to BDD2Dot::f_dot_file.
Definition bdd2dot.h:50
BDD_Info f_bdd_info
A class that gives information about the structure of BDDs.
Definition bdd2dot.h:42
int f_node_number
The smallest unused node number.
Definition bdd2dot.h:33
The class BDD_Info provides information about the structure of binary decision diagrams.
Definition bdd_info.h:26
static const mcrl2::data::data_expression & get_true_branch(const mcrl2::data::data_expression &a_bdd)
Method that returns the true-branch of a BDD.
Definition bdd_info.h:50
static bool is_if_then_else(const data_expression &a_bdd)
Method that indicates wether or not the root of a BDD is a guard node.
Definition bdd_info.h:85
static bool is_false(const data_expression &a_bdd)
Method that indicates whether or not a BDD equals false.
Definition bdd_info.h:76
static const mcrl2::data::data_expression & get_guard(const mcrl2::data::data_expression &a_bdd)
Method that returns the guard of a BDD.
Definition bdd_info.h:42
static const mcrl2::data::data_expression & get_false_branch(const mcrl2::data::data_expression &a_bdd)
Method that returns the false-branch of a BDD.
Definition bdd_info.h:58
static bool is_true(const data_expression &a_bdd)
Method that indicates whether or not a BDD equals true.
Definition bdd_info.h:67
Base class for storing properties of mCRL2 types. Properties are (key, value) pairs stored as strings...
data_property_map(const std::string &text)
The strings may appear in a random order, and not all of them need to be present.
std::string print(std::string s) const
unsigned int parse_unsigned_int(std::string const &text) const
const std::map< std::string, std::string > & data() const
Returns the stored properties.
std::set< core::identifier_string > names(const Container &v) const
Collects the names of the elements of the container. The name of element x is retrieved by x....
std::string compare(const std::string &property, unsigned int x, unsigned int y) const
Compares two integers, and returns a message if they are different. If if they are equal the empty st...
std::string print(const core::identifier_string &s) const
void parse_text(const std::string &text)
Initializes the property map with text containing lines in KEY = VALUE format.
std::string print(const data::variable &v) const
std::map< std::string, std::string > m_data
Contains a normalized string representation of the properties.
std::string compare(const data_property_map &other) const
Compares this property map with another property map. The function compare_property must be defined p...
std::string compare_property(const std::string &property, const std::string &, const std::string &) const
Compares two values x and y of a given property. This function should be redefined in derived classes...
std::string operator[](const std::string &key) const
Returns the value corresponding to key. Throws an exception if the key is not found.
unsigned int max_key_length() const
Returns the maximum length of the property names.
std::string print(std::size_t n) const
std::set< std::multiset< std::string > > parse_set_multiset_string(std::string const &text) const
std::set< std::string > parse_set_string(std::string const &text) const
std::string to_string() const
Returns a string representation of the properties.
data_property_map()
Default constructor for derived types.
std::string align(const std::string &s, unsigned int n) const
std::string compare(const std::string &property, const std::set< T > &x, const std::set< T > &y) const
Compares two sets and returns a string with the differences encountered. Elements present in the firs...
static std::string add_separators(std::string const &c, typename std::enable_if< atermpp::is_set< Container >::value >::type *=nullptr)
Add start/end separators for non-set container types.
std::string print(const Container &v, typename atermpp::enable_if_container< Container >::type *=nullptr) const
std::string print(const Container &v, bool print_separators, typename atermpp::enable_if_container< Container >::type *=nullptr) const
Rewriter that operates on data expressions.
Definition rewriter.h:81
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
\brief A data variable
Definition variable.h:28
const core::identifier_string & name() const
Definition variable.h:38
const sort_expression & sort() const
Definition variable.h:43
logger(const log_level_t l)
Default constructor.
Definition logger.h:164
LPS summand containing a multi-action.
Algorithm class that can be used to apply the binary algorithm.
Definition binary.h:45
data::assignment_list replace_enumerated_parameters_in_assignments(data::assignment_list v)
Replace assignments in v that are of a finite sort with a vector of assignments to Boolean variables.
Definition binary.h:298
data::data_expression make_if_tree(data::variable_vector new_parameters, const data::data_expression_vector &enumerated_elements)
Build an if-then-else tree of enumerated elements in terms of new parameters.
Definition binary.h:77
binary_algorithm(Specification &spec, DataRewriter &r, const std::string parameter_selection="")
Constructor for binary algorithm.
Definition binary.h:395
void update_deadlock_summand(deadlock_summand &s)
Update a deadlock summand with the new Boolean parameters.
Definition binary.h:370
detail::lps_algorithm< Specification > super
Definition binary.h:47
std::map< data::variable, std::vector< data::data_expression > > m_enumerated_elements
Mapping of variables to all values they can be assigned.
Definition binary.h:62
stochastic_process_initializer update_initial_process(const data::variable_list &parameters, const stochastic_process_initializer &init)
Definition binary.h:381
Specification::process_type process_type
Definition binary.h:48
data::set_identifier_generator m_if_trees_generator
Contains the names of variables appearing in rhs of m_if_trees.
Definition binary.h:68
const std::string m_parameter_selection
Definition binary.h:56
void replace_enumerated_parameters(const std::set< data::variable > &selected_params)
Take a specification and calculate a vector of boolean variables for each process parameter in select...
Definition binary.h:160
data::data_expression_list replace_enumerated_parameters_in_initial_expressions(const data::variable_list &vl, const data::data_expression_list &el)
Replace expressions in v that are of a finite sort with a vector of assignments to Boolean variables.
Definition binary.h:236
void update_action_summand(action_summand &s)
Update an action summand with the new Boolean parameters.
Definition binary.h:355
std::set< data::variable > select_parameters(const std::string parameter_selection) const
Determine which variables should be replaced, based on parameter_selection.
Definition binary.h:119
void run()
Apply the algorithm to the specification passed in the constructor.
Definition binary.h:405
process_type::action_summand_type action_summand_type
Definition binary.h:49
data::mutable_map_substitution m_if_trees
Mapping of variables to corresponding if-tree.
Definition binary.h:65
process_initializer update_initial_process(const data::variable_list &parameters, const process_initializer &init)
Definition binary.h:376
DataRewriter m_rewriter
Rewriter.
Definition binary.h:54
std::map< data::variable, std::vector< data::variable > > m_new_parameters
Mapping of finite variables to boolean vectors.
Definition binary.h:59
void update_action_summand(stochastic_action_summand &s)
Update an action summand with the new Boolean parameters.
Definition binary.h:363
data::enumerator_list_element_with_substitution enumerator_element
Definition binary.h:46
data::enumerator_identifier_generator m_id_generator
Identifier generator for the enumerator.
Definition binary.h:71
Algorithm class for elimination of constant parameters.
Definition constelm.h:26
LPS summand containing a deadlock.
Represents a deadlock.
Definition deadlock.h:26
void save_dot_file(std::size_t a_summand_number)
process_type::action_summand_type action_summand_type
bool check_summand(const data::data_expression &a_invariant, const action_summand_type &a_summand, const std::size_t a_summand_number)
action_summand_vector_type f_summands
bool check_summands(const data::data_expression &a_invariant)
bool check_init(const data::data_expression &a_invariant)
Specification::process_type process_type
std::vector< action_summand_type > action_summand_vector_type
bool check_invariant(const data::data_expression &a_invariant)
precondition: the argument passed as parameter a_invariant is a valid expression in internal mCRL2 fo...
Algorithm class for algorithms on linear process specifications. It can be instantiated with lps::spe...
Stores the following properties of a linear process specification:
std::string compare(const specification_property_map< Specification > &other) const
specification_property_map(const Specification &spec)
Constructor Initializes the specification_property_map with a linear process specification.
std::string compare_property(std::string property, std::string x, std::string y) const
data::detail::data_property_map< specification_property_map > super
std::string print(const process::action &a) const
std::string print(const multi_action &x) const
std::string print(const std::set< std::multiset< process::action_label > > &v) const
std::set< std::multiset< process::action_label > > compute_used_multi_actions(const Specification &spec) const
specification_property_map(const std::string &text)
Constructor. The strings may appear in a random order, and not all of them need to be present.
std::string info() const
Returns a textual overview of some properties of an LPS.
std::size_t compute_tau_summand_count(const Specification &spec) const
std::string print(const process::action_label &l) const
std::set< data::variable > compute_used_free_variables(const Specification &spec) const
std::set< process::action_label > compute_used_action_labels(const Specification &spec) const
invelm_algorithm(Specification &a_lps, const data::rewriter::strategy a_rewrite_strategy=data::jitty, const int a_time_limit=0, const bool a_path_eliminator=false, const data::detail::smt_solver_type a_solver_type=data::detail::solver_type_cvc, const bool a_apply_induction=false, const bool a_simplify_all=false)
detail::lps_algorithm< Specification > super
void simplify_summands(SummandSequence &summands, const data::data_expression &invariant, bool apply_prover)
void run(const data::data_expression &invariant, bool apply_prover)
void simplify_summand(summand_base &s, const data::data_expression &invariant, bool apply_prover)
Adds an invariant to the condition of the summand s, and optionally applies the prover to it.
process_type::action_summand_type action_summand_type
data::detail::BDD_Prover f_bdd_prover
Specification::process_type process_type
\brief A timed multi-action
Algorithm class for elimination of unused parameters from a linear process specification.
Definition parelm.h:66
parelm_algorithm(Specification &spec)
Constructor.
Definition parelm.h:250
std::set< data::variable > transition_variables()
Returns the data variables that are considered in the parelm algorithm.
Definition parelm.h:75
void parelm2()
Second version of parelm that builds a dependency graph.
Definition parelm.h:163
void report_results(const std::set< data::variable > &to_be_removed) const
Definition parelm.h:93
void run(bool variant1=true)
Runs the parelm algorithm.
Definition parelm.h:255
void parelm1()
First version of parelm1.
Definition parelm.h:106
lps::detail::lps_algorithm< Specification > super
Definition parelm.h:67
Linear process specification.
LPS summand containing a multi-action.
\brief A stochastic distribution
Base class for LPS summands.
Definition summand.h:25
data::data_expression & condition()
Returns the condition expression.
Definition summand.h:67
\brief An action label
const core::identifier_string & name() const
Standard exception class for reporting runtime errors.
Definition exception.h:27
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
std::string pp(const atermpp::aterm &t)
Transform an aterm to an ascii string.
Definition aterm.h:440
std::string pp(const core::identifier_string &x)
Definition core.cpp:26
std::string pp_format_to_string(const print_format_type pp_format)
Print string representation of pretty print format.
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
smt_solver_type
The enumeration type smt_solver_type enumerates all available SMT solvers.
Definition solver_type.h:27
bool compare_property_maps(const std::string &message, const PropertyMap &map1, const std::string &expected_result)
A collection of utilities for lazy expression construction.
data_expression and_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p or q.
Namespace for system defined sort bool_.
Definition bool.h:32
bool is_false_function_symbol(const atermpp::aterm &e)
Recogniser for function false.
Definition bool.h:119
application and_(const data_expression &arg0, const data_expression &arg1)
Application of function symbol &&.
Definition bool.h:260
application implies(const data_expression &arg0, const data_expression &arg1)
Application of function symbol =>.
Definition bool.h:388
Namespace for all data library functionality.
Definition data.cpp:22
std::vector< assignment > assignment_vector
\brief vector of assignments
Definition assignment.h:149
std::vector< variable > variable_vector
\brief vector of variables
Definition variable.h:89
std::vector< data_expression > data_expression_vector
\brief vector of data_expressions
atermpp::term_list< data_expression > data_expression_list
\brief list of data_expressions
atermpp::term_list< variable > variable_list
\brief list of variables
sort_expression parse_sort_expression(const std::string &text, const data_specification &data_spec=detail::default_specification())
Parses and type checks a sort expression.
Definition parse.h:399
atermpp::term_list< assignment > assignment_list
\brief list of assignments
Definition assignment.h:146
std::string pp(const data::data_expression &x)
Definition data.cpp:52
std::string pp(const data::sort_expression_vector &x)
Definition data.cpp:26
@ warning
Definition logger.h:34
@ verbose
Definition logger.h:37
std::vector< data::variable > find_matching_parameters(const data::variable_list &params, const data::data_specification &dataspec, const std::vector< std::pair< std::string, std::string > > &selections, OutputIterator o)
Find parameter declarations that match a given string.
void collect_transition_variables(const stochastic_action_summand &s, std::set< data::variable > &result)
Definition parelm.h:41
void collect_transition_variables(const deadlock_summand &s, std::set< data::variable > &result)
Definition parelm.h:49
void collect_transition_variables(const action_summand &s, std::set< data::variable > &result)
Definition parelm.h:29
The main namespace for the LPS library.
Definition constelm.h:21
void lpspp(const std::string &input_filename, const std::string &output_filename, bool print_summand_numbers, core::print_format_type format)
Definition tools.cpp:171
void lpssumelm(const std::string &input_filename, const std::string &output_filename, const bool decluster)
Definition tools.cpp:246
void txt2lps(const std::string &input_filename, const std::string &output_filename)
Definition tools.cpp:310
void lpsuntime(const std::string &input_filename, const std::string &output_filename, const bool add_invariants, const bool apply_fourier_motzkin, const data::rewriter::strategy rewrite_strategy)
Definition tools.cpp:296
std::string pp(const lps::stochastic_specification &x)
Definition lps.cpp:37
void lpssuminst(const std::string &input_filename, const std::string &output_filename, const data::rewriter::strategy rewrite_strategy, const std::string &sorts_string, const bool finite_sorts_only, const bool tau_summands_only)
Definition tools.cpp:259
std::size_t nr_of_booleans_for_elements(std::size_t n)
Definition binary.h:27
bool lpsinvelm(const std::string &input_filename, const std::string &output_filename, const std::string &invariant_filename, const std::string &dot_file_name, data::rewriter::strategy rewrite_strategy, data::detail::smt_solver_type solver_type, const bool no_check, const bool no_elimination, const bool simplify_all, const bool all_violations, const bool counter_example, const bool path_eliminator, const bool apply_induction, const int time_limit)
Definition tools.cpp:86
std::string pp(const lps::deadlock &x)
Definition lps.cpp:27
void lpsparelm(const std::string &input_filename, const std::string &output_filename)
Definition tools.cpp:161
std::string pp(const lps::multi_action &x)
Definition lps.cpp:30
void lpsbinary(const std::string &input_filename, const std::string &output_filename, const std::string &parameter_selection)
Definition tools.cpp:31
void parelm(Specification &spec, bool variant1=true)
Removes unused parameters from a linear process specification.
Definition parelm.h:273
lps_rewriter_type
An enumerated type for the available lps rewriters.
void lpsconstelm(const std::string &input_filename, const std::string &output_filename, data::rewriter::strategy rewrite_strategy, bool instantiate_free_variables, bool ignore_conditions, bool remove_trivial_summands, bool remove_singleton_sorts)
Definition tools.cpp:43
void lpsinfo(const std::string &input_filename, const std::string &input_file_message)
Definition tools.cpp:75
void parse_lps< stochastic_specification >(std::istream &from, stochastic_specification &result)
Parses a stochastic linear process specification from an input stream.
Definition parse.h:183
void lpsrewr(const std::string &input_filename, const std::string &output_filename, const data::rewriter::strategy rewrite_strategy, const lps_rewriter_type rewriter_type)
Definition tools.cpp:213
std::string pp_with_summand_numbers(const stochastic_specification &x)
Definition lps.cpp:83
The main namespace for the Process library.
std::string pp(const process::action &x)
Definition process.cpp:35
void iota(Iter first, Iter last, T value)
Generates the sequence value, value + 1, ... and writes it to the sequence [first,...
Definition iota.h:29
std::size_t ceil_log2(std::size_t n)
Definition math.h:28
std::string trim_copy(const std::string &text)
Remove all trailing and leading spaces from the input.
std::string remove_whitespace(const std::string &text)
Removes whitespace from a string.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
std::size_t operator()(const atermpp::detail::reference_aterm< T > &t) const