From 9297d6dd9fbcd79f40b88f0f75ffad89122d6382 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 6 Jan 2004 16:56:07 +0000 Subject: [PATCH] * iface/gspn/eesrg.cc (format_state): Do not rewrite n's, just strip the last one. Escaping must be done at output. * iface/gspn/gspm.cc (format_state): Likewise. * src/misc/escape.hh, src/misc/escape.cc: New files. * src/misc/Makefile.am: Add them. * src/tgba/bddprint.cc (bdd_format_accset): New function. * src/tgba/bddprint.hh (bdd_format_accset): New function. * src/tgbaalgos/dotty.cc (dotty_bfs::process_state): Escape the state name using escape_str(). (dotty_bfs::process_link): Escape conditions and acceptance conditions using escape_str(). * src/tgbaalgos/save.cc (save_bfs::start): Call print_acc(). (save_bfs::print_acc): New function extracted from save_bfs::start(). Escape each acceptance condition. (save_bfs::process_state): Use escape_str() and print_acc() --- ChangeLog | 16 ++++++++++ iface/gspn/eesrg.cc | 25 ++++----------- iface/gspn/gspn.cc | 28 +++++------------ src/misc/Makefile.am | 4 ++- src/misc/escape.cc | 56 ++++++++++++++++++++++++++++++++++ src/misc/escape.hh | 36 ++++++++++++++++++++++ src/tgba/bddprint.cc | 10 +++++- src/tgba/bddprint.hh | 11 ++++++- src/tgbaalgos/dotty.cc | 18 ++++++----- src/tgbaalgos/save.cc | 69 ++++++++++++++++++------------------------ 10 files changed, 182 insertions(+), 91 deletions(-) create mode 100644 src/misc/escape.cc create mode 100644 src/misc/escape.hh diff --git a/ChangeLog b/ChangeLog index f1939b992..4bbdae96e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,21 @@ 2004-01-06 Alexandre Duret-Lutz + * iface/gspn/eesrg.cc (format_state): Do not rewrite \n's, + just strip the last one. Escaping must be done at output. + * iface/gspn/gspm.cc (format_state): Likewise. + * src/misc/escape.hh, src/misc/escape.cc: New files. + * src/misc/Makefile.am: Add them. + * src/tgba/bddprint.cc (bdd_format_accset): New function. + * src/tgba/bddprint.hh (bdd_format_accset): New function. + * src/tgbaalgos/dotty.cc (dotty_bfs::process_state): + Escape the state name using escape_str(). + (dotty_bfs::process_link): Escape conditions and acceptance + conditions using escape_str(). + * src/tgbaalgos/save.cc (save_bfs::start): Call print_acc(). + (save_bfs::print_acc): New function extracted from save_bfs::start(). + Escape each acceptance condition. + (save_bfs::process_state): Use escape_str() and print_acc() + * src/ltlvisit/tostring.cc (to_string_visitor::visit(const atomic_prop*)): Quote propositions that start with F, G, or X. diff --git a/iface/gspn/eesrg.cc b/iface/gspn/eesrg.cc index c09cc3131..edd0ad4cf 100644 --- a/iface/gspn/eesrg.cc +++ b/iface/gspn/eesrg.cc @@ -19,7 +19,6 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include #include #include #include @@ -422,7 +421,6 @@ namespace spot { const state_gspn_eesrg* s = dynamic_cast(state); assert(s); - std::ostringstream os; char* str; State gs = s->left(); if (gs) @@ -430,30 +428,19 @@ namespace spot int err = print_state(gs, &str); if (err) throw gspn_exeption("print_state()", err); + // Strip trailing \n... + unsigned len = strlen(str); + while (str[--len] == '\n') + str[len] = 0; } else { str = strdup("-1"); } - // Rewrite all new lines as \\\n. - const char* pos = str; - while (*pos) - { - switch (*pos) - { - // Rewrite all new lines as \\n, and strip the last one. - case '\n': - if (pos[1]) - os << "\\n"; - break; - default: - os << *pos; - } - ++pos; - } + std::string res(str); free(str); - return os.str() + " * " + data_->operand->format_state(s->right()); + return res + " * " + data_->operand->format_state(s->right()); } state* diff --git a/iface/gspn/gspn.cc b/iface/gspn/gspn.cc index 065aec991..9262f525e 100644 --- a/iface/gspn/gspn.cc +++ b/iface/gspn/gspn.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 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 // et Marie Curie. // @@ -19,7 +19,6 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include #include #include #include "gspn.hh" @@ -366,30 +365,17 @@ namespace spot { const state_gspn* s = dynamic_cast(state); assert(s); - std::ostringstream os; char* str; int err = print_state(s->get_state(), &str); if (err) throw gspn_exeption("print_state()", err); - - // Rewrite all new lines as \\\n. - const char* pos = str; - while (*pos) - { - switch (*pos) - { - // Rewrite all new lines as \\n, and strip the last one. - case '\n': - if (pos[1]) - os << "\\n"; - break; - default: - os << *pos; - } - ++pos; - } + // Strip trailing \n... + unsigned len = strlen(str); + while (str[--len] == '\n') + str[len] = 0; + std::string res(str); free(str); - return os.str(); + return res; } bdd diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am index 5d0088e67..3df125c71 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2003 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 ## et Marie Curie. ## @@ -27,6 +27,7 @@ miscdir = $(pkgincludedir)/misc misc_HEADERS = \ bddalloc.hh \ bddlt.hh \ + escape.hh \ hash.hh \ minato.hh \ version.hh @@ -34,5 +35,6 @@ misc_HEADERS = \ noinst_LTLIBRARIES = libmisc.la libmisc_la_SOURCES = \ bddalloc.cc \ + escape.cc \ minato.cc \ version.cc diff --git a/src/misc/escape.cc b/src/misc/escape.cc new file mode 100644 index 000000000..6b4b4ded0 --- /dev/null +++ b/src/misc/escape.cc @@ -0,0 +1,56 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include "escape.hh" + +namespace spot +{ + std::ostream& + escape_str(std::ostream& os, const std::string& str) + { + for (std::string::const_iterator i = str.begin(); i != str.end(); ++i) + switch (*i) + { + case '\\': + os << "\\\\"; + break; + case '"': + os << "\\\""; + break; + case '\n': + os << "\\n"; + break; + default: + os << *i; + break; + } + return os; + } + + std::string + escape_str(const std::string& str) + { + std::ostringstream os; + escape_str(os, str); + return os.str(); + } +} diff --git a/src/misc/escape.hh b/src/misc/escape.hh new file mode 100644 index 000000000..4ca2bd31a --- /dev/null +++ b/src/misc/escape.hh @@ -0,0 +1,36 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_MISC_ESCAPE_HH +# define SPOT_MISC_ESCAPE_HH + +# include +# include + +namespace spot +{ + /// Escape " and \ characters in \a str. + std::ostream& escape_str(std::ostream& os, const std::string& str); + /// Escape " and \ characters in \a str. + std::string escape_str(const std::string& str); +} + +#endif // SPOT_MISC_ESCAPE_HH diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index 37a9c22da..7b4f74989 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 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 // et Marie Curie. // @@ -160,6 +160,14 @@ namespace spot return os; } + std::string + bdd_format_accset(const bdd_dict* d, bdd b) + { + std::ostringstream os; + bdd_print_accset(os, d, b); + return os.str(); + } + std::string bdd_format_sat(const bdd_dict* d, bdd b) { diff --git a/src/tgba/bddprint.hh b/src/tgba/bddprint.hh index 1541ecaba..e970a2ab5 100644 --- a/src/tgba/bddprint.hh +++ b/src/tgba/bddprint.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 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 // et Marie Curie. // @@ -67,6 +67,15 @@ namespace spot std::ostream& bdd_print_accset(std::ostream& os, const bdd_dict* dict, bdd b); + /// \brief Format a BDD as a set of acceptance conditions. + /// + /// This is used when saving a TGBA. + /// \param os The output stream. + /// \param dict The dictionary to use, to lookup variables. + /// \param b The BDD to print. + /// \return The BDD formated as a string. + std::string bdd_format_accset(const bdd_dict* dict, bdd b); + /// \brief Print a BDD as a set. /// \param os The output stream. /// \param dict The dictionary to use, to lookup variables. diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index a5a6e2c0b..2e8e836a2 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 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 // et Marie Curie. // @@ -23,6 +23,7 @@ #include "dotty.hh" #include "tgba/bddprint.hh" #include "reachiter.hh" +#include "misc/escape.hh" namespace spot { @@ -52,19 +53,20 @@ namespace spot void process_state(const state* s, int n, tgba_succ_iterator*) { - os_ << " " << n << " [label=\"" - << automata_->format_state(s) << "\"]" << std::endl; + os_ << " " << n << " [label=\""; + escape_str(os_, automata_->format_state(s)) << "\"]" << std::endl; } void process_link(int in, int out, const tgba_succ_iterator* si) { os_ << " " << in << " -> " << out << " [label=\""; - bdd_print_formula(os_, automata_->get_dict(), - si->current_condition()) << "\\n"; - bdd_print_accset(os_, automata_->get_dict(), - si->current_acceptance_conditions()) << "\"]" - << std::endl; + escape_str(os_, bdd_format_formula(automata_->get_dict(), + si->current_condition())) << "\\n"; + escape_str(os_, + bdd_format_accset(automata_->get_dict(), + si->current_acceptance_conditions())) + << "\"]" << std::endl; } private: diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index 6f5128e58..0e96806b7 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -24,6 +24,7 @@ #include "tgba/bddprint.hh" #include "ltlvisit/tostring.hh" #include "reachiter.hh" +#include "misc/escape.hh" namespace spot { @@ -39,10 +40,34 @@ namespace spot void start() { - const bdd_dict* d = automata_->get_dict(); os_ << "acc ="; + print_acc(automata_->all_acceptance_conditions()) << ";" << std::endl; + } - bdd acc = automata_->all_acceptance_conditions(); + void + process_state(const state* s, int, tgba_succ_iterator* si) + { + const bdd_dict* d = automata_->get_dict(); + std::string cur = automata_->format_state(s); + for (si->first(); !si->done(); si->next()) + { + state* dest = si->current_state(); + os_ << "\"" << cur << "\", \"" + << automata_->format_state(dest) << "\", \""; + escape_str(os_, bdd_format_formula(d, si->current_condition())); + os_ << "\","; + print_acc(si->current_acceptance_conditions()) << ";" << std::endl; + delete dest; + } + } + + private: + std::ostream& os_; + + std::ostream& + print_acc(bdd acc) + { + const bdd_dict* d = automata_->get_dict(); while (acc != bddfalse) { bdd cube = bdd_satone(acc); @@ -59,50 +84,14 @@ namespace spot d->acc_formula_map.find(v); assert(vi != d->acc_formula_map.end()); os_ << " \""; - ltl::to_string(vi->second, os_) << "\""; + escape_str(os_, ltl::to_string(vi->second)) << "\""; break; } cube = bdd_low(cube); } } - os_ << ";" << std::endl; + return os_; } - - void - process_state(const state* s, int, tgba_succ_iterator* si) - { - const bdd_dict* d = automata_->get_dict(); - std::string cur = automata_->format_state(s); - for (si->first(); !si->done(); si->next()) - { - state* dest = si->current_state(); - os_ << "\"" << cur << "\", \"" - << automata_->format_state(dest) << "\", \""; - std::string s = bdd_format_formula(d, si->current_condition()); - // Escape " and \ characters in s. - for (std::string::const_iterator i = s.begin(); - i != s.end(); ++i) - switch (*i) - { - case '\\': - os_ << "\\\\"; - break; - case '"': - os_ << "\\\""; - break; - default: - os_ << *i; - break; - } - os_ << "\","; - bdd_print_acc(os_, d, si->current_acceptance_conditions()); - os_ << ";" << std::endl; - delete dest; - } - } - - private: - std::ostream& os_; };