* src/ltltest/tostring.test: New file.

* src/ltltest/tostring.cc: New files.
* src/ltlvisit/tostring.hh: From ast to string New files.
* src/ltlvisit/tostring.cc: From ast to string New files.

ChangeLog

@@ -1,3 +1,10 @@
+2003-04-24  Rachid REBIHA  <rebiha@nyx>
+
+	* src/ltltest/tostring.test: New file.
+	* src/ltltest/tostring.cc: New files.
+	* src/ltlvisit/tostring.hh: From ast to string New files.
+	* src/ltlvisit/tostring.cc: From ast to string New files.
+
 2003-04-18  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>
 
 	* src/ltlparse/Makefile.am (EXTRA_DIST): Distribute ltlparse.yy.

src/ltltest/Makefile.am

@@ -5,7 +5,6 @@ LDADD = ../ltlparse/libltlparse.a \
 	../ltlenv/libltlenv.a 
 
 check_SCRIPTS = defs
-
 # Keep this sorted alphabetically.
 check_PROGRAMS = \
   equals \
@@ -13,22 +12,25 @@ check_PROGRAMS = \
   ltl2text \
   lunabbrev \
   nenoform \
+  tostring \
   tunabbrev \
   tunenoform
 
+equals_SOURCES = equals.cc
 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
 nenoform_SOURCES = equals.cc
 nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM
+tostring_SOURCES = tostring.cc
+tunabbrev_SOURCES = equals.cc
+tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DTUNABBREV
 tunenoform_SOURCES = equals.cc
 tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DTUNABBREV
 
+
 EXTRA_DIST = $(TESTS)
 
 # Ordered by strength of the test.  Test basic features first.
@@ -36,6 +38,7 @@ TESTS = \
   parse.test \
   parseerr.test \
   equals.test \
+  tostring.test \
   lunabbrev.test \
   tunabbrev.test \
   nenoform.test \

src/ltltest/tostring.cc

@@ -0,0 +1,45 @@
+#include <iostream>
+#include <sstream>
+#include "ltlparse/public.hh"
+#include "ltlvisit/tostring.hh"
+#include "ltlvisit/equals.hh"
+
+void
+syntax(char *prog)
+{
+  std::cerr << prog << " formula1" << std::endl;
+  exit(2);
+}
+
+int
+main(int argc, char **argv)
+{
+  if (argc != 2)
+    syntax(argv[0]);
+  
+  spot::ltl::parse_error_list p1;
+  spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
+
+  if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
+    return 2;
+
+  std::ostringstream os;
+  spot::ltl::to_string(*f1, os);
+  std::cout << os.str() << std::endl;
+
+  spot::ltl::formula* f2 = spot::ltl::parse(os.str(), p1);
+
+  if (spot::ltl::format_parse_errors(std::cerr, os.str(), p1))
+    return 2;
+
+  std::ostringstream os2;
+  spot::ltl::to_string(*f2, os2);
+  std::cout << os2.str() << std::endl;
+
+  if (os2.str() != os.str())
+    return 1;
+
+  if (! equals(f1, f2))
+    return 1;
+}
+ 

src/ltltest/tostring.test

@@ -0,0 +1,28 @@
+#! /bin/sh
+
+# Check that spot::ltl::tostring is correct: after to parse we get the
+# string of the abstract syntax tree and xe parse it again to apply spot::ltl::tostring one more times.
+
+. ./defs || exit 1
+
+check()
+{
+  ./tostring "$1" || exit 1
+}
+
+check 'a'
+check '1'
+check '0'
+check 'a => b'
+check 'G a '
+check 'a U b'
+check 'a & b'
+check 'a & b & c'
+check 'b & a & b'
+check 'b & a & a'
+check 'a & b & (c |(f U g)| e)'
+check 'b & a & a & (c | e |(f U g)| e | c) & b'
+check 'a <=> b'
+check 'a & b & (c |(f U g)| e)'
+check 'b & a & a & (c | e |(g U g)| e | c) & b'
+:

src/ltlvisit/Makefile.am

