From 09e4ab74a1b93804849de8063fca0f95cee6e310 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 7 Jul 2021 17:20:33 +0200
Subject: [PATCH] twa_run: reduce now diagnoses rejecting runs

Part of #471.

* spot/twaalgos/emptiness.cc: Throw an exception if
the cycle is rejecting.
* spot/twaalgos/emptiness.hh: Document this behavior.
* tests/python/except.py: Test it.
---
 spot/twaalgos/emptiness.cc | 11 +++++++++--
 spot/twaalgos/emptiness.hh |  5 ++++-
 tests/python/except.py     | 13 +++++++++++++
 3 files changed, 26 insertions(+), 3 deletions(-)

diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc
index 5ca65224d..fd3319141 100644
--- a/spot/twaalgos/emptiness.cc
+++ b/spot/twaalgos/emptiness.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011-2019 Laboratoire de Recherche et
+// Copyright (C) 2009, 2011-2019, 2021 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -343,8 +343,14 @@ namespace spot
       state_set seen;
       const state_set* target;
     };
+
+    [[noreturn]] static void report_rejecting_cycle()
+    {
+      throw std::runtime_error("twa_run::reduce() expects an accepting cycle");
+    }
   }
 
+
   twa_run_ptr twa_run::reduce() const
   {
     ensure_non_empty_cycle("twa_run::reduce()");
@@ -368,7 +374,8 @@ namespace spot
     twa_run::steps::const_iterator seg = cycle.end();
     do
       {
-        assert(seg != cycle.begin());
+        if (SPOT_UNLIKELY(seg == cycle.begin()))
+          report_rejecting_cycle();
         --seg;
         seen_acc |= seg->acc;
       }
diff --git a/spot/twaalgos/emptiness.hh b/spot/twaalgos/emptiness.hh
index 78eb88477..47896a1d7 100644
--- a/spot/twaalgos/emptiness.hh
+++ b/spot/twaalgos/emptiness.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013-2018, 2020 Laboratoire de
+// Copyright (C) 2011, 2013-2018, 2020-2021 Laboratoire de
 // Recherche et Developpement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -419,6 +419,9 @@ namespace spot
     /// this fragment with fewer edges than in the original cycle.
     /// (This step works best in Fin-less automata.)  And then trying
     /// to find a shorter prefix leading to any state of the cycle.
+    ///
+    /// An <code>std::runtime_error</code> is thrown if the run
+    /// to reduce is not accepting.
     twa_run_ptr reduce() const;
 
     /// \brief Project an accepting run
diff --git a/tests/python/except.py b/tests/python/except.py
index fdd1cf64a..0cf6ad1fe 100644
--- a/tests/python/except.py
+++ b/tests/python/except.py
@@ -134,6 +134,19 @@ except RuntimeError as e:
 else:
     report_missing_exception()
 
+a = spot.translate('Fa')
+a = spot.to_generalized_rabin(a, False)
+r = a.accepting_run()
+r = r.reduce()
+assert r.cycle[0].acc == spot.mark_t([1])
+r.cycle[0].acc = spot.mark_t([0])
+try:
+    r.reduce();
+except RuntimeError as e:
+    assert "expects an accepting cycle" in str(e)
+else:
+    report_missing_exception()
+
 f = spot.formula('GF(a | Gb)')
 try:
     spot.gf_guarantee_to_ba(f, spot._bdd_dict)