diff --git a/doc/org/tut01.org b/doc/org/tut01.org index 9d446e3cc..6693cf9a8 100644 --- a/doc/org/tut01.org +++ b/doc/org/tut01.org @@ -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 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 import spot diff --git a/doc/org/tut02.org b/doc/org/tut02.org index 5d63b35c9..ec703a2b2 100644 --- a/doc/org/tut02.org +++ b/doc/org/tut02.org @@ -68,8 +68,8 @@ import spot m = spot.relabeling_map() g = spot.relabel('"Proc@Here" U ("var > 10" | "var < 4")', spot.Pnn, m) for newname, oldname in m.items(): - print("#define {} ({})".format(newname.to_str(), oldname.to_str('spin', True))) - print(g.to_str('spin', True)) + print(f"#define {newname.to_str()} ({oldname.to_str('spin', True)})") +print(g.to_str('spin', True)) #+END_SRC #+RESULTS: diff --git a/doc/org/tut03.org b/doc/org/tut03.org index 40b59d82b..a266e765b 100644 --- a/doc/org/tut03.org +++ b/doc/org/tut03.org @@ -159,9 +159,9 @@ The Python equivalent is similar: # kindstr() prints the name of the operator # 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 - 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 for child in f: print(" *", child) diff --git a/doc/org/tut21.org b/doc/org/tut21.org index 677736aea..358577db9 100644 --- a/doc/org/tut21.org +++ b/doc/org/tut21.org @@ -557,9 +557,9 @@ Here is the very same example, but written in Python: print("Stutter Invariant:", aut.prop_stutter_invariant()) for s in range(0, aut.num_states()): - print("State {}:".format(s)) + print(f"State {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 # is inconvenient to use in Python. Instead we use # bdd_format_formula() as this simply returns a string. diff --git a/doc/org/tut24.org b/doc/org/tut24.org index fd561eec8..e2d947531 100644 --- a/doc/org/tut24.org +++ b/doc/org/tut24.org @@ -190,26 +190,26 @@ decide whether to enclose the destinations in braces. Here is the Python version of this code: #+BEGIN_SRC python - import spot + import spot - aut = spot.automaton("tut24.hoa") - bdict = aut.get_dict() - init = aut.get_init_state_number() - ui = aut.is_univ_dest(init) - print("Initial states: {}{}{}".format("{ " if ui else "", - " ".join(map(str, aut.univ_dests(init))), - " }" if ui else "")) - for s in range(0, aut.num_states()): - print("State {}:".format(s)) - for t in aut.out(s): - ud = aut.is_univ_dest(t) - print(" edge({} -> {}{}{})".format(t.src, - "{ " if ud else "", - " ".join(map(str, aut.univ_dests(t))), - " }" if ud else "")) - print(" label =", spot.bdd_format_formula(bdict, t.cond)) - print(" acc sets =", t.acc) + aut = spot.automaton("tut24.hoa") + + def format_dest(s): + if not aut.is_univ_dest(s): + return s + else: + return f'{{ {" ".join(map(str, aut.univ_dests(s)))} }}' + + bdict = aut.get_dict() + init = aut.get_init_state_number() + print(f"Initial states: {format_dest(init)}") + for s in range(0, aut.num_states()): + print("State {}:".format(s)) + for t in aut.out(s): + print(f" edge({t.src} -> {format_dest(t.dst)})") + print(" label =", spot.bdd_format_formula(bdict, t.cond)) + print(" acc sets =", t.acc) #+END_SRC #+RESULTS: diff --git a/doc/org/tut90.org b/doc/org/tut90.org index c352c356d..ea3657e6e 100644 --- a/doc/org/tut90.org +++ b/doc/org/tut90.org @@ -108,12 +108,12 @@ import spot aut1 = spot.make_twa_graph() ap1a = aut1.register_ap("a") ap1b = aut1.register_ap("b") -print("aut1: a={} b={}".format(ap1a, ap1b)) +print(f"aut1: a={ap1a} b={ap1b}") aut2 = spot.make_twa_graph() ap2c = aut2.register_ap("c") ap2b = aut2.register_ap("b") 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 #+RESULTS: @@ -271,7 +271,7 @@ all transition that belong to a certain acceptance set. self.set.add((src, guard, dst)) def str_trans(self, src, guard, dst): f = spot.bdd_format_formula(self.dict, guard) - return "({},{},{})".format(src, f, dst) + return f"({src},{f},{dst})" def __str__(self): 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)) def str_trans(self, src, guard, dest): f = spot.bdd_format_formula(self.dict, guard) - return "({},{},{})".format(src, f, dest) + return f"({src},{f},{dest})" def __str__(self): return '{' + ",".join([ self.str_trans(*t) for t in self.set ]) + '}' diff --git a/python/spot/__init__.py b/python/spot/__init__.py index b784fdbdf..3d3393797 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -512,7 +512,7 @@ class acd: .acdrej polygon{fill:red;} .acdacc polygon{fill:green;} ''' - js = ''' + js = f''' function acdremclasses(sel, classes) {{ document.querySelectorAll(sel).forEach(n=>{{n.classList.remove(...classes)}});}} function acdaddclasses(sel, classes) {{ @@ -545,30 +545,26 @@ function acd{num}_node(node, acc){{ acdaddclasses("#acdaut{num} .acdN" + node, [acc ? "acdacc" : "acdrej", "acdbold"]); acdaddclasses("#acd{num} #N" + node, ["acdbold", "acdhigh"]); -}};'''.format(num=num) +}};''' me = 0 for n in range(self.node_count()): for e in self.edges_of_node(n): me = max(e, me) - js += 'acdaddclasses("#acdaut{num} #E{e}", ["acdN{n}"]);\n'\ - .format(num=num, e=e, n=n) + js += f'acdaddclasses("#acdaut{num} #E{e}", ["acdN{n}"]);\n' for e in range(1, me + 1): - js += 'acdonclick("#acdaut{num} #E{e}",'\ - 'function(){{acd{num}_edge({e});}});\n'\ - .format(num=num, e=e) + js += f'acdonclick("#acdaut{num} #E{e}",'\ + f'function(){{acd{num}_edge({e});}});\n' for s in range(self.get_aut().num_states()): - js += 'acdonclick("#acdaut{num} #S{s}",'\ - 'function(){{acd{num}_state({s});}});\n'\ - .format(num=num, s=s) + js += f'acdonclick("#acdaut{num} #S{s}",'\ + f'function(){{acd{num}_state({s});}});\n' for n in range(self.node_count()): v = int(self.node_acceptance(n)) - js += 'acdonclick("#acd{num} #N{n}",'\ - 'function(){{acd{num}_node({n}, {v});}});\n'\ - .format(num=num, n=n, v=v) + js += f'acdonclick("#acd{num} #N{n}",'\ + f'function(){{acd{num}_node({n}, {v});}});\n' html = '
{}
{}
'\ .format(style, - self.get_aut().show('.i(acdaut{})'.format(num)).data, - self._repr_svg_("acd{}".format(num)), + self.get_aut().show(f'.i(acdaut{num})').data, + self._repr_svg_(f"acd{num}"), js); return html @@ -746,7 +742,7 @@ def automaton(filename, **kwargs): try: return next(automata(filename, **kwargs)) 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): """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)) except StopIteration: raise RuntimeError("Failed to read an aiger circuit " - "from {}".format(source)) + f"from {source}") def _postproc_translate_options(obj, default_type, *args): @@ -795,8 +791,7 @@ def _postproc_translate_options(obj, default_type, *args): def type_set(val): nonlocal type_, type_name_ if type_ is not None and type_name_ != val: - raise ValueError("type cannot be both {} and {}" - .format(type_name_, val)) + raise ValueError(f"type cannot be both {type_name_} and {val}") elif val == 'generic' or val == 'gen' or val == 'g': type_ = postprocessor.Generic elif val == 'tgba': # historical @@ -839,8 +834,8 @@ def _postproc_translate_options(obj, default_type, *args): def pref_set(val): nonlocal pref_, pref_name_ if pref_ is not None and pref_name_ != val: - raise ValueError("preference cannot be both {} and {}" - .format(pref_name_, val)) + raise ValueError("preference cannot be both "\ + f"{pref_name_} and {val}") elif val == 'small': pref_ = postprocessor.Small elif val == 'deterministic': @@ -853,8 +848,8 @@ def _postproc_translate_options(obj, default_type, *args): def optm_set(val): nonlocal optm_, optm_name_ if optm_ is not None and optm_name_ != val: - raise ValueError("optimization level cannot be both {} and {}" - .format(optm_name_, val)) + raise ValueError("optimization level cannot be both "\ + f"{optm_name_} and {val}") if val == 'high': optm_ = postprocessor.High elif val.startswith('med'): @@ -930,10 +925,10 @@ def _postproc_translate_options(obj, default_type, *args): if lc == 1: f(compat[0]) elif lc < 1: - raise ValueError("unknown option '{}'".format(arg)) + raise ValueError(f"unknown option '{arg}'") else: - raise ValueError("ambiguous option '{}' is prefix of {}" - .format(arg, str(compat))) + raise ValueError(f"ambiguous option '{arg}' "\ + f"is prefix of {str(compat)}") if type_ is None: type_ = default_type @@ -1307,7 +1302,7 @@ def sat_minimize(aut, acc=None, colored=False, if display_log or return_log: import pandas as pd with tempfile.NamedTemporaryFile(dir='.', suffix='.satlog') as t: - args += ',log="{}"'.format(t.name) + args += f',log="{t.name}"' aut = sm(aut, args, state_based) dfrm = pd.read_csv(t.name, dtype=object) if display_log: @@ -1397,10 +1392,10 @@ def mp_hierarchy_svg(cl=None): 'B': '110,198', } if cl in coords: - highlight = ''' + highlight = f''' - '''.format(coords[cl]) + ''' else: highlight = '' return ''' diff --git a/python/spot/jupyter.py b/python/spot/jupyter.py index 0bfea81a0..97d383b1b 100644 --- a/python/spot/jupyter.py +++ b/python/spot/jupyter.py @@ -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 displayed on each row, each one taking 1/per_row of the line width. """ - width = res = '' + w = res = '' if per_row: - width = 'width:{}%;'.format(100//per_row) + w = f'width:{100//per_row}%;' for arg in args: - dpy = 'inline-block' + dpy = 'display:inline-block' if show is not None and hasattr(arg, 'show'): arg = arg.show(show) if hasattr(arg, '_repr_html_'): @@ -65,9 +65,8 @@ def display_inline(*args, per_row=None, show=None): elif hasattr(arg, '_repr_latex_'): rep = arg._repr_latex_() if not per_row: - dpy = 'inline' + dpy = 'display:inline' else: rep = str(arg) - res += ("
{}
" - .format(dpy, width, rep)) + res += f"
{rep}
" display(HTML(res)) diff --git a/tests/python/acc.py b/tests/python/acc.py index b215428b1..1374bab8a 100644 --- a/tests/python/acc.py +++ b/tests/python/acc.py @@ -22,7 +22,7 @@ tc = TestCase() a = spot.acc_cond('parity min odd 5') 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') tc.assertEqual(str(a.fin_unit_one_split()), diff --git a/tests/python/acc_cond.ipynb b/tests/python/acc_cond.ipynb index f2773938b..d3b6ddffd 100644 --- a/tests/python/acc_cond.ipynb +++ b/tests/python/acc_cond.ipynb @@ -11,7 +11,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -100,7 +99,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -131,7 +129,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -194,7 +191,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -220,7 +216,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -252,7 +247,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -280,7 +274,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -331,7 +324,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -359,7 +351,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -400,7 +391,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -428,7 +418,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -455,7 +444,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -483,7 +471,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -552,7 +539,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -603,7 +589,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -630,7 +615,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -743,7 +727,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -775,11 +758,10 @@ "acc = spot.acc_code('Fin(0) & Inf(1) | Inf(2)')\n", "print(\"acc =\", acc)\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", "metadata": {}, "source": [ @@ -809,7 +791,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -837,7 +818,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -873,7 +853,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -909,7 +888,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -978,7 +956,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1049,7 +1026,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1078,7 +1054,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1108,7 +1083,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1138,7 +1112,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1170,7 +1143,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1202,7 +1174,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1235,7 +1206,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1264,7 +1234,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1292,7 +1261,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1320,7 +1288,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1346,11 +1313,10 @@ "source": [ "print(\"acc =\", acc)\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", "metadata": {}, "source": [ @@ -1419,7 +1385,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1446,7 +1411,6 @@ ] }, { - "attachments": {}, "cell_type": "markdown", "metadata": {}, "source": [ @@ -1566,7 +1530,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.10.5" + "version": "3.11.8" } }, "nbformat": 4, diff --git a/tests/python/complement_semidet.py b/tests/python/complement_semidet.py index 1aa3bcf5d..1027985e2 100644 --- a/tests/python/complement_semidet.py +++ b/tests/python/complement_semidet.py @@ -31,8 +31,7 @@ n = 10000 for aut in spot.automata( "randltl -n-1 a b " "| ltl2tgba " - "| autfilt --is-semi-deterministic --acceptance-is=Buchi -n{} |" - .format(n)): + f"| autfilt --is-semi-deterministic --acceptance-is=Buchi -n{n} |"): comp = complement(aut) semidet_comp = spot.complement_semidet(aut, True) diff --git a/tests/python/decompose.ipynb b/tests/python/decompose.ipynb index 9d1728f21..f1943ecee 100644 --- a/tests/python/decompose.ipynb +++ b/tests/python/decompose.ipynb @@ -359,7 +359,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c1623d0> >" + " *' at 0x7faaf7cffd80> >" ] }, "execution_count": 2, @@ -583,7 +583,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c162340> >" + " *' at 0x7faaf7d10240> >" ] }, "execution_count": 3, @@ -874,7 +874,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c161fe0> >" + " *' at 0x7faaf7d103f0> >" ] }, "execution_count": 4, @@ -1043,7 +1043,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c162070> >" + " *' at 0x7faaf7d10600> >" ] }, "execution_count": 5, @@ -1175,7 +1175,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c162eb0> >" + " *' at 0x7faaf7d10a80> >" ] }, "execution_count": 6, @@ -1400,7 +1400,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c163390> >" + " *' at 0x7faaf7d110e0> >" ] }, "metadata": {}, @@ -1681,7 +1681,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c163360> >" + " *' at 0x7faaf7cffde0> >" ] }, "metadata": {}, @@ -2008,7 +2008,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c163390> >" + " *' at 0x7faaf7cfff60> >" ] }, "metadata": {}, @@ -2775,7 +2775,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c162b50> >" + " *' at 0x7faaf7d115f0> >" ] }, "execution_count": 8, @@ -3509,7 +3509,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c162c70> >" + " *' at 0x7faaf7d10c00> >" ] }, "metadata": {}, @@ -3964,7 +3964,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c163390> >" + " *' at 0x7faaf7cfff60> >" ] }, "metadata": {}, @@ -4375,7 +4375,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c162c70> >" + " *' at 0x7faaf7d10c00> >" ] }, "metadata": {}, @@ -5120,7 +5120,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c163c00> >" + " *' at 0x7faaf7d10a20> >" ] }, "execution_count": 10, @@ -5415,7 +5415,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c163b40> >" + " *' at 0x7faaf7d10b40> >" ] }, "metadata": {}, @@ -5684,7 +5684,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c163a80> >" + " *' at 0x7faaf7d119e0> >" ] }, "metadata": {}, @@ -5965,7 +5965,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c163e10> >" + " *' at 0x7faaf7d114d0> >" ] }, "metadata": {}, @@ -6637,7 +6637,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c163150> >" + " *' at 0x7faaf7d11c20> >" ] }, "execution_count": 12, @@ -7293,7 +7293,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c162c10> >" + " *' at 0x7faaf7d12460> >" ] }, "metadata": {}, @@ -7638,7 +7638,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c163e10> >" + " *' at 0x7faaf7d114d0> >" ] }, "metadata": {}, @@ -7945,7 +7945,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c162c10> >" + " *' at 0x7faaf7d12460> >" ] }, "metadata": {}, @@ -8612,7 +8612,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c163240> >" + " *' at 0x7faaf7d12160> >" ] }, "execution_count": 14, @@ -8823,7 +8823,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c163d50> >" + " *' at 0x7faaf7d11c80> >" ] }, "execution_count": 15, @@ -8989,7 +8989,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c17c870> >" + " *' at 0x7faaf7d120d0> >" ] }, "metadata": {}, @@ -9132,7 +9132,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c1634b0> >" + " *' at 0x7faaf7d11290> >" ] }, "metadata": {}, @@ -9293,7 +9293,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c17c540> >" + " *' at 0x7faaf7d11e60> >" ] }, "execution_count": 18, @@ -9557,7 +9557,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c17c570> >" + " *' at 0x7faaf7d10180> >" ] }, "execution_count": 19, @@ -9830,7 +9830,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c17db90> >" + " *' at 0x7faaf7d137b0> >" ] }, "metadata": {}, @@ -10025,7 +10025,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c162c10> >" + " *' at 0x7faaf7d12460> >" ] }, "metadata": {}, @@ -10279,7 +10279,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c1626d0> >" + " *' at 0x7faaf7d137b0> >" ] }, "metadata": {}, @@ -10315,10 +10315,10 @@ "name": "stdout", "output_type": "stream", "text": [ - "SCC #0 contains states [1]\n", - "SCC #1 contains states [4]\n", - "SCC #2 contains states [3]\n", - "SCC #3 contains states [0, 2]\n" + "SCC #0 contains states (1,)\n", + "SCC #1 contains states (4,)\n", + "SCC #2 contains states (3,)\n", + "SCC #3 contains states (0, 2)\n" ] }, { @@ -10642,7 +10642,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c17d410> >" + " *' at 0x7faaf7d124c0> >" ] }, "metadata": {}, @@ -10915,7 +10915,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c17d3e0> >" + " *' at 0x7faaf7d117d0> >" ] }, "execution_count": 21, @@ -10927,7 +10927,7 @@ "aut = spot.translate('(Ga -> Gb) W c')\n", "si = spot.scc_info(aut)\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", "spot.decompose_scc(si, '0,1')" ] @@ -11089,7 +11089,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f328c17e160> >" + " *' at 0x7faaf7d13420> >" ] }, "execution_count": 22, @@ -11100,6 +11100,13 @@ "source": [ "spot.decompose_scc(si, 'a2')" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { @@ -11118,7 +11125,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.7" + "version": "3.11.8" } }, "nbformat": 4, diff --git a/tests/python/formulas.ipynb b/tests/python/formulas.ipynb index f20769a72..47b908c75 100644 --- a/tests/python/formulas.ipynb +++ b/tests/python/formulas.ipynb @@ -189,14 +189,14 @@ ], "source": [ "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", "metadata": {}, "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": [ - "print(\"\"\"\\\n", - "Spin: {0:s}\n", - "Spin+parentheses: {0:sp}\n", - "Spot (default): {0}\n", - "Spot+shell quotes: {0:q}\n", - "LBT, right aligned: {0:l:~>40}\n", - "LBT, no M/W/R: {0:[MWR]l}\"\"\".format(f))" + "print(f\"\"\"\\\n", + "Spin: {f:s}\n", + "Spin+parentheses: {f:sp}\n", + "Spot (default): {f}\n", + "Spot+shell quotes: {f:q}\n", + "LBT, right aligned: {f:l:~>40}\n", + "LBT, no M/W/R: {f:[MWR]l}\"\"\")" ] }, { @@ -1050,7 +1050,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.7" + "version": "3.11.8" } }, "nbformat": 4, diff --git a/tests/python/highlighting.ipynb b/tests/python/highlighting.ipynb index 07145174d..55b7006b2 100644 --- a/tests/python/highlighting.ipynb +++ b/tests/python/highlighting.ipynb @@ -330,7 +330,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4156190> >" + " *' at 0x7fed1691bbd0> >" ] }, "execution_count": 4, @@ -525,7 +525,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4155f80> >" + " *' at 0x7fed16a24420> >" ] }, "execution_count": 5, @@ -718,7 +718,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4156190> >" + " *' at 0x7fed1691bbd0> >" ] }, "execution_count": 6, @@ -830,9 +830,9 @@ ], "source": [ "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", - " print(\"edge {}: {}\".format(i, a.get_highlight_edge(i)))" + " print(f\"edge {i}: {a.get_highlight_edge(i)}\")" ] }, { @@ -1023,7 +1023,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4157900> >" + " *' at 0x7fed16a248a0> >" ] }, "execution_count": 9, @@ -1218,7 +1218,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4157780> >" + " *' at 0x7fed16a25c80> >" ] }, "execution_count": 10, @@ -1517,7 +1517,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f41574b0> >" + " *' at 0x7fed16a25950> >" ] }, "execution_count": 11, @@ -1846,7 +1846,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f41574b0> >" + " *' at 0x7fed16a25950> >" ] }, "execution_count": 14, @@ -2493,7 +2493,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f41745d0> >" + " *' at 0x7fed16a26100> >" ] }, "metadata": {}, @@ -3006,7 +3006,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4156100> >" + " *' at 0x7fed16a252c0> >" ] }, "metadata": {}, @@ -3363,7 +3363,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4157480> >" + " *' at 0x7fed16a25e00> >" ] }, "metadata": {}, @@ -3536,7 +3536,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4174d80> >" + " *' at 0x7fed16a26340> >" ] }, "metadata": {}, @@ -3637,7 +3637,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4174210> >" + " *' at 0x7fed16a26100> >" ] }, "metadata": {}, @@ -3804,7 +3804,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4174f30> >" + " *' at 0x7fed16a25f80> >" ] }, "execution_count": 17, @@ -4006,7 +4006,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4174f30> >" + " *' at 0x7fed16a25f80> >" ] }, "metadata": {}, @@ -4127,7 +4127,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4174d80> >" + " *' at 0x7fed16a26340> >" ] }, "metadata": {}, @@ -4228,7 +4228,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4174210> >" + " *' at 0x7fed16a26100> >" ] }, "metadata": {}, @@ -4635,7 +4635,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4176160> >" + " *' at 0x7fed16a279c0> >" ] }, "metadata": {}, @@ -4796,7 +4796,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4175320> >" + " *' at 0x7fed16a25e90> >" ] }, "metadata": {}, @@ -4981,7 +4981,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4176130> >" + " *' at 0x7fed16a27990> >" ] }, "metadata": {}, @@ -5284,7 +5284,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4175950> >" + " *' at 0x7fed16a27480> >" ] }, "execution_count": 22, @@ -5586,7 +5586,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4175950> >" + " *' at 0x7fed16a27480> >" ] }, "execution_count": 23, @@ -5883,7 +5883,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fa7f4175950> >" + " *' at 0x7fed16a27480> >" ] }, "metadata": {}, @@ -6391,7 +6391,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.7" + "version": "3.11.8" } }, "nbformat": 4, diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index 47b73f901..563808e52 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -154,7 +154,7 @@ def canonicalize(s, type, ignores): s, flags=re.DOTALL) for n, p in enumerate(ignores): - s = re.sub(p, 'IGN{}'.format(n), s) + s = re.sub(p, f'IGN{n}', s) return s @@ -219,8 +219,7 @@ def compare_outputs(ref, test, ignores=[]): ok = True if len(cref) != len(ctest): - print("output length mismatch (expected {}, got {})".format( - len(cref), len(ctest))) + print(f"output length mismatch: expected {len(cref)}, got {len(ctest)}") ok = False # There can be several outputs. For instance wnen the cell both # prints a result (goes to "stdout") and displays an automaton diff --git a/tests/python/ltlf.py b/tests/python/ltlf.py index afd114855..2d964d04b 100644 --- a/tests/python/ltlf.py +++ b/tests/python/ltlf.py @@ -42,7 +42,7 @@ for f in formulas: f2 = f1.unabbreviate() f3 = spot.formula_And([spot.from_ltlf(f1), cst]) f4 = spot.formula_And([spot.from_ltlf(f2), cst]) - print("{}\t=>\t{}".format(f1, f3)) - print("{}\t=>\t{}".format(f2, f4)) + print(f"{f1}\t=>\t{f3}") + print(f"{f2}\t=>\t{f4}") tc.assertTrue(lcc.equal(f3, f4)) print() diff --git a/tests/python/parity.ipynb b/tests/python/parity.ipynb index a47864c92..95778bd8c 100644 --- a/tests/python/parity.ipynb +++ b/tests/python/parity.ipynb @@ -64,8 +64,8 @@ "for kind in ['min', 'max']:\n", " for style in ['odd', 'even']:\n", " for sets in range(1, 5):\n", - " name = 'parity {} {} {}'.format(kind, style, sets)\n", - " print('{:17} = {}'.format(name, spot.acc_code(name)))" + " name = f'parity {kind} {style} {sets}'\n", + " print(f'{name:17} = {spot.acc_code(name)}')" ] }, { @@ -4949,7 +4949,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc0d6bea0d0> >" + " *' at 0x7f88de01ed30> >" ] }, "metadata": {}, @@ -5460,7 +5460,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.7" + "version": "3.11.8" } }, "nbformat": 4, diff --git a/tests/python/product.ipynb b/tests/python/product.ipynb index e5434e0c7..3a133e982 100644 --- a/tests/python/product.ipynb +++ b/tests/python/product.ipynb @@ -779,8 +779,7 @@ ], "source": [ "def show_prod(a1, a2, res):\n", - " s1 = a1.num_sets()\n", - " display_inline(a1, a2.show('.tvb+{}'.format(s1)), res)\n", + " display_inline(a1, a2.show(f'.tvb+{a1.num_sets()}'), res)\n", "\n", "show_prod(a1, a2, prod)" ] @@ -1714,7 +1713,7 @@ "\n", "The one-liner above is wrong for two reasons:\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", " - 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", "for u 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", - " .format(u=u, v=v, r1=(u&v), r2=(u and v)))" + " print(f\"{u!s:>5} & {v!s:<5} = {u&v!s:<5} {u!s:>5} and {v!s:<5} = {u and v !s:<5}\")" ] }, { @@ -2444,7 +2442,7 @@ "display(p3.show('.1'))\n", "pairs = p3.get_product_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", "output_type": "stream", "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", "output_type": "stream", "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", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.7" + "version": "3.11.8" } }, "nbformat": 4, diff --git a/tests/python/relabel.py b/tests/python/relabel.py index 3b68c2bc8..ed165ee37 100644 --- a/tests/python/relabel.py +++ b/tests/python/relabel.py @@ -25,7 +25,7 @@ m = spot.relabeling_map() g = spot.relabel_bse(f, spot.Pnn, m) res = "" for old, new in m.items(): - res += "#define {} {}\n".format(old, new) + res += f"#define {old} {new}\n" res += str(g) tc.assertEqual(res, """#define p0 a & b #define p1 c diff --git a/tests/python/satmin.ipynb b/tests/python/satmin.ipynb index 0c83d85f5..0522b602e 100644 --- a/tests/python/satmin.ipynb +++ b/tests/python/satmin.ipynb @@ -450,7 +450,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f61ac1ce910> >" + " *' at 0x7fe21cd04240> >" ] }, "execution_count": 3, @@ -799,7 +799,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f61ac1ce430> >" + " *' at 0x7fe21e17b0c0> >" ] }, "execution_count": 4, @@ -1244,7 +1244,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f61ac1ce940> >" + " *' at 0x7fe21cd04090> >" ] }, "execution_count": 5, @@ -1676,7 +1676,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f61ac1cefa0> >" + " *' at 0x7fe21cd04c00> >" ] }, "execution_count": 6, @@ -1938,7 +1938,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f61ac1cee80> >" + " *' at 0x7fe21cd04cf0> >" ] }, "execution_count": 7, @@ -2255,7 +2255,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f61ac1cec40> >" + " *' at 0x7fe21cd04a50> >" ] }, "execution_count": 8, @@ -2546,7 +2546,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f61ac1cebb0> >" + " *' at 0x7fe21cd04870> >" ] }, "execution_count": 9, @@ -2618,9 +2618,9 @@ " NaN\n", " 996\n", " 48806\n", - " 2\n", - " 0\n", + " 1\n", " 0\n", + " 1\n", " 0\n", " \n", " \n", @@ -2633,7 +2633,7 @@ " 2760\n", " 224707\n", " 5\n", - " 0\n", + " 1\n", " 5\n", " 0\n", " \n", @@ -2646,9 +2646,9 @@ " 32\n", " 2008\n", " 155020\n", - " 3\n", + " 4\n", " 0\n", - " 3\n", + " 2\n", " 0\n", " \n", " \n", @@ -2662,9 +2662,9 @@ "2 5 4 4 11 32 2008 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 48806 2 0 0 0 \n", - "1 224707 5 0 5 0 \n", - "2 155020 3 0 3 0 " + "0 48806 1 0 1 0 \n", + "1 224707 5 1 5 0 \n", + "2 155020 4 0 2 0 " ] }, "metadata": {}, @@ -2937,7 +2937,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f611de5a370> >" + " *' at 0x7fe208005380> >" ] }, "execution_count": 10, @@ -3005,10 +3005,10 @@ " NaN\n", " 348\n", " 15974\n", - " 0\n", - " 0\n", " 1\n", " 0\n", + " 0\n", + " 0\n", " \n", " \n", " 1\n", @@ -3021,7 +3021,7 @@ " 73187\n", " 2\n", " 0\n", - " 1\n", + " 0\n", " 0\n", " \n", " \n", @@ -3049,8 +3049,8 @@ "2 2 4 4 11 32 616 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 15974 0 0 1 0 \n", - "1 73187 2 0 1 0 \n", + "0 15974 1 0 0 0 \n", + "1 73187 2 0 0 0 \n", "2 37620 1 0 0 0 " ] }, @@ -3324,7 +3324,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f61ac1cf870> >" + " *' at 0x7fe21e11bc00> >" ] }, "execution_count": 11, @@ -3394,9 +3394,9 @@ " 40\n", " 2300\n", " 288887\n", - " 8\n", + " 7\n", " 0\n", - " 12\n", + " 8\n", " 0\n", " \n", " \n", @@ -3438,7 +3438,7 @@ "2 2 1 NaN NaN NaN 92 \n", "\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", "2 2337 0 0 0 0 " ] @@ -3627,7 +3627,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f61ac1cf960> >" + " *' at 0x7fe21cd04d80> >" ] }, "execution_count": 12, @@ -3695,7 +3695,7 @@ " 40\n", " 2742\n", " 173183\n", - " 4\n", + " 3\n", " 0\n", " 2\n", " 0\n", @@ -3711,7 +3711,7 @@ " 45412\n", " 1\n", " 0\n", - " 0\n", + " 1\n", " 0\n", " \n", " \n", @@ -3723,7 +3723,7 @@ " NaN\n", " 363\n", " 10496\n", - " 1\n", + " 0\n", " 0\n", " 0\n", " 0\n", @@ -3739,9 +3739,9 @@ "2 4 3 NaN NaN NaN 363 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 173183 4 0 2 0 \n", - "1 45412 1 0 0 0 \n", - "2 10496 1 0 0 0 " + "0 173183 3 0 2 0 \n", + "1 45412 1 0 1 0 \n", + "2 10496 0 0 0 0 " ] }, "metadata": {}, @@ -4006,7 +4006,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f611de5b3c0> >" + " *' at 0x7fe21cd04690> >" ] }, "execution_count": 13, @@ -4117,7 +4117,7 @@ " 173427\n", " 0\n", " 0\n", - " 1\n", + " 0\n", " 0\n", " \n", " \n", @@ -4133,7 +4133,7 @@ " clauses enc.user enc.sys sat.user sat.sys \n", "0 173427 3 0 2 0 \n", "1 173427 0 0 0 0 \n", - "2 173427 0 0 1 0 " + "2 173427 0 0 0 0 " ] }, "metadata": {}, @@ -4412,7 +4412,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f611de5b600> >" + " *' at 0x7fe2080067f0> >" ] }, "execution_count": 14, @@ -4484,7 +4484,7 @@ " 173183\n", " 4\n", " 0\n", - " 2\n", + " 1\n", " 0\n", " \n", " \n", @@ -4498,7 +4498,7 @@ " 173279\n", " 0\n", " 0\n", - " 0\n", + " 1\n", " 0\n", " \n", " \n", @@ -4526,8 +4526,8 @@ "2 4 3 NaN NaN NaN 2742 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 173183 4 0 2 0 \n", - "1 173279 0 0 0 0 \n", + "0 173183 4 0 1 0 \n", + "1 173279 0 0 1 0 \n", "2 173327 0 0 0 0 " ] }, @@ -4807,7 +4807,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f611de5bd50> >" + " *' at 0x7fe208006c10> >" ] }, "execution_count": 15, @@ -5108,7 +5108,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f611de5b6f0> >" + " *' at 0x7fe208006940> >" ] }, "metadata": {}, @@ -5159,7 +5159,7 @@ " 40\n", " 2742\n", " 173183\n", - " 4\n", + " 3\n", " 0\n", " 2\n", " 0\n", @@ -5176,7 +5176,7 @@ " 173279\n", " 0\n", " 0\n", - " 0\n", + " 1\n", " 0\n", " HOA: v1 States: 4 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...\n", " \n", @@ -5206,8 +5206,8 @@ "2 4 3 NaN NaN NaN 2742 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \\\n", - "0 173183 4 0 2 0 \n", - "1 173279 0 0 0 0 \n", + "0 173183 3 0 2 0 \n", + "1 173279 0 0 1 0 \n", "2 173327 0 0 0 0 \n", "\n", " automaton \n", @@ -5544,7 +5544,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f611de94660> >" + " *' at 0x7fe208007030> >" ] }, "metadata": {}, @@ -5830,7 +5830,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f611de946f0> >" + " *' at 0x7fe208006fa0> >" ] }, "metadata": {}, @@ -5840,7 +5840,7 @@ "source": [ "for line, data in log.iterrows():\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\"))" ] }, @@ -6261,7 +6261,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f61ac1cefa0> >" + " *' at 0x7fe21cd04c00> >" ] }, "execution_count": 18, @@ -6329,7 +6329,7 @@ " NaN\n", " 687\n", " 21896\n", - " 1\n", + " 0\n", " 0\n", " 0\n", " 0\n", @@ -6343,9 +6343,9 @@ " 32\n", " 1905\n", " 100457\n", - " 2\n", + " 3\n", " 0\n", - " 2\n", + " 1\n", " 0\n", " \n", " \n", @@ -6358,8 +6358,8 @@ "1 6 5 4 12 32 1905 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", - "0 21896 1 0 0 0 \n", - "1 100457 2 0 2 0 " + "0 21896 0 0 0 0 \n", + "1 100457 3 0 1 0 " ] }, "metadata": {}, @@ -6638,7 +6638,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f61ac1cf6c0> >" + " *' at 0x7fe21cd051d0> >" ] }, "execution_count": 19, @@ -6730,7 +6730,7 @@ " 10496\n", " 0\n", " 0\n", - " 0\n", + " 1\n", " 0\n", " \n", " \n", @@ -6746,7 +6746,7 @@ " clauses enc.user enc.sys sat.user sat.sys \n", "0 51612 1 0 1 0 \n", "1 3129 0 0 0 0 \n", - "2 10496 0 0 0 0 " + "2 10496 0 0 1 0 " ] }, "metadata": {}, @@ -7025,7 +7025,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f611de5b960> >" + " *' at 0x7fe208006fa0> >" ] }, "execution_count": 20, @@ -7581,7 +7581,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f611de5b570> >" + " *' at 0x7fe2080074e0> >" ] }, "execution_count": 21, @@ -7610,7 +7610,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.7" + "version": "3.11.8" } }, "nbformat": 4, diff --git a/tests/python/stutter-inv.ipynb b/tests/python/stutter-inv.ipynb index 2cfc87ac7..25b515199 100644 --- a/tests/python/stutter-inv.ipynb +++ b/tests/python/stutter-inv.ipynb @@ -215,7 +215,7 @@ "cell_type": "markdown", "metadata": {}, "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", "In doubt, you can always reset the property as follows:" ] @@ -351,7 +351,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f47047afc00> >" + " *' at 0x7f2110141680> >" ] }, "metadata": {}, @@ -418,9 +418,9 @@ " acc, rej, aut = \"rejected\", \"accepted\", pos\n", " word2 = spot.sl2(waut).intersecting_word(aut)\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", - "{} which is {} by {}\"\"\".format(word, acc, f, word2, rej, f))" + "{word2} which is {rej} by {f}\"\"\")" ] }, { @@ -804,7 +804,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f47047d0bd0> >" + " *' at 0x7f2110143b70> >" ] }, "metadata": {}, @@ -1165,7 +1165,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f47047d0bd0> >" + " *' at 0x7f2110143b70> >" ] }, "metadata": {}, @@ -1389,7 +1389,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f47047d1590> >" + " *' at 0x7f2110143d20> >" ] }, "metadata": {}, @@ -1576,7 +1576,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f47047d0ab0> >" + " *' at 0x7f2110142b50> >" ] }, "metadata": {}, @@ -1962,7 +1962,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f47047d2640> >" + " *' at 0x7f2110142340> >" ] }, "metadata": {}, @@ -2183,7 +2183,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f47047d1d10> >" + " *' at 0x7f2110142580> >" ] }, "metadata": {}, @@ -2392,7 +2392,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f47047d2370> >" + " *' at 0x7f21101417a0> >" ] }, "metadata": {}, @@ -2434,7 +2434,7 @@ "source": [ "sil_vec = spot.stutter_invariant_letters(pos, f)\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 @@ "\n" ], "text/plain": [ - " *' at 0x7f47047d13e0> >" + " *' at 0x7f2110142430> >" ] }, "metadata": {}, @@ -3408,7 +3408,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f47047d13e0> >" + " *' at 0x7f2110142430> >" ] }, "metadata": {}, @@ -3649,7 +3649,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.7" + "version": "3.11.8" } }, "nbformat": 4, diff --git a/tests/python/twagraph-internals.ipynb b/tests/python/twagraph-internals.ipynb index 230d47d89..6a1f7b2c5 100644 --- a/tests/python/twagraph-internals.ipynb +++ b/tests/python/twagraph-internals.ipynb @@ -252,7 +252,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd9b477e340> >" + " *' at 0x7f1fdcf63db0> >" ] }, "execution_count": 3, @@ -784,7 +784,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd9b477e340> >" + " *' at 0x7f1fdcf63db0> >" ] }, "metadata": {}, @@ -1043,7 +1043,8 @@ ], "source": [ "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 @@ "\n" ], "text/plain": [ - " *' at 0x7fd9b477e340> >" + " *' at 0x7f1fdcf63db0> >" ] }, "metadata": {}, @@ -1759,7 +1760,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd9b477e340> >" + " *' at 0x7f1fdcf63db0> >" ] }, "metadata": {}, @@ -1979,7 +1980,7 @@ "cell_type": "markdown", "metadata": {}, "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 @@ "\n" ], "text/plain": [ - " *' at 0x7fd9b477e340> >" + " *' at 0x7f1fdcf63db0> >" ] }, "metadata": {}, @@ -2604,7 +2605,7 @@ "while it:\n", " e = it.current()\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", " it.erase()\n", " else:\n", @@ -2900,7 +2901,8 @@ ], "source": [ "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": [ "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 @@ "\n" ], "text/plain": [ - " *' at 0x7fd9b477e340> >" + " *' at 0x7f1fdcf63db0> >" ] }, "execution_count": 22, @@ -4768,7 +4771,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd9b477e340> >" + " *' at 0x7f1fdcf63db0> >" ] }, "execution_count": 28, @@ -5552,7 +5555,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd9b477e340> >" + " *' at 0x7f1fdcf63db0> >" ] }, "metadata": {}, @@ -6260,7 +6263,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd9b477e340> >" + " *' at 0x7f1fdcf63db0> >" ] }, "metadata": {}, @@ -6758,7 +6761,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd9b4794630> >" + " *' at 0x7f1fdd05b7e0> >" ] }, "metadata": {}, @@ -7129,7 +7132,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fd9b4794630> >" + " *' at 0x7f1fdd05b7e0> >" ] }, "metadata": {}, @@ -7345,7 +7348,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.7" + "version": "3.11.8" } }, "nbformat": 4, diff --git a/tests/python/zlktree.ipynb b/tests/python/zlktree.ipynb index fd0f33a07..3eb6f013f 100644 --- a/tests/python/zlktree.ipynb +++ b/tests/python/zlktree.ipynb @@ -387,7 +387,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 2, @@ -985,7 +985,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f048b0c0> >" + " *' at 0x7f2d01decab0> >" ] }, "execution_count": 10, @@ -994,7 +994,7 @@ } ], "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" ] }, @@ -1809,7 +1809,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f048b510> >" + " *' at 0x7f2d01decd50> >" ] }, "execution_count": 11, @@ -2131,7 +2131,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f048b540> >" + " *' at 0x7f2d01ded4d0> >" ] }, "execution_count": 13, @@ -2140,7 +2140,7 @@ } ], "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" ] }, @@ -2999,7 +2999,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f04a4660> >" + " *' at 0x7f2d01dedc50> >" ] }, "execution_count": 14, @@ -3709,7 +3709,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4355,7 +4355,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4511,7 +4511,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4717,7 +4717,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4777,7 +4777,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -4837,7 +4837,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "metadata": {}, @@ -5222,7 +5222,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 18, @@ -6510,7 +6510,7 @@ "" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 20, @@ -7984,7 +7984,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f04a6d30> >" + " *' at 0x7f2d005206c0> >" ] }, "execution_count": 29, @@ -9202,7 +9202,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f04a6fa0> >" + " *' at 0x7f2d005207b0> >" ] }, "execution_count": 31, @@ -10624,7 +10624,7 @@ "" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 40, @@ -12328,7 +12328,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f0104390> >" + " *' at 0x7f2d00521bc0> >" ] }, "execution_count": 45, @@ -12687,7 +12687,7 @@ "" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 47, @@ -13081,7 +13081,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f0104450> >" + " *' at 0x7f2d005214d0> >" ] }, "execution_count": 48, @@ -13418,7 +13418,7 @@ "" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 49, @@ -13765,7 +13765,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f0104e40> >" + " *' at 0x7f2d00522310> >" ] }, "execution_count": 50, @@ -14036,7 +14036,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f0104960> >" + " *' at 0x7f2d00522970> >" ] }, "execution_count": 51, @@ -14219,7 +14219,7 @@ "\n" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 52, @@ -14530,7 +14530,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f0104ab0> >" + " *' at 0x7f2d00522ac0> >" ] }, "execution_count": 53, @@ -14850,7 +14850,7 @@ "" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 55, @@ -15094,7 +15094,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f0105710> >" + " *' at 0x7f2d00523150> >" ] }, "execution_count": 57, @@ -15367,7 +15367,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f0104d20> >" + " *' at 0x7f2d00523240> >" ] }, "execution_count": 58, @@ -15738,7 +15738,7 @@ "" ], "text/plain": [ - " >" + " >" ] }, "execution_count": 60, @@ -15966,7 +15966,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f01059e0> >" + " *' at 0x7f2d005239c0> >" ] }, "execution_count": 61, @@ -16205,7 +16205,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f01051d0> >" + " *' at 0x7f2d005238a0> >" ] }, "execution_count": 62, @@ -16744,7 +16744,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f01053b0> >" + " *' at 0x7f2d00523720> >" ] }, "execution_count": 63, @@ -16901,7 +16901,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f0106430> >" + " *' at 0x7f2d00523fc0> >" ] }, "execution_count": 64, @@ -17068,7 +17068,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f92f01051a0> >" + " *' at 0x7f2d00550090> >" ] }, "execution_count": 66, @@ -17126,7 +17126,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.7" + "version": "3.11.8" } }, "nbformat": 4,