@@ -9,6 +9,8 @@ libltlvisit_a_SOURCES = \
   dotty.hh \
   dump.cc \
   dump.hh \
+  tostring.cc \
+  tostring.hh \
   equals.cc \
   equals.hh \
   lunabbrev.hh \
@@ -16,4 +18,4 @@ libltlvisit_a_SOURCES = \
   nenoform.hh \
   nenoform.cc \
   tunabbrev.hh \
-  tunabbrev.cc
+  tunabbrev.cc

src/ltlvisit/equals.hh

@@ -43,3 +43,4 @@ namespace spot
     bool equals(const formula* f1, const formula* f2);
   }
 }
+

src/ltlvisit/tostring.cc

@@ -0,0 +1,125 @@
+#include <cassert>
+#include "tostring.hh"
+#include "ltlast/visitor.hh"
+#include "ltlast/allnodes.hh"
+
+
+namespace spot 
+{
+  namespace ltl
+  {
+
+    class to_string_visitor : public spot::ltl::const_visitor
+    {
+    public:
+      to_string_visitor(std::ostream& os = std::cout)
+	: os_(os)
+      {
+      }
+      
+      virtual 
+      ~to_string_visitor()
+      {
+      }
+
+      void 
+      visit(const spot::ltl::atomic_prop* ap)
+      {
+	   os_ << ap->name();
+    
+      }
+
+      void
+      visit(const spot::ltl::constant* c)
+      {
+	os_ << c->val_name();
+      }      
+      
+      void
+      visit(const spot::ltl::binop* bo)
+      {
+	os_ << "(";
+	bo->first()->accept(*this);
+	
+	switch(bo->op())
+	   {
+	      case spot::ltl::binop::Xor:
+	        os_ << " ^ ";
+	      break;
+	      case spot::ltl::binop::Implies:
+	        os_ << " => ";
+	      break;
+	      case spot::ltl::binop::Equiv:
+	        os_ << " <=> ";
+	      break;
+	      case spot::ltl::binop::U:
+	        os_ << " U ";
+	      break;
+	      case spot::ltl::binop::R:
+	        os_ << " R ";
+	      break;
+	   }
+	
+	bo->second()->accept(*this);
+	os_ << ")";
+      }
+      
+      void
+      visit(const spot::ltl::unop* uo)
+      {   
+ 	 switch(uo->op())
+	   {
+	   case spot::ltl::unop::Not:
+	     os_ << "!";
+	     break;
+	   case spot::ltl::unop::X:
+	     os_ << "X";
+	     break;
+	   case spot::ltl::unop::F:
+	     os_ << "F";
+	     break;
+	   case spot::ltl::unop::G:
+	     os_ << "G";
+	       break;
+	   }
+        
+	uo->child()->accept(*this);
+      }
+      
+      void
+      visit(const spot::ltl::multop* mo)
+      {
+	os_ << "(";
+	unsigned max = mo->size();
+	mo->nth(0)->accept(*this);
+	 const char* ch = " ";
+	switch (mo->op())
+	       {
+	          case spot::ltl::multop::Or:
+	            ch = " | ";
+	          break; 
+	          case spot::ltl::multop::And:
+	            ch = " & ";
+	          break;
+	       }
+
+	for (unsigned n = 1; n < max; ++n)
+	  {
+	    os_ << ch;
+	    mo->nth(n)->accept(*this);
+	  }
+	os_ << ")";
+      }
+    private:
+      std::ostream& os_;
+    };
+
+    void 
+    to_string(const formula& f, std::ostream& os)
+    {
+      to_string_visitor v(os);
+      f.accept(v);
+    }
+
+  }
+}

src/ltlvisit/tostring.hh

@@ -0,0 +1,15 @@
+#ifndef SPOT_LTLVISIT_AST2STRING_HH
+# define SPOT_LTLVISIT_AST2STRING_HH
+
+#include <ltlast/formula.hh>
+#include <iostream>
+
+namespace spot 
+{
+  namespace ltl
+  {
+    void to_string(const formula& f, std::ostream& os);
+  }
+}
+
+#endif // SPOT_LTLVISIT_AST2STRING_HH