Fix trivial rules for b₁:b₂ and b&f.

* src/ltlast/multop.cc (instance): Here.
* src/ltlast/multop.hh, doc/tl/tl.tex: Adjust documentation.
* src/ltltest/equals.test: Adjust test cases.

doc/tl/tl.tex

@@ -692,7 +692,7 @@ $b_1$, $b_2$ are assumed to be Boolean formul\ae.
 \end{align*}
 
 \noindent
-The following rules are all valid with the two arguments swapped, except the one marked with $\equivM$.
+The following rules are all valid with the two arguments swapped.
 %(Even for the non-commutative operators \samp{$\CONCAT$} and
 %\samp{$\FUSION$}.)
 
@@ -721,7 +721,7 @@ The following rules are all valid with the two arguments swapped, except the one
   b_1 \AND b_2 &\equiv b_1\ANDALT b_2 &
   &&
   &&
-  b:f &\equivM b\AND f\\
+  b_1:b_2 &\equiv b_1\ANDALT b_2\\
 \end{align*}
 
 \section{SERE-LTL Binding Operators}

src/ltlast/multop.cc

@@ -196,9 +196,9 @@ namespace spot
 	    // pointers that we must ignore.
 	    if ((*i) == 0)
 	      {
-		// FIXME: We should replace the pointer by the
-		// first non-null value at the end of the array
-		// instead of calling erase.
+		// FIXME: For commutative operators we should replace
+		// the pointer by the first non-null value at the end
+		// of the array instead of calling erase.
 		i = v->erase(i);
 		continue;
 	      }
@@ -271,9 +271,12 @@ namespace spot
 		    ++i;
 		  }
 	      }
-	    // - AndNLM(Exps1...,Bool1,Exps2...,Bool2,Exp3...) =
-	    //    AndNLM(Exps1...,Exps2...,Exp3...,And(Bool1,Bool2))
+	    // - AndNLM(Exps1...,Bool1,Exps2...,Bool2,Exps3...) =
+	    //    AndNLM(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2))
+	    if (!b->empty())
 	      v->push_back(instance(And, b));
+	    else
+	      delete b;
 	  }
 	  break;
 	case Or:
@@ -297,38 +300,39 @@ namespace spot
 	  abs2 = constant::empty_word_instance();
 	  weak_abs = 0;
 
-	  // Make a first pass to gather Boolean formulae.
+	  // Make a first pass to group adjacent Boolean formulae.
 	  // - Fusion(Exps1...,BoolExp1...BoolExpN,Exps2,Exps3...) =
-	  //   Fusion(Exps1...,AndNLM(And(BoolExp1...BoolExpN),Exps2),Exps3...)
+	  //   Fusion(Exps1...,And(BoolExp1...BoolExpN),Exps2,Exps3...)
 	  {
-	    vec* b = 0;
 	    vec::iterator i = v->begin();
 	    while (i != v->end())
 	      {
 		if ((*i)->is_boolean())
 		  {
-		    if (!b)
-		      b = new vec;
-		    b->push_back(*i);
-		    i = v->erase(i);
+		    vec::iterator first = i;
+		    ++i;
+		    if (i == v->end())
+		      break;
+		    if (!(*i)->is_boolean())
+		      {
+			++i;
+			continue;
+		      }
+		    do
+		      ++i;
+		    while (i != v->end() && (*i)->is_boolean());
+		    // We have at least two adjacent Boolean formulae.
+		    // Replace the first one by the conjunction of all.
+		    vec* b = new vec;
+		    b->insert(b->begin(), first, i);
+		    i = v->erase(first + 1, i);
+		    *first = instance(And, b);
 		  }
 		else
 		  {
-		    if (b)
-		      {
-			// We have found a non-Boolean Exp.  "AndNLM" it
-			// with all the previous Boolean formulae.
-			*i = instance(AndNLM, instance(And, b), *i);
-			b = 0;
-		      }
 		    ++i;
 		  }
 	      }
-	    if (b)
-	      {
-		// Group all trailing Boolean formulae.
-		v->push_back(instance(And, b));
-	      }
 	  }
 
 	  break;

src/ltlast/multop.hh

@@ -90,8 +90,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))
+      /// - AndNLM(Exps1...,BoolExp1,Exps2...,BoolExp2,Exps3...) =
+      ///    AndNLM(Exps1...,Exps2...,Exps3...,And(BoolExp1,BoolExp2))
       /// - Or(Exps1...,1,Exps2...) = 1
       /// - Or(Exps1...,0,Exps2...) = And(Exps1...,Exps2...)
       /// - Or(Exp) = Exp
@@ -103,7 +103,7 @@ namespace spot
       /// - Fusion(Exps1...,[*0],Exps2...) = 0
       /// - Fusion(Exp) = Exp
       /// - Fusion(Exps1...,BoolExp1...BoolExpN,Exps2,Exps3...) =
-      ///     Fusion(Exps1...,AndNLM(And(BoolExp1...BoolExpN),Exps2),Exps3...)
+      ///     Fusion(Exps1...,And(BoolExp1...BoolExpN),Exps2,Exps3...)
       static formula* instance(type op, vec* v);
 
       virtual void accept(visitor& v);

src/ltltest/equals.test

@@ -145,9 +145,10 @@ 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'
-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}: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]}'
 run 0 ../equals '{a[*..]}' '{a[*]}'