* HACKING, Makefile.am, configure.ac, m4/gccwarn.m4,

src/Makefile.am, src/ltlast/Makefile.am, src/ltlast/allnodes.hh,
src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc,
src/ltlast/constant.hh, src/ltlast/formulae.hh,
src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/predecl.hh,
src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlast/visitor.hh,
src/ltlparse/Makefile.am, src/ltlparse/ltlparse.yy,
src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
src/ltlparse/public.hh, src/ltlvisit/Makefile.am,
src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh,
src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
src/ltlvisit/rewrite.cc, src/ltlvisit/rewrite.hh,
src/ltltest/Makefile.am, src/ltltest/defs.in, src/ltltest/readltl.cc,
src/ltltest/parse.test, src/ltltest/parseerr.test,
src/misc/Makefile.am, src/misc/const_sel.hh: New files.

src/.cvsignore

@@ -0,0 +1,3 @@
+.deps
+Makefile
+Makefile.in

src/Makefile.am

@@ -0,0 +1,4 @@
+AUTOMAKE_OPTIONS = subdir-objects
+
+# List directories in the order they must be built.
+SUBDIRS = misc ltlast ltlvisit ltlparse ltltest 

src/ltlast/.cvsignore

@@ -0,0 +1,3 @@
+.deps
+Makefile
+Makefile.in

src/ltlast/Makefile.am

@@ -0,0 +1,19 @@
+AM_CPPFLAGS = -I$(srcdir)/..
+AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+
+lib_LIBRARIES = libltlast.a
+libltlast_a_SOURCES = \
+  allnodes.hh \
+  atomic_prop.cc \
+  atomic_prop.hh \
+  binop.cc \
+  binop.hh \
+  constant.cc \
+  constant.hh \
+  formulae.hh \
+  multop.cc \
+  multop.hh \
+  predecl.hh \
+  unop.cc \
+  unop.hh
+

src/ltlast/allnodes.hh

@@ -0,0 +1,10 @@
+#ifndef SPOT_LTLAST_ALLNODES_HH
+# define SPOT_LTLAST_ALLNODES_HH
+
+# include "binop.hh"
+# include "unop.hh"
+# include "multop.hh"
+# include "atomic_prop.hh"
+# include "constant.hh"
+
+#endif // SPOT_LTLAST_ALLNODES_HH

src/ltlast/atomic_prop.cc

@@ -0,0 +1,43 @@
+#include "atomic_prop.hh"
+#include "visitor.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+ 
+    atomic_prop::atomic_prop(std::string name)
+      : name_(name)
+    {
+    }
+
+    atomic_prop::~atomic_prop()
+    {
+    }
+
+    void 
+    atomic_prop::accept(visitor& v)
+    {
+      v.visit(this);
+    }
+    
+    void
+    atomic_prop::accept(const_visitor& v) const
+    {
+      v.visit(this);
+    }   
+
+    bool 
+    atomic_prop::equals(const formulae* f) const
+    {
+      const atomic_prop* p = dynamic_cast<const atomic_prop*>(f);
+      return p && p->name() == name();
+    }
+
+    const std::string&
+    atomic_prop::name() const
+    {
+      return name_;
+    }
+  }
+}

src/ltlast/atomic_prop.hh

@@ -0,0 +1,31 @@
+#ifndef SPOT_LTLAST_ATOMIC_PROP_HH
+# define SPOT_LTLAST_ATOMIC_PROP_HH
+
+#include <string>
+#include "formulae.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    
+    class atomic_prop : public formulae
+    {
+    public:
+      atomic_prop(std::string name);
+      virtual ~atomic_prop();
+
+      virtual void accept(visitor& visitor);
+      virtual void accept(const_visitor& visitor) const;
+
+      virtual bool equals(const formulae* f) const;
+
+      const std::string& name() const;
+    private:
+      std::string name_;
+    };
+
+  }
+}
+
+#endif // SPOT_LTLAST_ATOMICPROP_HH

src/ltlast/binop.cc

@@ -0,0 +1,91 @@
+#include <cassert>
+#include "binop.hh"
+#include "visitor.hh"
+
+namespace spot
+{
+  namespace ltl
+  {    
+    binop::binop(type op, formulae* first, formulae* second)
+      : op_(op), first_(first), second_(second)
+    {
+    }
+
+    binop::~binop()
+    {
+    }
+
+    void
+    binop::accept(visitor& v)
+    {
+      v.visit(this);
+    }
+
+    void
+    binop::accept(const_visitor& v) const
+    {
+      v.visit(this);
+    }
+
+    const formulae*
+    binop::first() const
+    {
+      return first_;
+    }
+
+    formulae*
+    binop::first()
+    {
+      return first_;
+    }
+
+    const formulae*
+    binop::second() const
+    {
+      return second_;
+    }
+
+    formulae* 
+    binop::second()
+    {
+      return second_;
+    }
+
+    bool 
+    binop::equals(const formulae* f) const
+    {
+      const binop* p = dynamic_cast<const binop*>(f);
+      return p && p->op() == op() 
+	&& first()->equals(p->first())
+	&& second()->equals(p->second());
+    }
+
+    binop::type 
+    binop::op() const
+    {
+      return op_;
+    }
+
+    const char* 
+    binop::op_name() const
+    {
+      switch (op_)
+	{
+	case Xor:
+	  return "Xor";
+	case Implies:
+	  return "Implies";
+	case Equiv:
+	  return "Equiv";
+	case U:
+	  return "U";
+	case R:
+	  return "R";
+	}
+      // Unreachable code.
+      assert(0);
+      return 0;
+    }
+
+  }
+}

