alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

modernize some Python code

Browse source 
Since we now require Python 3.6, we can use f-strings instead of
format() to make the code more readable.

* doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut21.org, doc/org/tut24.org, doc/org/tut90.org,
python/spot/__init__.py, python/spot/jupyter.py, tests/python/acc.py,
tests/python/acc_cond.ipynb, tests/python/complement_semidet.py,
tests/python/decompose.ipynb, tests/python/formulas.ipynb,
tests/python/highlighting.ipynb, tests/python/ipnbdoctest.py,
tests/python/ltlf.py, tests/python/parity.ipynb,
tests/python/product.ipynb, tests/python/relabel.py,
tests/python/satmin.ipynb, tests/python/stutter-inv.ipynb,
tests/python/twagraph-internals.ipynb, tests/python/zlktree.ipynb: Use
f-strings.
This commit is contained in:
Alexandre Duret-Lutz 2024-03-26 20:35:10 +01:00
parent df44f7a5c2
commit 7ac570fa3f
23 changed files with 292 additions and 327 deletions
Download patch file Download diff file Expand all files Collapse all files

3
doc/org/tut01.org
View file

@ -389,7 +389,8 @@ In C++ you can enable lenient using one of the Boolean arguments of
Formulas have a custom format specification language that allows you Formulas have a custom format specification language that allows you
to easily change the way a formula should be output when using the to easily change the way a formula should be output when using the
=format()= method of strings. =format()= method of strings, or using [[https://docs.python.org/3/tutorial/inputoutput.html#formatted-string-literals][formatted string litterals]].
#+BEGIN_SRC python #+BEGIN_SRC python
import spot import spot

4
doc/org/tut02.org
View file

@ -68,8 +68,8 @@ import spot
m = spot.relabeling_map() m = spot.relabeling_map()
g = spot.relabel('"Proc@Here" U ("var > 10" | "var < 4")', spot.Pnn, m) g = spot.relabel('"Proc@Here" U ("var > 10" | "var < 4")', spot.Pnn, m)
for newname, oldname in m.items(): for newname, oldname in m.items():
print("#define {} ({})".format(newname.to_str(), oldname.to_str('spin', True))) print(f"#define {newname.to_str()} ({oldname.to_str('spin', True)})")
print(g.to_str('spin', True)) print(g.to_str('spin', True))
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:

4
doc/org/tut03.org
View file

@ -159,9 +159,9 @@ The Python equivalent is similar:
# kindstr() prints the name of the operator # kindstr() prints the name of the operator
# size() return the number of operands of the operators # size() return the number of operands of the operators
print("{}, {} children".format(f.kindstr(), f.size())) print(f"{f.kindstr()}, {f.size()} children")
# [] accesses each operand # [] accesses each operand
print("left: {f[0]}, right: {f[1]}".format(f=f)) print(f"left: {f[0]}, right: {f[1]}")
# you can also iterate over all operands using a for loop # you can also iterate over all operands using a for loop
for child in f: for child in f:
print(" *", child) print(" *", child)

4
doc/org/tut21.org
View file

@ -557,9 +557,9 @@ Here is the very same example, but written in Python:
print("Stutter Invariant:", aut.prop_stutter_invariant()) print("Stutter Invariant:", aut.prop_stutter_invariant())
for s in range(0, aut.num_states()): for s in range(0, aut.num_states()):
print("State {}:".format(s)) print(f"State {s}:")
for t in aut.out(s): for t in aut.out(s):
print(" edge({} -> {})".format(t.src, t.dst)) print(f" edge({t.src} -> {t.dst})")
# bdd_print_formula() is designed to print on a std::ostream, and # bdd_print_formula() is designed to print on a std::ostream, and
# is inconvenient to use in Python. Instead we use # is inconvenient to use in Python. Instead we use
# bdd_format_formula() as this simply returns a string. # bdd_format_formula() as this simply returns a string.

36
doc/org/tut24.org
View file

@ -190,26 +190,26 @@ decide whether to enclose the destinations in braces.
Here is the Python version of this code: Here is the Python version of this code:
#+BEGIN_SRC python #+BEGIN_SRC python
import spot import spot
aut = spot.automaton("tut24.hoa")
bdict = aut.get_dict() aut = spot.automaton("tut24.hoa")
init = aut.get_init_state_number()
ui = aut.is_univ_dest(init) def format_dest(s):
print("Initial states: {}{}{}".format("{ " if ui else "", if not aut.is_univ_dest(s):
" ".join(map(str, aut.univ_dests(init))), return s
" }" if ui else "")) else:
for s in range(0, aut.num_states()): return f'{{ {" ".join(map(str, aut.univ_dests(s)))} }}'
print("State {}:".format(s))
for t in aut.out(s): bdict = aut.get_dict()
ud = aut.is_univ_dest(t) init = aut.get_init_state_number()
print(" edge({} -> {}{}{})".format(t.src, print(f"Initial states: {format_dest(init)}")
"{ " if ud else "", for s in range(0, aut.num_states()):
" ".join(map(str, aut.univ_dests(t))), print("State {}:".format(s))
" }" if ud else "")) for t in aut.out(s):
print(" label =", spot.bdd_format_formula(bdict, t.cond)) print(f" edge({t.src} -> {format_dest(t.dst)})")
print(" acc sets =", t.acc) print(" label =", spot.bdd_format_formula(bdict, t.cond))
print(" acc sets =", t.acc)
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:

8
doc/org/tut90.org
View file

@ -108,12 +108,12 @@ import spot
aut1 = spot.make_twa_graph() aut1 = spot.make_twa_graph()
ap1a = aut1.register_ap("a") ap1a = aut1.register_ap("a")
ap1b = aut1.register_ap("b") ap1b = aut1.register_ap("b")
print("aut1: a={} b={}".format(ap1a, ap1b)) print(f"aut1: a={ap1a} b={ap1b}")
aut2 = spot.make_twa_graph() aut2 = spot.make_twa_graph()
ap2c = aut2.register_ap("c") ap2c = aut2.register_ap("c")
ap2b = aut2.register_ap("b") ap2b = aut2.register_ap("b")
ap2a = aut2.register_ap("a") ap2a = aut2.register_ap("a")
print("aut1: a={} b={} c={}".format(ap2a, ap2b, ap2c)) print(f"aut1: a={ap2a} b={ap2b} c={ap2c}")
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
@ -271,7 +271,7 @@ all transition that belong to a certain acceptance set.
self.set.add((src, guard, dst)) self.set.add((src, guard, dst))
def str_trans(self, src, guard, dst): def str_trans(self, src, guard, dst):
f = spot.bdd_format_formula(self.dict, guard) f = spot.bdd_format_formula(self.dict, guard)
return "({},{},{})".format(src, f, dst) return f"({src},{f},{dst})"
def __str__(self): def __str__(self):
return '{' + ",".join([ self.str_trans(*t) for t in self.set ]) + '}' return '{' + ",".join([ self.str_trans(*t) for t in self.set ]) + '}'
@ -353,7 +353,7 @@ automaton registers its variables.
self.set.add((src, guard, dest)) self.set.add((src, guard, dest))
def str_trans(self, src, guard, dest): def str_trans(self, src, guard, dest):
f = spot.bdd_format_formula(self.dict, guard) f = spot.bdd_format_formula(self.dict, guard)
return "({},{},{})".format(src, f, dest) return f"({src},{f},{dest})"
def __str__(self): def __str__(self):
return '{' + ",".join([ self.str_trans(*t) for t in self.set ]) + '}' return '{' + ",".join([ self.str_trans(*t) for t in self.set ]) + '}'

53
python/spot/__init__.py
View file

@ -512,7 +512,7 @@ class acd:
.acdrej polygon{fill:red;} .acdrej polygon{fill:red;}
.acdacc polygon{fill:green;} .acdacc polygon{fill:green;}
''' '''
js = ''' js = f'''
function acdremclasses(sel, classes) {{ function acdremclasses(sel, classes) {{
document.querySelectorAll(sel).forEach(n=>{{n.classList.remove(...classes)}});}} document.querySelectorAll(sel).forEach(n=>{{n.classList.remove(...classes)}});}}
function acdaddclasses(sel, classes) {{ function acdaddclasses(sel, classes) {{
@ -545,30 +545,26 @@ function acd{num}_node(node, acc){{
acdaddclasses("#acdaut{num} .acdN" + node, acdaddclasses("#acdaut{num} .acdN" + node,
[acc ? "acdacc" : "acdrej", "acdbold"]); [acc ? "acdacc" : "acdrej", "acdbold"]);
acdaddclasses("#acd{num} #N" + node, ["acdbold", "acdhigh"]); acdaddclasses("#acd{num} #N" + node, ["acdbold", "acdhigh"]);
}};'''.format(num=num) }};'''
me = 0 me = 0
for n in range(self.node_count()): for n in range(self.node_count()):
for e in self.edges_of_node(n): for e in self.edges_of_node(n):
me = max(e, me) me = max(e, me)
js += 'acdaddclasses("#acdaut{num} #E{e}", ["acdN{n}"]);\n'\ js += f'acdaddclasses("#acdaut{num} #E{e}", ["acdN{n}"]);\n'
.format(num=num, e=e, n=n)
for e in range(1, me + 1): for e in range(1, me + 1):
js += 'acdonclick("#acdaut{num} #E{e}",'\ js += f'acdonclick("#acdaut{num} #E{e}",'\
'function(){{acd{num}_edge({e});}});\n'\ f'function(){{acd{num}_edge({e});}});\n'
.format(num=num, e=e)
for s in range(self.get_aut().num_states()): for s in range(self.get_aut().num_states()):
js += 'acdonclick("#acdaut{num} #S{s}",'\ js += f'acdonclick("#acdaut{num} #S{s}",'\
'function(){{acd{num}_state({s});}});\n'\ f'function(){{acd{num}_state({s});}});\n'
.format(num=num, s=s)
for n in range(self.node_count()): for n in range(self.node_count()):
v = int(self.node_acceptance(n)) v = int(self.node_acceptance(n))
js += 'acdonclick("#acd{num} #N{n}",'\ js += f'acdonclick("#acd{num} #N{n}",'\
'function(){{acd{num}_node({n}, {v});}});\n'\ f'function(){{acd{num}_node({n}, {v});}});\n'
.format(num=num, n=n, v=v)
html = '<style>{}</style><div>{}</div><div>{}</div><script>{}</script>'\ html = '<style>{}</style><div>{}</div><div>{}</div><script>{}</script>'\
.format(style, .format(style,
self.get_aut().show('.i(acdaut{})'.format(num)).data, self.get_aut().show(f'.i(acdaut{num})').data,
self._repr_svg_("acd{}".format(num)), self._repr_svg_(f"acd{num}"),
js); js);
return html return html
@ -746,7 +742,7 @@ def automaton(filename, **kwargs):
try: try:
return next(automata(filename, **kwargs)) return next(automata(filename, **kwargs))
except StopIteration: except StopIteration:
raise RuntimeError("Failed to read automaton from {}".format(filename)) raise RuntimeError(f"Failed to read automaton from {filename}")
def aiger_circuits(*sources, bdd_dict = None): def aiger_circuits(*sources, bdd_dict = None):
"""Read aiger circuits from a list of sources. """Read aiger circuits from a list of sources.
@ -777,7 +773,7 @@ def aiger_circuit(source, bdd_dict = None):
return next(aiger_circuits(source, bdd_dict = bdd_dict)) return next(aiger_circuits(source, bdd_dict = bdd_dict))
except StopIteration: except StopIteration:
raise RuntimeError("Failed to read an aiger circuit " raise RuntimeError("Failed to read an aiger circuit "
"from {}".format(source)) f"from {source}")
def _postproc_translate_options(obj, default_type, *args): def _postproc_translate_options(obj, default_type, *args):
@ -795,8 +791,7 @@ def _postproc_translate_options(obj, default_type, *args):
def type_set(val): def type_set(val):
nonlocal type_, type_name_ nonlocal type_, type_name_
if type_ is not None and type_name_ != val: if type_ is not None and type_name_ != val:
raise ValueError("type cannot be both {} and {}" raise ValueError(f"type cannot be both {type_name_} and {val}")
.format(type_name_, val))
elif val == 'generic' or val == 'gen' or val == 'g': elif val == 'generic' or val == 'gen' or val == 'g':
type_ = postprocessor.Generic type_ = postprocessor.Generic
elif val == 'tgba': # historical elif val == 'tgba': # historical
@ -839,8 +834,8 @@ def _postproc_translate_options(obj, default_type, *args):
def pref_set(val): def pref_set(val):
nonlocal pref_, pref_name_ nonlocal pref_, pref_name_
if pref_ is not None and pref_name_ != val: if pref_ is not None and pref_name_ != val:
raise ValueError("preference cannot be both {} and {}" raise ValueError("preference cannot be both "\
.format(pref_name_, val)) f"{pref_name_} and {val}")
elif val == 'small': elif val == 'small':
pref_ = postprocessor.Small pref_ = postprocessor.Small
elif val == 'deterministic': elif val == 'deterministic':
@ -853,8 +848,8 @@ def _postproc_translate_options(obj, default_type, *args):
def optm_set(val): def optm_set(val):
nonlocal optm_, optm_name_ nonlocal optm_, optm_name_
if optm_ is not None and optm_name_ != val: if optm_ is not None and optm_name_ != val:
raise ValueError("optimization level cannot be both {} and {}" raise ValueError("optimization level cannot be both "\
.format(optm_name_, val)) f"{optm_name_} and {val}")
if val == 'high': if val == 'high':
optm_ = postprocessor.High optm_ = postprocessor.High
elif val.startswith('med'): elif val.startswith('med'):
@ -930,10 +925,10 @@ def _postproc_translate_options(obj, default_type, *args):
if lc == 1: if lc == 1:
f(compat[0]) f(compat[0])
elif lc < 1: elif lc < 1:
raise ValueError("unknown option '{}'".format(arg)) raise ValueError(f"unknown option '{arg}'")
else: else:
raise ValueError("ambiguous option '{}' is prefix of {}" raise ValueError(f"ambiguous option '{arg}' "\
.format(arg, str(compat))) f"is prefix of {str(compat)}")
if type_ is None: if type_ is None:
type_ = default_type type_ = default_type
@ -1307,7 +1302,7 @@ def sat_minimize(aut, acc=None, colored=False,
if display_log or return_log: if display_log or return_log:
import pandas as pd import pandas as pd
with tempfile.NamedTemporaryFile(dir='.', suffix='.satlog') as t: with tempfile.NamedTemporaryFile(dir='.', suffix='.satlog') as t:
args += ',log="{}"'.format(t.name) args += f',log="{t.name}"'
aut = sm(aut, args, state_based) aut = sm(aut, args, state_based)
dfrm = pd.read_csv(t.name, dtype=object) dfrm = pd.read_csv(t.name, dtype=object)
if display_log: if display_log:
@ -1397,10 +1392,10 @@ def mp_hierarchy_svg(cl=None):
'B': '110,198', 'B': '110,198',
} }
if cl in coords: if cl in coords:
highlight = '''<g transform="translate({})"> highlight = f'''<g transform="translate({coords[cl]})">
<line x1="-10" y1="-10" x2="10" y2="10" stroke="red" stroke-width="5" /> <line x1="-10" y1="-10" x2="10" y2="10" stroke="red" stroke-width="5" />
<line x1="-10" y1="10" x2="10" y2="-10" stroke="red" stroke-width="5" /> <line x1="-10" y1="10" x2="10" y2="-10" stroke="red" stroke-width="5" />
</g>'''.format(coords[cl]) </g>'''
else: else:
highlight = '' highlight = ''
return ''' return '''

11
python/spot/jupyter.py
View file

@ -51,11 +51,11 @@ def display_inline(*args, per_row=None, show=None):
If the `per_row` argument is given, at most `per_row` arguments are If the `per_row` argument is given, at most `per_row` arguments are
displayed on each row, each one taking 1/per_row of the line width. displayed on each row, each one taking 1/per_row of the line width.
""" """
width = res = '' w = res = ''
if per_row: if per_row:
width = 'width:{}%;'.format(100//per_row) w = f'width:{100//per_row}%;'
for arg in args: for arg in args:
dpy = 'inline-block' dpy = 'display:inline-block'
if show is not None and hasattr(arg, 'show'): if show is not None and hasattr(arg, 'show'):
arg = arg.show(show) arg = arg.show(show)
if hasattr(arg, '_repr_html_'): if hasattr(arg, '_repr_html_'):
@ -65,9 +65,8 @@ def display_inline(*args, per_row=None, show=None):
elif hasattr(arg, '_repr_latex_'): elif hasattr(arg, '_repr_latex_'):
rep = arg._repr_latex_() rep = arg._repr_latex_()
if not per_row: if not per_row:
dpy = 'inline' dpy = 'display:inline'
else: else:
rep = str(arg) rep = str(arg)
res += ("<div style='vertical-align:text-top;display:{};{}'>{}</div>" res += f"<div style='vertical-align:text-top;{dpy};{w}'>{rep}</div>"
.format(dpy, width, rep))
display(HTML(res)) display(HTML(res))

2
tests/python/acc.py
View file

@ -22,7 +22,7 @@ tc = TestCase()
a = spot.acc_cond('parity min odd 5') a = spot.acc_cond('parity min odd 5')
tc.assertEqual(str(a.fin_unit_one_split()), tc.assertEqual(str(a.fin_unit_one_split()),
'(0, {}, spot.acc_cond(5, "f"))'.format(repr(a))) f'(0, {a!r}, spot.acc_cond(5, "f"))')
a.set_acceptance('Rabin 3') a.set_acceptance('Rabin 3')
tc.assertEqual(str(a.fin_unit_one_split()), tc.assertEqual(str(a.fin_unit_one_split()),

42
tests/python/acc_cond.ipynb
View file

@ -11,7 +11,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -100,7 +99,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -131,7 +129,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -194,7 +191,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -220,7 +216,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -252,7 +247,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -280,7 +274,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -331,7 +324,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -359,7 +351,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -400,7 +391,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -428,7 +418,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -455,7 +444,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -483,7 +471,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -552,7 +539,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -603,7 +589,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -630,7 +615,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -743,7 +727,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -775,11 +758,10 @@
"acc = spot.acc_code('Fin(0) & Inf(1) | Inf(2)')\n", "acc = spot.acc_code('Fin(0) & Inf(1) | Inf(2)')\n",
"print(\"acc =\", acc)\n", "print(\"acc =\", acc)\n",
"for x in ([0, 1, 2], [1, 2], [0, 1], [0, 2], [0], [1], [2], []):\n", "for x in ([0, 1, 2], [1, 2], [0, 1], [0, 2], [0], [1], [2], []):\n",
" print(\"acc.accepting({}) = {}\".format(x, acc.accepting(x)))" " print(f\"acc.accepting({x}) = {acc.accepting(x)}\")"
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -809,7 +791,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -837,7 +818,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -873,7 +853,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -909,7 +888,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -978,7 +956,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -1049,7 +1026,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -1078,7 +1054,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -1108,7 +1083,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -1138,7 +1112,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -1170,7 +1143,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -1202,7 +1174,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -1235,7 +1206,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -1264,7 +1234,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -1292,7 +1261,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -1320,7 +1288,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -1346,11 +1313,10 @@
"source": [ "source": [
"print(\"acc =\", acc)\n", "print(\"acc =\", acc)\n",
"for x in ([0, 1, 2, 3, 10], [1, 2]):\n", "for x in ([0, 1, 2, 3, 10], [1, 2]):\n",
" print(\"acc.accepting({}) = {}\".format(x, acc.accepting(x)))" " print(f\"acc.accepting({x}) = {acc.accepting(x)}\")"
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -1419,7 +1385,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -1446,7 +1411,6 @@
] ]
}, },
{ {
"attachments": {},
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
@ -1566,7 +1530,7 @@
"name": "python", "name": "python",
"nbconvert_exporter": "python", "nbconvert_exporter": "python",
"pygments_lexer": "ipython3", "pygments_lexer": "ipython3",
"version": "3.10.5" "version": "3.11.8"
} }
}, },
"nbformat": 4, "nbformat": 4,

3
tests/python/complement_semidet.py
View file

@ -31,8 +31,7 @@ n = 10000
for aut in spot.automata( for aut in spot.automata(
"randltl -n-1 a b " "randltl -n-1 a b "
"| ltl2tgba " "| ltl2tgba "
"| autfilt --is-semi-deterministic --acceptance-is=Buchi -n{} |" f"| autfilt --is-semi-deterministic --acceptance-is=Buchi -n{n} |"):
.format(n)):
comp = complement(aut) comp = complement(aut)
semidet_comp = spot.complement_semidet(aut, True) semidet_comp = spot.complement_semidet(aut, True)

83
tests/python/decompose.ipynb
View file

@ -359,7 +359,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c1623d0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7cffd80> >"
] ]
}, },
"execution_count": 2, "execution_count": 2,
@ -583,7 +583,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c162340> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d10240> >"
] ]
}, },
"execution_count": 3, "execution_count": 3,
@ -874,7 +874,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c161fe0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d103f0> >"
] ]
}, },
"execution_count": 4, "execution_count": 4,
@ -1043,7 +1043,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c162070> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d10600> >"
] ]
}, },
"execution_count": 5, "execution_count": 5,
@ -1175,7 +1175,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c162eb0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d10a80> >"
] ]
}, },
"execution_count": 6, "execution_count": 6,
@ -1400,7 +1400,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c163390> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d110e0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1681,7 +1681,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c163360> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7cffde0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -2008,7 +2008,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c163390> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7cfff60> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -2775,7 +2775,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c162b50> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d115f0> >"
] ]
}, },
"execution_count": 8, "execution_count": 8,
@ -3509,7 +3509,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c162c70> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d10c00> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -3964,7 +3964,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c163390> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7cfff60> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -4375,7 +4375,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c162c70> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d10c00> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -5120,7 +5120,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c163c00> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d10a20> >"
] ]
}, },
"execution_count": 10, "execution_count": 10,
@ -5415,7 +5415,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c163b40> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d10b40> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -5684,7 +5684,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c163a80> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d119e0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -5965,7 +5965,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c163e10> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d114d0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -6637,7 +6637,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c163150> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d11c20> >"
] ]
}, },
"execution_count": 12, "execution_count": 12,
@ -7293,7 +7293,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c162c10> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d12460> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -7638,7 +7638,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c163e10> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d114d0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -7945,7 +7945,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c162c10> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d12460> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -8612,7 +8612,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c163240> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d12160> >"
] ]
}, },
"execution_count": 14, "execution_count": 14,
@ -8823,7 +8823,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c163d50> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d11c80> >"
] ]
}, },
"execution_count": 15, "execution_count": 15,
@ -8989,7 +8989,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c17c870> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d120d0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -9132,7 +9132,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c1634b0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d11290> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -9293,7 +9293,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c17c540> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d11e60> >"
] ]
}, },
"execution_count": 18, "execution_count": 18,
@ -9557,7 +9557,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c17c570> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d10180> >"
] ]
}, },
"execution_count": 19, "execution_count": 19,
@ -9830,7 +9830,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c17db90> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d137b0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -10025,7 +10025,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c162c10> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d12460> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -10279,7 +10279,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c1626d0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d137b0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -10315,10 +10315,10 @@
"name": "stdout", "name": "stdout",
"output_type": "stream", "output_type": "stream",
"text": [ "text": [
"SCC #0 contains states [1]\n", "SCC #0 contains states (1,)\n",
"SCC #1 contains states [4]\n", "SCC #1 contains states (4,)\n",
"SCC #2 contains states [3]\n", "SCC #2 contains states (3,)\n",
"SCC #3 contains states [0, 2]\n" "SCC #3 contains states (0, 2)\n"
] ]
}, },
{ {
@ -10642,7 +10642,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c17d410> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d124c0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -10915,7 +10915,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c17d3e0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d117d0> >"
] ]
}, },
"execution_count": 21, "execution_count": 21,
@ -10927,7 +10927,7 @@
"aut = spot.translate('(Ga -> Gb) W c')\n", "aut = spot.translate('(Ga -> Gb) W c')\n",
"si = spot.scc_info(aut)\n", "si = spot.scc_info(aut)\n",
"for scc in range(si.scc_count()):\n", "for scc in range(si.scc_count()):\n",
" print(\"SCC #{} contains states {}\".format(scc, list(si.states_of(scc))))\n", " print(f\"SCC #{scc} contains states {si.states_of(scc)}\")\n",
"display(aut)\n", "display(aut)\n",
"spot.decompose_scc(si, '0,1')" "spot.decompose_scc(si, '0,1')"
] ]
@ -11089,7 +11089,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f328c17e160> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7faaf7d13420> >"
] ]
}, },
"execution_count": 22, "execution_count": 22,
@ -11100,6 +11100,13 @@
"source": [ "source": [
"spot.decompose_scc(si, 'a2')" "spot.decompose_scc(si, 'a2')"
] ]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
} }
], ],
"metadata": { "metadata": {
@ -11118,7 +11125,7 @@
"name": "python", "name": "python",
"nbconvert_exporter": "python", "nbconvert_exporter": "python",
"pygments_lexer": "ipython3", "pygments_lexer": "ipython3",
"version": "3.11.7" "version": "3.11.8"
} }
}, },
"nbformat": 4, "nbformat": 4,

