From 8e988470b171d3e8b0fb40179f477ace7527af64 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 12 May 2003 12:41:41 +0000 Subject: [PATCH] * src/ltlvisit/tostring.cc: Reindent and strip out superfluous spot::ltl:: prefixes. (to_string(formula)): New function. * src/ltlvisit/tostring.hh (to_string(formula)): Likewise. * src/ltltest/tostring.cc: Use this new to_string function to simplify. --- ChangeLog | 9 ++++ src/ltltest/tostring.cc | 17 +++--- src/ltlvisit/tostring.cc | 111 +++++++++++++++++++++------------------ src/ltlvisit/tostring.hh | 1 + 4 files changed, 76 insertions(+), 62 deletions(-) diff --git a/ChangeLog b/ChangeLog index 2e9d6e54a..4c19f120e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2003-05-12 Alexandre Duret-Lutz + + * src/ltlvisit/tostring.cc: Reindent and strip out superfluous + spot::ltl:: prefixes. + (to_string(formula)): New function. + * src/ltlvisit/tostring.hh (to_string(formula)): Likewise. + * src/ltltest/tostring.cc: Use this new to_string function to + simplify. + 2003-05-05 Alexandre Duret-Lutz * m4/buddy.m4: New file. diff --git a/src/ltltest/tostring.cc b/src/ltltest/tostring.cc index 3a2bb9217..50ff4fc98 100644 --- a/src/ltltest/tostring.cc +++ b/src/ltltest/tostring.cc @@ -1,5 +1,4 @@ #include -#include #include "ltlparse/public.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/equals.hh" @@ -26,13 +25,12 @@ main(int argc, char **argv) // The string generated from an abstract tree should be parsable // again. - std::ostringstream os; - spot::ltl::to_string(*f1, os); - std::cout << os.str() << std::endl; + std::string f1s = spot::ltl::to_string(*f1); + std::cout << f1s << std::endl; - spot::ltl::formula* f2 = spot::ltl::parse(os.str(), p1); + spot::ltl::formula* f2 = spot::ltl::parse(f1s, p1); - if (spot::ltl::format_parse_errors(std::cerr, os.str(), p1)) + if (spot::ltl::format_parse_errors(std::cerr, f1s, p1)) return 2; // This second abstract tree should be equal to the first. @@ -42,11 +40,10 @@ main(int argc, char **argv) // It should also map to the same string. - std::ostringstream os2; - spot::ltl::to_string(*f2, os2); - std::cout << os2.str() << std::endl; + std::string f2s = spot::ltl::to_string(*f2); + std::cout << f2s << std::endl; - if (os2.str() != os.str()) + if (f2s != f1s) return 1; } diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 4c23680e0..29fbc79e3 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -1,4 +1,5 @@ #include +#include #include "tostring.hh" #include "ltlast/visitor.hh" #include "ltlast/allnodes.hh" @@ -9,7 +10,7 @@ namespace spot namespace ltl { - class to_string_visitor : public spot::ltl::const_visitor + class to_string_visitor : public const_visitor { public: to_string_visitor(std::ostream& os = std::cout) @@ -21,88 +22,87 @@ namespace spot ~to_string_visitor() { } - + void - visit(const spot::ltl::atomic_prop* ap) + visit(const atomic_prop* ap) { - os_ << ap->name(); - + os_ << ap->name(); } void - visit(const spot::ltl::constant* c) + visit(const constant* c) { os_ << c->val_name(); } void - visit(const spot::ltl::binop* bo) + visit(const 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; - } + { + case binop::Xor: + os_ << " ^ "; + break; + case binop::Implies: + os_ << " => "; + break; + case binop::Equiv: + os_ << " <=> "; + break; + case binop::U: + os_ << " U "; + break; + case binop::R: + os_ << " R "; + break; + } bo->second()->accept(*this); os_ << ")"; } void - visit(const spot::ltl::unop* uo) + visit(const 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; - } + switch(uo->op()) + { + case unop::Not: + os_ << "!"; + break; + case unop::X: + os_ << "X"; + break; + case unop::F: + os_ << "F"; + break; + case unop::G: + os_ << "G"; + break; + } uo->child()->accept(*this); } void - visit(const spot::ltl::multop* mo) + visit(const multop* mo) { os_ << "("; unsigned max = mo->size(); mo->nth(0)->accept(*this); - const char* ch = " "; + const char* ch = " "; switch (mo->op()) - { - case spot::ltl::multop::Or: - ch = " | "; - break; - case spot::ltl::multop::And: - ch = " & "; - break; - } - + { + case multop::Or: + ch = " | "; + break; + case multop::And: + ch = " & "; + break; + } + for (unsigned n = 1; n < max; ++n) { os_ << ch; @@ -113,7 +113,7 @@ namespace spot private: std::ostream& os_; }; - + void to_string(const formula& f, std::ostream& os) { @@ -121,5 +121,12 @@ namespace spot f.accept(v); } + std::string + to_string(const formula& f) + { + std::ostringstream os; + to_string(f, os); + return os.str(); + } } } diff --git a/src/ltlvisit/tostring.hh b/src/ltlvisit/tostring.hh index 94b83e7e3..6b75a9bd4 100644 --- a/src/ltlvisit/tostring.hh +++ b/src/ltlvisit/tostring.hh @@ -9,6 +9,7 @@ namespace spot namespace ltl { void to_string(const formula& f, std::ostream& os); + std::string to_string(const formula& f); } }