diff --git a/wrap/python/spot.py b/wrap/python/spot.py
index 535d367ef..8b583c8b9 100644
--- a/wrap/python/spot.py
+++ b/wrap/python/spot.py
@@ -31,9 +31,9 @@ def _ostream_to_svg(ostr):
res = dotty.communicate()
return res[0].decode('utf-8')
-def _render_automaton_as_svg(a):
+def _render_automaton_as_svg(a, opt=""):
ostr = ostringstream()
- dotty_reachable(ostr, a)
+ dotty_reachable(ostr, a, opt)
return _ostream_to_svg(ostr)
tgba._repr_svg_ = _render_automaton_as_svg
@@ -47,6 +47,14 @@ def _render_formula_as_svg(a):
dotty(ostr, a)
return SVG(_ostream_to_svg(ostr))
+def _render_tgba_as_svg(a, opt=""):
+ # 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(_render_automaton_as_svg(a, opt))
+tgba.show = _render_tgba_as_svg
+
def _formula_str_ctor(self, str):
self.this = parse_formula(str)
@@ -72,10 +80,69 @@ formula.__init__ = _formula_str_ctor
formula.to_str = _formula_to_str
formula.show_ast = _render_formula_as_svg
-def _tgba_str_ctor(self, str):
- self.this = ltl_to_tgba_fm(parse_formula(str), _bdd_dict)
+def translate(formula, output='tgba', pref='small', level='high',
+ complete=False):
+ """Translate a formula into an automaton.
-tgba.__init__ = _tgba_str_ctor
+ Keep in mind that pref expresses just a preference that may not be
+ satisfied.
+
+ Keyword arguments:
+ output -- the type of automaton to build ('tgba', 'ba', 'monitor')
+ pref -- prefered characteristic of the produced automaton
+ ('small', 'deterministic', 'any')
+ level -- level of optimizations ('low', 'medium', 'high')
+ complete -- whether to produce a complete automaton (True, False)
+ """
+ if type(formula) == str:
+ formula = parse_formula(formula)
+
+ a = translator()
+
+ if type(output) == str:
+ output_ = output.lower()
+ if output_ == 'tgba':
+ output = postprocessor.TGBA
+ elif output_ == 'ba':
+ output = postprocessor.BA
+ elif output_.startswith('mon'):
+ output = postprocessor.Monitor
+ else:
+ raise ValueError("unknown output type: " + output)
+ a.set_type(output)
+
+ if complete:
+ complete = postprocessor.Complete
+ else:
+ complete = 0
+
+ if type(pref) == str:
+ pref_ = pref.lower()
+ if pref_.startswith('sm'):
+ pref = postprocessor.Small
+ elif pref_.startswith('det'):
+ pref = postprocessor.Deterministic
+ elif pref_ == 'any':
+ pref = postprocessor.Any
+ else:
+ raise ValueError("unknown output preference: " + pref)
+ a.set_pref(pref | complete)
+
+ if type(level) == str:
+ level_ = level.lower()
+ if level_ == 'high':
+ level = postprocessor.High
+ elif level_.starswith('med'):
+ level = postprocessor.Medium
+ elif level_ == 'low':
+ level = postprocessor.Low
+ else:
+ raise ValueError("unknown optimization level: " + level)
+ a.set_level(level)
+
+ return a.run(formula)
+
+formula.translate = translate
# Wrapper around a formula iterator to which we add some methods of formula
# (using _addfilter and _addmap), so that we can write things like
diff --git a/wrap/python/tests/Makefile.am b/wrap/python/tests/Makefile.am
index 518866fc4..b01bf3ed6 100644
--- a/wrap/python/tests/Makefile.am
+++ b/wrap/python/tests/Makefile.am
@@ -32,6 +32,7 @@ check_SCRIPTS = run
TESTS = \
alarm.py \
+ automata.ipynb \
bddnqueen.py \
formulas.ipynb \
implies.py \
diff --git a/wrap/python/tests/automata.ipynb b/wrap/python/tests/automata.ipynb
new file mode 100644
index 000000000..1ed4ffc98
--- /dev/null
+++ b/wrap/python/tests/automata.ipynb
@@ -0,0 +1,844 @@
+{
+ "metadata": {
+ "name": "",
+ "signature": "sha256:6c1898261f2fab59f18fc3b6d75fe387d6f811b02935833fc74fa5e476796d4c"
+ },
+ "nbformat": 3,
+ "nbformat_minor": 0,
+ "worksheets": [
+ {
+ "cells": [
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "import spot"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [],
+ "prompt_number": 1
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "a = spot.translate('(a U b) & GFc & GFd', 'BA', complete=True); a"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 2,
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7f79a4a46090> >"
+ ]
+ }
+ ],
+ "prompt_number": 2
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "a.show(\"cs\")"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 3,
+ "svg": [
+ ""
+ ],
+ "text": [
+ ""
+ ]
+ }
+ ],
+ "prompt_number": 3
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "f = spot.formula('a U b'); f"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "latex": [
+ "$a \\mathbin{\\mathsf{U}} b$"
+ ],
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 4,
+ "text": [
+ "a U b"
+ ]
+ }
+ ],
+ "prompt_number": 4
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "spot.translate(f)"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 5,
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7f79a4aa1810> >"
+ ]
+ }
+ ],
+ "prompt_number": 5
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "f.translate()"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 6,
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7f79a4aa1930> >"
+ ]
+ }
+ ],
+ "prompt_number": 6
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "f.translate('mon')"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 7,
+ "svg": [
+ "\n",
+ "\n",
+ "\n",
+ "\n",
+ "\n"
+ ],
+ "text": [
+ " *' at 0x7f79a4aa18a0> >"
+ ]
+ }
+ ],
+ "prompt_number": 7
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "f = spot.formula('Ga | Gb | Gc'); f"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "latex": [
+ "$\\mathsf{G} a \\lor \\mathsf{G} b \\lor \\mathsf{G} c$"
+ ],
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 8,
+ "text": [
+ "Ga | Gb | Gc"
+ ]
+ }
+ ],
+ "prompt_number": 8
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "f.translate('ba', 'small').show('vc')"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 9,
+ "svg": [
+ ""
+ ],
+ "text": [
+ ""
+ ]
+ }
+ ],
+ "prompt_number": 9
+ },
+ {
+ "cell_type": "code",
+ "collapsed": false,
+ "input": [
+ "f.translate('ba', 'det').show('vc')"
+ ],
+ "language": "python",
+ "metadata": {},
+ "outputs": [
+ {
+ "metadata": {},
+ "output_type": "pyout",
+ "prompt_number": 12,
+ "svg": [
+ ""
+ ],
+ "text": [
+ ""
+ ]
+ }
+ ],
+ "prompt_number": 12
+ }
+ ],
+ "metadata": {}
+ }
+ ]
+}
\ No newline at end of file