From d7781bc4d642a1ef62239556f02109a2b24b4c47 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 14 Oct 2010 18:38:28 +0200
Subject: [PATCH] Simplify ![*0] as [+].

* src/ltlast/unop.cc: Simplify ![*0] as 1[+].
* src/ltlast/unop.hh: Document it.
---
 src/ltlast/unop.cc | 7 +++++++
 src/ltlast/unop.hh | 7 +++++++
 2 files changed, 14 insertions(+)

diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc
index a5d78c697..04a8d9a40 100644
--- a/src/ltlast/unop.cc
+++ b/src/ltlast/unop.cc
@@ -145,6 +145,11 @@ namespace spot
 	    // !0 = 1
 	    if (child == constant::false_instance())
 	      return constant::true_instance();
+	    // ![*0] = 1[+]
+	    if (child == constant::empty_word_instance())
+	      return bunop::instance(bunop::Star,
+				     constant::true_instance(), 1);
+
 	    unop* u = dynamic_cast<unop*>(child);
 	    if (u)
 	      {
@@ -155,6 +160,7 @@ namespace spot
 		    u->destroy();
 		    return c;
 		  }
+		// !Closure(Exp) = NegClosure(Exp)
 		if (u->op() == Closure)
 		  {
 		    formula* c = unop::instance(NegClosure,
@@ -162,6 +168,7 @@ namespace spot
 		    u->destroy();
 		    return c;
 		  }
+		// !NegClosure(Exp) = Closure(Exp)
 		if (u->op() == NegClosure)
 		  {
 		    formula* c = unop::instance(Closure,
diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh
index 153eb19cc..687ecf47b 100644
--- a/src/ltlast/unop.hh
+++ b/src/ltlast/unop.hh
@@ -29,6 +29,7 @@
 #include <map>
 #include <iosfwd>
 #include "refformula.hh"
+#include "bunop.hh"
 
 namespace spot
 {
@@ -65,6 +66,7 @@ namespace spot
       ///   - G([*0]) = 1
       ///   - !1 = 0
       ///   - !0 = 1
+      ///   - ![*0] = 1[+]     (read below)
       ///   - !!Exp = Exp
       ///   - !Closure(Exp) = NegClosure(Exp)
       ///   - !NegClosure(Exp) = Closure(Exp)
@@ -78,6 +80,11 @@ namespace spot
       /// This rewriting implies that it is not possible to build an
       /// LTL formula object that is SYNTACTICALLY equal to one of
       /// these left expressions.
+      ///
+      /// Note that the "![*0]" form cannot be read using the PSL
+      /// grammar.  Spot cannot read it either.  However some
+      /// BDD-based algorithm may need to negate any constant, so we
+      /// handle this one as well.
       static formula* instance(type op, formula* child);
 
       virtual void accept(visitor& v);