src/ltlast/binop.hh

@@ -0,0 +1,43 @@
+#ifndef SPOT_LTLAST_BINOP_HH
+# define SPOT_LTLAST_BINOP_HH
+
+#include "formulae.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    
+    class binop : public formulae
+    {
+    public:
+      // And and Or are not here.  Because they
+      // are often nested we represent them as multops.
+      enum type { Xor, Implies, Equiv, U, R };
+
+      binop(type op, formulae* first, formulae* second);
+      virtual ~binop();
+
+      virtual void accept(visitor& v);
+      virtual void accept(const_visitor& v) const;
+
+      virtual bool equals(const formulae* f) const;
+
+      const formulae* first() const;
+      formulae* first();
+      const formulae* second() const;
+      formulae* second();
+
+      type op() const;
+      const char* op_name() const;
+
+    private:
+      type op_;
+      formulae* first_;
+      formulae* second_;
+    };
+
+  }
+}
+
+#endif // SPOT_LTLAST_BINOP_HH

src/ltlast/constant.cc

@@ -0,0 +1,59 @@
+#include "constant.hh"
+#include "visitor.hh"
+#include <cassert>
+
+namespace spot
+{
+  namespace ltl
+  {    
+    constant::constant(type val)
+      : val_(val)
+    {
+    }
+
+    constant::~constant()
+    {
+    }
+
+    void
+    constant::accept(visitor& v)
+    {
+      v.visit(this);
+    }
+
+    void
+    constant::accept(const_visitor& v) const
+    {
+      v.visit(this);
+    }
+
+    bool 
+    constant::equals(const formulae* f) const
+    {
+      const constant* p = dynamic_cast<const constant*>(f);
+      return p && p->val() == val();
+    }
+
+    constant::type 
+    constant::val() const
+    {
+      return val_;
+    }
+
+    const char* 
+    constant::val_name() const
+    {
+      switch (val_)
+	{
+	case True:
+	  return "1";
+	case False:
+	  return "0";
+	}
+      // Unreachable code.
+      assert(0);
+      return 0;
+    }
+
+  }
+}

src/ltlast/constant.hh

@@ -0,0 +1,37 @@
+#ifndef SPOT_LTLAST_CONSTANT_HH
+# define SPOT_LTLAST_CONSTANT_HH
+
+#include "formulae.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    
+    class constant : public formulae
+    {
+    public:
+      enum type { False, True };
+
+      constant(type val);
+      virtual ~constant();
+
+      virtual void accept(visitor& v);
+      virtual void accept(const_visitor& v) const;
+
+      virtual bool equals(const formulae* h) const;
+
+      const formulae* child() const;
+      formulae* child();
+
+      type val() const;
+      const char* val_name() const;
+
+    private:
+      type val_;
+    };
+
+  }
+}
+
+#endif // SPOT_LTLAST_CONSTANT_HH

src/ltlast/formulae.hh

@@ -0,0 +1,25 @@
+#ifndef SPOT_LTLAST_FORMULAE_HH
+# define SPOT_LTLAST_FORMULAE_HH
+
+#include "predecl.hh"
+
+namespace spot 
+{
+  namespace ltl 
+  {
+
+    class formulae 
+    {
+    public:
+      virtual void accept(visitor& v) = 0;
+      virtual void accept(const_visitor& v) const = 0;
+
+      virtual bool equals(const formulae* f) const = 0;
+    };
+
+  }
+}
+
+
+
+#endif // SPOT_LTLAST_FORMULAE_HH

src/ltlast/multop.cc

