From 7685d3a5b834c4ca8c77ab17fa17449bf3d7c3ff Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 16 May 2003 08:10:58 +0000 Subject: [PATCH] * src/ltlvisit/dump.hh (dump): Take a formula* as argument, not a formula&. This is more homogeneous. * src/ltlvisit/dump.cc (dump): Likewise. * src/ltlvisit/dotty.hh (dotty): Likewise. * src/ltlvisit/dotty.cc (dotty): Likewise. * src/ltlvisit/tostring.hh (to_string): Likewise. * src/ltlvisit/tostring.cc (to_string): Likewise. * src/ltltest/readltl.cc, src/ltltest/equals.cc, src/ltltest/tostring.cc: Adjust usage. --- ChangeLog | 12 +++++++++++- src/ltltest/equals.cc | 9 +++------ src/ltltest/readltl.cc | 4 ++-- src/ltltest/tostring.cc | 4 ++-- src/ltlvisit/dotty.cc | 26 ++++++++++++------------- src/ltlvisit/dotty.hh | 4 ++-- src/ltlvisit/dump.cc | 22 ++++++++++----------- src/ltlvisit/dump.hh | 4 ++-- src/ltlvisit/tostring.cc | 42 ++++++++++++++++++++-------------------- src/ltlvisit/tostring.hh | 6 +++--- 10 files changed, 70 insertions(+), 63 deletions(-) diff --git a/ChangeLog b/ChangeLog index f62058cc0..3f8fc5c7a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,9 +1,19 @@ 2003-05-16 Alexandre Duret-Lutz + * src/ltlvisit/dump.hh (dump): Take a formula* as argument, + not a formula&. This is more homogeneous. + * src/ltlvisit/dump.cc (dump): Likewise. + * src/ltlvisit/dotty.hh (dotty): Likewise. + * src/ltlvisit/dotty.cc (dotty): Likewise. + * src/ltlvisit/tostring.hh (to_string): Likewise. + * src/ltlvisit/tostring.cc (to_string): Likewise. + * src/ltltest/readltl.cc, src/ltltest/equals.cc, + src/ltltest/tostring.cc: Adjust usage. + Check trivial multop equality at build time. The makes the equal visitor useless, since two equals formulae will now share the same address. - + * src/ltlast/multop.hh (add_sorted): New function. (paircmp): New comparison functor. (map): Use paircmp, we want to compare the vectors' contents, diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc index b3c163be1..c1c3455a4 100644 --- a/src/ltltest/equals.cc +++ b/src/ltltest/equals.cc @@ -38,26 +38,23 @@ main(int argc, char** argv) #endif #ifdef LUNABBREV tmp = f1; - std::cout << spot::ltl::atomic_prop::instance_count() << std::endl; f1 = spot::ltl::unabbreviate_logic(f1); - std::cout << spot::ltl::atomic_prop::instance_count() << std::endl; spot::ltl::destroy(tmp); - std::cout << spot::ltl::atomic_prop::instance_count() << std::endl; - spot::ltl::dump(*f1, std::cout); + spot::ltl::dump(f1, std::cout); std::cout << std::endl; #endif #ifdef TUNABBREV tmp = f1; f1 = spot::ltl::unabbreviate_ltl(f1); spot::ltl::destroy(tmp); - spot::ltl::dump(*f1, std::cout); + spot::ltl::dump(f1, std::cout); std::cout << std::endl; #endif #ifdef NENOFORM tmp = f1; f1 = spot::ltl::negative_normal_form(f1); spot::ltl::destroy(tmp); - spot::ltl::dump(*f1, std::cout); + spot::ltl::dump(f1, std::cout); std::cout << std::endl; #endif diff --git a/src/ltltest/readltl.cc b/src/ltltest/readltl.cc index f403dacf4..9457fe3bd 100644 --- a/src/ltltest/readltl.cc +++ b/src/ltltest/readltl.cc @@ -43,9 +43,9 @@ main(int argc, char** argv) if (f) { #ifdef DOTTY - spot::ltl::dotty(*f, std::cout); + spot::ltl::dotty(f, std::cout); #else - spot::ltl::dump(*f, std::cout); + spot::ltl::dump(f, std::cout); std::cout << std::endl; #endif spot::ltl::destroy(f); diff --git a/src/ltltest/tostring.cc b/src/ltltest/tostring.cc index 8b4299068..fe4726542 100644 --- a/src/ltltest/tostring.cc +++ b/src/ltltest/tostring.cc @@ -26,7 +26,7 @@ main(int argc, char **argv) // The string generated from an abstract tree should be parsable // again. - std::string f1s = spot::ltl::to_string(*f1); + std::string f1s = spot::ltl::to_string(f1); std::cout << f1s << std::endl; spot::ltl::formula* f2 = spot::ltl::parse(f1s, p1); @@ -41,7 +41,7 @@ main(int argc, char **argv) // It should also map to the same string. - std::string f2s = spot::ltl::to_string(*f2); + std::string f2s = spot::ltl::to_string(f2); std::cout << f2s << std::endl; if (f2s != f1s) diff --git a/src/ltlvisit/dotty.cc b/src/ltlvisit/dotty.cc index d9b213713..741a88a84 100644 --- a/src/ltlvisit/dotty.cc +++ b/src/ltlvisit/dotty.cc @@ -3,7 +3,7 @@ #include "ltlast/allnodes.hh" -namespace spot +namespace spot { namespace ltl { @@ -16,12 +16,12 @@ namespace spot { } - virtual + virtual ~dotty_visitor() { } - void + void visit(const spot::ltl::atomic_prop* ap) { draw_node_(ap->name()); @@ -32,20 +32,20 @@ namespace spot { 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) { @@ -53,7 +53,7 @@ namespace spot label_ = draw_link_(label_, label_ + "c"); uo->child()->accept(*this); } - + void visit(const spot::ltl::multop* mo) { @@ -79,10 +79,10 @@ namespace spot return out; } - void + void draw_rec_node_(const char* str) const { - os_ << " " << label_ << " [label=\"" << str << "\", shabe=box];" + os_ << " " << label_ << " [label=\"" << str << "\", shabe=box];" << std::endl; } @@ -91,15 +91,15 @@ namespace spot { os_ << " " << label_ << " [label=\"" << str << "\"];" << std::endl; } - + }; - void - dotty(const formula& f, std::ostream& os) + void + dotty(const formula* f, std::ostream& os) { dotty_visitor v(os); os << "digraph G {" << std::endl; - f.accept(v); + f->accept(v); os << "}" << std::endl; } diff --git a/src/ltlvisit/dotty.hh b/src/ltlvisit/dotty.hh index 2af9606b4..f7de2b09a 100644 --- a/src/ltlvisit/dotty.hh +++ b/src/ltlvisit/dotty.hh @@ -4,7 +4,7 @@ #include #include -namespace spot +namespace spot { namespace ltl { @@ -14,7 +14,7 @@ namespace spot /// /// \c dot is part of the GraphViz package /// http://www.research.att.com/sw/tools/graphviz/ - void dotty(const formula& f, std::ostream& os); + void dotty(const formula* f, std::ostream& os); } } diff --git a/src/ltlvisit/dump.cc b/src/ltlvisit/dump.cc index 52c851397..4996cf50a 100644 --- a/src/ltlvisit/dump.cc +++ b/src/ltlvisit/dump.cc @@ -3,7 +3,7 @@ #include "ltlast/allnodes.hh" -namespace spot +namespace spot { namespace ltl { @@ -15,13 +15,13 @@ namespace spot : os_(os) { } - - virtual + + virtual ~dump_visitor() { } - void + void visit(const spot::ltl::atomic_prop* ap) { os_ << "AP(" << ap->name() << ")"; @@ -31,8 +31,8 @@ namespace spot visit(const spot::ltl::constant* c) { os_ << "constant(" << c->val_name() << ")"; - } - + } + void visit(const spot::ltl::binop* bo) { @@ -42,7 +42,7 @@ namespace spot bo->second()->accept(*this); os_ << ")"; } - + void visit(const spot::ltl::unop* uo) { @@ -50,7 +50,7 @@ namespace spot uo->child()->accept(*this); os_ << ")"; } - + void visit(const spot::ltl::multop* mo) { @@ -68,11 +68,11 @@ namespace spot std::ostream& os_; }; - void - dump(const formula& f, std::ostream& os) + void + dump(const formula* f, std::ostream& os) { dump_visitor v(os); - f.accept(v); + f->accept(v); } } diff --git a/src/ltlvisit/dump.hh b/src/ltlvisit/dump.hh index fb30dd0ee..3d0e6ed2e 100644 --- a/src/ltlvisit/dump.hh +++ b/src/ltlvisit/dump.hh @@ -4,7 +4,7 @@ #include "ltlast/formula.hh" #include -namespace spot +namespace spot { namespace ltl { @@ -13,7 +13,7 @@ namespace spot /// \param os The stream where it should be output. /// /// This is useful to display a formula when debugging. - void dump(const formula& f, std::ostream& os); + void dump(const formula* f, std::ostream& os); } } diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 29fbc79e3..43c141c51 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -5,7 +5,7 @@ #include "ltlast/allnodes.hh" -namespace spot +namespace spot { namespace ltl { @@ -17,13 +17,13 @@ namespace spot : os_(os) { } - - virtual + + virtual ~to_string_visitor() { } - - void + + void visit(const atomic_prop* ap) { os_ << ap->name(); @@ -33,14 +33,14 @@ namespace spot visit(const constant* c) { os_ << c->val_name(); - } - + } + void visit(const binop* bo) { os_ << "("; bo->first()->accept(*this); - + switch(bo->op()) { case binop::Xor: @@ -59,14 +59,14 @@ namespace spot os_ << " R "; break; } - + bo->second()->accept(*this); os_ << ")"; } - + void visit(const unop* uo) - { + { switch(uo->op()) { case unop::Not: @@ -82,10 +82,10 @@ namespace spot os_ << "G"; break; } - + uo->child()->accept(*this); } - + void visit(const multop* mo) { @@ -97,12 +97,12 @@ namespace spot { case multop::Or: ch = " | "; - break; + break; case multop::And: ch = " & "; break; } - + for (unsigned n = 1; n < max; ++n) { os_ << ch; @@ -113,16 +113,16 @@ namespace spot private: std::ostream& os_; }; - - void - to_string(const formula& f, std::ostream& os) + + void + to_string(const formula* f, std::ostream& os) { to_string_visitor v(os); - f.accept(v); + f->accept(v); } - std::string - to_string(const formula& f) + std::string + to_string(const formula* f) { std::ostringstream os; to_string(f, os); diff --git a/src/ltlvisit/tostring.hh b/src/ltlvisit/tostring.hh index 6b75a9bd4..beb5f6a98 100644 --- a/src/ltlvisit/tostring.hh +++ b/src/ltlvisit/tostring.hh @@ -4,12 +4,12 @@ #include #include -namespace spot +namespace spot { namespace ltl { - void to_string(const formula& f, std::ostream& os); - std::string to_string(const formula& f); + void to_string(const formula* f, std::ostream& os); + std::string to_string(const formula* f); } }