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             : 
      10             : /** \file
      11             :  *
      12             :  * \brief This file contains a class that contains labels for probabilistic transitions as a mCRL2 data expression of type real.
      13             :  * \author Jan Friso Groote
      14             :  */
      15             : 
      16             : 
      17             : #ifndef MCRL2_LPS_PROBABILISTIC_DATA_EXPRESSION_H
      18             : #define MCRL2_LPS_PROBABILISTIC_DATA_EXPRESSION_H
      19             : 
      20             : #include "mcrl2/data/rewriter.h"
      21             : 
      22             : 
      23             : namespace mcrl2
      24             : {
      25             : namespace lps
      26             : {
      27             : 
      28             : /** \brief This class contains labels for probabilistic transistions, consisting of a numerator and a denumerator.
      29             :  *  \details This class provides a number of operators to calculate with real constants (actually fractions). 
      30             :  *           Comparisons of more complex expressions may not always rewrite properly. 
      31             :  *           There are methods to add and subtract such labels. The numbers are used as 64 bit integers.
      32             :  *           If the integers do not fit into 64 bit, the numerator and denumerator are adapted to make
      33             :  *           them fit. This means that this library is not exact, but employs rounding at times.
      34             :  *
      35             :  */
      36             : class probabilistic_data_expression: public data::data_expression
      37             : {
      38             : 
      39             :   protected:
      40             : 
      41           2 :     static data::data_specification data_specification_with_real()
      42             :     {
      43           2 :       data::data_specification d;
      44           2 :       d.add_sort(data::sort_real::real_());
      45           2 :       return d;
      46           0 :     }
      47             : 
      48        3039 :     static const data::rewriter& m_rewriter()
      49             :     {
      50        3039 :       static data::rewriter m_r(data_specification_with_real());
      51        3039 :       return m_r;
      52             :     }
      53             : 
      54             :     inline static std::size_t to_number_t(const std::string& s)
      55             :     {
      56             :       return std::stoul(s);
      57             :     }
      58             : 
      59             :     // An algorithm to calculate the greatest common divisor
      60             :     static std::size_t greatest_common_divisor(std::size_t x, std::size_t y)
      61             :     {
      62             :       if (x==0) return y;
      63             :       if (y==0) return x;
      64             :       if (x>y)
      65             :       {
      66             :         const std::size_t temp=x; x=y; y=temp; // swap(x,y)
      67             :       }
      68             : 
      69             :       std::size_t remainder=y % x;
      70             :       while (remainder!=0)
      71             :       {
      72             :         y=x;
      73             :         x=remainder;
      74             :         remainder=y % x;
      75             :       }
      76             :       return x;
      77             :     }
      78             : 
      79             :     void remove_common_factors(std::size_t& enumerator, std::size_t& denominator)
      80             :     {
      81             :       std::size_t gcd=greatest_common_divisor(enumerator,denominator);
      82             :       while (gcd!=1)
      83             :       {
      84             :         enumerator=enumerator/gcd;
      85             :         denominator=denominator/gcd;
      86             :       }
      87             :     }
      88             : 
      89             : 
      90             :   public:
      91             :     /// \brief Constant zero.
      92        1618 :     static probabilistic_data_expression zero()
      93             :     {
      94             :       using namespace data;
      95        1618 :       static probabilistic_data_expression zero(sort_real::creal(data::sort_int::cint(sort_nat::c0()),sort_pos::c1()));
      96        1618 :       return zero;
      97             :     }
      98             : 
      99             :     /// \brief Constant one.
     100        1162 :     static probabilistic_data_expression one()
     101             :     {
     102             :       using namespace data;
     103        1162 :       static probabilistic_data_expression one(sort_real::creal(data::sort_int::cint(sort_nat::cnat(sort_pos::c1())),sort_pos::c1()));
     104        1162 :       return one;
     105             :     }
     106             : 
     107             :     /* \brief Default constructor. 
     108             :      */
     109          56 :     probabilistic_data_expression()
     110          56 :      : data::data_expression(zero())
     111          56 :     {}
     112             : 
     113             :     /** \brief Construct a probabilistic_data_expression from a data_expression, which must be of sort real.
     114             :      */
     115        1002 :     explicit probabilistic_data_expression(const data::data_expression& d)
     116        1002 :      : data::data_expression(d)
     117             :     { 
     118        1002 :       assert(d.sort()==data::sort_real::real_());
     119        1002 :     }
     120             : 
     121             :     /* \brief Constructor on the basis of two numbers. The denominator must not be 0.
     122             :      */
     123             :     probabilistic_data_expression(std::size_t enumerator, std::size_t denominator)
     124             :     {
     125             :       assert(denominator!=0);
     126             :       remove_common_factors(enumerator,denominator);
     127             :       *this = lps::probabilistic_data_expression(data::sort_real::creal(data::sort_int::int_(enumerator),data::sort_pos::pos(denominator)));
     128             :     }
     129             : 
     130             :     /* \brief A constructor, where the enumerator and denominator are constructed
     131             :      *        from two strings of digits.
     132             :      */
     133             :     probabilistic_data_expression(const std::string& enumerator, const std::string& denominator)
     134             :     {
     135             :       assert(enumerator.size() <= denominator.size());
     136             :       const data_expression d_enumerator=data::sort_nat::nat(enumerator);
     137             :       const data_expression d_denominator=data::sort_pos::pos(denominator);
     138             :       *this = lps::probabilistic_data_expression(data::sort_real::creal(data::sort_int::cint(d_enumerator),d_denominator));
     139             :     }
     140             : 
     141             :     /* \brief Standard comparison operator.
     142             :     */
     143         723 :     bool operator==(const probabilistic_data_expression& other) const
     144             :     {
     145         723 :       const data_expression result= m_rewriter()(data::equal_to(*this,other));
     146         723 :       if (result==data::sort_bool::true_())
     147             :       {
     148         386 :         return true;
     149             :       }
     150         337 :       if (result==data::sort_bool::false_())
     151             :       {
     152         337 :         return false;
     153             :       }
     154           0 :       throw mcrl2::runtime_error("Equality between fractions does not rewrite to true or false: " + pp(result) + ".");
     155         723 :     }
     156             : 
     157             :     /* \brief Standard comparison operator.
     158             :     */
     159         337 :     bool operator!=(const probabilistic_data_expression& other) const
     160             :     {
     161         337 :       return !this->operator==(other);
     162             :     }
     163             : 
     164             :     /* \brief Standard comparison operator.
     165             :     */
     166        1544 :     bool operator<(const probabilistic_data_expression& other) const
     167             :     {
     168        1544 :       const data_expression result= m_rewriter()(data::less(*this,other));
     169        1544 :       if (result==data::sort_bool::true_())
     170             :       {
     171         772 :         return true;
     172             :       }
     173         772 :       if (result==data::sort_bool::false_())
     174             :       {
     175         772 :         return false;
     176             :       }
     177           0 :       throw mcrl2::runtime_error("Comparison of fraction does not rewrite to true or false: " + pp(result) + ".");
     178        1544 :     } 
     179             : 
     180             :     /* \brief Standard comparison operator.
     181             :     */
     182         772 :     bool operator<=(const probabilistic_data_expression& other) const
     183             :     {
     184         772 :       return !this->operator>(other);
     185             :     } 
     186             : 
     187             :     /* \brief Standard comparison operator.
     188             :     */
     189        1544 :     bool operator>(const probabilistic_data_expression& other) const
     190             :     {
     191        1544 :       return other.operator<(*this);
     192             :     } 
     193             : 
     194             :     /* \brief Standard comparison operator.
     195             :     */
     196             :     bool operator>=(const probabilistic_data_expression& other) const
     197             :     {
     198             :       return other.operator<=(*this);
     199             :     } 
     200             : 
     201             :     /** \brief Standard addition operator. Note that the expression is not evaluated.
     202             :      *        For this the rewriter has to be applied on it explicitly.
     203             :      */
     204         772 :     probabilistic_data_expression operator+(const probabilistic_data_expression& other) const
     205             :     {
     206        1544 :       return probabilistic_data_expression(m_rewriter()(data::sort_real::plus(*this,other)));
     207             :     } 
     208             : 
     209             : 
     210             :     /** \brief Standard subtraction operator.
     211             :      */
     212             :     probabilistic_data_expression operator-(const probabilistic_data_expression& other) const
     213             :     {
     214             :       return probabilistic_data_expression(m_rewriter()(data::sort_real::minus(*this,other)));
     215             :     } 
     216             : };
     217             : 
     218             : /* \brief A pretty print operator on action labels, returning it as a string.
     219             : */
     220             : inline std::string pp(const probabilistic_data_expression& l)
     221             : {
     222             :   return pp(static_cast<data::data_expression>(l));
     223             : }
     224             : 
     225             : /** \brief Pretty print to an outstream 
     226             : */
     227             : inline
     228             : std::ostream& operator<<(std::ostream& out, const probabilistic_data_expression& x)
     229             : {
     230             :   return out << static_cast<data::data_expression>(x);
     231             : }
     232             : 
     233             : 
     234             : } // namespace lps
     235             : } // namespace mcrl2
     236             : 
     237             : namespace std
     238             : {
     239             : 
     240             : template <>
     241             : struct hash<mcrl2::lps::probabilistic_data_expression >
     242             : {
     243         140 :   std::size_t operator()(const mcrl2::lps::probabilistic_data_expression& p) const
     244             :   {
     245             :     hash<atermpp::aterm> aterm_hasher;
     246         140 :     return aterm_hasher(p);
     247             :   }
     248             : };
     249             : 
     250             : } // namespace std
     251             : 
     252             : #endif // MCRL2_LPS_PROBABILISTIC_DATA_EXPRESSION_H
     253             : 
     254             :