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/lps/linear_process.h 10 : /// \brief The class linear_process. 11 : 12 : #ifndef MCRL2_LPS_LINEAR_PROCESS_H 13 : #define MCRL2_LPS_LINEAR_PROCESS_H 14 : 15 : #include "mcrl2/lps/action_summand.h" 16 : #include "mcrl2/lps/deadlock_summand.h" 17 : // #include "mcrl2/lps/process_initializer.h" Is not used in this file. 18 : 19 : namespace mcrl2 20 : { 21 : 22 : namespace lps 23 : { 24 : 25 : namespace detail 26 : { 27 : 28 : // helper function for linear_process_base::linear_process_base(const atermpp::aterm_appl& lps) 29 : template <typename Summand> 30 : Summand make_action_summand(const data::variable_list&, 31 : const data::data_expression&, 32 : const multi_action&, 33 : const data::assignment_list&, 34 : const stochastic_distribution& 35 : ) 36 : { 37 : throw mcrl2::runtime_error("make_action_summand is not defined!"); 38 : } 39 : 40 : template <> 41 : inline 42 : action_summand make_action_summand<action_summand>(const data::variable_list& summation_variables, 43 : const data::data_expression& condition, 44 : const multi_action& a, 45 : const data::assignment_list& assignments, 46 : const stochastic_distribution& distribution 47 : ) 48 : { 49 : (void)distribution; // Suppress an unused variable warning. 50 : assert(!distribution.is_defined()); 51 : return action_summand(summation_variables, condition, a, assignments); 52 : } 53 : 54 : } // namespace detail 55 : 56 : class linear_process; // prototype declaration 57 : bool check_well_typedness(const linear_process& x); 58 : 59 : class stochastic_linear_process; // prototype declaration 60 : bool check_well_typedness(const stochastic_linear_process& x); 61 : 62 : template <typename ActionSummand> 63 : class linear_process_base 64 : { 65 : protected: 66 : /// \brief The process parameters of the process 67 : data::variable_list m_process_parameters; 68 : 69 : /// \brief The deadlock summands of the process 70 : deadlock_summand_vector m_deadlock_summands; 71 : 72 : /// \brief The action summands of the process 73 : std::vector<ActionSummand> m_action_summands; 74 : 75 : public: 76 : /// \brief The action summand type 77 : typedef ActionSummand action_summand_type; 78 : 79 : /// \brief Constructor. 80 14444 : linear_process_base() = default; 81 : 82 : /// \brief Constructor. 83 2032 : linear_process_base(const data::variable_list& process_parameters, 84 : const deadlock_summand_vector& deadlock_summands, 85 : const std::vector<ActionSummand>& action_summands 86 : ) 87 : : 88 2032 : m_process_parameters(process_parameters), 89 2032 : m_deadlock_summands(deadlock_summands), 90 2032 : m_action_summands(action_summands) 91 2032 : { } 92 : 93 : /// \brief Constructor. 94 : /// \param lps A term. 95 : /// \param stochastic_distributions_allowed True when stochastic processes are allowed 96 : explicit linear_process_base(const atermpp::aterm_appl& lps, bool stochastic_distributions_allowed = true) 97 : { 98 : using atermpp::down_cast; 99 : assert(core::detail::check_term_LinearProcess(lps)); 100 : m_process_parameters = down_cast<data::variable_list>(lps[0]); 101 : const auto& summands = atermpp::down_cast<atermpp::aterm_list>(lps[1]); 102 : for (const atermpp::aterm& summand: summands) 103 : { 104 : assert(core::detail::check_rule_LinearProcessSummand(summand)); 105 : const auto& t = down_cast<atermpp::aterm_appl>(summand); 106 : 107 : const auto& summation_variables = down_cast<data::variable_list>(t[0]); 108 : const auto& condition = down_cast<data::data_expression>(t[1]); 109 : const auto& time = down_cast<data::data_expression>(t[3]); 110 : const auto& assignments = down_cast<data::assignment_list>(t[4]); 111 : const auto& distribution = down_cast<stochastic_distribution>(t[5]); 112 : if (!stochastic_distributions_allowed && distribution.is_defined()) 113 : { 114 : throw mcrl2::runtime_error("Summand with stochastic distribution encountered, while this tool is not yet able to deal with stochastic distributions."); 115 : } 116 : if (down_cast<atermpp::aterm_appl>(t[2]).function() == core::detail::function_symbols::Delta) 117 : { 118 : m_deadlock_summands.push_back(deadlock_summand(summation_variables, condition, deadlock(time))); 119 : } 120 : else 121 : { 122 : assert(lps::is_multi_action(down_cast<atermpp::aterm_appl>(t[2]))); 123 : const auto& actions = down_cast<process::action_list>(down_cast<atermpp::aterm_appl>(t[2])[0]); 124 : m_action_summands.push_back(detail::make_action_summand<ActionSummand>(summation_variables, condition, multi_action(actions, time), assignments, distribution)); 125 : } 126 : } 127 : } 128 : 129 : /// \brief Returns the number of LPS summands. 130 : /// \return The number of LPS summands. 131 41 : std::size_t summand_count() const 132 : { 133 41 : return m_deadlock_summands.size() + m_action_summands.size(); 134 : } 135 : 136 : /// \brief Returns the sequence of action summands. 137 : /// \return The sequence of action summands. 138 35985 : const std::vector<ActionSummand>& action_summands() const 139 : { 140 35985 : return m_action_summands; 141 : } 142 : 143 : /// \brief Returns the sequence of action summands. 144 : /// \return The sequence of action summands. 145 6106 : std::vector<ActionSummand>& action_summands() 146 : { 147 6106 : return m_action_summands; 148 : } 149 : 150 : /// \brief Returns the sequence of deadlock summands. 151 : /// \return The sequence of deadlock summands. 152 6065 : const deadlock_summand_vector& deadlock_summands() const 153 : { 154 6065 : return m_deadlock_summands; 155 : } 156 : 157 : /// \brief Returns the sequence of deadlock summands. 158 : /// \return The sequence of deadlock summands. 159 3973 : deadlock_summand_vector& deadlock_summands() 160 : { 161 3973 : return m_deadlock_summands; 162 : } 163 : 164 : /// \brief Returns the sequence of process parameters. 165 : /// \return The sequence of process parameters. 166 18609 : const data::variable_list& process_parameters() const 167 : { 168 18609 : return m_process_parameters; 169 : } 170 : 171 : /// \brief Returns the sequence of process parameters. 172 : /// \return The sequence of process parameters. 173 5218 : data::variable_list& process_parameters() 174 : { 175 5218 : return m_process_parameters; 176 : } 177 : 178 : /// \brief Returns true if time is available in at least one of the summands. 179 : /// \return True if time is available in at least one of the summands. 180 316 : bool has_time() const 181 : { 182 1126 : for (auto i = m_action_summands.begin(); i != m_action_summands.end(); ++i) 183 : { 184 821 : if (i->has_time()) 185 : { 186 11 : return true; 187 : } 188 : } 189 457 : for (auto i = m_deadlock_summands.begin(); i != m_deadlock_summands.end(); ++i) 190 : { 191 152 : if (i->deadlock().has_time()) 192 : { 193 0 : return true; 194 : } 195 : } 196 305 : return false; 197 : } 198 : }; 199 : 200 : /// \brief linear process. 201 : class linear_process: public linear_process_base<action_summand> 202 : { 203 : typedef linear_process_base<action_summand> super; 204 : 205 : public: 206 : /// \brief Constructor. 207 474 : linear_process() = default; 208 : 209 : /// \brief Constructor. 210 141 : linear_process(const data::variable_list& process_parameters, 211 : const deadlock_summand_vector& deadlock_summands, 212 : const action_summand_vector& action_summands 213 : ) 214 141 : : super(process_parameters, deadlock_summands, action_summands) 215 141 : { } 216 : 217 : /// \brief Constructor. 218 : /// \param lps A term 219 : explicit linear_process(const atermpp::aterm_appl& lps, bool = false) 220 : : super(lps, false) 221 : { } 222 : }; 223 : 224 : /// \brief Conversion to aterm_appl. 225 : /// \return The action summand converted to aterm format. 226 : template <typename ActionSummand> 227 140 : atermpp::aterm_appl linear_process_to_aterm(const linear_process_base<ActionSummand>& p) 228 : { 229 140 : atermpp::term_list<atermpp::aterm_appl> summands; 230 172 : for (auto i = p.deadlock_summands().rbegin(); i != p.deadlock_summands().rend(); ++i) 231 : { 232 32 : atermpp::aterm_appl s = deadlock_summand_to_aterm(*i); 233 32 : summands.push_front(s); 234 : } 235 273 : for (auto i = p.action_summands().rbegin(); i != p.action_summands().rend(); ++i) 236 : { 237 133 : atermpp::aterm_appl s = action_summand_to_aterm(*i); 238 133 : summands.push_front(s); 239 : } 240 : 241 : return atermpp::aterm_appl(core::detail::function_symbol_LinearProcess(), 242 140 : p.process_parameters(), 243 : summands 244 280 : ); 245 140 : } 246 : 247 : //--- start generated class linear_process ---// 248 : // prototype declaration 249 : std::string pp(const linear_process& x); 250 : 251 : /// \\brief Outputs the object to a stream 252 : /// \\param out An output stream 253 : /// \\param x Object x 254 : /// \\return The output stream 255 : inline 256 : std::ostream& operator<<(std::ostream& out, const linear_process& x) 257 : { 258 : return out << lps::pp(x); 259 : } 260 : //--- end generated class linear_process ---// 261 : 262 : /// \brief Test for a linear_process expression 263 : /// \param x A term 264 : /// \return True if \a x is a linear process expression 265 : inline 266 : bool is_linear_process(const atermpp::aterm_appl& x) 267 : { 268 : return x.function() == core::detail::function_symbols::LinearProcess; 269 : } 270 : 271 : // template function overloads 272 : std::set<data::variable> find_all_variables(const lps::linear_process& x); 273 : std::set<data::variable> find_free_variables(const lps::linear_process& x); 274 : std::set<process::action_label> find_action_labels(const lps::linear_process& x); 275 : 276 : } // namespace lps 277 : 278 : } // namespace mcrl2 279 : 280 : #endif // MCRL2_LPS_LINEAR_PROCESS_H