20
tests/python/formulas.ipynb
View file

@ -189,14 +189,14 @@
], ],
"source": [ "source": [
"for i in ['spot', 'spin', 'lbt', 'wring', 'utf8', 'latex', 'sclatex', 'mathjax']:\n", "for i in ['spot', 'spin', 'lbt', 'wring', 'utf8', 'latex', 'sclatex', 'mathjax']:\n",
" print(\"%-10s%s\" % (i, f.to_str(i)))" " print(f\"{i:10}{f.to_str(i)}\")"
] ]
}, },
{ {
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
"Formulas output via `format()` can also use some convenient shorthand to select the syntax:" "Formulas output via `format()` of f-strings can also use some convenient shorthand to select the syntax:"
] ]
}, },
{ {
@ -218,13 +218,13 @@
} }
], ],
"source": [ "source": [
"print(\"\"\"\\\n", "print(f\"\"\"\\\n",
"Spin: {0:s}\n", "Spin: {f:s}\n",
"Spin+parentheses: {0:sp}\n", "Spin+parentheses: {f:sp}\n",
"Spot (default): {0}\n", "Spot (default): {f}\n",
"Spot+shell quotes: {0:q}\n", "Spot+shell quotes: {f:q}\n",
"LBT, right aligned: {0:l:~>40}\n", "LBT, right aligned: {f:l:~>40}\n",
"LBT, no M/W/R: {0:[MWR]l}\"\"\".format(f))" "LBT, no M/W/R: {f:[MWR]l}\"\"\")"
] ]
}, },
{ {
@ -1050,7 +1050,7 @@
"name": "python", "name": "python",
"nbconvert_exporter": "python", "nbconvert_exporter": "python",
"pygments_lexer": "ipython3", "pygments_lexer": "ipython3",
"version": "3.11.7" "version": "3.11.8"
} }
}, },
"nbformat": 4, "nbformat": 4,

