From 16373cfb107e89cfd2074a2900c8d5bcab30a2e4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 8 Dec 2022 17:27:32 +0100 Subject: [PATCH 01/21] Work around spurious g++-12 warnings * spot/twaalgos/ltl2tgba_fm.cc, spot/tl/formula.hh, spot/twaalgos/translate.cc: Add SPOT_ASSUME in various places to help g++. --- spot/tl/formula.hh | 4 +++- spot/twaalgos/ltl2tgba_fm.cc | 15 ++++++++++----- spot/twaalgos/translate.cc | 9 ++++++--- 3 files changed, 19 insertions(+), 9 deletions(-) diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index d01b8379c..b60000479 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -294,7 +294,9 @@ namespace spot { if (SPOT_UNLIKELY(i >= size())) report_non_existing_child(); - return children[i]; + const fnode* c = children[i]; + SPOT_ASSUME(c != nullptr); + return c; } /// \see formula::ff diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 42571f00f..9768dfbfd 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -1026,11 +1026,16 @@ namespace spot bool coacc = false; auto& st = sm->states_of(n); for (auto l: st) - if (namer->get_name(l).accepts_eword()) - { - coacc = true; - break; - } + { + formula lf = namer->get_name(l); + // Somehow gcc 12.2.0 thinks lf can be nullptr. + SPOT_ASSUME(lf != nullptr); + if (lf.accepts_eword()) + { + coacc = true; + break; + } + } if (!coacc) { // ... or if any of its successors is coaccessible. diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index d5b1aacd0..339463426 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -209,9 +209,12 @@ namespace spot if (!rest.empty() && !oblg.empty()) { auto safety = [](formula f) - { - return f.is_syntactic_safety(); - }; + { + // Prevent gcc 12.2.0 from warning us that f could be a + // nullptr formula. + SPOT_ASSUME(f != nullptr); + return f.is_syntactic_safety(); + }; auto i = std::remove_if(oblg.begin(), oblg.end(), safety); rest.insert(rest.end(), i, oblg.end()); oblg.erase(i, oblg.end()); From 2495004afd98b25a2e7b3c95fa2391d51db18a83 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 9 Dec 2022 16:35:05 +0100 Subject: [PATCH 02/21] avoid a g++-12 warning about potential null pointer dereference * spot/twaalgos/determinize.cc (sorted_nodes): Rewrite to avoid reallocation of temporary vector. --- spot/twaalgos/determinize.cc | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index ba4fb3ded..d2d35a824 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -472,15 +472,23 @@ namespace spot std::vector res; for (const auto& n: s.nodes_) { - int brace = n.second; - std::vector tmp; - while (brace >= 0) + // First, count the number of braces. + unsigned nbraces = 0; + for (int brace = n.second; brace >= 0; brace = s.braces_[brace]) + ++nbraces; + // Then list them in reverse order. Since we know the + // number of braces, we can allocate exactly what we need. + if (nbraces > 0) { - // FIXME: is there a smarter way? - tmp.insert(tmp.begin(), brace); - brace = s.braces_[brace]; + std::vector tmp(nbraces, 0); + for (int brace = n.second; brace >= 0; brace = s.braces_[brace]) + tmp[--nbraces] = brace; + res.emplace_back(n.first, std::move(tmp)); + } + else + { + res.emplace_back(n.first, std::vector{}); } - res.emplace_back(n.first, std::move(tmp)); } std::sort(res.begin(), res.end(), compare()); return res; From 9c6fa4921bf3bf7cce496d9b953a612ae4f8a804 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 11 May 2023 21:25:59 +0200 Subject: [PATCH 03/21] debian: add missing build dependencies * debian/control: Add Build-Depends on graphviz, jupyter-nbconvert, doxygen. --- debian/control | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/debian/control b/debian/control index d1f9c652c..e29454c54 100644 --- a/debian/control +++ b/debian/control @@ -2,7 +2,7 @@ Source: spot Section: science Priority: optional Maintainer: Alexandre Duret-Lutz -Build-Depends: debhelper (>= 12), python3-all-dev, ipython3-notebook | python3-ipykernel, ipython3-notebook | python3-nbconvert, libltdl-dev, dh-python +Build-Depends: debhelper (>= 12), python3-all-dev, ipython3-notebook | python3-ipykernel, ipython3-notebook | python3-nbconvert, libltdl-dev, dh-python, graphviz, jupyter-nbconvert, doxygen Standards-Version: 4.5.1 Homepage: http://spot.lrde.epita.fr/ From 75bd595d2877e7e41e331397d7da0d25de772b4f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 12 May 2023 11:32:46 +0200 Subject: [PATCH 04/21] bitvect: work around incorrect warning from gcc * spot/misc/bitvect.hh: Don't free the old ptr if realloc() returns NULL, as this confuse GCC who warns that we are freeing something that has already been freed. Instead, let the ~bitvect() destructor handle this. --- spot/misc/bitvect.hh | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/spot/misc/bitvect.hh b/spot/misc/bitvect.hh index 3588b406e..74ab2bf3f 100644 --- a/spot/misc/bitvect.hh +++ b/spot/misc/bitvect.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2021 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2021, 2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -111,22 +111,22 @@ namespace spot return; if (storage_ == &local_storage_) { - block_t* new_storage_ = static_cast + block_t* new_storage = static_cast (malloc(new_block_count * sizeof(block_t))); + if (SPOT_UNLIKELY(!new_storage)) + throw std::bad_alloc(); for (size_t i = 0; i < block_count_; ++i) - new_storage_[i] = storage_[i]; - storage_ = new_storage_; + new_storage[i] = storage_[i]; + storage_ = new_storage; } else { - auto old = storage_; - storage_ = static_cast - (realloc(old, new_block_count * sizeof(block_t))); - if (!storage_) - { - free(old); - throw std::bad_alloc(); - } + block_t* new_storage = static_cast + (realloc(storage_, new_block_count * sizeof(block_t))); + if (SPOT_UNLIKELY(!new_storage)) + // storage_, untouched, will be freed by the destructor. + throw std::bad_alloc(); + storage_ = new_storage; } block_count_ = new_block_count; } @@ -134,8 +134,8 @@ namespace spot private: void grow() { - size_t new_block_count_ = (block_count_ + 1) * 7 / 5; - reserve_blocks(new_block_count_); + size_t new_block_count = (block_count_ + 1) * 7 / 5; + reserve_blocks(new_block_count); } public: From 330b34e84d4e8b5ad1e93722259b1e0f932e4aac Mon Sep 17 00:00:00 2001 From: Florian Renkin Date: Thu, 4 May 2023 15:28:48 +0200 Subject: [PATCH 05/21] parity_type_to_parity: Add missing cases * spot/twaalgos/toparity.cc: Correct some cases where the solution was not detected. * tests/python/toparity.py: Update tests. --- spot/twaalgos/toparity.cc | 53 ++++++++++++++++++++++++--------------- tests/python/toparity.py | 24 +++++++++++++++++- 2 files changed, 56 insertions(+), 21 deletions(-) diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index c936ef57b..a82c7d57a 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -95,7 +95,8 @@ namespace spot const bool need_equivalent, std::vector &status, std::vector &res_colors, - acc_cond &new_cond, bool &was_able_to_color) + acc_cond &new_cond, bool &was_able_to_color, + unsigned max_col) { auto& ev = aut->edge_vector(); const auto ev_size = ev.size(); @@ -134,7 +135,7 @@ namespace spot kind == cond_kind::INF_PARITY; unsigned max_iter = want_parity ? -1U : 1; - unsigned color = want_parity ? SPOT_MAX_ACCSETS - 1 : 0; + unsigned color = max_col; // Do we want always accepting transitions? // Don't consider CO_BUCHI as it is done by Büchi bool search_inf = kind != cond_kind::FIN_PARITY; @@ -167,14 +168,15 @@ namespace spot auto filter_data = filter_data_t{aut, status}; scc_info si(aut, aut_init, filter, &filter_data, scc_info_options::TRACK_STATES); + if (search_inf) + si.determine_unknown_acceptance(); bool worked = false; unsigned ssc_size = si.scc_count(); for (unsigned scc = 0; scc < ssc_size; ++scc) { // scc_info can detect that we will not be able to find an - // accepting/rejecting cycle. - if (!((search_inf && !si.is_accepting_scc(scc)) || - (!search_inf && !si.is_rejecting_scc(scc)))) + // accepting cycle. + if ((search_inf && si.is_accepting_scc(scc)) || !search_inf) { accepting_transitions_scc(si, scc, cond, {}, not_decidable_transitions, *keep); @@ -224,6 +226,8 @@ namespace spot break; } + new_cond = acc_cond(new_code); + // We check parity if (need_equivalent) { @@ -269,19 +273,19 @@ namespace spot aut->set_acceptance(acc_cond(aut_acc_comp)); } } - new_cond = acc_cond(new_code); + return true; } static twa_graph_ptr cond_type_main(const twa_graph_ptr &aut, const cond_kind kind, - bool &was_able_to_color) + bool &was_able_to_color, unsigned max_color) { std::vector res_colors; std::vector status; acc_cond new_cond; if (cond_type_main_aux(aut, kind, true, status, res_colors, new_cond, - was_able_to_color)) + was_able_to_color, max_color)) { auto res = make_twa_graph(aut, twa::prop_set::all()); auto &res_vector = res->edge_vector(); @@ -311,14 +315,19 @@ namespace spot bool was_able_to_color; // If the automaton is parity-type with a condition that has Inf as // outermost term - auto res = cond_type_main(aut, cond_kind::INF_PARITY, was_able_to_color); + auto res = cond_type_main(aut, cond_kind::INF_PARITY, + was_able_to_color, SPOT_MAX_ACCSETS - 1); // If it was impossible to find an accepting edge, it is perhaps possible // to find a rejecting transition if (res == nullptr && !was_able_to_color) - res = cond_type_main(aut, cond_kind::FIN_PARITY, was_able_to_color); + res = cond_type_main(aut, cond_kind::FIN_PARITY, + was_able_to_color, SPOT_MAX_ACCSETS - 1); if (res) + { + res->prop_state_acc(false); reduce_parity_here(res); + } return res; } @@ -326,14 +335,14 @@ namespace spot buchi_type_to_buchi(const twa_graph_ptr &aut) { bool useless; - return cond_type_main(aut, cond_kind::BUCHI, useless); + return cond_type_main(aut, cond_kind::BUCHI, useless, 0); } twa_graph_ptr co_buchi_type_to_co_buchi(const twa_graph_ptr &aut) { bool useless; - return cond_type_main(aut, cond_kind::CO_BUCHI, useless); + return cond_type_main(aut, cond_kind::CO_BUCHI, useless, 0); } // New version for paritizing @@ -1943,12 +1952,14 @@ namespace spot // Is the maximal color accepting? bool start_inf = true; cond_type_main_aux(sub_aut, cond_kind::INF_PARITY, false, status, - res_colors, new_cond, was_able_to_color); + res_colors, new_cond, was_able_to_color, + SPOT_MAX_ACCSETS - 1); // Otherwise we can try to find a rejecting transition as first step if (!was_able_to_color) { cond_type_main_aux(sub_aut, cond_kind::FIN_PARITY, false, status, - res_colors, new_cond, was_able_to_color); + res_colors, new_cond, was_able_to_color, + SPOT_MAX_ACCSETS - 1); if (!was_able_to_color) return false; start_inf = false; @@ -2127,11 +2138,11 @@ namespace spot bool is_co_bu = false; bool was_able_to_color; if (!cond_type_main_aux(sub_aut, cond_kind::BUCHI, true, status, - res_colors, new_cond, was_able_to_color)) + res_colors, new_cond, was_able_to_color, 0)) { is_co_bu = true; if (!cond_type_main_aux(sub_aut, cond_kind::CO_BUCHI, true, status, - res_colors, new_cond, was_able_to_color)) + res_colors, new_cond, was_able_to_color, 0)) return false; change_to_odd(); } @@ -2172,16 +2183,18 @@ namespace spot acc_cond new_cond; bool was_able_to_color; if (!cond_type_main_aux(sub_aut, cond_kind::INF_PARITY, true, status, - res_colors, new_cond, was_able_to_color)) + res_colors, new_cond, was_able_to_color, + SPOT_MAX_ACCSETS - 3)) { if (!cond_type_main_aux(sub_aut, cond_kind::FIN_PARITY, true, status, - res_colors, new_cond, was_able_to_color)) + res_colors, new_cond, was_able_to_color, + SPOT_MAX_ACCSETS - 3)) return false; } bool is_max, is_odd; new_cond.is_parity(is_max, is_odd); - auto [min, max] = - std::minmax_element(res_colors.begin() + 1, res_colors.end()); + auto min = + std::min_element(res_colors.begin() + 1, res_colors.end()); // cond_type_main_aux returns a parity max condition assert(is_max); auto col_fun = diff --git a/tests/python/toparity.py b/tests/python/toparity.py index ab5fbf314..80c2c19ef 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -547,4 +547,26 @@ State: 9 3 {4} 2 3 {4} 6 --END-- b = spot.iar_maybe(a) tc.assertEqual(b.num_states(), 87) tc.assertTrue(a.equivalent_to(b)) -test(a, [87, 91, 91, 87, 87, 87, 51, 51, 21]) +test(a, [87, 91, 91, 87, 87, 87, 51, 35, 21]) + +a = spot.automaton("""HOA: v1 +States: 4 +Start: 0 +AP: 2 "p0" "p1" +Acceptance: 2 Fin(1) & Fin(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[!0&!1] 2 +[!0&!1] 1 +State: 1 +[!0&1] 0 +[0&1] 3 +State: 2 +[0&!1] 1 +State: 3 {0} +[!0&1] 3 +[!0&!1] 1 +--END--""") +b = spot.parity_type_to_parity(a) +tc.assertTrue(spot.are_equivalent(a, b)) From 47674c0d2f0bd1aa2d0ee98aec79eee08691a727 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 12 Jun 2023 11:01:30 +0200 Subject: [PATCH 06/21] fix spurious failure of ltlcross4.test Reported by Yuri Victorovich. * tests/core/ltlcross4.test: Drop the 'formula' column before computing aggregates. It causes warnings in some Pandas versions, and errors in others. --- tests/core/ltlcross4.test | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/tests/core/ltlcross4.test b/tests/core/ltlcross4.test index b7c85979a..7d124d689 100755 --- a/tests/core/ltlcross4.test +++ b/tests/core/ltlcross4.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012-2014, 2017, 2020 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2012-2014, 2017, 2020, 2023 Laboratoire de Recherche +# et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -54,8 +54,7 @@ x = pandas.read_csv("output.csv") # We used to call describe() instead of agg(), # but the output of this function was changed # in pandas 0.20. -print(x.filter(('formula', 'tool', - 'states', 'transitions')).\ +print(x.filter(('tool', 'states', 'transitions')).\ groupby('tool').\ agg([np.mean, np.std, np.min, np.max])) EOF From adca03a30afd0cd495b5b4b496435bbb67630a48 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 24 Jul 2023 12:16:30 +0200 Subject: [PATCH 07/21] * tests/core/ltlcross4.test: Work around recent Pandas change. --- tests/core/ltlcross4.test | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/tests/core/ltlcross4.test b/tests/core/ltlcross4.test index 7d124d689..f171876a9 100755 --- a/tests/core/ltlcross4.test +++ b/tests/core/ltlcross4.test @@ -65,12 +65,14 @@ $PYTHON test.py >out.1 # remove trailing whitespace from pandas' output, and limit to 6 # lines, because Pandas 0.13 adds the size of the dataframe # afterwards. Alse the spacing between columns differs from version -# to version. -sed 's/[ \t]*$//g;6q' py.out +# to version. The name of the output columns changed from "amin amax" +# to "min max" in some Pandas version (maybe around 2.0). +sed 's/[ \t]*$//g;s/amin/min/g;s/amax/max/g;6q' py.out cat >expected < Date: Mon, 24 Jul 2023 16:56:24 +0200 Subject: [PATCH 08/21] bin: handle thousands of output files Fixes #534. Test case is only on next branch. * bin/common_file.hh, bin/common_file.cc: Make it possible to reopen a closed file. * bin/common_output.cc, bin/common_aoutput.cc: Add a heuristic to decide when to close files. * NEWS: Mention the issue. --- NEWS | 7 +++++++ bin/common_aoutput.cc | 20 ++++++++++++++++++++ bin/common_file.cc | 19 ++++++++++++++++++- bin/common_file.hh | 2 ++ bin/common_output.cc | 20 ++++++++++++++++++++ 5 files changed, 67 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 0b425272f..29cfa7cb1 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,13 @@ New in spot 2.11.5.dev (not yet released) Nothing yet. + Bug fixes: + + - Running command lines such as "autfilt input.hoa -o output-%L.hoa" + where thousands of different filenames can be created failed with + "Too many open files". (Issue #534) + + New in spot 2.11.5 (2023-04-20) Bug fixes: diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 60f83289e..ea44d6c22 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -636,7 +636,27 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, auto [it, b] = outputfiles.try_emplace(fname, nullptr); if (b) it->second.reset(new output_file(fname.c_str())); + else + // reopen if the file has been closed; see below + it->second->reopen_for_append(fname); out = &it->second->ostream(); + + // If we have opened fewer than 10 files, we keep them all open + // to avoid wasting time on open/close calls. + // + // However we cannot keep all files open, especially in + // scenarios were we use thousands of files only once. To keep + // things simple, we only close the previous file if it is not + // the current output. This way we still save the close/open + // cost when consecutive automata are sent to the same file. + static output_file* previous = nullptr; + static const std::string* previous_name = nullptr; + if (previous + && outputfiles.size() > 10 + && &previous->ostream() != out) + previous->close(*previous_name); + previous = it->second.get(); + previous_name = &it->first; } // Output it. diff --git a/bin/common_file.cc b/bin/common_file.cc index 4e56c6d54..ebad8b878 100644 --- a/bin/common_file.cc +++ b/bin/common_file.cc @@ -44,13 +44,30 @@ output_file::output_file(const char* name, bool force_append) os_ = of_.get(); } +void +output_file::reopen_for_append(const std::string& name) +{ + if (of_ && of_->is_open()) // nothing to do + return; + const char* cname = name.c_str(); + if (cname[0] == '>' && cname[1] == '>') + cname += 2; + if (name[0] == '-' && name[1] == 0) + { + os_ = &std::cout; + return; + } + of_->open(cname, std::ios_base::app); + if (!*of_) + error(2, errno, "cannot reopen '%s'", cname); +} void output_file::close(const std::string& name) { // We close of_, not os_, so that we never close std::cout. if (os_) os_->flush(); - if (of_) + if (of_ && of_->is_open()) of_->close(); if (os_ && !*os_) error(2, 0, "error writing to %s", diff --git a/bin/common_file.hh b/bin/common_file.hh index b6aa0bec3..51000d18c 100644 --- a/bin/common_file.hh +++ b/bin/common_file.hh @@ -37,6 +37,8 @@ public: void close(const std::string& name); + void reopen_for_append(const std::string& name); + bool append() const { return append_; diff --git a/bin/common_output.cc b/bin/common_output.cc index 93cb2dfaf..4ab62a9aa 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -420,7 +420,27 @@ output_formula_checked(spot::formula f, spot::process_timer* ptimer, auto [it, b] = outputfiles.try_emplace(fname, nullptr); if (b) it->second.reset(new output_file(fname.c_str())); + else + // reopen if the file has been closed; see below + it->second->reopen_for_append(fname); out = &it->second->ostream(); + + // If we have opened fewer than 10 files, we keep them all open + // to avoid wasting time on open/close calls. + // + // However we cannot keep all files open, especially in + // scenarios were we use thousands of files only once. To keep + // things simple, we only close the previous file if it is not + // the current output. This way we still save the close/open + // cost when consecutive formulas are sent to the same file. + static output_file* previous = nullptr; + static const std::string* previous_name = nullptr; + if (previous + && outputfiles.size() > 10 + && &previous->ostream() != out) + previous->close(*previous_name); + previous = it->second.get(); + previous_name = &it->first; } output_formula(*out, f, ptimer, filename, linenum, prefix, suffix); *out << output_terminator; From 090dcf17eb7c45ce42cef6d34dcb9d77dbd204b2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 26 Jul 2023 16:17:31 +0200 Subject: [PATCH 09/21] work around spurious GCC 13 warnings * spot/graph/graph.hh (new_univ_dests): Add an overload taking a temporary vector. * spot/twa/twagraph.cc (defrag_states): Use it. * tests/core/parity.cc: Remove some temporary variables. --- spot/graph/graph.hh | 11 ++++++++++- spot/twa/twagraph.cc | 5 ++--- tests/core/parity.cc | 16 +++++++--------- 3 files changed, 19 insertions(+), 13 deletions(-) diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index 04c21fec9..d2a97d1c5 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2018, 2020-2022 Laboratoire de Recherche et +// Copyright (C) 2014-2018, 2020-2023 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -576,6 +576,15 @@ namespace spot return p.first->second; } + unsigned new_univ_dests(std::vector&& tmp) + { + std::sort(tmp.begin(), tmp.end()); + tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end()); + auto p = uniq_.emplace(tmp, 0); + if (p.second) + p.first->second = g_.new_univ_dests(tmp.begin(), tmp.end()); + return p.first->second; + } }; } // namespace internal diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 2a72702f3..055d6ca11 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2023 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -1243,8 +1243,7 @@ namespace spot // the state so that graph::degrag_states() will // eventually update it to the correct value. nd = newst.size(); - newst.emplace_back(uniq.new_univ_dests(tmp.begin(), - tmp.end())); + newst.emplace_back(uniq.new_univ_dests(std::move(tmp))); } } in_dst = nd; diff --git a/tests/core/parity.cc b/tests/core/parity.cc index 4cb8256ef..7ff391745 100644 --- a/tests/core/parity.cc +++ b/tests/core/parity.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016, 2018-2019 Laboratoire de Recherche et +// Copyright (C) 2016, 2018-2019, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -320,16 +320,14 @@ int main() for (auto acc_tuple: acceptance_sets) for (auto& aut_tuple: automata_tuples) { - auto& aut = aut_tuple.first; - auto aut_num_sets = aut_tuple.second; - - auto acc = std::get<0>(acc_tuple); - auto is_max = std::get<1>(acc_tuple); - auto is_odd = std::get<2>(acc_tuple); - auto acc_num_sets = std::get<3>(acc_tuple); + spot::twa_graph_ptr& aut = aut_tuple.first; + unsigned aut_num_sets = aut_tuple.second; + unsigned acc_num_sets = std::get<3>(acc_tuple); if (aut_num_sets <= acc_num_sets) { - aut->set_acceptance(acc_num_sets, acc); + bool is_max = std::get<1>(acc_tuple); + bool is_odd = std::get<2>(acc_tuple); + aut->set_acceptance(acc_num_sets, std::get<0>(acc_tuple)); // Check change_parity for (auto kind: parity_kinds) for (auto style: parity_styles) From 8065759fbd3ef9164094bdced28bd4e7623583e4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 26 Jul 2023 16:19:35 +0200 Subject: [PATCH 10/21] * HACKING: Mention the svgo version we use. --- HACKING | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HACKING b/HACKING index f2cf27e8c..8029fe6db 100644 --- a/HACKING +++ b/HACKING @@ -55,7 +55,7 @@ only for certain operations (like releases): pandoc used during Debian packaging for the conversion of IPython notebooks to html svgo for reducing SVG images before generating the tarball - (install with: npm install -g svgo) + (install with: npm install -g svgo@1.3.2) ltl2ba used in the generated documentation and the test suite ltl2dstar likewise ltl3dra likewise From 69b9ffef9a086533bb2386f144eb41c69e78f5aa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 26 Jul 2023 21:33:36 +0200 Subject: [PATCH 11/21] bin: fix handling for --output & --format with LTL outputs * bin/common_output.cc: Set the output stream for LTL formats. --- NEWS | 3 +++ bin/common_output.cc | 3 ++- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 29cfa7cb1..5691c96ea 100644 --- a/NEWS +++ b/NEWS @@ -8,6 +8,9 @@ New in spot 2.11.5.dev (not yet released) where thousands of different filenames can be created failed with "Too many open files". (Issue #534) + - Using --format=... on a tool that output formulas would force + the output on standard output, even when --output was given. + New in spot 2.11.5 (2023-04-20) diff --git a/bin/common_output.cc b/bin/common_output.cc index 4ab62a9aa..13b4daf0f 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -224,7 +224,7 @@ namespace } }; - class formula_printer final: protected spot::formater + class formula_printer final: public spot::formater { public: formula_printer(std::ostream& os, const char* format) @@ -392,6 +392,7 @@ output_formula(std::ostream& out, else { formula_with_location fl = { f, filename, linenum, prefix, suffix }; + format->set_output(out); format->print(fl, ptimer); } } From e548bf0a8e0a2a9967ff58f56a6043c7b28bc4d7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 26 Jul 2023 23:00:24 +0200 Subject: [PATCH 12/21] acc: remove some dead functions * spot/twa/acc.hh, spot/twa/acc.cc (has_parity_prefix, is_parity_max_equiv): Remove. * spot/twa/acc.hh, spot/twa/twagraph.cc, spot/twa/twagraph.hh (apply_permutation): Remove. --- spot/twa/acc.cc | 180 ------------------------------------------- spot/twa/acc.hh | 81 ------------------- spot/twa/twagraph.cc | 9 --- spot/twa/twagraph.hh | 4 +- 4 files changed, 1 insertion(+), 273 deletions(-) diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 07aac36f9..732ea124c 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1067,81 +1067,6 @@ namespace spot return res; } - namespace - { - bool - has_parity_prefix_aux(acc_cond original, - acc_cond &new_cond, - std::vector &colors, - std::vector elements, - acc_cond::acc_op op) - { - if (elements.size() > 2) - { - new_cond = original; - return false; - } - if (elements.size() == 2) - { - unsigned pos = (elements[1].back().sub.op == op - && elements[1][0].mark.is_singleton()); - if (!(elements[0].back().sub.op == op || pos)) - { - new_cond = original; - return false; - } - if ((elements[1 - pos].used_sets() & elements[pos][0].mark)) - { - new_cond = original; - return false; - } - if (!elements[pos][0].mark.is_singleton()) - { - return false; - } - colors.push_back(elements[pos][0].mark.min_set() - 1); - elements[1 - pos].has_parity_prefix(new_cond, colors); - return true; - } - return false; - } - } - - bool - acc_cond::acc_code::has_parity_prefix(acc_cond &new_cond, - std::vector &colors) const - { - auto disj = top_disjuncts(); - if (!(has_parity_prefix_aux((*this), new_cond, colors, - disj, acc_cond::acc_op::Inf) || - has_parity_prefix_aux((*this), new_cond, colors, - top_conjuncts(), acc_cond::acc_op::Fin))) - new_cond = acc_cond((*this)); - return disj.size() == 2; - } - - bool - acc_cond::has_parity_prefix(acc_cond& new_cond, - std::vector& colors) const - { - return code_.has_parity_prefix(new_cond, colors); - } - - bool - acc_cond::is_parity_max_equiv(std::vector&permut, bool even) const - { - if (code_.used_once_sets() != code_.used_sets()) - return false; - bool result = code_.is_parity_max_equiv(permut, 0, even); - int max_value = *std::max_element(std::begin(permut), std::end(permut)); - for (unsigned i = 0; i < permut.size(); ++i) - if (permut[i] != -1) - permut[i] = max_value - permut[i]; - else - permut[i] = i; - return result; - } - bool acc_cond::is_parity(bool& max, bool& odd, bool equiv) const { unsigned sets = num_; @@ -1408,111 +1333,6 @@ namespace spot return patterns; } - bool - acc_cond::acc_code::is_parity_max_equiv(std::vector& permut, - unsigned new_color, - bool even) const - { - auto conj = top_conjuncts(); - auto disj = top_disjuncts(); - if (conj.size() == 1) - { - if (disj.size() == 1) - { - acc_cond::acc_code elem = conj[0]; - if ((even && elem.back().sub.op == acc_cond::acc_op::Inf) - || (!even && elem.back().sub.op == acc_cond::acc_op::Fin)) - { - for (auto color : disj[0][0].mark.sets()) - { - if (permut[color] != -1 - && ((unsigned) permut[color]) != new_color) - return false; - permut[color] = new_color; - } - return true; - } - return false; - } - else - { - std::sort(disj.begin(), disj.end(), - [](acc_code c1, acc_code c2) - { - return (c1 != c2) && - c1.back().sub.op == acc_cond::acc_op::Inf; - }); - unsigned i = 0; - for (; i < disj.size() - 1; ++i) - { - if (disj[i].back().sub.op != acc_cond::acc_op::Inf - || !disj[i][0].mark.is_singleton()) - return false; - for (auto color : disj[i][0].mark.sets()) - { - if (permut[color] != -1 - && ((unsigned) permut[color]) != new_color) - return false; - permut[color] = new_color; - } - } - if (disj[i].back().sub.op == acc_cond::acc_op::Inf) - { - if (!even || !disj[i][0].mark.is_singleton()) - return false; - for (auto color : disj[i][0].mark.sets()) - { - if (permut[color] != -1 - && ((unsigned) permut[color]) != new_color) - return false; - permut[color] = new_color; - } - return true; - } - return disj[i].is_parity_max_equiv(permut, new_color + 1, even); - } - } - else - { - std::sort(conj.begin(), conj.end(), - [](acc_code c1, acc_code c2) - { - return (c1 != c2) - && c1.back().sub.op == acc_cond::acc_op::Fin; - }); - unsigned i = 0; - for (; i < conj.size() - 1; i++) - { - if (conj[i].back().sub.op != acc_cond::acc_op::Fin - || !conj[i][0].mark.is_singleton()) - return false; - for (auto color : conj[i][0].mark.sets()) - { - if (permut[color] != -1 && permut[color != new_color]) - return false; - permut[color] = new_color; - } - } - if (conj[i].back().sub.op == acc_cond::acc_op::Fin) - { - if (even) - return 0; - if (!conj[i][0].mark.is_singleton()) - return false; - for (auto color : conj[i][0].mark.sets()) - { - if (permut[color] != -1 && permut[color != new_color]) - return false; - permut[color] = new_color; - } - return true; - } - - return conj[i].is_parity_max_equiv(permut, new_color + 1, even); - } - } - - namespace { template diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 1c460cfc4..aed1b3a2a 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -60,11 +60,6 @@ namespace spot /// could be removed.) class SPOT_API acc_cond { - - public: - bool - has_parity_prefix(acc_cond& new_acc, std::vector& colors) const; - #ifndef SWIG private: [[noreturn]] static void report_too_many_sets(); @@ -102,10 +97,6 @@ namespace spot /// Initialize an empty mark_t. mark_t() = default; - mark_t - apply_permutation(std::vector permut); - - #ifndef SWIG /// Create a mark_t from a range of set numbers. template @@ -489,15 +480,6 @@ namespace spot acc_code unit_propagation(); - bool - has_parity_prefix(acc_cond& new_cond, - std::vector& colors) const; - - bool - is_parity_max_equiv(std::vector& permut, - unsigned new_color, - bool even) const; - bool operator==(const acc_code& other) const { unsigned pos = size(); @@ -1793,8 +1775,6 @@ namespace spot bool is_parity(bool& max, bool& odd, bool equiv = false) const; - bool is_parity_max_equiv(std::vector& permut, bool even) const; - /// \brief check is the acceptance condition matches one of the /// four type of parity acceptance defined in the HOA format. bool is_parity() const @@ -1976,57 +1956,6 @@ namespace spot return all_; } - acc_cond - apply_permutation(std::vectorpermut) - { - return acc_cond(apply_permutation_aux(permut)); - } - - acc_code - apply_permutation_aux(std::vectorpermut) - { - auto conj = top_conjuncts(); - auto disj = top_disjuncts(); - - if (conj.size() > 1) - { - auto transformed = std::vector(); - for (auto elem : conj) - transformed.push_back(elem.apply_permutation_aux(permut)); - std::sort(transformed.begin(), transformed.end()); - auto uniq = std::unique(transformed.begin(), transformed.end()); - auto result = std::accumulate(transformed.begin(), uniq, acc_code::t(), - [](acc_code c1, acc_code c2) - { - return c1 & c2; - }); - return result; - } - else if (disj.size() > 1) - { - auto transformed = std::vector(); - for (auto elem : disj) - transformed.push_back(elem.apply_permutation_aux(permut)); - std::sort(transformed.begin(), transformed.end()); - auto uniq = std::unique(transformed.begin(), transformed.end()); - auto result = std::accumulate(transformed.begin(), uniq, acc_code::f(), - [](acc_code c1, acc_code c2) - { - return c1 | c2; - }); - return result; - } - else - { - if (code_.back().sub.op == acc_cond::acc_op::Fin) - return fin(code_[0].mark.apply_permutation(permut)); - if (code_.back().sub.op == acc_cond::acc_op::Inf) - return inf(code_[0].mark.apply_permutation(permut)); - } - SPOT_ASSERT(false); - return {}; - } - /// \brief Check whether visiting *exactly* all sets \a inf /// infinitely often satisfies the acceptance condition. bool accepting(mark_t inf) const @@ -2473,16 +2402,6 @@ namespace spot { return {*this}; } - - inline acc_cond::mark_t - acc_cond::mark_t::apply_permutation(std::vector permut) - { - mark_t result { }; - for (auto color : sets()) - if (color < permut.size()) - result.set(permut[color]); - return result; - } } namespace std diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 055d6ca11..3f74d4d99 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -108,15 +108,6 @@ namespace namespace spot { - void - twa_graph::apply_permutation(std::vector permut) - { - for (auto& e : edges()) - { - e.acc.apply_permutation(permut); - } - } - std::string twa_graph::format_state(unsigned n) const { if (is_univ_dest(n)) diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 742a4d69a..1540692c6 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2023 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -220,8 +220,6 @@ namespace spot public: - void apply_permutation(std::vector permut); - twa_graph(const bdd_dict_ptr& dict) : twa(dict), init_number_(0) From 531252119ccc88fb1088ae4cad085fd4a187cf5f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 26 Jul 2023 23:57:12 +0200 Subject: [PATCH 13/21] aiger: order the inputs of binary AND gates * spot/twaalgos/aiger.cc: Here. * tests/core/ltlsynt.test: Adjust, and add test case for aiger=optim. --- spot/twaalgos/aiger.cc | 30 +++++++++++++++--------------- tests/core/ltlsynt.test | 8 ++++++-- 2 files changed, 21 insertions(+), 17 deletions(-) diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index af255a167..6b608dd59 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -552,20 +552,20 @@ namespace spot assert(var2bdd_.count(v1)); assert(var2bdd_.count(v2)); - if (v1 != v2) - { - bdd b = var2bdd_[v1] & var2bdd_[v2]; - auto [it, inserted] = bdd2var_.try_emplace(b.id(), 0); - if (!inserted) - return it->second; - max_var_ += 2; - it->second = max_var_; - and_gates_.emplace_back(v1, v2); - register_new_lit_(max_var_, b); - return max_var_; - } - else - return v1; + if (SPOT_UNLIKELY(v1 > v2)) + std::swap(v1, v2); + if (SPOT_UNLIKELY(v1 == v2)) + return v1; + + bdd b = var2bdd_[v1] & var2bdd_[v2]; + auto [it, inserted] = bdd2var_.try_emplace(b.id(), 0); + if (!inserted) + return it->second; + max_var_ += 2; + it->second = max_var_; + and_gates_.emplace_back(v1, v2); + register_new_lit_(max_var_, b); + return max_var_; } unsigned aig::aig_and(std::vector& vs) diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 4a7595539..02d248754 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017, 2019-2022 Laboratoire de Recherche et +# Copyright (C) 2017, 2019-2023 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -160,6 +160,10 @@ ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \ --algo=ds --simplify=no --aiger=isop >out diff out exp +ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \ + --algo=ds --simplify=no --aiger=optim >out +diff out exp + cat >exp < Date: Thu, 27 Jul 2023 09:48:00 +0200 Subject: [PATCH 14/21] tests: add some test to cover autcross' univ-edges removal * tests/core/ltl3ba.test: Here. --- tests/core/ltl3ba.test | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/tests/core/ltl3ba.test b/tests/core/ltl3ba.test index fdcebc926..acc68a2c5 100755 --- a/tests/core/ltl3ba.test +++ b/tests/core/ltl3ba.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016-2018, 2021 Laboratoire de Recherche et +# Copyright (C) 2016-2018, 2021, 2023 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -47,8 +47,10 @@ GF(((a & Xb) | XXc) & Xd) GF((b | Fa) & (b R Xb)) EOF randltl -n 30 2 -) | ltlcross -D 'ltl3ba -H1' 'ltl3ba -H2' 'ltl3ba -H3' ltl2tgba \ - --ambiguous --strength --csv=output.csv +) > file.ltl + +ltlcross -F file.ltl -D 'ltl3ba -H1' 'ltl3ba -H2' 'ltl3ba -H3' ltl2tgba \ + --ambiguous --strength --verbose --csv=output.csv grep _x output.csv && exit 1 @@ -59,6 +61,9 @@ while read l; do test "x$first" = "x$l" || exit 1 done) +ltldo 'ltl3ba -H1' -F file.ltl | + autcross --language-complemented 'autfilt --dualize' --verbose + # The name of the HOA is preserved case `ltldo 'ltl3ba -H' -f xxx --stats=%m` in *xxx*);; From 15857385a5a53d0d03a9a5c4a2891cbf4836adf5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 27 Jul 2023 10:23:33 +0200 Subject: [PATCH 15/21] bin: cover more tmpfile failure when running as root * tests/core/ltlcross5.test: reorganize to test missing directory before permission issues, as the latter cannot be run as root. --- tests/core/ltlcross5.test | 36 +++++++++++++++++++----------------- 1 file changed, 19 insertions(+), 17 deletions(-) diff --git a/tests/core/ltlcross5.test b/tests/core/ltlcross5.test index 82e9fdc89..c89a7bd0b 100644 --- a/tests/core/ltlcross5.test +++ b/tests/core/ltlcross5.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2019, 2023 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -24,10 +24,22 @@ set -e unset TMPDIR unset SPOT_TMPDIR +err=0 + +SPOT_TMPDIR=bar ltlcross ltl2tgba -f GFa 2>err && err=1 +cat err +grep 'failed to create temporary file' err +grep 'Note that the directory.*SPOT_TMPDIR ' err + +TMPDIR=bar ltlcross ltl2tgba -f GFa 2>err && err=2 +cat err +grep 'failed to create temporary file' err +grep 'Note that the directory.* TMPDIR ' err + + mkdir foo chmod a-w foo cd foo -err=0 if touch bar; then # We are likely running as root, so we cannot detect permission # issues. @@ -39,27 +51,17 @@ fi ltlcross ltl2tgba -f GFa 2>../err && err=1 cd .. cat err -grep 'failed to create temporary file' err || err=1 -grep 'executing this from a writable' err || err=1 +grep 'failed to create temporary file' err || err=3 +grep 'executing this from a writable' err || err=3 grep 'SPOT_TMPDIR' err || err=1 -SPOT_TMPDIR=foo ltlcross ltl2tgba -f GFa 2>err && err=2 +SPOT_TMPDIR=foo ltlcross ltl2tgba -f GFa 2>err && err=4 cat err -grep 'failed to create temporary file' err || err=2 -grep 'executing this from a writable' err && err=2 +grep 'failed to create temporary file' err || err=4 +grep 'executing this from a writable' err && err=4 grep 'SPOT_TMPDIR' err chmod a+w foo rmdir foo -SPOT_TMPDIR=bar ltlcross ltl2tgba -f GFa 2>err && err=3 -cat err -grep 'failed to create temporary file' err -grep 'Note that the directory.*SPOT_TMPDIR ' err - -TMPDIR=bar ltlcross ltl2tgba -f GFa 2>err && err=4 -cat err -grep 'failed to create temporary file' err -grep 'Note that the directory.* TMPDIR ' err - exit $err From 44d9e34e324629a8483d9b08209113763bc3ac5c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 27 Jul 2023 14:28:15 +0200 Subject: [PATCH 16/21] improve coverage of LaTeX/utf8 printers for SERE * bin/common_output.cc, bin/common_output.hh, bin/randltl.cc: Adjust so that running "randltl -S" use the SERE flavor of the spot/latex/utf8 formula printers. * tests/core/latex.test, tests/core/utf8.test, tests/python/ltlparse.py: Add more test cases. --- NEWS | 2 ++ bin/common_output.cc | 16 +++++++++++++--- bin/common_output.hh | 1 + bin/randltl.cc | 1 + tests/core/latex.test | 7 ++++--- tests/core/utf8.test | 17 ++++++++++++++++- tests/python/ltlparse.py | 18 +++++++++++++++++- 7 files changed, 54 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 5691c96ea..609805130 100644 --- a/NEWS +++ b/NEWS @@ -11,6 +11,8 @@ New in spot 2.11.5.dev (not yet released) - Using --format=... on a tool that output formulas would force the output on standard output, even when --output was given. + - Using "randltl -S" did not correctly go through the SERE printer + functions. New in spot 2.11.5 (2023-04-20) diff --git a/bin/common_output.cc b/bin/common_output.cc index 13b4daf0f..11d0da80e 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -45,6 +45,7 @@ output_format_t output_format = spot_output; bool full_parenth = false; bool escape_csv = false; char output_terminator = '\n'; +bool output_ratexp = false; static const argp_option options[] = { @@ -105,7 +106,10 @@ stream_formula(std::ostream& out, report_not_ltl(f, filename, linenum, "LBT"); break; case spot_output: - spot::print_psl(out, f, full_parenth); + if (output_ratexp) + spot::print_sere(out, f, full_parenth); + else + spot::print_psl(out, f, full_parenth); break; case spin_output: if (f.is_ltl_formula()) @@ -120,10 +124,16 @@ stream_formula(std::ostream& out, report_not_ltl(f, filename, linenum, "Wring"); break; case utf8_output: - spot::print_utf8_psl(out, f, full_parenth); + if (output_ratexp) + spot::print_utf8_sere(out, f, full_parenth); + else + spot::print_utf8_psl(out, f, full_parenth); break; case latex_output: - spot::print_latex_psl(out, f, full_parenth); + if (output_ratexp) + spot::print_latex_sere(out, f, full_parenth); + else + spot::print_latex_psl(out, f, full_parenth); break; case count_output: case quiet_output: diff --git a/bin/common_output.hh b/bin/common_output.hh index 1cff67229..1661929b9 100644 --- a/bin/common_output.hh +++ b/bin/common_output.hh @@ -36,6 +36,7 @@ enum output_format_t { spot_output, spin_output, utf8_output, extern output_format_t output_format; extern bool full_parenth; extern bool escape_csv; +extern bool output_ratexp; #define COMMON_X_OUTPUT_SPECS(where) \ "number of atomic propositions " #where "; " \ diff --git a/bin/randltl.cc b/bin/randltl.cc index 749fcf373..6f672f092 100644 --- a/bin/randltl.cc +++ b/bin/randltl.cc @@ -180,6 +180,7 @@ parse_opt(int key, char* arg, struct argp_state* as) break; case 'S': output = spot::randltlgenerator::SERE; + output_ratexp = true; break; case OPT_BOOLEAN_PRIORITIES: opt_pB = arg; diff --git a/tests/core/latex.test b/tests/core/latex.test index 6e94e14d6..61eeab993 100755 --- a/tests/core/latex.test +++ b/tests/core/latex.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2013, 2015, 2023 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -50,7 +50,8 @@ cat <<\EOF EOF ( ltlfilt --latex input --format='\texttt{%F:%L} & $%f$ \\'; genltl --go-theta=1..3 --latex \ - --format='\texttt{--%F:%L} & $%f$ \\') + --format='\texttt{--%F:%L} & $%f$ \\'; + randltl -S -n10 --latex 2 --format='\texttt{random %L} & $%f$ \\') cat <<\EOF \end{tabular} \end{document} diff --git a/tests/core/utf8.test b/tests/core/utf8.test index 45ba950f5..b0bfef043 100755 --- a/tests/core/utf8.test +++ b/tests/core/utf8.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012, 2013, 2015, 2016, 2019 Laboratoire de Recherche et +# Copyright (C) 2012, 2013, 2015, 2016, 2019, 2023 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -70,3 +70,18 @@ ltlfilt -8 -f 'X[!]a' >out diff in out ltlfilt -8 -F in >out diff in out + +randltl --sere -8 --seed 0 --tree-size 8 a b c -n 10 > formulae +cat >expected <3]') +tc.assertEqual(spot.str_sere(pf.f), 'a[->3]') +tc.assertEqual(spot.str_latex_sere(pf.f), 'a\\SereGoto{3}') +pf = spot.parse_infix_sere('(!b)[*];b;(!b)[*]') +tc.assertEqual(spot.str_sere(pf.f), 'b[=1]') +pf = spot.parse_infix_sere('b[=1]') +tc.assertEqual(spot.str_sere(pf.f), 'b[=1]') +tc.assertEqual(spot.str_latex_sere(pf.f), 'b\\SereEqual{1}') +tc.assertEqual(spot.str_sclatex_sere(pf.f), 'b^{=1}') +pf = spot.parse_infix_sere('(!b)[*];b') +tc.assertEqual(spot.str_sere(pf.f), 'b[->]') +pf = spot.parse_infix_sere('b[->1]') +tc.assertEqual(spot.str_latex_sere(pf.f), 'b\\SereGoto{}') +tc.assertEqual(spot.str_sclatex_sere(pf.f), 'b^{\\to}') From de7d5a956fe2ec6968283f5194bb27a6d8ded576 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 28 Jul 2023 16:20:18 +0200 Subject: [PATCH 17/21] * .gitlab-ci.yml: temporary disable raspbian. --- .gitlab-ci.yml | 42 +++++++++++++++++++++++------------------- 1 file changed, 23 insertions(+), 19 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 348bacba1..424f7bc21 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -458,22 +458,26 @@ publish-unstable: - curl -X POST -F ref=master -F token=$TRIGGER_SPOT_WEB -F "variables[spot_branch]=next" https://gitlab.lre.epita.fr/api/v4/projects/131/trigger/pipeline - curl -X POST -F ref=master -F token=$TRIGGER_SANDBOX https://gitlab.lre.epita.fr/api/v4/projects/181/trigger/pipeline -raspbian: - stage: build - only: - - branches - except: - - /wip/ - tags: - - armv7 - script: - - autoreconf -vfi - - ./configure - - make - - make distcheck || { chmod -R u+w ./spot-*; false; } - artifacts: - when: always - paths: - - ./spot-*/_build/sub/tests/*/*.log - - ./*.log - - ./*.tar.gz + +# The SD card of our Raspberry failed. Disable this job until we +# can make it work again. +# +# raspbian: +# stage: build +# only: +# - branches +# except: +# - /wip/ +# tags: +# - armv7 +# script: +# - autoreconf -vfi +# - ./configure +# - make +# - make distcheck || { chmod -R u+w ./spot-*; false; } +# artifacts: +# when: always +# paths: +# - ./spot-*/_build/sub/tests/*/*.log +# - ./*.log +# - ./*.tar.gz From e37bc9e1ae1935f81196c31e62cb8888026f8493 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 31 Jul 2023 21:07:07 +0200 Subject: [PATCH 18/21] [buddy] fix cache index of bdd_forall Fix a 20 year old typo that caused a bug reported by Guillermo Perez. * src/bddop.c (bdd_forall, bdd_forallcomp): Fix the cache index. --- buddy/src/bddop.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c index f54a39442..fd62ed9b8 100644 --- a/buddy/src/bddop.c +++ b/buddy/src/bddop.c @@ -2300,7 +2300,7 @@ RETURN {* The quantified BDD. *} */ BDD bdd_forall(BDD r, BDD var) { - return quantify(r, var, bddop_and, 0, CACHEID_EXIST); + return quantify(r, var, bddop_and, 0, CACHEID_FORALL); } /* @@ -2315,7 +2315,7 @@ RETURN {* The quantified BDD. *} */ BDD bdd_forallcomp(BDD r, BDD var) { - return quantify(r, var, bddop_and, 1, CACHEID_EXISTC); + return quantify(r, var, bddop_and, 1, CACHEID_FORALLC); } From bb95705d5251e97af646ada29b86cd986507a638 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 31 Jul 2023 21:11:39 +0200 Subject: [PATCH 19/21] mention the bug fixed in BuDDy * NEWS: Explain the bug fixed in previous patch and reported in issue #535. * THANKS: Add Guillermo. --- NEWS | 5 +++++ THANKS | 1 + 2 files changed, 6 insertions(+) diff --git a/NEWS b/NEWS index 609805130..888a05da4 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,11 @@ New in spot 2.11.5.dev (not yet released) - Using "randltl -S" did not correctly go through the SERE printer functions. + - Our copy of BuDDy's bdd_forall() had a 20 year old typo that + caused cache entries from bdd_exist() and bdd_forall() to be + mixed. Spot was safe from this bug because it was only using + bdd_exist(). (Issue #535) + New in spot 2.11.5 (2023-04-20) Bug fixes: diff --git a/THANKS b/THANKS index 93155f9d1..7986c3875 100644 --- a/THANKS +++ b/THANKS @@ -21,6 +21,7 @@ Felix Klaedtke Florian Perlié-Long František Blahoudek Gerard J. Holzmann +Guillermo A. Perez Hashim Ali Heikki Tauriainen Henrich Lauko From f4b397a2bfbcf171e6b2ef9c663b34f92d122616 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 1 Aug 2023 12:19:47 +0200 Subject: [PATCH 20/21] Release Spot 2.11.6 * NEWS, configure.ac, doc/org/setup.org: Update version. --- NEWS | 6 +++--- configure.ac | 2 +- doc/org/setup.org | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index 888a05da4..986e1be91 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,4 @@ -New in spot 2.11.5.dev (not yet released) - - Nothing yet. +New in spot 2.11.6 (2023-08-01) Bug fixes: @@ -19,6 +17,8 @@ New in spot 2.11.5.dev (not yet released) mixed. Spot was safe from this bug because it was only using bdd_exist(). (Issue #535) + - Work around recent Pandas and GCC changes. + New in spot 2.11.5 (2023-04-20) Bug fixes: diff --git a/configure.ac b/configure.ac index 09fe45364..9bfa98eac 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.11.5.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.11.6], [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 255a01c3d..772ff2cc0 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 2023-04-20 +#+MACRO: LASTDATE 2023-08-01 #+NAME: SPOT_VERSION #+BEGIN_SRC python :exports none :results value :wrap org -return "2.11.5" +return "2.11.6" #+END_SRC #+NAME: TARBALL_LINK From 41751b80a175e5110dae966a4c1399e87b94931c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 1 Aug 2023 14:22:32 +0200 Subject: [PATCH 21/21] * NEWS, configure.ac: Bump version to 2.11.6.dev. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 986e1be91..455c4825b 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.11.6.dev (not yet released) + + Nothing yet. + New in spot 2.11.6 (2023-08-01) Bug fixes: diff --git a/configure.ac b/configure.ac index 9bfa98eac..41261d84c 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.11.6], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.11.6.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])