python: use raw strings when appropriate

We had some incorrectly escaped strings that are now causing
SyntaxWarnings with Python 3.12

* bin/options.py, python/spot/aux_.py, python/spot/ltsmin.i,
python/spot/__init__.py: Here.
* NEWS: Mention the fix.

python/spot/__init__.py

@@ -344,8 +344,8 @@ class formula:
             return str_sclatex_psl(self, parenth)
         elif format == 'mathjax' or format == 'j':
             return (str_sclatex_psl(self, parenth).
-                    replace("``", "\\unicode{x201C}").
-                    replace("\\textrm{''}", "\\unicode{x201D}"))
+                    replace("``", r"\unicode{x201C}").
+                    replace(r"\textrm{''}", r"\unicode{x201D}"))
         elif format == 'dot' or format == 'd':
             ostr = ostringstream()
             print_dot_psl(ostr, self)
@@ -466,16 +466,16 @@ class formula:
 @_extend(atomic_prop_set)
 class atomic_prop_set:
     def _repr_latex_(self):
-        res = '$\{'
+        res = r'$\{'
         comma = ''
         for ap in self:
             apname = ap.to_str('j')
-            if not '\\unicode{' in apname:
-                apname = "\\unicode{x201C}" + apname + "\\unicode{x201D}"
+            if not r'\unicode{' in apname:
+                apname = r"\unicode{x201C}" + apname + r"\unicode{x201D}"
             res += comma
             comma = ', '
             res += apname
-        res += '\}$'
+        res += r'\}$'
         return res
 
 
@@ -1445,12 +1445,12 @@ class twa_word:
             res += bdd_to_formula(letter, bd).to_str('j')
         if len(res) > 1:
             res += '; '
-        res += '\\mathsf{cycle}\\{'
+        res += r'\mathsf{cycle}\{'
         for idx, letter in enumerate(self.cycle):
             if idx:
                 res += '; '
             res += bdd_to_formula(letter, bd).to_str('j')
-        return res + '\\}$'
+        return res + r'\}$'
 
     def as_svg(self):
         """

python/spot/aux_.py

@@ -51,7 +51,7 @@ def extend(*classes):
 # parameter is inverted.  https://gitlab.com/graphviz/graphviz/issues/1605
 # In our case, the scale parameters should both be <= 1, so we can
 # detect when that is not the case.
-svgscale_regex = re.compile('transform="scale\(([\d.]+) ([\d.]+)\) rotate')
+svgscale_regex = re.compile(r'transform="scale\(([\d.]+) ([\d.]+)\) rotate')
 
 def _gvfix(matchobj):
         xs = float(matchobj.group(1))

python/spot/ltsmin.i

@@ -74,7 +74,7 @@ def load(filename):
       p = subprocess.run(['spins', filename], stdout=subprocess.PIPE,
                          stderr=subprocess.STDOUT,
                          universal_newlines=True)
-      if p.stdout: print(re.sub('^\s*\[\.*\s*\]\n', '', p.stdout,
+      if p.stdout: print(re.sub(r'^\s*\[\.*\s*\]\n', '', p.stdout,
                                 flags=re.MULTILINE), file=sys.stderr)
       if p.stderr: print(p.stderr, file=sys.stderr)
       p.check_returncode()