alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Make it possible to format SERE.

Browse source 
* src/ltlvisit/tostring.hh, src/ltlvisit/tostring.cc (to_string):
Add third option to enable formating suitable for SERE.
This commit is contained in:
Alexandre Duret-Lutz 2011-02-13 22:35:11 +01:00
parent fe7d7473ed
commit cc889a7f66
2 changed files with 19 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ltlvisit/tostring.cc
View file

@ -61,9 +61,11 @@ namespace spot
class to_string_visitor: public const_visitor class to_string_visitor: public const_visitor
{ {
public: public:
to_string_visitor(std::ostream& os, bool full_parent = false) to_string_visitor(std::ostream& os,
bool full_parent = false,
bool ratexp = false)
: os_(os), top_level_(true), : os_(os), top_level_(true),
full_parent_(full_parent), in_ratexp_(false) full_parent_(full_parent), in_ratexp_(ratexp)
{ {
} }
@ -552,18 +554,19 @@ namespace spot
} // anonymous } // anonymous
std::ostream& std::ostream&
to_string(const formula* f, std::ostream& os, bool full_parent) to_string(const formula* f, std::ostream& os, bool full_parent,
bool ratexp)
{ {
to_string_visitor v(os, full_parent); to_string_visitor v(os, full_parent, ratexp);
f->accept(v); f->accept(v);
return os; return os;
} }
std::string std::string
to_string(const formula* f, bool full_parent) to_string(const formula* f, bool full_parent, bool ratexp)
{ {
std::ostringstream os; std::ostringstream os;
to_string(f, os, full_parent); to_string(f, os, full_parent, ratexp);
return os.str(); return os.str();
} }

9
src/ltlvisit/tostring.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2010 Laboratoire de Recherche et Développement de // Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de
// l'Epita (LRDE). // l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -40,16 +40,19 @@ namespace spot
/// \param os The stream where it should be output. /// \param os The stream where it should be output.
/// \param full_parent Whether or not the string should by fully /// \param full_parent Whether or not the string should by fully
/// parenthesized. /// parenthesized.
/// \param ratexp Whether we are printing a SERE.
std::ostream& std::ostream&
to_string(const formula* f, std::ostream& os, bool full_parent = false); to_string(const formula* f, std::ostream& os, bool full_parent = false,
bool ratexp = false);
/// \brief Output a formula as a string which is parsable unless the formula /// \brief Output a formula as a string which is parsable unless the formula
/// contains automaton operators (used in ELTL formulae). /// contains automaton operators (used in ELTL formulae).
/// \param f The formula to translate. /// \param f The formula to translate.
/// \param full_parent Whether or not the string should by fully /// \param full_parent Whether or not the string should by fully
/// parenthesized. /// parenthesized.
/// \param ratexp Whether we are printing a SERE.
std::string std::string
to_string(const formula* f, bool full_parent = false); to_string(const formula* f, bool full_parent = false, bool ratexp = false);
/// \brief Output a formula as a (parsable by Spin) string. /// \brief Output a formula as a (parsable by Spin) string.
/// \param f The formula to translate. /// \param f The formula to translate.