From 526012a795bd1c0a07e9b6d0045ab7ac8bd879ff Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 16 Apr 2003 15:30:44 +0000 Subject: [PATCH] * src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltlast/multop.cc (multop::multop(type)): New constructor. * src/ltlast/multop.hh (multop::multop(type)): New constructor. * src/ltltest/lunabbrev.test: New file. * src/ltltest/Makefile.am (TESTS): Add lunabbrev.test. (check_PROGRAMS): Add lunabbrev. (lunabbrev_SOURCES, lunabbrev_CPPFLAGS): New variables. * src/ltltest/equals.cc (main) [LUNABBREV]: Call unabbreviate_logic. --- ChangeLog | 10 ++++ src/ltlast/multop.cc | 5 ++ src/ltlast/multop.hh | 5 +- src/ltltest/.cvsignore | 1 + src/ltltest/Makefile.am | 6 ++- src/ltltest/equals.cc | 7 +++ src/ltltest/lunabbrev.test | 35 ++++++++++++++ src/ltlvisit/Makefile.am | 4 +- src/ltlvisit/lunabbrev.cc | 99 ++++++++++++++++++++++++++++++++++++++ src/ltlvisit/lunabbrev.hh | 30 ++++++++++++ 10 files changed, 197 insertions(+), 5 deletions(-) create mode 100755 src/ltltest/lunabbrev.test create mode 100644 src/ltlvisit/lunabbrev.cc create mode 100644 src/ltlvisit/lunabbrev.hh diff --git a/ChangeLog b/ChangeLog index daf5630b9..1fd46ef09 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,15 @@ 2003-04-16 Alexandre DURET-LUTZ + * src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: New files. + * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. + * src/ltlast/multop.cc (multop::multop(type)): New constructor. + * src/ltlast/multop.hh (multop::multop(type)): New constructor. + * src/ltltest/lunabbrev.test: New file. + * src/ltltest/Makefile.am (TESTS): Add lunabbrev.test. + (check_PROGRAMS): Add lunabbrev. + (lunabbrev_SOURCES, lunabbrev_CPPFLAGS): New variables. + * src/ltltest/equals.cc (main) [LUNABBREV]: Call unabbreviate_logic. + * src/ltltest/equals.test (check0, check1): Remove. Use check 0, and check 1 instead. diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index ce7b034b3..1da9f5595 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -7,6 +7,11 @@ namespace spot { namespace ltl { + multop::multop(type op) + : op_(op) + { + } + multop::multop(type op, formula* first, formula* second) : op_(op) { diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 40722e0e4..c7912d15d 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -14,9 +14,10 @@ namespace spot public: enum type { Or, And }; - // A multop has at least two arguments. + multop::multop(type op); + // A multop usually has at least two arguments. multop(type op, formula* first, formula* second); - // More argument can be added. + // More arguments can be added. void add(formula* f); virtual ~multop(); diff --git a/src/ltltest/.cvsignore b/src/ltltest/.cvsignore index 366cfea50..0c619ec66 100644 --- a/src/ltltest/.cvsignore +++ b/src/ltltest/.cvsignore @@ -8,3 +8,4 @@ parser.dot expect defs equals +lunabbrev diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index 60e614c38..20414c461 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -4,13 +4,15 @@ LDADD = ../ltlparse/libltlparse.a \ ../ltlast/libltlast.a check_SCRIPTS = defs -check_PROGRAMS = ltl2dot ltl2text equals +check_PROGRAMS = ltl2dot ltl2text equals lunabbrev 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 EXTRA_DIST = $(TESTS) -TESTS = parse.test parseerr.test equals.test +TESTS = parse.test parseerr.test equals.test lunabbrev.test CLEANFILES = stdout expect parse.dot diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index 4acd2e232..6494f8d8b 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -1,6 +1,8 @@ #include #include "ltlparse/public.hh" #include "ltlvisit/equals.hh" +#include "ltlvisit/lunabbrev.hh" +#include "ltlvisit/dump.hh" void syntax(char *prog) @@ -28,6 +30,11 @@ main(int argc, char **argv) if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2)) return 2; +#ifdef LUNABBREV + f1 = spot::ltl::unabbreviate_logic(f1); + spot::ltl::dump(*f1, std::cout); +#endif + if (equals(f1, f2)) return 0; return 1; diff --git a/src/ltltest/lunabbrev.test b/src/ltltest/lunabbrev.test new file mode 100755 index 000000000..023f434ae --- /dev/null +++ b/src/ltltest/lunabbrev.test @@ -0,0 +1,35 @@ +#! /bin/sh + +# Check for the equals visitor + +. ./defs || exit 1 + +check() +{ + ./lunabbrev "$1" "$2" || exit 1 +} + +# A few things that do not change +check 'a' 'a' +check '1' '1' +check '0' '0' +check 'G a ' ' G a' +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' + +# other formulae that do change +check 'a ^ b' '(a & !b) | (!a & b)' +check 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)' +check 'GF a => F G(b)' '!GFa | F Gb' +check '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)' +check '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)' + +# Success. +: \ No newline at end of file diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index a79549bf7..9ee40941a 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -8,4 +8,6 @@ libltlvisit_a_SOURCES = \ dump.cc \ dump.hh \ equals.cc \ - equals.hh + equals.hh \ + lunabbrev.hh \ + lunabbrev.cc diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc new file mode 100644 index 000000000..53be6d476 --- /dev/null +++ b/src/ltlvisit/lunabbrev.cc @@ -0,0 +1,99 @@ +#include "ltlast/allnodes.hh" +#include "lunabbrev.hh" + +namespace spot +{ + namespace ltl + { + unabbreviate_logic_visitor::unabbreviate_logic_visitor() + { + } + + unabbreviate_logic_visitor::~unabbreviate_logic_visitor() + { + } + + formula* + unabbreviate_logic_visitor::result() const + { + return result_; + } + + void + unabbreviate_logic_visitor::visit(const atomic_prop* ap) + { + result_ = new atomic_prop(ap->name()); + } + + void + unabbreviate_logic_visitor::visit(const constant* c) + { + result_ = new constant(c->val()); + } + + void + unabbreviate_logic_visitor::visit(const unop* uo) + { + result_ = new unop(uo->op(), unabbreviate_logic(uo->child())); + } + + void + unabbreviate_logic_visitor::visit(const binop* bo) + { + formula* f1 = unabbreviate_logic(bo->first()); + formula* f2 = unabbreviate_logic(bo->second()); + switch (bo->op()) + { + /* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */ + case binop::Xor: + result_ = new multop(multop::Or, + new multop(multop::And, f1, + new unop(unop::Not, f2)), + new multop(multop::And, f2, + new unop(unop::Not, f1))); + return; + /* f1 => f2 == !f1 | f2 */ + case binop::Implies: + result_ = new multop(multop::Or, new unop(unop::Not, f1), f2); + return; + /* f1 <=> f2 == (f1 & f2) | (!f1 & !f2) */ + case binop::Equiv: + result_ = new multop(multop::Or, + new multop(multop::And, f1, f2), + new multop(multop::And, + new unop(unop::Not, f1), + new unop(unop::Not, f2))); + return; + /* f1 U f2 == f1 U f2 */ + /* f1 R f2 == f1 R f2 */ + case binop::U: + case binop::R: + result_ = new binop(bo->op(), f1, f2); + return; + } + /* Unreachable code. */ + assert(0); + } + + void + unabbreviate_logic_visitor::visit(const multop* mo) + { + multop* res = new multop(mo->op()); + unsigned mos = mo->size(); + for (unsigned i = 0; i < mos; ++i) + { + res->add(unabbreviate_logic(mo->nth(i))); + } + result_ = res; + } + + formula* + unabbreviate_logic(const formula* f) + { + unabbreviate_logic_visitor v; + f->accept(v); + return v.result(); + } + + } +} diff --git a/src/ltlvisit/lunabbrev.hh b/src/ltlvisit/lunabbrev.hh new file mode 100644 index 000000000..03b40e1f2 --- /dev/null +++ b/src/ltlvisit/lunabbrev.hh @@ -0,0 +1,30 @@ +#include "ltlast/formula.hh" +#include "ltlast/visitor.hh" + +namespace spot +{ + namespace ltl + { + // This visitor is public, because it's convenient + // to derive from it and override part of its methods. + class unabbreviate_logic_visitor : public const_visitor + { + public: + unabbreviate_logic_visitor(); + virtual ~unabbreviate_logic_visitor(); + + formula* result() const; + + void visit(const atomic_prop* ap); + void visit(const unop* uo); + void visit(const binop* bo); + void visit(const multop* mo); + void visit(const constant* c); + + private: + formula* result_; + }; + + formula* unabbreviate_logic(const formula* f); + } +}