From e73ce85cfcb8f266802ff942427fd901441d7b73 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 23 Jan 2004 13:01:43 +0000
Subject: [PATCH] * src/tgbaalgos/ltl2tgba_fm.cc: Typos in comments.

---
 ChangeLog                    |  4 ++++
 src/tgbaalgos/ltl2tgba_fm.cc | 11 +++++++----
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 00062b622..6618bcc99 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,7 @@
+2004-01-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* src/tgbaalgos/ltl2tgba_fm.cc: Typos in comments.
+
 2004-01-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* configure.ac, NEWS: Bump version to 0.0o.
diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index 8bf9bede0..9109abfbf 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -40,8 +40,8 @@ namespace spot
   namespace
   {
 
-    // Helper dictionary.  We represent formula using a BDD to simplify
-    // them, and them translate the BDD back into formulae.
+    // Helper dictionary.  We represent formulae using BDDs to
+    // simplify them, and then translate BDDs back into formulae.
     //
     // The name of the variables are inspired from Couvreur's FM paper.
     //   "a" variables are promises (written "a" in the paper)
@@ -323,7 +323,7 @@ namespace spot
 	    {
 	      const formula* child = node->child();
 	      int x = dict_.register_next_variable(node);
-	      // GFy is pretty frequent and easy to optimize, to we
+	      // GFy is pretty frequent and easy to optimize, so we
 	      // want to detect it.
 	      const unop* Fy = dynamic_cast<const unop*>(child);
 	      if (Fy && Fy->op() == unop::F)
@@ -344,11 +344,13 @@ namespace spot
 	    }
 	  case unop::Not:
 	    {
+	      // r(!y) = !r(y)
 	      res_ = bdd_not(recurse(node->child()));
 	      return;
 	    }
 	  case unop::X:
 	    {
+	      // r(Xy) = Next[y]
 	      int x = dict_.register_next_variable(node->child());
 	      res_ = bdd_ithvar(x);
 	      return;
@@ -366,6 +368,7 @@ namespace spot
 
 	switch (node->op())
 	  {
+	    // r(f1 logical-op f2) = r(f1) logical-op r(f2)
 	  case binop::Xor:
 	    res_ = bdd_apply(f1, f2, bddop_xor);
 	    return;