Line data Source code
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/process/process_specification.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_PROCESS_PROCESS_SPECIFICATION_H 13 : #define MCRL2_PROCESS_PROCESS_SPECIFICATION_H 14 : 15 : #include "mcrl2/core/load_aterm.h" 16 : #include "mcrl2/core/print.h" 17 : #include "mcrl2/data/data_io.h" 18 : #include "mcrl2/data/detail/io.h" 19 : #include "mcrl2/process/process_equation.h" 20 : 21 : namespace mcrl2 22 : { 23 : 24 : /// \brief The main namespace for the Process library. 25 : namespace process 26 : { 27 : 28 : class process_specification; 29 : atermpp::aterm_appl process_specification_to_aterm(const process_specification& spec); 30 : void complete_data_specification(process_specification&); 31 : 32 : // template function overloads 33 : std::string pp(const process_specification& x); 34 : void normalize_sorts(process_specification& x, const data::sort_specification& sortspec); 35 : void translate_user_notation(process::process_specification& x); 36 : std::set<data::sort_expression> find_sort_expressions(const process::process_specification& x); 37 : std::set<core::identifier_string> find_identifiers(const process::process_specification& x); 38 : std::set<data::variable> find_free_variables(const process::process_specification& x); 39 : 40 : /// \brief Test for a process specification expression 41 : /// \param x A term 42 : /// \return True if \a x is a process specification expression 43 : inline 44 : bool is_process_specification(const atermpp::aterm_appl& x) 45 : { 46 : return x.function() == core::detail::function_symbols::ProcSpec; 47 : } 48 : 49 : /// \brief Process specification consisting of a data specification, action labels, a sequence of process equations and a process initialization. 50 : //<ProcSpec> ::= ProcSpec(<DataSpec>, <ActSpec>, <GlobVarSpec>, <ProcEqnSpec>, <ProcInit>) 51 : class process_specification 52 : { 53 : protected: 54 : /// \brief The data specification of the specification 55 : data::data_specification m_data; 56 : 57 : /// \brief The action specification of the specification 58 : process::action_label_list m_action_labels; 59 : 60 : /// \brief The set of global variables 61 : std::set<data::variable> m_global_variables; 62 : 63 : /// \brief The equations of the specification 64 : std::vector<process_equation> m_equations; 65 : 66 : /// \brief The initial state of the specification 67 : process_expression m_initial_process; 68 : 69 : /// \brief Initializes the specification with an aterm. 70 : /// \param t A term 71 0 : void construct_from_aterm(const atermpp::aterm_appl& t) 72 : { 73 0 : atermpp::aterm_appl::iterator i = t.begin(); 74 0 : m_data = data::data_specification(atermpp::down_cast<atermpp::aterm_appl>(*i++)); 75 0 : m_action_labels = atermpp::down_cast<process::action_label_list>(atermpp::down_cast<atermpp::aterm_appl>(*i++)[0]); 76 0 : data::variable_list global_variables = atermpp::down_cast<data::variable_list>(atermpp::down_cast<atermpp::aterm_appl>(*i++)[0]); 77 0 : m_global_variables = std::set<data::variable>(global_variables.begin(),global_variables.end()); 78 0 : process_equation_list l = atermpp::down_cast<process_equation_list>(atermpp::down_cast<atermpp::aterm_appl>(*i++)[0]); 79 0 : atermpp::aterm_appl init = atermpp::down_cast<atermpp::aterm_appl>(*i); 80 0 : m_initial_process = process_expression(atermpp::down_cast<atermpp::aterm_appl>(init[0])); 81 0 : m_equations = std::vector<process_equation>(l.begin(), l.end()); 82 0 : } 83 : 84 : public: 85 : /// \brief Constructor. 86 1151 : process_specification() 87 1151 : {} 88 : 89 : /// \brief Constructor. 90 : /// \param t A term containing an aterm representation of a process specification. 91 0 : process_specification(atermpp::aterm_appl t) 92 0 : { 93 0 : assert(core::detail::check_term_ProcSpec(t)); 94 0 : construct_from_aterm(t); 95 0 : complete_data_specification(*this); 96 0 : } 97 : 98 : /// \brief Constructor that sets the global variables to empty; 99 : process_specification(data::data_specification data, process::action_label_list action_labels, process_equation_list equations, process_expression init) 100 : : m_data(data), 101 : m_action_labels(action_labels), 102 : m_equations(equations.begin(), equations.end()), 103 : m_initial_process(init) 104 : {} 105 : 106 : /// \brief Constructor of a process specification. 107 : process_specification( 108 : data::data_specification data, 109 : process::action_label_list action_labels, 110 : data::variable_list global_variables, 111 : process_equation_list equations, 112 : process_expression init) 113 : : m_data(data), 114 : m_action_labels(action_labels), 115 : m_global_variables(global_variables.begin(),global_variables.end()), 116 : m_equations(equations.begin(), equations.end()), 117 : m_initial_process(init) 118 : {} 119 : 120 : /// \brief Returns the data specification 121 : /// \return The data specification 122 179 : const data::data_specification& data() const 123 : { 124 179 : return m_data; 125 : } 126 : 127 : /// \brief Returns the data specification 128 : /// \return The data specification 129 6579 : data::data_specification& data() 130 : { 131 6579 : return m_data; 132 : } 133 : 134 : /// \brief Returns the action label specification 135 : /// \return The action label specification 136 1068 : const process::action_label_list& action_labels() const 137 : { 138 1068 : return m_action_labels; 139 : } 140 : 141 : /// \brief Returns the action label specification 142 : /// \return The action label specification 143 6307 : process::action_label_list& action_labels() 144 : { 145 6307 : return m_action_labels; 146 : } 147 : 148 : /// \brief Returns the declared free variables of the process specification. 149 : /// \return The declared free variables of the process specification. 150 1068 : const std::set<data::variable>& global_variables() const 151 : { 152 1068 : return m_global_variables; 153 : } 154 : 155 : /// \brief Returns the declared free variables of the process specification. 156 : /// \return The declared free variables of the process specification. 157 6046 : std::set<data::variable>& global_variables() 158 : { 159 6046 : return m_global_variables; 160 : } 161 : 162 : /// \brief Returns the equations of the process specification 163 : /// \return The equations of the process specification 164 1656 : const std::vector<process_equation>& equations() const 165 : { 166 1656 : return m_equations; 167 : } 168 : 169 : /// \brief Returns the equations of the process specification 170 : /// \return The equations of the process specification 171 7468 : std::vector<process_equation>& equations() 172 : { 173 7468 : return m_equations; 174 : } 175 : 176 : /// \brief Returns the initialization of the process specification 177 : /// \return The initialization of the process specification 178 1455 : const process_expression& init() const 179 : { 180 1455 : return m_initial_process; 181 : } 182 : 183 : /// \brief Returns the initialization of the process specification 184 : /// \return The initialization of the process specification 185 9722 : process_expression& init() 186 : { 187 9722 : return m_initial_process; 188 : } 189 : }; 190 : 191 : //--- start generated class process_specification ---// 192 : // prototype declaration 193 : std::string pp(const process_specification& x); 194 : 195 : /// \\brief Outputs the object to a stream 196 : /// \\param out An output stream 197 : /// \\param x Object x 198 : /// \\return The output stream 199 : inline 200 3 : std::ostream& operator<<(std::ostream& out, const process_specification& x) 201 : { 202 3 : return out << process::pp(x); 203 : } 204 : //--- end generated class process_specification ---// 205 : 206 : /// \brief Adds all sorts that appear in the process specification spec 207 : /// to the data specification of spec. 208 : /// \param spec A process specification 209 : inline 210 0 : void complete_data_specification(process_specification& spec) 211 : { 212 0 : std::set<data::sort_expression> s = process::find_sort_expressions(spec); 213 0 : spec.data().add_context_sorts(s); 214 0 : } 215 : 216 : /// \brief Conversion to aterm_appl. 217 : /// \return The specification converted to aterm format. 218 : /// \param spec A process specification 219 : inline 220 : atermpp::aterm_appl process_specification_to_aterm(const process_specification& spec) 221 : { 222 : return atermpp::aterm_appl(core::detail::function_symbol_ProcSpec(), 223 : data::detail::data_specification_to_aterm(spec.data()), 224 : atermpp::aterm_appl(core::detail::function_symbol_ActSpec(), spec.action_labels()), 225 : atermpp::aterm_appl(core::detail::function_symbol_GlobVarSpec(), data::variable_list(spec.global_variables().begin(),spec.global_variables().end())), 226 : atermpp::aterm_appl(core::detail::function_symbol_ProcEqnSpec(), process_equation_list(spec.equations().begin(), spec.equations().end())), 227 : atermpp::aterm_appl(core::detail::function_symbol_ProcessInit(), spec.init()) 228 : ); 229 : } 230 : 231 : /// \brief Equality operator 232 : inline 233 : bool operator==(const process_specification& spec1, const process_specification& spec2) 234 : { 235 : return process_specification_to_aterm(spec1) == process_specification_to_aterm(spec2); 236 : } 237 : 238 : /// \brief Inequality operator 239 : inline 240 : bool operator!=(const process_specification& spec1, const process_specification& spec2) 241 : { 242 : return !(spec1 == spec2); 243 : } 244 : 245 : } // namespace process 246 : 247 : } // namespace mcrl2 248 : 249 : #endif // MCRL2_PROCESS_PROCESS_SPECIFICATION_H 250 : 251 :