From e2378b4904d9ee67087592e0195d806914a0ea49 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 30 Apr 2013 00:01:35 +0200
Subject: [PATCH] Fix genltl --gh-r
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Reported by František Blahoudek.

* src/bin/genltl.cc (R_n): Really generate (GFp1 || FGp2), not
(GFp1 || GFp2).
* NEWS: Mention the bug.
* THANKS: Update.
---
 NEWS              | 4 +++-
 THANKS            | 1 +
 src/bin/genltl.cc | 6 +++---
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/NEWS b/NEWS
index bf1593d6d..b3e69866c 100644
--- a/NEWS
+++ b/NEWS
@@ -1,6 +1,8 @@
 New in spot 1.1a (not yet released):
 
-  Nothing yet.
+  Bug fixes:
+
+    - genltl --gh-r generated the wrong formulas due to a typo.
 
 New in spot 1.1 (2013-04-28):
 
diff --git a/THANKS b/THANKS
index 6cca9ada1..8c7623ffd 100644
--- a/THANKS
+++ b/THANKS
@@ -5,6 +5,7 @@ Akim Demaille
 Christian Dax
 Étienne Renault
 Felix Klaedtke
+František Blahoudek
 Gerard J. Holzmann
 Heikki Tauriainen
 Jean-Michel Couvreur
diff --git a/src/bin/genltl.cc b/src/bin/genltl.cc
index fd7b7c9fb..678f396a5 100644
--- a/src/bin/genltl.cc
+++ b/src/bin/genltl.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Développement de
-// l'Epita (LRDE).
+// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -429,7 +429,7 @@ R_n(std::string name, int n)
       p << name << i + 1;
       pi = env.require(p.str());
 
-      const formula* fg = G_(F_(pi->clone()));
+      const formula* fg = F_(G_(pi->clone()));
 
       const formula* f = Or_(gf, fg);