diff --git a/.cvsignore b/.cvsignore new file mode 100644 index 000000000..72c96115e --- /dev/null +++ b/.cvsignore @@ -0,0 +1,7 @@ +Makefile +Makefile.in +configure +config.log +config.status +aclocal.m4 +autom4te.cache diff --git a/ChangeLog b/ChangeLog new file mode 100644 index 000000000..5ff0dad63 --- /dev/null +++ b/ChangeLog @@ -0,0 +1,18 @@ +2003-04-15 Alexandre DURET-LUTZ + + * 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. diff --git a/HACKING b/HACKING new file mode 100644 index 000000000..c4323725f --- /dev/null +++ b/HACKING @@ -0,0 +1,196 @@ +Bootstraping: +============= + +Some files in SPOT's source tree are generated. They are distributed +so that users do not need to tools to rebuild them, but we don't keep +all of them under CVS because it can generate lots of changes or +conflicts. + +Here are the tools you need to bootstrap the CVS tree, or more +generally if you plan to regenerate some of the generated files. + + GNU Autoconf 2.57 + GNU Automake 1.7.3 + GNU Flex (the version probably doesn't matter much, we used 2.5.4) + The CVS version of GNU Bison (called 1.875b at the time of writing) + +Bootstrap the CVS tree by running + + autoreconf -vfi + +and then go on with the usual + + ./configure + make + +Coding conventions: +=================== + +Here are the conventions we follow in Spot, so that the code looks +homogeneous. + +Comments +-------- + + * The language to use is American. + + * When comments are sentences, they should start with a capital and + end with a dot. Dots that end sentences should be followed by two + spaces (i.e., American typing convention), like in this paragraph. + +Formating +--------- + + * Braces on their own line. + + * Text within braces is two-space indented. + + { + f(12); + + } + + * Anything after a control statement is two-space indented. This + includes braces. + + if (test) + { + f(123); + while (test2) + g(456); + } + + * Braces from function/structure/enum/classe/namespace definitions + are not indented. + + class foo + { + public: + Foo(); + protected: + static int get_mumble(); + }; + + * The above corresponds to the `gnu' indentation style under Emacs. + + * Put return types or linkage specifiers on their own line in + function/method _definitions_ : + + static int + Foo::get_mumble() + { + return 2; + } + + This makes it easier to grep functions in the code. + + Function/method declarations can be put on one line. + + * Space before parentheses in control statements + + if (test) + { + do + { + something(); + } + while (0); + } + + * No space before parentheses in function calls. + (`some()->foo()->bar()' is far more readable than + `some ()->foo ()->bar ()' is) + + * No space after opening or before closing parentheses, however + put a space after commas (as in english). + + func(arg1, arg2, arg3); + + * No useless parentheses in return statements. + + return 2; (not `return (2);') + + + * Spaces around infix binary or ternary operators: + + 2 + 2; + a = b; + a <<= (3 + 5) * 3 + f(67 + (really ? 45 : 0)); + + * No space after prefix unary operators, or befor postfix unary operators: + + if (!test && y++ != 0) + { + ++x; + } + + * When an expression spans over several lines, split it before + operators. If it's inside a parenthesis, the following lines + should be 1-indented w.r.t. the opening parenthesis. + + if (foo_this_is_long && bar > win(x, y, z) + && !remaining_condition) + { + ... + } + + * If a line takes more than 80 columns, split it or rethink it. + +Naming +====== + + * Functions, methods, types, classes, etc. are named with lowercase + letters, using an underscore to separate words. + + int compute_this_and_that(); + + class this_is_a_class; + + typedef int int_array[]; + + That is the style used in STL. + + * private members end with an underscore. + + class my_class + { + public: + ... + int get_val() const; + private: + int name_; + }; + + * Identifiers (even internal) starting with `_' are best avoided + to limit clashes with system definitions. + + * Template arguments use capitalized name, with joined words. + + template + class foo + { + ... + }; + + * Enum mumblers also use capitalized name, with joined words. + + * C Macros are all uppercase. + + * Pointers and references are part of the type, and should be put + near the type, not near the variable. + + int* p; // not `int *p;' + list& l; // not `list &l;' + void* magic(); // not `void *magic();' + + * Do not declare many variables on one line. + Use + int* p; + int* q; + instead of + int *p, *q; + The former declarations also allow you to describe each variable. + + * The include guard for src/somedir/foo.hh is + SPOT_SOMEDIR_FOO_HH + diff --git a/Makefile.am b/Makefile.am new file mode 100644 index 000000000..d0716beeb --- /dev/null +++ b/Makefile.am @@ -0,0 +1,3 @@ +SUBDIRS = src +ACLOCAL_AMFLAGS = -I m4 +EXTRA_DIST = m4/gccwarn.m4 \ No newline at end of file diff --git a/configure.ac b/configure.ac new file mode 100644 index 000000000..9ba463d70 --- /dev/null +++ b/configure.ac @@ -0,0 +1,28 @@ +AC_PREREQ([2.57]) +AC_INIT([spot], [0.1]) +AC_CONFIG_AUX_DIR([tools]) +AM_INIT_AUTOMAKE([foreign 1.7.3]) + +AC_PROG_CXX + +AC_PROG_RANLIB +AM_PROG_LEX +AC_PROG_YACC + +AC_LANG(C++) + +CF_GXX_WARNINGS + +AC_CHECK_PROG([DOT], [dot], [dot]) + +AC_CONFIG_FILES([ + Makefile + src/Makefile + src/ltlast/Makefile + src/ltlparse/Makefile + src/ltltest/Makefile + src/ltltest/defs + src/ltlvisit/Makefile + src/misc/Makefile +]) +AC_OUTPUT \ No newline at end of file diff --git a/m4/gccwarn.m4 b/m4/gccwarn.m4 new file mode 100644 index 000000000..878d614da --- /dev/null +++ b/m4/gccwarn.m4 @@ -0,0 +1,46 @@ +dnl Check if the compiler supports useful warning options. There's a few that +dnl we don't use, simply because they're too noisy: +dnl +dnl -ansi (prevents declaration of functions like strdup, and because +dnl it makes warning in system headers). +dnl -Wconversion (useful in older versions of gcc, but not in gcc 2.7.x) +dnl -Wtraditional (combines too many unrelated messages, only a few useful) +dnl -Wredundant-decls (system headers make this too noisy) +dnl -pedantic +dnl -Wunreachable-code (broken, see GCC PR/7827) +dnl -Wredundant-decls (too many warnings in GLIBC's header with old GCC) +dnl +dnl A few other options have been left out because they are annoying in C++. + + +AC_DEFUN([CF_GXX_WARNINGS], +[if test -n "$GXX"; then + AC_CACHE_CHECK([for g++ warning options], ac_cv_prog_gxx_warn_flags, + [ + cat > conftest.$ac_ext <(f); + return p && p->name() == name(); + } + + const std::string& + atomic_prop::name() const + { + return name_; + } + } +} diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh new file mode 100644 index 000000000..fc915d4d3 --- /dev/null +++ b/src/ltlast/atomic_prop.hh @@ -0,0 +1,31 @@ +#ifndef SPOT_LTLAST_ATOMIC_PROP_HH +# define SPOT_LTLAST_ATOMIC_PROP_HH + +#include +#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 diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc new file mode 100644 index 000000000..993aaf816 --- /dev/null +++ b/src/ltlast/binop.cc @@ -0,0 +1,91 @@ +#include +#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(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; + } + + } +} diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh new file mode 100644 index 000000000..c621c7155 --- /dev/null +++ b/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 diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc new file mode 100644 index 000000000..27c4927e3 --- /dev/null +++ b/src/ltlast/constant.cc @@ -0,0 +1,59 @@ +#include "constant.hh" +#include "visitor.hh" +#include + +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(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; + } + + } +} diff --git a/src/ltlast/constant.hh b/src/ltlast/constant.hh new file mode 100644 index 000000000..60c7cd010 --- /dev/null +++ b/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 diff --git a/src/ltlast/formulae.hh b/src/ltlast/formulae.hh new file mode 100644 index 000000000..d329f6811 --- /dev/null +++ b/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 diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc new file mode 100644 index 000000000..3f74646b6 --- /dev/null +++ b/src/ltlast/multop.cc @@ -0,0 +1,111 @@ +#include +#include +#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(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; + } + + } +} diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh new file mode 100644 index 000000000..16409d46e --- /dev/null +++ b/src/ltlast/multop.hh @@ -0,0 +1,44 @@ +#ifndef SPOT_LTLAST_MULTOP_HH +# define SPOT_LTLAST_MULTOP_HH + +#include +#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 children_; + }; + + } +} + +#endif // SPOT_LTLAST_MULTOP_HH diff --git a/src/ltlast/predecl.hh b/src/ltlast/predecl.hh new file mode 100644 index 000000000..8dfb679a6 --- /dev/null +++ b/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 diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc new file mode 100644 index 000000000..975aecc75 --- /dev/null +++ b/src/ltlast/unop.cc @@ -0,0 +1,75 @@ +#include "unop.hh" +#include "visitor.hh" +#include + +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(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; + } + + } +} diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh new file mode 100644 index 000000000..cee1f4f89 --- /dev/null +++ b/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 diff --git a/src/ltlast/visitor.hh b/src/ltlast/visitor.hh new file mode 100644 index 000000000..672fa38fe --- /dev/null +++ b/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 + struct generic_visitor + { + virtual void visit(typename const_sel::t* node) + = 0; + + virtual void visit(typename const_sel::t* node) + = 0; + + virtual void visit(typename const_sel::t* node) = 0; + + virtual void visit(typename const_sel::t* node) = 0; + + virtual void visit(typename const_sel::t* node) = 0; + }; + + struct visitor : public generic_visitor {}; + struct const_visitor : public generic_visitor {}; + + } +} + +#endif // SPOT_LTLAST_VISITOR_HH diff --git a/src/ltlparse/.cvsignore b/src/ltlparse/.cvsignore new file mode 100644 index 000000000..635dda921 --- /dev/null +++ b/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 diff --git a/src/ltlparse/Makefile.am b/src/ltlparse/Makefile.am new file mode 100644 index 000000000..957735ce0 --- /dev/null +++ b/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 diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy new file mode 100644 index 000000000..0f17b8a02 --- /dev/null +++ b/src/ltlparse/ltlparse.yy @@ -0,0 +1,183 @@ +%{ +#include +#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 OP_AND OP_XOR OP_OR +%left OP_IMPLIES OP_EQUIV + +/* LTL operators. */ +%left OP_U OP_R +%nonassoc OP_F OP_G +%nonassoc OP_X + +/* Not has the most important priority. */ +%nonassoc OP_NOT + +/* Grouping (parentheses). */ +%token PAR_OPEN PAR_CLOSE + +/* Atomic proposition. */ +%token ATOMIC_PROP + +/* Constants */ +%token CONST_TRUE +%token CONST_FALSE +%token END_OF_INPUT + +%type 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: diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll new file mode 100644 index 000000000..248173a8c --- /dev/null +++ b/src/ltlparse/ltlscan.ll @@ -0,0 +1,71 @@ +%option noyywrap + +%{ +#include +#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; + +<> return END_OF_INPUT; diff --git a/src/ltlparse/parsedecl.hh b/src/ltlparse/parsedecl.hh new file mode 100644 index 000000000..1448d1dcd --- /dev/null +++ b/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 + diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh new file mode 100644 index 000000000..921de7fcd --- /dev/null +++ b/src/ltlparse/public.hh @@ -0,0 +1,24 @@ +#ifndef SPOT_LTLPARSE_PUBLIC_HH +# define SPOT_LTLPARSE_PUBLIC_HH + +# include +# include "ltlast/formulae.hh" +# include "location.hh" +# include +# include + +namespace spot +{ + namespace ltl + { + typedef std::pair parse_error; + typedef std::list 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 diff --git a/src/ltltest/.cvsignore b/src/ltltest/.cvsignore new file mode 100644 index 000000000..2da84b9d4 --- /dev/null +++ b/src/ltltest/.cvsignore @@ -0,0 +1,9 @@ +Makefile +Makefile.in +.deps +ltl2dot +ltl2text +stdout +parser.dot +expect +defs diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am new file mode 100644 index 000000000..982f83d7e --- /dev/null +++ b/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 diff --git a/src/ltltest/defs.in b/src/ltltest/defs.in new file mode 100644 index 000000000..68de36ac3 --- /dev/null +++ b/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 diff --git a/src/ltltest/parse.test b/src/ltltest/parse.test new file mode 100755 index 000000000..6ba29c911 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/src/ltltest/parseerr.test b/src/ltltest/parseerr.test new file mode 100755 index 000000000..829bf3250 --- /dev/null +++ b/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))' diff --git a/src/ltltest/readltl.cc b/src/ltltest/readltl.cc new file mode 100644 index 000000000..03e5c0e5e --- /dev/null +++ b/src/ltltest/readltl.cc @@ -0,0 +1,69 @@ +#include +#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; +} diff --git a/src/ltlvisit/.cvsignore b/src/ltlvisit/.cvsignore new file mode 100644 index 000000000..e99558847 --- /dev/null +++ b/src/ltlvisit/.cvsignore @@ -0,0 +1,3 @@ +.deps +Makefile +Makefile.in diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am new file mode 100644 index 000000000..1bb9fb656 --- /dev/null +++ b/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 diff --git a/src/ltlvisit/dotty.cc b/src/ltlvisit/dotty.cc new file mode 100644 index 000000000..d5a72687c --- /dev/null +++ b/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; + } + + } +} diff --git a/src/ltlvisit/dotty.hh b/src/ltlvisit/dotty.hh new file mode 100644 index 000000000..48ed2e62d --- /dev/null +++ b/src/ltlvisit/dotty.hh @@ -0,0 +1,15 @@ +#ifndef SPOT_LTLVISIT_DOTTY_HH +# define SPOT_LTLVISIT_DOTTY_HH + +#include +#include + +namespace spot +{ + namespace ltl + { + void dotty(const formulae& f, std::ostream& os); + } +} + +#endif // SPOT_LTLVISIT_DOTTY_HH diff --git a/src/ltlvisit/dump.cc b/src/ltlvisit/dump.cc new file mode 100644 index 000000000..712e17992 --- /dev/null +++ b/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); + } + + } +} diff --git a/src/ltlvisit/dump.hh b/src/ltlvisit/dump.hh new file mode 100644 index 000000000..d375fd3d7 --- /dev/null +++ b/src/ltlvisit/dump.hh @@ -0,0 +1,15 @@ +#ifndef SPOT_LTLVISIT_DUMP_HH +# define SPOT_LTLVISIT_DUMP_HH + +#include +#include + +namespace spot +{ + namespace ltl + { + void dump(const formulae& f, std::ostream& os); + } +} + +#endif // SPOT_LTLVISIT_DUMP_HH diff --git a/src/misc/.cvsignore b/src/misc/.cvsignore new file mode 100644 index 000000000..051d1bd50 --- /dev/null +++ b/src/misc/.cvsignore @@ -0,0 +1,3 @@ +Makefile +Makefile.in +.deps diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am new file mode 100644 index 000000000..f90599a76 --- /dev/null +++ b/src/misc/Makefile.am @@ -0,0 +1,2 @@ + +include_HEADERS = const_sel.hh \ No newline at end of file diff --git a/src/misc/const_sel.hh b/src/misc/const_sel.hh new file mode 100644 index 000000000..f610710ed --- /dev/null +++ b/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 + struct const_sel + { + typedef T t; + }; + + // If const is wanted, add it. + template + struct const_sel + { + typedef const T t; + }; + + // If const is present but isn't wanted, remove it. + template + struct const_sel + { + typedef const T t; + }; +} + +#endif // SPOT_MISC_CONSTSEL_HH diff --git a/tools/.cvsignore b/tools/.cvsignore new file mode 100644 index 000000000..81ac0ddb9 --- /dev/null +++ b/tools/.cvsignore @@ -0,0 +1,4 @@ +depcomp +install-sh +missing +mkinstalldirs