diff --git a/ChangeLog b/ChangeLog index fee359774..7bf116da3 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,13 @@ 2003-04-16 Alexandre DURET-LUTZ + * src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: New files. + * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add equals.hh + and equals.cc. + * src/ltltest/equals.cc, src/ltltest/equals.test: New files. + * src/ltltest/Makefile.am (check_PROGRAMS): Add equals. + (equals_SOURCES): New variable. + (TESTS): Add equals.test. + * src/ltlast/multop.cc (multop::multop): Use multop::add. (multop::add): If the formulae we add is itself a multop for the same operator, merge its children with ours. diff --git a/src/ltltest/.cvsignore b/src/ltltest/.cvsignore index 2da84b9d4..366cfea50 100644 --- a/src/ltltest/.cvsignore +++ b/src/ltltest/.cvsignore @@ -7,3 +7,4 @@ stdout parser.dot expect defs +equals diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index 982f83d7e..60e614c38 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -4,12 +4,13 @@ LDADD = ../ltlparse/libltlparse.a \ ../ltlast/libltlast.a check_SCRIPTS = defs -check_PROGRAMS = ltl2dot ltl2text +check_PROGRAMS = ltl2dot ltl2text equals ltl2dot_SOURCES = readltl.cc ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY ltl2text_SOURCES = readltl.cc +equals_SOURCES = equals.cc EXTRA_DIST = $(TESTS) -TESTS = parse.test parseerr.test +TESTS = parse.test parseerr.test equals.test CLEANFILES = stdout expect parse.dot diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc new file mode 100644 index 000000000..9029ce976 --- /dev/null +++ b/src/ltltest/equals.cc @@ -0,0 +1,59 @@ +#include +#include "ltlparse/public.hh" +#include "ltlvisit/equals.hh" + +void +syntax(char *prog) +{ + std::cerr << prog << " formulae1 formulae2" << std::endl; + exit(2); +} + +bool +print_parse_error(const char* f, spot::ltl::parse_error_list& pel) +{ + bool err = false; + + spot::ltl::parse_error_list::iterator it; + for (it = pel.begin(); it != pel.end(); ++it) + { + std::cerr << ">>> " << f << 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; + err = true; + } + return err; +} + +int +main(int argc, char **argv) +{ + if (argc != 3) + syntax(argv[0]); + + + spot::ltl::parse_error_list p1; + spot::ltl::formulae *f1 = spot::ltl::parse(argv[1], p1); + + if (print_parse_error(argv[1], p1)) + return 2; + + spot::ltl::parse_error_list p2; + spot::ltl::formulae *f2 = spot::ltl::parse(argv[2], p2); + + if (print_parse_error(argv[2], p2)) + return 2; + + if (equals(f1, f2)) + return 0; + return 1; + +} diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test new file mode 100755 index 000000000..3432051c2 --- /dev/null +++ b/src/ltltest/equals.test @@ -0,0 +1,51 @@ +#! /bin/sh + +# Check for the equals visitor + +. ./defs || exit 1 + +check() +{ + ./equals "$2" "$3" + test $? != $1 && exit 1; +} + +check0() +{ + check 0 "$@" +} + +check1() +{ + check 1 "$@" +} + +# A few things which are equal +check0 'a' 'a' +check0 '1' '1' +check0 '0' '0' +check0 'a => b' 'a => b' +check0 'G a ' ' G a' +check0 'a U b' 'a U b' +check0 'a & b' 'a & b' +check0 'a & b' 'b & a' +check0 'a & b & c' 'c & a & b' +check0 'a & b & c' 'b & c & a' +check0 'a & b & a' 'b & a & b' +check0 'a & b' 'b & a & b' +check0 'a & b' 'b & a & a' +check0 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b' + +# other formulae which are not +check1 'a' 'b' +check1 '1' '0' +check1 'a => b' 'b => a' +check1 'a => b' 'a <=> b' +check1 'a => b' 'a U b' +check1 'a R b' 'a U b' +check1 'a & b & c' 'c & a' +check1 'b & c' 'c & a & b' +check1 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(g U g)| e | c) & b' + +# Success. +: \ No newline at end of file diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index 1bb9fb656..a79549bf7 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -6,4 +6,6 @@ libltlvisit_a_SOURCES = \ dotty.cc \ dotty.hh \ dump.cc \ - dump.hh + dump.hh \ + equals.cc \ + equals.hh diff --git a/src/ltlvisit/equals.cc b/src/ltlvisit/equals.cc new file mode 100644 index 000000000..28c1572f7 --- /dev/null +++ b/src/ltlvisit/equals.cc @@ -0,0 +1,140 @@ +#include +#include "equals.hh" +#include "ltlast/allnodes.hh" + +namespace spot +{ + namespace ltl + { + equals_visitor::equals_visitor(const formulae* f) + : f_(f), result_(false) + { + } + + equals_visitor::~equals_visitor() + { + } + + bool + equals_visitor::result() const + { + return result_; + } + + void + equals_visitor::visit(const atomic_prop* ap) + { + const atomic_prop* p = dynamic_cast(f_); + if (p && p->name() == ap->name()) + result_ = true; + } + + void + equals_visitor::visit(const constant* c) + { + const constant* p = dynamic_cast(f_); + if (p && p->val() == c->val()) + result_ = true; + } + + void + equals_visitor::visit(const unop* uo) + { + const unop* p = dynamic_cast(f_); + if (!p || p->op() != uo->op()) + return; + f_ = p->child(); + uo->child()->accept(*this); + } + + void + equals_visitor::visit(const binop* bo) + { + const binop* p = dynamic_cast(f_); + if (!p || p->op() != bo->op()) + return; + + // The current visitor will descend the left branch. + // Build a second visitor for the right branch. + equals_visitor v2(p->second()); + f_ = p->first(); + + bo->first()->accept(*this); + if (result_ == false) + return; + + bo->second()->accept(v2); + result_ = v2.result(); + } + + void + equals_visitor::visit(const multop* m) + { + const multop* p = dynamic_cast(f_); + if (!p || p->op() != m->op()) + return; + + // This check is a bit more complicated than other checks + // because And(a, b, c) is equal to And(c, a, b, a). + + unsigned m_size = m->size(); + unsigned p_size = p->size(); + std::vector p_seen(p_size, false); + + for (unsigned nf = 0; nf < m_size; ++nf) + { + unsigned np; + const formulae* mnth = m->nth(nf); + for (np = 0; np < p_size; ++np) + { + if (equals(p->nth(np), mnth)) + { + p_seen[np] = true; + break; + } + } + // We we haven't found mnth in any child of p, then + // the two formulaes aren't equal. + if (np == p_size) + return; + } + // At this point, we have found all children of m' in children + // of `p'. That doesn't means that both formula are equal. + // Condider m = And(a, b, c) against p = And(c, d, a, b). + // We should now check if any unmarked (accodring to p_seen) + // child of `p' has an counterpart in `m'. Because `m' might + // contain duplicate children, its faster to test that + // unmarked children of `p' have a counterpart in marked children + // of `p'. + for (unsigned np = 0; np < p_size; ++np) + { + // Consider only unmarked children. + if (p_seen[np]) + continue; + + // Compare with marked children. + unsigned np2; + const formulae *pnth = p->nth(np); + for (np2 = 0; np2 < p_size; ++np2) + if (p_seen[np2] && equals(p->nth(np2), pnth)) + break; + + // No match? Too bad. + if (np2 == p_size) + return; + } + + // The two formulaes match. + result_ = true; + } + + + bool + equals(const formulae* f1, const formulae* f2) + { + equals_visitor v(f1); + f2->accept(v); + return v.result(); + } + } +} diff --git a/src/ltlvisit/equals.hh b/src/ltlvisit/equals.hh new file mode 100644 index 000000000..704093d9e --- /dev/null +++ b/src/ltlvisit/equals.hh @@ -0,0 +1,34 @@ +#include "ltlast/formulae.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 equals_visitor : public const_visitor + { + public: + equals_visitor(const formulae* f); + virtual ~equals_visitor(); + + // Return true iff the visitor has visited a + // formulae which is equal to `f'. + bool result() const; + + void visit(const atomic_prop* ap); + void visit(const unop* uo); + void visit(const binop* bo); + void visit(const multop* bo); + void visit(const constant* c); + + private: + const formulae* f_; + bool result_; + + }; + + bool equals(const formulae* f1, const formulae* f2); + } +}