Add trivial identities for &&, <>->, []-> and Boolean arguments.

* src/ltlast/binop.cc (EConcat, UConcat): Rewrite "{b}<>-> f"
as "b && f", and rewrite "{b}[]->f" as "b->f".
* src/ltlast/binop.hh (binop::instance): Document trivial
identities for <>-> and []->.
* src/ltlast/multop.cc (multop::instance): Rewrite "b1 & b2"
as "b1 && b2" when b1 and b2 are Boolean.
(multop::multop): Always disable is.boolean for AndNLM.
* src/ltlast/multop.hh: Document the rewriting.
* src/ltltest/equals.cc: Show the two formulas if the exit_code
is 1, to help debugging.
* src/ltltest/equals.test: Add more tests.
* src/ltltest/kind.test: Adjust tests.

src/ltlast/binop.cc

@@ -25,6 +25,7 @@
 #include <utility>
 #include "binop.hh"
 #include "unop.hh"
+#include "multop.hh"
 #include "constant.hh"
 #include "visitor.hh"
 #include <iostream>
@@ -365,6 +366,7 @@ namespace spot
 	  //   - 1 <>-> Exp = Exp
 	  //   - [*0] <>-> Exp = 0
 	  //   - Exp <>-> 0 = 0
+	  //   - boolExp <>-> Exp = boolExp & Exp
 	  if (first == constant::true_instance())
 	    return second;
 	  if (first == constant::false_instance()
@@ -378,12 +380,15 @@ namespace spot
 	      first->destroy();
 	      return second;
 	    }
+	  if (first->is_boolean())
+	    return multop::instance(multop::And, first, second);
 	  break;
 	case UConcat:
 	  //   - 0 []-> Exp = 1
 	  //   - 1 []-> Exp = Exp
 	  //   - [*0] []-> Exp = 1
 	  //   - Exp []-> 1 = 1
+	  //   - boolExp []-> Exp = boolExp -> Exp
 	  if (first == constant::true_instance())
 	    return second;
 	  if (first == constant::false_instance()
@@ -397,6 +402,8 @@ namespace spot
 	      first->destroy();
 	      return second;
 	    }
+	  if (first->is_boolean())
+	    return binop::instance(binop::Implies, first, second);
 	  break;
 	}
 

src/ltlast/binop.hh

@@ -1,4 +1,4 @@
-// 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épartement Systèmes Répartis Coopératifs (SRC),
@@ -96,6 +96,16 @@ namespace spot
       ///   - (1 M Exp) = Exp
       ///   - (0 M Exp) = 0
       ///   - (Exp M Exp) = Exp
+      ///   - 0 <>-> Exp = 0
+      ///   - 1 <>-> Exp = Exp
+      ///   - [*0] <>-> Exp = 0
+      ///   - Exp <>-> 0 = 0
+      ///   - boolExp <>-> Exp = boolExp & Exp
+      ///   - 0 []-> Exp = 1
+      ///   - 1 []-> Exp = Exp
+      ///   - [*0] []-> Exp = 1
+      ///   - Exp []-> 1 = 1
+      ///   - boolExp <>-> Exp = boolExp -> Exp
       static formula* instance(type op, formula* first, formula* second);
 
       virtual void accept(visitor& v);

src/ltlast/multop.cc