50
tests/python/highlighting.ipynb
View file

@ -330,7 +330,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4156190> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed1691bbd0> >"
] ]
}, },
"execution_count": 4, "execution_count": 4,
@ -525,7 +525,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fa7f4155f80> >" "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fed16a24420> >"
] ]
}, },
"execution_count": 5, "execution_count": 5,
@ -718,7 +718,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4156190> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed1691bbd0> >"
] ]
}, },
"execution_count": 6, "execution_count": 6,
@ -830,9 +830,9 @@
], ],
"source": [ "source": [
"for i in range(0, a.num_states()):\n", "for i in range(0, a.num_states()):\n",
" print(\"state {}: {}\".format(i, a.get_highlight_state(i)))\n", " print(f\"state {i}: {a.get_highlight_state(i)}\")\n",
"for i in range(1, a.num_edges() + 1):\n", "for i in range(1, a.num_edges() + 1):\n",
" print(\"edge {}: {}\".format(i, a.get_highlight_edge(i)))" " print(f\"edge {i}: {a.get_highlight_edge(i)}\")"
] ]
}, },
{ {
@ -1023,7 +1023,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fa7f4157900> >" "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fed16a248a0> >"
] ]
}, },
"execution_count": 9, "execution_count": 9,
@ -1218,7 +1218,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fa7f4157780> >" "<spot.twa; proxy of <Swig Object of type 'std::shared_ptr< spot::twa > *' at 0x7fed16a25c80> >"
] ]
}, },
"execution_count": 10, "execution_count": 10,
@ -1517,7 +1517,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f41574b0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a25950> >"
] ]
}, },
"execution_count": 11, "execution_count": 11,
@ -1846,7 +1846,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f41574b0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a25950> >"
] ]
}, },
"execution_count": 14, "execution_count": 14,
@ -2493,7 +2493,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f41745d0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a26100> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -3006,7 +3006,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4156100> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a252c0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -3363,7 +3363,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4157480> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a25e00> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -3536,7 +3536,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4174d80> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a26340> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -3637,7 +3637,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4174210> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a26100> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -3804,7 +3804,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4174f30> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a25f80> >"
] ]
}, },
"execution_count": 17, "execution_count": 17,
@ -4006,7 +4006,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4174f30> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a25f80> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -4127,7 +4127,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4174d80> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a26340> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -4228,7 +4228,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4174210> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a26100> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -4635,7 +4635,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7fa7f4176160> >" "<spot.impl.twa_product; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_product > *' at 0x7fed16a279c0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -4796,7 +4796,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4175320> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a25e90> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -4981,7 +4981,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4176130> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a27990> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -5284,7 +5284,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4175950> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a27480> >"
] ]
}, },
"execution_count": 22, "execution_count": 22,
@ -5586,7 +5586,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4175950> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a27480> >"
] ]
}, },
"execution_count": 23, "execution_count": 23,
@ -5883,7 +5883,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fa7f4175950> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fed16a27480> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -6391,7 +6391,7 @@
"name": "python", "name": "python",
"nbconvert_exporter": "python", "nbconvert_exporter": "python",
"pygments_lexer": "ipython3", "pygments_lexer": "ipython3",
"version": "3.11.7" "version": "3.11.8"
} }
}, },
"nbformat": 4, "nbformat": 4,

