From 3612f3416d251664c3ac70e046136710e252ddde Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 3 Dec 2021 08:57:33 +0100 Subject: [PATCH 01/18] * NEWS, configure.ac: Bump version to 2.10.2.dev. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index e82fb0d22..4ca413e07 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.10.2.dev (not yet released) + + Nothing yet. + New in spot 2.10.2 (2021-12-03) Bugs fixed: diff --git a/configure.ac b/configure.ac index 3bc02156b..75fac2b26 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.69]) -AC_INIT([spot], [2.10.2], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.10.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]) From 1bd112949423382544cd3263716fbec261524ca9 Mon Sep 17 00:00:00 2001 From: philipp Date: Mon, 6 Dec 2021 00:02:11 +0100 Subject: [PATCH 02/18] Fixing state reorder bug for mealy minimization Isomorph but different machines were created depending on ARM vs Intel * spot/twaalgos/mealy_machine.cc: Fix here --- spot/twaalgos/mealy_machine.cc | 23 +++++++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index aa7821213..99b762f16 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -2951,6 +2951,19 @@ namespace decltype(iaj_eq)>& used_ziaj_map) { const unsigned n_env_states = minmach->num_states(); + // Looping over unordered is different on arm vs intel + // todo better way to do this? + // We could move it I guess, but the elements are fairly cheap to copy + auto used_ziaj_ordered = std::vector>(); + used_ziaj_ordered.reserve(used_ziaj_map.size()); + + for (const auto& e : used_ziaj_map) + used_ziaj_ordered.push_back(e); + + std::sort(used_ziaj_ordered.begin(), used_ziaj_ordered.end(), + [](const auto& pl, const auto& pr) + {return pl.first < pr.first; }); + // For each minimal letter, create the (input) condition that it represents // This has to be created for each minimal letters // and might be shared between alphabets @@ -2958,7 +2971,7 @@ namespace = comp_represented_cond(red); #ifdef TRACE - for (const auto& el : used_ziaj_map) + for (const auto& el : used_ziaj_ordered) { const unsigned group = x_in_class[el.first.i].first; const bdd& incond = gmm2cond[group][el.first.a]; @@ -3014,7 +3027,7 @@ namespace minmach->edge_storage(it->second).cond |= incond; }; - for (const auto& [iaj, outcond] : used_ziaj_map) + for (const auto& [iaj, outcond] : used_ziaj_ordered) { // The group determines the incond const unsigned group = x_in_class[iaj.i].first; @@ -3232,8 +3245,10 @@ namespace incomp_cubes_list.end(), incomp_cubes_list.begin(), [&](auto& el) -> std::pair - {return {repl1(el.first), - repl2(el.second)}; }); + { + auto r1 = repl1(el.first); + auto r2 = repl2(el.second); + return {r1, r2}; }); }; std::vector> incomp_cubes_list; From 6dd709714865937421fb3e494313d9bda4e88749 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 13 Dec 2021 10:00:51 +0100 Subject: [PATCH 03/18] org: update mailman urls * doc/org/index.org, tests/python/bdditer.py: Here. --- doc/org/index.org | 4 ++-- tests/python/bdditer.py | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/doc/org/index.org b/doc/org/index.org index 72463b7b6..f676b8aa4 100644 --- a/doc/org/index.org +++ b/doc/org/index.org @@ -69,10 +69,10 @@ with]] Spot, you should distribute the source code of that tool as well. =spot-announce@lrde.epita.fr= is an extremely low-traffic and read-only mailing list for release announcements. If you want to stay -informed about future releases of Spot, we invite you to [[https://lists.lrde.epita.fr/listinfo/spot-announce][subscribe]]. +informed about future releases of Spot, we invite you to [[https://lists.lrde.epita.fr/postorius/lists/spot-announce.lrde.epita.fr/][subscribe]]. [[mailto:spot@lrde.epita.fr][=spot@lrde.epita.fr=]] is a list for general discussions and questions -about Spot. [[https://lists.lrde.epita.fr/listinfo/spot][Subscribe here]] if you want to join, but feel free to send +about Spot. [[https://lists.lrde.epita.fr/postorius/lists/spot.lrde.epita.fr/][Subscribe here]] if you want to join, but feel free to send in any question (in English) or bug report without subscribing. * Citing diff --git a/tests/python/bdditer.py b/tests/python/bdditer.py index ea701ac80..3d3bb7894 100644 --- a/tests/python/bdditer.py +++ b/tests/python/bdditer.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de l'Epita -# (LRDE). +# Copyright (C) 2017, 2018, 2021 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -19,8 +19,8 @@ # Tests different ways to explore a BDD label, as discussed in -# http://lists.lrde.epita.fr/pipermail/spot/2017q1/000117.html - +# https://lists.lrde.epita.fr/hyperkitty/list/spot@lrde.epita.fr/\ +# message/WIAOWDKKPXTTK6UBE3MAHDFWIT36EUMX/ import spot import buddy import sys From b860bb242e28c10f4a2c8b51ab30692b13b98b95 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 14 Dec 2021 14:18:53 +0100 Subject: [PATCH 04/18] tl: fix first_match definition * doc/tl/tl.tex: Here. --- doc/tl/tl.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 39e0f1f48..2c0599f82 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -707,7 +707,7 @@ $a$ is an atomic proposition. \VDash f\FSTAR{\mvar{i-1}..}))\\ \end{cases}\\ \sigma\VDash \FIRSTMATCH\code(f\code) & \iff - (\sigma\VDash f)\land (\nexists k<|\sigma|,\,\sigma^{0..k}\nVDash f) + (\sigma\VDash f)\land (\forall k<|\sigma|,\,\sigma^{0..k}\nVDash f) \end{align*}} Notes: From 9d6ba3ff77fb74518e36f20e5c88ad44a1aa9d15 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 16 Dec 2021 14:20:12 +0100 Subject: [PATCH 05/18] * tests/python/word.ipynb: Typo. --- tests/python/word.ipynb | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/python/word.ipynb b/tests/python/word.ipynb index 26f891bca..4e02bf224 100644 --- a/tests/python/word.ipynb +++ b/tests/python/word.ipynb @@ -350,7 +350,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Calling `simplifify()` will produce a shorter word that is compatible with the original word. For instance in the above word, the second `a` is compatible with `!a & b`, so the prefix can be shortened by rotating the cycle." + "Calling `simplify()` will produce a shorter word that is compatible with the original word. For instance, in the above word the second `a` is compatible with `!a & b`, so the prefix can be shortened by rotating the cycle." ] }, { From 80fd158ed5fd60439dea2490a4fbbb9ed63261fa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 16 Dec 2021 17:23:06 +0100 Subject: [PATCH 06/18] sbacc: remove spurious initial state in some output MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This fixes #492, based on a report from Jérôme Dubois. * spot/twaalgos/sbacc.cc: If the initial state is in a rejecting component, start with an initial state whose colors are unsat_mark. * tests/core/sbacc.test: Add test case. * tests/python/pdegen.py: Adjust it. --- NEWS | 6 +++++- spot/twaalgos/sbacc.cc | 2 ++ tests/core/sbacc.test | 34 ++++++++++++++++++++++++++++++++++ tests/python/pdegen.py | 12 ++++++------ 4 files changed, 47 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index 4ca413e07..12176da5e 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,10 @@ New in spot 2.10.2.dev (not yet released) - Nothing yet. + Bugs fixed: + + - On automata where the absence of color is not rejecting + (e.g. co-Büchi) and where the initial state was in a rejecting + SCC, sbacc() could output a superflous state. (Issue #492) New in spot 2.10.2 (2021-12-03) diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index c64ca321f..e79cba774 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -145,6 +145,8 @@ namespace spot // Use any edge going into the initial state to set the first // acceptance mark. init_acc = one_in[s] | common_out[s]; + else + init_acc = unsat_mark.second; old_st.push_back(new_state(s, init_acc)); } diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test index d694fa831..715001b7b 100755 --- a/tests/core/sbacc.test +++ b/tests/core/sbacc.test @@ -289,3 +289,37 @@ State: 0 [0] 0 {0} State: 1 [0] 1 [0] 0 --END-- EOF + +autfilt -S > out <exp < Date: Fri, 17 Dec 2021 12:05:33 +0100 Subject: [PATCH 07/18] complement: fix a regression with 2.9.8 Reported by Reuben Rowe. * spot/twaalgos/complement.cc (complement): Remove the hard-coded simul=0 option on automata with >32 states. In 2.10 simul=0 now implies det-simul=0, causing the regression, and most importantly it is not needed anymore, because we have other threashold like simul-max and simul-trans-pruning in place. * tests/core/complement.test: Add Reuben's automaton as test case. * NEWS: Mention the fix. --- NEWS | 5 + spot/twaalgos/complement.cc | 9 +- tests/core/complement.test | 326 +++++++++++++++++++++++++++++++++++- 3 files changed, 334 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index 12176da5e..80c4a2ed1 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,11 @@ New in spot 2.10.2.dev (not yet released) (e.g. co-Büchi) and where the initial state was in a rejecting SCC, sbacc() could output a superflous state. (Issue #492) + - Compared to 2.9.8, complement() (and many functions using it) was + slower and produced larger outputs on some automata with more than + 32 states due to an optimization of the determinization being + unintentionally disabled. + New in spot 2.10.2 (2021-12-03) Bugs fixed: diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc index 20be9c3eb..8db33225a 100644 --- a/spot/twaalgos/complement.cc +++ b/spot/twaalgos/complement.cc @@ -522,11 +522,10 @@ namespace spot m.set("det-max-states", aborter->max_states()); m.set("det-max-edges", aborter->max_edges()); } - if (aut->num_states() > 32) - { - m.set("ba-simul", 0); - m.set("simul", 0); - } + // In addition to the above options, the simulation-based + // optimization of the determinization is already restricted by + // the default values of simul-max and simul-trans-pruning. + // (See spot-x(7) for details.) spot::postprocessor p(&m); p.set_type(spot::postprocessor::Generic); p.set_pref(spot::postprocessor::Deterministic); diff --git a/tests/core/complement.test b/tests/core/complement.test index 35931f82c..eb3902d28 100755 --- a/tests/core/complement.test +++ b/tests/core/complement.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015-2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2015-2019, 2021 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -157,4 +157,328 @@ HOA: v1 States: 8 Start: 0 AP: 3 "a" "b" "c" Acceptance: 3 Fin(0) | EOF autfilt --complement pos.hoa >neg.hoa autfilt -q --intersect=pos.hoa neg.hoa && exit 1 + + +# The following automaton, generated by the Cyclist theorem prover was +# sent by Reuben Rowe to show a regression between Spot 2.9.8 and Spot +# 2.10. In the latter version, complementation was slower and larger, +# because the simulation-based optimization of the determinization was +# turned off. Here we do not check the runtime, but we can check the output +# size, which should be 4 and not 153. +cat >large.hoa< Date: Fri, 7 Jan 2022 09:28:11 +0100 Subject: [PATCH 08/18] Fixes #495 Monitors can now be split AND completed at the same time. Split can be called on games without providing "synthesis-outputs" - relying on named prop. * spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: Here --- spot/twaalgos/synthesis.cc | 70 ++++++++++++++++++++++++++++---------- spot/twaalgos/synthesis.hh | 12 +++++-- 2 files changed, 61 insertions(+), 21 deletions(-) diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 2143408b1..fc78352f9 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -447,16 +447,28 @@ namespace spot const bdd& output_bdd, bool complete_env) { auto split = make_twa_graph(aut->get_dict()); + + auto [has_unsat, unsat_mark] = aut->acc().unsat_mark(); + split->copy_ap_of(aut); - split->copy_acceptance_of(aut); split->new_states(aut->num_states()); split->set_init_state(aut->get_init_state_number()); - split->set_named_prop("synthesis-outputs", new bdd(output_bdd)); + set_synthesis_outputs(split, output_bdd); - auto [is_unsat, unsat_mark] = aut->acc().unsat_mark(); - if (!is_unsat && complete_env) - throw std::runtime_error("split_2step(): Cannot complete arena for " - "env as there is no unsat mark."); + const auto use_color = has_unsat; + if (has_unsat) + split->copy_acceptance_of(aut); + else + { + if (complete_env) + { + split->set_co_buchi(); // Fin(0) + unsat_mark = acc_cond::mark_t({0}); + has_unsat = true; + } + else + split->acc().set_acceptance(acc_cond::acc_code::t()); + } bdd input_bdd = bddtrue; { @@ -504,9 +516,10 @@ namespace spot unsigned sink_con = -1u; unsigned sink_env = -1u; auto get_sink_con_state = [&split, &sink_con, &sink_env, - um = unsat_mark] + um = unsat_mark, hu = has_unsat] (bool create = true) { + assert(hu); if (SPOT_UNLIKELY((sink_con == -1u) && create)) { sink_con = split->new_state(); @@ -518,7 +531,8 @@ namespace spot }; // Loop over all states - for (unsigned src = 0; src < aut->num_states(); ++src) + const auto n_states = aut->num_states(); + for (unsigned src = 0; src < n_states; ++src) { env_edge_hash.clear(); e_cache.clear(); @@ -579,11 +593,16 @@ namespace spot auto out = split->out(i); if (std::equal(out.begin(), out.end(), dests.begin(), dests.end(), - [](const twa_graph::edge_storage_t& x, + [uc = use_color] + (const twa_graph::edge_storage_t& x, const e_info_t* y) { + // If there is no unsat -> we do not care + // about color + // todo further optim? return x.dst == y->dst - && x.acc == y->acc + && (!uc + || x.acc == y->acc) && x.cond.id() == y->econdout.id(); })) { @@ -592,6 +611,7 @@ namespace spot if (it != env_edge_hash.end()) it->second.second |= one_letter; else + // Uncolored env_edge_hash.emplace(i, eeh_t(split->new_edge(src, i, bddtrue), one_letter)); break; @@ -605,7 +625,8 @@ namespace spot env_hash.emplace(h, d); env_edge_hash.emplace(d, eeh_t(n_e, one_letter)); for (const auto &t: dests) - split->new_edge(d, t->dst, t->econdout, t->acc); + split->new_edge(d, t->dst, t->econdout, + use_color ? t->acc : acc_cond::mark_t({})); } } // letters // save locally stored condition @@ -619,21 +640,34 @@ namespace spot // The named property // compute the owners // env is equal to false - std::vector* owner = - new std::vector(split->num_states(), false); + auto owner = std::vector(split->num_states(), false); // All "new" states belong to the player - std::fill(owner->begin()+aut->num_states(), owner->end(), true); + std::fill(owner.begin()+aut->num_states(), owner.end(), true); // Check if sinks have been created if (sink_env != -1u) - owner->at(sink_env) = false; - split->set_named_prop("state-player", owner); - split->set_named_prop("synthesis-outputs", - new bdd(output_bdd)); + owner.at(sink_env) = false; + + // !use_color -> all words accepted + // complete_env && sink_env == -1u + // complet. for env demanded but already + // satisfied -> split is also all true + if (complete_env && sink_env == -1u && !use_color) + split->acc() = acc_cond::acc_code::t(); + + set_state_players(split, std::move(owner)); // Done return split; } + twa_graph_ptr + split_2step(const const_twa_graph_ptr& aut, bool complete_env) + { + return split_2step(aut, + get_synthesis_outputs(aut), + complete_env); + } + twa_graph_ptr unsplit_2step(const const_twa_graph_ptr& aut) { diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index 9ecd90e73..f85d9b3a6 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -52,11 +52,17 @@ namespace spot /// \param complete_env Whether the automaton should be complete for the /// environment, i.e. the player of inputs /// \note This function also computes the state players - /// \note If the automaton is to be completed for both env and player - /// then egdes between the sinks will be added + /// \note If the automaton is to be completed, sink states will + /// be added for both env and player if necessary SPOT_API twa_graph_ptr split_2step(const const_twa_graph_ptr& aut, - const bdd& output_bdd, bool complete_env); + const bdd& output_bdd, bool complete_env = true); + + /// \ingroup synthesis + /// \brief Like split_2step but relying on the named property + /// 'synthesis-outputs' + SPOT_API twa_graph_ptr + split_2step(const const_twa_graph_ptr& aut, bool complete_env = true); /// \ingroup synthesis /// \brief the inverse of split_2step From cfb782ce75e8036c85176c4d9283cabce9ca232b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 6 Jan 2022 16:41:24 +0100 Subject: [PATCH 09/18] bump copyright year * bin/common_setup.cc, debian/copyright: Here. --- bin/common_setup.cc | 4 ++-- debian/copyright | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/bin/common_setup.cc b/bin/common_setup.cc index 88bfac872..24cacae85 100644 --- a/bin/common_setup.cc +++ b/bin/common_setup.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -35,7 +35,7 @@ display_version(FILE *stream, struct argp_state*) fputs(program_name, stream); fputs(" (" PACKAGE_NAME ") " PACKAGE_VERSION "\n\ \n\ -Copyright (C) 2021 Laboratoire de Recherche et Développement de l'Epita.\n\ +Copyright (C) 2022 Laboratoire de Recherche et Développement de l'Epita.\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/debian/copyright b/debian/copyright index 08af5120c..9c4653c28 100644 --- a/debian/copyright +++ b/debian/copyright @@ -4,7 +4,7 @@ Source: http://spot.lrde.epita.fr/dload/spot/ Files: * Copyright: 2003-2007 Laboratoire d'Informatique de Paris 6 (LIP6) - 2007-2021 Laboratoire de Recherche et Développement de l'Epita (LRDE) + 2007-2022 Laboratoire de Recherche et Développement de l'Epita (LRDE) 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 From da681e6b4d55f5148fca747d86348d486c15ec62 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 11 Jan 2022 22:19:20 +0100 Subject: [PATCH 10/18] dot: improve output to work around GraphViz bug The related GraphViz issue is https://gitlab.com/graphviz/graphviz/-/issues/2179 * spot/twaalgos/dot.cc: Avoid initial newline in title. * NEWS: Mention the bug. * tests/core/det.test, tests/core/dstar.test, tests/core/neverclaimread.test, tests/python/automata-io.ipynb: Adjust test cases. --- NEWS | 3 +++ spot/twaalgos/dot.cc | 13 +++++++++++-- tests/core/det.test | 4 ++-- tests/core/dstar.test | 8 ++++---- tests/core/neverclaimread.test | 4 ++-- tests/python/automata-io.ipynb | 2 +- 6 files changed, 23 insertions(+), 11 deletions(-) diff --git a/NEWS b/NEWS index 80c4a2ed1..735a6798e 100644 --- a/NEWS +++ b/NEWS @@ -11,6 +11,9 @@ New in spot 2.10.2.dev (not yet released) 32 states due to an optimization of the determinization being unintentionally disabled. + - Work around GraphViz bug #2179 by avoiding unnecessary empty + lines in the acceptance conditions shown in dot. + New in spot 2.10.2 (2021-12-03) Bugs fixed: diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 9d8c16d91..7f2511f28 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2014-2021 Laboratoire de Recherche +// Copyright (C) 2011, 2012, 2014-2022 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -626,7 +626,16 @@ namespace spot std::string accstr = aut_->acc().name("d"); if (accstr.empty()) return; - os_ << nl_ << '[' << accstr << ']'; + // If a name or an acceptance formula was printed, + // we need to add a newline before the human version of the acceptance. + // + // We used to always add that line, but on unnamed Büchi + // automata with double circles, this would (1) create an + // empty line, and (2) run into the following GraphViz bug: + // https://gitlab.com/graphviz/graphviz/-/issues/2179 + if (name_ || !dcircles_) + os_ << nl_; + os_ << '[' << accstr << ']'; } void diff --git a/tests/core/det.test b/tests/core/det.test index 4c24b14b6..d6f76226e 100755 --- a/tests/core/det.test +++ b/tests/core/det.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013-2021 Laboratoire de Recherche et Développement de +# Copyright (C) 2013-2022 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -113,7 +113,7 @@ run 0 ../ikwiad -x -DC 'GFa & XGFb' > out.tgba cat >ex.tgba <expected <expected < stdout cat >expected <[Büchi]>\n", + " label=<[Büchi]>\n", " labelloc=\"t\"\n", " node [shape=\"circle\"]\n", " node [style=\"filled\", fillcolor=\"#ffffaa\"]\n", From 480289867f3af5a38b1a9acda252dbb510c05e56 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 14 Jan 2022 15:46:53 +0100 Subject: [PATCH 11/18] sccinfo: fix accepting run computation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * spot/twaalgos/sccinfo.cc (scc_info::get_accepting_run): Ignore edges whose colors are not part of the colors gathered in the SCC up to deciding acceptance. * tests/python/genem.py: New test case, reported by Clément Tamines. * THANKS: Add him. * NEWS: Mention the bug. --- NEWS | 3 +++ THANKS | 1 + spot/twaalgos/sccinfo.cc | 8 ++++---- tests/python/genem.py | 13 +++++++++++-- 4 files changed, 19 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index 735a6798e..835d6d704 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,9 @@ New in spot 2.10.2.dev (not yet released) - Work around GraphViz bug #2179 by avoiding unnecessary empty lines in the acceptance conditions shown in dot. + - Fix a case where generic_accepting_run() incorrectly returns a + cycle around a rejecting self-loop. + New in spot 2.10.2 (2021-12-03) Bugs fixed: diff --git a/THANKS b/THANKS index cd1a8be60..c526bf75e 100644 --- a/THANKS +++ b/THANKS @@ -9,6 +9,7 @@ Cambridge Yang Caroline Lemieux Christian Dax Christopher Ziegler +Clément Tamines David Müller Ernesto Posse Étienne Renault diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index c31999c37..7d82c6b81 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2021 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -637,8 +637,8 @@ namespace spot const unsigned start = (unsigned)substart; // Cycle search - acc_cond actual_cond = acccond.restrict_to(node.acc_marks()) - .force_inf(node.acc_marks()); + acc_cond::mark_t allc = node.acc_marks(); + acc_cond actual_cond = acccond.restrict_to(allc).force_inf(allc); assert(!actual_cond.uses_fin_acceptance()); assert(!actual_cond.is_f()); acc_cond::mark_t acc_to_see = actual_cond.accepting_sets(node.acc_marks()); @@ -650,7 +650,7 @@ namespace spot [&](const twa_graph::edge_storage_t& t) { // Stay in the specified SCC. - return scc_of(t.dst) != scc || filter(t); + return scc_of(t.dst) != scc || filter(t) || !t.acc.subset(allc); }, [&](const twa_graph::edge_storage_t& t) { diff --git a/tests/python/genem.py b/tests/python/genem.py index efc0a84a8..5da9ce85c 100644 --- a/tests/python/genem.py +++ b/tests/python/genem.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018-2021 Laboratoire de Recherche et Développement de l'Epita +# Copyright (C) 2018-2022 Laboratoire de Recherche et Développement de l'Epita # (LRDE). # # This file is part of Spot, a model checking library. @@ -138,6 +138,15 @@ State: 0 [0&1] 0 {4 6 7} [0&!1] 1 {0 6} [!0&1] 0 {3 7} [!0&!1] 0 {0} State: 1 [0&1] 0 {4 6 7} [0&!1] 1 {3 6} [!0&1] 0 {4 7} [!0&!1] 1 {0} --END--""") +# From Clément Tamines (2022-01-14) +act = spot.automaton("""HOA: v1 States: 5 Start: 0 AP: 1 "p0" +acc-name: none Acceptance: 8 (Inf(6) | Fin(7)) & (Inf(4) | Fin(5)) & +(Inf(2) | Fin(3)) & (Inf(0) | Fin(1)) properties: trans-labels +explicit-labels trans-acc --BODY-- State: 0 [!0] 1 {1 2 5 6} [!0] 3 {0 +2 5 6} State: 1 [!0] 4 {1 3 5 6} [0] 3 {0 2 4 7} [!0] 1 {0 2 4 7} +State: 2 [0] 2 {1 2 5 6} [0] 1 {0 3 4 6} [!0] 4 {0 2 4 6} State: 3 +[!0] 2 {0 3 5 7} State: 4 [!0] 2 {0 3 4 6} --END--""") + def generic_emptiness2_rec(aut): spot.cleanup_acceptance_here(aut, False) @@ -306,4 +315,4 @@ def run_bench(automata): assert run3.replay(spot.get_cout()) is True -run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a360]) +run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a360, act]) From 25d6bfd64dabbe9428939c8189fa401e2a72b33e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 14 Jan 2022 15:49:23 +0100 Subject: [PATCH 12/18] bib: more references * doc/spot.bib (blahoudek.16.atva, degiacomo.13.ijcai): New entries. * spot/tl/ltlf.hh, spot/twaalgos/complement.hh: Use them. --- doc/spot.bib | 42 +++++++++++++++++++++++++++++++++++++ spot/tl/ltlf.hh | 6 +++--- spot/twaalgos/complement.hh | 6 +++--- 3 files changed, 48 insertions(+), 6 deletions(-) diff --git a/doc/spot.bib b/doc/spot.bib index 6092de0a5..91ad52f53 100644 --- a/doc/spot.bib +++ b/doc/spot.bib @@ -82,6 +82,20 @@ doi = {10.1007/978-3-642-36742-7_3} } +@InProceedings{ blahoudek.16.atva, + author = {Franti{\v{s}}ek Blahoudek and Matthias Heizmann and Sven + Schewe and Jan Strej{\v{c}}ek and Ming-Hsien Tsai}, + editor = {Marsha Chechik and Jean-Fran{\c{c}}ois Raskin}, + title = {Complementing Semi-deterministic {B\"u}chi Automata}, + booktitle = {Proceedings of the 22th International Conférence on Tools + and Algorithms for the Construction and Analysis of + Systems}, + year = 2016, + publisher = {Springer}, + pages = {770--787}, + doi = {10.1007/978-3-662-49674-9_49} +} + @InProceedings{ bloemen.16.hvc, title = {Multi-core SCC-Based LTL Model Checking}, author = {Vincent Bloemen and {van de Pol}, {Jan Cornelis}}, @@ -283,6 +297,18 @@ doi = {10.1007/978-3-642-04761-9_19} } +@InProceedings{ degiacomo.13.ijcai, + author = {Giuseppe De Giacomo and Moshe Y. Vardi}, + title = {Linear Temporal Logic and Linear Dynamic Logic on Finite + Traces}, + booktitle = {Proceedings of the 23rd International Joint Conference on + Artificial Intelligence (IJCAI'13)}, + year = 2013, + editor = {Francesca Rossi}, + pages = {854--860}, + month = aug +} + @InProceedings{ duret.11.vecos, author = {Alexandre Duret-Lutz}, title = {{LTL} Translation Improvements in {Spot}}, @@ -795,6 +821,22 @@ doi = {10.1007/978-3-642-36742-7_42} } +@InProceedings{ renkin.20.atva, + author = {Florian Renkin and Alexandre Duret-Lutz and Adrien + Pommellet}, + title = {Practical ``Paritizing'' of {E}merson-{L}ei Automata}, + booktitle = {Proceedings of the 18th International Symposium on + Automated Technology for Verification and Analysis + (ATVA'20)}, + year = {2020}, + volume = {12302}, + series = {Lecture Notes in Computer Science}, + pages = {127--143}, + month = oct, + publisher = {Springer}, + doi = {10.1007/978-3-030-59152-6_7} +} + @InProceedings{ rozier.07.spin, author = {Kristin Y. Rozier and Moshe Y. Vardi}, title = {LTL Satisfiability Checking}, diff --git a/spot/tl/ltlf.hh b/spot/tl/ltlf.hh index 4235590c6..1042e2f65 100644 --- a/spot/tl/ltlf.hh +++ b/spot/tl/ltlf.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -27,7 +27,7 @@ namespace spot /// \brief Convert an LTLf into an LTL formula. /// /// This is based on De Giacomo & Vardi (IJCAI'13) reduction from - /// LTLf (finite-LTL) to LTL. + /// LTLf (finite-LTL) to LTL. \cite degiacomo.13.ijcai /// /// In this reduction, finite words are extended into infinite words /// in which a new atomic proposition alive marks the diff --git a/spot/twaalgos/complement.hh b/spot/twaalgos/complement.hh index 330bff664..902f11363 100644 --- a/spot/twaalgos/complement.hh +++ b/spot/twaalgos/complement.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2015, 2017, 2019 Laboratoire de Recherche et +// Copyright (C) 2013-2015, 2017, 2019, 2022 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -49,8 +49,8 @@ namespace spot /// /// The automaton \a aut should be semideterministic. /// - /// Uses the NCSB algorithm described by F. Blahoudek, M. Heizmann, - /// S. Schewe, J. Strejček, and MH. Tsai (TACAS'16). + /// Uses the NCSB algorithm described by F. Blahoudek, et al. + /// \cite blahoudek.16.atva SPOT_API twa_graph_ptr complement_semidet(const const_twa_graph_ptr& aut, bool show_names = false); From cdbf83001017ad45c143363fa3d3d9c3373997f4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 14 Jan 2022 15:52:52 +0100 Subject: [PATCH 13/18] * doc/org/tut40.org: Finish a sentence. --- doc/org/tut40.org | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/doc/org/tut40.org b/doc/org/tut40.org index f3b938d62..b68efe558 100644 --- a/doc/org/tut40.org +++ b/doc/org/tut40.org @@ -25,7 +25,8 @@ $(s',c',a',d')$ leaving $s'$ with a condition $c'$ that covers $c$, some colors $a'\supseteq a$ that covers the colors of $a$ other transition, and reaching a destination state $d'$ that simulates $d$. -In the following automaton, for instance, XXX +In the following automaton, for instance, state 5 simulates state 1, +and state 4 simulates state 0. #+NAME: tut40in #+BEGIN_SRC hoa From 346260c684ab1a3a7d079fd9588707e05fa14ac0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 14 Jan 2022 17:38:14 +0100 Subject: [PATCH 14/18] org: install from GNU Fixes #496. * doc/org/init.el.in: Install org-mode from GNU ELPA. --- doc/org/init.el.in | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/org/init.el.in b/doc/org/init.el.in index 268378b2f..e16d097cc 100644 --- a/doc/org/init.el.in +++ b/doc/org/init.el.in @@ -33,10 +33,10 @@ (message "unloading feature %s" feature) (unload-feature feature t))) ;; install org-plus-contrib, not org, as the former includes htmlize - (add-to-list 'package-archives '("org" . "http://orgmode.org/elpa/") t) + (add-to-list 'package-archives '("gnu" . "https://elpa.gnu.org/packages/") t) (package-refresh-contents) - (let ((org-p-c (cadr (assq 'org-plus-contrib package-archive-contents)))) - (package-install org-p-c))) + (let ((org (cadr (assq 'org package-archive-contents)))) + (package-install org))) (let ((have-htmlize (require 'htmlize nil t)) (have-ess (require 'ess nil t))) From 34646bc0ab63383385527f62e438690d10206d16 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 14 Jan 2022 17:40:55 +0100 Subject: [PATCH 15/18] allow RPM build failure until we can fix it The current building issue is a docker issue unrelated to Spot, so it should not prevent us from doing a release. * .gitlab-ci.yml (rpm-pkg): Allow failure. --- .gitlab-ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 0abb1c6cb..583774da0 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -330,6 +330,7 @@ rpm-pkg: - cp spot.spec ~/rpmbuild/SPECS/ - rpmbuild -bb ~/rpmbuild/SPECS/spot.spec - mv ~/rpmbuild/RPMS/x86_64/*.rpm . + allow_failure: true artifacts: when: always expire_in: 1 week From 4692b8962910cca48f3828c3e7558612c5490365 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 14 Jan 2022 20:34:16 +0100 Subject: [PATCH 16/18] * NEWS: Prepare for next release. --- NEWS | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 835d6d704..610514baa 100644 --- a/NEWS +++ b/NEWS @@ -4,19 +4,27 @@ New in spot 2.10.2.dev (not yet released) - On automata where the absence of color is not rejecting (e.g. co-Büchi) and where the initial state was in a rejecting - SCC, sbacc() could output a superflous state. (Issue #492) + SCC, sbacc() could output a superfluous state. (Issue #492) - Compared to 2.9.8, complement() (and many functions using it) was slower and produced larger outputs on some automata with more than 32 states due to an optimization of the determinization being unintentionally disabled. + - The split_2step() function used to create a synthesis game could + complain that it was unable to complement a monitor (Issue #495). + - Work around GraphViz bug #2179 by avoiding unnecessary empty lines in the acceptance conditions shown in dot. - Fix a case where generic_accepting_run() incorrectly returns a cycle around a rejecting self-loop. + - Mealy machine resulting from SAT-based minimization could differ + on architectures with different hash tables implementations. + + - org-mode moved to GNU ELPA (Issue #496). + New in spot 2.10.2 (2021-12-03) Bugs fixed: From dd3395083646eafe0117ddbc1a6380ed6226cfd0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 15 Jan 2022 08:02:18 +0100 Subject: [PATCH 17/18] Release Spot 2.10.3 * NEWS, configure.ac, doc/org/setup.org: Update version. --- NEWS | 2 +- configure.ac | 4 ++-- doc/org/setup.org | 10 +++++----- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 610514baa..50e9a513a 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.10.2.dev (not yet released) +New in spot 2.10.3 (2022-01-15) Bugs fixed: diff --git a/configure.ac b/configure.ac index 75fac2b26..b297e2090 100644 --- a/configure.ac +++ b/configure.ac @@ -1,5 +1,5 @@ # -*- coding: utf-8 -*- -# Copyright (C) 2008-2021, Laboratoire de Recherche et Développement +# Copyright (C) 2008-2022, Laboratoire de Recherche et Développement # de l'Epita (LRDE). # Copyright (C) 2003-2007 Laboratoire d'Informatique de Paris 6 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.69]) -AC_INIT([spot], [2.10.2.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.10.3], [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 a1a8493a2..6333e2379 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: SPOTVERSION 2.10.2 -#+MACRO: LASTRELEASE 2.10.2 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.10.2.tar.gz][=spot-2.10.2.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-10-2/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2021-12-03 +#+MACRO: SPOTVERSION 2.10.3 +#+MACRO: LASTRELEASE 2.10.3 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.10.3.tar.gz][=spot-2.10.3.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-10-3/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2022-01-15 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From c12842c16f8b1631c58a01f6dce5e4285225bec5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 15 Jan 2022 08:04:10 +0100 Subject: [PATCH 18/18] * NEWS, configure.ac: Bump version to 2.10.3.dev. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 50e9a513a..3175ee43f 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.10.3.dev (net yet released) + + Nothing yet. + New in spot 2.10.3 (2022-01-15) Bugs fixed: diff --git a/configure.ac b/configure.ac index b297e2090..73823354d 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.69]) -AC_INIT([spot], [2.10.3], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.10.3.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])