python: better way to extend existing classes
* wrap/python/spot.py: Use a decorator to extend classes. * wrap/python/tests/formulas.ipynb: Adjust expected help text.
This commit is contained in:
Alexandre Duret-Lutz
parent
1f0258e9f7
commit
e8ce08a989
2 changed files with 173 additions and 174 deletions
|
|
@ -23,6 +23,21 @@ import sys
|
||||||
from functools import lru_cache
|
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
|
||||||
|
|
||||||
|
|
||||||
def setup(**kwargs):
|
def setup(**kwargs):
|
||||||
"""Configure Spot for fancy display.
|
"""Configure Spot for fancy display.
|
||||||
|
|
||||||
|
|
@ -56,6 +71,7 @@ def setup(**kwargs):
|
||||||
d = 'rf({})'.format(kwargs.get('font', 'Lato')) + bullets
|
d = 'rf({})'.format(kwargs.get('font', 'Lato')) + bullets
|
||||||
os.environ['SPOT_DOTDEFAULT'] = d
|
os.environ['SPOT_DOTDEFAULT'] = d
|
||||||
|
|
||||||
|
|
||||||
# In version 3.0.2, Swig puts strongly typed enum in the main
|
# In version 3.0.2, Swig puts strongly typed enum in the main
|
||||||
# namespace without prefixing them. Latter versions fix this. So we
|
# 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
|
# can remove for following hack once 3.0.2 is no longer used in our
|
||||||
|
|
@ -92,201 +108,184 @@ def _ostream_to_svg(ostr):
|
||||||
return _str_to_svg(ostr.str().encode('utf-8'))
|
return _str_to_svg(ostr.str().encode('utf-8'))
|
||||||
|
|
||||||
|
|
||||||
def _render_automaton_as_svg(a, opt=None):
|
@_extend(twa, ta)
|
||||||
ostr = ostringstream()
|
class twa:
|
||||||
print_dot(ostr, a, opt)
|
def _repr_svg_(self, opt=None):
|
||||||
return _ostream_to_svg(ostr)
|
"""Output the automaton as SVG"""
|
||||||
|
ostr = ostringstream()
|
||||||
|
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"""
|
||||||
|
# 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))
|
||||||
|
|
||||||
|
|
||||||
twa._repr_svg_ = _render_automaton_as_svg
|
@_extend(twa)
|
||||||
ta._repr_svg_ = _render_automaton_as_svg
|
class twa:
|
||||||
|
def to_str(a, format='hoa', opt=None):
|
||||||
|
format = format.lower()
|
||||||
def _render_formula_as_svg(a):
|
if format == 'hoa':
|
||||||
# Load the SVG function only if we need it. This way the bindings
|
ostr = ostringstream()
|
||||||
# can still be used outside of IPython if IPython is not
|
print_hoa(ostr, a, opt)
|
||||||
# installed.
|
return ostr.str()
|
||||||
from IPython.display import SVG
|
if format == 'dot':
|
||||||
ostr = ostringstream()
|
ostr = ostringstream()
|
||||||
print_dot_psl(ostr, a)
|
print_dot(ostr, a, opt)
|
||||||
return SVG(_ostream_to_svg(ostr))
|
return ostr.str()
|
||||||
|
if format == 'spin':
|
||||||
|
ostr = ostringstream()
|
||||||
def _return_automaton_as_svg(a, opt=None):
|
print_never_claim(ostr, a, opt)
|
||||||
# Load the SVG function only if we need it. This way the bindings
|
return ostr.str()
|
||||||
# can still be used outside of IPython if IPython is not
|
if format == 'lbtt':
|
||||||
# installed.
|
ostr = ostringstream()
|
||||||
from IPython.display import SVG
|
print_lbtt(ostr, a, opt)
|
||||||
return SVG(_render_automaton_as_svg(a, opt))
|
return ostr.str()
|
||||||
|
|
||||||
|
|
||||||
twa.show = _return_automaton_as_svg
|
|
||||||
ta.show = _return_automaton_as_svg
|
|
||||||
|
|
||||||
|
|
||||||
def _formula_str_ctor(self, str):
|
|
||||||
self.this = parse_formula(str)
|
|
||||||
|
|
||||||
|
|
||||||
def _formula_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)
|
|
||||||
else:
|
|
||||||
raise ValueError("unknown string format: " + format)
|
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
|
||||||
|
|
||||||
def _formula_format(self, spec):
|
|
||||||
"""Format the formula according to `spec`.
|
|
||||||
|
|
||||||
Parameters
|
@_extend(formula)
|
||||||
----------
|
class formula:
|
||||||
spec : str, optional
|
def __init__(self, str):
|
||||||
a list of letters that specify how the formula
|
"""Parse the given string to create a formula."""
|
||||||
should be formatted.
|
self.this = parse_formula(str)
|
||||||
|
|
||||||
Supported specifiers
|
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
|
||||||
|
ostr = ostringstream()
|
||||||
|
print_dot_psl(ostr, self)
|
||||||
|
return SVG(_ostream_to_svg(ostr))
|
||||||
|
|
||||||
- 'f': use Spot's syntax (default)
|
def to_str(self, format='spot', parenth=False):
|
||||||
- '8': use Spot's syntax in UTF-8 mode
|
if format == 'spot' or format == 'f':
|
||||||
- 's': use Spin's syntax
|
return str_psl(self, parenth)
|
||||||
- 'l': use LBT's syntax
|
elif format == 'spin' or format == 's':
|
||||||
- 'w': use Wring's syntax
|
return str_spin_ltl(self, parenth)
|
||||||
- 'x': use LaTeX output
|
elif format == 'utf8' or format == '8':
|
||||||
- 'X': use self-contained LaTeX output
|
return str_utf8_psl(self, parenth)
|
||||||
|
elif format == 'lbt' or format == 'l':
|
||||||
Add some of those letters for additional options:
|
return str_lbt_ltl(self)
|
||||||
|
elif format == 'wring' or format == 'w':
|
||||||
- 'p': use full parentheses
|
return str_wring_ltl(self)
|
||||||
- 'c': escape the formula for CSV output (this will
|
elif format == 'latex' or format == 'x':
|
||||||
enclose the formula in double quotes, and escape
|
return str_latex_psl(self, parenth)
|
||||||
any included double quotes)
|
elif format == 'sclatex' or format == 'X':
|
||||||
- 'h': escape the formula for HTML output
|
return str_sclatex_psl(self, parenth)
|
||||||
- '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:
|
else:
|
||||||
raise ValueError("unknown format specification: " + c + spec)
|
raise ValueError("unknown string format: " + format)
|
||||||
|
|
||||||
s = self.to_str(syntax, parent)
|
def __format__(self, spec):
|
||||||
|
"""Format the formula according to `spec`.
|
||||||
|
|
||||||
if escape == 'c':
|
Parameters
|
||||||
o = ostringstream()
|
----------
|
||||||
escape_rfc4180(o, s)
|
spec : str, optional
|
||||||
s = '"' + o.str() + '"'
|
a list of letters that specify how the formula
|
||||||
elif escape == 'd':
|
should be formatted.
|
||||||
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)
|
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
|
||||||
|
|
||||||
def _formula_traverse(self, func):
|
Add some of those letters for additional options:
|
||||||
if func(self):
|
|
||||||
return
|
|
||||||
for f in self:
|
|
||||||
f.traverse(func)
|
|
||||||
|
|
||||||
|
- '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.
|
||||||
|
|
||||||
def _formula_map(self, func):
|
- ':spec': pass the remaining specification to the
|
||||||
k = self.kind()
|
formating function for strings.
|
||||||
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")
|
|
||||||
|
|
||||||
|
"""
|
||||||
|
|
||||||
formula.__init__ = _formula_str_ctor
|
syntax = 'f'
|
||||||
formula.to_str = _formula_to_str
|
parent = False
|
||||||
formula.show_ast = _render_formula_as_svg
|
escape = None
|
||||||
formula.traverse = _formula_traverse
|
|
||||||
formula.__format__ = _formula_format
|
|
||||||
formula.map = _formula_map
|
|
||||||
|
|
||||||
|
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)
|
||||||
|
|
||||||
def _twa_to_str(a, format='hoa', opt=None):
|
s = self.to_str(syntax, parent)
|
||||||
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)
|
|
||||||
|
|
||||||
|
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()
|
||||||
|
|
||||||
def _twa_save(a, filename, format='hoa', opt=None, append=False):
|
return s.__format__(spec)
|
||||||
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
|
|
||||||
|
|
||||||
|
def traverse(self, func):
|
||||||
|
if func(self):
|
||||||
|
return
|
||||||
|
for f in self:
|
||||||
|
f.traverse(func)
|
||||||
|
|
||||||
twa.to_str = _twa_to_str
|
def map(self, func):
|
||||||
twa.save = _twa_save
|
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(*filenames):
|
def automata(*filenames):
|
||||||
|
|
|
||||||
|
|
@ -243,9 +243,9 @@
|
||||||
"output_type": "stream",
|
"output_type": "stream",
|
||||||
"stream": "stdout",
|
"stream": "stdout",
|
||||||
"text": [
|
"text": [
|
||||||
"Help on function _formula_format in module spot:\n",
|
"Help on function __format__ in module spot:\n",
|
||||||
"\n",
|
"\n",
|
||||||
"_formula_format(self, spec)\n",
|
"__format__(self, spec)\n",
|
||||||
" Format the formula according to `spec`.\n",
|
" Format the formula according to `spec`.\n",
|
||||||
" \n",
|
" \n",
|
||||||
" Parameters\n",
|
" Parameters\n",
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue