From 5bfd0267e73ec3950e0561863e463de8d069254d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 3 Oct 2015 11:20:02 +0200 Subject: [PATCH] python: implement formula.__format__ Fixes #105. * src/bin/common_trans.cc (quote_shell_string): Move ... * src/misc/escape.cc, src/misc/escape.hh (quote_shell_string): ... here. * wrap/python/spot_impl.i: Wrap escape.hh. * wrap/python/spot.py: Implement formula.__format__. * wrap/python/tests/ltlsimple.py: Test it. * NEWS, doc/org/tut01.org, wrap/python/tests/formulas.ipynb: Document it. --- NEWS | 2 + doc/org/tut01.org | 78 ++++++++++++++ src/bin/common_trans.cc | 34 +------ src/misc/escape.cc | 32 ++++++ src/misc/escape.hh | 8 ++ wrap/python/spot.py | 84 ++++++++++++++-- wrap/python/spot_impl.i | 2 + wrap/python/tests/formulas.ipynb | 168 +++++++++++++++++++++++++------ wrap/python/tests/ltlsimple.py | 23 +++++ 9 files changed, 364 insertions(+), 67 deletions(-) diff --git a/NEWS b/NEWS index 909739907..c3d817ac3 100644 --- a/NEWS +++ b/NEWS @@ -3,6 +3,8 @@ New in spot 1.99.4a (not yet released) Python: * Add bindings for complete(). + * Formulas now have a custom __format__ function. See + https://spot.lrde.epita.fr/tut01.html for examples. Bugs fixed: diff --git a/doc/org/tut01.org b/doc/org/tut01.org index 8548e16d3..dd2174b75 100644 --- a/doc/org/tut01.org +++ b/doc/org/tut01.org @@ -376,3 +376,81 @@ ltlfilt --lenient -f '(a U ) U c' In C++ you can enable lenient using one of the Boolean arguments of =parse_infix_psl()=. +** Python formatting + +Formulas have a custom format specification language that allows you +to easily change the way a formula should be output when using the +=format()= method of strings. + +#+BEGIN_SRC python :results output :exports both +import spot +formula = spot.formula('a U b U "$strange[0]=name"') +print("""\ +Default output: {f} +Spin syntax: {f:s} +(Spin syntax): {f:sp} +Default for shell: echo {f:q} | ... +LBT for shell: echo {f:lq} | ... +Default for CSV: ...,{f:c},... +Wring, centered: {f:w:~^50}""".format(f = formula)) +#+END_SRC + +#+RESULTS: +: Default output: a U (b U "$strange[0]=name") +: Spin syntax: a U (b U ($strange[0]=name)) +: (Spin syntax): (a) U ((b) U ($strange[0]=name)) +: Default for shell: echo 'a U (b U "$strange[0]=name")' | ... +: LBT for shell: echo 'U "a" U "b" "$strange[0]=name"' | ... +: Default for CSV: ...,"a U (b U ""$strange[0]=name"")",... +: Wring, centered: ~~~~~(a=1) U ((b=1) U ("$strange[0]=name"=1))~~~~~ + +The specifiers after the first =:= are specific to formulas. The +specifiers after the second =:= (if any) are the usual [[https://docs.python.org/3/library/string.html#formatspec][format +specifiers]] (typically alignment choices) and are applied on the string +produced from the formula. + +The complete list of specified that apply to formulas can always be +printed with =help(spot.formula.__format__)=: + +#+BEGIN_SRC python :results output :exports results +import spot +help(spot.formula.__format__) +#+END_SRC + +#+RESULTS: +#+begin_example +Help on function _formula_format in module spot: + +_formula_format(self, spec) + Format the formula according to spec. + + 'spec' should be a list of letters that select + how the formula should be formatted. + + Use one of the following letters to select the syntax: + + - 'f': use Spot's syntax (default) + - '8': use Spot's syntax in UTF-8 mode + - 's': use Spin's syntax + - 'l': use LBT's syntax + - 'w': use Wring's syntax + - 'x': use LaTeX output + - 'X': use self-contained LaTeX output + + Add some of those letters for additional options: + + - 'p': use full parentheses + - 'c': escape the formula for CSV output (this will + enclose the formula in double quotes, and escape + any included double quotes) + - 'h': escape the formula for HTML output + - 'd': escape double quotes and backslash, + for use in C-strings (the outermost double + quotes are *not* added) + - 'q': quote and escape for shell output, using single + quotes or double quotes depending on the contents. + + - ':spec': pass the remaining specification to the + formating function for strings. + +#+end_example diff --git a/src/bin/common_trans.cc b/src/bin/common_trans.cc index 84eb35064..f484b03b8 100644 --- a/src/bin/common_trans.cc +++ b/src/bin/common_trans.cc @@ -30,6 +30,7 @@ #include "tl/print.hh" #include "common_conv.hh" +#include "misc/escape.hh" // A set of tools for which we know the correct output static struct shorthands_t @@ -146,39 +147,10 @@ translator_spec::~translator_spec() std::vector translators; -static void -quote_shell_string(std::ostream& os, const char* str) -{ - // Single quotes are best, unless the string to quote contains one. - if (!strchr(str, '\'')) - { - os << '\'' << str << '\''; - } - else - { - // In double quotes we have to escape $ ` " or \. - os << '"'; - while (*str) - switch (*str) - { - case '$': - case '`': - case '"': - case '\\': - os << '\\'; - // fall through - default: - os << *str++; - break; - } - os << '"'; - } -} - void quoted_string::print(std::ostream& os, const char*) const { - quote_shell_string(os, val().c_str()); + spot::quote_shell_string(os, val().c_str()); } printable_result_filename::printable_result_filename() @@ -209,7 +181,7 @@ printable_result_filename::print(std::ostream& os, const char*) const snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num); const_cast(this)->val_ = spot::create_tmpfile(prefix); - quote_shell_string(os, val()->name()); + spot::quote_shell_string(os, val()->name()); } diff --git a/src/misc/escape.cc b/src/misc/escape.cc index 526578d17..f8dc32050 100644 --- a/src/misc/escape.cc +++ b/src/misc/escape.cc @@ -27,6 +27,7 @@ #include #include #include +#include #include "escape.hh" namespace spot @@ -143,4 +144,35 @@ namespace spot std::find_if(str.begin(), str.end(), std::not1(std::ptr_fun(std::isspace)))); } + + std::ostream& + quote_shell_string(std::ostream& os, const char* str) + { + // Single quotes are best, unless the string to quote contains one. + if (!strchr(str, '\'')) + { + os << '\'' << str << '\''; + } + else + { + // In double quotes we have to escape $ ` " or \. + os << '"'; + while (*str) + switch (*str) + { + case '$': + case '`': + case '"': + case '\\': + os << '\\'; + // fall through + default: + os << *str++; + break; + } + os << '"'; + } + return os; + } + } diff --git a/src/misc/escape.hh b/src/misc/escape.hh index 0080536f1..b3476c53a 100644 --- a/src/misc/escape.hh +++ b/src/misc/escape.hh @@ -65,5 +65,13 @@ namespace spot /// \brief Remove spaces at the front and back of \a str. SPOT_API void trim(std::string& str); + + /// \brief Output \a str between simple quote or double quotes + /// + /// Simple quotes are preferred unless \a str contains some simple + /// quotes. In that case we use double quotes and escape anything + /// that needs to be escaped. + SPOT_API std::ostream& + quote_shell_string(std::ostream& os, const char* str); /// @} } diff --git a/wrap/python/spot.py b/wrap/python/spot.py index 668cc9878..ddcc140ad 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -114,23 +114,92 @@ def _formula_str_ctor(self, str): self.this = parse_formula(str) def _formula_to_str(self, format = 'spot', parenth = False): - if format == 'spot': + if format == 'spot' or format == 'f': return str_psl(self, parenth) - elif format == 'spin': + elif format == 'spin' or format == 's': return str_spin_ltl(self, parenth) - elif format == 'utf8': + elif format == 'utf8' or format == '8': return str_utf8_psl(self, parenth) - elif format == 'lbt': + elif format == 'lbt' or format == 'l': return str_lbt_ltl(self) - elif format == 'wring': + elif format == 'wring' or format == 'w': return str_wring_ltl(self) - elif format == 'latex': + elif format == 'latex' or format == 'x': return str_latex_psl(self, parenth) - elif format == 'sclatex': + elif format == 'sclatex' or format == 'X': return str_sclatex_psl(self, parenth) else: raise ValueError("unknown string format: " + format) +def _formula_format(self, spec): + """Format the formula according to spec. + + 'spec' should be a list of letters that select + how the formula should be formatted. + + Use one of the following letters to select the syntax: + + - 'f': use Spot's syntax (default) + - '8': use Spot's syntax in UTF-8 mode + - 's': use Spin's syntax + - 'l': use LBT's syntax + - 'w': use Wring's syntax + - 'x': use LaTeX output + - 'X': use self-contained LaTeX output + + Add some of those letters for additional options: + + - 'p': use full parentheses + - 'c': escape the formula for CSV output (this will + enclose the formula in double quotes, and escape + any included double quotes) + - 'h': escape the formula for HTML output + - 'd': escape double quotes and backslash, + for use in C-strings (the outermost double + quotes are *not* added) + - 'q': quote and escape for shell output, using single + quotes or double quotes depending on the contents. + + - ':spec': pass the remaining specification to the + formating function for strings. + """ + + syntax = 'f' + parent = False + escape = None + + while spec: + c, spec = spec[0], spec[1:] + if c in ('f', 's', '8', 'l', 'w', 'x', 'X'): + syntax = c + elif c == 'p': + parent = True + elif c in ('c', 'd', 'h', 'q'): + escape = c + elif c == ':': + break + else: + raise ValueError("unknown format specification: " + c + spec) + + s = self.to_str(syntax, parent) + + if escape == 'c': + o = ostringstream() + escape_rfc4180(o, s) + s = '"' + o.str() + '"' + elif escape == 'd': + s = escape_str(s) + elif escape == 'h': + o = ostringstream() + escape_html(o, s) + s = o.str() + elif escape == 'q': + o = ostringstream() + quote_shell_string(o, s) + s = o.str() + + return s.__format__(spec) + def _formula_traverse(self, func): if func(self): return @@ -158,6 +227,7 @@ formula.__init__ = _formula_str_ctor formula.to_str = _formula_to_str formula.show_ast = _render_formula_as_svg formula.traverse = _formula_traverse +formula.__format__ = _formula_format formula.map = _formula_map def _twa_to_str(a, format='hoa', opt=None): diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 3ca147720..6d7005cd5 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -79,6 +79,7 @@ #include "misc/minato.hh" #include "misc/optionmap.hh" #include "misc/random.hh" +#include "misc/escape.hh" #include "tl/formula.hh" @@ -215,6 +216,7 @@ using namespace spot; %include "misc/minato.hh" %include "misc/optionmap.hh" %include "misc/random.hh" +%include "misc/escape.hh" %implicitconv std::vector; diff --git a/wrap/python/tests/formulas.ipynb b/wrap/python/tests/formulas.ipynb index 52882384d..8199091a6 100644 --- a/wrap/python/tests/formulas.ipynb +++ b/wrap/python/tests/formulas.ipynb @@ -1,7 +1,23 @@ { "metadata": { - "name": "", - "signature": "sha256:049261ec6b13505007796a9e9d1d8279783233b9b1eb8f9b8e5727070a38db7a" + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.4.3+" + }, + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -172,6 +188,100 @@ ], "prompt_number": 6 }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Formulas output via `format()` can also use some convenient shorthand to select the syntax:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(\"\"\"\\\n", + "Spin: {0:s}\n", + "Spin+parentheses: {0:sp}\n", + "Spot (default): {0}\n", + "Spot+shell quotes: {0:q}\n", + "LBT, right aligned: {0:l:~>40}\"\"\".format(f))" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "Spin: p1 U (p2 V (p3 && !p4))\n", + "Spin+parentheses: (p1) U ((p2) V ((p3) && (!(p4))))\n", + "Spot (default): p1 U (p2 R (p3 & !p4))\n", + "Spot+shell quotes: 'p1 U (p2 R (p3 & !p4))'\n", + "LBT, right aligned: ~~~~~~~~~~~~~~~~~~~~~U p1 V p2 & p3 ! p4\n" + ] + } + ], + "prompt_number": 7 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The specifiers that can be used with `format` are documented as follows:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "help(spot.formula.__format__)" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "Help on function _formula_format in module spot:\n", + "\n", + "_formula_format(self, spec)\n", + " Format the formula according to spec.\n", + " \n", + " 'spec' should be a list of letters that select\n", + " how the formula should be formatted.\n", + " \n", + " Use one of the following letters to select the syntax:\n", + " \n", + " - 'f': use Spot's syntax (default)\n", + " - '8': use Spot's syntax in UTF-8 mode\n", + " - 's': use Spin's syntax\n", + " - 'l': use LBT's syntax\n", + " - 'w': use Wring's syntax\n", + " - 'x': use LaTeX output\n", + " - 'X': use self-contained LaTeX output\n", + " \n", + " Add some of those letters for additional options:\n", + " \n", + " - 'p': use full parentheses\n", + " - 'c': escape the formula for CSV output (this will\n", + " enclose the formula in double quotes, and escape\n", + " any included double quotes)\n", + " - 'h': escape the formula for HTML output\n", + " - 'd': escape double quotes and backslash,\n", + " for use in C-strings (the outermost double\n", + " quotes are *not* added)\n", + " - 'q': quote and escape for shell output, using single\n", + " quotes or double quotes depending on the contents.\n", + " \n", + " - ':spec': pass the remaining specification to the\n", + " formating function for strings.\n", + "\n" + ] + } + ], + "prompt_number": 8 + }, { "cell_type": "markdown", "metadata": {}, @@ -191,13 +301,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 7, + "prompt_number": 9, "text": [ "True" ] } ], - "prompt_number": 7 + "prompt_number": 9 }, { "cell_type": "code", @@ -211,13 +321,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 8, + "prompt_number": 10, "text": [ "False" ] } ], - "prompt_number": 8 + "prompt_number": 10 }, { "cell_type": "markdown", @@ -238,13 +348,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 9, + "prompt_number": 11, "text": [ "True" ] } ], - "prompt_number": 9 + "prompt_number": 11 }, { "cell_type": "code", @@ -258,13 +368,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 10, + "prompt_number": 12, "text": [ "False" ] } ], - "prompt_number": 10 + "prompt_number": 12 }, { "cell_type": "code", @@ -278,13 +388,13 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 11, + "prompt_number": 13, "text": [ "True" ] } ], - "prompt_number": 11 + "prompt_number": 13 }, { "cell_type": "markdown", @@ -308,13 +418,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 12, + "prompt_number": 14, "text": [ "\"a > b\" & \"proc[2]@init\" & GF_foo_" ] } ], - "prompt_number": 12 + "prompt_number": 14 }, { "cell_type": "code", @@ -331,13 +441,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 13, + "prompt_number": 15, "text": [ "a & b & GFc" ] } ], - "prompt_number": 13 + "prompt_number": 15 }, { "cell_type": "code", @@ -354,13 +464,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 14, + "prompt_number": 16, "text": [ "p0 & p1 & GFp2" ] } ], - "prompt_number": 14 + "prompt_number": 16 }, { "cell_type": "markdown", @@ -388,7 +498,7 @@ { "metadata": {}, "output_type": "pyout", - "prompt_number": 15, + "prompt_number": 17, "svg": [ "\n", "\n", @@ -493,11 +603,11 @@ "" ], "text": [ - "" + "" ] } ], - "prompt_number": 15 + "prompt_number": 17 }, { "cell_type": "code", @@ -514,13 +624,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 16, + "prompt_number": 18, "text": [ "F(a & X(!a & b))" ] } ], - "prompt_number": 16 + "prompt_number": 18 }, { "cell_type": "markdown", @@ -544,13 +654,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 17, + "prompt_number": 19, "text": [ "F(a & ((a & (a U (!a & b)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & b)) & ((!b U a) | (b U a))) | (b & (b U (!a & b & !b)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b)) & ((!a U b) | (a U b))) | (!a & b & (G!a | Ga) & (G!b | Gb))))" ] } ], - "prompt_number": 17 + "prompt_number": 19 }, { "cell_type": "markdown", @@ -575,13 +685,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 18, + "prompt_number": 20, "text": [ "(0 R !(a <-> b)) -> (1 U (a <-> b))" ] } ], - "prompt_number": 18 + "prompt_number": 20 }, { "cell_type": "code", @@ -598,13 +708,13 @@ ], "metadata": {}, "output_type": "pyout", - "prompt_number": 19, + "prompt_number": 21, "text": [ "(1 U ((a & b) | (!a & !b))) | !(0 R ((!a & b) | (a & !b)))" ] } ], - "prompt_number": 19 + "prompt_number": 21 } ], "metadata": {} diff --git a/wrap/python/tests/ltlsimple.py b/wrap/python/tests/ltlsimple.py index 10be6e283..9eb9f909f 100755 --- a/wrap/python/tests/ltlsimple.py +++ b/wrap/python/tests/ltlsimple.py @@ -93,3 +93,26 @@ def count_g(f): x += 1 f.traverse(count_g) assert x == 3 + +#---------------------------------------------------------------------- + +# The example from tut01.org + +formula = spot.formula('a U b U "$strange[0]=name"') +res = """\ +Default output: {f} +Spin syntax: {f:s} +(Spin syntax): {f:sp} +Default for shell: echo {f:q} | ... +LBT for shell: echo {f:lq} | ... +Default for CSV: ...,{f:c},... +Wring, centered: {f:w:~^50}""".format(f = formula) + +assert res == """\ +Default output: a U (b U "$strange[0]=name") +Spin syntax: a U (b U ($strange[0]=name)) +(Spin syntax): (a) U ((b) U ($strange[0]=name)) +Default for shell: echo 'a U (b U "$strange[0]=name")' | ... +LBT for shell: echo 'U "a" U "b" "$strange[0]=name"' | ... +Default for CSV: ...,"a U (b U ""$strange[0]=name"")",... +Wring, centered: ~~~~~(a=1) U ((b=1) U ("$strange[0]=name"=1))~~~~~"""