12#ifndef MCRL2_DATA_DETAIL_DATA_PROPERTY_MAP_H
13#define MCRL2_DATA_DETAIL_DATA_PROPERTY_MAP_H
15#include "mcrl2/data/variable.h"
32template <
typename Derived =
void >
38 template <
typename Container >
39 static std::string
add_separators(
std::string
const& c,
typename std::enable_if< atermpp::is_set< Container >::value >::type* =
nullptr)
45 template <
typename Container >
46 static std::string
add_separators(
std::string
const& c,
typename std::enable_if< !atermpp::is_set< Container >::value >::type* = 0)
59 std::ostringstream out;
76 return data::pp(v) +
":" + data::pp(v.sort());
79 template <
typename Container >
80 std::string
print(
const Container& v,
typename atermpp::enable_if_container< Container >::type* =
nullptr)
const
82 std::set<std::string> elements;
84 for (
auto i = v.begin(); i != v.end(); ++i)
86 elements.insert(
static_cast< Derived
const& >(*
this).print(*i));
89 return utilities::string_join(elements,
", ");
92 template <
typename Container >
93 std::string
print(
const Container& v,
bool print_separators,
typename atermpp::enable_if_container< Container >::type* =
nullptr)
const
95 return (print_separators) ? add_separators< Container >(print(v)) : print(v);
108 std::vector<std::string> v = utilities::split(text,
",");
109 std::for_each(v.begin(), v.end(), utilities::trim);
110 return std::set<std::string>(v.begin(), v.end());
115 std::set<std::multiset<std::string> > result;
116 std::vector<std::string> multisets = utilities::split(text,
";");
117 for (
const std::string& ms: multisets)
119 std::string s = utilities::regex_replace(
"[{}]",
"", ms);
120 std::vector<std::string> v = utilities::split(s,
",");
121 std::for_each(v.begin(), v.end(), utilities::trim);
122 result.insert(std::multiset<std::string>(v.begin(), v.end()));
132 std::string
compare(
const std::string& property,
unsigned int x,
unsigned int y)
const
136 std::ostringstream out;
137 out <<
"Difference in property " << property <<
" detected: " << x <<
" versus " << y <<
"\n";
149 template <
typename T>
150 std::string
compare(
const std::string& property,
const std::set<T>& x,
const std::set<T>& y)
const
152 std::ostringstream out;
156 std::set_difference(x.begin(), x.end(), y.begin(), y.end(), std::inserter(plus, plus.end()));
160 std::set_difference(y.begin(), y.end(), x.begin(), x.end(), std::inserter(minus, minus.end()));
162 if (!plus.empty() || !minus.empty())
164 out <<
"Difference in property " << property <<
" detected:";
165 for (
auto i = plus.begin(); i != plus.end(); ++i)
167 out <<
" +" << print(*i);
169 for (
auto i = minus.begin(); i != minus.end(); ++i)
171 out <<
" -" << print(*i);
185 return "ERROR: unknown property " + property +
" encountered!";
194 unsigned int result = 0;
195 for (
auto i = m_data.begin(); i != m_data.end(); ++i)
197 result = (std::max)(
static_cast< std::size_t >(result), i->first.size());
208 return s +
std::string(n - s.size(),
' ');
213 template <
typename Container>
216 std::set<core::identifier_string> result;
217 for (
auto i = v.begin(); i != v.end(); ++i)
219 result.insert(i->name());
233 for (
const std::string& line: utilities::split(text,
"\n"))
235 std::vector<std::string> words = utilities::split(line,
"=");
236 if (words.size() == 2)
238 utilities::trim(words[0]);
239 utilities::trim(words[1]);
240 m_data[words[0]] = words[1];
256 std::vector<std::string> lines;
257 for (
auto i = m_data.begin(); i != m_data.end(); ++i)
259 lines.push_back(align(i->first, n) +
" = " + i->second);
261 return utilities::string_join(lines,
"\n");
274 auto i = m_data.find(key);
275 if (i == m_data.end())
277 throw mcrl2::runtime_error(
"property_map: could not find key " + key);
288 std::ostringstream out;
289 for (
auto i = m_data.begin(); i != m_data.end(); ++i)
291 auto j = other.data().find(i->first);
292 if (j != other.data().end())
294 out <<
static_cast< Derived
const& >(*
this).compare_property(i->first, i->second, j->second);
301template <
typename PropertyMap>
304 PropertyMap map2(expected_result);
305 std::string result = map1.compare(map2);
308 std::cerr <<
"------------------------------" <<
std::endl;
309 std::cerr <<
" Failed test " <<
std::endl;
310 std::cerr <<
"------------------------------" <<
std::endl;
311 std::cerr << message <<
std::endl;
312 std::cerr <<
"--- expected result ---" <<
std::endl;
313 std::cerr << expected_result <<
std::endl;
314 std::cerr <<
"--- found result ---" <<
std::endl;
315 std::cerr << map1.to_string() <<
std::endl;
316 std::cerr <<
"--- differences ---" <<
std::endl;
317 std::cerr << result <<
std::endl;
319 return result.empty();
aterm_string(const std::string &s)
Constructor that allows construction from a string.
bool operator==(const unprotected_aterm_core &t) const
Comparison operator.
bool operator!=(const unprotected_aterm_core &t) const
Inequality operator on two unprotected aterms.
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.
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
const core::identifier_string & name() const
const sort_expression & sort() const
logger(const log_level_t l)
Default constructor.
LPS summand containing a multi-action.
Algorithm class that can be used to apply the binary algorithm.
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.
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.
binary_algorithm(Specification &spec, DataRewriter &r, const std::string parameter_selection="")
Constructor for binary algorithm.
void update_deadlock_summand(deadlock_summand &s)
Update a deadlock summand with the new Boolean parameters.
detail::lps_algorithm< Specification > super
std::map< data::variable, std::vector< data::data_expression > > m_enumerated_elements
Mapping of variables to all values they can be assigned.
stochastic_process_initializer update_initial_process(const data::variable_list ¶meters, const stochastic_process_initializer &init)
Specification::process_type process_type
data::set_identifier_generator m_if_trees_generator
Contains the names of variables appearing in rhs of m_if_trees.
const std::string m_parameter_selection
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...
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.
void update_action_summand(action_summand &s)
Update an action summand with the new Boolean parameters.
std::set< data::variable > select_parameters(const std::string parameter_selection) const
Determine which variables should be replaced, based on parameter_selection.
void run()
Apply the algorithm to the specification passed in the constructor.
process_type::action_summand_type action_summand_type
data::mutable_map_substitution m_if_trees
Mapping of variables to corresponding if-tree.
process_initializer update_initial_process(const data::variable_list ¶meters, const process_initializer &init)
DataRewriter m_rewriter
Rewriter.
std::map< data::variable, std::vector< data::variable > > m_new_parameters
Mapping of finite variables to boolean vectors.
void update_action_summand(stochastic_action_summand &s)
Update an action summand with the new Boolean parameters.
data::enumerator_list_element_with_substitution enumerator_element
data::enumerator_identifier_generator m_id_generator
Identifier generator for the enumerator.
Algorithm class for elimination of constant parameters.
LPS summand containing a deadlock.
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
std::string print(const deadlock &x) 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
\brief A timed multi-action
Linear process specification.
LPS summand containing a multi-action.
\brief A stochastic distribution
A stochastic process initializer.
Linear process specification.
const core::identifier_string & name() const
Standard exception class for reporting runtime errors.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
std::string pp(const atermpp::aterm &t)
Transform an aterm to an ascii string.
std::string pp(const core::identifier_string &x)
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.
bool compare_property_maps(const std::string &message, const PropertyMap &map1, const std::string &expected_result)
Namespace for all data library functionality.
std::vector< assignment > assignment_vector
\brief vector of assignments
std::vector< variable > variable_vector
\brief vector of variables
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.
atermpp::term_list< assignment > assignment_list
\brief list of assignments
std::string pp(const data::sort_expression_vector &x)
std::vector< data::variable > find_matching_parameters(const data::variable_list ¶ms, 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.
The main namespace for the LPS library.
void lpspp(const std::string &input_filename, const std::string &output_filename, bool print_summand_numbers, core::print_format_type format)
void lpssumelm(const std::string &input_filename, const std::string &output_filename, const bool decluster)
void txt2lps(const std::string &input_filename, const std::string &output_filename)
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)
std::string pp(const lps::stochastic_specification &x)
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)
std::size_t nr_of_booleans_for_elements(std::size_t n)
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)
std::string pp(const lps::deadlock &x)
void lpsparelm(const std::string &input_filename, const std::string &output_filename)
std::string pp(const lps::multi_action &x)
void lpsbinary(const std::string &input_filename, const std::string &output_filename, const std::string ¶meter_selection)
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)
void lpsinfo(const std::string &input_filename, const std::string &input_file_message)
void parse_lps< stochastic_specification >(std::istream &from, stochastic_specification &result)
Parses a stochastic linear process specification from an input stream.
void lpsrewr(const std::string &input_filename, const std::string &output_filename, const data::rewriter::strategy rewrite_strategy, const lps_rewriter_type rewriter_type)
std::string pp_with_summand_numbers(const stochastic_specification &x)
The main namespace for the Process library.
std::string pp(const process::action &x)
std::size_t ceil_log2(std::size_t n)
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