@@ -0,0 +1,111 @@
+#include <cassert>
+#include <utility>
+#include "multop.hh"
+#include "visitor.hh"
+
+namespace spot
+{
+  namespace ltl
+  {    
+    multop::multop(type op, formulae* first, formulae* second)
+      : op_(op), children_(2)
+    {
+      children_[0] = first;
+      children_[1] = second;
+    }
+    
+    void
+    multop::add(formulae* f)
+    {
+      children_.push_back(f);
+    }
+
+    multop::~multop()
+    {
+    }
+
+    void
+    multop::accept(visitor& v)
+    {
+      v.visit(this);
+    }
+
+    void
+    multop::accept(const_visitor& v) const
+    {
+      v.visit(this);
+    }
+
+    unsigned
+    multop::size() const
+    {
+      return children_.size();
+    }
+
+    const formulae*
+    multop::nth(unsigned n) const
+    {
+      return children_[n];
+    }
+
+    formulae* 
+    multop::nth(unsigned n)
+    {
+      return children_[n];
+    }
+
+    multop::type 
+    multop::op() const
+    {
+      return op_;
+    }
+
+    bool 
+    multop::equals(const formulae* f) const
+    {
+      // This check is a bit more complicated than other checks
+      // because And(a, b, c) is equal to And(c, a, b, a).
+      const multop* p1 = dynamic_cast<const multop*>(f);
+      if (!p1 || p1->op() != op())
+	return false;
+      
+      const multop* p2 = this;
+      unsigned s1 = p1->size();
+      unsigned s2 = p2->size();
+      if (s1 > s2)
+	{
+	  std::swap(s1, s2);
+	  std::swap(p1, p2);
+	}
+      
+      for (unsigned n1 = 0; n1 < s1; ++n1)
+	{
+	  unsigned n2;
+	  for (n2 = 0; n2 < s2; ++n2)
+	    {
+	      if (p1->nth(n1)->equals(p2->nth(n2)))
+		break;
+	    }
+	  if (n2 == s2)
+	    return false;
+	}
+      return true;
+    }
+
+    const char* 
+    multop::op_name() const
+    {
+      switch (op_)
+	{
+	case And:
+	  return "And";
+	case Or:
+	  return "Or";
+	}
+      // Unreachable code.
+      assert(0);
+      return 0;
+    }
+
+  }
+}

src/ltlast/multop.hh

@@ -0,0 +1,44 @@
+#ifndef SPOT_LTLAST_MULTOP_HH
+# define SPOT_LTLAST_MULTOP_HH
+
+#include <vector>
+#include "formulae.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    
+    class multop : public formulae
+    {
+    public:
+      enum type { Or, And };
+
+      // A multop has at least two arguments.
+      multop(type op, formulae* first, formulae* second);
+      // More argument can be added.
+      void add(formulae* f);
+      
+      virtual ~multop();
+
+      virtual void accept(visitor& v);
+      virtual void accept(const_visitor& v) const;
+
+      virtual bool equals(const formulae* f) const;
+
+      unsigned size() const;
+      const formulae* nth(unsigned n) const;
+      formulae* nth(unsigned n);
+
+      type op() const;
+      const char* op_name() const;
+
+    private:
+      type op_;
+      std::vector<formulae*> children_;
+    };
+
+  }
+}
+
+#endif // SPOT_LTLAST_MULTOP_HH

src/ltlast/predecl.hh

@@ -0,0 +1,18 @@
+#ifndef SPOT_LTLAST_PREDECL_HH
+# define SPOT_LTLAST_PREDECL_HH
+
+namespace spot {
+  namespace ltl {
+    struct visitor;
+    struct const_visitor;
+
+    struct atomic_prop;
+    struct unop;
+    struct constant;
+    struct binop;
+    struct formulae;
+    struct multop;
+  }
+}
+
+#endif // SPOT_LTLAST_PREDECL_HH

src/ltlast/unop.cc

@@ -0,0 +1,75 @@
+#include "unop.hh"
+#include "visitor.hh"
+#include <cassert>
+
+namespace spot
+{
+  namespace ltl
+  {    
+    unop::unop(type op, formulae* child)
+      : op_(op), child_(child)
+    {
+    }
+
+    unop::~unop()
+    {
+    }
+
+    void
+    unop::accept(visitor& v)
+    {
+      v.visit(this);
+    }
+
+    void
+    unop::accept(const_visitor& v) const
+    {
+      v.visit(this);
+    }
+
+    const formulae*
+    unop::child() const
+    {
+      return child_;
+    }
+
+    formulae*
+    unop::child()
+    {
+      return child_;
+    }
+
+    bool 
+    unop::equals(const formulae* f) const
+    {
+      const unop* p = dynamic_cast<const unop*>(f);
+      return p && p->op() == op() && child()->equals(p->child());
+    }
+
+    unop::type 
+    unop::op() const
+    {
+      return op_;
+    }
+
+    const char* 
+    unop::op_name() const
+    {
+      switch (op_)
+	{
+	case Not:
+	  return "Not";
+	case X:
+	  return "X";
+	case F:
+	  return "F";
+	case G:
+	  return "G";
+	}
+      // Unreachable code.
+      assert(0);
+      return 0;
+    }
+
+  }
+}

src/ltlast/unop.hh

@@ -0,0 +1,38 @@
+#ifndef SPOT_LTLAST_UNOP_HH
+# define SPOT_LTLAST_UNOP_HH
+
+#include "formulae.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    
+    class unop : public formulae
+    {
+    public:
+      enum type { Not, X, F, G };
+
+      unop(type op, formulae* child);
+      virtual ~unop();
+
+      virtual void accept(visitor& v);
+      virtual void accept(const_visitor& v) const;
+
+      virtual bool equals(const formulae* h) const;
+
+      const formulae* child() const;
+      formulae* child();
+
+      type op() const;
+      const char* op_name() const;
+
+    private:
+      type op_;
+      formulae* child_;
+    };
+
+  }
+}
+
+#endif // SPOT_LTLAST_UNOP_HH

