From 34f9fb5d68d0f6f714017b2aec76d79454ee7316 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 12 Oct 2018 13:38:30 +0200
Subject: [PATCH] option --low should disable gf-guarantee

Fixes #367.

* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Fix it.
* NEWS: Mention the change.
* tests/core/ltl2tgba2.test: Test this.
---
 NEWS                       | 3 +++
 spot/twaalgos/translate.cc | 8 ++++++--
 spot/twaalgos/translate.hh | 5 ++++-
 tests/core/ltl2tgba2.test  | 6 ++++++
 4 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/NEWS b/NEWS
index 7f33fbfa1..3db0ef002 100644
--- a/NEWS
+++ b/NEWS
@@ -7,6 +7,9 @@ New in spot 2.6.2.dev (not yet released)
     This in turn caused "ltl2tgba -U -B" to not produce unambiguous
     automata.
 
+  - ltl2tgba --low now disables the "gf-guarantee" feature, as
+    documented.
+
 New in spot 2.6.2 (2018-09-28)
 
   Build:
diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc
index a3c2a160c..baaa53e5f 100644
--- a/spot/twaalgos/translate.cc
+++ b/spot/twaalgos/translate.cc
@@ -36,7 +36,6 @@ namespace spot
   {
     comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0;
     relabel_bool_ = tls_impl_ = -1;
-    gf_guarantee_ = level_ != Low;
     ltl_split_ = true;
 
     opt_ = opt;
@@ -52,7 +51,12 @@ namespace spot
         skel_simul_ = opt->get("skel-simul", 1);
       }
     tls_impl_ = opt->get("tls-impl", -1);
-    gf_guarantee_ = opt->get("gf-guarantee", gf_guarantee_);
+    int gfg = opt->get("gf-guarantee", -1);
+    if (gfg >= 0)
+      {
+        gf_guarantee_ = !!gfg;
+        gf_guarantee_set_ = true;
+      }
     ltl_split_ = opt->get("ltl-split", 1);
   }
 
diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh
index 7e4aadf9a..db65348dd 100644
--- a/spot/twaalgos/translate.hh
+++ b/spot/twaalgos/translate.hh
@@ -119,6 +119,8 @@ namespace spot
           delete simpl_owned_;
           build_simplifier(d);
         }
+      if (!gf_guarantee_set_)
+        gf_guarantee_ = level != Low;
     }
 
     /// \brief Convert \a f into an automaton.
@@ -149,7 +151,8 @@ namespace spot
     int skel_simul_;
     int relabel_bool_;
     int tls_impl_;
-    bool gf_guarantee_;
+    bool gf_guarantee_ = true;
+    bool gf_guarantee_set_ = false;
     bool ltl_split_;
     const option_map* opt_;
   };
diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test
index 588e7b57e..a01e37c8e 100755
--- a/tests/core/ltl2tgba2.test
+++ b/tests/core/ltl2tgba2.test
@@ -381,6 +381,12 @@ ltl2tgba -Fformulas/1 --stats='%f, %s,%t' |
 
 diff formulas output
 
+# Issue #367.
+test 4 = `ltl2tgba 'GF(a<->XXa)' --stats=%s`
+test 9 = `ltl2tgba --low 'GF(a<->XXa)' --stats=%s`
+test 9 = `ltl2tgba -x gf-guarantee=0 'GF(a<->XXa)' --stats=%s`
+test 4 = `ltl2tgba --low -x gf-guarantee=1 'GF(a<->XXa)' --stats=%s`
+
 # Regression test for issue #357.  The second formula used to
 # incorrectly produce 13 edges when translated after the first one
 # because the transition were explored in a different order.