LCOV - code coverage report
Current view: top level - lps/include/mcrl2/lps/detail - ultimate_delay.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 23 23 100.0 %
Date: 2020-02-19 00:44:21 Functions: 10 10 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jan Friso Groote
       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 ultimate_delay.h
      10             : /// \brief This file defines the class ultimate_delay.
      11             : ///        An ultimate delay consists of a time variable t
      12             : ///        and expression exp(t,x) and free variables x.
      13             : ///        It can be read as a predicate on t of the form
      14             : ///        exists x.exp(t,x). If this is true for certain t, this
      15             : ///        indicates that a process can wait until time t.  
      16             : 
      17             : 
      18             : #ifndef MCRL2_LPS_DETAIL_ULTIMATE_DELAY_H
      19             : #define MCRL2_LPS_DETAIL_ULTIMATE_DELAY_H
      20             : 
      21             : #include "mcrl2/data/real.h"
      22             : 
      23             : namespace mcrl2
      24             : {
      25             : namespace lps
      26             : {
      27             : namespace detail
      28             : {
      29             : 
      30             : using namespace data;
      31             : 
      32        4074 : class ultimate_delay
      33             : {
      34             :   protected:
      35             :     variable m_time;
      36             :     variable_list m_vl;
      37             :     data_expression m_data;
      38             : 
      39             :   public:
      40             :     /// \brief Constructor.
      41        1358 :     ultimate_delay()
      42        1358 :      : m_data(sort_bool::false_())
      43        1358 :      {}
      44             : 
      45             : 
      46             :     /// \brief Constructor.
      47         723 :     ultimate_delay(const variable& t)
      48         723 :      : m_time(t), m_vl(), m_data(sort_bool::true_())
      49             :     {
      50         723 :       assert(t.sort()==sort_real::real_());
      51         723 :     }
      52             : 
      53             :     /// \brief Constructor.
      54         635 :     ultimate_delay(const variable& t, const variable_list& vl, const data_expression& d)
      55         635 :      : m_time(t), m_vl(vl), m_data(d)
      56             :     {
      57         635 :       assert(d.sort()==sort_bool::bool_());
      58         635 :       assert(t.sort()==sort_real::real_());
      59         635 :     }
      60             : 
      61             :     /// \brief Obtain the variables. 
      62        4189 :     const variable_list& variables() const
      63             :     {
      64        4189 :       return m_vl;
      65             :     }
      66             : 
      67             :     /// \brief Reference to the variables. 
      68        2907 :     variable_list& variables()
      69             :     {
      70        2907 :       return m_vl;
      71             :     }
      72             : 
      73             :     /// \brief Obtain the constraint in the ultimate delay.
      74        3934 :     const data_expression& constraint() const
      75             :     {
      76        3934 :       return m_data;
      77             :     }
      78             : 
      79             :     /// \brief Obtain a reference to the constraint. 
      80        5168 :     data_expression& constraint()
      81             :     {
      82        5168 :       return m_data;
      83             :     }
      84             : 
      85             :     /// \brief Obtain the constraint in the ultimate delay.
      86        1685 :     const variable& time_var() const
      87             :     {
      88        1685 :       return m_time;
      89             :     }
      90             : 
      91             :     /// \brief Obtain a reference to the time variable in the ultimate delay.
      92             :     variable& time_var()
      93             :     {
      94             :       return m_time;
      95             :     }
      96             : };
      97             : 
      98             : 
      99             : 
     100             : /// \brief Returns the conjunction of the two delay conditions and the join of the variables, where
     101             : ///        the variables in delay2 are renamed to avoid conflict with those in delay1. 
     102             : ultimate_delay combine_ultimate_delays(const ultimate_delay& delay1, const ultimate_delay& delay2);
     103             : 
     104             : }  // namespace detail
     105             : }  // namespace lps
     106             : }  // namespace mcrl2
     107             : 
     108             : #endif // MCRL2_LPS_DETAIL_ULTIMATE_DELAY_H
     109             : 

Generated by: LCOV version 1.13