5
tests/python/ipnbdoctest.py
View file

@ -154,7 +154,7 @@ def canonicalize(s, type, ignores):
s, flags=re.DOTALL) s, flags=re.DOTALL)
for n, p in enumerate(ignores): for n, p in enumerate(ignores):
s = re.sub(p, 'IGN{}'.format(n), s) s = re.sub(p, f'IGN{n}', s)
return s return s
@ -219,8 +219,7 @@ def compare_outputs(ref, test, ignores=[]):
ok = True ok = True
if len(cref) != len(ctest): if len(cref) != len(ctest):
print("output length mismatch (expected {}, got {})".format( print(f"output length mismatch: expected {len(cref)}, got {len(ctest)}")
len(cref), len(ctest)))
ok = False ok = False
# There can be several outputs. For instance wnen the cell both # There can be several outputs. For instance wnen the cell both
# prints a result (goes to "stdout") and displays an automaton # prints a result (goes to "stdout") and displays an automaton

4
tests/python/ltlf.py
View file

@ -42,7 +42,7 @@ for f in formulas:
f2 = f1.unabbreviate() f2 = f1.unabbreviate()
f3 = spot.formula_And([spot.from_ltlf(f1), cst]) f3 = spot.formula_And([spot.from_ltlf(f1), cst])
f4 = spot.formula_And([spot.from_ltlf(f2), cst]) f4 = spot.formula_And([spot.from_ltlf(f2), cst])
print("{}\t=>\t{}".format(f1, f3)) print(f"{f1}\t=>\t{f3}")
print("{}\t=>\t{}".format(f2, f4)) print(f"{f2}\t=>\t{f4}")
tc.assertTrue(lcc.equal(f3, f4)) tc.assertTrue(lcc.equal(f3, f4))
print() print()

8
tests/python/parity.ipynb
View file

@ -64,8 +64,8 @@
"for kind in ['min', 'max']:\n", "for kind in ['min', 'max']:\n",
" for style in ['odd', 'even']:\n", " for style in ['odd', 'even']:\n",
" for sets in range(1, 5):\n", " for sets in range(1, 5):\n",
" name = 'parity {} {} {}'.format(kind, style, sets)\n", " name = f'parity {kind} {style} {sets}'\n",
" print('{:17} = {}'.format(name, spot.acc_code(name)))" " print(f'{name:17} = {spot.acc_code(name)}')"
] ]
}, },
{ {
@ -4949,7 +4949,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fc0d6bea0d0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f88de01ed30> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -5460,7 +5460,7 @@
"name": "python", "name": "python",
"nbconvert_exporter": "python", "nbconvert_exporter": "python",
"pygments_lexer": "ipython3", "pygments_lexer": "ipython3",
"version": "3.11.7" "version": "3.11.8"
} }
}, },
"nbformat": 4, "nbformat": 4,