src/ltlast/visitor.hh

@@ -0,0 +1,32 @@
+#ifndef SPOT_LTLAST_VISITOR_HH
+# define SPOT_LTLAST_VISITOR_HH
+
+#include "predecl.hh"
+#include "misc/const_sel.hh"
+
+namespace spot {
+  namespace ltl {
+    
+    template <bool WantConst>
+    struct generic_visitor
+    {
+      virtual void visit(typename const_sel<atomic_prop, WantConst>::t* node) 
+	= 0;
+
+      virtual void visit(typename const_sel<constant, WantConst>::t* node) 
+	= 0;
+
+      virtual void visit(typename const_sel<binop, WantConst>::t* node) = 0;
+      
+      virtual void visit(typename const_sel<unop, WantConst>::t* node) = 0;
+
+      virtual void visit(typename const_sel<multop, WantConst>::t* node) = 0;
+    };
+
+    struct visitor : public generic_visitor<false> {};
+    struct const_visitor : public generic_visitor<true> {};
+
+  }
+}
+
+#endif // SPOT_LTLAST_VISITOR_HH

src/ltlparse/.cvsignore

@@ -0,0 +1,11 @@
+.deps
+Makefile
+Makefile.in
+location.hh
+ltlparse.cc
+ltlparse.hh
+ltlparse.output
+ltlscan.cc
+position.hh
+readltl
+stack.hh

src/ltlparse/Makefile.am

@@ -0,0 +1,27 @@
+AM_CPPFLAGS = -I$(srcdir)/..
+
+lib_LIBRARIES = libltlparse.a
+
+LTLPARSE_YY = ltlparse.yy
+FROM_LTLPARSE_YY_MAIN = ltlparse.cc
+FROM_LTLPARSE_YY_OTHERS = \
+  stack.hh \
+  position.hh \
+  location.hh \
+  ltlparse.hh
+FROM_LTLPARSE_YY = $(FROM_LTLPARSE_YY_MAIN) $(FROM_LTLPARSE_YY_OTHERS)
+
+BUILT_SOURCES = $(FROM_LTLPARSE_YY)
+MAINTAINERCLEANFILES = $(FROM_LTLPARSE_YY)
+
+$(FROM_LTLPARSE_YY_MAIN): $(srcdir)/$(LTLPARSE_YY)
+	bison --defines --locations --skeleton=lalr1.cc --report=all \
+	  $(srcdir)/$(LTLPARSE_YY) -o $@
+$(FROM_LTLPARSE_YY_OTHERS): $(LTLPARSE_YY)
+	@test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_LTLPARSE_YY_MAIN)
+
+libltlparse_a_SOURCES = \
+  $(FROM_LTLPARSE_YY) \
+  ltlscan.ll \
+  parsedecl.hh \
+  public.hh

src/ltlparse/ltlparse.yy

