LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts - probabilistic_arbitrary_precision_fraction.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 116 116 100.0 %
Date: 2019-09-14 00:54:39 Functions: 30 30 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             : 
      10             : /** \file
      11             :  *
      12             :  * \brief This file contains a class that contains labels for probabilistic transitions.
      13             :  *        These consist of a 64 bit enumerator and denominator. This library maintains
      14             :  *        precision as long as the enuemerator and denominator fit in 64 bits positive numbers.
      15             :  *        If they do not fit, rounding is applied.
      16             :  * \author Jan Friso Groote
      17             :  */
      18             : 
      19             : 
      20             : #ifndef MCRL2_LTS_PROBABILISTIC_ARBITRARY_PRECISION_FRACTION_H
      21             : #define MCRL2_LTS_PROBABILISTIC_ARBITRARY_PRECISION_FRACTION_H
      22             : 
      23             : #include <cstddef>
      24             : #include <string>
      25             : #include <cassert>
      26             : #include <sstream>
      27             : #include <limits>
      28             : #include "mcrl2/utilities/hash_utility.h"
      29             : #include "mcrl2/utilities/big_numbers.h"
      30             : 
      31             : 
      32             : namespace mcrl2
      33             : {
      34             : namespace lts
      35             : {
      36             : 
      37             : /** \brief This class contains labels for probabilistic transistions, consisting of a numerator and a denominator
      38             :  *         as a string of digits.
      39             :  */
      40      131019 : class probabilistic_arbitrary_precision_fraction
      41             : {
      42             :   protected:
      43             :     utilities::big_natural_number m_enumerator;
      44             :     utilities::big_natural_number m_denominator;
      45             : 
      46             :     // The three buffers below are used to avoid continuous redeclaring of big_natural_numbers, which is extremely time 
      47             :     // consuming. 
      48      277019 :     static utilities::big_natural_number& buffer1()
      49             :     {
      50      277019 :       static utilities::big_natural_number buffer;
      51      277019 :       return buffer;
      52             :     }
      53             : 
      54      315245 :     static utilities::big_natural_number& buffer2()
      55             :     {
      56      315245 :       static utilities::big_natural_number buffer;
      57      315245 :       return buffer;
      58             :     }
      59             : 
      60      178285 :     static utilities::big_natural_number& buffer3()
      61             :     {
      62      178285 :       static utilities::big_natural_number buffer;
      63      178285 :       return buffer;
      64             :     }
      65             : 
      66             :   public:
      67             : 
      68             :     /// \brief Constant zero.
      69       38914 :     static probabilistic_arbitrary_precision_fraction& zero()
      70             :     {
      71       38914 :       static probabilistic_arbitrary_precision_fraction zero(utilities::big_natural_number(0), utilities::big_natural_number(1));
      72       38914 :       return zero;
      73             :     }
      74             : 
      75             :     /// \brief Constant one.
      76       36182 :     static probabilistic_arbitrary_precision_fraction& one()
      77             :     {
      78       36182 :       static probabilistic_arbitrary_precision_fraction one(utilities::big_natural_number(1), utilities::big_natural_number(1));
      79       36182 :       return one;
      80             :     }                          
      81             : 
      82             :     /* \brief Default constructor. The label will contain the default string.
      83             :      */
      84        2032 :     probabilistic_arbitrary_precision_fraction()
      85             :      : m_enumerator(),
      86        2032 :        m_denominator(utilities::big_natural_number(1))
      87        2032 :     {}
      88             : 
      89             :     /* \brief A constructor, where the enumerator and denominator are constructed
      90             :      *        from two strings of digits.
      91             :      */
      92       19162 :     probabilistic_arbitrary_precision_fraction(const utilities::big_natural_number& enumerator, const utilities::big_natural_number& denominator)
      93             :      : m_enumerator(enumerator),
      94       19162 :        m_denominator(denominator)
      95             :     {
      96       19162 :       assert(enumerator<= denominator);
      97       19162 :     }
      98             : 
      99             :     /* \brief A constructor, where the enumerator and denominator are constructed
     100             :      *        from two strings of digits.
     101             :      */
     102        2684 :     explicit probabilistic_arbitrary_precision_fraction(const std::string& enumerator, const std::string& denominator)
     103             :      : m_enumerator(utilities::big_natural_number(enumerator)),
     104        2684 :        m_denominator(utilities::big_natural_number(denominator))
     105             :     {
     106        2684 :       assert(m_enumerator<= m_denominator);
     107        2684 :     }
     108             : 
     109             :     /* \brief Return the enumerator of the fraction.
     110             :     */
     111        1285 :     const utilities::big_natural_number& enumerator() const
     112             :     {
     113        1285 :       return m_enumerator;
     114             :     }
     115             : 
     116             :     /* \brief Return the denominator of the label.
     117             :     */
     118        1285 :     const utilities::big_natural_number& denominator() const
     119             :     {
     120        1285 :       return m_denominator;
     121             :     }
     122             : 
     123             :     /* \brief Standard comparison operator.
     124             :     */
     125       22254 :     bool operator==(const probabilistic_arbitrary_precision_fraction& other) const
     126             :     {
     127             :       // return this->m_enumerator*other.m_denominator==other.m_enumerator*this->m_denominator;
     128       22254 :       buffer1().clear();
     129       22254 :       this->m_enumerator.multiply(other.m_denominator, buffer1(), buffer3());
     130       22254 :       buffer2().clear();
     131       22254 :       other.m_enumerator.multiply(this->m_denominator, buffer2(), buffer3());
     132       22254 :       return buffer1()==buffer2();
     133             :     }
     134             : 
     135             :     /* \brief Standard comparison operator.
     136             :     */
     137        6369 :     bool operator!=(const probabilistic_arbitrary_precision_fraction& other) const
     138             :     {
     139        6369 :       return !this->operator==(other);
     140             :     }
     141             : 
     142             :     /* \brief Standard comparison operator.
     143             :     */
     144       38184 :     bool operator<(const probabilistic_arbitrary_precision_fraction& other) const
     145             :     {
     146             :       // return this->m_enumerator*other.m_denominator<other.m_enumerator*this->m_denominator;
     147       38184 :       buffer1().clear();
     148       38184 :       this->m_enumerator.multiply(other.m_denominator, buffer1(), buffer3());
     149       38184 :       buffer2().clear();
     150       38184 :       other.m_enumerator.multiply(this->m_denominator, buffer2(), buffer3());
     151       38184 :       return buffer1()<buffer2();
     152             :     }
     153             : 
     154             :     /* \brief Standard comparison operator.
     155             :     */
     156       17778 :     bool operator<=(const probabilistic_arbitrary_precision_fraction& other) const
     157             :     {
     158       17778 :       return !this->operator>(other);
     159             :     }
     160             : 
     161             :     /* \brief Standard comparison operator.
     162             :     */
     163       35564 :     bool operator>(const probabilistic_arbitrary_precision_fraction& other) const
     164             :     {
     165       35564 :       return other.operator<(*this);
     166             :     }
     167             : 
     168             :     /* \brief Standard comparison operator.
     169             :     */
     170             :     bool operator>=(const probabilistic_arbitrary_precision_fraction& other) const
     171             :     {
     172             :       return other.operator<=(*this);
     173             :     }
     174             : 
     175             :     /* \brief Standard addition operator.
     176             :      */
     177       18284 :     probabilistic_arbitrary_precision_fraction operator+(const probabilistic_arbitrary_precision_fraction& other) const
     178             :     {
     179             :       /* utilities::big_natural_number enumerator=this->enumerator()*other.denominator() +
     180             :                                                other.enumerator()*this->denominator();
     181             :       utilities::big_natural_number denominator=this->denominator()*other.denominator();
     182             :       remove_common_factors(enumerator,denominator);
     183             :       return probabilistic_arbitrary_precision_fraction(enumerator,denominator); */
     184             : 
     185       18284 :       buffer1().clear();
     186       18284 :       m_enumerator.multiply(other.m_denominator, buffer1(), buffer3());
     187       18284 :       buffer2().clear();
     188       18284 :       other.m_enumerator.multiply(m_denominator, buffer2(), buffer3());
     189       18284 :       buffer1().add(buffer2());
     190       18284 :       buffer2().clear();
     191       18284 :       m_denominator.multiply(other.m_denominator,buffer2(),buffer3());
     192       18284 :       remove_common_factors(buffer1(),buffer2());
     193       18284 :       return probabilistic_arbitrary_precision_fraction(buffer1(),buffer2()); 
     194             :     }
     195             : 
     196             :     /* \brief Standard subtraction operator.
     197             :      */
     198         829 :     probabilistic_arbitrary_precision_fraction operator-(const probabilistic_arbitrary_precision_fraction& other) const
     199             :     {
     200             :       /* utilities::big_natural_number enumerator= this->enumerator()*other.denominator() -
     201             :                                     other.enumerator()*this->denominator();
     202             :       utilities::big_natural_number denominator=this->denominator()*other.denominator();
     203             :       remove_common_factors(enumerator,denominator);
     204             :       return probabilistic_arbitrary_precision_fraction(enumerator,denominator); */
     205             : 
     206         829 :       buffer1().clear();
     207         829 :       m_enumerator.multiply(other.m_denominator, buffer1(), buffer3());
     208         829 :       buffer2().clear();
     209         829 :       other.m_enumerator.multiply(m_denominator, buffer2(), buffer3());
     210         829 :       buffer1().subtract(buffer2());
     211         829 :       buffer2().clear();
     212         829 :       m_denominator.multiply(other.m_denominator,buffer2(),buffer3());
     213         829 :       remove_common_factors(buffer1(),buffer2());
     214         829 :       return probabilistic_arbitrary_precision_fraction(buffer1(),buffer2()); 
     215             :     }
     216             : 
     217             :     /* \brief Standard multiplication operator.
     218             :      */
     219          28 :     probabilistic_arbitrary_precision_fraction operator*(const probabilistic_arbitrary_precision_fraction& other) const
     220             :     {
     221             :       /* utilities::big_natural_number enumerator= this->enumerator()*other.enumerator();
     222             :       utilities::big_natural_number denominator=this->denominator()*other.denominator();
     223             :       remove_common_factors(enumerator,denominator);
     224             :       return probabilistic_arbitrary_precision_fraction(enumerator,denominator); */
     225             : 
     226          28 :       buffer1().clear();
     227          28 :       m_enumerator.multiply(other.m_enumerator, buffer1(), buffer3());
     228          28 :       buffer2().clear();
     229          28 :       m_denominator.multiply(other.m_denominator,buffer2(),buffer3());
     230          28 :       remove_common_factors(buffer1(),buffer2());
     231          28 :       return probabilistic_arbitrary_precision_fraction(buffer1(),buffer2()); 
     232             :     }
     233             : 
     234             :     /* \brief Standard division operator.
     235             :      */
     236           7 :     probabilistic_arbitrary_precision_fraction operator/(const probabilistic_arbitrary_precision_fraction& other) const
     237             :     {
     238             :       /* assert(other>probabilistic_arbitrary_precision_fraction::zero());
     239             :       utilities::big_natural_number enumerator= this->enumerator()*other.denominator();
     240             :       utilities::big_natural_number denominator=this->denominator()*other.enumerator();
     241             :       remove_common_factors(enumerator,denominator);
     242             :       return probabilistic_arbitrary_precision_fraction(enumerator,denominator); */
     243             : 
     244           7 :       buffer1().clear();
     245           7 :       m_enumerator.multiply(other.m_denominator, buffer1(), buffer3());
     246           7 :       buffer2().clear();
     247           7 :       m_denominator.multiply(other.m_enumerator,buffer2(),buffer3());
     248           7 :       remove_common_factors(buffer1(),buffer2());
     249           7 :       return probabilistic_arbitrary_precision_fraction(buffer1(),buffer2()); 
     250             :     }
     251             : 
     252             :     // An algorithm to calculate the greatest common divisor, which destroys its arguments.
     253             :     // The result is passed back in x. y has no sensible value at the end. 
     254       38328 :     static void greatest_common_divisor_destructive(
     255             :                                                utilities::big_natural_number& x, 
     256             :                                                utilities::big_natural_number& y,
     257             :                                                utilities::big_natural_number& buffer_divide,
     258             :                                                utilities::big_natural_number& buffer_remainder,
     259             :                                                utilities::big_natural_number& buffer)
     260             :     {
     261       38328 :       if (x.is_zero()) { x=y; return; }
     262       38310 :       if (y.is_zero()) { return; } // The answer is x. 
     263       38310 :       if (x>y)
     264             :       {
     265          15 :         utilities::swap(x,y);
     266             :       }
     267             :       // utilities::big_natural_number remainder=y % x;
     268       38310 :       y.div_mod(x,buffer_divide,buffer_remainder,buffer);  // buffer_remainder contains remainder.
     269       66010 :       while (!buffer_remainder.is_zero())
     270             :       {
     271       13850 :         y=x;
     272       13850 :         x=buffer_remainder;
     273             :         // remainder=y % x;
     274       13850 :         y.div_mod(x,buffer_divide,buffer_remainder,buffer);
     275             :       }
     276       38310 :       return;  // the value x is now the result.
     277             :     }
     278             : 
     279             :     // \detail An algorithm to calculate the greatest common divisor.
     280             :     // The arguments are intentionally passed by value. That means this routine is not very efficient as it copies two vectors.
     281       19180 :     static utilities::big_natural_number greatest_common_divisor(utilities::big_natural_number x, utilities::big_natural_number y)
     282             :     {
     283       19180 :       static utilities::big_natural_number buffer1, buffer2, buffer3;
     284       19180 :       greatest_common_divisor_destructive(x,y,buffer1,buffer2,buffer3);
     285       19180 :       return x;
     286             :     } 
     287             : 
     288       19148 :     static void remove_common_factors(utilities::big_natural_number& enumerator, utilities::big_natural_number& denominator)
     289             :     {
     290             :       /* const utilities::big_natural_number gcd=greatest_common_divisor(enumerator,denominator);
     291             :       enumerator=enumerator/gcd;
     292             :       denominator=denominator/gcd;
     293             :       assert(greatest_common_divisor(enumerator,denominator).is_number(1)); */
     294             : 
     295       19148 :       static utilities::big_natural_number enumerator_copy, denominator_copy, gcd, buffer1, buffer2,buffer3;
     296       19148 :       gcd=enumerator;
     297       19148 :       enumerator_copy=enumerator;
     298       19148 :       denominator_copy=denominator;
     299       19148 :       greatest_common_divisor_destructive(gcd,denominator,buffer1,buffer2,buffer3);
     300       19148 :       enumerator_copy.div_mod(gcd,enumerator,buffer1,buffer2);   // enumerator=enumerator/gcd
     301       19148 :       denominator_copy.div_mod(gcd,denominator,buffer1,buffer2); // denominator=denominator/gcd;
     302       19148 :       assert(greatest_common_divisor(enumerator,denominator).is_number(1));
     303       19148 :     }
     304             :     
     305             : };
     306             : 
     307             : /* \brief A pretty print operator on action labels, returning it as a string.
     308             : */
     309         126 : inline std::string pp(const probabilistic_arbitrary_precision_fraction& l)
     310             : {
     311         252 :   std::stringstream s;
     312         126 :   s << l.enumerator() << "/" << l.denominator();
     313         252 :   return s.str();
     314             : }
     315             : 
     316             : inline
     317         126 : std::ostream& operator<<(std::ostream& out, const probabilistic_arbitrary_precision_fraction& x)
     318             : {
     319         126 :   return out << pp(x);
     320             : }
     321             : 
     322             : } // namespace lts
     323             : } // namespace mcrl2
     324             : 
     325             : namespace std
     326             : {
     327             : 
     328             : /// \brief specialization of the standard std::hash function.
     329             : template <>
     330             : struct hash< mcrl2::lts::probabilistic_arbitrary_precision_fraction >
     331             : {
     332        1159 :   std::size_t operator()(const mcrl2::lts::probabilistic_arbitrary_precision_fraction& p) const
     333             :   {
     334             :     hash<mcrl2::utilities::big_natural_number> hasher;
     335        1159 :     return mcrl2::utilities::detail::hash_combine(hasher(p.enumerator()), hasher(p.denominator()));
     336             :   }
     337             : };
     338             : 
     339             : } // namespace std
     340             : 
     341             : #endif // MCRL2_LTS_PROBABILISTIC_ARBITRARY_PRECISION_FRACTION_H
     342             : 
     343             : 

Generated by: LCOV version 1.12