From cd5ac041f24a9c3a13ea80283c093bf2793f9eae Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 30 Oct 2024 12:07:55 +0100 Subject: [PATCH 1/7] hierarchy: improve error message * spot/tl/hierarchy.cc (mp_class): Fix type of o so that it is displayed as an character in error messages. --- spot/tl/hierarchy.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc index 3ab6f5930..5112c9c12 100644 --- a/spot/tl/hierarchy.cc +++ b/spot/tl/hierarchy.cc @@ -312,7 +312,7 @@ namespace spot bool wide = false; if (opt) for (;;) - switch (int o = *opt++) + switch (char o = *opt++) { case 'v': verbose = true; From 6e6219af54ad332f932d267fb3e31415b58ca57d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 2 Dec 2024 23:24:30 +0100 Subject: [PATCH 2/7] correct to_finite This fixes issue #596. * spot/twaalgos/remprop.cc: Rewrite main loop. * tests/core/ltlf.test: Add test case. * tests/python/game.py: Remove a test that appears to make incorrect assumptions about to_finite. * NEWS: Mention the bug. --- NEWS | 3 + spot/twaalgos/remprop.cc | 21 +++--- tests/core/ltlf.test | 37 +++++++---- tests/python/game.py | 137 --------------------------------------- 4 files changed, 39 insertions(+), 159 deletions(-) diff --git a/NEWS b/NEWS index 68457a365..0afe8a878 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,9 @@ New in spot 2.12.1.dev (not yet released) Nothing yet. + - to_finite() was dealing incorrectly with edges that were + both alive and dead. (Issue #596.) + New in spot 2.12.1 (2024-09-23) Bug fixes: diff --git a/spot/twaalgos/remprop.cc b/spot/twaalgos/remprop.cc index 14570f148..eb7c54dd0 100644 --- a/spot/twaalgos/remprop.cc +++ b/spot/twaalgos/remprop.cc @@ -19,6 +19,7 @@ #include "config.h" #include #include +#include #include #include @@ -180,6 +181,8 @@ namespace spot make_twa_graph(aut, { false, false, true, false, false, false }); + scc_info si(aut, scc_info_options::TRACK_SUCCS); + bdd rem = bddtrue; bdd neg = bddfalse; int v = res->get_dict()-> @@ -194,18 +197,18 @@ namespace spot unsigned ns = res->num_states(); std::vector isacc(ns, false); for (unsigned s = 0; s < ns; ++s) - { - for (auto& e: res->out(s)) - if (bdd_implies(e.cond, neg)) + for (auto& e: res->out(s)) + { + if (!si.is_useful_state(e.dst)) { - isacc[e.src] = true; e.cond = bddfalse; + continue; } - else - { - e.cond = bdd_restrict(e.cond, rem); - } - } + if (bdd_have_common_assignment(e.cond, neg)) + isacc[e.src] = true; + e.cond = bdd_restrict(e.cond, rem); + } + res->set_buchi(); res->prop_state_acc(true); diff --git a/tests/core/ltlf.test b/tests/core/ltlf.test index b8691adc8..77e68d8d8 100755 --- a/tests/core/ltlf.test +++ b/tests/core/ltlf.test @@ -173,51 +173,62 @@ cmp out3 out4 && exit 1 # make sure we did remove something autfilt out3 > out4 diff out4 expected3 -# Issue #526 -ltlfilt -f '(i->XXo)|G(i<->Xo2)' --from-ltlf | ltl2tgba -D |\ +# Issue #526 and Issue #596 +ltlfilt -f '(i->XXo)|G(i<->Xo2)' -f XXXo --from-ltlf | ltl2tgba -D |\ autfilt -C --to-finite > out cat >exp < selfloop - # 2 Prune - acc_state = set() - sp = list(spot.get_state_players(auts)) - for e in auts.edges(): - if e.acc: - acc_state.add(e.src) - for s in acc_state: - e_kill = auts.out_iteraser(s) - while (e_kill): - e_kill.erase() - for s in acc_state: - sprime = auts.new_state() - sp.append(not sp[s]) - auts.new_edge(s, sprime, buddy.bddtrue, [0]) - auts.new_edge(sprime, s, buddy.bddtrue, [0]) - spot.set_state_players(auts, sp) - auts.purge_dead_states() - spot.alternate_players(auts, False, False) - return auts - -def is_input_complete(auts): - sp = spot.get_state_players(auts) - for s in range(auts.num_states()): - if sp[s]: - continue # Player - cumul = buddy.bddfalse - for e in auts.out(s): - cumul |= e.cond - if cumul != buddy.bddtrue: - return False - - return True - -def synt_from_ltlf(f:str, outs): - ff = spot.from_ltlf(f, alive) - aut = ff.translate("buchi", "sbacc") - outbdd = buddy.bddtrue - for out in outs: - outbdd &= buddy.bdd_ithvar(aut.register_ap(out)) - alive_bdd = buddy.bdd_ithvar(aut.register_ap(alive)) - auts = spot.split_2step(aut, outbdd & alive_bdd, False) - auts = spot.to_finite(auts, alive) - spot.alternate_players(auts, False, False) - spot.set_synthesis_outputs(auts, outbdd) - if not is_input_complete(auts): - print("Not synthesizable") - return None - auts = finite_existential(auts) - - return auts - -def synt_ltlf(f:str, outs, res:str = "aut"): - auts = synt_from_ltlf(f, outs) - - succ = spot.solve_parity_game(auts) - if not succ: - if res == "aut": - return False, auts - else: - return False, None - - mealy_cc = spot.solved_game_to_split_mealy(auts) - - if res == "aut": - return True, mealy_cc - elif res == "aig": - return True, spot.mealy_machine_to_aig(mealy_cc, "isop") - else: - raise RuntimeError("Unknown option") - - -sink_player = None - -def negate_ltlf(f:str, outs, opt = "buchi"): - - global sink_player - sink_player = None - - aut = synt_from_ltlf(f, outs) - # Implies input completeness - # We need output completeness - acc = [] - - sp = list(spot.get_state_players(aut)) - - def get_sink(): - global sink_player - if sink_player is None: - sink_player = aut.new_states(2) - aut.new_edge(sink_player, sink_player + 1, buddy.bddtrue, acc) - aut.new_edge(sink_player + 1, sink_player, buddy.bddtrue, acc) - sp.append(False) - sp.append(True) - spot.set_state_players(aut, sp) - return sink_player - - for s in range(aut.num_states()): - if not sp[s]: - continue - rem = buddy.bddtrue - for e in aut.out(s): - rem -= e.cond - if rem != buddy.bddfalse: - aut.new_edge(s, get_sink(), rem) - - # Better to invert colors or condition? - if opt == "buchi": - for e in aut.edges(): - if e.acc: - e.acc = spot.mark_t() - else: - e.acc = spot.mark_t([0]) - elif opt == "cobuchi": - aut.set_co_buchi() - else: - raise RuntimeError("Unknown opt") - return aut - -# Game where the edge_vector is larger -# than the number of transitions -f1 = "((((G (F (idle))) && (G (((idle) && (X ((! (grant_0)) \ - && (! (grant_1))))) -> (X (idle))))) && (G ((X (! (grant_0))) \ - || (X (((! (request_0)) && (! (idle))) U ((! (request_0)) \ - && (idle))))))) -> (((G (((((X (((! (grant_0)) && (true)) \ - || ((true) && (! (grant_1))))) && ((X (grant_0)) -> (request_0))) \ - && ((X (grant_1)) -> (request_1))) && ((request_0) -> (grant_1))) \ - && ((! (idle)) -> (X ((! (grant_0)) && (! (grant_1))))))) \ - && (! (F (G ((request_0) && (X (! (grant_0)))))))) \ - && (! (F (G ((request_1) && (X (! (grant_1)))))))))" -outs = ["grant_0", "grant1"] -tc.assertEqual(synt_ltlf(f1, outs)[0], False) From c67332f8250010bd5ea19b3927561fd87d77e91c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 9 Dec 2024 12:09:15 +0100 Subject: [PATCH 3/7] Fix LaTeX rendering of strong next Fix #597. * spot/tl/print.cc: Fix rendering of X[!]. * doc/tl/spotltl.sty: Add a \StrongX definition. * tests/core/latex.test: Add a test case. * NEWS: Mention the issue. --- NEWS | 3 +++ doc/tl/spotltl.sty | 1 + spot/tl/print.cc | 4 ++-- tests/core/latex.test | 1 + 4 files changed, 7 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 0afe8a878..e0aba4488 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,9 @@ New in spot 2.12.1.dev (not yet released) - to_finite() was dealing incorrectly with edges that were both alive and dead. (Issue #596.) + - LaTeX output of the X[!] operator with broken in both + LaTeX and self-contained LaTeX mode. (Issue #597) + New in spot 2.12.1 (2024-09-23) Bug fixes: diff --git a/doc/tl/spotltl.sty b/doc/tl/spotltl.sty index b8178ee6b..e4b612b20 100644 --- a/doc/tl/spotltl.sty +++ b/doc/tl/spotltl.sty @@ -12,6 +12,7 @@ \newcommand{\F}{\mathsf{F}} % eventually \newcommand{\G}{\mathsf{G}} % always \newcommand{\X}{\mathsf{X}} % next +\newcommand{\StrongX}{\mathsf{X^{[!]}}} % strong next % The \mathbin tells TeX to adjust spacing for binary operators \newcommand{\M}{\mathbin{\mathsf{M}}} % strong release \newcommand{\R}{\mathbin{\mathsf{R}}} % release diff --git a/spot/tl/print.cc b/spot/tl/print.cc index ef998ba86..bb5c5c068 100644 --- a/spot/tl/print.cc +++ b/spot/tl/print.cc @@ -273,7 +273,7 @@ namespace spot "\\SereEqual{", "\\SereGoto{", "\\FirstMatch", - "\\StrongX", + "\\StrongX ", }; const char* sclatex_kw[] = { @@ -318,7 +318,7 @@ namespace spot "^{=", "^{\\to", "\\mathsf{first\\_match}", - "\\textcircled{\\mathsf{X}}", + "\\mathsf{X^{[!]}}", }; static bool diff --git a/tests/core/latex.test b/tests/core/latex.test index 4101e25bb..c2218b4d3 100755 --- a/tests/core/latex.test +++ b/tests/core/latex.test @@ -37,6 +37,7 @@ a U b W c R (d & e) M f {a*;(b;c)[:*3..4];(c;d)[:+];d}! G(uglyname->Fuglierlongname42) "#foo/$bar$" U "baz~yes^no" +X[!]XX[!]a | G[2:4!]b EOF ( From e4a49cda02491249af49ff4ded9a598571da8a12 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 1 Jan 2025 21:46:35 +0100 Subject: [PATCH 4/7] work around a change in python 3.13 * python/spot/__init__.py: Unindent the docstring for formula.__format__. Because Python 3.13 strips the indentation but previous version didn't, the following test case failed with Python 3.13. * tests/python/formulas.ipynb: Adjust to unindented docstring. --- python/spot/__init__.py | 67 ++++++++++++++++++++----------------- tests/python/formulas.ipynb | 66 ++++++++++++++++++------------------ 2 files changed, 69 insertions(+), 64 deletions(-) diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 6f571f932..126d7e625 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -360,45 +360,50 @@ class formula: raise ValueError("unknown string format: " + format) def __format__(self, spec): + # Some test case print this docstring, and different + # Python version will handled indentation differently. + # (Python versions before 3.13 don't strip indentation.) + # So we cannot indent this until Python 3.13 is thee + # smallest version we support. """Format the formula according to `spec`. - Parameters - ---------- - spec : str, optional - a list of letters that specify how the formula - should be formatted. +Parameters +---------- +spec : str, optional + a list of letters that specify how the formula + should be formatted. - Supported specifiers - -------------------- +Supported specifiers +-------------------- - - 'f': use Spot's syntax (default) - - '8': use Spot's syntax in UTF-8 mode - - 's': use Spin's syntax - - 'l': use LBT's syntax - - 'w': use Wring's syntax - - 'x': use LaTeX output - - 'X': use self-contained LaTeX output - - 'j': use self-contained LaTeX output, adjusted for MathJax +- 'f': use Spot's syntax (default) +- '8': use Spot's syntax in UTF-8 mode +- 's': use Spin's syntax +- 'l': use LBT's syntax +- 'w': use Wring's syntax +- 'x': use LaTeX output +- 'X': use self-contained LaTeX output +- 'j': use self-contained LaTeX output, adjusted for MathJax - Add some of those letters for additional options: +Add some of those letters for additional options: - - 'p': use full parentheses - - 'c': escape the formula for CSV output (this will - enclose the formula in double quotes, and escape - any included double quotes) - - 'h': escape the formula for HTML output - - 'd': escape double quotes and backslash, - for use in C-strings (the outermost double - quotes are *not* added) - - 'q': quote and escape for shell output, using single - quotes or double quotes depending on the contents. - - '[...]': rewrite away all the operators specified in brackets, - using spot.unabbreviate(). +- 'p': use full parentheses +- 'c': escape the formula for CSV output (this will + enclose the formula in double quotes, and escape + any included double quotes) +- 'h': escape the formula for HTML output +- 'd': escape double quotes and backslash, + for use in C-strings (the outermost double + quotes are *not* added) +- 'q': quote and escape for shell output, using single + quotes or double quotes depending on the contents. +- '[...]': rewrite away all the operators specified in brackets, + using spot.unabbreviate(). - - ':spec': pass the remaining specification to the - formating function for strings. +- ':spec': pass the remaining specification to the + formating function for strings. - """ +""" syntax = 'f' parent = False diff --git a/tests/python/formulas.ipynb b/tests/python/formulas.ipynb index 2882ac7ac..c7e894b09 100644 --- a/tests/python/formulas.ipynb +++ b/tests/python/formulas.ipynb @@ -246,43 +246,43 @@ "text": [ "Format the formula according to `spec`.\n", "\n", - " Parameters\n", - " ----------\n", - " spec : str, optional\n", - " a list of letters that specify how the formula\n", - " should be formatted.\n", + "Parameters\n", + "----------\n", + "spec : str, optional\n", + " a list of letters that specify how the formula\n", + " should be formatted.\n", "\n", - " Supported specifiers\n", - " --------------------\n", + "Supported specifiers\n", + "--------------------\n", "\n", - " - 'f': use Spot's syntax (default)\n", - " - '8': use Spot's syntax in UTF-8 mode\n", - " - 's': use Spin's syntax\n", - " - 'l': use LBT's syntax\n", - " - 'w': use Wring's syntax\n", - " - 'x': use LaTeX output\n", - " - 'X': use self-contained LaTeX output\n", - " - 'j': use self-contained LaTeX output, adjusted for MathJax\n", + "- 'f': use Spot's syntax (default)\n", + "- '8': use Spot's syntax in UTF-8 mode\n", + "- 's': use Spin's syntax\n", + "- 'l': use LBT's syntax\n", + "- 'w': use Wring's syntax\n", + "- 'x': use LaTeX output\n", + "- 'X': use self-contained LaTeX output\n", + "- 'j': use self-contained LaTeX output, adjusted for MathJax\n", "\n", - " Add some of those letters for additional options:\n", + "Add some of those letters for additional options:\n", "\n", - " - 'p': use full parentheses\n", - " - 'c': escape the formula for CSV output (this will\n", - " enclose the formula in double quotes, and escape\n", - " any included double quotes)\n", - " - 'h': escape the formula for HTML output\n", - " - 'd': escape double quotes and backslash,\n", - " for use in C-strings (the outermost double\n", - " quotes are *not* added)\n", - " - 'q': quote and escape for shell output, using single\n", - " quotes or double quotes depending on the contents.\n", - " - '[...]': rewrite away all the operators specified in brackets,\n", - " using spot.unabbreviate().\n", + "- 'p': use full parentheses\n", + "- 'c': escape the formula for CSV output (this will\n", + " enclose the formula in double quotes, and escape\n", + " any included double quotes)\n", + "- 'h': escape the formula for HTML output\n", + "- 'd': escape double quotes and backslash,\n", + " for use in C-strings (the outermost double\n", + " quotes are *not* added)\n", + "- 'q': quote and escape for shell output, using single\n", + " quotes or double quotes depending on the contents.\n", + "- '[...]': rewrite away all the operators specified in brackets,\n", + " using spot.unabbreviate().\n", "\n", - " - ':spec': pass the remaining specification to the\n", - " formating function for strings.\n", + "- ':spec': pass the remaining specification to the\n", + " formating function for strings.\n", "\n", - " \n" + "\n" ] } ], @@ -505,7 +505,7 @@ "\n", "\n", - "\n", "\n", " Date: Sun, 5 Jan 2025 13:18:35 +0100 Subject: [PATCH 5/7] Fix slight error in aiger The negation of global equivalences for outputs contained a slight error when the output corresponded to a negated gate. * spot/twaalgos/aiger.cc: Fix * tests/core/ltlsynt.test: Test --- spot/twaalgos/aiger.cc | 5 ++++- tests/core/ltlsynt.test | 12 ++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index 95c758ede..8c29dfe41 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -2061,7 +2061,10 @@ namespace assert(it2 != output_names_all.end()); unsigned outnum = it2 - output_names_all.begin(); unsigned outvar = circuit.output(outnum); - circuit.set_output(i, outvar + neg_repr); + assert(outvar != -1u); + if (neg_repr) + outvar = circuit.aig_not(outvar); + circuit.set_output(i, outvar); } } } diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index dd3e4152c..d8a4c2f44 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -1304,3 +1304,15 @@ f2='G(i1->(o1|!o2)) & G(!i1->(o3|!o4)) & G(i2->(!o1|o2)) & G(!i2->(!o3|o4))&Go5' ltlsynt -f "$f2" --polarity=before-decom --verbose 2>out 1>&2 sed 's/ [0-9.e-]* seconds/ X seconds/g;s/ -> /->/g;' out > outx diff outx exp + +# Additional test for global equivalences +# Specifically if the output is set to the negation of another output + +ltlsynt -f "((G((p0)<->(!(p1))))&&(((F(a))||(G(b)))<->(G(F(p0)))))" \ + --outs "p1, p0" \ + --verify --aiger | tail -n 1 > out + +cat > expected < Date: Fri, 17 Jan 2025 22:50:20 +0100 Subject: [PATCH 6/7] release Spot 2.12.2 * configure.ac, doc/org/setup.org: Bump version to 2.12.2. * bin/common_setup.cc, debian/copyright: Bump copyright year to 2025. * NEWS: Update. --- NEWS | 9 +++++++-- bin/common_setup.cc | 2 +- configure.ac | 2 +- debian/copyright | 2 +- doc/org/setup.org | 4 ++-- 5 files changed, 12 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index e0aba4488..7de69604b 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,6 @@ -New in spot 2.12.1.dev (not yet released) +New in spot 2.12.2 (2025-01-18) - Nothing yet. + Bug fixes: - to_finite() was dealing incorrectly with edges that were both alive and dead. (Issue #596.) @@ -8,6 +8,11 @@ New in spot 2.12.1.dev (not yet released) - LaTeX output of the X[!] operator with broken in both LaTeX and self-contained LaTeX mode. (Issue #597) + - Fix a bug in the AIGER encoding with certain forms of + global-equivalence. + + - Work around a spurious test failure with Python 3.13. + New in spot 2.12.1 (2024-09-23) Bug fixes: diff --git a/bin/common_setup.cc b/bin/common_setup.cc index 1b23833df..7a25a77e9 100644 --- a/bin/common_setup.cc +++ b/bin/common_setup.cc @@ -35,7 +35,7 @@ display_version(FILE *stream, struct argp_state*) fputs(program_name, stream); fputs(" (" PACKAGE_NAME ") " PACKAGE_VERSION "\n\ \n\ -Copyright (C) 2024 by the Spot authors, see the AUTHORS File for details.\n\ +Copyright (C) 2025 by the Spot authors, see the AUTHORS File for details.\n\ License GPLv3+: \ GNU GPL version 3 or later .\n\ This is free software: you are free to change and redistribute it.\n\ diff --git a/configure.ac b/configure.ac index 6f64eab68..69bc4faae 100644 --- a/configure.ac +++ b/configure.ac @@ -17,7 +17,7 @@ # along with this program. If not, see . AC_PREREQ([2.69]) -AC_INIT([spot], [2.12.1.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.12.2], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) diff --git a/debian/copyright b/debian/copyright index 66fdb75c2..ae0fbe68d 100644 --- a/debian/copyright +++ b/debian/copyright @@ -3,7 +3,7 @@ Upstream-Name: spot Source: http://www.lrde.epita.fr/dload/spot/ Files: * -Copyright: 2003-2024 the Spot authors +Copyright: 2003-2025 the Spot authors License: GPL-3+ Spot is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by diff --git a/doc/org/setup.org b/doc/org/setup.org index d8f8f2a3e..bf1a21760 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,11 +1,11 @@ #+OPTIONS: H:2 num:nil toc:t html-postamble:nil ^:nil #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: LASTDATE 2024-09-23 +#+MACRO: LASTDATE 2025-01-18 #+NAME: SPOT_VERSION #+BEGIN_SRC python :exports none :results value :wrap org -return "2.12.1" +return "2.12.2" #+END_SRC #+NAME: TARBALL_LINK From 5cbc28897e16f565d2085d2993f70ee0020334f4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 18 Jan 2025 11:12:22 +0100 Subject: [PATCH 7/7] * configure.ac, NEWS: Bump version to 2.12.2.dev. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 7de69604b..643483799 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.12.2.dev (not yet released) + + Nothing yet. + New in spot 2.12.2 (2025-01-18) Bug fixes: diff --git a/configure.ac b/configure.ac index 69bc4faae..e361d79c6 100644 --- a/configure.ac +++ b/configure.ac @@ -17,7 +17,7 @@ # along with this program. If not, see . AC_PREREQ([2.69]) -AC_INIT([spot], [2.12.2], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.12.2.dev], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])