Rewrite xor, =>, and <=> in negative_normal_form().

* src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc
(ltl_simplify::negative_normal_form): Remove the third
parameter and always rewrite XOR, =>, and <=>.  This avoid
problems with the cache, that could have been populated with
a different value for this third parameter.
* src/ltltest/reduc.cc, src/tgbaalgos/ltl2tgba_fm.cc: Adjust
calls to negative_normal_form().
* src/ltltest/nenoform.test: Adjust tests.

src/ltltest/nenoform.test

@@ -1,8 +1,8 @@
 #! /bin/sh
-# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
-# d<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC), Universit<69> Pierre
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
 # This file is part of Spot, a model checking library.
@@ -44,7 +44,7 @@ run 0 ../nenoform 'a & b' 'b & a & b'
 run 0 ../nenoform 'a & !b' '!b & a & a'
 run 0 ../nenoform 'a & b & (Xc |(f U !g)| e)' \
                   'b & a & a & (Xc | e |(f U !g)| e | Xc) & b'
-run 0 ../nenoform 'GFa => FGb' 'GFa => FGb'
+run 0 ../nenoform 'GFa => FGb' 'FG!a || FGb'
 
 # Basic rewritings
 run 0 ../nenoform '!!a' 'a'
@@ -52,8 +52,8 @@ run 0 ../nenoform '!!!!!a' '!a'
 run 0 ../nenoform '!Xa' 'X!a'
 run 0 ../nenoform '!Fa' 'G!a'
 run 0 ../nenoform '!Ga' 'F!a'
-run 0 ../nenoform '!(a ^ b)' 'a <=> b'
+run 0 ../nenoform '!(a ^ b)' '!a&!b | a&b'
-run 0 ../nenoform '!(a <=> b)' '(((a) ^ (b)))'
+run 0 ../nenoform '!(a <=> b)' '(!a&b) | a&!b'
 run 0 ../nenoform '!(a => b)' 'a&!b'
 run 0 ../nenoform '!(!a => !b)' '!a&b'
 run 0 ../nenoform '!(a U b)' '!a R !b'

src/ltltest/reduc.cc

@@ -202,7 +202,7 @@ main(int argc, char** argv)
     spot::ltl::formula* ftmp1;
 
     ftmp1 = f1;
-    f1 = simp->negative_normal_form(f1, false, true);
+    f1 = simp->negative_normal_form(f1, false);
     ftmp1->destroy();
 
     int length_f1_before = spot::ltl::length(f1);
@@ -219,7 +219,7 @@ main(int argc, char** argv)
     if (f2)
       {
 	ftmp1 = f2;
-	f2 = simp->negative_normal_form(f2, false, true);
+	f2 = simp->negative_normal_form(f2, false);
 	ftmp1->destroy();
 	f2s = spot::ltl::to_string(f2);
       }

src/ltlvisit/simplify.cc

@@ -365,15 +365,13 @@ namespace spot
       const formula*
       nenoform_recursively(const formula* f,
 			   bool negated,
-			   bool lunabbrev,
 			   ltl_simplifier_cache* c);
 
       class negative_normal_form_visitor: public visitor
       {
       public:
-	negative_normal_form_visitor(bool negated, bool lunabbrev,
+	negative_normal_form_visitor(bool negated, ltl_simplifier_cache* c)
-				     ltl_simplifier_cache* c)
+	  : negated_(negated), cache_(c)
-	  : negated_(negated), lunabbrev_(lunabbrev), cache_(c)
 	{
 	}
 
@@ -466,10 +464,6 @@ namespace spot
 
 	formula* equiv_or_xor(bool equiv, formula* f1, formula* f2)
 	{
-	  if (!lunabbrev_)
-	    return binop::instance(equiv ? binop::Equiv : binop::Xor,
-				   recurse_(f1, false),
-				   recurse_(f2, false));
 	  // Rewrite a<=>b as (a&b)|(!a&!b)
 	  if (equiv)
 	    return
@@ -513,10 +507,6 @@ namespace spot
 		result_ = multop::instance(multop::And,
 					   recurse_(f1, false),
 					   recurse_(f2, true));
-	      else if (!lunabbrev_)
-		result_ = binop::instance(binop::Implies,
-					  recurse_(f1, false),
-					  recurse_(f2, false));
 	      else // a => b == !a | b
 		result_ = multop::instance(multop::Or,
 					   recurse_(f1, true),
@@ -626,8 +616,7 @@ namespace spot
 	recurse_(formula* f, bool negated)
 	{
 	  return
-	    const_cast<formula*>(nenoform_recursively(f, negated,
+	    const_cast<formula*>(nenoform_recursively(f, negated, cache_));
-						      lunabbrev_, cache_));
 	}
 
 	formula*
@@ -639,7 +628,6 @@ namespace spot
       protected:
 	formula* result_;
 	bool negated_;
-	bool lunabbrev_;
 	ltl_simplifier_cache* cache_;
       };
 
@@ -647,7 +635,6 @@ namespace spot
       const formula*
       nenoform_recursively(const formula* f,
 			   bool negated,
-			   bool lunabbrev,
 			   ltl_simplifier_cache* c)
       {
 	if (f->kind() == formula::UnOp)
@@ -674,7 +661,7 @@ namespace spot
 	  }
 	else
 	  {
-	    negative_normal_form_visitor v(negated, lunabbrev, c);
+	    negative_normal_form_visitor v(negated, c);
 	    const_cast<formula*>(f)->accept(v);
 	    result = v.result();
 	  }
@@ -2277,7 +2264,7 @@ namespace spot
     {
       formula* neno = 0;
       if (!f->is_in_nenoform())
-	f = neno = negative_normal_form(f, false, true);
+	f = neno = negative_normal_form(f, false);
       formula* res = const_cast<formula*>(simplify_recursively(f, cache_));
       if (neno)
 	neno->destroy();
@@ -2285,11 +2272,9 @@ namespace spot
     }
 
     formula*
-    ltl_simplifier::negative_normal_form(const formula* f, bool negated,
+    ltl_simplifier::negative_normal_form(const formula* f, bool negated)
-					 bool lunabbrev)
     {
-      return const_cast<formula*>(nenoform_recursively(f, negated, lunabbrev,
+      return const_cast<formula*>(nenoform_recursively(f, negated, cache_));
-						       cache_));
     }
 
 

src/ltlvisit/simplify.hh

@@ -75,16 +75,13 @@ namespace spot
 
       /// Build the negative normal form of formula \a f.
       /// All negations of the formula are pushed in front of the
-      /// atomic propositions.
+      /// atomic propositions.  Operators <=>, =>, xor are all removed
+      /// (calling spot::ltl::unabbreviate_ltl is not needed).
       ///
       /// \param f The formula to normalize.
       /// \param negated If \c true, return the negative normal form of
       ///        \c !f
-      /// \param lunabbrev If \c true, also remove Xor, Equiv, and Implies
+      formula* negative_normal_form(const formula* f, bool negated = false);
-      ///        operators.  (It is faster than calling
-      ///        spot::ltl::unabbreviate_ltl first.)
-      formula* negative_normal_form(const formula* f, bool negated = false,
-				    bool lunabbrev = false);
 
 
     private:

src/tgbaalgos/ltl2tgba_fm.cc

@@ -1604,7 +1604,7 @@ namespace spot
 	// logic abbreviations such as <=>, =>, or XOR, since they
 	// would involve negations at the BDD level.
 	ltl_simplifier s;
-	f2 = s.negative_normal_form(f, false, true);
+	f2 = s.negative_normal_form(f, false);
       }
 
     typedef std::set<const formula*, formula_ptr_less_than> set_type;