From ac9d0a502aad7ed8a27585d3620199b679859413 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 3 Dec 2010 18:29:59 +0100 Subject: [PATCH] Add full_parent support to to_spin_string(). * src/ltlvisit/tostrinc.hh (to_spin_string): Add a full_parent optional parameter, like for the to_string() function. * src/ltlvisit/tostrinc.cc (to_string_visitor): Fix the handling of full_parent. (to_spin_string_visitor): Handle full_parent. --- ChangeLog | 14 ++++++++++-- src/ltlvisit/tostring.cc | 48 +++++++++++++++++++++++++++++++--------- src/ltlvisit/tostring.hh | 11 +++++++-- 3 files changed, 59 insertions(+), 14 deletions(-) diff --git a/ChangeLog b/ChangeLog index 54ffa1c68..606871c68 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,9 +1,19 @@ -2010-12-01 Alexandre Duret-Lutz +2010-12-03 Alexandre Duret-Lutz + + Add full_parent support to to_spin_string(). + + * src/ltlvisit/tostrinc.hh (to_spin_string): Add a full_parent + optional parameter, like for the to_string() function. + * src/ltlvisit/tostrinc.cc (to_string_visitor): Fix the + handling of full_parent. + (to_spin_string_visitor): Handle full_parent. + +2010-12-01 Alexandre Duret-Lutz Halve the number of application of eventual_universal_visitor in reduce_visitor::visit(binop). - * src/ltlvisit/reduce.cc (eventual_universal_visitor::recurse_): + * src/ltlvisit/reduce.cc (eventual_universal_visitor::recurse_): Move this method... (recurse_eu): ... outside as a separate function. Likewise for the universal/eventual result struct. diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index b0ba0de08..799024a09 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -75,6 +75,8 @@ namespace spot visit(const atomic_prop* ap) { std::string str = ap->name(); + if (full_parent_) + os_ << "("; if (!is_bare_word(str.c_str())) { os_ << '"' << str << '"'; @@ -83,12 +85,18 @@ namespace spot { os_ << str; } + if (full_parent_) + os_ << ")"; } void visit(const constant* c) { + if (full_parent_) + os_ << "("; os_ << c->val_name(); + if (full_parent_) + os_ << ")"; } void @@ -137,6 +145,16 @@ namespace spot // The parser treats F0, F1, G0, G1, X0, and X1 as atomic // propositions. So make sure we output F(0), G(1), etc. bool need_parent = !!dynamic_cast(uo->child()); + bool top_level = top_level_; + + if (full_parent_) + { + need_parent = false; // These will be printed by each subformula + + if (!top_level) + os_ << "("; + } + switch (uo->op()) { case unop::Not: @@ -159,10 +177,13 @@ namespace spot } top_level_ = false; - if (need_parent || full_parent_) + if (need_parent) os_ << "("; uo->child()->accept(*this); - if (need_parent || full_parent_) + if (need_parent) + os_ << ")"; + + if (full_parent_ && !top_level) os_ << ")"; } @@ -225,8 +246,8 @@ namespace spot class to_spin_string_visitor : public to_string_visitor { public: - to_spin_string_visitor(std::ostream& os) - : to_string_visitor(os) + to_spin_string_visitor(std::ostream& os, bool full_parent = false) + : to_string_visitor(os, full_parent) { } @@ -302,8 +323,9 @@ namespace spot void visit(const unop* uo) { - // The parser treats X0, and X1 as atomic propositions. So - // make sure we output X(0) and X(1). + bool top_level = top_level_; + if (full_parent_ && !top_level) + os_ << "("; bool need_parent = false; switch (uo->op()) { @@ -311,7 +333,11 @@ namespace spot os_ << "!"; break; case unop::X: + // The parser treats X0, and X1 as atomic propositions. So + // make sure we output X(0) and X(1). need_parent = !!dynamic_cast(uo->child()); + if (full_parent_) + need_parent = false; os_ << "X"; break; case unop::F: @@ -332,6 +358,8 @@ namespace spot uo->child()->accept(*this); if (need_parent) os_ << ")"; + if (full_parent_ && !top_level) + os_ << ")"; } void @@ -405,18 +433,18 @@ namespace spot } std::ostream& - to_spin_string(const formula* f, std::ostream& os) + to_spin_string(const formula* f, std::ostream& os, bool full_parent) { - to_spin_string_visitor v(os); + to_spin_string_visitor v(os, full_parent); f->accept(v); return os; } std::string - to_spin_string(const formula* f) + to_spin_string(const formula* f, bool full_parent) { std::ostringstream os; - to_spin_string(f, os); + to_spin_string(f, os, full_parent); return os.str(); } } diff --git a/src/ltlvisit/tostring.hh b/src/ltlvisit/tostring.hh index 857a67489..62fda4f0a 100644 --- a/src/ltlvisit/tostring.hh +++ b/src/ltlvisit/tostring.hh @@ -1,3 +1,5 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -52,11 +54,16 @@ namespace spot /// \brief Output a formula as a (parsable by Spin) string. /// \param f The formula to translate. /// \param os The stream where it should be output. - std::ostream& to_spin_string(const formula* f, std::ostream& os); + /// \param full_parent Whether or not the string should by fully + /// parenthesized. + std::ostream& to_spin_string(const formula* f, std::ostream& os, + bool full_parent = false); /// \brief Convert a formula into a (parsable by Spin) string. /// \param f The formula to translate. - std::string to_spin_string(const formula* f); + /// \param full_parent Whether or not the string should by fully + /// parenthesized. + std::string to_spin_string(const formula* f, bool full_parent = false); /// @} }