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             : 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        1455 :     ultimate_delay()
      42        1455 :      : m_data(sort_bool::false_())
      43        1455 :      {}
      44             : 
      45             : 
      46             :     /// \brief Constructor.
      47         799 :     ultimate_delay(const variable& t)
      48         799 :      : m_time(t), m_vl(), m_data(sort_bool::true_())
      49             :     {
      50         799 :       assert(t.sort()==sort_real::real_());
      51         799 :     }
      52             : 
      53             :     /// \brief Constructor.
      54         656 :     ultimate_delay(const variable& t, const variable_list& vl, const data_expression& d)
      55         656 :      : m_time(t), m_vl(vl), m_data(d)
      56             :     {
      57         656 :       assert(d.sort()==sort_bool::bool_());
      58         656 :       assert(t.sort()==sort_real::real_());
      59         656 :     }
      60             : 
      61             :     /// \brief Obtain the variables. 
      62        5250 :     const variable_list& variables() const
      63             :     {
      64        5250 :       return m_vl;
      65             :     }
      66             : 
      67             :     /// \brief Reference to the variables. 
      68        3279 :     variable_list& variables()
      69             :     {
      70        3279 :       return m_vl;
      71             :     }
      72             : 
      73             :     /// \brief Obtain the constraint in the ultimate delay.
      74        5072 :     const data_expression& constraint() const
      75             :     {
      76        5072 :       return m_data;
      77             :     }
      78             : 
      79             :     /// \brief Obtain a reference to the constraint. 
      80        5682 :     data_expression& constraint()
      81             :     {
      82        5682 :       return m_data;
      83             :     }
      84             : 
      85             :     /// \brief Obtain the constraint in the ultimate delay.
      86        1675 :     const variable& time_var() const
      87             :     {
      88        1675 :       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             :