mCRL2
Loading...
Searching...
No Matches
probabilistic_arbitrary_precision_fraction.h
Go to the documentation of this file.
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
20#ifndef MCRL2_UTILITIES_PROBABILISTIC_ARBITRARY_PRECISION_FRACTION_H
21#define MCRL2_UTILITIES_PROBABILISTIC_ARBITRARY_PRECISION_FRACTION_H
22
24
25
26namespace mcrl2
27{
28namespace utilities
29{
30
35{
36 protected:
39
40 // The three buffers below are used to avoid continuous redeclaring of big_natural_numbers, which is extremely time
41 // consuming.
43 {
44 thread_local utilities::big_natural_number buffer;
45 return buffer;
46 }
47
49 {
50 thread_local utilities::big_natural_number buffer;
51 return buffer;
52 }
53
55 {
56 thread_local utilities::big_natural_number buffer;
57 return buffer;
58 }
59
60 public:
61
64 {
66 return zero;
67 }
68
71 {
73 return one;
74 }
75
76 /* \brief Default constructor. The label will contain the default string.
77 */
79 : m_enumerator(),
81 {}
82
83 /* \brief A constructor, where the enumerator and denominator are constructed
84 * from two strings of digits.
85 */
89 {
90 assert(enumerator<= denominator);
91 }
92
93 /* \brief A constructor, where the enumerator and denominator are constructed
94 * from two strings of digits.
95 */
96 explicit probabilistic_arbitrary_precision_fraction(const std::string& enumerator, const std::string& denominator)
99 {
100 assert(m_enumerator<= m_denominator);
101 }
102
103 /* \brief Return the enumerator of the fraction.
104 */
106 {
107 return m_enumerator;
108 }
109
110 /* \brief Return the denominator of the label.
111 */
113 {
114 return m_denominator;
115 }
116
117 /* \brief Standard comparison operator.
118 */
120 {
121 // return this->m_enumerator*other.m_denominator==other.m_enumerator*this->m_denominator;
122 buffer1().clear();
123 this->m_enumerator.multiply(other.m_denominator, buffer1(), buffer3());
124 buffer2().clear();
125 other.m_enumerator.multiply(this->m_denominator, buffer2(), buffer3());
126 return buffer1()==buffer2();
127 }
128
129 /* \brief Standard comparison operator.
130 */
132 {
133 return !this->operator==(other);
134 }
135
136 /* \brief Standard comparison operator.
137 */
139 {
140 // return this->m_enumerator*other.m_denominator<other.m_enumerator*this->m_denominator;
141 buffer1().clear();
142 this->m_enumerator.multiply(other.m_denominator, buffer1(), buffer3());
143 buffer2().clear();
144 other.m_enumerator.multiply(this->m_denominator, buffer2(), buffer3());
145 return buffer1()<buffer2();
146 }
147
148 /* \brief Standard comparison operator.
149 */
151 {
152 return !this->operator>(other);
153 }
154
155 /* \brief Standard comparison operator.
156 */
158 {
159 return other.operator<(*this);
160 }
161
162 /* \brief Standard comparison operator.
163 */
165 {
166 return other.operator<=(*this);
167 }
168
169 /* \brief Standard addition operator.
170 */
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 buffer1().clear();
181 buffer2().clear();
183 buffer1().add(buffer2());
184 buffer2().clear();
188 }
189
190 /* \brief Standard subtraction operator.
191 */
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 buffer1().clear();
202 buffer2().clear();
205 buffer2().clear();
209 }
210
211 /* \brief Standard multiplication operator.
212 */
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 buffer1().clear();
222 buffer2().clear();
226 }
227
228 /* \brief Standard division operator.
229 */
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 buffer1().clear();
240 buffer2().clear();
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.
251 utilities::big_natural_number& buffer_divide,
252 utilities::big_natural_number& buffer_remainder,
254 {
255 if (x.is_zero()) { x=y; return; }
256 if (y.is_zero()) { return; } // The answer is x.
257 if (x>y)
258 {
259 utilities::swap(x,y);
260 }
261 // utilities::big_natural_number remainder=y % x;
262 y.div_mod(x,buffer_divide,buffer_remainder,buffer); // buffer_remainder contains remainder.
263 while (!buffer_remainder.is_zero())
264 {
265 y=x;
266 x=buffer_remainder;
267 // remainder=y % x;
268 y.div_mod(x,buffer_divide,buffer_remainder,buffer);
269 }
270 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.
276 {
279 return x;
280 }
281
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 thread_local utilities::big_natural_number enumerator_copy, denominator_copy, gcd, buffer1, buffer2,buffer3;
290 gcd=enumerator;
291 enumerator_copy=enumerator;
292 denominator_copy=denominator;
294 enumerator_copy.div_mod(gcd,enumerator,buffer1,buffer2); // enumerator=enumerator/gcd
295 denominator_copy.div_mod(gcd,denominator,buffer1,buffer2); // denominator=denominator/gcd;
296 assert(greatest_common_divisor(enumerator,denominator).is_number(1));
297 }
298
299};
300
301/* \brief A pretty print operator on action labels, returning it as a string.
302*/
304{
305 std::stringstream s;
306 s << l.enumerator() << "/" << l.denominator();
307 return s.str();
308}
309
310inline
311std::ostream& operator<<(std::ostream& out, const probabilistic_arbitrary_precision_fraction& x)
312{
313 return out << pp(x);
314}
315
316} // namespace utilities
317} // namespace mcrl2
318
319namespace std
320{
321
323template <>
324struct hash< mcrl2::utilities::probabilistic_arbitrary_precision_fraction >
325{
327 {
328 hash<mcrl2::utilities::big_natural_number> hasher;
329 return mcrl2::utilities::detail::hash_combine(hasher(p.enumerator()), hasher(p.denominator()));
330 }
331};
332
333} // namespace std
334
335#endif // MCRL2_UTILITIES_PROBABILISTIC_ARBITRARY_PRECISION_FRACTION_H
336
337
This file contains a class big_natural_number that stores big positive numbers of arbitrary size....
void div_mod(const big_natural_number &other, big_natural_number &result, big_natural_number &remainder, big_natural_number &calculation_buffer_divisor) const
void add(const big_natural_number &other)
void clear()
Sets the number to zero.
bool is_zero() const
Returns whether this number equals zero.
void multiply(const big_natural_number &other, big_natural_number &result, big_natural_number &calculation_buffer_for_multiplicand) const
void subtract(const big_natural_number &other)
This class contains labels for probabilistic transistions, consisting of a numerator and a denominato...
probabilistic_arbitrary_precision_fraction operator*(const probabilistic_arbitrary_precision_fraction &other) const
static void greatest_common_divisor_destructive(utilities::big_natural_number &x, utilities::big_natural_number &y, utilities::big_natural_number &buffer_divide, utilities::big_natural_number &buffer_remainder, utilities::big_natural_number &buffer)
bool operator>=(const probabilistic_arbitrary_precision_fraction &other) const
static void remove_common_factors(utilities::big_natural_number &enumerator, utilities::big_natural_number &denominator)
bool operator!=(const probabilistic_arbitrary_precision_fraction &other) const
probabilistic_arbitrary_precision_fraction operator+(const probabilistic_arbitrary_precision_fraction &other) const
bool operator<(const probabilistic_arbitrary_precision_fraction &other) const
bool operator>(const probabilistic_arbitrary_precision_fraction &other) const
static probabilistic_arbitrary_precision_fraction & one()
Constant one.
static utilities::big_natural_number greatest_common_divisor(utilities::big_natural_number x, utilities::big_natural_number y)
probabilistic_arbitrary_precision_fraction operator-(const probabilistic_arbitrary_precision_fraction &other) const
static probabilistic_arbitrary_precision_fraction & zero()
Constant zero.
probabilistic_arbitrary_precision_fraction operator/(const probabilistic_arbitrary_precision_fraction &other) const
bool operator<=(const probabilistic_arbitrary_precision_fraction &other) const
probabilistic_arbitrary_precision_fraction(const std::string &enumerator, const std::string &denominator)
probabilistic_arbitrary_precision_fraction(const utilities::big_natural_number &enumerator, const utilities::big_natural_number &denominator)
bool operator==(const probabilistic_arbitrary_precision_fraction &other) const
std::size_t hash_combine(const std::size_t h1, const std::size_t h2)
void swap(big_natural_number &x, big_natural_number &y)
Standard overload of swap.
std::string pp(const big_natural_number &l)
std::ostream & operator<<(std::ostream &ss, const big_natural_number &l)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.
std::size_t operator()(const mcrl2::utilities::probabilistic_arbitrary_precision_fraction &p) const
#define hash(l, r, m)
Definition tree_set.cpp:23