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

* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
* src/ltltest/tunabbrev.test: New file.
* src/ltltest/lunabbrev.test: Fix comment.
* src/ltltest/Makefile.am (TESTS): Add tunabbrev.test.
(check_PROGRAMS): Add tunabbrev.
(tunabbrev_SOURCES, tunabbrev_CPPFLAGS): New variables.
* src/ltltest/equals.cc (main) [TUNABBREV]: Call unabbreviate_ltl.
* src/ltlvisit/lunabbrev.hh (unabbreviate_logic_visitor::recurse):
New virtual function.
* src/ltlvisit/lunabbrev.cc (unabbreviate_logic_visitor::recurse):
Likewise.
(unabbreviate_logic_visitor::visit): Use it instead of calling
unabbreviate_logic directly.

ChangeLog

@@ -1,5 +1,20 @@
 2003-04-16  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>
 
+	* src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh: New files.
+	* src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
+	* src/ltltest/tunabbrev.test: New file.
+	* src/ltltest/lunabbrev.test: Fix comment.
+	* src/ltltest/Makefile.am (TESTS): Add tunabbrev.test.
+	(check_PROGRAMS): Add tunabbrev.
+	(tunabbrev_SOURCES, tunabbrev_CPPFLAGS): New variables.
+	* src/ltltest/equals.cc (main) [TUNABBREV]: Call unabbreviate_ltl.
+	* src/ltlvisit/lunabbrev.hh (unabbreviate_logic_visitor::recurse):
+	New virtual function.
+	* src/ltlvisit/lunabbrev.cc (unabbreviate_logic_visitor::recurse):
+	Likewise.
+	(unabbreviate_logic_visitor::visit): Use it instead of calling 
+	unabbreviate_logic directly.
+
 	* src/ltlvisit/lunabbrev.hh: Add missing include guard.
 
 	* src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: New files.

src/ltltest/.cvsignore

@@ -9,3 +9,4 @@ expect
 defs
 equals
 lunabbrev
+tunabbrev

src/ltltest/Makefile.am

@@ -4,15 +4,17 @@ LDADD = ../ltlparse/libltlparse.a \
         ../ltlast/libltlast.a 
 
 check_SCRIPTS = defs
-check_PROGRAMS = ltl2dot ltl2text equals lunabbrev
+check_PROGRAMS = ltl2dot ltl2text equals lunabbrev tunabbrev
 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
+tunabbrev_SOURCES = equals.cc
+tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DTUNABBREV
 
 EXTRA_DIST = $(TESTS)
-TESTS = parse.test parseerr.test equals.test lunabbrev.test
+TESTS = parse.test parseerr.test equals.test lunabbrev.test tunabbrev.test
 
 CLEANFILES = stdout expect parse.dot

src/ltltest/equals.cc

@@ -2,6 +2,7 @@
 #include "ltlparse/public.hh"
 #include "ltlvisit/equals.hh"
 #include "ltlvisit/lunabbrev.hh"
+#include "ltlvisit/tunabbrev.hh"
 #include "ltlvisit/dump.hh"
 
 void
@@ -34,6 +35,10 @@ main(int argc, char **argv)
   f1 = spot::ltl::unabbreviate_logic(f1);
   spot::ltl::dump(*f1, std::cout);
 #endif
+#ifdef TUNABBREV
+  f1 = spot::ltl::unabbreviate_ltl(f1);
+  spot::ltl::dump(*f1, std::cout);
+#endif
 
   if (equals(f1, f2))
     return 0;

src/ltltest/lunabbrev.test

@@ -1,6 +1,6 @@
 #! /bin/sh
 
-# Check for the equals visitor
+# Check for the unabbreviate_logic visitor
 
 . ./defs || exit 1
 

src/ltltest/tunabbrev.test

@@ -0,0 +1,39 @@
+#! /bin/sh
+
+# Check for the unabbreviate_ltl visitor
+
+. ./defs || exit 1
+
+check()
+{
+  ./tunabbrev "$1" "$2" || exit 1
+}
+
+# A few things that do not change
+check 'a' 'a'
+check '1' '1'
+check '0' '0'
+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'
+
+# same as in lunabbrev.test:
+check 'a ^ b' '(a & !b) | (!a & b)'
+check 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
+check '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
+check '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
+
+# LTL unabbreviations:
+check 'G a ' 'false R a'
+check 'GF a => F G(b)' '!(false R (true U a)) | (true U (false V b))'
+check 'GGGGa' 'false V (false V (false V (false V a)))'
+check 'FFFfalse' 'true U ((true) U (true U (false)))'
+
+# Success.
+:

