Implements spot::ltl::destroy() and exercise it.

* src/ltlast/atomic_prop.hh: Declare instance_count().
* src/ltlast/binop.hh, src/ltlast/unop.hh, src/ltlast/multop.hh:
Likewise.  Also, really inherit for ref_formula this time.
* src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
src/ltlast/unop.cc, src/ltlast/multop.cc: On destruction, suppress
the instance from the instance map.  Implement instance_count().
* src/ltlast/formula.cc, src/ltlast/formula.hh,
src/ltlast/ref_formula.cc, src/ltlast/ref_formula.hh: Add virtual
destructors.
* src/ltlparse/ltlparse.yy: Recover from binary operators with
missing right hand operand (the point is just to destroy the
the left hand operand).
* src/ltltest/equals.cc, src/ltltest/readltl.cc,
src/ltltest/tostring.cc: Destroy used formulae.  Make sure
instance_count()s are null are the end.
* src/ltltest/parseerr.test: Adjust expected result, now
that the parser lnows about missing right hand operands.
* src/ltlvisit/destroy.hh, src/ltlvisit/destroy.cc,
src/ltlvisit/postfix.hh, src/ltlvisit/postfix.cc: New files.
* src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Add them.
* src/ltlvisit/lunabbrev.cc (Xor, Equiv): Clone formulae
occurring twice in the rewritten expression.

ChangeLog

@@ -1,5 +1,30 @@
 2003-05-15  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	Implements spot::ltl::destroy() and exercise it.
+
+	* src/ltlast/atomic_prop.hh: Declare instance_count().
+	* src/ltlast/binop.hh, src/ltlast/unop.hh, src/ltlast/multop.hh:
+	Likewise.  Also, really inherit for ref_formula this time.
+	* src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
+	src/ltlast/unop.cc, src/ltlast/multop.cc: On destruction, suppress
+	the instance from the instance map.  Implement instance_count().
+	* src/ltlast/formula.cc, src/ltlast/formula.hh,
+	src/ltlast/ref_formula.cc, src/ltlast/ref_formula.hh: Add virtual
+	destructors.
+	* src/ltlparse/ltlparse.yy: Recover from binary operators with
+	missing right hand operand (the point is just to destroy the
+	the left hand operand).
+	* src/ltltest/equals.cc, src/ltltest/readltl.cc,
+	src/ltltest/tostring.cc: Destroy used formulae.  Make sure
+	instance_count()s are null are the end.
+	* src/ltltest/parseerr.test: Adjust expected result, now
+	that the parser lnows about missing right hand operands.
+	* src/ltlvisit/destroy.hh, src/ltlvisit/destroy.cc,
+	src/ltlvisit/postfix.hh, src/ltlvisit/postfix.cc: New files.
+	* src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Add them.
+	* src/ltlvisit/lunabbrev.cc (Xor, Equiv): Clone formulae
+	occurring twice in the rewritten expression.
+
 	Massage the AST so that identical sub-formula share the same
 	reference-counted formula*.  One can't call constructors for AST
 	items anymore, everything need to be acquired through instance()

src/ltlast/atomic_prop.cc

@@ -13,6 +13,11 @@ namespace spot
 
     atomic_prop::~atomic_prop()
     {
+      // Get this instance out of the instance map.
+      pair p(name(), &env());
+      map::iterator i = instances.find(p);
+      assert (i != instances.end());
+      instances.erase(i);
     }
 
     void
@@ -55,5 +60,11 @@ namespace spot
       return static_cast<atomic_prop*>(ap->ref());
     }
 
+    unsigned
+    atomic_prop::instance_count()
+    {
+      return instances.size();
+    }
+
   }
 }

src/ltlast/atomic_prop.hh

@@ -26,6 +26,10 @@ namespace spot
       const std::string& name() const;
       /// Get the environment of the atomic proposition.
       environment& env() const;
+
+      /// Number of instantiated atomic propositions.  For debugging.
+      static unsigned instance_count();
+
     protected:
       atomic_prop(const std::string& name, environment& env);
       virtual ~atomic_prop();

src/ltlast/binop.cc

@@ -13,6 +13,12 @@ namespace spot
 
     binop::~binop()
     {
+      // Get this instance out of the instance map.
+      pairf pf(first(), second());
+      pair p(op(), pf);
+      map::iterator i = instances.find(p);
+      assert (i != instances.end());
+      instances.erase(i);
     }
 
     void
@@ -95,5 +101,10 @@ namespace spot
       return static_cast<binop*>(ap->ref());
     }
 
+    unsigned
+    binop::instance_count()
+    {
+      return instances.size();
+    }
   }
 }

