LCOV - code coverage report
Current view: top level - lps/include/mcrl2/lps/detail - make_timed_lps.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 18 26 69.2 %
Date: 2024-03-08 02:52:28 Functions: 3 4 75.0 %
Legend: Lines: hit not hit

          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

Generated by: LCOV version 1.14