From 997f7ec7fbd064182f7af6860b9099e5696dc9cf Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 14 Nov 2023 15:40:24 +0100
Subject: [PATCH] gfguarantee: fix handling of true/false languages

Fixes #546 (again).

* spot/twaalgos/gfguarantee.cc (g_f_terminal_inplace): Detect
true/false languages early, so that we do not tag them as
non-inherently-weak.
* tests/core/ltlcross.test: Improve test case.
---
 spot/twaalgos/gfguarantee.cc | 13 ++++++++++++-
 tests/core/ltlcross.test     |  4 +++-
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/spot/twaalgos/gfguarantee.cc b/spot/twaalgos/gfguarantee.cc
index f0aa58274..f25c378c4 100644
--- a/spot/twaalgos/gfguarantee.cc
+++ b/spot/twaalgos/gfguarantee.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2018, 2021 Laboratoire de Recherche et Développement
+// Copyright (C) 2018, 2021, 2023 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -61,6 +61,11 @@ namespace spot
       if (!is_terminal_automaton(aut, &si, true))
         throw std::runtime_error("g_f_terminal() expects a terminal automaton");
 
+      // If a terminal automaton has only one SCC, it is either
+      // universal or empty.   In both cases G(automaton)=automaton.
+      if (si.scc_count() == 1)
+        return aut;
+
       unsigned ns = si.scc_count();
       std::vector<bool> term(ns, false);
       for (unsigned n = 0; n < ns; ++n)
@@ -69,6 +74,9 @@ namespace spot
 
       aut->prop_keep({ false, false, true, false, true, true });
       aut->prop_state_acc(state_based);
+      // The case where the input automaton is universal or empty has
+      // already been dealt with, before do_g_f_terminal_inplace was
+      // called.
       aut->prop_inherently_weak(false);
       aut->set_buchi();
 
@@ -477,8 +485,11 @@ namespace spot
       }
     twa_graph_ptr aut = ltl_to_tgba_fm(f, dict, true);
     twa_graph_ptr reduced = minimize_obligation(aut, f);
+
+    // If f was not an obligation, we cannot deal with it here.
     if (reduced == aut)
       return nullptr;
+
     scc_info si(reduced);
     if (!is_terminal_automaton(reduced, &si, true))
       return nullptr;
diff --git a/tests/core/ltlcross.test b/tests/core/ltlcross.test
index faa386cb9..381cf7a66 100755
--- a/tests/core/ltlcross.test
+++ b/tests/core/ltlcross.test
@@ -70,4 +70,6 @@ ltlcross --verbose ltl2tgba ltl2tgba \
 ltlcross ltl2tgba -f '!(X(v3 | G!v5) | ((Xv5 & !(v5 & !X!v3)) U !v5))'
 
 # Issue #546.
-ltlcross 'ltl2tgba --medium -p' 'ltl2tgba -p' -f 'a | FGa | GF(!b | Gb)'
+ltlcross 'ltl2tgba --medium -p' 'ltl2tgba -p' 'ltl2tgba --medium -D -p' \
+         -f 'a | FGa | GF(!b | Gb)' \
+         -f '(~ v1 U ~ v5) | G(F v9 & F G v1) | G F(~ v7 | G v7 | G v3)'