mCRL2
Loading...
Searching...
No Matches
equal_sorts.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/equal_sorts.h
10/// \brief add your file description here.
11
12#ifndef MCRL2_DATA_DETAIL_EQUAL_SORTS_H
13#define MCRL2_DATA_DETAIL_EQUAL_SORTS_H
14
15#include "mcrl2/data/data_specification.h"
16
17namespace mcrl2 {
18
19namespace data {
20
21namespace detail {
22
23/// \brief Checks if the sorts of the variables/expressions in both lists are equal.
24/// \param v A sequence of data variables
25/// \param w A sequence of data expressions
26/// \return True if the sorts match pairwise
27inline
28bool equal_sorts(const data::variable_list& v, const data::data_expression_list& w, const data::data_specification& data_spec)
29{
30 if (v.size() != w.size())
31 {
32 return false;
33 }
34 data::variable_list::iterator i = v.begin();
35 data::data_expression_list::iterator j = w.begin();
36 for (; i != v.end(); ++i, ++j)
37 {
38 if (!data_spec.equal_sorts(i->sort(), j->sort()))
39 {
40 return false;
41 }
42 }
43 return true;
44}
45
46} // namespace detail
47
48} // namespace data
49
50} // namespace mcrl2
51
52#endif // MCRL2_DATA_DETAIL_EQUAL_SORTS_H
bool operator==(const unprotected_aterm_core &t) const
Comparison operator.
Definition aterm_core.h:83
bool is_well_typed() const
Returns true if.
Algorithm class for the abstract algorithm.
Definition abstract.h:120
void run(pbes &p, const detail::pbes_parameter_map &parameter_map, bool value_true)
Runs the algorithm.
Definition abstract.h:126
parameterized boolean equation system
Definition pbes.h:58
std::set< data::variable > & global_variables()
Returns the declared free variables of the pbes.
Definition pbes.h:185
bool is_closed() const
True if the pbes is closed.
Definition pbes.h:245
data::data_specification m_data
The data specification.
Definition pbes.h:64
pbes(const data::data_specification &data, const std::vector< pbes_equation > &equations, propositional_variable_instantiation initial_state)
Constructor.
Definition pbes.h:116
std::set< data::variable > m_global_variables
The set of global variables.
Definition pbes.h:70
std::set< propositional_variable > compute_declared_variables() const
Returns the predicate variables appearing in the left hand side of an equation.
Definition pbes.h:77
pbes_equation equation_type
Definition pbes.h:60
pbes(const data::data_specification &data, const std::set< data::variable > &global_variables, const std::vector< pbes_equation > &equations, propositional_variable_instantiation initial_state)
Constructor.
Definition pbes.h:134
const propositional_variable_instantiation & initial_state() const
Returns the initial state.
Definition pbes.h:192
std::set< propositional_variable > binding_variables() const
Returns the set of binding variables of the pbes. This is the set variables that occur on the left ha...
Definition pbes.h:207
std::set< propositional_variable > occurring_variables() const
Returns the set of occurring propositional variable declarations of the pbes, i.e....
Definition pbes.h:227
std::set< propositional_variable_instantiation > occurring_variable_instantiations() const
Returns the set of occurring propositional variable instantiations of the pbes. This is the set of va...
Definition pbes.cpp:108
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the pbes.
Definition pbes.h:178
std::vector< pbes_equation > & equations()
Returns the equations.
Definition pbes.h:171
propositional_variable_instantiation & initial_state()
Returns the initial state.
Definition pbes.h:199
propositional_variable_instantiation m_initial_state
The initial state.
Definition pbes.h:73
pbes()=default
Constructor.
std::vector< pbes_equation > m_equations
The sequence of pbes equations.
Definition pbes.h:67
bool is_declared_in(Iter first, Iter last, const propositional_variable_instantiation &v, const data::data_specification &data_spec) const
Checks if the propositional variable instantiation v appears with the right type in the sequence of p...
Definition pbes.h:96
const std::vector< pbes_equation > & equations() const
Returns the equations.
Definition pbes.h:164
bool is_well_typed() const
Checks if the PBES is well typed.
Definition pbes.h:267
\brief A propositional variable instantiation
const data::data_expression_list & parameters() const
propositional_variable_instantiation(const propositional_variable_instantiation &) noexcept=default
Move semantics.
Standard exception class for reporting runtime errors.
Definition exception.h:27
Simple timer to time the CPU time used by a piece of code.
void write_report(std::ostream &s)
Write the report to an output stream.
std::map< std::string, timing > m_timings
collection of timings
void start(const std::string &timing_name)
Start measurement with a hint.
std::string m_filename
name of the file to write timings to
void finish(const std::string &timing_name)
Finish a measurement with a hint.
void report()
Write all timing information that has been recorded.
execution_timer(const std::string &tool_name="", std::string const &filename="")
Constructor of a simple execution timer.
std::string m_tool_name
name of the tool we are timing
std::vector< std::string > m_extensions
const std::string & shortname() const
bool operator==(const file_format &other) const
bool operator<(const file_format &other) const
const std::string & description() const
The main namespace for the aterm++ library.
Definition algorithm.h:21
bool equal_sorts(const data::variable_list &v, const data::data_expression_list &w, const data::data_specification &data_spec)
Checks if the sorts of the variables/expressions in both lists are equal.
Definition equal_sorts.h:28
Namespace for all data library functionality.
Definition data.cpp:22
rewrite_strategy
The strategy of the rewriter.
atermpp::term_list< data_expression > data_expression_list
\brief list of data_expressions
atermpp::term_list< variable > variable_list
\brief list of variables
void normalize(pbes &x)
The function normalize brings (embedded) pbes expressions into positive normal form,...
std::map< core::identifier_string, std::vector< data::variable > > pbes_parameter_map
Data structure for storing the variables that should be expanded by the finite pbesinst algorithm.
pbes_parameter_map parse_pbes_parameter_map(const pbes &p, const std::string &text)
Parses parameter selection for finite pbesinst algorithm.
The main namespace for the PBES library.
bool is_pbes_file_format(const utilities::file_format &format)
Definition io.h:29
void lps2pbes(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, const std::string &formula_filename, bool timed, bool structured, bool unoptimized, bool preprocess_modal_operators, bool generate_counter_example, bool check_only)
Definition lps2pbes.h:42
std::set< data::variable > find_free_variables(const pbes_system::pbes &x)
Definition pbes.cpp:54
std::string description(const absinthe_strategy strategy)
Prints an absinthe strategy.
std::istream & operator>>(std::istream &is, pbesinst_strategy &s)
std::istream & operator>>(std::istream &is, absinthe_strategy &strategy)
pbes_rewriter_type parse_pbes_rewriter_type(const std::string &type)
Parses a pbes rewriter type.
void pbesabstract(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, const std::string &parameter_selection, bool value_true)
pbes_rewriter_type
An enumerated type for the available pbes rewriters.
std::set< data::sort_expression > find_sort_expressions(const pbes_system::pbes &x)
Definition pbes.cpp:52
const utilities::file_format & pbes_format_internal_bes()
Definition io.h:46
void txt2pbes(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, bool normalize)
Definition txt2pbes.h:21
void pbesstategraph(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, const pbesstategraph_options &options)
void lpsbisim2pbes(const std::string &input_filename1, const std::string &input_filename2, const std::string &output_filename, const utilities::file_format &output_format, bisimulation_type type, bool normalize)
const utilities::file_format & pbes_format_pgsolver()
Definition io.h:48
void complps2pbes(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, const std::string &formula_filename)
void normalize_sorts(pbes_system::pbes &x, const data::sort_specification &)
Definition pbes.cpp:48
pbesinst_strategy
pbesinst transformation strategies
void pbesrewr(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type)
Definition pbesrewr.h:31
std::istream & operator>>(std::istream &is, pbes_rewriter_type &t)
Stream operator for rewriter type.
bool is_well_typed_pbes(const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const std::set< data::variable > &occurring_global_variables, const std::set< propositional_variable > &declared_variables, const std::set< propositional_variable_instantiation > &occ, const propositional_variable_instantiation &init, const data::data_specification &data_spec)
Definition pbes.cpp:91
void pbesinfo(const std::string &input_filename, const std::string &input_file_message, const utilities::file_format &file_format, bool opt_full)
Definition pbesinfo.h:22
std::set< data::function_symbol > find_function_symbols(const pbes_system::pbes &x)
Definition pbes.cpp:57
void pbespareqelm(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type, bool ignore_initial_state)
void pbespp(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, core::print_format_type format, bool use_pfnf_printer)
Definition pbespp.h:22
void pbesparelm(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format)
Definition pbesparelm.h:22
pbesinst_strategy parse_pbesinst_strategy(const std::string &s)
Parse a pbesinst transformation strategy.
atermpp::aterm pbes_to_aterm(const pbes &p)
Conversion to atermappl.
Definition io.cpp:328
std::string print_pbesinst_strategy(const pbesinst_strategy strategy)
Returns a string representation of a pbesinst transformation strategy.
std::istream & operator>>(std::istream &is, bisimulation_type &t)
bool operator==(const pbes &p1, const pbes &p2)
Equality operator on PBESs.
Definition pbes.h:325
const std::vector< utilities::file_format > & pbes_file_formats()
Definition io.cpp:26
void save_bes_pgsolver(const pbes &bes, std::ostream &stream, bool maxpg)
Definition pgsolver.cpp:142
std::string print_pbes_rewriter_type(const pbes_rewriter_type type)
Prints a pbes rewriter type.
std::string pp(const pbes_system::pbes &x)
Definition pbes.cpp:42
std::string print_absinthe_strategy(const absinthe_strategy strategy)
Prints an absinthe strategy.
void save_pbes(const pbes &pbes, std::ostream &stream, utilities::file_format format)
Save a PBES in the format specified.
Definition io.cpp:49
std::string print_bisimulation_type(const bisimulation_type t)
Returns a description of a bisimulation type.
std::set< data::variable > find_all_variables(const pbes_system::pbes &x)
Definition pbes.cpp:53
void complete_data_specification(pbes &)
Adds all sorts that appear in the PBES p to the data specification of p.
Definition pbes.h:314
bisimulation_type
An enumerated type for the available bisimulation types.
const utilities::file_format & pbes_format_internal()
Definition io.h:42
void pbesconstelm(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type, bool compute_conditions, bool remove_redundant_equations, bool check_quantifiers)
const utilities::file_format & pbes_format_text()
Definition io.h:44
bool is_well_typed_equation(const pbes_equation &eqn, const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const data::data_specification &data_spec)
Definition pbes.cpp:82
absinthe_strategy parse_absinthe_strategy(const std::string &strategy)
Parses an absinthe strategy.
std::string description(const pbes_rewriter_type type)
Returns a description of a pbes rewriter.
std::string description(const pbesinst_strategy strategy)
Returns a string representation of a pbesinst transformation strategy.
void translate_user_notation(pbes_system::pbes &x)
Definition pbes.cpp:50
std::string description(const bisimulation_type t)
Returns a description of a bisimulation type.
void pbesabsinthe(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, const std::string &abstraction_file, absinthe_strategy strategy, bool print_used_function_symbols, bool enable_logging)
bisimulation_type parse_bisimulation_type(const std::string &type)
Returns the string corresponding to a bisimulation type.
absinthe_strategy
The approximation strategies of the absinthe tool.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Pair of start and finish times.
std::chrono::steady_clock::time_point finish
std::chrono::steady_clock::time_point start
std::size_t operator()(const atermpp::detail::reference_aterm< T > &t) const