src/ltlvisit/Makefile.am

@@ -10,4 +10,6 @@ libltlvisit_a_SOURCES = \
   equals.cc \
   equals.hh \
   lunabbrev.hh \
-  lunabbrev.cc
+  lunabbrev.cc \
+  tunabbrev.hh \
+  tunabbrev.cc

src/ltlvisit/lunabbrev.cc

@@ -34,14 +34,14 @@ namespace spot
     void 
     unabbreviate_logic_visitor::visit(const unop* uo)
     {
-      result_ = new unop(uo->op(), unabbreviate_logic(uo->child()));
+      result_ = new unop(uo->op(), recurse(uo->child()));
     }
     
     void 
     unabbreviate_logic_visitor::visit(const binop* bo)
     {
-      formula* f1 = unabbreviate_logic(bo->first());
+      formula* f1 = recurse(bo->first());
-      formula* f2 = unabbreviate_logic(bo->second());
+      formula* f2 = recurse(bo->second());
       switch (bo->op())
 	{
 	  /* f1 ^ f2  ==  (f1 & !f2) | (f2 & !f1) */
@@ -82,11 +82,16 @@ namespace spot
       unsigned mos = mo->size();
       for (unsigned i = 0; i < mos; ++i)
 	{
-	  res->add(unabbreviate_logic(mo->nth(i)));
+	  res->add(recurse(mo->nth(i)));
 	}
       result_ = res;
     }
 
+    formula* unabbreviate_logic_visitor::recurse(const formula* f)
+    {
+      return unabbreviate_logic(f);
+    }
+
     formula* 
     unabbreviate_logic(const formula* f)
     {

src/ltlvisit/lunabbrev.hh

@@ -24,7 +24,9 @@ namespace spot
       void visit(const multop* mo);
       void visit(const constant* c);
 	
-    private:
+      virtual formula* recurse(const formula* f);
+      
+    protected:
       formula* result_;
     };
 

src/ltlvisit/tunabbrev.cc

@@ -0,0 +1,53 @@
+#include "ltlast/allnodes.hh"
+#include "tunabbrev.hh"
+
+namespace spot 
+{
+  namespace ltl
+  {
+    unabbreviate_ltl_visitor::unabbreviate_ltl_visitor()
+    {
+    }
+
+    unabbreviate_ltl_visitor::~unabbreviate_ltl_visitor()
+    {
+    }
+
+    void 
+    unabbreviate_ltl_visitor::visit(const unop* uo)
+    {
+      switch (uo->op())
+	{
+	case unop::X:
+	case unop::Not:
+	  this->super::visit(uo);
+	  return;
+	case unop::F:
+	  result_ = new binop(binop::U, 
+			      new constant(constant::True),
+			      recurse(uo->child()));
+	  return;
+	case unop::G:
+	  result_ = new binop(binop::R, 
+			      new constant(constant::False),
+			      recurse(uo->child()));
+	  return;
+	}
+    }
+    
+    formula* 
+    unabbreviate_ltl_visitor::recurse(const formula* f)
+    {
+      return unabbreviate_ltl(f);
+    }
+
+    formula* 
+    unabbreviate_ltl(const formula* f)
+    {
+      unabbreviate_ltl_visitor v;
+      f->accept(v);
+      return v.result();
+    }
+
+  }
+}

src/ltlvisit/tunabbrev.hh

@@ -0,0 +1,27 @@
+#ifndef SPOT_LTLVISIT_TUNABBREV_HH
+# define SPOT_LTLVISIT_TUNABBREV_HH
+
+#include "ltlast/formula.hh"
+#include "ltlvisit/lunabbrev.hh"
+
+namespace spot 
+{
+  namespace ltl
+  {
+    class unabbreviate_ltl_visitor : public unabbreviate_logic_visitor
+    {
+      typedef unabbreviate_logic_visitor super;
+    public:
+      unabbreviate_ltl_visitor();
+      virtual ~unabbreviate_ltl_visitor();
+
+      void visit(const unop* uo);
+
+      formula* recurse(const formula* f);
+    };
+
+    formula* unabbreviate_ltl(const formula* f);
+  }
+}
+
+#endif // SPOT_LTLVISIT_TUNABBREV_HH