From f68f639e68e8485685791dbbebcac0aafb5f3e6f Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 13 Nov 2011 18:12:53 +0100
Subject: [PATCH] Rewrite {b}<>->f as (!b)|f instead of b->f.

* src/ltlast/binop.cc, src/ltlast/binop.hh: Here.
* doc/tl/tl.tex, src/ltltest/equals.test: Adjust.
---
 doc/tl/tl.tex           | 2 +-
 src/ltlast/binop.cc     | 5 +++--
 src/ltlast/binop.hh     | 2 +-
 src/ltltest/equals.test | 6 +++---
 4 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 6f5d778be..ed6cc45c2 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -842,7 +842,7 @@ formula $b$, the following rewritings are systematically performed
 & \ratgroup{\eword}\Esuffix f&\equiv \0
 & \ratgroup{\eword} & \equiv \0
 & \nratgroup{\eword} & \equiv \1 \\
-  \ratgroup{b}\Asuffix f&\equiv b\IMPLIES f
+  \ratgroup{b}\Asuffix f&\equiv (\NOT{b})\OR f
 & \ratgroup{b}\Esuffix f&\equiv b\AND f
 & \ratgroup{b} &\equiv b
 & \nratgroup{b} &\equiv \NOT b\\
diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc
index 0fa9fbf23..3f08ccd61 100644
--- a/src/ltlast/binop.cc
+++ b/src/ltlast/binop.cc
@@ -520,7 +520,7 @@ namespace spot
 	  //   - 1 []-> Exp = Exp
 	  //   - [*0] []-> Exp = 1
 	  //   - Exp []-> 1 = 1
-	  //   - boolExp []-> Exp = boolExp -> Exp
+	  //   - boolExp []-> Exp = !boolExp | Exp
 	  if (first == constant::true_instance())
 	    return second;
 	  if (first == constant::false_instance()
@@ -535,7 +535,8 @@ namespace spot
 	      return second;
 	    }
 	  if (first->is_boolean())
-	    return binop::instance(binop::Implies, first, second);
+	    return multop::instance(multop::Or,
+				    unop::instance(unop::Not, first), second);
 	  break;
 	}
 
diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh
index 9b340cf9b..7b7b80d74 100644
--- a/src/ltlast/binop.hh
+++ b/src/ltlast/binop.hh
@@ -105,7 +105,7 @@ namespace spot
       ///   - 1 []-> Exp = Exp
       ///   - [*0] []-> Exp = 1
       ///   - Exp []-> 1 = 1
-      ///   - boolExp <>-> Exp = boolExp -> Exp
+      ///   - boolExp <>-> Exp = !boolExp | Exp
       static formula* instance(type op, formula* first, formula* second);
 
       virtual void accept(visitor& v);
diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test
index 13f21d1e6..b6b3c2c6a 100755
--- a/src/ltltest/equals.test
+++ b/src/ltltest/equals.test
@@ -141,11 +141,11 @@ run 0 ../equals '{x;x}[]->FF(0)' '{x;x}[]->0'
 run 0 ../equals '{x;x}[]->y' '{x;x}|->y'
 run 0 ../equals '{x;x}[]->y' '{x;x}(y)'
 run 0 ../equals '{a*}!' '{a*}<>->1'
-run 0 ../equals '{a -> b} (c)' '(a->b)->c'
+run 0 ../equals '{a -> b} (c)' '!(a->b)|c'
 run 0 ../equals '{a & !b}!' 'a & !b'
-run 0 ../equals '{a;[*0]}|->!Xb' 'a -> !Xb'
+run 0 ../equals '{a;[*0]}|->!Xb' '!a | !Xb'
 run 0 ../equals '{{a;b}:b:c:d*:e:f}!' '{{a;b}:{{b && c } & d[*]}:{e && f}}!'
-run 0 ../equals '{a:b:c}|->!Xb' '(a&b&c) -> !Xb'
+run 0 ../equals '{a:b:c}|->!Xb' '!(a&b&c) | !Xb'
 run 0 ../equals '{a:b:c*}|->!Xb' '{(a&&b)&c*}|-> !Xb'
 
 run 0 ../equals '{a[*0]}' '{[*0]}'