src/ltlast/binop.hh

@@ -2,7 +2,7 @@
 # define SPOT_LTLAST_BINOP_HH
 
 #include <map>
-#include "formula.hh"
+#include "refformula.hh"
 
 namespace spot
 {
@@ -10,7 +10,7 @@ namespace spot
   {
 
     /// Binary operator.
-    class binop : public formula
+    class binop : public ref_formula
     {
     public:
       /// Different kinds of binary opertaors
@@ -40,6 +40,9 @@ namespace spot
       /// Get the type of this operator, as a string.
       const char* op_name() const;
 
+      /// Number of instantiated binary operators.  For debugging.
+      static unsigned instance_count();
+
     protected:
       typedef std::pair<formula*, formula*> pairf;
       typedef std::pair<type, pairf> pair;

src/ltlast/formula.cc

@@ -11,6 +11,10 @@ namespace spot
       return this;
     }
 
+    formula::~formula()
+    {
+    }
+
     void
     formula::unref(formula* f)
     {

src/ltlast/formula.hh

@@ -15,6 +15,8 @@ namespace spot
     class formula
     {
     public:
+      virtual ~formula();
+
       virtual void accept(visitor& v) = 0;
       virtual void accept(const_visitor& v) const = 0;
 

src/ltlast/multop.cc

@@ -14,6 +14,12 @@ namespace spot
 
     multop::~multop()
     {
+      // Get this instance out of the instance map.
+      pair p(op(), children_);
+      map::iterator i = instances.find(p);
+      assert (i != instances.end());
+      instances.erase(i);
+
       delete children_;
     }
 
@@ -132,5 +138,10 @@ namespace spot
       *m = instance(op, v);
     }
 
+    unsigned
+    multop::instance_count()
+    {
+      return instances.size();
+    }
   }
 }

src/ltlast/multop.hh

@@ -3,7 +3,7 @@
 
 #include <vector>
 #include <map>
-#include "formula.hh"
+#include "refformula.hh"
 
 namespace spot
 {
@@ -13,7 +13,7 @@ namespace spot
     /// \brief Multi-operand operators.
     ///
     /// These operators are considered commutative and associative.
-    class multop : public formula
+    class multop : public ref_formula
     {
     public:
       enum type { Or, And };
@@ -61,6 +61,9 @@ namespace spot
       /// Get the type of this operator, as a string.
       const char* op_name() const;
 
+      /// Number of instantiated multi-operand operators.  For debugging.
+      static unsigned instance_count();
+
     protected:
       typedef std::vector<formula*> vec;
       typedef std::pair<type, vec*> pair;

src/ltlast/refformula.cc

@@ -10,6 +10,10 @@ namespace spot
     {
     }
 
+    ref_formula::~ref_formula()
+    {
+    }
+
     void
     ref_formula::ref_()
     {

src/ltlast/refformula.hh

@@ -12,6 +12,7 @@ namespace spot
     class ref_formula : public formula
     {
     protected:
+      virtual ~ref_formula();
       ref_formula();
       void ref_();
       bool unref_();

src/ltlast/unop.cc

@@ -13,6 +13,11 @@ namespace spot
 
     unop::~unop()
     {
+      // Get this instance out of the instance map.
+      pair p(op(), child());
+      map::iterator i = instances.find(p);
+      assert (i != instances.end());
+      instances.erase(i);
     }
 
     void
@@ -80,5 +85,10 @@ namespace spot
       return static_cast<unop*>(ap->ref());
     }
 
+    unsigned
+    unop::instance_count()
+    {
+      return instances.size();
+    }
   }
 }

src/ltlast/unop.hh

@@ -2,7 +2,7 @@
 # define SPOT_LTLAST_UNOP_HH
 
 #include <map>
-#include "formula.hh"
+#include "refformula.hh"
 
 namespace spot
 {
@@ -10,7 +10,7 @@ namespace spot
   {
 
     /// Unary operator.
-    class unop : public formula
+    class unop : public ref_formula
     {
     public:
       enum type { Not, X, F, G };
@@ -32,6 +32,9 @@ namespace spot
       /// Get the type of this operator, as a string.
       const char* op_name() const;
 
+      /// Number of instantiated unary operators.  For debugging.
+      static unsigned instance_count();
+
     protected:
       typedef std::pair<type, formula*> pair;
       typedef std::map<pair, formula*> map;

src/ltlparse/ltlparse.yy

@@ -2,6 +2,7 @@
 #include <string>
 #include "public.hh"
 #include "ltlast/allnodes.hh"
+#include "ltlvisit/destroy.hh"
 
 extern spot::ltl::formula* result;
 
@@ -83,6 +84,9 @@ ltl_formula: subformula
 many_errors: error
 	    | many_errors error
 
+/* The reason we use `constant::false_instance()' for error recovery
+   is that it isn't reference counted.  (Hence it can't leak references.)  */
+
 subformula: ATOMIC_PROP
 	      {
 		$$ = parse_environment.require(*$1);
@@ -120,18 +124,67 @@ subformula: ATOMIC_PROP
 	      { $$ = unop::instance(unop::Not, $2); }
             | subformula OP_AND subformula
 	      { $$ = multop::instance(multop::And, $1, $3); }
+            | subformula OP_AND error
+              {
+		destroy($1);
+	        error_list.push_back(parse_error(@2,
+				     "missing right operand for OP_AND"));
+		$$ = constant::false_instance();
+	      }
 	    | subformula OP_OR subformula
 	      { $$ = multop::instance(multop::Or, $1, $3); }
+            | subformula OP_OR error
+              {
+		destroy($1);
+	        error_list.push_back(parse_error(@2,
+				     "missing right operand for OP_OR"));
+		$$ = constant::false_instance();
+	      }
 	    | subformula OP_XOR subformula
 	      { $$ = binop::instance(binop::Xor, $1, $3); }
+            | subformula OP_XOR error
+              {
+		destroy($1);
+	        error_list.push_back(parse_error(@2,
+				     "missing right operand for OP_XOR"));
+		$$ = constant::false_instance();
+	      }
 	    | subformula OP_IMPLIES subformula
 	      { $$ = binop::instance(binop::Implies, $1, $3); }
+            | subformula OP_IMPLIES error
+              {
+		destroy($1);
+	        error_list.push_back(parse_error(@2,
+				     "missing right operand for OP_IMPLIES"));
+		$$ = constant::false_instance();
+	      }
             | subformula OP_EQUIV subformula
 	      { $$ = binop::instance(binop::Equiv, $1, $3); }
+            | subformula OP_EQUIV error
+              {
+		destroy($1);
+	        error_list.push_back(parse_error(@2,
+				     "missing right operand for OP_EQUIV"));
+		$$ = constant::false_instance();
+	      }
             | subformula OP_U subformula
 	      { $$ = binop::instance(binop::U, $1, $3); }
+            | subformula OP_U error
+              {
+		destroy($1);
+	        error_list.push_back(parse_error(@2,
+				     "missing right operand for OP_U"));
+		$$ = constant::false_instance();
+	      }
             | subformula OP_R subformula
 	      { $$ = binop::instance(binop::R, $1, $3); }
+            | subformula OP_R error
+              {
+		destroy($1);
+	        error_list.push_back(parse_error(@2,
+				     "missing right operand for OP_R"));
+		$$ = constant::false_instance();
+	      }
             | OP_F subformula
 	      { $$ = unop::instance(unop::F, $2); }
             | OP_G subformula

src/ltltest/equals.cc

@@ -5,6 +5,8 @@
 #include "ltlvisit/tunabbrev.hh"
 #include "ltlvisit/dump.hh"
 #include "ltlvisit/nenoform.hh"
+#include "ltlvisit/destroy.hh"
+#include "ltlast/allnodes.hh"
 
 void
 syntax(char* prog)
@@ -32,24 +34,44 @@ main(int argc, char** argv)
   if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
     return 2;
 
+#if (defined LUNABBREV) || (defined TUNABBREV) || (defined NENOFORM)
+  spot::ltl::formula* tmp;
+#endif
 #ifdef LUNABBREV
+  tmp = f1;
+  std::cout << spot::ltl::atomic_prop::instance_count() << std::endl;
   f1 = spot::ltl::unabbreviate_logic(f1);
+  std::cout << spot::ltl::atomic_prop::instance_count() << std::endl;
+  spot::ltl::destroy(tmp);
+  std::cout << spot::ltl::atomic_prop::instance_count() << std::endl;
   spot::ltl::dump(*f1, std::cout);
   std::cout << std::endl;
 #endif
 #ifdef TUNABBREV
+  tmp = f1;
   f1 = spot::ltl::unabbreviate_ltl(f1);
+  spot::ltl::destroy(tmp);
   spot::ltl::dump(*f1, std::cout);
   std::cout << std::endl;
 #endif
 #ifdef NENOFORM
+  tmp = f1;
   f1 = spot::ltl::negative_normal_form(f1);
+  spot::ltl::destroy(tmp);
   spot::ltl::dump(*f1, std::cout);
   std::cout << std::endl;
 #endif
 
-  if (equals(f1, f2))
+  int exit_code = !equals(f1, f2);
-    return 0;
-  return 1;
 
+  spot::ltl::destroy(f1);
+  std::cout << spot::ltl::atomic_prop::instance_count() << std::endl;
+  spot::ltl::destroy(f2);
+  std::cout << spot::ltl::atomic_prop::instance_count() << std::endl;
+  assert(spot::ltl::atomic_prop::instance_count() == 0);
+  assert(spot::ltl::unop::instance_count() == 0);
+  assert(spot::ltl::binop::instance_count() == 0);
+  assert(spot::ltl::multop::instance_count() == 0);
+
+  return exit_code;
 }

src/ltltest/parseerr.test

@@ -33,17 +33,19 @@ check()
 # Empty or unparsable strings
 check '' ''
 check '+' ''
-check 'a U' ''
-check 'a U b V c R' ''
 
 # leading and trailing garbage are skipped
 check '/2/3/4/5 a + b /6/7/8/' 'multop(Or, AP(a), AP(b))'
 check 'a U b c' 'binop(U, AP(a), AP(b))'
-check 'a &&& b' 'AP(b)'
+check 'a &&& b' 'multop(And, constant(0), AP(b))'
 # (check multop merging while we are at it)
 check 'a & b & c & d e' 'multop(And, AP(a), AP(b), AP(c), AP(d))'
 check 'a & (b | c) & d should work' 'multop(And, AP(a), multop(Or, AP(b), AP(c)), AP(d))'
 
+# Binop recovery
+check 'a U' 'constant(0)'
+check 'a U b V c R' 'constant(0)'
+
 # Recovery inside parentheses
 check 'a U (b c) U e R (f g <=> h)' \
       'binop(R, binop(U, binop(U, AP(a), AP(b)), AP(e)), AP(f))'

src/ltltest/readltl.cc

@@ -2,6 +2,8 @@
 #include "ltlparse/public.hh"
 #include "ltlvisit/dump.hh"
 #include "ltlvisit/dotty.hh"
+#include "ltlvisit/destroy.hh"
+#include "ltlast/allnodes.hh"
 
 void
 syntax(char* prog)
@@ -46,11 +48,16 @@ main(int argc, char** argv)
       spot::ltl::dump(*f, std::cout);
       std::cout << std::endl;
 #endif
+      spot::ltl::destroy(f);
     }
   else
     {
       exit_code = 1;
     }
 
+  assert(spot::ltl::atomic_prop::instance_count() == 0);
+  assert(spot::ltl::unop::instance_count() == 0);
+  assert(spot::ltl::binop::instance_count() == 0);
+  assert(spot::ltl::multop::instance_count() == 0);
   return exit_code;
 }

src/ltltest/tostring.cc

@@ -2,6 +2,8 @@
 #include "ltlparse/public.hh"
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/equals.hh"
+#include "ltlvisit/destroy.hh"
+#include "ltlast/allnodes.hh"
 
 void
 syntax(char *prog)
@@ -45,5 +47,12 @@ main(int argc, char **argv)
 
   if (f2s != f1s)
     return 1;
-}
 
+  spot::ltl::destroy(f1);
+  spot::ltl::destroy(f2);
+  assert(spot::ltl::atomic_prop::instance_count() == 0);
+  assert(spot::ltl::unop::instance_count() == 0);
+  assert(spot::ltl::binop::instance_count() == 0);
+  assert(spot::ltl::multop::instance_count() == 0);
+  return 0;
+}

src/ltlvisit/Makefile.am

@@ -5,6 +5,8 @@ noinst_LTLIBRARIES = libltlvisit.la
 libltlvisit_la_SOURCES = \
   clone.cc \
   clone.hh \
+  destroy.cc \
+  destroy.hh \
   dotty.cc \
   dotty.hh \
   dump.cc \
@@ -17,5 +19,7 @@ libltlvisit_la_SOURCES = \
   lunabbrev.cc \
   nenoform.hh \
   nenoform.cc \
+  postfix.hh \
+  postfix.cc \
   tunabbrev.hh \
   tunabbrev.cc

src/ltlvisit/destroy.cc

@@ -0,0 +1,25 @@
+#include "ltlvisit/destroy.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+
+    class destroy_visitor : public postfix_visitor
+    {
+    public:
+      virtual void
+      doit_default(formula* c)
+      {
+	formula::unref(c);
+      }
+    };
+
+    void
+    destroy(formula *f)
+    {
+      destroy_visitor v;
+      f->accept(v);
+    }
+  }
+}

