Trivially reduce 1[*]&&f = f and 1[*]|f = 1[*].

* src/ltlast/bunop.hh (one_star): New static method building 1[*].
* src/ltlast/bunop.cc (bunop::~bunop, bunop::instance_count): Adjust.
* src/ltlast/multop.cc: Implement the trivial rewriting.
* src/ltlast/multop.hh, doc/tl/tl.tex: Document it.
* src/ltltest/equals.test: Test it.

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 (on input).
+The following rules are all valid with the two arguments swapped.
 %(Even for the non-commutative operators \samp{$\CONCAT$} and
 %\samp{$\FUSION$}.)
 
@@ -713,6 +713,11 @@ The following rules are all valid with the two arguments swapped (on input).
   \1\ANDALT b   &\equiv b &
   \1\OR b &\equiv \1 &
   \1 \FUSION f & \equiv f\mathrlap{\text{~if~}\varepsilon\nVDash f}\\
+  &&
+  \1\STAR{} \AND f &\equiv f &
+  \1\STAR{} \OR f &\equiv \1\STAR{} &
+  &&
+  && \\
   \eword\AND f &\equiv f &
   \eword\ANDALT f &\equiv
   \begin{cases}

src/ltlast/bunop.cc

@@ -31,6 +31,10 @@ namespace spot
 {
   namespace ltl
   {
+    // Can't build it on startup, because it uses
+    // constant::true_instance that may not have been built yet...
+    formula* bunop::one_star_ = 0;
+
     bunop::bunop(type op, formula* child, unsigned min, unsigned max)
       : ref_formula(BUnOp), op_(op), child_(child), min_(min), max_(max)
     {
@@ -62,6 +66,10 @@ namespace spot
 
     bunop::~bunop()
     {
+      // one_star_ should never get delete.  Otherwise, that means
+      // is has been destroyed too much, or not cloned enough.
+      assert(this != one_star_);
+
       // Get this instance out of the instance map.
       pair p(pairo(op(), child()), pairu(min_, max_));
       map::iterator i = instances.find(p);
@@ -316,7 +324,8 @@ namespace spot
     unsigned
     bunop::instance_count()
     {
-      return instances.size();
+      // Don't count one_star_ since it should not be destroyed.
+      return instances.size() - !!one_star_;
     }
 
     std::ostream&

src/ltlast/bunop.hh

@@ -26,6 +26,7 @@
 #include <map>
 #include <iosfwd>
 #include "refformula.hh"
+#include "constant.hh"
 
 namespace spot
 {
@@ -116,6 +117,18 @@ namespace spot
       /// Dump all instances.  For debugging.
       static std::ostream& dump_instances(std::ostream& os);
 
+      /// \brief Return a formula for <code>1[*]</code>.
+      ///
+      /// A global instance is returned, and it should not be
+      /// destroyed.  Remember to clone it if you use it to build a
+      /// formula.
+      static formula* one_star()
+      {
+	if (!one_star_)
+	  one_star_ = instance(Star, constant::true_instance());
+	return one_star_;
+      }
+
     protected:
       typedef std::pair<unsigned, unsigned> pairu;
       typedef std::pair<type, formula*> pairo;
@@ -131,6 +144,7 @@ namespace spot
       formula* child_;
       unsigned min_;
       unsigned max_;
+      static formula* one_star_;
     };
 
     /// \brief Cast \a f into a bunop.

src/ltlast/multop.cc

@@ -27,6 +27,7 @@
 #include <iostream>
 #include "multop.hh"
 #include "constant.hh"
+#include "bunop.hh"
 #include "visitor.hh"
 
 namespace spot
@@ -300,7 +301,7 @@ namespace spot
 	  weak_abs = 0;
 	  break;
 	case AndRat:
-	  neutral = 0; /* FIXME: we should use 1[*] as neutral */
+	  neutral = bunop::one_star();
 	  neutral2 = 0;
 	  abs = constant::false_instance();
 	  abs2 = 0;
@@ -325,7 +326,7 @@ namespace spot
 	case OrRat:
 	  neutral = constant::false_instance();
 	  neutral2 = 0;
-	  abs = 0; // FIXME: should be 1[*].
+	  abs = bunop::one_star();
 	  abs2 = 0;
 	  weak_abs = 0;
 	  gather_bool(v, Or);
@@ -409,7 +410,7 @@ namespace spot
 		for (i = v->begin(); i != v->end(); ++i)
 		  (*i)->destroy();
 		delete v;
-		return abs;
+		return abs->clone();
 	      }
 	    else
 	      {
@@ -469,7 +470,7 @@ namespace spot
 	{
 	  delete v;
 	  assert(neutral != 0);
-	  return neutral;
+	  return neutral->clone();
 	}
       else if (s == 1)
 	{

src/ltlast/multop.hh

@@ -101,9 +101,11 @@ namespace spot
       ///    AndRat(Exps1...,Exps2...,And(BoolExp1,BoolExps2...))
       /// - AndRat(Exps1...,[*0],Exps2...) = [*0] if all Expi accept [*0]
       /// - AndRat(Exps1...,[*0],Exps2...) = 0 if some Expi reject [*0]
+      /// - AndRat(Exps1...,1[*],Exps2...) = AndRat(Exps1...,Exps2...)
       /// - OrRat(Exps1...,0,Exps2...) = OrRat(Exps1...,Exps2...)
       /// - OrRat(Exps1...,BoolExp1,Exps2...,BoolExps2...) =
       ///    OrRat(Exps1...,Exps2...,Or(BoolExp1,BoolExps2...))
+      /// - OrRat(Exps1...,1[*],Exps2...) = 1[*]
       /// - Concat(Exps1...,0,Exps2...) = 0
       /// - Concat(Exps1...,[*0],Exps2...) = Concat(Exps1...,Exps2...)
       /// - Concat(Exp) = Exp

src/ltltest/equals.test

@@ -149,6 +149,8 @@ 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&&[*]}!' 'a'
+run 0 ../equals '{[*]||a||[*]}!' '{[*]}!'
 run 0 ../equals '{0&{f;g*}}!' '0'
 run 0 ../equals '{1&{f;g*}}!' '{f;g*}!'
 # 1 should not be removed in the following two formulae