16
tests/python/product.ipynb
View file

@ -779,8 +779,7 @@
], ],
"source": [ "source": [
"def show_prod(a1, a2, res):\n", "def show_prod(a1, a2, res):\n",
" s1 = a1.num_sets()\n", " display_inline(a1, a2.show(f'.tvb+{a1.num_sets()}'), res)\n",
" display_inline(a1, a2.show('.tvb+{}'.format(s1)), res)\n",
"\n", "\n",
"show_prod(a1, a2, prod)" "show_prod(a1, a2, prod)"
] ]
@ -1714,7 +1713,7 @@
"\n", "\n",
"The one-liner above is wrong for two reasons:\n", "The one-liner above is wrong for two reasons:\n",
"\n", "\n",
" - if `left` and `right` are non-deterministic, their product could be deterministic, so calling prop_universal(False) would be wrong. \n", " - if `left` and `right` are non-deterministic, their product could be deterministic, so calling `prop_universal(False)` would be wrong. \n",
"\n", "\n",
" - the use of the `and` operator on `trival` is misleading in non-Boolean context. The `&` operator would be the correct operator to use if you want to work in threed-valued logic. Compare: " " - the use of the `and` operator on `trival` is misleading in non-Boolean context. The `&` operator would be the correct operator to use if you want to work in threed-valued logic. Compare: "
] ]
@ -1746,8 +1745,7 @@
"maybe = spot.trival_maybe()\n", "maybe = spot.trival_maybe()\n",
"for u in (no, maybe, yes):\n", "for u in (no, maybe, yes):\n",
" for v in (no, maybe, yes):\n", " for v in (no, maybe, yes):\n",
" print(\"{u!s:>5} & {v!s:<5} = {r1!s:<5} {u!s:>5} and {v!s:<5} = {r2!s:<5}\"\n", " print(f\"{u!s:>5} & {v!s:<5} = {u&v!s:<5} {u!s:>5} and {v!s:<5} = {u and v !s:<5}\")"
" .format(u=u, v=v, r1=(u&v), r2=(u and v)))"
] ]
}, },
{ {
@ -2444,7 +2442,7 @@
"display(p3.show('.1'))\n", "display(p3.show('.1'))\n",
"pairs = p3.get_product_states()\n", "pairs = p3.get_product_states()\n",
"for s in range(p3.num_states()):\n", "for s in range(p3.num_states()):\n",
" print(\"{}: {}\".format(s, pairs[s]))" " print(f\"{s}: {pairs[s]}\")"
] ]
}, },
{ {
@ -2465,7 +2463,7 @@
"name": "stdout", "name": "stdout",
"output_type": "stream", "output_type": "stream",
"text": [ "text": [
"87.6 µs ± 982 ns per loop (mean ± std. dev. of 7 runs, 10,000 loops each)\n" "107 µs ± 2.91 µs per loop (mean ± std. dev. of 7 runs, 10,000 loops each)\n"
] ]
} }
], ],
@ -2482,7 +2480,7 @@
"name": "stdout", "name": "stdout",
"output_type": "stream", "output_type": "stream",
"text": [ "text": [
"2.14 µs ± 9.61 ns per loop (mean ± std. dev. of 7 runs, 100,000 loops each)\n" "2.23 µs ± 47.3 ns per loop (mean ± std. dev. of 7 runs, 100,000 loops each)\n"
] ]
} }
], ],
@ -2525,7 +2523,7 @@
"name": "python", "name": "python",
"nbconvert_exporter": "python", "nbconvert_exporter": "python",
"pygments_lexer": "ipython3", "pygments_lexer": "ipython3",
"version": "3.11.7" "version": "3.11.8"
} }
}, },
"nbformat": 4, "nbformat": 4,

2
tests/python/relabel.py
View file

