Make spot.py a python package instead of a module

* python/spot.py, python/spot_impl.i: Rename as... * python/spot/__init__.py, python/spot/impl.i: ... these. * python/Makefile.am, tests/run.in: Adjust for new paths. * tests/python/automata-io.ipynb, tests/python/automata.ipynb, tests/python/decompose.ipynb, tests/python/piperead.ipynb, tests/python/testingaut.ipynb: Adjust messages to refer to spot.impl instead of spot_impl.
2016-01-24 16:45:10 +01:00 · 2016-01-24 16:45:10 +01:00 · 215fcb799a
commit 215fcb799a
parent 727d4cc678
9 changed files with 83 additions and 74 deletions
--- a/python/spot/init.py
+++ b/python/spot/init.py
@ -0,0 +1,876 @@
+# -*- coding: utf-8 -*-
+# Copyright (C) 2014, 2015, 2016  Laboratoire de
+# Recherche et Développement de l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+
+import sys
+
+
+if sys.hexversion < 0x03030000:
+    sys.exit("This module requires Python 3.3 or newer")
+
+
+from spot.impl import *
+import subprocess
+import os
+import signal
+from functools import lru_cache
+
+
+def _extend(*classes):
+    """
+    Decorator that extends all the given classes with the contents
+    of the class currently being defined.
+    """
+    def wrap(this):
+        for cls in classes:
+            for (name, val) in this.__dict__.items():
+                if name not in ('__dict__', '__weakref__') \
+                   and not (name == '__doc__' and val is None):
+                    setattr(cls, name, val)
+        return classes[0]
+    return wrap
+
+_show_default = None
+
+def setup(**kwargs):
+    """Configure Spot for fancy display.
+
+    This is manly useful in Jupyter/IPython.
+
+    Note that this function needs to be called before any automaton is
+    displayed.  Afterwards it will have no effect (you should restart
+    Python, or the Jupyter/IPython Kernel).
+
+    Parameters
+    ----------
+    bullets : bool
+        whether to display acceptance conditions as UTF8 bullets
+        (default: True)
+    fillcolor : str
+        the color to use for states (default: '#ffffaa')
+    size : str
+        the width and height of the GraphViz output in inches
+        (default: '10.2,5')
+    font : str
+        the font to use in the GraphViz output (default: 'Lato')
+    show_default : str
+        default options for show()
+    """
+    import os
+
+    s = ('size="{}" node[style=filled,fillcolor="{}"] '
+         'edge[arrowhead=vee, arrowsize=.7]')
+    os.environ['SPOT_DOTEXTRA'] = s.format(kwargs.get('size', '10.2,5'),
+                                           kwargs.get('fillcolor', '#ffffaa'))
+
+    bullets = 'B' if kwargs.get('bullets', True) else ''
+    d = 'rf({})'.format(kwargs.get('font', 'Lato')) + bullets
+    global _show_default
+    _show_default = kwargs.get('show_default', None)
+    os.environ['SPOT_DOTDEFAULT'] = d
+
+
+# In version 3.0.2, Swig puts strongly typed enum in the main
+# namespace without prefixing them.  Latter versions fix this.  So we
+# can remove for following hack once 3.0.2 is no longer used in our
+# build farm.
+if 'op_ff' not in globals():
+    for i in ('ff', 'tt', 'eword', 'ap', 'Not', 'X', 'F', 'G',
+              'Closure', 'NegClosure', 'NegClosureMarked',
+              'Xor', 'Implies', 'Equiv', 'U', 'R', 'W', 'M',
+              'EConcat', 'EConcatMarked', 'UConcat', 'Or',
+              'OrRat', 'And', 'AndRat', 'AndNLM', 'Concat',
+              'Fusion', 'Star', 'FStar'):
+        globals()['op_' + i] = globals()[i]
+        del globals()[i]
+
+
+# Global BDD dict so that we do not have to create one in user code.
+_bdd_dict = make_bdd_dict()
+
+
+# Add a small LRU cache so that when we display automata into a
+# interactive widget, we avoid some repeated calls to dot for
+# identical inputs.
+@lru_cache(maxsize=64)
+def _str_to_svg(str):
+    dotty = subprocess.Popen(['dot', '-Tsvg'],
+                             stdin=subprocess.PIPE,
+                             stdout=subprocess.PIPE)
+    dotty.stdin.write(str)
+    res = dotty.communicate()
+    return res[0].decode('utf-8')
+
+
+def _ostream_to_svg(ostr):
+    return _str_to_svg(ostr.str().encode('utf-8'))
+
+
+@_extend(twa, ta)
+class twa:
+    def _repr_svg_(self, opt=None):
+        """Output the automaton as SVG"""
+        ostr = ostringstream()
+        if opt is None:
+            global _show_default
+            opt = _show_default
+        print_dot(ostr, self, opt)
+        return _ostream_to_svg(ostr)
+
+    def show(self, opt=None):
+        """Display the automaton as SVG, in the IPython/Jupyter notebook"""
+        if opt is None:
+            global _show_default
+            opt = _show_default
+        # Load the SVG function only if we need it. This way the
+        # bindings can still be used outside of IPython if IPython is
+        # not installed.
+        from IPython.display import SVG
+        return SVG(self._repr_svg_(opt))
+
+
+@_extend(twa)
+class twa:
+    def to_str(a, format='hoa', opt=None):
+        format = format.lower()
+        if format == 'hoa':
+            ostr = ostringstream()
+            print_hoa(ostr, a, opt)
+            return ostr.str()
+        if format == 'dot':
+            ostr = ostringstream()
+            print_dot(ostr, a, opt)
+            return ostr.str()
+        if format == 'spin':
+            ostr = ostringstream()
+            print_never_claim(ostr, a, opt)
+            return ostr.str()
+        if format == 'lbtt':
+            ostr = ostringstream()
+            print_lbtt(ostr, a, opt)
+            return ostr.str()
+        raise ValueError("unknown string format: " + format)
+
+    def save(a, filename, format='hoa', opt=None, append=False):
+        with open(filename, 'a' if append else 'w') as f:
+            s = a.to_str(format, opt)
+            f.write(s)
+            if s[-1] != '\n':
+                f.write('\n')
+        return a
+
+
+@_extend(formula)
+class formula:
+    def __init__(self, str):
+        """Parse the given string to create a formula."""
+        self.this = parse_formula(str)
+
+    def show_ast(self):
+        """Display the syntax tree of the formula."""
+        # Load the SVG function only if we need it. This way the bindings
+        # can still be used outside of IPython if IPython is not
+        # installed.
+        from IPython.display import SVG
+        return SVG(_str_to_svg(self.to_str('d')))
+
+    def to_str(self, format='spot', parenth=False):
+        if format == 'spot' or format == 'f':
+            return str_psl(self, parenth)
+        elif format == 'spin' or format == 's':
+            return str_spin_ltl(self, parenth)
+        elif format == 'utf8' or format == '8':
+            return str_utf8_psl(self, parenth)
+        elif format == 'lbt' or format == 'l':
+            return str_lbt_ltl(self)
+        elif format == 'wring' or format == 'w':
+            return str_wring_ltl(self)
+        elif format == 'latex' or format == 'x':
+            return str_latex_psl(self, parenth)
+        elif format == 'sclatex' or format == 'X':
+            return str_sclatex_psl(self, parenth)
+        elif format == 'dot' or format == 'd':
+            ostr = ostringstream()
+            print_dot_psl(ostr, self)
+            return ostr.str().encode('utf-8')
+        else:
+            raise ValueError("unknown string format: " + format)
+
+    def __format__(self, spec):
+        """Format the formula according to `spec`.
+
+        Parameters
+        ----------
+        spec : str, optional
+            a list of letters that specify how the formula
+            should be formatted.
+
+        Supported specifiers
+        --------------------
+
+        - '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 traverse(self, func):
+        if func(self):
+            return
+        for f in self:
+            f.traverse(func)
+
+    def map(self, func):
+        k = self.kind()
+        if k in (op_ff, op_tt, op_eword, op_ap):
+            return self
+        if k in (op_Not, op_X, op_F, op_G, op_Closure,
+                 op_NegClosure, op_NegClosureMarked):
+            return formula.unop(k, func(self[0]))
+        if k in (op_Xor, op_Implies, op_Equiv, op_U, op_R, op_W,
+                 op_M, op_EConcat, op_EConcatMarked, op_UConcat):
+            return formula.binop(k, func(self[0]), func(self[1]))
+        if k in (op_Or, op_OrRat, op_And, op_AndRat, op_AndNLM,
+                 op_Concat, op_Fusion):
+            return formula.multop(k, [func(x) for x in self])
+        if k in (op_Star, op_FStar):
+            return formula.bunop(k, func(self[0]), self.min(), self.max())
+        raise ValueError("unknown type of formula")
+
+
+def automata(*sources, timeout=None, ignore_abort=True,
+             trust_hoa=True, debug=False):
+    """Read automata from a list of sources.
+
+    Parameters
+    ----------
+    *sources : list of str
+        These sources can be either commands (end with `|`),
+        textual represantations of automata (contain `\n`),
+        or filenames (else).
+    timeout : int, optional
+        Number of seconds to wait for the result of a command.
+        If None (the default), not limit is used.
+    ignore_abort : bool, optional
+        If True (the default), skip HOA atomata that ends with
+        `--ABORT--`, and return the next automaton in the stream.
+        If False, aborted automata are reported as syntax errors.
+    trust_hoa : bool, optional
+        If True (the default), supported HOA properies that
+        cannot be easily verified are trusted.
+    debug : bool, optional
+        Whether to run the parser in debug mode.
+
+    Notes
+    -----
+
+    The automata can be written in the `HOA format`_, as `never
+    claims`_, in `LBTT's format`_, or in `ltl2dstar's format`_.
+
+    .. _HOA format: http://adl.github.io/hoaf/
+    .. _never claims: http://spinroot.com/spin/Man/never.html
+    .. _LBTT's format:
+       http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html
+    .. _ltl2dstar's format:
+       http://www.ltl2dstar.de/docs/ltl2dstar.html#output-format-dstar
+
+    If an argument ends with a `|`, then this argument is interpreted as
+    a shell command, and the output of that command (without the `|`)
+    is parsed.
+
+    If an argument contains a newline, then it is interpreted as
+    actual contents to be parsed.
+
+    Otherwise, the argument is assumed to be a filename.
+
+    The result of this function is a generator on all the automata
+    objects read from these sources.  The typical usage is::
+
+        for aut in spot.automata(filename, command, ...):
+            # do something with aut
+
+    When the source is a command, and no `timeout` is specified,
+    parsing is done straight out of the pipe connecting the
+    command.  So
+
+        for aut in spot.automata('randaut -H -n 10 2 |'):
+            process(aut)
+
+    will call `process(aut)` on each automaton as soon as it is output by
+    `randaut`, and without waiting for `randaut` to terminate.
+
+    However if `timeout` is passed, then `automata()` will wait for
+    the entire command to terminate before parsing its entire output.
+    If one command takes more than `timeout` seconds,
+    `subprocess.TimeoutExpired` is raised.
+
+    If any command terminates with a non-zero error,
+    `subprocess.CalledProcessError` is raised.
+    """
+
+    o = automaton_parser_options()
+    o.debug = debug
+    o.ignore_abort = ignore_abort
+    o.trust_hoa = trust_hoa
+    o.raise_errors = True
+    for filename in sources:
+        try:
+            p = None
+            proc = None
+            if filename[-1] == '|':
+                # universal_newlines for str output instead of bytes
+                # when the pipe is read from Python (which happens
+                # when timeout is set).
+                proc = subprocess.Popen(filename[:-1], shell=True,
+                                        preexec_fn=os.setsid,
+                                        universal_newlines=True,
+                                        stdout=subprocess.PIPE)
+                if timeout is None:
+                    p = automaton_stream_parser(proc.stdout.fileno(),
+                                                filename, o)
+                else:
+                    try:
+                        out, err = proc.communicate(timeout=timeout)
+                    except subprocess.TimeoutExpired:
+                        # Using subprocess.check_output() with timeout
+                        # would just kill the shell, not its children.
+                        os.killpg(proc.pid, signal.SIGKILL)
+                        raise
+                    else:
+                        ret = proc.wait()
+                        if ret:
+                            raise subprocess.CalledProcessError(ret,
+                                                                filename[:-1])
+                    finally:
+                        proc = None
+                    p = automaton_stream_parser(out, filename, o)
+            elif '\n' in filename:
+                p = automaton_stream_parser(filename, "<string>", o)
+            else:
+                p = automaton_stream_parser(filename, o)
+            a = True
+            while a:
+                # This returns None when we reach the end of the file.
+                a = p.parse(_bdd_dict).aut
+                if a:
+                    yield a
+        finally:
+            # Make sure we destroy the parser (p) and the subprocess
+            # (prop) in the correct order...
+            del p
+            if proc is not None:
+                if not a:
+                    # We reached the end of the stream.  Wait for the
+                    # process to finish, so that we get its exit code.
+                    ret = proc.wait()
+                else:
+                    # if a != None, we probably got there through an
+                    # exception, and the subprocess might still be
+                    # running.  Check if an exit status is available
+                    # just in case.
+                    ret = proc.poll()
+                del proc
+                if ret:
+                    raise subprocess.CalledProcessError(ret, filename[:-1])
+    # deleting o explicitely now prevents Python 3.5 from
+    # reporting the following error: "<built-in function
+    # delete_automaton_parser_options> returned a result with
+    # an error set".  It's not clear to me if the bug is in Python
+    # or Swig.  At least it's related to the use of generators.
+    del o
+    return
+
+
+def automaton(filename, **kwargs):
+    """Read a single automaton from a file.
+
+    See `spot.automata` for a list of supported formats."""
+    try:
+        return next(automata(filename, **kwargs))
+    except StopIteration:
+        raise RuntimeError("Failed to read automaton from {}".format(filename))
+
+
+def _postproc_translate_options(obj, default_type, *args):
+    type_ = None
+    pref_ = None
+    optm_ = None
+    comp_ = 0
+    unam_ = 0
+    sbac_ = 0
+
+    def type_set(val):
+        nonlocal type_
+        if type_ is not None and type_ != val:
+            raise ValueError("type cannot be both {} and {}"
+                             .format(type_, val))
+        elif val == 'generic':
+            type_ = postprocessor.Generic
+        elif val == 'tgba':
+            type_ = postprocessor.TGBA
+        elif val == 'ba':
+            type_ = postprocessor.BA
+        else:
+            assert(val == 'monitor')
+            type_ = postprocessor.Monitor
+
+    def pref_set(val):
+        nonlocal pref_
+        if pref_ is not None and pref_ != val:
+            raise ValueError("preference cannot be both {} and {}"
+                             .format(pref_, val))
+        elif val == 'small':
+            pref_ = postprocessor.Small
+        elif val == 'deterministic':
+            pref_ = postprocessor.Deterministic
+        else:
+            assert(val == 'any')
+            pref_ = postprocessor.Any
+
+    def optm_set(val):
+        nonlocal optm_
+        if optm_ is not None and optm_ != val:
+            raise ValueError("optimization level cannot be both {} and {}"
+                             .format(optm_, val))
+        if val == 'high':
+            optm_ = postprocessor.High
+        elif val.startswith('med'):
+            optm_ = postprocessor.Medium
+        else:
+            assert(val == 'low')
+            optm_ = postprocessor.Low
+
+    def misc_set(val):
+        nonlocal comp_, unam_, sbac_
+        if val == 'complete':
+            comp_ = postprocessor.Complete
+        elif val == 'sbacc' or val == 'state-based-acceptance':
+            sbac_ = postprocessor.SBAcc
+        else:
+            assert(val == 'unambiguous')
+            unam_ = postprocessor.Unambiguous
+
+    options = {
+        'tgba': type_set,
+        'ba': type_set,
+        'monitor': type_set,
+        'generic': type_set,
+        'small': pref_set,
+        'deterministic': pref_set,
+        'any': pref_set,
+        'high': optm_set,
+        'medium': optm_set,
+        'low': optm_set,
+        'complete': misc_set,
+        'unambiguous': misc_set,
+        'statebasedacceptance': misc_set,
+        'sbacc': misc_set,
+    }
+
+    for arg in args:
+        arg = arg.lower()
+        fn = options.get(arg)
+        if fn:
+            fn(arg)
+        else:
+            # arg is not an know option, but maybe it is a prefix of
+            # one of them
+            compat = []
+            f = None
+            for key, fn in options.items():
+                if key.startswith(arg):
+                    compat.append(key)
+                    f = fn
+            lc = len(compat)
+            if lc == 1:
+                f(compat[0])
+            elif lc < 1:
+                raise ValueError("unknown option '{}'".format(arg))
+            else:
+                raise ValueError("ambiguous option '{}' is prefix of {}"
+                                 .format(arg, str(compat)))
+
+    if type_ is None:
+        type_ = default_type
+    if pref_ is None:
+        pref_ = postprocessor.Small
+    if optm_ is None:
+        optm_ = postprocessor.High
+
+    obj.set_type(type_)
+    obj.set_pref(pref_ | comp_ | unam_ | sbac_)
+    obj.set_level(optm_)
+
+
+def translate(formula, *args, dict=_bdd_dict):
+    """Translate a formula into an automaton.
+
+    Keep in mind that 'Deterministic' expresses just a preference that
+    may not be satisfied.
+
+    The optional arguments should be strings among the following:
+    - at most one in 'TGBA', 'BA', or 'Monitor'
+      (type of automaton to build)
+    - at most one in 'Small', 'Deterministic', 'Any'
+      (preferred characteristics of the produced automaton)
+    - at most one in 'Low', 'Medium', 'High'
+      (optimization level)
+    - any combination of 'Complete', 'Unambiguous', and
+      'StateBasedAcceptance' (or 'SBAcc' for short)
+
+    The default corresponds to 'tgba', 'small' and 'high'.
+    """
+    a = translator(dict)
+    _postproc_translate_options(a, postprocessor.TGBA, *args)
+    if type(formula) == str:
+        formula = parse_formula(formula)
+    return a.run(formula)
+
+
+formula.translate = translate
+
+
+def postprocess(automaton, *args, formula=None):
+    """Post process an automaton.
+
+    This applies a number of simlification algorithms, depending on
+    the options supplied. Keep in mind that 'Deterministic' expresses
+    just a preference that may not be satisfied if the input is
+    not already 'Deterministic'.
+
+    The optional arguments should be strings among the following:
+    - at most one in 'Generic', 'TGBA', 'BA', or 'Monitor'
+      (type of automaton to build)
+    - at most one in 'Small', 'Deterministic', 'Any'
+      (preferred characteristics of the produced automaton)
+    - at most one in 'Low', 'Medium', 'High'
+      (optimization level)
+    - any combination of 'Complete' and 'StateBasedAcceptance'
+      (or 'SBAcc' for short)
+
+    The default corresponds to 'generic', 'small' and 'high'.
+
+    If a formula denoted by this automaton is known, pass it to as the
+    optional `formula` argument; it can help some algorithms by
+    providing an easy way to complement the automaton.
+    """
+    p = postprocessor()
+    if type(automaton) == str:
+        automaton = globals()['automaton'](automaton)
+    _postproc_translate_options(p, postprocessor.Generic, *args)
+    return p.run(automaton, formula)
+
+
+twa.postprocess = postprocess
+
+# Wrap C++-functions into lambdas so that they get converted into
+# instance methods (i.e., self passed as first argument
+# automatically), because only used-defined functions are converted as
+# instance methods.
+def _add_twa_graph(meth):
+    setattr(twa_graph, meth, (lambda self, *args, **kwargs:
+                              globals()[meth](self, *args, **kwargs)))
+
+for meth in ('scc_filter', 'scc_filter_states',
+             'is_deterministic', 'is_unambiguous'):
+    _add_twa_graph(meth)
+
+# Wrapper around a formula iterator to which we add some methods of formula
+# (using _addfilter and _addmap), so that we can write things like
+# formulas.simplify().is_X_free().
+class formulaiterator:
+    def __init__(self, formulas):
+        self._formulas = formulas
+
+    def __iter__(self):
+        return self
+
+    def __next__(self):
+        return next(self._formulas)
+
+
+# fun shoud be a predicate and should be a method of formula.
+# _addfilter adds this predicate as a filter whith the same name in
+# formulaiterator.
+def _addfilter(fun):
+    def filtf(self, *args, **kwargs):
+        it = filter(lambda f: getattr(f, fun)(*args, **kwargs), self)
+        return formulaiterator(it)
+
+    def nfiltf(self, *args, **kwargs):
+        it = filter(lambda f: not getattr(f, fun)(*args, **kwargs), self)
+        return formulaiterator(it)
+
+    if fun[:3] == 'is_':
+        notfun = 'is_not_' + fun[3:]
+    elif fun[:4] == 'has_':
+        notfun = 'has_no_' + fun[4:]
+    else:
+        notfun = 'not_' + fun
+    setattr(formulaiterator, fun, filtf)
+    setattr(formulaiterator, notfun, nfiltf)
+
+
+# fun should be a function taking a formula as its first parameter and
+# returning a formula.  _addmap adds this function as a method of
+# formula and formulaiterator.
+def _addmap(fun):
+    def mapf(self, *args, **kwargs):
+        return formulaiterator(map(lambda f: getattr(f, fun)(*args, **kwargs),
+                                   self))
+    setattr(formula, fun,
+            lambda self, *args, **kwargs:
+            globals()[fun](self, *args, **kwargs))
+    setattr(formulaiterator, fun, mapf)
+
+
+def randltl(ap, n=-1, **kwargs):
+    """Generate random formulas.
+
+    Returns a random formula iterator.
+
+    ap: the number of atomic propositions used to generate random formulas.
+
+    n: number of formulas to generate, or unbounded if n < 0.
+
+    **kwargs:
+    seed: seed for the random number generator (0).
+    output: can be 'ltl', 'psl', 'bool' or 'sere' ('ltl').
+    allow_dups: allow duplicate formulas (False).
+    tree_size: tree size of the formulas generated, before mandatory
+    simplifications (15)
+    boolean_priorities: set priorities for Boolean formulas.
+    ltl_priorities: set priorities for LTL formulas.
+    sere_priorities: set priorities for SERE formulas.
+    dump_priorities: show current priorities, do not generate any formula.
+    simplify:
+      0           No rewriting
+      1           basic rewritings and eventual/universal rules
+      2           additional syntactic implication rules
+      3 (default) better implications using containment
+    """
+    opts = option_map()
+    output_map = {
+        "ltl": OUTPUTLTL,
+        "psl": OUTPUTPSL,
+        "bool": OUTPUTBOOL,
+        "sere": OUTPUTSERE
+    }
+
+    if isinstance(ap, list):
+        aprops = atomic_prop_set()
+        for elt in ap:
+            aprops.insert(formula.ap(elt))
+        ap = aprops
+    ltl_priorities = kwargs.get("ltl_priorities", None)
+    sere_priorities = kwargs.get("sere_priorities", None)
+    boolean_priorities = kwargs.get("boolean_priorities", None)
+    output = output_map[kwargs.get("output", "ltl")]
+    opts.set("output", output)
+    opts.set("seed", kwargs.get("seed", 0))
+    tree_size = kwargs.get("tree_size", 15)
+    if isinstance(tree_size, tuple):
+        tree_size_min, tree_size_max = tree_size
+    else:
+        tree_size_min = tree_size_max = tree_size
+    opts.set("tree_size_min", tree_size_min)
+    opts.set("tree_size_max", tree_size_max)
+    opts.set("unique", not kwargs.get("allow_dups", False))
+    opts.set("wf", kwargs.get("weak_fairness", False))
+    simpl_level = kwargs.get("simplify", 0)
+    if simpl_level > 3 or simpl_level < 0:
+        sys.stderr.write('invalid simplification level: ' + simpl_level)
+        return
+    opts.set("simplification_level", simpl_level)
+
+    rg = randltlgenerator(ap, opts, ltl_priorities, sere_priorities,
+                          boolean_priorities)
+
+    dump_priorities = kwargs.get("dump_priorities", False)
+    if dump_priorities:
+        dumpstream = ostringstream()
+        if output == OUTPUTLTL:
+            print('Use argument ltl_priorities=STRING to set the following '
+                  'LTL priorities:\n')
+            rg.dump_ltl_priorities(dumpstream)
+            print(dumpstream.str())
+        elif output == OUTPUTBOOL:
+            print('Use argument boolean_priorities=STRING to set the '
+                  'following Boolean formula priorities:\n')
+            rg.dump_bool_priorities(dumpstream)
+            print(dumpstream.str())
+        elif output == OUTPUTPSL or output == OUTPUTSERE:
+            if output != OUTPUTSERE:
+                print('Use argument ltl_priorities=STRING to set the '
+                      'following LTL priorities:\n')
+                rg.dump_psl_priorities(dumpstream)
+                print(dumpstream.str())
+            print('Use argument sere_priorities=STRING to set the '
+                  'following SERE priorities:\n')
+            rg.dump_sere_priorities(dumpstream)
+            print(dumpstream.str())
+            print('Use argument boolean_priorities=STRING to set the '
+                  'following Boolean formula priorities:\n')
+            rg.dump_sere_bool_priorities(dumpstream)
+            print(dumpstream.str())
+        else:
+            sys.stderr.write("internal error: unknown type of output")
+        return
+
+    class _randltliterator:
+        def __init__(self, rg, n):
+            self.rg = rg
+            self.i = 0
+            self.n = n
+
+        def __iter__(self):
+            return self
+
+        def __next__(self):
+            if self.i == self.n:
+                raise StopIteration
+            f = self.rg.next()
+            if f is None:
+                sys.stderr.write("Warning: could not generate a new "
+                                 "unique formula after {} trials.\n"
+                                 .format(MAX_TRIALS))
+                raise StopIteration
+            self.i += 1
+            return f
+
+    return formulaiterator(_randltliterator(rg, n))
+
+
+def simplify(f, **kwargs):
+    level = kwargs.get('level', None)
+    if level is not None:
+        return tl_simplifier(tl_simplifier_options(level)).simplify(f)
+
+    basics = kwargs.get('basics', True)
+    synt_impl = kwargs.get('synt_impl', True)
+    event_univ = kwargs.get('event_univ', True)
+    cont_checks = kwargs.get('containment_checks', False)
+    cont_checks_stronger = kwargs.get('containment_checks_stronger', False)
+    nenoform_stop_on_boolean = kwargs.get('nenoform_stop_on_boolean', False)
+    reduce_size_strictly = kwargs.get('reduce_size_strictly', False)
+    boolean_to_isop = kwargs.get('boolean_to_isop', False)
+    favor_event_univ = kwargs.get('favor_event_univ', False)
+
+    simp_opts = tl_simplifier_options(basics,
+                                       synt_impl,
+                                       event_univ,
+                                       cont_checks,
+                                       cont_checks_stronger,
+                                       nenoform_stop_on_boolean,
+                                       reduce_size_strictly,
+                                       boolean_to_isop,
+                                       favor_event_univ)
+    return tl_simplifier(simp_opts).simplify(f)
+
+
+for fun in dir(formula):
+    if (callable(getattr(formula, fun)) and (fun[:3] == 'is_' or
+                                             fun[:4] == 'has_')):
+        _addfilter(fun)
+
+for fun in ['remove_x', 'relabel', 'relabel_bse',
+            'simplify', 'unabbreviate']:
+    _addmap(fun)
+
+
+
+# Better interface to the corresponding C++ function.
+def sat_minimize(aut, acc=None, colored=False,
+                 state_based=False, states=0,
+                 max_states=0, dichotomy=False):
+    args=''
+    if acc is not None:
+        if type(acc) is not str:
+            raise ValueError("argument 'acc' should be a string")
+        args += ',acc="' + acc + '"'
+    if colored:
+        args += ',colored'
+    if states:
+        if type(states) is not int or states < 0:
+            raise ValueError("argument 'states' should be a positive integer")
+        args += ',states=' + str(states)
+    if max_states:
+        if type(max_states) is not int or max_states < 0:
+            raise ValueError("argument 'states' should be a positive integer")
+        args += ',max-states=' + str(max_states)
+    if dichotomy:
+        args += ',dichotomy';
+    from spot_impl import sat_minimize as sm
+    return sm(aut, args, state_based)
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@ -0,0 +1,728 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
+// 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.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+%{
+  // Workaround for SWIG 2.0.2 using ptrdiff_t but not including cstddef.
+  // It matters with g++ 4.6.
+#include <cstddef>
+%}
+
+
+%module(package="spot", director="1") impl
+
+%include "std_shared_ptr.i"
+%include "std_vector.i"
+%include "std_string.i"
+%include "std_list.i"
+%include "std_set.i"
+%include "std_map.i"
+%include "std_pair.i"
+%include "stdint.i"
+%include "exception.i"
+%include "typemaps.i"
+
+ // git grep 'typedef.*std::shared_ptr' | grep -v const |
+ //   sed 's/.*<\(.*\)>.*/%shared_ptr(spot::\1)/g'
+%shared_ptr(spot::dstar_aut)
+%shared_ptr(spot::parsed_aut)
+%shared_ptr(spot::fair_kripke)
+%shared_ptr(spot::kripke)
+%shared_ptr(spot::kripke_graph)
+%shared_ptr(spot::kripke)
+%shared_ptr(spot::ta)
+%shared_ptr(spot::ta_explicit)
+%shared_ptr(spot::ta_product)
+%shared_ptr(spot::tgta)
+%shared_ptr(spot::tgta_explicit)
+%shared_ptr(spot::bdd_dict)
+%shared_ptr(spot::twa)
+%shared_ptr(spot::twa_graph)
+%shared_ptr(spot::twa_product)
+%shared_ptr(spot::twa_product_init)
+%shared_ptr(spot::taa_tgba)
+%shared_ptr(spot::taa_tgba_string)
+%shared_ptr(spot::taa_tgba_formula)
+%shared_ptr(spot::twa_safra_complement)
+%shared_ptr(spot::twa_run)
+%shared_ptr(spot::emptiness_check_result)
+%shared_ptr(spot::emptiness_check)
+%shared_ptr(spot::emptiness_check_instantiator)
+%shared_ptr(spot::tgbasl)
+
+%import "buddy.i"
+
+%{
+#include <iostream>
+#include <fstream>
+#include <sstream>
+#include <signal.h>
+
+#include <spot/misc/common.hh>
+#include <spot/misc/version.hh>
+#include <spot/misc/minato.hh>
+#include <spot/misc/optionmap.hh>
+#include <spot/misc/random.hh>
+#include <spot/misc/escape.hh>
+#include <spot/misc/trival.hh>
+
+#include <spot/tl/formula.hh>
+
+#include <spot/tl/environment.hh>
+#include <spot/tl/defaultenv.hh>
+
+#include <spot/tl/parse.hh>
+
+#include <spot/twa/bdddict.hh>
+
+#include <spot/tl/apcollect.hh>
+#include <spot/tl/dot.hh>
+#include <spot/tl/nenoform.hh>
+#include <spot/tl/print.hh>
+#include <spot/tl/simplify.hh>
+#include <spot/tl/unabbrev.hh>
+#include <spot/tl/randomltl.hh>
+#include <spot/tl/length.hh>
+#include <spot/tl/remove_x.hh>
+#include <spot/tl/relabel.hh>
+
+#include <spot/twa/bddprint.hh>
+#include <spot/twa/fwd.hh>
+#include <spot/twa/acc.hh>
+#include <spot/twa/twa.hh>
+#include <spot/twa/taatgba.hh>
+#include <spot/twa/twaproduct.hh>
+
+#include <spot/twaalgos/cleanacc.hh>
+#include <spot/twaalgos/degen.hh>
+#include <spot/twaalgos/dot.hh>
+#include <spot/twaalgos/copy.hh>
+#include <spot/twaalgos/complete.hh>
+#include <spot/twaalgos/complement.hh>
+#include <spot/twaalgos/emptiness.hh>
+#include <spot/twaalgos/gtec/gtec.hh>
+#include <spot/twaalgos/lbtt.hh>
+#include <spot/twaalgos/ltl2taa.hh>
+#include <spot/twaalgos/ltl2tgba_fm.hh>
+#include <spot/twaalgos/compsusp.hh>
+#include <spot/twaalgos/magic.hh>
+#include <spot/twaalgos/minimize.hh>
+#include <spot/twaalgos/neverclaim.hh>
+#include <spot/twaalgos/remfin.hh>
+#include <spot/twaalgos/strength.hh>
+#include <spot/twaalgos/sccfilter.hh>
+#include <spot/twaalgos/stats.hh>
+#include <spot/twaalgos/isdet.hh>
+#include <spot/twaalgos/isunamb.hh>
+#include <spot/twaalgos/simulation.hh>
+#include <spot/twaalgos/postproc.hh>
+#include <spot/twaalgos/product.hh>
+#include <spot/twaalgos/stutter.hh>
+#include <spot/twaalgos/translate.hh>
+#include <spot/twaalgos/hoa.hh>
+#include <spot/twaalgos/dtwasat.hh>
+#include <spot/twaalgos/relabel.hh>
+
+#include <spot/parseaut/public.hh>
+
+#include <spot/ta/ta.hh>
+#include <spot/ta/tgta.hh>
+#include <spot/ta/taexplicit.hh>
+#include <spot/ta/tgtaexplicit.hh>
+#include <spot/taalgos/tgba2ta.hh>
+#include <spot/taalgos/dot.hh>
+#include <spot/taalgos/stats.hh>
+#include <spot/taalgos/minimize.hh>
+
+using namespace spot;
+%}
+
+
+// Swig come with iterators that implement a decrement method.
+// This is not supported in our "successor" iterators.
+%fragment("ForwardIterator_T","header",fragment="SwigPyIterator_T") {
+namespace swig
+{
+  template<typename OutIterator,
+	   typename ValueType =
+	   typename std::iterator_traits<OutIterator>::value_type,
+	   typename FromOper = from_oper<ValueType> >
+  class ForwardIterator_T :  public SwigPyIterator_T<OutIterator>
+  {
+  public:
+    FromOper from;
+    typedef OutIterator out_iterator;
+    typedef ValueType value_type;
+    typedef SwigPyIterator_T<out_iterator>  base;
+    typedef ForwardIterator_T<OutIterator, ValueType, FromOper> self_type;
+
+    ForwardIterator_T(out_iterator curr, out_iterator first,
+		      out_iterator last, PyObject *seq)
+      : SwigPyIterator_T<OutIterator>(curr, seq), begin(first), end(last)
+    {
+    }
+
+    PyObject *value() const {
+      if (base::current == end) {
+	throw stop_iteration();
+      } else {
+	return from(static_cast<const value_type&>(*(base::current)));
+      }
+    }
+
+    SwigPyIterator *copy() const
+    {
+      return new self_type(*this);
+    }
+
+    SwigPyIterator *incr(size_t n = 1)
+    {
+      while (n--) {
+	if (base::current == end) {
+	  throw stop_iteration();
+	} else {
+	  ++base::current;
+	}
+      }
+      return this;
+    }
+
+  private:
+    out_iterator begin;
+    out_iterator end;
+  };
+
+  template<typename OutIter>
+  inline SwigPyIterator*
+  make_forward_iterator(const OutIter& current,
+			const OutIter& begin,
+			const OutIter& end, PyObject *seq = 0)
+  {
+    return new ForwardIterator_T<OutIter>(current, begin, end, seq);
+  }
+}
+}
+%fragment("ForwardIterator_T");
+
+// For spot::emptiness_check_instantiator::construct and any other
+// function that return errors via a "char **err" argument.
+%typemap(in, numinputs=0) char** OUTPUT (char* temp) {
+  $1 = &temp;
+}
+%typemap(argout) char** OUTPUT {
+  PyObject *obj = SWIG_FromCharPtr(*$1);
+  if (!$result) {
+    $result = obj;
+  //# If the function returns null_ptr (i.e. Py_None), we
+  //# don't want to override it with OUTPUT as in the
+  //# default implementation of t_output_helper.
+  // } else if ($result == Py_None) {
+  //   Py_DECREF($result);
+  //   $result = obj;
+  } else {
+    if (!PyList_Check($result)) {
+      PyObject *o2 = $result;
+      $result = PyList_New(1);
+      PyList_SetItem($result, 0, o2);
+    }
+    PyList_Append($result, obj);
+    Py_DECREF(obj);
+  }
+
+ };
+%apply char** OUTPUT { char** err };
+
+// This is mainly for acc_cond::is_parity()
+%typemap(in, numinputs=0) bool& (bool temp) {
+  $1 = &temp;
+ };
+%typemap(argout) bool& {
+  PyObject *obj = SWIG_From_bool(*$1);
+  if (!$result) {
+    $result = obj;
+  } else {
+    if (!PyList_Check($result)) {
+      PyObject *o2 = $result;
+      $result = PyList_New(1);
+      PyList_SetItem($result, 0, o2);
+    }
+    PyList_Append($result, obj);
+    Py_DECREF(obj);
+  }
+ };
+
+// Allow None to be passed for formula.  Some functions like
+// postprocessor::run() take an optional formula that defaults to
+// nullptr.  So it make sense to have function that take formulas that
+// default to None on the Python side.
+%typemap(in) spot::formula {
+    void *tmp;
+    int res = SWIG_ConvertPtr($input, &tmp, $descriptor(spot::formula*), 0);
+    if (!SWIG_IsOK(res)) {
+      %argument_fail(res, "spot::formula", $symname, $argnum);
+    }
+    if (tmp) {
+      spot::formula* temp = reinterpret_cast< spot::formula * >(tmp);
+      $1 = *temp;
+      if (SWIG_IsNewObj(res)) delete temp;
+    }
+    // if tmp == nullptr, then the default value of $1 is fine.
+}
+
+%typemap(typecheck) spot::formula {
+    $1 = SWIG_CheckState(SWIG_ConvertPtr($input, nullptr,
+					 $descriptor(spot::formula*), 0));
+}
+
+%typemap(out) spot::formula {
+  if (!$1)
+    $result = SWIG_Py_Void();
+  else
+    $result = SWIG_NewPointerObj(new spot::formula($1), $descriptor(spot::formula*), SWIG_POINTER_OWN);
+}
+
+%typemap(out) std::string* {
+  if (!$1)
+    $result = SWIG_Py_Void();
+  else
+    $result = SWIG_FromCharPtr($1->c_str());
+}
+
+%exception {
+  try {
+    $action
+  }
+  catch (const spot::parse_error& e)
+  {
+    std::string er("\n");
+    er += e.what();
+    SWIG_exception(SWIG_SyntaxError, er.c_str());
+  }
+  catch (const std::invalid_argument& e)
+  {
+    SWIG_exception(SWIG_ValueError, e.what());
+  }
+  catch (const std::runtime_error& e)
+  {
+    SWIG_exception(SWIG_RuntimeError, e.what());
+  }
+}
+
+%include <spot/misc/common.hh>
+%include <spot/misc/version.hh>
+%include <spot/misc/minato.hh>
+%include <spot/misc/optionmap.hh>
+%include <spot/misc/random.hh>
+%include <spot/misc/escape.hh>
+
+%implicitconv spot::trival;
+%include <spot/misc/trival.hh>
+
+%implicitconv std::vector<spot::formula>;
+
+%include <spot/tl/formula.hh>
+
+namespace std {
+  %template(liststr) list<std::string>;
+  %template(vectorformula) vector<spot::formula>;
+  %template(vectorunsigned) vector<unsigned>;
+  %template(vectorstring) vector<string>;
+  %template(atomic_prop_set) set<spot::formula>;
+  %template(relabeling_map) map<spot::formula, spot::formula>;
+}
+
+%include <spot/tl/environment.hh>
+%include <spot/tl/defaultenv.hh>
+
+%include <spot/tl/parse.hh>
+
+ /* these must come before apcollect.hh */
+%include <spot/twa/bdddict.hh>
+%include <spot/twa/bddprint.hh>
+%include <spot/twa/fwd.hh>
+%implicitconv spot::acc_cond::mark_t;
+%implicitconv spot::acc_cond::acc_code;
+%feature("flatnested") spot::acc_cond::mark_t;
+%feature("flatnested") spot::acc_cond::acc_code;
+%apply bool* OUTPUT {bool& max, bool& odd};
+%include <spot/twa/acc.hh>
+%template(pair_bool_mark) std::pair<bool, spot::acc_cond::mark_t>;
+
+%include <spot/twa/twa.hh>
+
+%include <spot/tl/apcollect.hh>
+%include <spot/tl/dot.hh>
+%include <spot/tl/nenoform.hh>
+%include <spot/tl/print.hh>
+%include <spot/tl/simplify.hh>
+%include <spot/tl/unabbrev.hh>
+%include <spot/tl/randomltl.hh>
+%include <spot/tl/length.hh>
+%include <spot/tl/remove_x.hh>
+%include <spot/tl/relabel.hh>
+
+%include <spot/twa/taatgba.hh>
+%include <spot/twa/twaproduct.hh>
+
+%include <spot/graph/graph.hh>
+%nodefaultctor spot::digraph;
+%nodefaultctor spot::internal::state_out;
+%traits_swigtype(spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >);
+%fragment(SWIG_Traits_frag(spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >));
+
+%typemap(out, optimal="1") spot::internal::state_out<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>> {
+  $result = SWIG_NewPointerObj(new $1_ltype($1), $&1_descriptor,
+			       SWIG_POINTER_OWN);
+}
+
+%noexception spot::twa_graph::out;
+%include <spot/twa/twagraph.hh>
+
+%template(twa_graph_state_out) spot::internal::state_out<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>>;
+%template(twa_graph_edge_boxed_data) spot::internal::boxed_label<spot::twa_graph_edge_data, false>;
+%template(twa_graph_edge_storage) spot::internal::edge_storage<unsigned int, unsigned int, unsigned int, spot::internal::boxed_label<spot::twa_graph_edge_data, false> >;
+
+// Should come after the definition of twa_graph
+
+%include <spot/twaalgos/cleanacc.hh>
+%include <spot/twaalgos/degen.hh>
+%include <spot/twaalgos/dot.hh>
+%include <spot/twaalgos/copy.hh>
+%include <spot/twaalgos/complete.hh>
+%include <spot/twaalgos/complement.hh>
+%include <spot/twaalgos/emptiness.hh>
+%include <spot/twaalgos/gtec/gtec.hh>
+%include <spot/twaalgos/lbtt.hh>
+%include <spot/twaalgos/ltl2taa.hh>
+%include <spot/twaalgos/ltl2tgba_fm.hh>
+%include <spot/twaalgos/compsusp.hh>
+%include <spot/twaalgos/magic.hh>
+%include <spot/twaalgos/minimize.hh>
+%include <spot/twaalgos/neverclaim.hh>
+%include <spot/twaalgos/remfin.hh>
+%include <spot/twaalgos/strength.hh>
+%include <spot/twaalgos/sccfilter.hh>
+%include <spot/twaalgos/stats.hh>
+%include <spot/twaalgos/isdet.hh>
+%include <spot/twaalgos/isunamb.hh>
+%include <spot/twaalgos/simulation.hh>
+%include <spot/twaalgos/postproc.hh>
+%include <spot/twaalgos/product.hh>
+%include <spot/twaalgos/stutter.hh>
+%include <spot/twaalgos/translate.hh>
+%include <spot/twaalgos/hoa.hh>
+%include <spot/twaalgos/dtwasat.hh>
+%include <spot/twaalgos/relabel.hh>
+
+%include <spot/parseaut/public.hh>
+
+%include <spot/ta/ta.hh>
+%include <spot/ta/tgta.hh>
+%include <spot/ta/taexplicit.hh>
+%include <spot/ta/tgtaexplicit.hh>
+%include <spot/taalgos/tgba2ta.hh>
+%include <spot/taalgos/dot.hh>
+%include <spot/taalgos/stats.hh>
+%include <spot/taalgos/minimize.hh>
+
+
+%extend spot::trival {
+  std::string __repr__()
+  {
+    std::ostringstream os;
+    os << *self;
+    return os.str();
+  }
+
+  std::string __str__()
+  {
+    std::ostringstream os;
+    os << *self;
+    return os.str();
+  }
+
+  spot::trival __neg__()
+  {
+    return !*self;
+  }
+
+  spot::trival __and__(spot::trival other)
+  {
+    return *self && other;
+  }
+
+  spot::trival __or__(spot::trival other)
+  {
+    return *self || other;
+  }
+}
+
+%exception spot::formula::__getitem__ {
+  try {
+    $action
+  }
+  catch (const std::runtime_error& e)
+  {
+    SWIG_exception(SWIG_IndexError, e.what());
+  }
+}
+
+%extend spot::formula {
+  // __cmp__ is for Python 2.0
+  int __cmp__(spot::formula b) { return self->id() - b.id(); }
+  size_t __hash__() { return self->id(); }
+  unsigned __len__() { return self->size(); }
+  formula __getitem__(unsigned pos) { return (*self)[pos]; }
+
+  std::string __repr__() { return spot::str_psl(*self); }
+  std::string _repr_latex_()
+  {
+    return std::string("$") + spot::str_sclatex_psl(*self) + '$';
+  }
+  std::string __str__() { return spot::str_psl(*self); }
+}
+
+%extend spot::bdd_dict {
+  bool operator==(const spot::bdd_dict& b) const
+  {
+    return self == &b;
+  }
+
+  bool operator!=(const spot::bdd_dict& b) const
+  {
+    return self != &b;
+  }
+}
+
+%extend spot::twa {
+  void set_name(std::string name)
+  {
+    self->set_named_prop("automaton-name", new std::string(name));
+  }
+
+  std::string* get_name()
+  {
+    return self->get_named_prop<std::string>("automaton-name");
+  }
+
+  void set_state_names(std::vector<std::string> names)
+  {
+    self->set_named_prop("state-names",
+			 new std::vector<std::string>(std::move(names)));
+  }
+
+  std::vector<std::string>* get_state_names()
+  {
+    return self->get_named_prop<std::vector<std::string>>("state-names");
+  }
+}
+
+
+%extend spot::internal::state_out<spot::digraph<spot::twa_graph_state, spot::twa_graph_edge_data>> {
+  swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF)
+   {
+      return swig::make_forward_iterator(self->begin(), self->begin(),
+				         self->end(), *PYTHON_SELF);
+   }
+}
+
+%extend spot::acc_cond::acc_code {
+  std::string __repr__()
+  {
+    std::ostringstream os;
+    os << *self;
+    return os.str();
+  }
+
+  std::string __str__()
+  {
+    std::ostringstream os;
+    os << *self;
+    return os.str();
+  }
+}
+
+%extend spot::acc_cond::mark_t {
+  // http://comments.gmane.org/gmane.comp.programming.swig/14822
+  mark_t(const std::vector<unsigned>& f)
+  {
+    return new spot::acc_cond::mark_t(f.begin(), f.end());
+  }
+
+  std::string __repr__()
+  {
+    std::ostringstream os;
+    os << *self;
+    return os.str();
+  }
+
+  std::string __str__()
+  {
+    std::ostringstream os;
+    os << *self;
+    return os.str();
+  }
+}
+
+%extend spot::acc_cond {
+  std::string __repr__()
+  {
+    std::ostringstream os;
+    os << *self;
+    return os.str();
+  }
+
+  std::string __str__()
+  {
+    std::ostringstream os;
+    os << *self;
+    return os.str();
+  }
+}
+
+%extend spot::twa_run {
+  std::string __str__()
+  {
+    std::ostringstream os;
+    os << *self;
+    return os.str();
+  }
+}
+
+%nodefaultctor std::ostream;
+namespace std {
+  class ostream {};
+  class ofstream : public ostream
+  {
+  public:
+     ofstream(const char *fn);
+     ~ofstream();
+  };
+  class ostringstream : public ostream
+  {
+  public:
+     ostringstream();
+     std::string str() const;
+     ~ostringstream();
+  };
+}
+
+%inline %{
+bool fnode_instances_check()
+{
+  return spot::fnode::instances_check();
+}
+
+spot::parse_error_list
+empty_parse_error_list()
+{
+  parse_error_list l;
+  return l;
+}
+
+spot::parse_aut_error_list
+empty_parse_aut_error_list()
+{
+  parse_aut_error_list l;
+  return l;
+}
+
+spot::twa_graph_ptr
+ensure_digraph(const spot::twa_ptr& a)
+{
+  auto aa = std::dynamic_pointer_cast<spot::twa_graph>(a);
+  if (aa)
+    return aa;
+  return spot::make_twa_graph(a, spot::twa::prop_set::all());
+}
+
+std::ostream&
+get_cout()
+{
+  return std::cout;
+}
+
+void
+nl_cout()
+{
+  std::cout << std::endl;
+}
+
+std::ostream&
+get_cerr()
+{
+  return std::cerr;
+}
+
+void
+nl_cerr()
+{
+  std::cerr << std::endl;
+}
+
+void
+print_on(std::ostream& on, const std::string& what)
+{
+  on << what;
+}
+
+int
+unblock_signal(int signum)
+{
+  sigset_t set;
+  sigemptyset(&set);
+  sigaddset(&set, signum);
+  return sigprocmask(SIG_UNBLOCK, &set, 0);
+}
+
+%}
+
+%extend spot::parse_error_list {
+
+bool
+__nonzero__()
+{
+  return !self->empty();
+}
+
+bool
+__bool__()
+{
+  return !self->empty();
+}
+
+}
+
+%extend spot::parse_aut_error_list {
+
+bool
+__nonzero__()
+{
+  return !self->empty();
+}
+
+bool
+__bool__()
+{
+  return !self->empty();
+}
+
+}