* src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: New files.

* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add equals.hh
and equals.cc.
* src/ltltest/equals.cc, src/ltltest/equals.test: New files.
* src/ltltest/Makefile.am (check_PROGRAMS): Add equals.
(equals_SOURCES): New variable.
(TESTS): Add equals.test.

ChangeLog

 2003-04-16  Alexandre DURET-LUTZ  <aduret@circe.lip6.fr>
 
+	* src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: New files.
+	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add equals.hh
+	and equals.cc.
+	* src/ltltest/equals.cc, src/ltltest/equals.test: New files.
+	* src/ltltest/Makefile.am (check_PROGRAMS): Add equals.
+	(equals_SOURCES): New variable.
+	(TESTS): Add equals.test.
+
 	* src/ltlast/multop.cc (multop::multop): Use multop::add.
 	(multop::add): If the formulae we add is itself a multop for the 
 	same operator, merge its children with ours.

src/ltltest/.cvsignore

@@ -7,3 +7,4 @@ stdout
 parser.dot
 expect
 defs
+equals

src/ltltest/Makefile.am

@@ -4,12 +4,13 @@ LDADD = ../ltlparse/libltlparse.a \
         ../ltlast/libltlast.a 
 
 check_SCRIPTS = defs
-check_PROGRAMS = ltl2dot ltl2text
+check_PROGRAMS = ltl2dot ltl2text equals
 ltl2dot_SOURCES = readltl.cc
 ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
 ltl2text_SOURCES = readltl.cc
+equals_SOURCES = equals.cc
 
 EXTRA_DIST = $(TESTS)
-TESTS = parse.test parseerr.test
+TESTS = parse.test parseerr.test equals.test
 
 CLEANFILES = stdout expect parse.dot

src/ltltest/equals.cc

+#include <iostream>
+#include "ltlparse/public.hh"
+#include "ltlvisit/equals.hh"
+
+void
+syntax(char *prog)
+{
+  std::cerr << prog << " formulae1 formulae2" << std::endl;
+  exit(2);
+}
+
+bool 
+print_parse_error(const char* f, spot::ltl::parse_error_list& pel)
+{
+  bool err = false;
+
+  spot::ltl::parse_error_list::iterator it;
+  for (it = pel.begin(); it != pel.end(); ++it)
+    {
+      std::cerr << ">>> " << f << std::endl;
+      unsigned n = 0;
+      yy::Location& l = it->first;
+      for (; n < 4 + l.begin.column; ++n)
+	std::cerr << ' ';
+      // Write at least one '^', even if begin==end.
+      std::cerr << '^';
+      ++n;
+      for (; n < 4 + l.end.column; ++n)
+	std::cerr << '^';
+      std::cerr << std::endl << it->second << std::endl << std::endl;
+      err = true;
+    }
+  return err;
+}
+
+int
+main(int argc, char **argv)
+{
+  if (argc != 3)
+    syntax(argv[0]);
+
+  
+  spot::ltl::parse_error_list p1;
+  spot::ltl::formulae *f1 = spot::ltl::parse(argv[1], p1);
+
+  if (print_parse_error(argv[1], p1))
+    return 2;
+
+  spot::ltl::parse_error_list p2;
+  spot::ltl::formulae *f2 = spot::ltl::parse(argv[2], p2);
+			
+  if (print_parse_error(argv[2], p2))
+    return 2;
+
+  if (equals(f1, f2))
+    return 0;
+  return 1;
+
+}

src/ltltest/equals.test

+#! /bin/sh
+
+# Check for the equals visitor
+
+. ./defs || exit 1
+
+check()
+{
+  ./equals "$2" "$3" 
+  test $? != $1 && exit 1;
+}
+
+check0()
+{
+  check 0 "$@"
+}
+
+check1()
+{
+  check 1 "$@"
+}
+
+# A few things which are equal
+check0 'a' 'a'
+check0 '1' '1'
+check0 '0' '0'
+check0 'a => b' 'a => b'
+check0 'G a ' ' G a'
+check0 'a U b' 'a U b'
+check0 'a & b' 'a & b'
+check0 'a & b' 'b & a'
+check0 'a & b & c' 'c & a & b'
+check0 'a & b & c' 'b & c & a'
+check0 'a & b & a' 'b & a & b'
+check0 'a & b' 'b & a & b'
+check0 'a & b' 'b & a & a'
+check0 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
+
+# other formulae which are not
+check1 'a' 'b'
+check1 '1' '0'
+check1 'a => b' 'b => a'
+check1 'a => b' 'a <=> b'
+check1 'a => b' 'a U b'
+check1 'a R b' 'a U b'
+check1 'a & b & c' 'c & a'
+check1 'b & c' 'c & a & b'
+check1 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(g U g)| e | c) & b'
+
+# Success.
+:
\ No newline at end of file

src/ltlvisit/Makefile.am

@@ -6,4 +6,6 @@ libltlvisit_a_SOURCES = \
   dotty.cc \
   dotty.hh \
   dump.cc \