@ -25,7 +25,7 @@ m = spot.relabeling_map()
g = spot.relabel_bse(f, spot.Pnn, m) g = spot.relabel_bse(f, spot.Pnn, m)
res = "" res = ""
for old, new in m.items(): for old, new in m.items():
res += "#define {} {}\n".format(old, new) res += f"#define {old} {new}\n"
res += str(g) res += str(g)
tc.assertEqual(res, """#define p0 a & b tc.assertEqual(res, """#define p0 a & b
#define p1 c #define p1 c

122
tests/python/satmin.ipynb
View file

@ -450,7 +450,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f61ac1ce910> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe21cd04240> >"
] ]
}, },
"execution_count": 3, "execution_count": 3,
@ -799,7 +799,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f61ac1ce430> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe21e17b0c0> >"
] ]
}, },
"execution_count": 4, "execution_count": 4,
@ -1244,7 +1244,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f61ac1ce940> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe21cd04090> >"
] ]
}, },
"execution_count": 5, "execution_count": 5,
@ -1676,7 +1676,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f61ac1cefa0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe21cd04c00> >"
] ]
}, },
"execution_count": 6, "execution_count": 6,
@ -1938,7 +1938,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f61ac1cee80> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe21cd04cf0> >"
] ]
}, },
"execution_count": 7, "execution_count": 7,
@ -2255,7 +2255,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f61ac1cec40> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe21cd04a50> >"
] ]
}, },
"execution_count": 8, "execution_count": 8,
@ -2546,7 +2546,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f61ac1cebb0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe21cd04870> >"
] ]
}, },
"execution_count": 9, "execution_count": 9,
@ -2618,9 +2618,9 @@
" <td>NaN</td>\n", " <td>NaN</td>\n",
" <td>996</td>\n", " <td>996</td>\n",
" <td>48806</td>\n", " <td>48806</td>\n",
" <td>2</td>\n", " <td>1</td>\n",
" <td>0</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>1</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" </tr>\n", " </tr>\n",
" <tr>\n", " <tr>\n",
@ -2633,7 +2633,7 @@
" <td>2760</td>\n", " <td>2760</td>\n",
" <td>224707</td>\n", " <td>224707</td>\n",
" <td>5</td>\n", " <td>5</td>\n",
" <td>0</td>\n", " <td>1</td>\n",
" <td>5</td>\n", " <td>5</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" </tr>\n", " </tr>\n",
@ -2646,9 +2646,9 @@
" <td>32</td>\n", " <td>32</td>\n",
" <td>2008</td>\n", " <td>2008</td>\n",
" <td>155020</td>\n", " <td>155020</td>\n",
" <td>3</td>\n", " <td>4</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>3</td>\n", " <td>2</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" </tr>\n", " </tr>\n",
" </tbody>\n", " </tbody>\n",
@ -2662,9 +2662,9 @@
"2 5 4 4 11 32 2008 \n", "2 5 4 4 11 32 2008 \n",
"\n", "\n",
" clauses enc.user enc.sys sat.user sat.sys \n", " clauses enc.user enc.sys sat.user sat.sys \n",
"0 48806 2 0 0 0 \n", "0 48806 1 0 1 0 \n",
"1 224707 5 0 5 0 \n", "1 224707 5 1 5 0 \n",
"2 155020 3 0 3 0 " "2 155020 4 0 2 0 "
] ]
}, },
"metadata": {}, "metadata": {},
@ -2937,7 +2937,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f611de5a370> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe208005380> >"
] ]
}, },
"execution_count": 10, "execution_count": 10,
@ -3005,10 +3005,10 @@
" <td>NaN</td>\n", " <td>NaN</td>\n",
" <td>348</td>\n", " <td>348</td>\n",
" <td>15974</td>\n", " <td>15974</td>\n",
" <td>0</td>\n",
" <td>0</td>\n",
" <td>1</td>\n", " <td>1</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>0</td>\n",
" <td>0</td>\n",
" </tr>\n", " </tr>\n",
" <tr>\n", " <tr>\n",
" <th>1</th>\n", " <th>1</th>\n",
@ -3021,7 +3021,7 @@
" <td>73187</td>\n", " <td>73187</td>\n",
" <td>2</td>\n", " <td>2</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>1</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" </tr>\n", " </tr>\n",
" <tr>\n", " <tr>\n",
@ -3049,8 +3049,8 @@
"2 2 4 4 11 32 616 \n", "2 2 4 4 11 32 616 \n",
"\n", "\n",
" clauses enc.user enc.sys sat.user sat.sys \n", " clauses enc.user enc.sys sat.user sat.sys \n",
"0 15974 0 0 1 0 \n", "0 15974 1 0 0 0 \n",
"1 73187 2 0 1 0 \n", "1 73187 2 0 0 0 \n",
"2 37620 1 0 0 0 " "2 37620 1 0 0 0 "
] ]
}, },
@ -3324,7 +3324,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f61ac1cf870> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe21e11bc00> >"
] ]
}, },
"execution_count": 11, "execution_count": 11,
@ -3394,9 +3394,9 @@
" <td>40</td>\n", " <td>40</td>\n",
" <td>2300</td>\n", " <td>2300</td>\n",
" <td>288887</td>\n", " <td>288887</td>\n",
" <td>8</td>\n", " <td>7</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>12</td>\n", " <td>8</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" </tr>\n", " </tr>\n",
" <tr>\n", " <tr>\n",
@ -3438,7 +3438,7 @@
"2 2 1 NaN NaN NaN 92 \n", "2 2 1 NaN NaN NaN 92 \n",
"\n", "\n",
" clauses enc.user enc.sys sat.user sat.sys \n", " clauses enc.user enc.sys sat.user sat.sys \n",
"0 288887 8 0 12 0 \n", "0 288887 7 0 8 0 \n",
"1 18569 1 0 0 0 \n", "1 18569 1 0 0 0 \n",
"2 2337 0 0 0 0 " "2 2337 0 0 0 0 "
] ]
@ -3627,7 +3627,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f61ac1cf960> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe21cd04d80> >"
] ]
}, },
"execution_count": 12, "execution_count": 12,
@ -3695,7 +3695,7 @@
" <td>40</td>\n", " <td>40</td>\n",
" <td>2742</td>\n", " <td>2742</td>\n",
" <td>173183</td>\n", " <td>173183</td>\n",
" <td>4</td>\n", " <td>3</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>2</td>\n", " <td>2</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
@ -3711,7 +3711,7 @@
" <td>45412</td>\n", " <td>45412</td>\n",
" <td>1</td>\n", " <td>1</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>1</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" </tr>\n", " </tr>\n",
" <tr>\n", " <tr>\n",
@ -3723,7 +3723,7 @@
" <td>NaN</td>\n", " <td>NaN</td>\n",
" <td>363</td>\n", " <td>363</td>\n",
" <td>10496</td>\n", " <td>10496</td>\n",
" <td>1</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
@ -3739,9 +3739,9 @@
"2 4 3 NaN NaN NaN 363 \n", "2 4 3 NaN NaN NaN 363 \n",
"\n", "\n",
" clauses enc.user enc.sys sat.user sat.sys \n", " clauses enc.user enc.sys sat.user sat.sys \n",
"0 173183 4 0 2 0 \n", "0 173183 3 0 2 0 \n",
"1 45412 1 0 0 0 \n", "1 45412 1 0 1 0 \n",
"2 10496 1 0 0 0 " "2 10496 0 0 0 0 "
] ]
}, },
"metadata": {}, "metadata": {},
@ -4006,7 +4006,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f611de5b3c0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe21cd04690> >"
] ]
}, },
"execution_count": 13, "execution_count": 13,
@ -4117,7 +4117,7 @@
" <td>173427</td>\n", " <td>173427</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>1</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" </tr>\n", " </tr>\n",
" </tbody>\n", " </tbody>\n",
@ -4133,7 +4133,7 @@
" clauses enc.user enc.sys sat.user sat.sys \n", " clauses enc.user enc.sys sat.user sat.sys \n",
"0 173427 3 0 2 0 \n", "0 173427 3 0 2 0 \n",
"1 173427 0 0 0 0 \n", "1 173427 0 0 0 0 \n",
"2 173427 0 0 1 0 " "2 173427 0 0 0 0 "
] ]
}, },
"metadata": {}, "metadata": {},
@ -4412,7 +4412,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f611de5b600> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe2080067f0> >"
] ]
}, },
"execution_count": 14, "execution_count": 14,
@ -4484,7 +4484,7 @@
" <td>173183</td>\n", " <td>173183</td>\n",
" <td>4</td>\n", " <td>4</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>2</td>\n", " <td>1</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" </tr>\n", " </tr>\n",
" <tr>\n", " <tr>\n",
@ -4498,7 +4498,7 @@
" <td>173279</td>\n", " <td>173279</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>1</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" </tr>\n", " </tr>\n",
" <tr>\n", " <tr>\n",
@ -4526,8 +4526,8 @@
"2 4 3 NaN NaN NaN 2742 \n", "2 4 3 NaN NaN NaN 2742 \n",
"\n", "\n",
" clauses enc.user enc.sys sat.user sat.sys \n", " clauses enc.user enc.sys sat.user sat.sys \n",
"0 173183 4 0 2 0 \n", "0 173183 4 0 1 0 \n",
"1 173279 0 0 0 0 \n", "1 173279 0 0 1 0 \n",
"2 173327 0 0 0 0 " "2 173327 0 0 0 0 "
] ]
}, },
@ -4807,7 +4807,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f611de5bd50> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe208006c10> >"
] ]
}, },
"execution_count": 15, "execution_count": 15,
@ -5108,7 +5108,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f611de5b6f0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe208006940> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -5159,7 +5159,7 @@
" <td>40</td>\n", " <td>40</td>\n",
" <td>2742</td>\n", " <td>2742</td>\n",
" <td>173183</td>\n", " <td>173183</td>\n",
" <td>4</td>\n", " <td>3</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>2</td>\n", " <td>2</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
@ -5176,7 +5176,7 @@
" <td>173279</td>\n", " <td>173279</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>1</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>HOA: v1 States: 4 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...</td>\n", " <td>HOA: v1 States: 4 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...</td>\n",
" </tr>\n", " </tr>\n",
@ -5206,8 +5206,8 @@
"2 4 3 NaN NaN NaN 2742 \n", "2 4 3 NaN NaN NaN 2742 \n",
"\n", "\n",
" clauses enc.user enc.sys sat.user sat.sys \\\n", " clauses enc.user enc.sys sat.user sat.sys \\\n",
"0 173183 4 0 2 0 \n", "0 173183 3 0 2 0 \n",
"1 173279 0 0 0 0 \n", "1 173279 0 0 1 0 \n",
"2 173327 0 0 0 0 \n", "2 173327 0 0 0 0 \n",
"\n", "\n",
" automaton \n", " automaton \n",
@ -5544,7 +5544,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f611de94660> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe208007030> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -5830,7 +5830,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f611de946f0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe208006fa0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -5840,7 +5840,7 @@
"source": [ "source": [
"for line, data in log.iterrows():\n", "for line, data in log.iterrows():\n",
" if type(data.automaton) is str:\n", " if type(data.automaton) is str:\n",
" print(\"automaton from line {}:\".format(line))\n", " print(f\"automaton from line {line}:\")\n",
" display(spot.automaton(data.automaton + \"\\n\"))" " display(spot.automaton(data.automaton + \"\\n\"))"
] ]
}, },
@ -6261,7 +6261,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f61ac1cefa0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe21cd04c00> >"
] ]
}, },
"execution_count": 18, "execution_count": 18,
@ -6329,7 +6329,7 @@
" <td>NaN</td>\n", " <td>NaN</td>\n",
" <td>687</td>\n", " <td>687</td>\n",
" <td>21896</td>\n", " <td>21896</td>\n",
" <td>1</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
@ -6343,9 +6343,9 @@
" <td>32</td>\n", " <td>32</td>\n",
" <td>1905</td>\n", " <td>1905</td>\n",
" <td>100457</td>\n", " <td>100457</td>\n",
" <td>2</td>\n", " <td>3</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>2</td>\n", " <td>1</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" </tr>\n", " </tr>\n",
" </tbody>\n", " </tbody>\n",
@ -6358,8 +6358,8 @@
"1 6 5 4 12 32 1905 \n", "1 6 5 4 12 32 1905 \n",
"\n", "\n",
" clauses enc.user enc.sys sat.user sat.sys \n", " clauses enc.user enc.sys sat.user sat.sys \n",
"0 21896 1 0 0 0 \n", "0 21896 0 0 0 0 \n",
"1 100457 2 0 2 0 " "1 100457 3 0 1 0 "
] ]
}, },
"metadata": {}, "metadata": {},
@ -6638,7 +6638,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f61ac1cf6c0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe21cd051d0> >"
] ]
}, },
"execution_count": 19, "execution_count": 19,
@ -6730,7 +6730,7 @@
" <td>10496</td>\n", " <td>10496</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" <td>0</td>\n", " <td>1</td>\n",
" <td>0</td>\n", " <td>0</td>\n",
" </tr>\n", " </tr>\n",
" </tbody>\n", " </tbody>\n",
@ -6746,7 +6746,7 @@
" clauses enc.user enc.sys sat.user sat.sys \n", " clauses enc.user enc.sys sat.user sat.sys \n",
"0 51612 1 0 1 0 \n", "0 51612 1 0 1 0 \n",
"1 3129 0 0 0 0 \n", "1 3129 0 0 0 0 \n",
"2 10496 0 0 0 0 " "2 10496 0 0 1 0 "
] ]
}, },
"metadata": {}, "metadata": {},
@ -7025,7 +7025,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f611de5b960> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe208006fa0> >"
] ]
}, },
"execution_count": 20, "execution_count": 20,
@ -7581,7 +7581,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f611de5b570> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe2080074e0> >"
] ]
}, },
"execution_count": 21, "execution_count": 21,
@ -7610,7 +7610,7 @@
"name": "python", "name": "python",
"nbconvert_exporter": "python", "nbconvert_exporter": "python",
"pygments_lexer": "ipython3", "pygments_lexer": "ipython3",
"version": "3.11.7" "version": "3.11.8"
} }
}, },
"nbformat": 4, "nbformat": 4,

