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/detail/make_timed_lps.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_LPS_DETAIL_MAKE_TIMED_LPS_H 13 : #define MCRL2_LPS_DETAIL_MAKE_TIMED_LPS_H 14 : 15 : #include "mcrl2/lps/linear_process.h" 16 : 17 : namespace mcrl2 { 18 : 19 : namespace lps { 20 : 21 : namespace detail { 22 : 23 : /// \brief Adds a time parameter t to s if needed and returns the result. The time t 24 : /// is chosen such that it doesn't appear in context. 25 : template <typename IdentifierGenerator> 26 : struct make_timed_lps_summand 27 : { 28 : IdentifierGenerator& m_generator; 29 : 30 5 : make_timed_lps_summand(IdentifierGenerator& generator) 31 5 : : m_generator(generator) 32 5 : {} 33 : 34 : /// \brief Adds time to the summand s (either an action or a deadlock summand) 35 : /// \param s An action summand 36 0 : void operator()(deadlock_summand& s) const 37 : { 38 0 : if (!s.deadlock().has_time()) 39 : { 40 0 : data::variable t(m_generator("T"), data::sort_real::real_()); 41 0 : s.deadlock().time() = t; 42 0 : s.summation_variables() = push_back(s.summation_variables(), t); 43 : /* data::variable_vector v = data::variable_vector(s.summation_variables().begin(),s.summation_variables().end()); 44 : v.push_back(t); 45 : s.summation_variables() = data::variable_list(v.begin(),v.end()); */ 46 0 : } 47 0 : } 48 : 49 : /// \brief Adds time to the summand s (either an action or a deadlock summand) 50 : /// \param s An action summand 51 5 : void operator()(action_summand& s) const 52 : { 53 5 : if (!s.multi_action().has_time()) 54 : { 55 8 : data::variable t(m_generator("T"), data::sort_real::real_()); 56 4 : s.multi_action() = multi_action(s.multi_action().actions(), t); 57 4 : s.summation_variables()=push_back(s.summation_variables(), t); 58 : /* data::variable_vector v = data::variable_vector(s.summation_variables().begin(),s.summation_variables().end()); 59 : v.push_back(t); 60 : s.summation_variables() = data::variable_list(v.begin(),v.end()); 61 : */ 62 4 : } 63 5 : } 64 : }; 65 : 66 : /// \brief Adds time parameters to the lps if needed and returns the result. 67 : /// The times are chosen such that they don't appear in context. 68 : /// \param lps A linear process 69 : /// \param context A term 70 : /// \return A timed linear process 71 : template <class LINEAR_PROCESS> 72 5 : void make_timed_lps(LINEAR_PROCESS& lps, 73 : const std::set<core::identifier_string>& context, 74 : typename std::enable_if<std::is_same<LINEAR_PROCESS, linear_process>::value || 75 : std::is_same<LINEAR_PROCESS, stochastic_linear_process>::value>::type* = nullptr) 76 : { 77 5 : data::set_identifier_generator generator; 78 5 : generator.add_identifiers(context); 79 5 : make_timed_lps_summand<data::set_identifier_generator> f(generator); 80 10 : for (action_summand& s: lps.action_summands()) 81 : { 82 5 : f(s); 83 : } 84 5 : for (deadlock_summand& s: lps.deadlock_summands()) 85 : { 86 0 : f(s); 87 : } 88 5 : } 89 : 90 : } // namespace detail 91 : 92 : } // namespace lps 93 : 94 : } // namespace mcrl2 95 : 96 : #endif // MCRL2_LPS_DETAIL_MAKE_TIMED_LPS_H