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