diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 9945d11a7e015865588b008e10a94b92782dec50..89cd540e268fe1a6c745c77cdbebdd8e4f905981 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -33,6 +33,7 @@ %code requires { #include +#include #include "public.hh" #include "ltlast/allnodes.hh" #include "ltlvisit/tostring.hh" @@ -1034,6 +1035,24 @@ namespace spot return result; } + const formula* + parse_formula(const std::string& ltl_string, environment& env) + { + parse_error_list pel; + const formula* f = parse(ltl_string, pel, env); + std::ostringstream s; + if (format_parse_errors(s, ltl_string, pel)) + { + parse_error_list pel2; + const formula* g = parse_lbt(ltl_string, pel2, env); + if (pel2.empty()) + return g; + else + throw parse_error(s.str()); + } + return f; + } + } } diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index be0e6ad6c7cae34283fe02b1f8f504fb00f02691..6624af8836ddadf98bc6c16770c3fdbf9fc88ee7 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -110,7 +110,7 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇" unput(')'); if (!missing_parent) error_list.push_back( - spot::ltl::parse_error(*yylloc, + spot::ltl::one_parse_error(*yylloc, "missing closing parenthese")); missing_parent = true; } @@ -164,7 +164,7 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇" unput(')'); if (!missing_parent) error_list.push_back( - spot::ltl::parse_error(*yylloc, + spot::ltl::one_parse_error(*yylloc, "missing closing brace")); missing_parent = true; } @@ -204,7 +204,7 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇" if (errno || yylval->num != n) { error_list.push_back( - spot::ltl::parse_error(*yylloc, + spot::ltl::one_parse_error(*yylloc, "value too large ignored")); // Skip this number and read next token yylloc->step(); diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh index e2a8d111333b88a4474848bab8d308195ea09aff..3f4e5a944fca7d114d0e56ae10aaf402e7fcb255 100644 --- a/src/ltlparse/public.hh +++ b/src/ltlparse/public.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -40,9 +40,9 @@ namespace spot #ifndef SWIG /// \brief A parse diagnostic with its location. - typedef std::pair parse_error; + typedef std::pair one_parse_error; /// \brief A list of parser diagnostics, as filled by parse. - typedef std::list parse_error_list; + typedef std::list parse_error_list; #else // Turn parse_error_list into an opaque type for Swig. struct parse_error_list {}; @@ -124,6 +124,24 @@ namespace spot environment& env = default_environment::instance(), bool debug = false); + + + struct SPOT_API parse_error: public std::runtime_error + { + parse_error(const std::string& s): std::runtime_error(s) + { + } + }; + + /// \brief A simple wrapper to parse() and parse_lbt(). + /// + /// This is mostly meant for interactive use. It first tries parse(); if + /// this fails it tries parse_lbt(); and if both fails it returns the errors + /// of the first call to parse() as a std::runtime_error(). + SPOT_API const formula* + parse_formula(const std::string& ltl_string, + environment& env = default_environment::instance()); + /// \brief Build a formula from a string representing a SERE. /// \param sere_string The string to parse. /// \param error_list A list that will be filled with diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 5a1170df0a39cf98c586bccf88c9adeef726d32e..6fe648cdca8a27f0e4c2d042d567a881956ca13d 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -260,6 +260,47 @@ namespace spot "\\SereGoto{", }; + const char* sclatex_kw[] = { + "\\ffalse", + "\\ttrue", + "\\varepsilon", + " \\oplus ", + " \\rightarrow ", + " \\leftrightarrow ", + " \\mathbin{\\mathsf{U}} ", + " \\mathbin{\\mathsf{R}} ", + " \\mathbin{\\mathsf{W}} ", + " \\mathbin{\\mathsf{M}} ", + ("\\mathrel{\\Diamond\\kern-1.7pt\\raise.4pt" + "\\hbox{$\\mathord{\\rightarrow}$}} "), + ("\\mathrel{\\Diamond\\kern-1.7pt\\raise.4pt" + "\\hbox{$\\mathord{\\Rightarrow}$}} "), + "\\seqM ", + "\\seqXM ", + ("\\mathrel{\\Box\\kern-1.7pt\\raise.4pt" + "\\hbox{$\\mathord{\\rightarrow}$}} "), + ("\\mathrel{\\Box\\kern-1.7pt\\raise.4pt" + "\\hbox{$\\mathord{\\Rightarrow}$}} "), + "\\lnot ", + "\\mathsf{X} ", + "\\mathsf{F} ", + "\\mathsf{G} ", + " \\lor ", + " \\cup ", + " \\land ", + " \\cap ", + " \\mathbin{\\mathsf{\\&}} ", + " \\mathbin{\\mathsf{;}} ", + " \\mathbin{\\mathsf{:}} ", + "\\{", + "\\}", + "}", + "^{\\star", + "^+", + "^{=", + "^{\\to", + }; + static bool is_bare_word(const char* str) { @@ -370,7 +411,7 @@ namespace spot } else { - if (kw_ == latex_kw) + if (kw_ == latex_kw || kw_ == sclatex_kw) { size_t s = str.size(); while (str[s - 1] >= '0' && str[s - 1] <= '9') @@ -945,6 +986,24 @@ namespace spot return os.str(); } + std::ostream& + to_sclatex_string(const formula* f, std::ostream& os, + bool full_parent, bool ratexp) + { + to_string_visitor v(os, full_parent, ratexp, sclatex_kw); + f->accept(v); + return os; + } + + std::string + to_sclatex_string(const formula* f, + bool full_parent, bool ratexp) + { + std::ostringstream os; + to_sclatex_string(f, os, full_parent, ratexp); + return os.str(); + } + } } diff --git a/src/ltlvisit/tostring.hh b/src/ltlvisit/tostring.hh index baab4a7fb1ebf7bec19be4a808ee562faa5e575a..c8a270f2d1e5902e51639e7043aa9945f5c00cc8 100644 --- a/src/ltlvisit/tostring.hh +++ b/src/ltlvisit/tostring.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2010, 2011, 2012, 2013, 2014 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 @@ -101,8 +101,7 @@ namespace spot SPOT_API std::string to_wring_string(const formula* f); - /// \brief Output a formula as an LaTeX string which is parsable unless - /// the formula contains automaton operators (used in ELTL formulae). + /// \brief Output a formula as an LaTeX 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 @@ -112,7 +111,7 @@ namespace spot to_latex_string(const formula* f, std::ostream& os, bool full_parent = false, bool ratexp = false); - /// \brief Output a formula as a LaTeX string which is parsable + /// \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 @@ -122,6 +121,29 @@ namespace spot to_latex_string(const formula* f, bool full_parent = false, bool ratexp = false); + + /// \brief Output a formula as a self-contained LaTeX string. + /// + /// The result cannot be parsed back. + /// \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. + SPOT_API std::ostream& + to_sclatex_string(const formula* f, std::ostream& os, + bool full_parent = false, bool ratexp = false); + + /// \brief Output a 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); /// @} } } diff --git a/wrap/python/spot.i b/wrap/python/spot.i index ed3c4eb42cfa6c02ae42de1655c5378986ffa4b9..0fbae6b2e66179c62ddaf2bcfde135aa0e7bab4c 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -31,6 +31,7 @@ %include "std_shared_ptr.i" %include "std_string.i" %include "std_list.i" +%include "exception.i" // git grep 'typedef.*std::shared_ptr' | grep -v const // sed 's/.*<\(.*\)>.*/%shared_ptr(spot::\1)/g' @@ -172,6 +173,19 @@ using namespace spot; }; %apply char** OUTPUT { char** err }; + +%exception { + try { + $action + } + catch (const spot::ltl::parse_error& e) + { + std::string er("\n"); + er += e.what(); + SWIG_exception(SWIG_SyntaxError, er.c_str()); + } +} + // False and True cannot be redefined in Python3, even in a class. // Spot uses these in an enum of the constant class. %rename(FalseVal) False; @@ -286,12 +300,12 @@ namespace spot { size_t __hash__() { return self->hash(); } - std::string - __str__(void) + std::string __repr__() { return spot::ltl::to_string(self); } + std::string _repr_latex_() { - return spot::ltl::to_string(self); + return std::string("$") + spot::ltl::to_sclatex_string(self) + '$'; } - + std::string __str__() { return spot::ltl::to_string(self); } } %nodefaultctor std::ostream; diff --git a/wrap/python/tests/run.in b/wrap/python/tests/run.in index 79a21ee7aeb7d49d3717e8f2f4d641cc1d264a67..87bfecb42d00abc00d2ebfa9eb26b9a13b8b029f 100644 --- a/wrap/python/tests/run.in +++ b/wrap/python/tests/run.in @@ -40,6 +40,8 @@ case $1 in PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath exec @PYTHON@ "$@";; *.test) exec sh -x "$@";; + ipython*) + PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath exec "$@";; *) echo "Unknown extension" >&2 exit 2;;