@@ -0,0 +1,183 @@
+%{
+#include <string>
+#include "public.hh"
+#include "ltlast/allnodes.hh"
+
+extern spot::ltl::formulae* result;
+
+%}
+
+%debug
+%error-verbose
+%union
+{
+  int token;
+  std::string* str;
+  spot::ltl::formulae* ltl;
+}
+
+%{
+/* Spotparse.hh and parsedecl.hh include each other recursively.
+   We mut ensure that YYSTYPE is declared (by the above %union)
+   before parsedecl.hh uses it. */
+#include "parsedecl.hh"
+using namespace spot::ltl;
+
+// At the time of writing C++ support in Bison is quite
+// new and there is still no way to pass error_list to
+// the parser.  We use a global variable instead.
+namespace spot
+{
+  namespace ltl
+  {
+    extern parse_error_list* error_list;
+  }
+}
+%}
+
+/* Logical operators.  */
+%left <token> OP_AND OP_XOR OP_OR
+%left <token> OP_IMPLIES OP_EQUIV
+
+/* LTL operators.  */
+%left <token> OP_U OP_R
+%nonassoc <token> OP_F OP_G
+%nonassoc <token> OP_X
+
+/* Not has the most important priority.  */
+%nonassoc <token> OP_NOT
+
+/* Grouping (parentheses).  */
+%token <token> PAR_OPEN PAR_CLOSE
+
+/* Atomic proposition.  */
+%token <str> ATOMIC_PROP
+
+/* Constants */
+%token CONST_TRUE 
+%token CONST_FALSE
+%token END_OF_INPUT
+
+%type <ltl> result ltl_formulae subformulae
+
+%%
+result:       ltl_formulae END_OF_INPUT
+              { result = $$ = $1; 
+		YYACCEPT;
+	      }
+	    | many_errors END_OF_INPUT
+              { error_list->push_back(parse_error(@1,
+				      "couldn't parse anything sensible")); 
+	        result = $$ = 0;
+		YYABORT;
+	      }
+	    | END_OF_INPUT
+              { error_list->push_back(parse_error(@1,
+				      "empty input")); 
+	        result = $$ = 0;
+		YYABORT;
+	      }
+
+many_errors_diagnosed : many_errors 
+              { error_list->push_back(parse_error(@1, 
+				     "unexpected input ignored")); }
+
+ltl_formulae: subformulae
+              { $$ = $1; }
+	    | many_errors_diagnosed subformulae
+              { $$ = $2; }
+	    | ltl_formulae many_errors_diagnosed
+              { $$ = $1; }
+
+many_errors: error
+	    | many_errors error
+
+subformulae: ATOMIC_PROP
+	      { $$ = new atomic_prop(*$1); delete $1; }
+	    | CONST_TRUE
+              { $$ = new constant(constant::True); }
+	    | CONST_FALSE
+              { $$ = new constant(constant::False); }
+	    | PAR_OPEN subformulae PAR_CLOSE
+	      { $$ = $2; }
+	    | PAR_OPEN error PAR_CLOSE
+              { error_list->push_back(parse_error(@$, 
+                 "treating this parenthetical block as false")); 
+	        $$ = new constant(constant::False);
+	      }
+	    | PAR_OPEN subformulae many_errors PAR_CLOSE
+              { error_list->push_back(parse_error(@3, 
+				      "unexpected input ignored")); 
+	        $$ = $2;
+	      }
+	    | OP_NOT subformulae
+	      { $$ = new unop(unop::Not, $2); }
+            | subformulae OP_AND subformulae
+	      { $$ = new multop(multop::And, $1, $3); }
+	    | subformulae OP_OR subformulae
+	      { $$ = new multop(multop::Or, $1, $3); }
+	    | subformulae OP_XOR subformulae
+	      { $$ = new binop(binop::Xor, $1, $3); }
+	    | subformulae OP_IMPLIES subformulae
+	      { $$ = new binop(binop::Implies, $1, $3); }
+            | subformulae OP_EQUIV subformulae
+	      { $$ = new binop(binop::Equiv, $1, $3); }
+            | subformulae OP_U subformulae
+	      { $$ = new binop(binop::U, $1, $3); }
+            | subformulae OP_R subformulae
+	      { $$ = new binop(binop::R, $1, $3); }
+            | OP_F subformulae
+	      { $$ = new unop(unop::F, $2); }
+            | OP_G subformulae
+	      { $$ = new unop(unop::G, $2); }
+            | OP_X subformulae
+	      { $$ = new unop(unop::X, $2); }
+//	    | subformulae many_errors
+//              { error_list->push_back(parse_error(@2, 
+//		  "ignoring these unexpected trailing tokens")); 
+//	        $$ = $1;
+//	      }
+	    
+;
+
+%%
+
+void
+yy::Parser::print_()
+{
+  if (looka_ == ATOMIC_PROP) 
+    YYCDEBUG << " '" << *value.str << "'";
+}
+
+void
+yy::Parser::error_()
+{
+  error_list->push_back(parse_error(location, message));
+}
+
+formulae* result = 0;
+
+namespace spot
+{
+  namespace ltl
+  {
+    parse_error_list* error_list;
+
+    formulae*
+    parse(const std::string& ltl_string, 
+	  parse_error_list& error_list,
+	  bool debug)
+    {
+      result = 0;
+      ltl::error_list = &error_list;
+      flex_set_buffer(ltl_string.c_str());
+      yy::Parser parser(debug, yy::Location());
+      parser.parse();  
+      return result;
+    }
+  }
+}
+
+// Local Variables:
+// mode: c++
+// End:

src/ltlparse/ltlscan.ll

@@ -0,0 +1,71 @@
+%option noyywrap
+
+%{
+#include <string>
+#include "parsedecl.hh"
+
+/* Hack Flex so we read from a string instead of reading from a file.  */
+# define YY_INPUT(buf, result, max_size)				\
+  do {									\
+    result = (max_size < to_parse_size) ? max_size : to_parse_size;	\
+    memcpy(buf, to_parse, result);					\
+    to_parse_size -= result;						\
+    to_parse += result;							\
+  } while (0);
+
+#define YY_USER_ACTION \
+    yylloc->columns (yyleng);
+
+static const char *to_parse = 0;
+static int to_parse_size = 0;
+  
+void
+flex_set_buffer(const char *buf)
+{
+  to_parse = buf;
+  to_parse_size = strlen(to_parse);
+}
+
+%}
+
+%%
+
+%{
+  yylloc->step ();
+%}
+
+"("		return PAR_OPEN;
+")"		return PAR_CLOSE;
+
+"!"		return OP_NOT;
+"|"|"+"		return OP_OR;
+"&"|"."|"*"	return OP_AND;
+"^"		return OP_XOR;
+"=>"|"->"	return OP_IMPLIES;
+"<=>"|"<->"	return OP_EQUIV;
+
+  /* <>, [], and () are used in Spin.  */
+"F"|"<>"	return OP_F;
+"G"|"[]"	return OP_G;
+"U"		return OP_U;
+"R"|"V"		return OP_R;
+"X"|"()"	return OP_X;
+
+"1"|"true"	return CONST_TRUE;
+"0"|"false"	return CONST_FALSE;
+
+[ \t\n]+	yylloc->step (); /* discard whitespace */
+
+  /* An Atomic propisition cannot start with the letter
+     used by a unary operator (F,G,X), unless this
+     letter is followed by a digit in which case we assume
+     it's an ATOMIC_PROP (even though F0 could be seen as Ffalse).  */
+[a-zA-EH-WYZ_][a-zA-Z0-9_]* | 
+[FGX][0-9_][a-zA-Z0-9_]* { 
+		  yylval->str = new std::string(yytext); 
+	          return ATOMIC_PROP;
+		}
+
+.		return *yytext;
+
+<<EOF>>		return END_OF_INPUT;

