From 913e807d66843c657c6d1b1066dfa3c9922e350a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 16 May 2024 12:17:17 +0200
Subject: [PATCH] stats: fix rounding issues

Fixes #582.

* spot/twaalgos/stats.cc: Add 0.5 to the result of bdd_satcountset()
before truncating it.
* NEWS: Mention the bug.
---
 NEWS                   |  3 +++
 spot/twaalgos/stats.cc | 15 ++++++++++++---
 2 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/NEWS b/NEWS
index 33a40d185..48ebbdb15 100644
--- a/NEWS
+++ b/NEWS
@@ -325,6 +325,9 @@ New in spot 2.11.6.dev  (not yet released)
   - The configure script failed to detect the include path for Python 3.12.
     (Issue #577.)
 
+  - Work around many failures caused by incorrect rounding of floating
+    point values in the counting of transitions.  (Issue #582)
+
   - Some incorrectly escaped strings in Python code were causing
     warnings with Python 3.12.
 
diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc
index 4b3b6185c..c8f45f634 100644
--- a/spot/twaalgos/stats.cc
+++ b/spot/twaalgos/stats.cc
@@ -35,7 +35,10 @@ namespace spot
     unsigned long long tr = 0;
     bdd v = g->ap_vars();
     for (auto& e: g->edges())
-      tr += bdd_satcountset(e.cond, v);
+      // We add 0.5 to work around rounding errors in the computation
+      // of bdd_satcountset(), as the conversion is done by
+      // truncation.  See issue #582.
+      tr += 0.5 + bdd_satcountset(e.cond, v);
     return tr;
   }
 
@@ -79,7 +82,10 @@ namespace spot
                    const twa_succ_iterator* it) override
       {
         ++s_.edges;
-        s_.transitions += bdd_satcountset(it->cond(), apvars_);
+        // We add 0.5 to work around rounding errors in the
+        // computation of bdd_satcountset(), as the conversion is done
+        // by truncation.  See issue #582.
+        s_.transitions += 0.5 + bdd_satcountset(it->cond(), apvars_);
       }
 
     private:
@@ -182,7 +188,10 @@ namespace spot
             [&s, &ge](bdd cond)
             {
               ++s.edges;
-              s.transitions += bdd_satcountset(cond, ge->ap_vars());
+              // We add 0.5 to work around rounding errors in the
+              // computation of bdd_satcountset(), as the conversion
+              // is done by truncation.  See issue #582.
+              s.transitions += 0.5 + bdd_satcountset(cond, ge->ap_vars());
             });
       }
     return s;