30
tests/python/stutter-inv.ipynb
View file

@ -215,7 +215,7 @@
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
"You have to be aware of this property being set in your back because if while playing with `is_stutter_invariant()` you the incorrect formula for an automaton by mistake, the automaton will have its property set incorrectly, and running `is_stutter_invariant()` with the correct formula will simply return the cached property.\n", "You have to be aware of this property being set in your back. If, after calling `is_stutter_invariant()`, you modify the automaton (e.g., adding edges, or changing labels), the modified automaton might then have its property set incorrectly, and running `is_stutter_invariant()` will not recompute a property that is set.\n",
"\n", "\n",
"In doubt, you can always reset the property as follows:" "In doubt, you can always reset the property as follows:"
] ]
@ -351,7 +351,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f47047afc00> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2110141680> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -418,9 +418,9 @@
" acc, rej, aut = \"rejected\", \"accepted\", pos\n", " acc, rej, aut = \"rejected\", \"accepted\", pos\n",
" word2 = spot.sl2(waut).intersecting_word(aut)\n", " word2 = spot.sl2(waut).intersecting_word(aut)\n",
" word2.simplify()\n", " word2.simplify()\n",
" print(\"\"\"{} is {} by {}\n", " print(f\"\"\"{word} is {acc} by {f}\n",
" but if we stutter some of its letters, we get\n", " but if we stutter some of its letters, we get\n",
"{} which is {} by {}\"\"\".format(word, acc, f, word2, rej, f))" "{word2} which is {rej} by {f}\"\"\")"
] ]
}, },
{ {
@ -804,7 +804,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f47047d0bd0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2110143b70> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1165,7 +1165,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f47047d0bd0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2110143b70> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1389,7 +1389,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f47047d1590> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2110143d20> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1576,7 +1576,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f47047d0ab0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2110142b50> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1962,7 +1962,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f47047d2640> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2110142340> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -2183,7 +2183,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f47047d1d10> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2110142580> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -2392,7 +2392,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f47047d2370> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f21101417a0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -2434,7 +2434,7 @@
"source": [ "source": [
"sil_vec = spot.stutter_invariant_letters(pos, f)\n", "sil_vec = spot.stutter_invariant_letters(pos, f)\n",
"for q in range(pos.num_states()):\n", "for q in range(pos.num_states()):\n",
" print(\"sil_vec[{}] =\".format(q), spot.bdd_format_formula(pos.get_dict(), sil_vec[q]))" " print(f\"sil_vec[{q}] =\", spot.bdd_format_formula(pos.get_dict(), sil_vec[q]))"
] ]
}, },
{ {
@ -2848,7 +2848,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f47047d13e0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2110142430> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -3408,7 +3408,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f47047d13e0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2110142430> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -3649,7 +3649,7 @@
"name": "python", "name": "python",
"nbconvert_exporter": "python", "nbconvert_exporter": "python",
"pygments_lexer": "ipython3", "pygments_lexer": "ipython3",
"version": "3.11.7" "version": "3.11.8"
} }
}, },
"nbformat": 4, "nbformat": 4,

37
tests/python/twagraph-internals.ipynb
View file

@ -252,7 +252,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b477e340> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1fdcf63db0> >"
] ]
}, },
"execution_count": 3, "execution_count": 3,
@ -784,7 +784,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b477e340> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1fdcf63db0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1043,7 +1043,8 @@
], ],
"source": [ "source": [
"for ed in aut.out(0):\n", "for ed in aut.out(0):\n",
" print(\"edges[{e}].src={src}, edges[{e}].dst={dst}\".format(e=aut.edge_number(ed), src=ed.src, dst=ed.dst))" " en = aut.edge_number(ed)\n",
" print(f\"edges[{en}].src={ed.src}, edges[{en}].dst={ed.dst}\")"
] ]
}, },
{ {
@ -1293,7 +1294,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b477e340> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1fdcf63db0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1759,7 +1760,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b477e340> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1fdcf63db0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -1979,7 +1980,7 @@
"cell_type": "markdown", "cell_type": "markdown",
"metadata": {}, "metadata": {},
"source": [ "source": [
"Note that the `succ_tail` field of the `states` vector is seldom used when reading automata as the linked list of edges ends when `next_succ` (or `succ`) equals `0`. Its main use is during calls to `new_edge()`: new edges are always created at the end of the list (otherwise it would be hard to preserve the order of edges when parsing and automaton and printing it)." "Note that the `succ_tail` field of the `states` vector is seldom used when reading automata as the linked list of edges ends when `next_succ` (or `succ`) equals `0`. Its main use is during calls to `new_edge()`: new edges are always created at the end of the list (otherwise it would be hard to preserve the order of edges when parsing an automaton and printing it)."
] ]
}, },
{ {
@ -2233,7 +2234,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b477e340> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1fdcf63db0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -2604,7 +2605,7 @@
"while it:\n", "while it:\n",
" e = it.current()\n", " e = it.current()\n",
" toerase = e.acc.has(1)\n", " toerase = e.acc.has(1)\n",
" print(\"pos={}, acc={}, toerase={}\".format(aut.edge_number(e), e.acc, toerase))\n", " print(f\"pos={aut.edge_number(e)}, acc={e.acc}, toerase={toerase}\")\n",
" if toerase:\n", " if toerase:\n",
" it.erase()\n", " it.erase()\n",
" else:\n", " else:\n",
@ -2900,7 +2901,8 @@
], ],
"source": [ "source": [
"for e in aut.edges(): # iterate over all non-erased edges\n", "for e in aut.edges(): # iterate over all non-erased edges\n",
" print(\"edges[{e}].src={src}, edges[{e}].dst={dst}\".format(e=aut.edge_number(e), src=e.src, dst=e.dst))" " en = aut.edge_number(e)\n",
" print(f\"edges[{en}].src={e.src}, edges[{en}].dst={e.dst}\")"
] ]
}, },
{ {
@ -3398,7 +3400,8 @@
], ],
"source": [ "source": [
"for e in aut.edges(): # iterate over all non-erased edges\n", "for e in aut.edges(): # iterate over all non-erased edges\n",
" print(\"edges[{e}].src={src}, edges[{e}].dst={dst}\".format(e=aut.edge_number(e), src=e.src, dst=e.dst))" " en = aut.edge_number(e)\n",
" print(f\"edges[{en}].src={e.src}, edges[{en}].dst={e.dst}\")"
] ]
}, },
{ {
@ -3954,7 +3957,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b477e340> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1fdcf63db0> >"
] ]
}, },
"execution_count": 22, "execution_count": 22,
@ -4768,7 +4771,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b477e340> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1fdcf63db0> >"
] ]
}, },
"execution_count": 28, "execution_count": 28,
@ -5552,7 +5555,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b477e340> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1fdcf63db0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -6260,7 +6263,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b477e340> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1fdcf63db0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -6758,7 +6761,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b4794630> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1fdd05b7e0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -7129,7 +7132,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd9b4794630> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f1fdd05b7e0> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -7345,7 +7348,7 @@
"name": "python", "name": "python",
"nbconvert_exporter": "python", "nbconvert_exporter": "python",
"pygments_lexer": "ipython3", "pygments_lexer": "ipython3",
"version": "3.11.7" "version": "3.11.8"
} }
}, },
"nbformat": 4, "nbformat": 4,

