From eed40025beec573d0d2b54a7f1d2ce3ceab427d2 Mon Sep 17 00:00:00 2001 From: rebiha Date: Thu, 24 Apr 2003 10:43:26 +0000 Subject: [PATCH] * 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 | 7 +++ src/ltltest/Makefile.am | 11 ++-- src/ltltest/tostring.cc | 45 ++++++++++++++ src/ltltest/tostring.test | 28 +++++++++ src/ltlvisit/Makefile.am | 4 +- src/ltlvisit/equals.hh | 1 + src/ltlvisit/tostring.cc | 125 ++++++++++++++++++++++++++++++++++++++ src/ltlvisit/tostring.hh | 15 +++++ 8 files changed, 231 insertions(+), 5 deletions(-) create mode 100644 src/ltltest/tostring.cc create mode 100755 src/ltltest/tostring.test create mode 100644 src/ltlvisit/tostring.cc create mode 100644 src/ltlvisit/tostring.hh diff --git a/ChangeLog b/ChangeLog index 8f214ce58..6824c5e8c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2003-04-24 Rachid REBIHA + + * 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 * src/ltlparse/Makefile.am (EXTRA_DIST): Distribute ltlparse.yy. diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index f056d381f..ffcd690f3 100644 --- a/src/ltltest/Makefile.am +++ b/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 \ diff --git a/src/ltltest/tostring.cc b/src/ltltest/tostring.cc new file mode 100644 index 000000000..66cb29a1d --- /dev/null +++ b/src/ltltest/tostring.cc @@ -0,0 +1,45 @@ +#include +#include +#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; +} + diff --git a/src/ltltest/tostring.test b/src/ltltest/tostring.test new file mode 100755 index 000000000..04c7a3015 --- /dev/null +++ b/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' +: diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index c3558c3ce..7ee553574 100644 --- a/src/ltlvisit/Makefile.am +++ 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 \ No newline at end of file diff --git a/src/ltlvisit/equals.hh b/src/ltlvisit/equals.hh index a4f8a4d92..b5e56c817 100644 --- a/src/ltlvisit/equals.hh +++ b/src/ltlvisit/equals.hh @@ -43,3 +43,4 @@ namespace spot bool equals(const formula* f1, const formula* f2); } } + diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc new file mode 100644 index 000000000..4c23680e0 --- /dev/null +++ b/src/ltlvisit/tostring.cc @@ -0,0 +1,125 @@ +#include +#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); + } + + } +} diff --git a/src/ltlvisit/tostring.hh b/src/ltlvisit/tostring.hh new file mode 100644 index 000000000..94b83e7e3 --- /dev/null +++ b/src/ltlvisit/tostring.hh @@ -0,0 +1,15 @@ +#ifndef SPOT_LTLVISIT_AST2STRING_HH +# define SPOT_LTLVISIT_AST2STRING_HH + +#include +#include + +namespace spot +{ + namespace ltl + { + void to_string(const formula& f, std::ostream& os); + } +} + +#endif // SPOT_LTLVISIT_AST2STRING_HH