From 413eab1d32e6734d79baf23d9d7a846175185dad Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 9 Dec 2016 21:37:15 +0100
Subject: [PATCH] ltlf: ensure alive holds initially

Reported by Shufang Zhu.

* spot/tl/ltlf.cc, spot/tl/ltlf.hh: Fix the transltion
and update the comments.
* tests/core/ltlfilt.test: Adjust test cases.
* NEWS: Mention the fix.
* THANKS: Add Shufang Zhu.
---
 NEWS                    |  3 +++
 THANKS                  |  1 +
 spot/tl/ltlf.cc         |  6 +++++-
 spot/tl/ltlf.hh         |  2 +-
 tests/core/ltlfilt.test | 42 ++++++++++++++++++++---------------------
 5 files changed, 31 insertions(+), 23 deletions(-)

diff --git a/NEWS b/NEWS
index b0bf094a8..8a5f5929e 100644
--- a/NEWS
+++ b/NEWS
@@ -28,6 +28,9 @@ New in spot 2.2.1.dev (Not yet released)
     spot/misc/mspool.hh, spot/twaalgos/emptiness_stats.hh) were not
     self-contained.
 
+  * ltlfilt --from-ltlf should ensure that "alive" holds initially in
+    order to reject empty traces.
+
 New in spot 2.2.1 (2016-11-21)
 
   Bug fix:
diff --git a/THANKS b/THANKS
index 99800934b..98d23b3d5 100644
--- a/THANKS
+++ b/THANKS
@@ -29,6 +29,7 @@ Nikos Gorogiannis
 Reuben Rowe
 Rüdiger Ehlers
 Silien Hong
+Shufang Zhu
 Sonali Dutta
 Tomáš Babiak
 Valentin Iovene
diff --git a/spot/tl/ltlf.cc b/spot/tl/ltlf.cc
index dcdcc68bd..74532eabb 100644
--- a/spot/tl/ltlf.cc
+++ b/spot/tl/ltlf.cc
@@ -37,6 +37,10 @@ namespace spot
           // the IJCAI'13 paper by De Giacomo & Vardi has a typo.
           //  t(a U b) should be equal to t(a) U t(b & alive).
           // This typo is fixed in the Memocode'14 paper by Dutta & Vardi.
+          //
+          // (However beware that the translation given in the
+          // Memocode'14 paper forgets to ensure that alive holds
+          // initially, as required in the IJCAI'13 paper.)
         case op::U:
           return formula::U(t(f[0]), formula::And({alive, t(f[1])}));
         case op::R:
@@ -60,7 +64,7 @@ namespace spot
     auto al = ((*alive == '!')
                ? formula::Not(formula::ap(alive + 1))
                : formula::ap(alive));
-    return formula::And({from_ltlf_aux(f, al),
+    return formula::And({from_ltlf_aux(f, al), al,
                          formula::U(al, formula::G(formula::Not(al)))});
   }
 }
diff --git a/spot/tl/ltlf.hh b/spot/tl/ltlf.hh
index 385ed1c12..4235590c6 100644
--- a/spot/tl/ltlf.hh
+++ b/spot/tl/ltlf.hh
@@ -35,7 +35,7 @@ namespace spot
   /// finite word.  The formula is rewritten to ensure that the
   /// eventualities occur during the "alive" portion.  For instance
   /// <code>a U b</code> becomes
-  /// <code>(a U (b & alive))&(alive U G!alive)</code>.
+  /// <code>alive&(a U (b & alive))&(alive U G!alive)</code>.
   ///
   /// The \a alive argument can be used to change the name of the
   /// atomic property used to introduce.  Additionally if \a alive is
diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test
index 0ccaa3a36..5c24e866b 100755
--- a/tests/core/ltlfilt.test
+++ b/tests/core/ltlfilt.test
@@ -182,30 +182,30 @@ EOF
 run 0 ltlfilt --ltl formulas > formulas2
 mv formulas2 formulas
 
-checkopt --ltl --from-ltlf <<EOF
-(G(!alive | F(a & alive)) | F(alive & G(!alive | b))) & (alive U G!alive)
-F(alive & (G(!alive | F(a & alive)) | G(!alive | b))) & (alive U G!alive)
-F(alive & ((!alive | b) W G(!alive | F(a & alive)))) & (alive U G!alive)
-(G(!alive | F(a & alive)) | G(!alive | b)) & (alive U G!alive)
-((!alive | b) W G(!alive | F(a & alive))) & (alive U G!alive)
-(a U (alive & F(alive & b))) & (alive U G!alive)
-G(!alive | (a & X(alive & b))) & (alive U G!alive)
-X(a & alive) & (alive U G!alive)
-F(a & alive & !X(a & alive) & X(alive & b)) & (alive U G!alive)
-a & (b | c) & (alive U G!alive)
+checkopt --ltl --from-ltlf=al <<EOF
+al & (G(!al | F(a & al)) | F(al & G(!al | b))) & (al U G!al)
+al & F(al & (G(!al | F(a & al)) | G(!al | b))) & (al U G!al)
+al & F(al & ((!al | b) W G(!al | F(a & al)))) & (al U G!al)
+al & (G(!al | F(a & al)) | G(!al | b)) & (al U G!al)
+al & ((!al | b) W G(!al | F(a & al))) & (al U G!al)
+al & (a U (al & F(al & b))) & (al U G!al)
+al & G(!al | (a & X(al & b))) & (al U G!al)
+al & X(a & al) & (al U G!al)
+al & F(a & al & !X(a & al) & X(al & b)) & (al U G!al)
+a & al & (b | c) & (al U G!al)
 EOF
 
 checkopt --ltl --from-ltlf='!dead' <<EOF
-(G(dead | F(a & !dead)) | F(!dead & G(b | dead))) & (!dead U Gdead)
-F(!dead & (G(dead | F(a & !dead)) | G(b | dead))) & (!dead U Gdead)
-F(!dead & ((b | dead) W G(dead | F(a & !dead)))) & (!dead U Gdead)
-(G(dead | F(a & !dead)) | G(b | dead)) & (!dead U Gdead)
-((b | dead) W G(dead | F(a & !dead))) & (!dead U Gdead)
-(a U (!dead & F(b & !dead))) & (!dead U Gdead)
-G(dead | (a & X(b & !dead))) & (!dead U Gdead)
-X(a & !dead) & (!dead U Gdead)
-F(a & !dead & !X(a & !dead) & X(b & !dead)) & (!dead U Gdead)
-a & (b | c) & (!dead U Gdead)
+!dead & (G(dead | F(a & !dead)) | F(!dead & G(b | dead))) & (!dead U Gdead)
+!dead & F(!dead & (G(dead | F(a & !dead)) | G(b | dead))) & (!dead U Gdead)
+!dead & F(!dead & ((b | dead) W G(dead | F(a & !dead)))) & (!dead U Gdead)
+!dead & (G(dead | F(a & !dead)) | G(b | dead)) & (!dead U Gdead)
+!dead & ((b | dead) W G(dead | F(a & !dead))) & (!dead U Gdead)
+!dead & (a U (!dead & F(b & !dead))) & (!dead U Gdead)
+!dead & G(dead | (a & X(b & !dead))) & (!dead U Gdead)
+!dead & X(a & !dead) & (!dead U Gdead)
+!dead & F(a & !dead & !X(a & !dead) & X(b & !dead)) & (!dead U Gdead)
+a & !dead & (b | c) & (!dead U Gdead)
 EOF
 
 cat >in <<EOF