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: 19 28 67.9 %
Date: 2020-02-19 00:44:21 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 :       data::variable_vector v = data::variable_vector(s.summation_variables().begin(),s.summation_variables().end());
      43           0 :       v.push_back(t);
      44           0 :       s.summation_variables() = data::variable_list(v.begin(),v.end());
      45             :     }
      46           0 :   }
      47             : 
      48             :   /// \brief Adds time to the summand s (either an action or a deadlock summand)
      49             :   /// \param s An action summand
      50           5 :   void operator()(action_summand& s) const
      51             :   {
      52           5 :     if (!s.multi_action().has_time())
      53             :     {
      54           8 :       data::variable t(m_generator("T"), data::sort_real::real_());
      55           4 :       s.multi_action().time() = t;
      56           8 :       data::variable_vector v = data::variable_vector(s.summation_variables().begin(),s.summation_variables().end());
      57           4 :       v.push_back(t);
      58           4 :       s.summation_variables() = data::variable_list(v.begin(),v.end());
      59             :     }
      60           5 :   }
      61             : };
      62             : 
      63             : /// \brief Adds time parameters to the lps if needed and returns the result.
      64             : /// The times are chosen such that they don't appear in context.
      65             : /// \param lps A linear process
      66             : /// \param context A term
      67             : /// \return A timed linear process
      68             : inline
      69           5 : void make_timed_lps(linear_process& lps, const std::set<core::identifier_string>& context)
      70             : {
      71          10 :   data::set_identifier_generator generator;
      72           5 :   generator.add_identifiers(context);
      73           5 :   make_timed_lps_summand<data::set_identifier_generator> f(generator);
      74          10 :   for (action_summand& s: lps.action_summands())
      75             :   {
      76           5 :     f(s);
      77             :   }
      78           5 :   for (deadlock_summand& s: lps.deadlock_summands())
      79             :   {
      80           0 :     f(s);
      81             :   }
      82           5 : }
      83             : 
      84             : } // namespace detail
      85             : 
      86             : } // namespace lps
      87             : 
      88             : } // namespace mcrl2
      89             : 
      90             : #endif // MCRL2_LPS_DETAIL_MAKE_TIMED_LPS_H

Generated by: LCOV version 1.13