From b1c820af4db9035d21a488a6aec9c39dcde49a97 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 19 Apr 2007 12:10:22 +0000
Subject: [PATCH] * src/ltlvisit/contain.cc (reduce_tau03_visitor): Simplify
 the rules for "a U b" and "a R b", an implication check is enough.

---
 ChangeLog               |  5 +++++
 src/ltlvisit/contain.cc | 10 +++++-----
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index aad49b222..aa04d637c 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,8 @@
+2007-04-19  Alexandre Duret-Lutz  <adl@gnu.org>
+
+	* src/ltlvisit/contain.cc (reduce_tau03_visitor): Simplify the
+	rules for "a U b" and "a R b", an implication check is enough.
+
 2007-04-17  Alexandre Duret-Lutz  <adl@gnu.org>
 
 	* src/misc/bddalloc.cc (bdd_allocator::initialize): Call
diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc
index 7b2694ee8..afa772fc7 100644
--- a/src/ltlvisit/contain.cc
+++ b/src/ltlvisit/contain.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -181,8 +181,8 @@ namespace spot
 	  switch (bo->op())
 	    {
 	    case binop::U:
-	      // if (a U b) = b, then keep b !
-	      if (stronger && lcc->equal(bo, b))
+	      // if (a U b) => b, then keep b !
+	      if (stronger && lcc->contained(bo, b))
 		{
 		  destroy(a);
 		  result_ = b;
@@ -205,8 +205,8 @@ namespace spot
 		}
 	      break;
 	    case binop::R:
-	      // if (a R b) = b, then keep b !
-	      if (stronger && lcc->equal(bo, b))
+	      // if (a R b) => b, then keep b !
+	      if (stronger && lcc->contained(b, bo))
 		{
 		  destroy(a);
 		  result_ = b;