diff --git a/src/ltltest/randltl.cc b/src/ltltest/randltl.cc index 94f5906e3..0321194db 100644 --- a/src/ltltest/randltl.cc +++ b/src/ltltest/randltl.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2005 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// 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. // @@ -47,6 +48,7 @@ syntax(char* prog) << " -P generate PSL formulae" << std::endl << std::endl << "Options:" << std::endl + << " -8 output in UTF-8" << std::endl << " -d dump priorities, do not generate any formula" << std::endl << " -f N the size of the formula [15]" << std::endl @@ -89,6 +91,7 @@ main(int argc, char** argv) { enum { OutputBool, OutputLTL, OutputSERE, OutputPSL } output = OutputLTL; bool opt_d = false; + bool utf8 = false; int opt_s = 0; int opt_f = 15; int opt_F = 1; @@ -110,7 +113,11 @@ main(int argc, char** argv) while (++argn < argc) { - if (!strcmp(argv[argn], "-B")) + if (!strcmp(argv[argn], "-8")) + { + utf8 = true; + } + else if (!strcmp(argv[argn], "-B")) { output = OutputBool; } @@ -341,8 +348,9 @@ main(int argc, char** argv) << "of size " << opt_r << " or more." << std::endl; exit(2); } - std::string txt = spot::ltl::to_string(f, false, - output == OutputSERE); + std::string txt = utf8 + ? spot::ltl::to_utf8_string(f, false, output == OutputSERE) + : spot::ltl::to_string(f, false, output == OutputSERE); f->destroy(); if (!opt_u || unique.insert(txt).second) { diff --git a/src/ltltest/utf8.test b/src/ltltest/utf8.test index 9527cec09..3527f10bd 100755 --- a/src/ltltest/utf8.test +++ b/src/ltltest/utf8.test @@ -70,3 +70,7 @@ ignoring trailing garbage EOF cmp exp err + + +../randltl -P -8 -u -s 0 -f 16 a b c -F 100 > formulae +../reduc -f -h 0 formulae \ No newline at end of file diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index ab6d3d076..4f2774b1f 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -1,3 +1,4 @@ +// -*- coding: utf-8 -*- // Copyright (C) 2008, 2010, 2012 Laboratoire de Recherche et // Développement de l'Epita (LRDE) // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), @@ -79,12 +80,12 @@ namespace spot " R ", " W ", " M ", - " <>-> ", - " <>=> ", - " <>+> ", - " <>=+> ", - " []-> ", - " []=> ", + "<>-> ", + "<>=> ", + "<>+> ", + "<>=+> ", + "[]-> ", + "[]=> ", "!", "X", "F", @@ -109,12 +110,12 @@ namespace spot " V ", " W ", // not supported " M ", // not supported - " <>-> ", // not supported - " <>=> ", // not supported - " <>+> ", // not supported - " <>=+> ", // not supported - " []-> ", // not supported - " []=> ", // not supported + "<>-> ", // not supported + "<>=> ", // not supported + "<>+> ", // not supported + "<>=+> ", // not supported + "[]-> ", // not supported + "[]=> ", // not supported "!", "()", "<>", @@ -128,6 +129,36 @@ namespace spot ":", // not supported }; + const char* utf8_kw[] = { + "0", + "1", + "[*0]", + "⊕", + " → ", + " ↔ ", + " U ", + " R ", + " W ", + " M ", + "◇→ ", + "◇⇒ ", + "◇→̃ ", + "◇⇒̃ ", + "□→ ", + "□⇒ ", + "¬", + "â—‹", + "â—‡", + "â–¡", + "∨", + " | ", + "∧", + " ∩ ", + " & ", + ";", + ":", + }; + static bool is_bare_word(const char* str) { @@ -491,7 +522,8 @@ namespace spot top_level_ = true; break; case unop::NegClosure: - os_ << "!{"; + emit(KNot); + os_ << "{"; in_ratexp_ = true; top_level_ = true; break; @@ -684,6 +716,23 @@ namespace spot return os.str(); } + std::ostream& + to_utf8_string(const formula* f, std::ostream& os, bool full_parent, + bool ratexp) + { + to_string_visitor v(os, full_parent, ratexp, utf8_kw); + f->accept(v); + return os; + } + + std::string + to_utf8_string(const formula* f, bool full_parent, bool ratexp) + { + std::ostringstream os; + to_utf8_string(f, os, full_parent, ratexp); + return os.str(); + } + std::ostream& to_spin_string(const formula* f, std::ostream& os, bool full_parent) { diff --git a/src/ltlvisit/tostring.hh b/src/ltlvisit/tostring.hh index 65916b9fc..15654d530 100644 --- a/src/ltlvisit/tostring.hh +++ b/src/ltlvisit/tostring.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2011, 2012 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 +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -54,6 +55,27 @@ namespace spot std::string to_string(const formula* f, 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 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. + 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. + std::string + to_utf8_string(const formula* f, bool full_parent = false, + bool ratexp = false); + /// \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.