From e48506f5484c216a085ea9108ed8d35685e166e5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 Jul 2024 12:11:10 +0200 Subject: [PATCH 01/13] improve some comments * spot/twaalgos/complement.hh, spot/twaalgos/complement.cc: Here. --- spot/twaalgos/complement.cc | 7 ++++--- spot/twaalgos/complement.hh | 3 ++- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc index 00e9cb0ce..9fad4eac4 100644 --- a/spot/twaalgos/complement.cc +++ b/spot/twaalgos/complement.cc @@ -515,7 +515,7 @@ namespace spot twa_graph_ptr res = dualize(aut); // There are cases with "t" acceptance that get converted to // Büchi during completion, then dualized to co-Büchi, but the - // acceptance is still not used. To try to clean it up in this + // acceptance is still not used. Try to clean it up in this // case. if (aut->num_sets() == 0 || // Also dualize removes sink states, but doesn't simplify @@ -525,8 +525,9 @@ namespace spot return res; } if (is_very_weak_automaton(aut)) - // removing alternation may need more acceptance sets than we support. - // in this case res==nullptr and we try the other determinization. + // Removing alternation may need more acceptance sets than Spot + // supports. When this happens res==nullptr and we fall back to + // determinization-based complementation. if (twa_graph_ptr res = remove_alternation(dualize(aut), false, aborter, false)) return res; diff --git a/spot/twaalgos/complement.hh b/spot/twaalgos/complement.hh index 4b74f27b8..6bb8ff1d9 100644 --- a/spot/twaalgos/complement.hh +++ b/spot/twaalgos/complement.hh @@ -73,7 +73,8 @@ namespace spot /// If an output_aborter is supplied, it is used to /// abort the construction of larger automata. /// - /// complement_semidet() is not yet used. + /// complement_semidet() is not yet used, as it is not always better + /// when the input is semi-deterministic. SPOT_API twa_graph_ptr complement(const const_twa_graph_ptr& aut, const output_aborter* aborter = nullptr); From 783efa2fe800089ee80505bf1580ceb20deffab7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 25 Jul 2024 18:01:42 +0200 Subject: [PATCH 02/13] * doc/tl/tl.tex: Some typos. --- doc/tl/tl.tex | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 141daa7b8..80c47e973 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1473,10 +1473,10 @@ The goals in most of these simplification are to: \end{itemize} Rewritings defined with $\equivEU$ are applied only when -\verb|tl_simplifier_options::favor_event_univ|' is \texttt{true}: +`\verb|tl_simplifier_options::favor_event_univ|' is \texttt{true}: they try to lift subformulas that are both eventual and universal \emph{higher} in the syntax tree. Conversely, rules defined with $\equivNeu$ -are applied only when \verb|favor_event_univ|' is \texttt{false}: they +are applied only when `\verb|favor_event_univ|' is \texttt{false}: they try to \textit{lower} subformulas that are both eventual and universal. Currently all these simplifications assume LTL semantics, so they make @@ -1486,10 +1486,10 @@ only listed with $\X$. \subsection{Basic Simplifications}\label{sec:basic-simp} These simplifications are enabled with -\verb|tl_simplifier_options::reduce_basics|'. A couple of them may +`\verb|tl_simplifier_options::reduce_basics|'. A couple of them may enlarge the size of the formula: they are denoted using $\equiV$ instead of $\equiv$, and they can be disabled by setting the -\verb|tl_simplifier_options::reduce_size_strictly|' option to +`\verb|tl_simplifier_options::reduce_size_strictly|' option to \texttt{true}. \subsubsection{Basic Simplifications for Temporal Operators} @@ -1715,7 +1715,7 @@ $\Esuffix$. They assume that $b$, denote a Boolean formula. As noted at the beginning for section~\ref{sec:basic-simp}, rewritings denoted with $\equiV$ can be disabled by setting the -\verb|tl_simplifier_options::reduce_size_strictly|' option to +`\verb|tl_simplifier_options::reduce_size_strictly|' option to \texttt{true}. \begin{align*} @@ -1818,7 +1818,7 @@ $q,\,q_i$ & a pure eventuality that is also purely universal \\ \G(f_1\AND\ldots\AND f_n \AND q_1 \AND \ldots \AND q_p)&\equivEU \G(f_1\AND\ldots\AND f_n)\AND q_1 \AND \ldots \AND q_p \\ \G\F(f_1\AND\ldots\AND f_n \AND q_1 \AND \ldots \AND q_p)&\equiv \G(\F(f_1\AND\ldots\AND f_n)\AND q_1 \AND \ldots \AND q_p) \\ \G(f_1\AND\ldots\AND f_n \AND e_1 \AND \ldots \AND e_m \AND \G(e_{m+1}) \AND \ldots\AND \G(e_p))&\equivEU \G(f_1\AND\ldots\AND f_n)\AND \G(e_1 \AND \ldots \AND e_p) \\ - \G(f_1\AND\ldots\AND f_n \AND \G(g_1) \AND \ldots \AND \G(g_m) &\equiv \G(f_1\AND\ldots\AND f_n\AND g_1 \AND \ldots \AND g_m) \\ + \G(f_1\AND\ldots\AND f_n \AND \G(g_1) \AND \ldots \AND \G(g_m)) &\equiv \G(f_1\AND\ldots\AND f_n\AND g_1 \AND \ldots \AND g_m) \\ \F(f_1 \OR \ldots \OR f_n \OR u_1 \OR \ldots \OR u_m \OR \F(u_{m+1})\OR\ldots\OR \F(u_p)) &\equivEU \F(f_1\OR \ldots\OR f_n) \OR \F(u_1 \OR \ldots \OR u_p)\\ \F(f_1 \OR \ldots \OR f_n \OR \F(g_1) \OR \ldots \OR \G(g_m)) &\equiv \F(f_1\OR \ldots\OR f_n \OR g_1 \OR \ldots \OR g_m)\\ \G(f_1)\AND\ldots\AND \G(f_n) \AND \G(e_1) \AND \ldots\AND \G(e_p)&\equivEU \G(f_1\AND\ldots\AND f_n)\AND \G(e_1 \AND \ldots \AND e_p) \\ @@ -1837,19 +1837,19 @@ implication can be done in two ways: \begin{description} \item[Syntactic Implication Checks] were initially proposed by~\citet{somenzi.00.cav}. This detection is enabled by the - ``\verb|tl_simplifier_options::synt_impl|'' option. This is a + `\verb|tl_simplifier_options::synt_impl|' option. This is a cheap way to detect implications, but it may miss some. The rules we implement are described in Appendix~\ref{ann:syntimpl}. \item[Language Containment Checks] were initially proposed by~\citet{tauriainen.03.tr}. This detection is enabled by the - ``\verb|tl_simplifier_options::containment_checks|'' option. + `\verb|tl_simplifier_options::containment_checks|' option. \end{description} In the following rewritings rules, $f\simp g$ means that $g$ was proved to be implied by $f$ using either of the above two methods. Additionally, implications denoted by $f\Simp g$ are only checked if -the ``\verb|tl_simplifier_options::containment_checks_stronger|'' +the `\verb|tl_simplifier_options::containment_checks_stronger|' option is set (otherwise the rewriting rule is not applied). We write $f\simpe g$ iff $f\simp g$ and $g\simp f$. @@ -1936,7 +1936,7 @@ The first six rules, about n-ary operators $\AND$ and $\OR$, are implemented for $n$ operands by testing each operand against all other. To prevent the complexity to escalate, this is only performed with up to 16 operands. That value can be changed in -``\verb|tl_simplifier_options::containment_max_ops|''. +`\verb|tl_simplifier_options::containment_max_ops|'. The following rules mix implication-based checks with formulas that are pure eventualities ($e$) or that are purely universal ($u$). From bdc63db9f041b753134d5342965edee60e58be20 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 21 Aug 2024 11:18:14 +0200 Subject: [PATCH 03/13] ltlgrind: improve error message when formulas are missing The error message, inherited from ltl2tgba, used to say "No formula to translate", but "translate" isn't appropriate here. * bin/common_finput.cc, bin/common_finput.hh (check_no_formula): Allow "translate" to be changed. * bin/ltlgrind.cc: Change it. * tests/core/ltlgrind.test: Test it. --- bin/common_finput.cc | 6 +++--- bin/common_finput.hh | 2 +- bin/ltlgrind.cc | 2 +- tests/core/ltlgrind.test | 8 ++++++++ 4 files changed, 13 insertions(+), 5 deletions(-) diff --git a/bin/common_finput.cc b/bin/common_finput.cc index df0343dd1..14cd06b36 100644 --- a/bin/common_finput.cc +++ b/bin/common_finput.cc @@ -388,14 +388,14 @@ job_processor::run() return error; } -void check_no_formula() +void check_no_formula(const char* action) { if (!jobs.empty()) return; if (isatty(STDIN_FILENO)) - error(2, 0, "No formula to translate? Run '%s --help' for help.\n" + error(2, 0, "No formula to %s? Run '%s --help' for help.\n" "Use '%s -' to force reading formulas from the standard " - "input.", program_name, program_name); + "input.", action, program_name, program_name); jobs.emplace_back("-", job_type::LTL_FILENAME); } diff --git a/bin/common_finput.hh b/bin/common_finput.hh index 30b7f333c..491364d19 100644 --- a/bin/common_finput.hh +++ b/bin/common_finput.hh @@ -93,5 +93,5 @@ public: // Report and error message or add a default job depending on whether // the input is a tty. -void check_no_formula(); +void check_no_formula(const char* action = "translate"); void check_no_automaton(); diff --git a/bin/ltlgrind.cc b/bin/ltlgrind.cc index 626211adc..61ffc3cd5 100644 --- a/bin/ltlgrind.cc +++ b/bin/ltlgrind.cc @@ -199,7 +199,7 @@ main(int argc, char* argv[]) mut_opts |= opt_all; - check_no_formula(); + check_no_formula("mutate"); mutate_processor processor; if (processor.run()) diff --git a/tests/core/ltlgrind.test b/tests/core/ltlgrind.test index f508c4826..bfceef88a 100755 --- a/tests/core/ltlgrind.test +++ b/tests/core/ltlgrind.test @@ -200,3 +200,11 @@ EOF ltlgrind -f 'a U b' -m 999999999999999999999999999 2>err && exit 1 grep 'too large' err + +# The following message appears only if run from a tty. +if (: > /dev/tty) >/dev/null 2>&1 ; then + ltlgrind err && exit 1 + grep 'No formula to mutate' err +fi + +: From 97832af321e1081c07a1473e2f0feefece750fbf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 21 Aug 2024 21:36:54 +0200 Subject: [PATCH 04/13] randltl: fix generation without unary operators * spot/tl/randomltl.hh (has_unary_ops): New method. * spot/tl/randomltl.cc: Avoid creating subformulas of even size when we do not have unary operators. * tests/core/randpsl.test: Test it. * NEWS: Mention it. --- NEWS | 5 ++++- spot/tl/randomltl.cc | 38 +++++++++++++++++++++++++++++++++----- spot/tl/randomltl.hh | 6 ++++++ tests/core/randpsl.test | 18 ++++++++++++++++++ 4 files changed, 61 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index c0ab55c77..47cd487cc 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,9 @@ New in spot 2.12.0.dev (not yet released) - Nothing yet. + Bug fixes: + + - Generating random formula without any unary opertors would very + often create formulas much smaller than asked. New in spot 2.12 (2024-05-16) diff --git a/spot/tl/randomltl.cc b/spot/tl/randomltl.cc index 9aa604ee2..e415535b2 100644 --- a/spot/tl/randomltl.cc +++ b/spot/tl/randomltl.cc @@ -92,14 +92,20 @@ namespace spot { assert(n >= 3); --n; - int l = rrand(1, n - 1); + int l; // size of left + if ((n & 1) | rl->has_unary_ops()) + l = rrand(1, n - 1); + else + // if we do not have unary ops, we must split n in two odd sizes + l = rrand(0, n/2 - 1)*2 + 1; + // Force the order of generation of operands to be right, then // left. This is historical, because gcc evaluates argument // from right to left and we used to make the two calls to // generate() inside of the call to instance() before // discovering that clang would perform the nested calls from // left to right. - auto right = rl->generate(n - l); + formula right = rl->generate(n - l); return formula::binop(Op, rl->generate(l), right); } @@ -110,7 +116,25 @@ namespace spot assert(n >= 3); --n; const random_psl* rp = static_cast(rl); - int l = rrand(1, n - 1); + int l; // size of left + bool left_must_be_odd = !rp->rs.has_unary_ops(); + bool right_must_be_odd = !rl->has_unary_ops(); + if (n & 1) + { + if (left_must_be_odd && !right_must_be_odd) + l = rrand(0, n/2 - 1) * 2 + 1; + else if (!left_must_be_odd && right_must_be_odd) + l = rrand(1, n/2) * 2; + else + l = rrand(1, n - 1); + } + else + { + if (left_must_be_odd || right_must_be_odd) + l = rrand(0, n/2 - 1) * 2 + 1; + else + l = rrand(1, n - 1); + } // See comment in binop_builder. auto right = rl->generate(n - l); return formula::binop(Op, rp->rs.generate(l), right); @@ -152,9 +176,13 @@ namespace spot { assert(n >= 3); --n; - int l = rrand(1, n - 1); // See comment in binop_builder. - auto right = rl->generate(n - l); + int l; // size of left + if ((n & 1) | rl->has_unary_ops()) + l = rrand(1, n - 1); + else + l = rrand(0, n/2 - 1)*2 + 1; + formula right = rl->generate(n - l); return formula::multop(Op, {rl->generate(l), right}); } diff --git a/spot/tl/randomltl.hh b/spot/tl/randomltl.hh index d4c52debf..a7ea3561c 100644 --- a/spot/tl/randomltl.hh +++ b/spot/tl/randomltl.hh @@ -72,6 +72,12 @@ namespace spot /// occurrences of the \c F operator. const char* parse_options(char* options); + /// \brief whether we can use unary operators + bool has_unary_ops() const + { + return total_2_ > 0.0; + } + protected: void update_sums(); diff --git a/tests/core/randpsl.test b/tests/core/randpsl.test index 5e7192894..9d4f825aa 100755 --- a/tests/core/randpsl.test +++ b/tests/core/randpsl.test @@ -36,3 +36,21 @@ test `wc -l < formulas` = 50 randltl --psl --sere-priorities=first_match=10 -n 100 2 | grep first_match + +# the random generator had trouble generating formulas of the proper size when +# unary operators were disabled +P=true=0,false=0,not=0 +randltl --tree-size=19 -B --boolean-prio=$P 1000 -n10 --stats=%a >out +cat >expected < Date: Fri, 30 Aug 2024 16:05:50 +0200 Subject: [PATCH 05/13] game: fix solving "parity min" games with multi-colored edges * spot/twaalgos/game.cc: If the original acceptance is "parity min", use min_set(), not max_set(), to read edge priorities. * tests/python/game.py: Add a test case. * NEWS: Mention the bug. --- NEWS | 5 +++++ spot/twaalgos/game.cc | 3 ++- tests/python/game.py | 25 ++++++++++++++++++++++++- 3 files changed, 31 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 47cd487cc..343c36543 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,11 @@ New in spot 2.12.0.dev (not yet released) - Generating random formula without any unary opertors would very often create formulas much smaller than asked. + - The parity game solver, which internally works on "parity max + odd", but actually accept any type of parity acceptance, could be + confused by games with "parity min" acceptance using transition + with several colors (a rather uncommon situation). + New in spot 2.12 (2024-05-16) Build: diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index 404fa4778..e2c550531 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -357,7 +357,8 @@ namespace spot // Takes an edge and returns the "equivalent" max odd parity auto equiv_par = [max, odd, next_max_par, inv = 2*max-1](const auto& e) { - par_t e_par = e.acc.max_set() - 1; // -1 for empty + par_t e_par = + (max ? e.acc.max_set() : e.acc.min_set()) - 1; // -1 for empty // If "min" and empty -> set to n if (!max & (e_par == -1)) e_par = next_max_par; diff --git a/tests/python/game.py b/tests/python/game.py index e0d880647..3eba9bf41 100644 --- a/tests/python/game.py +++ b/tests/python/game.py @@ -351,6 +351,21 @@ State: 17 --END--""" ) +def maximize_colors(aut, is_max): + ns = aut.num_sets() + v = [] + if is_max: + for c in range(ns+1): + v.append(spot.mark_t(list(range(c)))) + for e in aut.edges(): + e.acc = v[e.acc.max_set()] + else: + for c in range(ns+1): + v.append(spot.mark_t(list(range(c, ns)))) + v.insert(0, spot.mark_t([])) + for e in aut.edges(): + e.acc = v[e.acc.min_set()] + # Test the different parity conditions gdpa = spot.tgba_determinize(spot.degeneralize_tba(g), False, True, True, False) @@ -370,6 +385,14 @@ for kind in [spot.parity_kind_min, spot.parity_kind_max]: tc.assertTrue(spot.solve_parity_game(g_test_split1)) c_strat1 = spot.get_strategy(g_test_split1) tc.assertTrue(c_strat == c_strat1) + # Same test, but adding a lot of useless colors in the game + g_test_split2 = spot.change_parity(g_test_split, kind, style) + maximize_colors(g_test_split2, kind == spot.parity_kind_max) + spot.set_state_players(g_test_split2, sp) + tc.assertTrue(spot.solve_parity_game(g_test_split2)) + c_strat2 = spot.get_strategy(g_test_split2) + tc.assertTrue(c_strat == c_strat2) + # Test that strategies are not appended # if solve is called multiple times @@ -520,4 +543,4 @@ f1 = "((((G (F (idle))) && (G (((idle) && (X ((! (grant_0)) \ && (! (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) \ No newline at end of file +tc.assertEqual(synt_ltlf(f1, outs)[0], False) From f5ab5678b5f6145f21af0f9da2f258073d5a9f40 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 2 Sep 2024 13:50:36 +0200 Subject: [PATCH 06/13] python: improve support of spot-extra, and recent swig I could not run "make check" in a copy of seminator 2.0 regenerated with swig 4.0, because of changes in the way Swig imports its shared libraries. * python/spot/__init__.py: If sys.path contains "/spot-extra" directory, add it to spot.__path__ as well. This helps situations where a plugin use libtool and the development tree has the shared libraries in .../spot-extra/.libs/ --- python/spot/__init__.py | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 1c6133390..6f571f932 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -38,11 +38,17 @@ if 'SPOT_UNINSTALLED' in os.environ: # We may have third-party plugins that want to be loaded as "spot.xxx", but # that are installed in a different $prefix. This sets things so that any # file that looks like spot-extra/xxx.py can be loaded with "import spot.xxx". +# When libtool is used in a development build, it is likely that PYTHONPATH +# is already set up to contains something like .../spot-extra/.libs, so we +# want to copy those as well. for path in sys.path: if path not in __path__: - path += "/spot-extra" - if os.path.isdir(path): + if "/spot-extra" in path: __path__.append(path) + else: + path += "/spot-extra" + if os.path.isdir(path): + __path__.append(path) from spot.impl import * @@ -58,7 +64,7 @@ from spot.aux import \ ostream_to_svg as _ostream_to_svg -# The parrameters used by default when show() is called on an automaton. +# The parameters used by default when show() is called on an automaton. _show_default = None From 514209e80f9097de974da2cc31c6dbc6db95de7f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 2 Sep 2024 13:54:36 +0200 Subject: [PATCH 07/13] * configure.ac: Typo. --- configure.ac | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/configure.ac b/configure.ac index 4ec7633e4..e85feb8cf 100644 --- a/configure.ac +++ b/configure.ac @@ -220,7 +220,7 @@ AC_CHECK_PROG([LBTT_TRANSLATE], [lbtt-translate], [lbtt-translate]) AX_CHECK_VALGRIND # Debian used to reserve the name 'swig' for swig-2.0. So prefer # swig4.0 (available in Debian bullseye) to swig3.0 (available in Debian buster) -# ti swig. +# to swig. AC_CHECK_PROGS([SWIG], [swig4.0 swig3.0 swig], [swig]) AC_SUBST([CROSS_COMPILING], [$cross_compiling]) From 1a36ea6ce4248ad50fb5169d37489b77ae29b283 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 2 Sep 2024 17:26:42 +0200 Subject: [PATCH 08/13] ltlsynt: fix usage for --dot's argument * bin/ltlsynt.cc (dispatch_print_hoa): Pass the right argument to print_dot. * tests/core/ltlsynt.test: Test it. * NEWS: Mention the bug. --- NEWS | 2 ++ bin/ltlsynt.cc | 2 +- tests/core/ltlsynt.test | 6 +++++- 3 files changed, 8 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 343c36543..c1045dcca 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,8 @@ New in spot 2.12.0.dev (not yet released) confused by games with "parity min" acceptance using transition with several colors (a rather uncommon situation). + - "ltlsynt ... --print-game --dot=ARGS" was ignoring ARGS. + New in spot 2.12 (2024-05-16) Build: diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 24f4af16a..a85dbc3a9 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -322,7 +322,7 @@ namespace rs->patch_game(game); if (opt_dot) - spot::print_dot(std::cout, game, opt_print_hoa_args); + spot::print_dot(std::cout, game, opt_dot_arg); else if (opt_print_pg) spot::print_pg(std::cout, game); else diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 1e0397a5f..dd3e4152c 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -1085,7 +1085,11 @@ diff outx exp # Test --dot and --hide-status ltlsynt -f 'i <-> Fo' --ins=i --aiger --dot | grep arrowhead=dot -ltlsynt -f 'i <-> Fo' --ins=i --print-game-hoa --dot | grep 'shape="diamond"' +ltlsynt -f 'i <-> Fo' --ins=i --print-game-hoa --dot > out +grep 'shape="diamond"' out +grep 'Inf(0)' out +ltlsynt -f 'i <-> Fo' --ins=i --print-game-hoa --dot=bar > out +grep 'label= Fo' --ins=i --dot --hide-status > res cat >exp < Date: Mon, 2 Sep 2024 17:28:28 +0200 Subject: [PATCH 09/13] fix spurious g++-14 warning * spot/twaalgos/mealy_machine.cc (mm_sat_prob_t::get_sol): Here. --- spot/twaalgos/mealy_machine.cc | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index e63193cdc..5021f2a94 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -2604,9 +2604,14 @@ namespace return {}; case PICOSAT_SATISFIABLE: { - std::vector - res(1 + (unsigned) picosat_variables(lm.psat_), -1); - SPOT_ASSUME(res.data()); // g++ 11 believes data might be nullptr + unsigned nvar = 1 + (unsigned) picosat_variables(lm.psat_); + // Asssuming res.data() non-null was enough to prevent g++ + // 11 from issuing a spurious "potential null pointer + // dereference" on the res[0] assignment. Since g++14 we + // also need to assume nvar>0. + SPOT_ASSUME(nvar > 0); + std::vector res(nvar, -1); + SPOT_ASSUME(res.data()); res[0] = 0; // Convention for (int lit : lm.all_lits) res[lit] = picosat_deref(lm.psat_, lit); From 376755dbd46eec1b12ca111c3a2ea94fa0d27519 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 3 Sep 2024 17:37:59 +0200 Subject: [PATCH 10/13] game: avoid a spurious g++14 warning * spot/twaalgos/game.cc, spot/twaalgos/game.hh (get_state_winners): Declare a non-const version as well to avoid a "possibly dangling reference" error in code show by tut40.org. --- spot/twaalgos/game.cc | 33 +++++++++++++++++++++++---------- spot/twaalgos/game.hh | 26 ++++++++++++++++---------- 2 files changed, 39 insertions(+), 20 deletions(-) diff --git a/spot/twaalgos/game.cc b/spot/twaalgos/game.cc index e2c550531..9f739d423 100644 --- a/spot/twaalgos/game.cc +++ b/spot/twaalgos/game.cc @@ -1085,12 +1085,12 @@ namespace spot return aut; } - void set_state_players(twa_graph_ptr arena, const region_t& owners) + void set_state_players(twa_graph_ptr& arena, const region_t& owners) { set_state_players(arena, region_t(owners)); } - void set_state_players(twa_graph_ptr arena, region_t&& owners) + void set_state_players(twa_graph_ptr& arena, region_t&& owners) { if (owners.size() != arena->num_states()) throw std::runtime_error @@ -1100,7 +1100,7 @@ namespace spot new region_t(std::move(owners))); } - void set_state_player(twa_graph_ptr arena, unsigned state, bool owner) + void set_state_player(twa_graph_ptr& arena, unsigned state, bool owner) { if (state >= arena->num_states()) throw std::runtime_error("set_state_player(): invalid state number"); @@ -1141,7 +1141,7 @@ namespace spot return *owners; } - bool get_state_player(const_twa_graph_ptr arena, unsigned state) + bool get_state_player(const const_twa_graph_ptr& arena, unsigned state) { if (state >= arena->num_states()) throw std::runtime_error("get_state_player(): invalid state number"); @@ -1165,11 +1165,11 @@ namespace spot return *strat_ptr; } - void set_strategy(twa_graph_ptr arena, const strategy_t& strat) + void set_strategy(twa_graph_ptr& arena, const strategy_t& strat) { set_strategy(arena, strategy_t(strat)); } - void set_strategy(twa_graph_ptr arena, strategy_t&& strat) + void set_strategy(twa_graph_ptr& arena, strategy_t&& strat) { if (arena->num_states() != strat.size()) throw std::runtime_error("set_strategy(): strategies need to have " @@ -1214,12 +1214,12 @@ namespace spot } - void set_state_winners(twa_graph_ptr arena, const region_t& winners) + void set_state_winners(twa_graph_ptr& arena, const region_t& winners) { set_state_winners(arena, region_t(winners)); } - void set_state_winners(twa_graph_ptr arena, region_t&& winners) + void set_state_winners(twa_graph_ptr& arena, region_t&& winners) { if (winners.size() != arena->num_states()) throw std::runtime_error @@ -1229,7 +1229,7 @@ namespace spot new region_t(std::move(winners))); } - void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner) + void set_state_winner(twa_graph_ptr& arena, unsigned state, bool winner) { if (state >= arena->num_states()) throw std::runtime_error("set_state_winner(): invalid state number"); @@ -1258,7 +1258,20 @@ namespace spot return *winners; } - bool get_state_winner(const_twa_graph_ptr arena, unsigned state) + // This second version should not be needed, but g++14 emits + // "possibly dangling reference" warnings when it sees that the + // first function is called with a temporary const_twa_graph_ptr to + // return a reference. + const region_t& get_state_winners(twa_graph_ptr& arena) + { + region_t *winners = arena->get_named_prop("state-winner"); + if (!winners) + throw std::runtime_error + ("get_state_winners(): state-winner property not defined, not a game?"); + return *winners; + } + + bool get_state_winner(const const_twa_graph_ptr& arena, unsigned state) { if (state >= arena->num_states()) throw std::runtime_error("get_state_winner(): invalid state number"); diff --git a/spot/twaalgos/game.hh b/spot/twaalgos/game.hh index c376304be..737a50d78 100644 --- a/spot/twaalgos/game.hh +++ b/spot/twaalgos/game.hh @@ -151,20 +151,20 @@ namespace spot /// \brief Set the owner for all the states. /// @{ SPOT_API - void set_state_players(twa_graph_ptr arena, const region_t& owners); + void set_state_players(twa_graph_ptr& arena, const region_t& owners); SPOT_API - void set_state_players(twa_graph_ptr arena, region_t&& owners); + void set_state_players(twa_graph_ptr& arena, region_t&& owners); /// @} /// \ingroup games /// \brief Set the owner of a state. SPOT_API - void set_state_player(twa_graph_ptr arena, unsigned state, bool owner); + void set_state_player(twa_graph_ptr& arena, unsigned state, bool owner); /// \ingroup games /// \brief Get the owner of a state. SPOT_API - bool get_state_player(const_twa_graph_ptr arena, unsigned state); + bool get_state_player(const const_twa_graph_ptr& arena, unsigned state); /// \ingroup games /// \brief Get the owner of all states @@ -181,9 +181,9 @@ namespace spot SPOT_API const strategy_t& get_strategy(const const_twa_graph_ptr& arena); SPOT_API - void set_strategy(twa_graph_ptr arena, const strategy_t& strat); + void set_strategy(twa_graph_ptr& arena, const strategy_t& strat); SPOT_API - void set_strategy(twa_graph_ptr arena, strategy_t&& strat); + void set_strategy(twa_graph_ptr& arena, strategy_t&& strat); /// @} /// \ingroup games @@ -205,23 +205,29 @@ namespace spot /// \brief Set the winner for all the states. /// @{ SPOT_API - void set_state_winners(twa_graph_ptr arena, const region_t& winners); + void set_state_winners(twa_graph_ptr& arena, const region_t& winners); SPOT_API - void set_state_winners(twa_graph_ptr arena, region_t&& winners); + void set_state_winners(twa_graph_ptr& arena, region_t&& winners); /// @} /// \ingroup games /// \brief Set the winner of a state. SPOT_API - void set_state_winner(twa_graph_ptr arena, unsigned state, bool winner); + void set_state_winner(twa_graph_ptr& arena, unsigned state, bool winner); /// \ingroup games /// \brief Get the winner of a state. SPOT_API - bool get_state_winner(const_twa_graph_ptr arena, unsigned state); + bool get_state_winner(const const_twa_graph_ptr& arena, unsigned state); /// \ingroup games /// \brief Get the winner of all states + /// @{ SPOT_API const region_t& get_state_winners(const const_twa_graph_ptr& arena); +#ifndef SWIG + SPOT_API + const region_t& get_state_winners(twa_graph_ptr& arena); +#endif + /// @} } From c92418b51c7606f27197061970b070fcb047f531 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 23 Sep 2024 11:49:26 +0200 Subject: [PATCH 11/13] * .gitlab-ci.yml (publish-stable): Add scp for LRE's dload host. --- .gitlab-ci.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8aabfb8fa..a48b23ae8 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -436,11 +436,12 @@ publish-stable: - cd .. - ls -l - tgz=`ls spot-*.tar.* | head -n 1` - - case $tgz in *[0-9].tar.*) scp $tgz doc@perso:/var/www/dload/spot/;; esac + - case $tgz in *[0-9].tar.*) scp $tgz doc@perso:/var/www/dload/spot/; scp $tgz doc@dload:/var/www/html/spot/;; esac - rm -rf ./* - curl -X POST -F ref=master -F token=$TRIGGER_SPOT_WEB -F "variables[spot_branch]=stable" https://gitlab.lre.epita.fr/api/v4/projects/131/trigger/pipeline - curl -X POST "https://archive.softwareheritage.org/api/1/origin/save/git/url/https://gitlab.lre.epita.fr/spot/spot/" - curl "https://web.archive.org/save/https://www.lrde.epita.fr/dload/spot/$tgz" + - curl "https://web.archive.org/save/https://www.lre.epita.fr/dload/spot/$tgz" publish-unstable: only: From b63f16060ab9c9437bcd15cb704fecb71eec8978 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 23 Sep 2024 12:04:28 +0200 Subject: [PATCH 12/13] release Spot 2.12.1 * NEWS, configure.ac, doc/org/setup.org: Update. --- NEWS | 7 ++++++- configure.ac | 2 +- doc/org/setup.org | 4 ++-- 3 files changed, 9 insertions(+), 4 deletions(-) diff --git a/NEWS b/NEWS index c1045dcca..329cc51ad 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.12.0.dev (not yet released) +New in spot 2.12.1 (2024-09-23) Bug fixes: @@ -12,6 +12,11 @@ New in spot 2.12.0.dev (not yet released) - "ltlsynt ... --print-game --dot=ARGS" was ignoring ARGS. + - Work around various warnings from g++14. + + - Improved handling of spot-extra/ directory with newer Swig + versions. Necessary to recompile Seminator 2 with Swig 4. + New in spot 2.12 (2024-05-16) Build: diff --git a/configure.ac b/configure.ac index e85feb8cf..9f229582b 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.0.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.12.1], [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/doc/org/setup.org b/doc/org/setup.org index 440dcfa00..d8f8f2a3e 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-05-14 +#+MACRO: LASTDATE 2024-09-23 #+NAME: SPOT_VERSION #+BEGIN_SRC python :exports none :results value :wrap org -return "2.12" +return "2.12.1" #+END_SRC #+NAME: TARBALL_LINK From b05c90cd87caa5183706a463e3e0095a23b661c5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 23 Sep 2024 13:33:08 +0200 Subject: [PATCH 13/13] bump version to 2.12.1.dev * NEWS, configure.ac: Here. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 329cc51ad..68457a365 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.12.1.dev (not yet released) + + Nothing yet. + New in spot 2.12.1 (2024-09-23) Bug fixes: diff --git a/configure.ac b/configure.ac index 9f229582b..6f64eab68 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], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.12.1.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])