src/ltlvisit/destroy.hh

@@ -0,0 +1,15 @@
+#ifndef SPOT_LTLVISIT_DESTROY_HH
+# define SPOT_LTLVISIT_DESTROY_HH
+
+#include "ltlvisit/postfix.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    /// \brief Destroys a formula
+    void destroy(formula *f);
+  }
+}
+
+#endif // SPOT_LTLVISIT_DESTROY_HH

src/ltlvisit/lunabbrev.cc

@@ -1,4 +1,5 @@
 #include "ltlast/allnodes.hh"
+#include "ltlvisit/clone.hh"
 #include "lunabbrev.hh"
 
 namespace spot
@@ -23,10 +24,10 @@ namespace spot
 	  /* f1 ^ f2  ==  (f1 & !f2) | (f2 & !f1) */
 	case binop::Xor:
 	  result_ = multop::instance(multop::Or,
-				     multop::instance(multop::And, f1,
+				     multop::instance(multop::And, clone(f1),
 						      unop::instance(unop::Not,
 								     f2)),
-				     multop::instance(multop::And, f2,
+				     multop::instance(multop::And, clone(f2),
 						      unop::instance(unop::Not,
 								     f1)));
 	  return;
@@ -38,7 +39,8 @@ namespace spot
 	  /* f1 <=> f2  ==  (f1 & f2) | (!f1 & !f2) */
 	case binop::Equiv:
 	  result_ = multop::instance(multop::Or,
-				     multop::instance(multop::And, f1, f2),
+				     multop::instance(multop::And,
+						      clone(f1), clone(f2)),
 				     multop::instance(multop::And,
 						      unop::instance(unop::Not,
 								     f1),

src/ltlvisit/postfix.cc

@@ -0,0 +1,89 @@
+#include "ltlvisit/postfix.hh"
+#include "ltlast/allnodes.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    postfix_visitor::postfix_visitor()
+    {
+    }
+
+    postfix_visitor::~postfix_visitor()
+    {
+    }
+
+    void
+    postfix_visitor::visit(atomic_prop* ap)
+    {
+      doit(ap);
+    }
+
+    void
+    postfix_visitor::visit(unop* uo)
+    {
+      uo->child()->accept(*this);
+      doit(uo);
+    }
+
+    void
+    postfix_visitor::visit(binop* bo)
+    {
+      bo->first()->accept(*this);
+      bo->second()->accept(*this);
+      doit(bo);
+    }
+
+    void
+    postfix_visitor::visit(multop* mo)
+    {
+      unsigned s = mo->size();
+      for (unsigned i = 0; i < s; ++i)
+	mo->nth(i)->accept(*this);
+      doit(mo);
+    }
+
+    void
+    postfix_visitor::visit(constant* c)
+    {
+      doit(c);
+    }
+
+    void
+    postfix_visitor::doit(atomic_prop* ap)
+    {
+      doit_default(ap);
+    }
+
+    void
+    postfix_visitor::doit(unop* uo)
+    {
+      doit_default(uo);
+    }
+
+    void
+    postfix_visitor::doit(binop* bo)
+    {
+      doit_default(bo);
+    }
+
+    void
+    postfix_visitor::doit(multop* mo)
+    {
+      doit_default(mo);
+    }
+
+    void
+    postfix_visitor::doit(constant* c)
+    {
+      doit_default(c);
+    }
+
+    void
+    postfix_visitor::doit_default(formula* f)
+    {
+      (void)f;
+      // Dummy implementation that does nothing.
+    }
+  }
+}

src/ltlvisit/postfix.hh

@@ -0,0 +1,38 @@
+#ifndef SPOT_LTLVISIT_POSTFIX_HH
+# define SPOT_LTLVISIT_POSTFIX_HH
+
+#include "ltlast/formula.hh"
+#include "ltlast/visitor.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    /// \brief Apply a algorithm on each node of an AST,
+    /// during a postfix traversal.
+    ///
+    /// Override one or more of the postifix_visitor::doit methods
+    /// with the algorithm to apply.
+    class postfix_visitor : public visitor
+    {
+    public:
+      postfix_visitor();
+      virtual ~postfix_visitor();
+
+      void visit(atomic_prop* ap);
+      void visit(unop* uo);
+      void visit(binop* bo);
+      void visit(multop* mo);
+      void visit(constant* c);
+
+      virtual void doit(atomic_prop* ap);
+      virtual void doit(unop* uo);
+      virtual void doit(binop* bo);
+      virtual void doit(multop* mo);
+      virtual void doit(constant* c);
+      virtual void doit_default(formula* f);
+    };
+  }
+}
+
+#endif // SPOT_LTLVISIT_POSTFIX_HH