From 8fb7b279f7090032d50b6718b8b6dc0de7351b1c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 Jun 2015 22:56:57 +0200 Subject: [PATCH] ltlvisit: rename tostring.hh as print.hh and rename printer functions This actually performs three related changes, but separating them would be quite inconvenient. 1) rename tostring.hh to print.hh a welcome side-effect is that I could fix several files that included this file for not reason. 2) de-overload some of the to_string functions, and rename them as follow: to_string -> print_psl, print_sere, str_psl, str_sere to_utf8_string -> print_utf8_psl, print_utf8_sere, str_utf8_psl, str_utf8_sere to_spin_string -> print_spin_ltl, str_spin_ltl to_wring_string -> print_wring_ltl, str_wing_ltl to_lbt_string -> print_lbt_ltl, str_lbt_ltl to_latex_string -> print_latex_psl, str_latex_psl to_sclatex_string -> print_sclatex_psl, str_sclatex_psl Now it is clearer what these functions do, and their restrictions. 3) all those print_* functions now take the stream to write onto as their first argument. This fixes #88. * src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh: Rename into... * src/ltlvisit/print.cc, src/ltlvisit/print.hh: ... those, and make the changes listed above. * doc/org/tut01.org, src/bin/common_output.cc, src/bin/common_trans.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/ltlfilt.cc, src/bin/randltl.cc, src/ltlparse/ltlparse.yy, src/ltlvisit/Makefile.am, src/ltlvisit/mark.cc, src/ltlvisit/relabel.cc, src/ltlvisit/simplify.cc, src/ltlvisit/snf.cc, src/ta/taexplicit.cc, src/ta/tgtaexplicit.cc, src/taalgos/tgba2ta.cc, src/tests/equalsf.cc, src/tests/ltl2tgba.cc, src/tests/ltlrel.cc, src/tests/randtgba.cc, src/tests/reduc.cc, src/tests/syntimpl.cc, src/tests/tostring.cc, src/twa/bdddict.cc, src/twa/bddprint.cc, src/twa/taatgba.cc, src/twa/taatgba.hh, src/twa/twagraph.cc, src/twaalgos/compsusp.cc, src/twaalgos/lbtt.cc, src/twaalgos/ltl2taa.cc, src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/neverclaim.cc, src/twaalgos/remprop.cc, src/twaalgos/stats.cc, wrap/python/ajax/spot.in, wrap/python/spot.py, wrap/python/spot_impl.i: Adjust. --- doc/org/tut01.org | 45 ++++--- src/bin/common_output.cc | 16 +-- src/bin/common_trans.cc | 10 +- src/bin/ltl2tgba.cc | 4 +- src/bin/ltl2tgta.cc | 4 +- src/bin/ltlcross.cc | 6 +- src/bin/ltldo.cc | 1 - src/bin/ltlfilt.cc | 4 +- src/bin/randltl.cc | 1 - src/ltlparse/ltlparse.yy | 6 +- src/ltlvisit/Makefile.am | 4 +- src/ltlvisit/mark.cc | 3 +- src/ltlvisit/{tostring.cc => print.cc} | 143 +++++++++++++------- src/ltlvisit/{tostring.hh => print.hh} | 179 ++++++++++++++++--------- src/ltlvisit/relabel.cc | 17 +-- src/ltlvisit/simplify.cc | 30 ++--- src/ltlvisit/snf.cc | 1 - src/ta/taexplicit.cc | 2 - src/ta/tgtaexplicit.cc | 6 +- src/taalgos/tgba2ta.cc | 1 - src/tests/equalsf.cc | 11 +- src/tests/ltl2tgba.cc | 8 +- src/tests/ltlrel.cc | 8 +- src/tests/randtgba.cc | 4 +- src/tests/reduc.cc | 14 +- src/tests/syntimpl.cc | 6 +- src/tests/tostring.cc | 11 +- src/twa/bdddict.cc | 11 +- src/twa/bddprint.cc | 16 +-- src/twa/taatgba.cc | 4 +- src/twa/taatgba.hh | 1 - src/twa/twagraph.cc | 4 +- src/twaalgos/compsusp.cc | 10 +- src/twaalgos/lbtt.cc | 4 +- src/twaalgos/ltl2taa.cc | 1 - src/twaalgos/ltl2tgba_fm.cc | 36 +---- src/twaalgos/neverclaim.cc | 8 +- src/twaalgos/remprop.cc | 1 - src/twaalgos/stats.cc | 4 +- wrap/python/ajax/spot.in | 8 +- wrap/python/spot.py | 14 +- wrap/python/spot_impl.i | 10 +- 42 files changed, 365 insertions(+), 312 deletions(-) rename src/ltlvisit/{tostring.cc => print.cc} (88%) rename src/ltlvisit/{tostring.hh => print.hh} (51%) diff --git a/doc/org/tut01.org b/doc/org/tut01.org index 71857cf15..541d36c87 100644 --- a/doc/org/tut01.org +++ b/doc/org/tut01.org @@ -65,14 +65,15 @@ exceptions. #+BEGIN_SRC C++ :results verbatim :exports both #include #include "ltlparse/public.hh" - #include "ltlvisit/tostring.hh" + #include "ltlvisit/print.hh" int main() { const spot::ltl::formula* f = spot::ltl::parse_formula("[]<>p0 || <>[]p1"); - to_lbt_string(f, std::cout) << '\n'; - to_spin_string(f, std::cout, true) << '\n'; - to_latex_string(spot::ltl::parse_formula("& & G p0 p1 p2"), std::cout); + print_lbt_ltl(std::cout, f) << '\n'; + print_spin_ltl(std::cout, f, true) << '\n'; + print_latex_psl(std::cout, spot::ltl::parse_formula("& & G p0 p1 p2")); + f->destroy(); } #+END_SRC @@ -81,6 +82,19 @@ exceptions. : ([](<>(p0))) || (<>([](p1))) : p_{1} \land p_{2} \land \G p_{0} +Notice that the different output routines specify in their name the +syntax the output, and the type of formula they expect. Here we are +only using LTL formulas for demonstration, so those three functions +are OK with that (LTL is a subset of PSL as far as Spot is concerned). +However if we input PSL formula, it's clear that the above code will +be a problem. If you want to add additional checks, you can easily +tests whether =f->is_ltl_formula()= returns true. + +Did you notice the calls to =f->destroy()= at the end? The LTL +formula objects are implemented as DAG with sharing of subformulas. +Each (sub)formula is therefore reference counted, and currently this +is done manually by calling =f->clone()= and =f->destroy()= (do not +ever =delete= a formula, always call =f->destroy()=). We do not recommend using this =parse_formula()= interface because of the potential formulas (like =f= or =t=) that have different meanings @@ -96,7 +110,7 @@ parser. Additionally, this give you control over how to print errors. #include #include #include "ltlparse/public.hh" - #include "ltlvisit/tostring.hh" + #include "ltlvisit/print.hh" int main() { @@ -109,8 +123,8 @@ parser. Additionally, this give you control over how to print errors. f->destroy(); return 1; } - to_lbt_string(f, std::cout) << '\n'; - to_spin_string(f, std::cout, true) << '\n'; + print_lbt_ltl(std::cout, f) << '\n'; + print_spin_ltl(std::cout, f, true) << '\n'; f->destroy(); } #+END_SRC @@ -144,7 +158,7 @@ with the "fixed" formula if you wish. Here is an example: #include #include #include "ltlparse/public.hh" - #include "ltlvisit/tostring.hh" + #include "ltlvisit/print.hh" int main() { @@ -156,8 +170,8 @@ with the "fixed" formula if you wish. Here is an example: (void) spot::ltl::format_parse_errors(std::cout, input, pel); if (f == nullptr) return 1; - to_lbt_string(f, std::cout) << '\n'; - to_spin_string(f, std::cout, true) << '\n'; + print_lbt_ltl(std::cout, f) << '\n'; + print_spin_ltl(std::cout, f, true) << '\n'; f->destroy(); } #+END_SRC @@ -180,13 +194,6 @@ U "a" "b" The formula =f= is only returned as null when the parser really cannot recover anything. -Did you notice the calls to =f->destroy()= in these two examples? The -LTL formula objects are implemented as DAG with sharing of -subformulas. Each (sub)formula is therefore reference counted, and -currently this is done manually by calling =f->clone()= and -=f->destroy()= (do not ever =delete= a formula, always call -=f->destroy()=). - ** Calling the prefix parser explicitly The only difference here is the call to =parse_prefix_ltl()= instead of @@ -196,7 +203,7 @@ The only difference here is the call to =parse_prefix_ltl()= instead of #include #include #include "ltlparse/public.hh" - #include "ltlvisit/tostring.hh" + #include "ltlvisit/print.hh" int main() { @@ -209,7 +216,7 @@ The only difference here is the call to =parse_prefix_ltl()= instead of f->destroy(); return 1; } - to_latex_string(f, std::cout) << '\n'; + print_latex_psl(std::cout, f) << '\n'; f->destroy(); } #+END_SRC diff --git a/src/bin/common_output.cc b/src/bin/common_output.cc index 37090fb44..0418946c7 100644 --- a/src/bin/common_output.cc +++ b/src/bin/common_output.cc @@ -21,7 +21,7 @@ #include "common_output.hh" #include #include -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "misc/formater.hh" #include "misc/escape.hh" #include "common_cout.hh" @@ -71,7 +71,7 @@ void report_not_ltl(const spot::ltl::formula* f, const char* filename, int linenum, const char* syn) { - std::string s = spot::ltl::to_string(f); + std::string s = spot::ltl::str_psl(f); static const char msg[] = "formula '%s' cannot be written %s's syntax because it is not LTL"; if (filename) @@ -88,30 +88,30 @@ stream_formula(std::ostream& out, { case lbt_output: if (f->is_ltl_formula()) - spot::ltl::to_lbt_string(f, out); + spot::ltl::print_lbt_ltl(out, f); else report_not_ltl(f, filename, linenum, "LBT"); break; case spot_output: - spot::ltl::to_string(f, out, full_parenth); + spot::ltl::print_psl(out, f, full_parenth); break; case spin_output: if (f->is_ltl_formula()) - spot::ltl::to_spin_string(f, out, full_parenth); + spot::ltl::print_spin_ltl(out, f, full_parenth); else report_not_ltl(f, filename, linenum, "Spin"); break; case wring_output: if (f->is_ltl_formula()) - spot::ltl::to_wring_string(f, out); + spot::ltl::print_wring_ltl(out, f); else report_not_ltl(f, filename, linenum, "Wring"); break; case utf8_output: - spot::ltl::to_utf8_string(f, out, full_parenth); + spot::ltl::print_utf8_psl(out, f, full_parenth); break; case latex_output: - spot::ltl::to_latex_string(f, out, full_parenth); + spot::ltl::print_latex_psl(out, f, full_parenth); break; case count_output: case quiet_output: diff --git a/src/bin/common_trans.cc b/src/bin/common_trans.cc index 6c8a9c751..8133586f1 100644 --- a/src/bin/common_trans.cc +++ b/src/bin/common_trans.cc @@ -28,7 +28,7 @@ #include "error.h" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "common_conv.hh" // A set of tools for which we know the correct output @@ -288,13 +288,13 @@ void translator_runner::round_formula(const spot::ltl::formula* f, unsigned serial) { if (has('f') || has('F')) - string_ltl_spot = spot::ltl::to_string(f, true); + string_ltl_spot = spot::ltl::str_psl(f, true); if (has('s') || has('S')) - string_ltl_spin = spot::ltl::to_spin_string(f, true); + string_ltl_spin = spot::ltl::str_spin_ltl(f, true); if (has('l') || has('L')) - string_ltl_lbt = spot::ltl::to_lbt_string(f); + string_ltl_lbt = spot::ltl::str_lbt_ltl(f); if (has('w') || has('W')) - string_ltl_wring = spot::ltl::to_wring_string(f); + string_ltl_wring = spot::ltl::str_wring_ltl(f); if (has('F')) string_to_tmp(string_ltl_spot, serial, filename_ltl_spot); if (has('S')) diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index df4534140..8de53a26e 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -34,7 +34,7 @@ #include "common_post.hh" #include "ltlast/formula.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "twaalgos/translate.hh" #include "misc/optionmap.hh" #include "misc/timer.hh" @@ -147,7 +147,7 @@ namespace // future-proof. if (!f->is_psl_formula()) { - std::string s = spot::ltl::to_string(f); + std::string s = spot::ltl::str_psl(f); error_at_line(2, 0, filename, linenum, "formula '%s' is not an LTL or PSL formula", s.c_str()); diff --git a/src/bin/ltl2tgta.cc b/src/bin/ltl2tgta.cc index b1b78b301..7580f6abc 100644 --- a/src/bin/ltl2tgta.cc +++ b/src/bin/ltl2tgta.cc @@ -33,7 +33,7 @@ #include "common_post.hh" #include "ltlparse/public.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "ltlvisit/simplify.hh" #include "twaalgos/dotty.hh" #include "twaalgos/ltl2tgba_fm.hh" @@ -181,7 +181,7 @@ namespace // future-proof. if (!f->is_psl_formula()) { - std::string s = spot::ltl::to_string(f); + std::string s = spot::ltl::str_psl(f); error_at_line(2, 0, filename, linenum, "formula '%s' is not an LTL or PSL formula", s.c_str()); diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 173ee70c9..b390cb697 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -40,7 +40,7 @@ #include "dstarparse/public.hh" #include "hoaparse/public.hh" #include "ltlast/unop.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "ltlvisit/apcollect.hh" #include "ltlvisit/mutation.hh" #include "ltlvisit/relabel.hh" @@ -971,9 +971,9 @@ namespace if (res) { if (lbt_input) - bogus = spot::ltl::to_lbt_string(f); + bogus = spot::ltl::str_lbt_ltl(f); else - bogus = spot::ltl::to_string(f); + bogus = spot::ltl::str_psl(f); if (bogus_output) bogus_output->ostream() << bogus << std::endl; } diff --git a/src/bin/ltldo.cc b/src/bin/ltldo.cc index f164174bb..7c9009fa1 100644 --- a/src/bin/ltldo.cc +++ b/src/bin/ltldo.cc @@ -35,7 +35,6 @@ #include "common_post.hh" #include "common_trans.hh" -#include "ltlvisit/tostring.hh" #include "ltlvisit/relabel.hh" #include "misc/bareword.hh" #include "misc/timer.hh" diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index a74ceeb80..cf58a67ba 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -42,7 +42,7 @@ #include "ltlvisit/remove_x.hh" #include "ltlvisit/apcollect.hh" #include "ltlvisit/exclusive.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "ltlast/unop.hh" #include "ltlast/multop.hh" #include "twaalgos/ltl2tgba_fm.hh" @@ -648,7 +648,7 @@ namespace // Sort the formulas alphabetically. std::map m; for (auto& p: relmap) - m.emplace(to_string(p.first), p.second); + m.emplace(str_psl(p.first), p.second); for (auto& p: m) stream_formula(output_define->ostream() << "#define " << p.first << " (", diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index 9ce5f2f18..4acd55102 100644 --- a/src/bin/randltl.cc +++ b/src/bin/randltl.cc @@ -36,7 +36,6 @@ #include "ltlast/multop.hh" #include "ltlast/unop.hh" #include "ltlvisit/randomltl.hh" -#include "ltlvisit/tostring.hh" #include "ltlvisit/length.hh" #include "ltlvisit/simplify.hh" #include "ltlenv/defaultenv.hh" diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 517e22044..c16ad59ff 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -36,7 +36,7 @@ #include #include "public.hh" #include "ltlast/allnodes.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" struct minmax_t { unsigned min, max; }; } @@ -240,8 +240,8 @@ using namespace spot::ltl; %destructor { $$->destroy(); } %printer { debug_stream() << *$$; } -%printer { spot::ltl::to_string($$, debug_stream()); } -%printer { spot::ltl::to_string($$, debug_stream(), false, true); } sere bracedsere +%printer { spot::ltl::print_psl(debug_stream(), $$); } +%printer { spot::ltl::print_sere(debug_stream(), $$); } sere bracedsere %printer { debug_stream() << $$; } %printer { debug_stream() << $$.min << ".." << $$.max; } diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index 08f989ab5..5c56a104e 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -36,6 +36,7 @@ ltlvisit_HEADERS = \ lunabbrev.hh \ mutation.hh \ nenoform.hh \ + print.hh \ postfix.hh \ randomltl.hh \ relabel.hh \ @@ -43,7 +44,6 @@ ltlvisit_HEADERS = \ simpfg.hh \ simplify.hh \ snf.hh \ - tostring.hh \ tunabbrev.hh \ wmunabbrev.hh @@ -61,6 +61,7 @@ libltlvisit_la_SOURCES = \ mark.hh \ mutation.cc \ nenoform.cc \ + print.cc \ postfix.cc \ randomltl.cc \ relabel.cc \ @@ -68,6 +69,5 @@ libltlvisit_la_SOURCES = \ simpfg.cc \ simplify.cc \ snf.cc \ - tostring.cc \ tunabbrev.cc \ wmunabbrev.cc diff --git a/src/ltlvisit/mark.cc b/src/ltlvisit/mark.cc index 6553e12bb..8afd03552 100644 --- a/src/ltlvisit/mark.cc +++ b/src/ltlvisit/mark.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2014 Laboratoire de Recherche et +// Copyright (C) 2010, 2012, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -23,7 +23,6 @@ #include #include #include -#include "ltlvisit/tostring.hh" #include "misc/casts.hh" namespace spot diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/print.cc similarity index 88% rename from src/ltlvisit/tostring.cc rename to src/ltlvisit/print.cc index 5b97e074b..1e05131f3 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/print.cc @@ -29,7 +29,7 @@ #include "ltlast/visitor.hh" #include "lunabbrev.hh" #include "wmunabbrev.hh" -#include "tostring.hh" +#include "print.hh" #include "misc/escape.hh" namespace spot @@ -912,44 +912,78 @@ namespace spot const char** kw_; }; + + std::ostream& + printer_(std::ostream& os, const formula* f, bool full_parent, + bool ratexp, const char** kw) + { + to_string_visitor v(os, full_parent, ratexp, kw); + f->accept(v); + return os; + } + + std::string + str_(const formula* f, bool full_parent, bool ratexp, const char** kw) + { + std::ostringstream os; + printer_(os, f, full_parent, ratexp, kw); + return os.str(); + } + } // anonymous std::ostream& - to_string(const formula* f, std::ostream& os, bool full_parent, - bool ratexp) + print_psl(std::ostream& os, const formula* f, bool full_parent) { - to_string_visitor v(os, full_parent, ratexp, spot_kw); - f->accept(v); - return os; + return printer_(os, f, full_parent, false, spot_kw); } std::string - to_string(const formula* f, bool full_parent, bool ratexp) + str_psl(const formula* f, bool full_parent) { - std::ostringstream os; - to_string(f, os, full_parent, ratexp); - return os.str(); + return str_(f, full_parent, false, spot_kw); } std::ostream& - to_utf8_string(const formula* f, std::ostream& os, bool full_parent, - bool ratexp) + print_sere(std::ostream& os, const formula* f, bool full_parent) { - to_string_visitor v(os, full_parent, ratexp, utf8_kw); - f->accept(v); - return os; + return printer_(os, f, full_parent, true, spot_kw); } std::string - to_utf8_string(const formula* f, bool full_parent, bool ratexp) + str_sere(const formula* f, bool full_parent) { - std::ostringstream os; - to_utf8_string(f, os, full_parent, ratexp); - return os.str(); + return str_(f, full_parent, false, spot_kw); + } + + + std::ostream& + print_utf8_psl(std::ostream& os, const formula* f, bool full_parent) + { + return printer_(os, f, full_parent, false, utf8_kw); + } + + std::string + str_utf8_psl(const formula* f, bool full_parent) + { + return str_(f, full_parent, false, utf8_kw); } std::ostream& - to_spin_string(const formula* f, std::ostream& os, bool full_parent) + print_utf8_sere(std::ostream& os, const formula* f, bool full_parent) + { + return printer_(os, f, full_parent, true, utf8_kw); + } + + std::string + str_utf8_sere(const formula* f, bool full_parent) + { + return str_(f, full_parent, false, utf8_kw); + } + + + std::ostream& + print_spin_ltl(std::ostream& os, const formula* f, bool full_parent) { // Remove xor, ->, and <-> first. const formula* fu = unabbreviate_logic(f); @@ -963,15 +997,15 @@ namespace spot } std::string - to_spin_string(const formula* f, bool full_parent) + str_spin_ltl(const formula* f, bool full_parent) { std::ostringstream os; - to_spin_string(f, os, full_parent); + print_spin_ltl(os, f, full_parent); return os.str(); } std::ostream& - to_wring_string(const formula* f, std::ostream& os) + print_wring_ltl(std::ostream& os, const formula* f) { // Remove W and M. f = unabbreviate_wm(f); @@ -982,47 +1016,60 @@ namespace spot } std::string - to_wring_string(const formula* f) + str_wring_ltl(const formula* f) { std::ostringstream os; - to_wring_string(f, os); + print_wring_ltl(os, f); return os.str(); } std::ostream& - to_latex_string(const formula* f, std::ostream& os, - bool full_parent, bool ratexp) + print_latex_psl(std::ostream& os, const formula* f, bool full_parent) { - to_string_visitor v(os, full_parent, ratexp, latex_kw); - f->accept(v); - return os; + return printer_(os, f, full_parent, false, latex_kw); } std::string - to_latex_string(const formula* f, - bool full_parent, bool ratexp) + str_latex_psl(const formula* f, bool full_parent) { - std::ostringstream os; - to_latex_string(f, os, full_parent, ratexp); - return os.str(); + return str_(f, full_parent, false, latex_kw); } std::ostream& - to_sclatex_string(const formula* f, std::ostream& os, - bool full_parent, bool ratexp) + print_latex_sere(std::ostream& os, const formula* f, bool full_parent) { - to_string_visitor v(os, full_parent, ratexp, sclatex_kw); - f->accept(v); - return os; + return printer_(os, f, full_parent, true, latex_kw); } std::string - to_sclatex_string(const formula* f, - bool full_parent, bool ratexp) + str_latex_sere(const formula* f, bool full_parent) { - std::ostringstream os; - to_sclatex_string(f, os, full_parent, ratexp); - return os.str(); + return str_(f, full_parent, true, latex_kw); + } + + + std::ostream& + print_sclatex_psl(std::ostream& os, const formula* f, bool full_parent) + { + return printer_(os, f, full_parent, false, sclatex_kw); + } + + std::string + str_sclatex_psl(const formula* f, bool full_parent) + { + return str_(f, full_parent, false, sclatex_kw); + } + + std::ostream& + print_sclatex_sere(std::ostream& os, const formula* f, bool full_parent) + { + return printer_(os, f, full_parent, true, sclatex_kw); + } + + std::string + str_sclatex_sere(const formula* f, bool full_parent) + { + return str_(f, full_parent, true, sclatex_kw); } namespace @@ -1199,7 +1246,7 @@ namespace spot } // anonymous std::ostream& - to_lbt_string(const formula* f, std::ostream& os) + print_lbt_ltl(std::ostream& os, const formula* f) { assert(f->is_ltl_formula()); lbt_visitor v(os); @@ -1208,10 +1255,10 @@ namespace spot } std::string - to_lbt_string(const formula* f) + str_lbt_ltl(const formula* f) { std::ostringstream os; - to_lbt_string(f, os); + print_lbt_ltl(os, f); return os.str(); } diff --git a/src/ltlvisit/tostring.hh b/src/ltlvisit/print.hh similarity index 51% rename from src/ltlvisit/tostring.hh rename to src/ltlvisit/print.hh index 150e134e7..cad3fefb5 100644 --- a/src/ltlvisit/tostring.hh +++ b/src/ltlvisit/print.hh @@ -32,117 +32,168 @@ namespace spot /// \addtogroup ltl_io /// @{ - /// \brief Output a formula as a string which is parsable unless the formula - /// contains automaton operators (used in ELTL formulae). - /// \param f The formula to translate. + /// \brief Output a PSL formula as a string which is parsable. /// \param os The stream where it should be output. - /// \param full_parent Whether or not the string should by fully - /// parenthesized. - /// \param ratexp Whether we are printing a SERE. - SPOT_API std::ostream& - 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 - /// contains automaton operators (used in ELTL formulae). /// \param f The formula to translate. /// \param full_parent Whether or not the string should by fully /// parenthesized. - /// \param ratexp Whether we are printing a SERE. + SPOT_API std::ostream& + print_psl(std::ostream& os, const formula* f, bool full_parent = false); + + /// \brief Convert a PSL formula into a string which is parsable + /// \param f The formula to translate. + /// \param full_parent Whether or not the string should by fully + /// parenthesized. SPOT_API std::string - to_string(const formula* f, bool full_parent = false, bool ratexp = false); + str_psl(const formula* f, bool full_parent = false); - /// \brief Output a formula as an utf8 string which is parsable unless - /// the formula contains automaton operators (used in ELTL formulae). - /// \param f The formula to translate. + /// \brief Output a PSL formula as an utf-8 string which is parsable. /// \param os The stream where it should be output. - /// \param full_parent Whether or not the string should by fully - /// parenthesized. - /// \param ratexp Whether we are printing a SERE. - SPOT_API std::ostream& - to_utf8_string(const formula* f, std::ostream& os, bool full_parent = false, - bool ratexp = false); - - /// \brief Output a formula as an utf8 string which is parsable - /// unless the formula contains automaton operators (used in ELTL formulae). /// \param f The formula to translate. /// \param full_parent Whether or not the string should by fully /// parenthesized. - /// \param ratexp Whether we are printing a SERE. - SPOT_API std::string - to_utf8_string(const formula* f, bool full_parent = false, - bool ratexp = false); - - /// \brief Output a formula as a string parsable by Spin. - /// \param f The formula to translate. - /// \param os The stream where it should be output. - /// \param full_parent Whether or not the string should by fully - /// parenthesized. SPOT_API std::ostream& - to_spin_string(const formula* f, std::ostream& os, + print_utf8_psl(std::ostream& os, const formula* f, bool full_parent = false); - /// \brief Convert a formula into a string parsable by Spin. + /// \brief Convert a PSL formula into a utf-8 string which is parsable /// \param f The formula to translate. /// \param full_parent Whether or not the string should by fully /// parenthesized. SPOT_API std::string - to_spin_string(const formula* f, bool full_parent = false); + str_utf8_psl(const formula* f, bool full_parent = false); - /// \brief Output a formula as a string parsable by Wring. + /// \brief Output a SERE formula as a string which is parsable. /// \param f The formula to translate. /// \param os The stream where it should be output. + /// \param full_parent Whether or not the string should by fully + /// parenthesized. SPOT_API std::ostream& - to_wring_string(const formula* f, std::ostream& os); + print_sere(std::ostream& os, const formula* f, bool full_parent = false); + + /// \brief Convert a SERE formula into a string which is parsable + /// \param f The formula to translate. + /// \param full_parent Whether or not the string should by fully + /// parenthesized. + SPOT_API std::string + str_sere(const formula* f, bool full_parent = false); + + /// \brief Output a SERE formula as a utf-8 string which is parsable. + /// \param os The stream where it should be output. + /// \param f The formula to translate. + /// \param full_parent Whether or not the string should by fully + /// parenthesized. + SPOT_API std::ostream& + print_utf8_sere(std::ostream& os, const formula* f, + bool full_parent = false); + + /// \brief Convert a SERE formula into a string which is parsable + /// \param f The formula to translate. + /// \param full_parent Whether or not the string should by fully + /// parenthesized. + SPOT_API std::string + str_utf8_sere(const formula* f, bool full_parent = false); + + /// \brief Output an LTL formula as a string parsable by Spin. + /// \param os The stream where it should be output. + /// \param f The formula to translate. + /// \param full_parent Whether or not the string should by fully + /// parenthesized. + SPOT_API std::ostream& + print_spin_ltl(std::ostream& os, const formula* f, + bool full_parent = false); + + /// \brief Convert an LTL formula into a string parsable by Spin. + /// \param f The formula to translate. + /// \param full_parent Whether or not the string should by fully + /// parenthesized. + SPOT_API std::string + str_spin_ltl(const formula* f, bool full_parent = false); + + /// \brief Output an LTL formula as a string parsable by Wring. + /// \param os The stream where it should be output. + /// \param f The formula to translate. + SPOT_API std::ostream& + print_wring_ltl(std::ostream& os, const formula* f); /// \brief Convert a formula into a string parsable by Wring /// \param f The formula to translate. SPOT_API std::string - to_wring_string(const formula* f); + str_wring_ltl(const formula* f); - /// \brief Output a formula as an LaTeX string which is parsable. - /// \param f The formula to translate. + /// \brief Output a PSL formula as a LaTeX string. /// \param os The stream where it should be output. + /// \param f The formula to translate. /// \param full_parent Whether or not the string should by fully /// parenthesized. - /// \param ratexp Whether we are printing a SERE. SPOT_API std::ostream& - to_latex_string(const formula* f, std::ostream& os, - bool full_parent = false, bool ratexp = false); + print_latex_psl(std::ostream& os, const formula* f, + bool full_parent = false); /// \brief Output a formula as a LaTeX string which is parsable. /// unless the formula contains automaton operators (used in ELTL formulae). /// \param f The formula to translate. /// \param full_parent Whether or not the string should by fully /// parenthesized. - /// \param ratexp Whether we are printing a SERE. SPOT_API std::string - to_latex_string(const formula* f, - bool full_parent = false, bool ratexp = false); + str_latex_psl(const formula* f, bool full_parent = false); - - /// \brief Output a formula as a self-contained LaTeX string. - /// - /// The result cannot be parsed back. - /// \param f The formula to translate. + /// \brief Output a SERE formula as a LaTeX string. /// \param os The stream where it should be output. + /// \param f The formula to translate. /// \param full_parent Whether or not the string should by fully /// parenthesized. - /// \param ratexp Whether we are printing a SERE. SPOT_API std::ostream& - to_sclatex_string(const formula* f, std::ostream& os, - bool full_parent = false, bool ratexp = false); + print_latex_sere(std::ostream& os, const formula* f, + bool full_parent = false); - /// \brief Output a formula as a self-contained LaTeX string. + /// \brief Output a SERE formula as a LaTeX string which is parsable. + /// unless the formula contains automaton operators (used in ELTL formulae). + /// \param f The formula to translate. + /// \param full_parent Whether or not the string should by fully + /// parenthesized. + SPOT_API std::string + str_latex_sere(const formula* f, bool full_parent = false); + + /// \brief Output a PSL formula as a self-contained LaTeX string. + /// + /// The result cannot be parsed back. + /// \param os The stream where it should be output. + /// \param f The formula to translate. + /// \param full_parent Whether or not the string should by fully + /// parenthesized. + SPOT_API std::ostream& + print_sclatex_psl(std::ostream& os, const formula* f, + bool full_parent = false); + + /// \brief Output a PSL formula as a self-contained LaTeX string. /// /// The result cannot be parsed bacl. /// \param f The formula to translate. /// \param full_parent Whether or not the string should by fully /// parenthesized. - /// \param ratexp Whether we are printing a SERE. SPOT_API std::string - to_sclatex_string(const formula* f, - bool full_parent = false, bool ratexp = false); + str_sclatex_psl(const formula* f, bool full_parent = false); + + /// \brief Output a SERE formula as a self-contained LaTeX string. + /// + /// The result cannot be parsed back. + /// \param os The stream where it should be output. + /// \param f The formula to translate. + /// \param full_parent Whether or not the string should by fully + /// parenthesized. + SPOT_API std::ostream& + print_sclatex_sere(std::ostream& os, const formula* f, + bool full_parent = false); + + /// \brief Output a SERE formula as a self-contained LaTeX string. + /// + /// The result cannot be parsed bacl. + /// \param f The formula to translate. + /// \param full_parent Whether or not the string should by fully + /// parenthesized. + SPOT_API std::string + str_sclatex_sere(const formula* f, bool full_parent = false); /// \brief Output an LTL formula as a string in LBT's format. /// @@ -155,7 +206,7 @@ namespace spot /// \param f The formula to translate. /// \param os The stream where it should be output. SPOT_API std::ostream& - to_lbt_string(const formula* f, std::ostream& os); + print_lbt_ltl(std::ostream& os, const formula* f); /// \brief Output an LTL formula as a string in LBT's format. /// @@ -167,7 +218,7 @@ namespace spot /// /// \param f The formula to translate. SPOT_API std::string - to_lbt_string(const formula* f); + str_lbt_ltl(const formula* f); /// @} } } diff --git a/src/ltlvisit/relabel.cc b/src/ltlvisit/relabel.cc index 73ca7f624..5ddacf40d 100644 --- a/src/ltlvisit/relabel.cc +++ b/src/ltlvisit/relabel.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -26,9 +26,7 @@ #include #include #include - #include -#include "tostring.hh" namespace spot { @@ -394,7 +392,6 @@ namespace spot while (!s.empty()) { - // std::cerr << "-- visiting " << to_string(s.top().parent) << '\n'; stack_entry& e = s.top(); if (e.current_child != e.last_child) { @@ -406,9 +403,6 @@ namespace spot ++e.current_child; continue; } - // std::cerr << " grand parent is " - // << to_string(e.grand_parent) - // << "\n child is " << to_string(child) << '\n'; auto i = data.emplace(std::piecewise_construct, std::forward_as_tuple(child), std::forward_as_tuple(num, num)); @@ -448,15 +442,6 @@ namespace spot dgrand_parent.low = dparent.low; } } - //std::cerr << " state of data:\n"; - //for (fmap_t::const_iterator i = data.begin(); - // i != data.end(); ++i) - // { - // std::cerr << " " << to_string(i->first) - // << " = { num=" << i->second.num - // << ", low=" << i->second.low - // << " }\n"; - // } } } diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index e2b0d8e2f..0330e373d 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -30,7 +30,7 @@ #include "ltlast/allnodes.hh" #include "ltlast/visitor.hh" #include "ltlvisit/contain.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "ltlvisit/snf.hh" #include "twa/formula2bdd.hh" #include @@ -280,8 +280,8 @@ namespace spot bool implication(const formula* f1, const formula* f2) { - trace << "[->] does " << to_string(f1) << " implies " - << to_string(f2) << " ?" << std::endl; + trace << "[->] does " << str_psl(f1) << " implies " + << str_psl(f2) << " ?" << std::endl; if ((options.synt_impl && syntactic_implication(f1, f2)) || (options.containment_checks && contained(f1, f2))) { @@ -318,8 +318,8 @@ namespace spot { if (!f1->is_psl_formula() || !f2->is_psl_formula()) return false; - trace << "[CN] Does (" << to_string(f1) << ") implies !(" - << to_string(f2) << ") ?" << std::endl; + trace << "[CN] Does (" << str_psl(f1) << ") implies !(" + << str_psl(f2) << ") ?" << std::endl; if (lcc.contained_neg(f1, f2)) { trace << "[CN] Yes" << std::endl; @@ -337,8 +337,8 @@ namespace spot { if (!f1->is_psl_formula() || !f2->is_psl_formula()) return false; - trace << "[NC] Does (" << to_string(f1) << ") implies !(" - << to_string(f2) << ") ?" << std::endl; + trace << "[NC] Does (" << str_psl(f1) << ") implies !(" + << str_psl(f2) << ") ?" << std::endl; if (lcc.neg_contained(f1, f2)) { trace << "[NC] Yes" << std::endl; @@ -359,8 +359,8 @@ namespace spot implication_neg(const formula* f1, const formula* f2, bool right) { trace << "[IN] Does " << (right ? "(" : "!(") - << to_string(f1) << ") implies " - << (right ? "!(" : "(") << to_string(f2) << ") ?" + << str_psl(f1) << ") implies " + << (right ? "!(" : "(") << str_psl(f2) << ") ?" << std::endl; if ((options.synt_impl && syntactic_implication_neg(f1, f2, right)) || (options.containment_checks && right && contained_neg(f1, f2)) @@ -4211,13 +4211,13 @@ namespace spot static int srec = 0; for (int i = srec; i; --i) trace << ' '; - trace << "** simplify_recursively(" << to_string(f) << ')'; + trace << "** simplify_recursively(" << str_psl(f) << ')'; #endif const formula* result = c->lookup_simplified(f); if (result) { - trace << " cached: " << to_string(result) << std::endl; + trace << " cached: " << str_psl(result) << std::endl; return result; } else @@ -4244,8 +4244,8 @@ namespace spot --srec; for (int i = srec; i; --i) trace << ' '; - trace << "** simplify_recursively(" << to_string(f) << ") result: " - << to_string(result) << std::endl; + trace << "** simplify_recursively(" << str_psl(f) << ") result: " + << str_psl(result) << std::endl; #endif c->cache_simplified(f, result); @@ -4656,8 +4656,8 @@ namespace spot { pairf p(f->clone(), g->clone()); syntimpl_[p] = result; - // std::cerr << to_string(f) << (result ? " ==> " : " =/=> ") - // << to_string(g) << std::endl; + // std::cerr << str_psl(f) << (result ? " ==> " : " =/=> ") + // << str_psl(g) << std::endl; } return result; diff --git a/src/ltlvisit/snf.cc b/src/ltlvisit/snf.cc index e187ab698..4cb3ac6a6 100644 --- a/src/ltlvisit/snf.cc +++ b/src/ltlvisit/snf.cc @@ -20,7 +20,6 @@ #include "snf.hh" #include "ltlast/allnodes.hh" #include "ltlast/visitor.hh" -#include "ltlvisit/tostring.hh" namespace spot { diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc index ebd168c78..a7bde3c08 100644 --- a/src/ta/taexplicit.cc +++ b/src/ta/taexplicit.cc @@ -31,8 +31,6 @@ #include "taexplicit.hh" #include "twa/formula2bdd.hh" #include -#include "ltlvisit/tostring.hh" - #include "twa/bddprint.hh" namespace spot diff --git a/src/ta/tgtaexplicit.cc b/src/ta/tgtaexplicit.cc index 6abb74035..678512f79 100644 --- a/src/ta/tgtaexplicit.cc +++ b/src/ta/tgtaexplicit.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2014 Laboratoire de Recherche et -// Developpement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2014, 2015 Laboratoire de Recherche +// et Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -21,8 +21,6 @@ #include "ltlast/constant.hh" #include "tgtaexplicit.hh" #include "twa/formula2bdd.hh" -#include "ltlvisit/tostring.hh" - #include "twa/bddprint.hh" namespace spot diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index 900628be3..4d5eeff80 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -30,7 +30,6 @@ #include "ltlast/constant.hh" #include "twa/formula2bdd.hh" #include -#include "ltlvisit/tostring.hh" #include #include "twa/bddprint.hh" #include diff --git a/src/tests/equalsf.cc b/src/tests/equalsf.cc index 471d16234..8d4e1238f 100644 --- a/src/tests/equalsf.cc +++ b/src/tests/equalsf.cc @@ -34,7 +34,7 @@ #include "ltlvisit/nenoform.hh" #include "ltlast/allnodes.hh" #include "ltlvisit/simplify.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" void syntax(char* prog) @@ -165,8 +165,7 @@ main(int argc, char** argv) { std::cerr << "Source and simplified formulae are not equivalent!\n"; - std::cerr - << "Simplified: " << spot::ltl::to_string(f1) << '\n'; + spot::ltl::print_psl(std::cerr << "Simplified: ", f1) << '\n'; exit_code = 1; } @@ -188,8 +187,7 @@ main(int argc, char** argv) { std::cerr << "Source and simplified formulae are not equivalent!\n"; - std::cerr - << "Simplified: " << spot::ltl::to_string(f1) << '\n'; + spot::ltl::print_psl(std::cerr << "Simplified: ", f1) << '\n'; exit_code = 1; } @@ -211,8 +209,7 @@ main(int argc, char** argv) { std::cerr << "Source and simplified formulae are not equivalent!\n"; - std::cerr - << "Simplified: " << spot::ltl::to_string(f1) << '\n'; + spot::ltl::print_psl(std::cerr << "Simplified: ", f1) << '\n'; exit_code = 1; } diff --git a/src/tests/ltl2tgba.cc b/src/tests/ltl2tgba.cc index 7399ec625..9cee95f9d 100644 --- a/src/tests/ltl2tgba.cc +++ b/src/tests/ltl2tgba.cc @@ -26,7 +26,7 @@ #include #include #include -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "ltlvisit/apcollect.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" @@ -1041,9 +1041,9 @@ checked_main(int argc, char** argv) if (display_reduced_form) { if (utf8_opt) - std::cout << spot::ltl::to_utf8_string(f) << std::endl; + print_utf8_psl(std::cout, f) << '\n'; else - std::cout << spot::ltl::to_string(f) << std::endl; + print_psl(std::cout, f) << '\n'; } // This helps ltl_to_tgba_fm() to order BDD variables in // a more natural way. @@ -1470,7 +1470,7 @@ checked_main(int argc, char** argv) } if (f) - a->set_named_prop("automaton-name", new std::string(to_string(f))); + a->set_named_prop("automaton-name", new std::string(str_psl(f))); if (output != -1) { diff --git a/src/tests/ltlrel.cc b/src/tests/ltlrel.cc index c977e39a1..723e4d35a 100644 --- a/src/tests/ltlrel.cc +++ b/src/tests/ltlrel.cc @@ -23,7 +23,7 @@ #include "ltlparse/public.hh" #include "ltlvisit/relabel.hh" #include "ltlast/allnodes.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" void syntax(char *prog) @@ -47,15 +47,15 @@ main(int argc, char **argv) spot::ltl::relabeling_map* m = new spot::ltl::relabeling_map; const spot::ltl::formula* f2 = spot::ltl::relabel_bse(f1, spot::ltl::Pnn, m); f1->destroy(); - spot::ltl::to_string(f2, std::cout) << '\n'; + spot::ltl::print_psl(std::cout, f2) << '\n'; typedef std::map map_t; map_t sorted_map; for (spot::ltl::relabeling_map::const_iterator i = m->begin(); i != m->end(); ++i) - sorted_map[spot::ltl::to_string(i->first)] = - spot::ltl::to_string(i->second); + sorted_map[spot::ltl::str_psl(i->first)] = + spot::ltl::str_psl(i->second); for (map_t::const_iterator i = sorted_map.begin(); i != sorted_map.end(); ++i) std::cout << " " << i->first << " -> " diff --git a/src/tests/randtgba.cc b/src/tests/randtgba.cc index d4d57372d..93159b90a 100644 --- a/src/tests/randtgba.cc +++ b/src/tests/randtgba.cc @@ -33,7 +33,7 @@ #include "ltlparse/public.hh" #include "ltlvisit/apcollect.hh" #include "ltlvisit/randomltl.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "ltlvisit/length.hh" #include "ltlvisit/simplify.hh" #include "twaalgos/randomgraph.hh" @@ -527,7 +527,7 @@ generate_formula(const spot::ltl::random_ltl& rl, << "of size " << opt_l << " or more." << std::endl; return 0; } - std::string txt = spot::ltl::to_string(f); + std::string txt = spot::ltl::str_psl(f); if (!opt_u || unique.insert(txt).second) { return f; diff --git a/src/tests/reduc.cc b/src/tests/reduc.cc index 0355854ac..38187fe93 100644 --- a/src/tests/reduc.cc +++ b/src/tests/reduc.cc @@ -28,7 +28,7 @@ #include #include "ltlparse/public.hh" #include "ltlvisit/dump.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "ltlvisit/simplify.hh" #include "ltlvisit/length.hh" #include "ltlast/allnodes.hh" @@ -214,7 +214,7 @@ main(int argc, char** argv) ftmp1->destroy(); int length_f1_before = spot::ltl::length(f1); - std::string f1s_before = spot::ltl::to_string(f1); + std::string f1s_before = spot::ltl::str_psl(f1); std::string f1l; const spot::ltl::formula* input_f = f1; @@ -222,14 +222,14 @@ main(int argc, char** argv) if (!simp_size->are_equivalent(input_f, f1)) { std::cerr << "Incorrect reduction from `" << f1s_before - << "' to `" << spot::ltl::to_string(f1) << "'." - << std::endl; + << "' to `"; + print_psl(std::cerr, f1) << "'.\n"; exit_code = 3; } else { const spot::ltl::formula* maybe_larger = simp->simplify(input_f); - f1l = spot::ltl::to_string(maybe_larger); + f1l = spot::ltl::str_psl(maybe_larger); if (!simp->are_equivalent(input_f, maybe_larger)) { std::cerr << "Incorrect reduction (reduce_size_strictly=0) from `" @@ -242,7 +242,7 @@ main(int argc, char** argv) input_f->destroy(); int length_f1_after = spot::ltl::length(f1); - std::string f1s_after = spot::ltl::to_string(f1); + std::string f1s_after = spot::ltl::str_psl(f1); std::string f2s = ""; if (f2) @@ -250,7 +250,7 @@ main(int argc, char** argv) ftmp1 = f2; f2 = simp_size->negative_normal_form(f2, false); ftmp1->destroy(); - f2s = spot::ltl::to_string(f2); + f2s = spot::ltl::str_psl(f2); } sum_before += length_f1_before; diff --git a/src/tests/syntimpl.cc b/src/tests/syntimpl.cc index f5ac31837..27c999a7a 100644 --- a/src/tests/syntimpl.cc +++ b/src/tests/syntimpl.cc @@ -27,7 +27,7 @@ #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/tunabbrev.hh" #include "ltlvisit/dump.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "ltlvisit/simplify.hh" #include "ltlast/allnodes.hh" #include "ltlvisit/nenoform.hh" @@ -62,8 +62,8 @@ main(int argc, char** argv) const spot::ltl::formula* f1 = spot::ltl::negative_normal_form(ftmp1); const spot::ltl::formula* f2 = spot::ltl::negative_normal_form(ftmp2); - std::string f1s = spot::ltl::to_string(f1); - std::string f2s = spot::ltl::to_string(f2); + std::string f1s = spot::ltl::str_psl(f1); + std::string f2s = spot::ltl::str_psl(f2); int exit_return = 0; spot::ltl::ltl_simplifier* c = new spot::ltl::ltl_simplifier; diff --git a/src/tests/tostring.cc b/src/tests/tostring.cc index d798ecc32..720f8001a 100644 --- a/src/tests/tostring.cc +++ b/src/tests/tostring.cc @@ -24,7 +24,7 @@ #include #include #include "ltlparse/public.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "ltlast/allnodes.hh" void @@ -49,8 +49,8 @@ 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::cout << f1s << std::endl; + std::string f1s = spot::ltl::str_psl(f1); + std::cout << f1s << '\n'; auto* f2 = spot::ltl::parse_infix_psl(f1s, p1); @@ -64,8 +64,8 @@ main(int argc, char **argv) // It should also map to the same string. - std::string f2s = spot::ltl::to_string(f2); - std::cout << f2s << std::endl; + std::string f2s = spot::ltl::str_psl(f2); + std::cout << f2s << '\n'; if (f2s != f1s) return 1; @@ -76,5 +76,6 @@ main(int argc, char **argv) assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); + assert(spot::ltl::bunop::instance_count() == 0); return 0; } diff --git a/src/twa/bdddict.cc b/src/twa/bdddict.cc index 321d8f42f..9a4d57651 100644 --- a/src/twa/bdddict.cc +++ b/src/twa/bdddict.cc @@ -23,8 +23,7 @@ #include #include #include -#include -#include +#include #include #include #include "priv/bddalloc.hh" @@ -199,7 +198,7 @@ namespace spot std::ostringstream s; // FIXME: We could be smarter and reuse unused "$n" numbers. - s << ltl::to_string(i.f) << '$' << ++i.clone_counts; + ltl::print_psl(s, i.f) << '$' << ++i.clone_counts; const ltl::formula* f = ltl::atomic_prop::instance(s.str(), ltl::default_environment::instance()); @@ -378,10 +377,12 @@ namespace spot os << (r.refs.empty() ? "Free" : "Anon"); break; case acc: - os << "Acc[" << to_string(r.f) << ']'; + os << "Acc["; + print_psl(os, r.f) << ']'; break; case var: - os << "Var[" << to_string(r.f) << ']'; + os << "Var["; + print_psl(os, r.f) << ']'; break; } if (!r.refs.empty()) diff --git a/src/twa/bddprint.cc b/src/twa/bddprint.cc index 4becfd38e..ea849d9c4 100644 --- a/src/twa/bddprint.cc +++ b/src/twa/bddprint.cc @@ -24,7 +24,7 @@ #include #include #include "bddprint.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "formula2bdd.hh" #include "misc/minato.hh" @@ -40,12 +40,12 @@ namespace spot static bool utf8; static - std::ostream& print_ltl(const ltl::formula* f, std::ostream& o) + std::ostream& print_(std::ostream& o, const ltl::formula* f) { if (utf8) - ltl::to_utf8_string(f, o); + ltl::print_utf8_psl(o, f); else - ltl::to_string(f, o); + ltl::print_psl(o, f); return o; } @@ -58,18 +58,18 @@ namespace spot switch (ref.type) { case bdd_dict::var: - to_string(ref.f, o); + print_(o, ref.f); break; case bdd_dict::acc: if (want_acc) { o << "Acc["; - print_ltl(ref.f, o) << ']'; + print_(o, ref.f) << ']'; } else { o << '"'; - print_ltl(ref.f, o) << '"'; + print_(o, ref.f) << '"'; } break; case bdd_dict::anon: @@ -173,7 +173,7 @@ namespace spot bdd_print_formula(std::ostream& os, const bdd_dict_ptr& d, bdd b) { const ltl::formula* f = bdd_to_formula(b, d); - print_ltl(f, os); + print_(os, f); f->destroy(); return os; } diff --git a/src/twa/taatgba.cc b/src/twa/taatgba.cc index 5efc0cf54..1f37ceeef 100644 --- a/src/twa/taatgba.cc +++ b/src/twa/taatgba.cc @@ -22,7 +22,7 @@ #include #include #include "twa/formula2bdd.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "ltlvisit/clone.hh" #include "taatgba.hh" @@ -360,7 +360,7 @@ namespace spot std::string taa_tgba_formula::label_to_string(const label_t& label) const { - return ltl::to_string(label); + return ltl::str_psl(label); } const ltl::formula* diff --git a/src/twa/taatgba.hh b/src/twa/taatgba.hh index 9cfcb019d..7394bfea8 100644 --- a/src/twa/taatgba.hh +++ b/src/twa/taatgba.hh @@ -27,7 +27,6 @@ #include "ltlast/formula.hh" #include "bdddict.hh" #include "twa.hh" -#include "ltlvisit/tostring.hh" namespace spot { diff --git a/src/twa/twagraph.cc b/src/twa/twagraph.cc index 10eb6a409..d2ea465b4 100644 --- a/src/twa/twagraph.cc +++ b/src/twa/twagraph.cc @@ -19,7 +19,7 @@ #include "twagraph.hh" #include "ltlast/constant.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" namespace spot { @@ -38,7 +38,7 @@ namespace spot auto f = n[i]; if (f) { - (*v)[i] = to_string(f); + (*v)[i] = str_psl(f); f->destroy(); } } diff --git a/src/twaalgos/compsusp.cc b/src/twaalgos/compsusp.cc index fb115cb23..57ceecb4b 100644 --- a/src/twaalgos/compsusp.cc +++ b/src/twaalgos/compsusp.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -26,7 +26,7 @@ #include "simulation.hh" #include "safety.hh" #include "ltlast/allnodes.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "ltlvisit/clone.hh" #include #include @@ -167,8 +167,7 @@ namespace spot std::ostringstream s; s << "〈"; - to_string(f, s); - s << "〉"; + print_psl(s, f) << "〉"; res = suspenv.require(s.str()); // We have to clone f, because it is not always a sub-tree // of the original formula. (Think n-ary operators.) @@ -184,8 +183,7 @@ namespace spot std::ostringstream s; s << '['; - to_string(f, s); - s << ']'; + print_psl(s, f) << ']'; res = suspenv.require(s.str()); // We have to clone f, because it is not always a sub-tree // of the original formula. (Think n-ary operators.) diff --git a/src/twaalgos/lbtt.cc b/src/twaalgos/lbtt.cc index f9b81cb50..4dfb376ca 100644 --- a/src/twaalgos/lbtt.cc +++ b/src/twaalgos/lbtt.cc @@ -28,7 +28,7 @@ #include "reachiter.hh" #include "misc/bddlt.hh" #include "priv/accmap.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "ltlparse/public.hh" namespace spot @@ -107,7 +107,7 @@ namespace spot } const ltl::formula* f = bdd_to_formula(si->current_condition(), aut_->get_dict()); - to_lbt_string(f, body_); + print_lbt_ltl(body_, f); f->destroy(); body_ << '\n'; } diff --git a/src/twaalgos/ltl2taa.cc b/src/twaalgos/ltl2taa.cc index 09c2d60df..92b484dc0 100644 --- a/src/twaalgos/ltl2taa.cc +++ b/src/twaalgos/ltl2taa.cc @@ -24,7 +24,6 @@ #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/tunabbrev.hh" #include "ltlvisit/nenoform.hh" -#include "ltlvisit/tostring.hh" #include "ltlvisit/contain.hh" #include "ltl2taa.hh" diff --git a/src/twaalgos/ltl2tgba_fm.cc b/src/twaalgos/ltl2tgba_fm.cc index b2ce03ba0..8b16af870 100644 --- a/src/twaalgos/ltl2tgba_fm.cc +++ b/src/twaalgos/ltl2tgba_fm.cc @@ -26,11 +26,11 @@ #include "ltlast/visitor.hh" #include "ltlast/allnodes.hh" #include "ltlvisit/nenoform.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "ltlvisit/postfix.hh" #include "ltlvisit/apcollect.hh" #include "ltlvisit/mark.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include #include #include @@ -392,7 +392,7 @@ namespace spot for (auto& fi: next_map) { os << " " << fi.second << ": Next["; - to_string(fi.first, os) << ']' << std::endl; + print_psl(os, fi.first) << ']' << std::endl; } os << "Shared Dict:" << std::endl; dict->dump(os); @@ -513,9 +513,8 @@ namespace spot bdd dest_bdd = bdd_existcomp(cube, d.next_set); const formula* dest = d.conj_bdd_to_formula(dest_bdd); bdd_print_set(std::cerr, d.dict, label) << " => "; - bdd_print_set(std::cerr, d.dict, dest_bdd) << " = " - << to_string(dest) - << '\n'; + bdd_print_set(std::cerr, d.dict, dest_bdd) << " = "; + print_psl(std::cerr, dest) << '\n'; dest->destroy(); } return std::cerr; @@ -1071,14 +1070,6 @@ namespace spot translate_ratexp(const formula* f, translate_dict& dict, const formula* to_concat) { - // static unsigned indent = 0; - // for (unsigned i = indent; i > 0; --i) - // std::cerr << "| "; - // std::cerr << "translate_ratexp[" << to_string(f); - // if (to_concat) - // std::cerr << ", " << to_string(to_concat); - // std::cerr << ']' << std::endl; - // ++indent; bdd res; if (!f->is_boolean()) { @@ -1096,11 +1087,6 @@ namespace spot res &= bdd_ithvar(x); to_concat->destroy(); } - // --indent; - // for (unsigned i = indent; i > 0; --i) - // std::cerr << "| "; - // std::cerr << "\\ "; - // bdd_print_set(std::cerr, dict.dict, res) << std::endl; return res; } @@ -1834,11 +1820,6 @@ namespace spot formula_set implied; implied_subformulae(node, implied); - // std::cerr << "---" << std::endl; - // for (formula_set::const_iterator i = implied.begin(); - // i != implied.end(); ++i) - // std::cerr << to_string(*i) << std::endl; - res_ = bddtrue; unsigned s = node->size(); for (unsigned n = 0; n < s; ++n) @@ -1860,13 +1841,8 @@ namespace spot // G(Fa & Fb) get optimized. See the comment in // the case handling G. bdd res = recurse(sub, recurring_); - //std::cerr << "== in And (" << to_string(sub) - // << ')' << std::endl; - // trace_ltl_bdd(dict_, res); res_ &= res; } - //std::cerr << "=== And final" << std::endl; - // trace_ltl_bdd(dict_, res_); break; } case multop::Or: @@ -2111,7 +2087,7 @@ namespace spot translate_dict::translated t = d_.ltl_to_bdd(f, !f->is_marked()); // std::cerr << "-----" << std::endl; - // std::cerr << "Formula: " << to_string(f) << std::endl; + // std::cerr << "Formula: " << str_psl(f) << std::endl; // std::cerr << "Rational: " << t.has_rational << std::endl; // std::cerr << "Marked: " << t.has_marked << std::endl; // std::cerr << "Mark all: " << !f->is_marked() << std::endl; diff --git a/src/twaalgos/neverclaim.cc b/src/twaalgos/neverclaim.cc index 38daf1a2c..992bf8cea 100644 --- a/src/twaalgos/neverclaim.cc +++ b/src/twaalgos/neverclaim.cc @@ -26,7 +26,7 @@ #include "twa/bddprint.hh" #include "twa/twagraph.hh" #include "reachiter.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "twa/formula2bdd.hh" namespace spot @@ -151,11 +151,13 @@ namespace spot else os_ << " :: ("; const ltl::formula* f = bdd_to_formula(t.cond, aut_->get_dict()); - to_spin_string(f, os_, true); + // This is actually a Boolean formula, but the LTL printer + // is all we have. + print_spin_ltl(os_, f, true); if (atom) { os_ << ") -> assert(!("; - to_spin_string(f, os_, true); + print_spin_ltl(os_, f, true); os_ << ")) }"; } else diff --git a/src/twaalgos/remprop.cc b/src/twaalgos/remprop.cc index b6819c606..59d5160dc 100644 --- a/src/twaalgos/remprop.cc +++ b/src/twaalgos/remprop.cc @@ -21,7 +21,6 @@ #include "ltlenv/defaultenv.hh" #include "twaalgos/mask.hh" #include "misc/casts.hh" -#include "ltlvisit/tostring.hh" #include #include diff --git a/src/twaalgos/stats.cc b/src/twaalgos/stats.cc index aa960c784..12d211676 100644 --- a/src/twaalgos/stats.cc +++ b/src/twaalgos/stats.cc @@ -25,7 +25,7 @@ #include "twa/twa.hh" #include "stats.hh" #include "reachiter.hh" -#include "ltlvisit/tostring.hh" +#include "ltlvisit/print.hh" #include "twaalgos/isdet.hh" #include "twaalgos/sccinfo.hh" @@ -137,7 +137,7 @@ namespace spot void printable_formula::print(std::ostream& os, const char*) const { - ltl::to_string(val_, os); + ltl::print_psl(os, val_); }; stat_printer::stat_printer(std::ostream& os, const char* format) diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 3e2236370..d985eaddf 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -460,7 +460,7 @@ if output_type == 'f': unbufprint(format_formula(f)) elif formula_format == 'i': unbufprint('
' - + spot.to_spin_string(f) + '
') + + spot.str_spin_ltl(f) + '') if f.is_psl_formula() and not f.is_ltl_formula(): s = '' if simpopt.reduce_size_strictly: @@ -470,12 +470,12 @@ if output_type == 'f': if not f.is_ltl_formula(): unbufprint('
PSL formulas cannot be expressed in this format.
') else: - unbufprint('
' + spot.to_lbt_string(f) + '
') + unbufprint('
' + spot.str_lbt_ltl(f) + '
') elif formula_format == 'g': render_formula(f) elif formula_format == 'p': if utf8: - s = spot.to_utf8_string(f) + s = spot.str_utf8_psl(f) else: s = str(f) unbufprint('Properties for ' + format_formula(f, 'span') + '
    \n') @@ -574,7 +574,7 @@ elif translator == 'l3': l3opt.remove('-p') args = ["@LTL3BA@", l3out] args.extend(l3opt) - args.extend(['-f', spot.to_spin_string(f)]) + args.extend(['-f', spot.str_spin_ltl(f)]) import subprocess l3file = tmpdir + "/aut" with open(l3file, "w+") as l3aut: diff --git a/wrap/python/spot.py b/wrap/python/spot.py index 74ad828c4..c61c2d9d1 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -100,19 +100,19 @@ def _formula_str_ctor(self, str): def _formula_to_str(self, format = 'spot', parenth = False): if format == 'spot': - return to_string(self, parenth) + return str_psl(self, parenth) elif format == 'spin': - return to_spin_string(self, parenth) + return str_spin_ltl(self, parenth) elif format == 'utf8': - return to_utf8_string(self, parenth) + return str_utf8_psl(self, parenth) elif format == 'lbt': - return to_lbt_string(self) + return str_lbt_ltl(self) elif format == 'wring': - return to_wring_string(self) + return str_wring_ltl(self) elif format == 'latex': - return to_latex_string(self, parenth) + return str_latex_psl(self, parenth) elif format == 'sclatex': - return to_sclatex_string(self, parenth) + return str_sclatex_psl(self, parenth) else: raise ValueError("unknown string format: " + format) diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 5580c5ef8..bbf5f2ff1 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -101,8 +101,8 @@ namespace std { #include "ltlvisit/dump.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/nenoform.hh" +#include "ltlvisit/print.hh" #include "ltlvisit/simplify.hh" -#include "ltlvisit/tostring.hh" #include "ltlvisit/tunabbrev.hh" #include "ltlvisit/randomltl.hh" #include "ltlvisit/length.hh" @@ -243,8 +243,8 @@ using namespace spot; %include "ltlvisit/dump.hh" %include "ltlvisit/lunabbrev.hh" %include "ltlvisit/nenoform.hh" +%include "ltlvisit/print.hh" %include "ltlvisit/simplify.hh" -%include "ltlvisit/tostring.hh" %include "ltlvisit/tunabbrev.hh" %include "ltlvisit/randomltl.hh" %include "ltlvisit/length.hh" @@ -336,12 +336,12 @@ spot::ltl::formula_ptr_less_than>; size_t __hash__() { return self->hash(); } - std::string __repr__() { return spot::ltl::to_string(self); } + std::string __repr__() { return spot::ltl::str_psl(self); } std::string _repr_latex_() { - return std::string("$") + spot::ltl::to_sclatex_string(self) + '$'; + return std::string("$") + spot::ltl::str_sclatex_psl(self) + '$'; } - std::string __str__() { return spot::ltl::to_string(self); } + std::string __str__() { return spot::ltl::str_psl(self); } } %extend spot::acc_cond::acc_code {