@@ -45,18 +45,18 @@ namespace spot
 	{
 	case Concat:
 	case Fusion:
+	case AndNLM:
+	  // Note: AndNLM(p1,p2) is a Boolean formula, but it is
+	  // actually rewritten as And(p1,p2) by trivial identities
+	  // before this constructor is called.  So at this point,
+	  // AndNLM is always used with at most one Boolean argument,
+	  // and the result is therefore NOT Boolean.
 	  is.boolean = false;
 	  is.ltl_formula = false;
 	  is.eltl_formula = false;
 	  is.psl_formula = false;
 	  is.eventual = false;
 	  is.universal = false;
-	  // fall through
-	case AndNLM:
-	  // The non-matching-length-And (&) can only appear in the
-	  // rational parts of PSL formula.  We don't remove the
-	  // Boolean flag, because applied to atomic propositions a&b
-	  // has the same effect as a&&b.
 	case And:
 	  for (unsigned i = 1; i < s; ++i)
 	    props &= (*v)[i]->get_props();
@@ -229,6 +229,27 @@ namespace spot
 	  abs = constant::false_instance();
 	  abs2 = 0;
 	  weak_abs = 0;
+
+	  // Make a first pass to gather all boolean terms.
+	  {
+	    vec* b = new vec;
+	    vec::iterator i = v->begin();
+	    while (i != v->end())
+	      {
+		if ((*i)->is_boolean())
+		  {
+		    b->push_back(*i);
+		    i = v->erase(i);
+		  }
+		else
+		  {
+		    ++i;
+		  }
+	      }
+	    // - AndNLM(Exps1...,Bool1,Exps2...,Bool2,Exp3...) =
+	    //    AndNLM(Exps1...,Exps2...,Exp3...,And(Bool1,Bool2))
+	    v->push_back(instance(And, b));
+	  }
 	  break;
 	case Or:
 	  neutral = constant::false_instance();
@@ -291,6 +312,7 @@ namespace spot
 		++i;
 	      }
 	  }
+
 	// We have    a* & [*0] & c  = 0
 	//     and    a* & [*0] & c* = [*0]
 	// So if [*0] has been seen, check if alls term recognize the

src/ltlast/multop.hh

@@ -89,6 +89,8 @@ namespace spot
       /// - AndNLM(Exps1...,0,Exps2...) = 0
       /// - AndNLM(Exps1...,[*0],Exps2...) = AndNLM(Exps1...,Exps2...)
       /// - AndNLM(Exp) = Exp
+      /// - AndNLM(Exps1...,BoolExp1,Exps2...,BoolExp2,Exp3...) =
+      ///    AndNLM(Exps1...,Exps2...,Exp3...,And(BoolExp1,BoolExp2))
       /// - Or(Exps1...,1,Exps2...) = 1
       /// - Or(Exps1...,0,Exps2...) = And(Exps1...,Exps2...)
       /// - Or(Exp) = Exp

src/ltltest/equals.cc

@@ -1,5 +1,5 @@
-// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Développement
+// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
-// de l'Epita (LRDE).
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -120,6 +120,12 @@ main(int argc, char** argv)
 
   int exit_code = f1 != f2;
 
+  if (exit_code)
+    {
+      spot::ltl::dump(std::cerr, f1) << std::endl;
+      spot::ltl::dump(std::cerr, f2) << std::endl;
+    }
+
   f1->destroy();
   f2->destroy();
 

src/ltltest/equals.test

@@ -51,6 +51,9 @@ run 0 ../equals 'a & false & a' 'false'
 run 0 ../equals 'a | false | a' 'a'
 run 0 ../equals 'true | a | a' 'true'
 run 0 ../equals '{a*}!' '{a*}<>->1'
+run 0 ../equals '{a -> b} (c)' '(a->b)->c'
+run 0 ../equals '{a & !b}!' 'a & !b'
+run 0 ../equals '{a;[*0]}|->!Xb' 'a -> !Xb'
 
 # other formulae which are not
 run 1 ../equals 'a' 'b'

src/ltltest/kind.test

@@ -49,10 +49,10 @@ check 'a M b'     '&!xfLP'
 check 'a M 1'     '&!xfLPe'
 check 'a R b'     '&!xfLP'
 check '0 R b'     '&!xfLPu'
-check '{a}|->!Xb' '&fP'
+check '{a;b}|->!Xb' '&fP'
-check '{a}|->X!b' '&!fP'
+check '{a;b}|->X!b' '&!fP'
-check '{a}|->!Gb' '&xP'
+check '{a;b}|->!Gb' '&xP'
-check '{a}|->F!b' '&!xP'
+check '{a;b}|->F!b' '&!xP'
 
 run 0 ../consterm '1'
 run 0 ../consterm '0'