src/ltlparse/parsedecl.hh

@@ -0,0 +1,14 @@
+#ifndef SPOT_LTLPARSE_PARSEDECL_HH
+# define SPOT_LTLPARSE_PARSEDECL_HH
+
+#include "ltlparse.hh"
+#include "location.hh"
+
+# define YY_DECL \
+  int yylex (yystype *yylval, yy::Location *yylloc)
+YY_DECL;
+
+void flex_set_buffer(const char *buf);
+
+#endif // SPOT_LTLPARSE_PARSEDECL_HH
+

src/ltlparse/public.hh

@@ -0,0 +1,24 @@
+#ifndef SPOT_LTLPARSE_PUBLIC_HH
+# define SPOT_LTLPARSE_PUBLIC_HH
+
+# include <string>
+# include "ltlast/formulae.hh"
+# include "location.hh"
+# include <list>
+# include <utility>
+
+namespace spot 
+{
+  namespace ltl
+  {
+    typedef std::pair<yy::Location, std::string> parse_error;
+    typedef std::list<parse_error> parse_error_list;
+
+    // Beware: this function is *not* reentrant.
+    formulae* parse(const std::string& ltl_string, 
+		    parse_error_list& error_list,
+		    bool debug = false);
+  }
+}
+
+#endif // SPOT_LTLPARSE_PUBLIC_HH

src/ltltest/.cvsignore

@@ -0,0 +1,9 @@
+Makefile
+Makefile.in
+.deps
+ltl2dot
+ltl2text
+stdout
+parser.dot
+expect
+defs

src/ltltest/Makefile.am

@@ -0,0 +1,15 @@
+AM_CPPFLAGS = -I$(srcdir)/..
+LDADD = ../ltlparse/libltlparse.a \
+        ../ltlvisit/libltlvisit.a \
+        ../ltlast/libltlast.a 
+
+check_SCRIPTS = defs
+check_PROGRAMS = ltl2dot ltl2text
+ltl2dot_SOURCES = readltl.cc
+ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
+ltl2text_SOURCES = readltl.cc
+
+EXTRA_DIST = $(TESTS)
+TESTS = parse.test parseerr.test
+
+CLEANFILES = stdout expect parse.dot

src/ltltest/defs.in

@@ -0,0 +1,35 @@
+# -*- shell-script -*-
+
+# Ensure we are running from the right directory.
+test -f ./defs || {
+   echo "defs: not found in current directory" 1>&2
+   exit 1
+}
+
+# If srcdir is not set, then we are not running from `make check', be verbose.
+if test -z "$srcdir"; then
+   test -z "$VERBOSE" && VERBOSE=x
+   # compute $srcdir.
+   srcdir=`echo "$0" | sed -e 's,/[^\\/]*$,,'`
+   test $srcdir = $0 && srcdir=.
+fi
+
+# Ensure $srcdir is set correctly.
+test -f $srcdir/defs.in || {
+   echo "$srcdir/defs.in not found, check \$srcdir" 1>&2
+   exit 1
+}
+
+# User can set VERBOSE to see all output.
+test -z "$VERBOSE" && exec >/dev/null 2>&1
+
+echo "== Running test $0"
+
+DOT='@DOT@'
+
+# Turn on shell traces when VERBOSE=x.
+if test "x$VERBOSE" = xx; then
+  set -x
+else
+  :
+fi

src/ltltest/parse.test