-  dump.hh 
+  dump.hh \
+  equals.cc \
+  equals.hh

src/ltlvisit/equals.cc

+#include <vector>
+#include "equals.hh"
+#include "ltlast/allnodes.hh"
+
+namespace spot 
+{
+  namespace ltl
+  {
+    equals_visitor::equals_visitor(const formulae* f)
+      : f_(f), result_(false)
+    {
+    }
+
+    equals_visitor::~equals_visitor()
+    {
+    }
+
+    bool 
+    equals_visitor::result() const
+    {
+      return result_;
+    }
+      
+    void
+    equals_visitor::visit(const atomic_prop* ap)
+    {
+      const atomic_prop* p = dynamic_cast<const atomic_prop*>(f_);
+      if (p && p->name() == ap->name())
+	result_ = true;
+    }
+
+    void
+    equals_visitor::visit(const constant* c)
+    {
+      const constant* p = dynamic_cast<const constant*>(f_);
+      if (p && p->val() == c->val())
+	result_ = true;
+    }
+
+    void
+    equals_visitor::visit(const unop* uo)
+    {
+      const unop* p = dynamic_cast<const unop*>(f_);
+      if (!p || p->op() != uo->op())
+	return;
+      f_ = p->child();
+      uo->child()->accept(*this);
+    }
+
+    void
+    equals_visitor::visit(const binop* bo)
+    {
+      const binop* p = dynamic_cast<const binop*>(f_);
+      if (!p || p->op() != bo->op())
+	return;
+      
+      // The current visitor will descend the left branch.
+      // Build a second visitor for the right branch.
+      equals_visitor v2(p->second());
+      f_ = p->first();
+      
+      bo->first()->accept(*this);
+      if (result_ == false)
+	return;
+      
+      bo->second()->accept(v2);
+      result_ = v2.result();
+    }
+    
+    void
+    equals_visitor::visit(const multop* m)
+    {
+      const multop* p = dynamic_cast<const multop*>(f_);
+      if (!p || p->op() != m->op())
+	return;
+      
+      // This check is a bit more complicated than other checks
+      // because And(a, b, c) is equal to And(c, a, b, a).
+      
+      unsigned m_size = m->size();
+      unsigned p_size = p->size();
+      std::vector<bool> p_seen(p_size, false);
+      
+      for (unsigned nf = 0; nf < m_size; ++nf)
+	{
+	  unsigned np;
+	  const formulae* mnth = m->nth(nf);
+	  for (np = 0; np < p_size; ++np)
+	    {
+	      if (equals(p->nth(np), mnth))
+		{
+		  p_seen[np] = true;
+		  break;
+		}
+	    }
+	  // We we haven't found mnth in any child of p, then
+	  // the two formulaes aren't equal.
+	  if (np == p_size)
+	    return;
+	}
+      // At this point, we have found all children of m' in children
+      // of `p'.  That doesn't means that both formula are equal.
+      // Condider m = And(a, b, c) against p = And(c, d, a, b).
+      // We should now check if any unmarked (accodring to p_seen)
+      // child of `p' has an counterpart in `m'.  Because `m' might 
+      // contain duplicate children, its faster to test that
+      // unmarked children of `p' have a counterpart in marked children
+      // of `p'.
+      for (unsigned np = 0; np < p_size; ++np)
+	{
+	  // Consider only unmarked children.
+	  if (p_seen[np])
+	    continue;
+	  
+	  // Compare with marked children.
+	  unsigned np2;
+	  const formulae *pnth = p->nth(np);
+	  for (np2 = 0; np2 < p_size; ++np2)
+	    if (p_seen[np2] && equals(p->nth(np2), pnth))
+	      break;
+	  
+	  // No match?  Too bad.
+	  if (np2 == p_size) 
+	    return;
+	}
+      
+      // The two formulaes match.
+      result_ = true;
+    }
+
+
+    bool 
+    equals(const formulae* f1, const formulae* f2)
+    {
+      equals_visitor v(f1);
+      f2->accept(v);
+      return v.result();
+    }
+  }
+}

src/ltlvisit/equals.hh

+#include "ltlast/formulae.hh"
+#include "ltlast/visitor.hh"
+
+namespace spot 
+{
+  namespace ltl
+  {
+    // This visitor is public, because it's convenient
+    // to derive from it and override part of its methods.
+    class equals_visitor : public const_visitor
+    {
+    public:
+      equals_visitor(const formulae* f);
+      virtual ~equals_visitor();
+
+      // Return true iff the visitor has visited a
+      // formulae which is equal to `f'.
+      bool result() const;
+      
+      void visit(const atomic_prop* ap);
+      void visit(const unop* uo);
+      void visit(const binop* bo);
+      void visit(const multop* bo);
+      void visit(const constant* c);
+	
+    private:
+      const formulae* f_;
+      bool result_;
+	      
+    };
+
+    bool equals(const formulae* f1, const formulae* f2);
+  }
+}