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

* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
* src/ltlast/multop.cc (multop::multop(type)): New constructor.
* src/ltlast/multop.hh (multop::multop(type)): New constructor.
* src/ltltest/lunabbrev.test: New file.
* src/ltltest/Makefile.am (TESTS): Add lunabbrev.test.
(check_PROGRAMS): Add lunabbrev.
(lunabbrev_SOURCES, lunabbrev_CPPFLAGS): New variables.
* src/ltltest/equals.cc (main) [LUNABBREV]: Call unabbreviate_logic.

ChangeLog

@@ -1,5 +1,15 @@
 2003-04-16  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>
 
+	* src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: New files.
+	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
+	* src/ltlast/multop.cc (multop::multop(type)): New constructor.
+	* src/ltlast/multop.hh (multop::multop(type)): New constructor.
+	* src/ltltest/lunabbrev.test: New file.
+	* src/ltltest/Makefile.am (TESTS): Add lunabbrev.test.
+	(check_PROGRAMS): Add lunabbrev.
+	(lunabbrev_SOURCES, lunabbrev_CPPFLAGS): New variables.
+	* src/ltltest/equals.cc (main) [LUNABBREV]: Call unabbreviate_logic.
+
 	* src/ltltest/equals.test (check0, check1): Remove. Use check 0, and
 	check 1 instead.
 

src/ltlast/multop.cc

@@ -7,6 +7,11 @@ namespace spot
 {
   namespace ltl
   {    
+    multop::multop(type op)
+      : op_(op)
+    {
+    }
+
     multop::multop(type op, formula* first, formula* second)
       : op_(op)
     {

src/ltlast/multop.hh

@@ -14,9 +14,10 @@ namespace spot
     public:
       enum type { Or, And };
 
-      // A multop has at least two arguments.
+      multop::multop(type op);
+      // A multop usually has at least two arguments.
       multop(type op, formula* first, formula* second);
-      // More argument can be added.
+      // More arguments can be added.
       void add(formula* f);
       
       virtual ~multop();

src/ltltest/.cvsignore

@@ -8,3 +8,4 @@ parser.dot
 expect
 defs
 equals
+lunabbrev

src/ltltest/Makefile.am

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

src/ltltest/equals.cc

@@ -1,6 +1,8 @@
 #include <iostream>
 #include "ltlparse/public.hh"
 #include "ltlvisit/equals.hh"
+#include "ltlvisit/lunabbrev.hh"
+#include "ltlvisit/dump.hh"
 
 void
 syntax(char *prog)
@@ -28,6 +30,11 @@ main(int argc, char **argv)
   if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
     return 2;
 
+#ifdef LUNABBREV
+  f1 = spot::ltl::unabbreviate_logic(f1);
+  spot::ltl::dump(*f1, std::cout);
+#endif
+
   if (equals(f1, f2))
     return 0;
   return 1;

src/ltltest/lunabbrev.test

@@ -0,0 +1,35 @@
+#! /bin/sh
+
+# Check for the equals visitor
+
+. ./defs || exit 1
+
+check()
+{
+  ./lunabbrev "$1" "$2" || exit 1
+}
+
+# A few things that do not change
+check 'a' 'a'
+check '1' '1'
+check '0' '0'
+check 'G a ' ' G a'
+check 'a U b' 'a U b'
+check 'a & b' 'a & b'
+check 'a & b' 'b & a'
+check 'a & b & c' 'c & a & b'
+check 'a & b & c' 'b & c & a'
+check 'a & b & a' 'b & a & b'
+check 'a & b' 'b & a & b'
+check 'a & b' 'b & a & a'
+check 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
+
+# other formulae that do change
+check 'a ^ b' '(a & !b) | (!a & b)'
+check 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
+check 'GF a => F G(b)' '!GFa | F Gb'
+check '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
+check '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
+
+# Success.
+:

src/ltlvisit/Makefile.am

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

src/ltlvisit/lunabbrev.cc

@@ -0,0 +1,99 @@
+#include "ltlast/allnodes.hh"
+#include "lunabbrev.hh"
+
+namespace spot 
+{
+  namespace ltl
+  {
+    unabbreviate_logic_visitor::unabbreviate_logic_visitor()
+    {
+    }
+
+    unabbreviate_logic_visitor::~unabbreviate_logic_visitor()
+    {
+    }
+
+    formula*
+    unabbreviate_logic_visitor::result() const
+    {
+      return result_;
+    }
+    
+    void 
+    unabbreviate_logic_visitor::visit(const atomic_prop* ap)
+    {
+      result_ = new atomic_prop(ap->name());
+    }
+
+    void 
+    unabbreviate_logic_visitor::visit(const constant* c)
+    {
+      result_ = new constant(c->val());
+    }
+
+    void 
+    unabbreviate_logic_visitor::visit(const unop* uo)
+    {
+      result_ = new unop(uo->op(), unabbreviate_logic(uo->child()));
+    }
+    
+    void 
+    unabbreviate_logic_visitor::visit(const binop* bo)
+    {
+      formula* f1 = unabbreviate_logic(bo->first());
+      formula* f2 = unabbreviate_logic(bo->second());
+      switch (bo->op())
+	{
+	  /* f1 ^ f2  ==  (f1 & !f2) | (f2 & !f1) */
+	case binop::Xor:
+	  result_ = new multop(multop::Or,
+			       new multop(multop::And, f1,
+					  new unop(unop::Not, f2)),
+			       new multop(multop::And, f2,
+					  new unop(unop::Not, f1)));
+	  return;
+	  /* f1 => f2  ==  !f1 | f2 */
+	case binop::Implies:
+	  result_ = new multop(multop::Or, new unop(unop::Not, f1), f2);
+	  return;
+	  /* f1 <=> f2  ==  (f1 & f2) | (!f1 & !f2) */
+	case binop::Equiv:
+	  result_ = new multop(multop::Or,
+			       new multop(multop::And, f1, f2),
+			       new multop(multop::And, 
+					  new unop(unop::Not, f1),
+					  new unop(unop::Not, f2)));
+	  return;
+	  /* f1 U f2 == f1 U f2 */
+	  /* f1 R f2 == f1 R f2 */
+	case binop::U:
+	case binop::R:
+	  result_ = new binop(bo->op(), f1, f2);
+	  return;
+	}
+      /* Unreachable code. */
+      assert(0);
+    }
+    
+    void 
+    unabbreviate_logic_visitor::visit(const multop* mo)
+    {
+      multop* res = new multop(mo->op());
+      unsigned mos = mo->size();
+      for (unsigned i = 0; i < mos; ++i)
+	{
+	  res->add(unabbreviate_logic(mo->nth(i)));
+	}
+      result_ = res;
+    }
+
+    formula* 
+    unabbreviate_logic(const formula* f)
+    {
+      unabbreviate_logic_visitor v;
+      f->accept(v);
+      return v.result();
+    }
+
+  }
+}

src/ltlvisit/lunabbrev.hh

@@ -0,0 +1,30 @@
+#include "ltlast/formula.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 unabbreviate_logic_visitor : public const_visitor
+    {
+    public:
+      unabbreviate_logic_visitor();
+      virtual ~unabbreviate_logic_visitor();
+
+      formula* result() const;
+      
+      void visit(const atomic_prop* ap);
+      void visit(const unop* uo);
+      void visit(const binop* bo);
+      void visit(const multop* mo);
+      void visit(const constant* c);
+	
+    private:
+      formula* result_;
+    };
+
+    formula* unabbreviate_logic(const formula* f);
+  }
+}