From 8ecf57e8321a9e218d3085fcc995a6963d524f43 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 23 May 2011 15:06:57 +0200
Subject: [PATCH] Generalize computation of is.eventual and is.universal.

* src/ltlast/binop.cc (binop::binop): Generalize detection
of pure eventualities and purely universal formulae.  E.g.
`f U g' is a pure eventuality if g is a pure eventuality
(regardless of f) or if g is 1.
* src/ltlast/unop.cc (unop::unop): Compute is.eventual
and is.universal for Not.
* src/ltltest/kind.test: Adjust.
---
 src/ltlast/binop.cc   | 43 ++++++++++++++++++++++++++-----------------
 src/ltlast/unop.cc    |  2 ++
 src/ltltest/kind.test |  2 +-
 3 files changed, 29 insertions(+), 18 deletions(-)

diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc
index f0547692e..04b87fd37 100644
--- a/src/ltlast/binop.cc
+++ b/src/ltlast/binop.cc
@@ -37,23 +37,30 @@ namespace spot
     binop::binop(type op, formula* first, formula* second)
       : ref_formula(BinOp), op_(op), first_(first), second_(second)
     {
-      // Beware: (f U g) is purely eventual if both operands
-      // are purely eventual, unlike in the proceedings of
+      // Beware: (f U g) is a pure eventuality if both operands
+      // are pure eventualities, unlike in the proceedings of
       // Concur'00.  (The revision of the paper available at
       // http://www.bell-labs.com/project/TMP/ is fixed.)  See
-      // also http://arxiv.org/abs/1011.4214 for a discussion
+      // also http://arxiv.org/abs/1011.4214v2 for a discussion
       // about this problem.  (Which we fixed in 2005 thanks
       // to LBTT.)
-
       // This means that we can use the following line to handle
       // all cases of (f U g), (f R g), (f W g), (f M g) for
       // universality and eventuality.
       props = first->get_props() & second->get_props();
-
+      // The matter can be further refined because:
+      //  (f U g) and (g M f) are pure eventualities if
+      //                         g is a pure eventuality (regardless of f)
+      //                      or f == 1
+      //  (f W g) and (g R f) are purely universal if
+      //                         f is purely universal (regardless of g)
+      //                      or g == 0
       switch (op)
 	{
 	case Xor:
 	case Equiv:
+	  is.eventual = false;
+	  is.universal = false;
 	  is.sere_formula = is.boolean;
 	  is.sugar_free_boolean = false;
 	  is.in_nenoform = false;
@@ -78,6 +85,8 @@ namespace spot
 	    }
 	  break;
 	case Implies:
+	  is.eventual = false;
+	  is.universal = false;
 	  is.sere_formula = is.boolean;
 	  is.sugar_free_boolean = false;
 	  is.in_nenoform = false;
@@ -148,9 +157,9 @@ namespace spot
 	  assert(second->is_psl_formula());
 	  break;
 	case U:
-	  // 1 U a = Fa
-	  if (first == constant::true_instance())
-	    is.eventual = 1;
+	  // f U g is universal if g is eventual, or if f == 1.
+	  is.eventual = second->is_eventual();
+	  is.eventual |= (first == constant::true_instance());
 	  is.boolean = false;
 	  is.eltl_formula = false;
 	  is.sere_formula = false;
@@ -168,9 +177,9 @@ namespace spot
 	  // is.syntactic_persistence = Persistence U Persistance
 	  break;
 	case W:
-	  // a W 0 = Ga
-	  if (second == constant::false_instance())
-	    is.universal = 1;
+	  // f W g is universal if f is universal, or if g == 0.
+	  is.universal = first->is_universal();
+	  is.universal |= (second == constant::false_instance());
 	  is.boolean = false;
 	  is.eltl_formula = false;
 	  is.sere_formula = false;
@@ -188,9 +197,9 @@ namespace spot
 
 	  break;
 	case R:
-	  // 0 R a = Ga
-	  if (first == constant::false_instance())
-	    is.universal = 1;
+	  // g R f is universal if f is universal, or if g == 0.
+	  is.universal = second->is_universal();
+	  is.universal |= (first == constant::false_instance());
 	  is.boolean = false;
 	  is.eltl_formula = false;
 	  is.sere_formula = false;
@@ -208,9 +217,9 @@ namespace spot
 
 	  break;
 	case M:
-	  // a M 1 = Fa
-	  if (second == constant::true_instance())
-	    is.eventual = 1;
+	  // g M f is universal if g is eventual, or if f == 1.
+	  is.eventual = first->is_eventual();
+	  is.eventual |= (second == constant::true_instance());
 	  is.boolean = false;
 	  is.eltl_formula = false;
 	  is.sere_formula = false;
diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc
index 369c4d23a..cd203184a 100644
--- a/src/ltlast/unop.cc
+++ b/src/ltlast/unop.cc
@@ -39,6 +39,8 @@ namespace spot
       switch (op)
 	{
 	case Not:
+	  is.eventual = child->is_universal();
+	  is.universal = child->is_eventual();
 	  is.in_nenoform = (child->kind() == AtomicProp);
 	  is.sere_formula = is.boolean;
 
diff --git a/src/ltltest/kind.test b/src/ltltest/kind.test
index 8e7bb4ed3..c1e61d7ad 100755
--- a/src/ltltest/kind.test
+++ b/src/ltltest/kind.test
@@ -40,7 +40,7 @@ check '!(a|b)'    'B&xfLEPSFsgopr'
 check 'F(a)'      '&!xLPegopr'
 check 'G(a)'      '&!xLPusopr'
 check 'a U b'     '&!xfLPgopr'
-check 'a U Fb'    '&!xLPgopr'
+check 'a U Fb'    '&!xLPegopr'
 check 'Ga U b'    '&!xLPopr'
 check '1 U a'     '&!xfLPegopr'
 check 'a W b'     '&!xfLPsopr'