Merged requested to merge double-round into master
(a-b < ɛ) is not transitive and thus doesn't induce
an equality relation. Since the whole job of the algorithm is to
partition according to an equality relation, this may be problematic.
Instead, to compare doubles a and b, we now round both values to floats and compare those exactly. This means that we get a proper equality relation, even if it fails to distinguish some states and wrongly distinguishes others when compared to operations on true real numbers.