From e91c6ba2f10e354a21f23fee80e6393eafef1a04 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 1 May 2016 18:58:08 +0200
Subject: [PATCH] python: support operator rewriting in __format__

Fixes #168.

* python/spot/__init__.py: Implement it.
* tests/python/formulas.ipynb: Test it.
* NEWS: Mention it.
---
 NEWS                        |  5 +++++
 python/spot/__init__.py     | 12 +++++++++++-
 tests/python/formulas.ipynb | 10 +++++++---
 3 files changed, 23 insertions(+), 4 deletions(-)

diff --git a/NEWS b/NEWS
index cc8f51c1e..13e1c6c97 100644
--- a/NEWS
+++ b/NEWS
@@ -55,6 +55,11 @@ New in spot 2.0a (not yet released)
 
   * The tgba_determinize() function is now accessible in Python.
 
+  * The __format__() method for formula support the same
+    operator-rewritting feature introduced in ltldo and ltlcross.
+    So "{:[i]s}".format(f) is the same as
+    "{:s}".format(f.unabbreviate("i")).
+
   Bug fixes:
 
   * Typo in documentation of the -H option in --help output.
diff --git a/python/spot/__init__.py b/python/spot/__init__.py
index 3f0369775..0042b3347 100644
--- a/python/spot/__init__.py
+++ b/python/spot/__init__.py
@@ -230,6 +230,8 @@ class formula:
                quotes are *not* added)
         - 'q': quote and escape for shell output, using single
                quotes or double quotes depending on the contents.
+        - '[...]': rewrite away all the operators specified in brackets,
+               using spot.unabbreviate().
 
         - ':spec': pass the remaining specification to the
                    formating function for strings.
@@ -240,6 +242,8 @@ class formula:
         parent = False
         escape = None
 
+        form = self
+
         while spec:
             c, spec = spec[0], spec[1:]
             if c in ('f', 's', '8', 'l', 'w', 'x', 'X'):
@@ -250,10 +254,16 @@ class formula:
                 escape = c
             elif c == ':':
                 break
+            elif c == '[':
+                pos = spec.find(']')
+                if pos < 0:
+                    raise ValueError("unclosed bracket: [" + spec)
+                form = form.unabbreviate(spec[0:pos])
+                spec = spec[pos+1:]
             else:
                 raise ValueError("unknown format specification: " + c + spec)
 
-        s = self.to_str(syntax, parent)
+        s = form.to_str(syntax, parent)
 
         if escape == 'c':
             o = ostringstream()
diff --git a/tests/python/formulas.ipynb b/tests/python/formulas.ipynb
index cdfea32d9..ca075be66 100644
--- a/tests/python/formulas.ipynb
+++ b/tests/python/formulas.ipynb
@@ -204,7 +204,8 @@
       "Spin+parentheses:   {0:sp}\n",
       "Spot (default):     {0}\n",
       "Spot+shell quotes:  {0:q}\n",
-      "LBT, right aligned: {0:l:~>40}\"\"\".format(f))"
+      "LBT, right aligned: {0:l:~>40}\n",
+      "LBT, no M/W/R:      {0:[MWR]l}\"\"\".format(f))"
      ],
      "language": "python",
      "metadata": {},
@@ -217,7 +218,8 @@
         "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"
+        "LBT, right aligned: ~~~~~~~~~~~~~~~~~~~~~U p1 V p2 & p3 ! p4\n",
+        "LBT, no M/W/R:      U p1 U & p3 ! p4 | & & p2 p3 ! p4 G & p3 ! p4\n"
        ]
       }
      ],
@@ -277,6 +279,8 @@
         "           quotes are *not* added)\n",
         "    - 'q': quote and escape for shell output, using single\n",
         "           quotes or double quotes depending on the contents.\n",
+        "    - '[...]': rewrite away all the operators specified in brackets,\n",
+        "           using spot.unabbreviate().\n",
         "    \n",
         "    - ':spec': pass the remaining specification to the\n",
         "               formating function for strings.\n",
@@ -724,4 +728,4 @@
    "metadata": {}
   }
  ]
-}
+}
\ No newline at end of file
-- 
GitLab