72
tests/python/zlktree.ipynb
View file

@ -387,7 +387,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f92f048a010> >" "<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f2d01ddfe70> >"
] ]
}, },
"execution_count": 2, "execution_count": 2,
@ -985,7 +985,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f048b0c0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d01decab0> >"
] ]
}, },
"execution_count": 10, "execution_count": 10,
@ -994,7 +994,7 @@
} }
], ],
"source": [ "source": [
"a1 = spot.automaton(\"randaut -Q4 --colored -e.7 -A '{}' 2 |\".format(c.get_acceptance()))\n", "a1 = spot.automaton(f\"randaut -Q4 --colored -e.7 -A '{c.get_acceptance()}' 2 |\")\n",
"a1" "a1"
] ]
}, },
@ -1809,7 +1809,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f048b510> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d01decd50> >"
] ]
}, },
"execution_count": 11, "execution_count": 11,
@ -2131,7 +2131,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f048b540> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d01ded4d0> >"
] ]
}, },
"execution_count": 13, "execution_count": 13,
@ -2140,7 +2140,7 @@
} }
], ],
"source": [ "source": [
"a2 = spot.automaton(\"randaut -Q3 -e.8 --seed=4 -A '{}' 2 |\".format(c.get_acceptance()))\n", "a2 = spot.automaton(f\"randaut -Q3 -e.8 --seed=4 -A '{c.get_acceptance()}' 2 |\")\n",
"a2" "a2"
] ]
}, },
@ -2999,7 +2999,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f04a4660> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d01dedc50> >"
] ]
}, },
"execution_count": 14, "execution_count": 14,
@ -3709,7 +3709,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f92f04a6460> >" "<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f2d01defb10> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -4355,7 +4355,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f92f04a6490> >" "<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f2d01defb40> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -4511,7 +4511,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f92f04a5ad0> >" "<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f2d01def180> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -4717,7 +4717,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f92f04a6460> >" "<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f2d01defb10> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -4777,7 +4777,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f92f04a6490> >" "<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f2d01defb40> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -4837,7 +4837,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f92f04a5ad0> >" "<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f2d01def180> >"
] ]
}, },
"metadata": {}, "metadata": {},
@ -5222,7 +5222,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f92f04a62b0> >" "<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f2d01deff30> >"
] ]
}, },
"execution_count": 18, "execution_count": 18,
@ -6510,7 +6510,7 @@
"</script>" "</script>"
], ],
"text/plain": [ "text/plain": [
"<spot.acd; proxy of <Swig Object of type 'spot::acd *' at 0x7f92f04a6730> >" "<spot.acd; proxy of <Swig Object of type 'spot::acd *' at 0x7f2d01deefa0> >"
] ]
}, },
"execution_count": 20, "execution_count": 20,
@ -7984,7 +7984,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f04a6d30> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d005206c0> >"
] ]
}, },
"execution_count": 29, "execution_count": 29,
@ -9202,7 +9202,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f04a6fa0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d005207b0> >"
] ]
}, },
"execution_count": 31, "execution_count": 31,
@ -10624,7 +10624,7 @@
"</script>" "</script>"
], ],
"text/plain": [ "text/plain": [
"<spot.acd; proxy of <Swig Object of type 'spot::acd *' at 0x7f92f04a7c60> >" "<spot.acd; proxy of <Swig Object of type 'spot::acd *' at 0x7f2d00520b40> >"
] ]
}, },
"execution_count": 40, "execution_count": 40,
@ -12328,7 +12328,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f0104390> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d00521bc0> >"
] ]
}, },
"execution_count": 45, "execution_count": 45,
@ -12687,7 +12687,7 @@
"</script>" "</script>"
], ],
"text/plain": [ "text/plain": [
"<spot.acd; proxy of <Swig Object of type 'spot::acd *' at 0x7f92f0104510> >" "<spot.acd; proxy of <Swig Object of type 'spot::acd *' at 0x7f2d00522160> >"
] ]
}, },
"execution_count": 47, "execution_count": 47,
@ -13081,7 +13081,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f0104450> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d005214d0> >"
] ]
}, },
"execution_count": 48, "execution_count": 48,
@ -13418,7 +13418,7 @@
"</script>" "</script>"
], ],
"text/plain": [ "text/plain": [
"<spot.acd; proxy of <Swig Object of type 'spot::acd *' at 0x7f92f01040f0> >" "<spot.acd; proxy of <Swig Object of type 'spot::acd *' at 0x7f2d00521e60> >"
] ]
}, },
"execution_count": 49, "execution_count": 49,
@ -13765,7 +13765,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f0104e40> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d00522310> >"
] ]
}, },
"execution_count": 50, "execution_count": 50,
@ -14036,7 +14036,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f0104960> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d00522970> >"
] ]
}, },
"execution_count": 51, "execution_count": 51,
@ -14219,7 +14219,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f92f01050e0> >" "<spot.zielonka_tree; proxy of <Swig Object of type 'spot::zielonka_tree *' at 0x7f2d00522c40> >"
] ]
}, },
"execution_count": 52, "execution_count": 52,
@ -14530,7 +14530,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f0104ab0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d00522ac0> >"
] ]
}, },
"execution_count": 53, "execution_count": 53,
@ -14850,7 +14850,7 @@
"</script>" "</script>"
], ],
"text/plain": [ "text/plain": [
"<spot.acd; proxy of <Swig Object of type 'spot::acd *' at 0x7f92f0105500> >" "<spot.acd; proxy of <Swig Object of type 'spot::acd *' at 0x7f2d00522760> >"
] ]
}, },
"execution_count": 55, "execution_count": 55,
@ -15094,7 +15094,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f0105710> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d00523150> >"
] ]
}, },
"execution_count": 57, "execution_count": 57,
@ -15367,7 +15367,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f0104d20> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d00523240> >"
] ]
}, },
"execution_count": 58, "execution_count": 58,
@ -15738,7 +15738,7 @@
"</script>" "</script>"
], ],
"text/plain": [ "text/plain": [
"<spot.acd; proxy of <Swig Object of type 'spot::acd *' at 0x7f92f01058c0> >" "<spot.acd; proxy of <Swig Object of type 'spot::acd *' at 0x7f2d00523ab0> >"
] ]
}, },
"execution_count": 60, "execution_count": 60,
@ -15966,7 +15966,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f01059e0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d005239c0> >"
] ]
}, },
"execution_count": 61, "execution_count": 61,
@ -16205,7 +16205,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f01051d0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d005238a0> >"
] ]
}, },
"execution_count": 62, "execution_count": 62,
@ -16744,7 +16744,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f01053b0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d00523720> >"
] ]
}, },
"execution_count": 63, "execution_count": 63,
@ -16901,7 +16901,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f0106430> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d00523fc0> >"
] ]
}, },
"execution_count": 64, "execution_count": 64,
@ -17068,7 +17068,7 @@
"</svg>\n" "</svg>\n"
], ],
"text/plain": [ "text/plain": [
"<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f92f01051a0> >" "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f2d00550090> >"
] ]
}, },
"execution_count": 66, "execution_count": 66,
@ -17126,7 +17126,7 @@
"name": "python", "name": "python",
"nbconvert_exporter": "python", "nbconvert_exporter": "python",
"pygments_lexer": "ipython3", "pygments_lexer": "ipython3",
"version": "3.11.7" "version": "3.11.8"
} }
}, },
"nbformat": 4, "nbformat": 4,