@@ -0,0 +1,64 @@
+#! /bin/sh
+
+# Check that spot::ltl::parse succeed on valid input, and that
+# dump and dotty will work with the resulting trees.  Note that
+# this doesn't check that the tree is correct w.r.t. the formula.
+
+. ./defs || exit 1
+
+for f in \
+  '0' \
+  '1' \
+  'true' \
+  'false' \
+  'a' \
+  'p11011' \
+  '(p11011)' \
+  'a & b' \
+  'a * _b12' \
+  'a . b' \
+  'a + b' \
+  'a3214 | b' \
+  'a & b' \
+  '_a_ U b' \
+  'a R b' \
+  'a <=> b' \
+  'a <-> b' \
+  'a ^ b' \
+  'a => b' \
+  'a -> b' \
+  'F b' \
+  'Gb' \
+  'G(b)' \
+  '!G(!b)' \
+  '!b' \
+  '[]b' \
+  '<>b' \
+  'X b' \
+  '()b' \
+  'long_atomic_proposition_1 U long_atomic_proposition_2' \
+  '  ab & ac | ad ^ af' \
+  '(ab & ac | ad ) <=> af ' \
+  'a U b U c U d U e U f U g U h U i U j U k U l U m' \
+  '(ab * !Xad + ad U ab) & FG p12 & GF p13' \
+  '((([]<>()p12))   )' \
+  'a R ome V anille'
+do
+  if ./ltl2text "$f"; then
+    :
+  else
+    echo "ltl2dot failed to parse '$f'"
+    exit 1
+  fi
+
+  if test -n "$DOT"; then
+    ./ltl2dot "$f" > parse.dot 
+    if $DOT -o /dev/null parse.dot; then
+      rm -f parse.dot
+    else
+      rm -f parse.dot
+      echo "dot failed to parse ltl2dot output for '$f'"
+      exit 1
+    fi
+  fi
+done

src/ltltest/parseerr.test

@@ -0,0 +1,47 @@
+#! /bin/sh
+
+# Check error recovery in parsing.  This also check how the
+# resulting tree looks like.
+
+. ./defs || exit 1
+
+check()
+{
+  if ./ltl2text "$1" >stdout; then
+    echo "ltl2text unexpectedly parsed '$1' successfully"
+    rm -f stdout
+    exit 1
+  else
+    if test -n "$2"; then
+      echo "$2" >expect
+    else
+      : >expect
+    fi
+    if cmp stdout expect; then
+      :
+    else
+      echo "'$1' parsed as"
+      cat stdout
+      echo "instead of"
+      cat expect
+      rm -f stdout expect
+      exit 1
+    fi
+  fi
+}
+
+# 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))'
+
+# 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))'
+check 'a U ((c) U e) R (<=> f g)' \
+      'binop(R, binop(U, AP(a), binop(U, AP(c), AP(e))), constant(0))'

src/ltltest/readltl.cc

@@ -0,0 +1,69 @@
+#include <iostream>
+#include "ltlparse/public.hh"
+#include "ltlvisit/dump.hh"
+#include "ltlvisit/dotty.hh"
+
+void
+syntax(char *prog)
+{
+  std::cerr << prog << " [-d] formulae" << std::endl;
+  exit(2);
+}
+
+int
+main(int argc, char **argv)
+{
+  int exit_code = 0;
+
+  if (argc < 2)
+    syntax(argv[0]);
+
+  bool debug = false;
+  int formulae_index = 1;
+
+  if (!strcmp(argv[1], "-d"))
+    {
+      debug = true;
+      if (argc < 3)
+	syntax(argv[0]);
+      formulae_index = 2;
+    }    
+  
+  spot::ltl::parse_error_list pel;
+  spot::ltl::formulae *f = spot::ltl::parse(argv[formulae_index], 
+					    pel, debug);
+
+  spot::ltl::parse_error_list::iterator it;
+  for (it = pel.begin(); it != pel.end(); ++it)
+    {
+      std::cerr << ">>> " << argv[formulae_index] << 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;
+      exit_code = 1;
+    }
+
+  if (f)
+    {
+#ifdef DOTTY
+      spot::ltl::dotty(*f, std::cout);
+#else
+      spot::ltl::dump(*f, std::cout);
+      std::cout << std::endl;
+#endif
+      delete f;
+    }
+  else
+    {
+      exit_code = 1;
+    }
+    
+  return exit_code;
+}

src/ltlvisit/.cvsignore

@@ -0,0 +1,3 @@
+.deps
+Makefile
+Makefile.in

src/ltlvisit/Makefile.am

@@ -0,0 +1,9 @@
+AM_CPPFLAGS = -I$(srcdir)/..
+AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+
+lib_LIBRARIES = libltlvisit.a
+libltlvisit_a_SOURCES = \
+  dotty.cc \
+  dotty.hh \
+  dump.cc \
+  dump.hh 

src/ltlvisit/dotty.cc

@@ -0,0 +1,107 @@
+#include "dotty.hh"
+#include "ltlast/visitor.hh"
+#include "ltlast/allnodes.hh"
+
+
+namespace spot 
+{
+  namespace ltl
+  {
+
+    class dotty_visitor : public spot::ltl::const_visitor
+    {
+    public:
+      dotty_visitor(std::ostream& os = std::cout)
+	: os_(os), label_("i")
+      {
+      }
+
+      virtual 
+      ~dotty_visitor()
+      {
+      }
+
+      void 
+      visit(const spot::ltl::atomic_prop* ap)
+      {
+	draw_node_(ap->name());
+      }
+
+      void
+      visit(const spot::ltl::constant* c)
+      {
+	draw_node_(c->val_name());
+      }
+      
+      void
+      visit(const spot::ltl::binop* bo)
+      {
+	draw_rec_node_(bo->op_name());
+	std::string label = label_;
+	
+	label_ += "l";
+	draw_link_(label, label_);
+	bo->first()->accept(*this);
+	label_ = draw_link_(label, label + "r");
+	bo->second()->accept(*this);
+      }
+      
+      void
+      visit(const spot::ltl::unop* uo)
+      {
+	draw_rec_node_(uo->op_name());
+	label_ = draw_link_(label_, label_ + "c");
+	uo->child()->accept(*this);
+      }
+      
+      void
+      visit(const spot::ltl::multop* mo)
+      {
+	draw_rec_node_(mo->op_name());
+
+	unsigned max = mo->size();
+	std::string label = label_;
+	for (unsigned n = 0; n < max; ++n)
+	  {
+	    // FIXME: use `n' as a string for label names.
+	    label_ = draw_link_(label, label_ + "m");
+	    mo->nth(n)->accept(*this);
+	  }
+      }
+    private:
+      std::ostream& os_;
+      std::string label_;
+
+      const std::string&
+      draw_link_(const std::string& in, const std::string& out)
+      {
+	os_ << "  " << in << " -> " << out << ";" << std::endl;
+	return out;
+      }
+
+      void 
+      draw_rec_node_(const char* str) const
+      {
+	os_ << "  " << label_ << " [label=\"" << str << "\", shabe=box];" 
+	    << std::endl;
+      }
+
+      void
+      draw_node_(const std::string& str) const
+      {
+	os_ << "  " << label_ << " [label=\"" << str << "\"];" << std::endl;
+      }
+      
+    };
+
+    void 
+    dotty(const formulae& f, std::ostream& os)
+    {
+      dotty_visitor v(os);
+      os << "digraph G {" << std::endl;
+      f.accept(v);
+      os << "}" << std::endl;
+    }
+
+  }
+}

src/ltlvisit/dotty.hh

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

src/ltlvisit/dump.cc

@@ -0,0 +1,79 @@
+#include "dump.hh"
+#include "ltlast/visitor.hh"
+#include "ltlast/allnodes.hh"
+
+
+namespace spot 
+{
+  namespace ltl
+  {
+
+    class dump_visitor : public spot::ltl::const_visitor
+    {
+    public:
+      dump_visitor(std::ostream& os = std::cout)
+	: os_(os)
+      {
+      }
+      
+      virtual 
+      ~dump_visitor()
+      {
+      }
+
+      void 
+      visit(const spot::ltl::atomic_prop* ap)
+      {
+	os_ << "AP(" << ap->name() << ")";
+      }
+
+      void
+      visit(const spot::ltl::constant* c)
+      {
+	os_ << "constant(" << c->val_name() << ")";
+      }      
+      
+      void
+      visit(const spot::ltl::binop* bo)
+      {
+	os_ << "binop(" << bo->op_name() << ", ";
+	bo->first()->accept(*this);
+	os_ << ", ";
+	bo->second()->accept(*this);
+	os_ << ")";
+      }
+      
+      void
+      visit(const spot::ltl::unop* uo)
+      {
+	os_ << "unop(" << uo->op_name() << ", ";
+	uo->child()->accept(*this);
+	os_ << ")";
+      }
+      
+      void
+      visit(const spot::ltl::multop* mo)
+      {
+	os_ << "multop(" << mo->op_name() << ", ";
+	unsigned max = mo->size();
+	mo->nth(0)->accept(*this);
+	for (unsigned n = 1; n < max; ++n)
+	  {
+	    std::cout << ", ";
+	    mo->nth(n)->accept(*this);
+	  }
+	os_ << ")";
+      }
+    private:
+      std::ostream& os_;
+    };
+
+    void 
+    dump(const formulae& f, std::ostream& os)
+    {
+      dump_visitor v(os);
+      f.accept(v);
+    }
+
+  }
+}

src/ltlvisit/dump.hh

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

src/misc/.cvsignore

@@ -0,0 +1,3 @@
+Makefile
+Makefile.in
+.deps

src/misc/Makefile.am

@@ -0,0 +1,2 @@
+
+include_HEADERS = const_sel.hh

src/misc/const_sel.hh

@@ -0,0 +1,28 @@
+#ifndef SPOT_MISC_CONSTSEL_HH
+# define SPOT_MISC_CONSTSEL_HH
+
+namespace spot 
+{
+  // Be default, define the type as-is.
+  template <class T, bool WantConst>
+  struct const_sel
+  {
+    typedef T t;
+  };
+  
+  // If const is wanted, add it.
+  template <class T>
+  struct const_sel<T, true>
+  {
+    typedef const T t;
+  };
+  
+  // If const is present but isn't wanted, remove it.
+  template <class T>
+  struct const_sel<const T, false>
+  {
+    typedef const T t;
+  };
+}
+
+#endif // SPOT_MISC_CONSTSEL_HH