From 3820f369b0dcf5ee9a357b7fda2652de58fd8330 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 4 Mar 2020 16:41:23 +0100 Subject: [PATCH 1/9] genem: fix suboptimal selection of Fin to remove * spot/twaalgos/genem.cc: If a disjunct has no unit-Fin to remove the code should select any Fin occuring in the disjunct, but it was selecting any Fin occuring in the acceptance condition (made of disjuncts) instead. This could potentially double the number of recursive calls. --- spot/twaalgos/genem.cc | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index c4e541f72..3d8383843 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2019 Laboratoire de Recherche et Developpement +// Copyright (C) 2017-2020 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -74,9 +74,7 @@ namespace spot } else { - int fo = acc.fin_one(); - if (fo < 0) - std::cerr << autacc << acc << '\n'; + int fo = disjunct.fin_one(); assert(fo >= 0); // Try to accept when Fin(fo) == true acc_cond::mark_t fo_m = {(unsigned) fo}; From fa90a97d54fb9cad53a1b09597a649dd35661c0a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 4 Mar 2020 23:22:21 +0100 Subject: [PATCH 2/9] org: fix some typos * doc/org/tut12.org: Here. --- doc/org/tut12.org | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/doc/org/tut12.org b/doc/org/tut12.org index 1a77dc74f..b91b6da70 100644 --- a/doc/org/tut12.org +++ b/doc/org/tut12.org @@ -20,7 +20,7 @@ However there is a trick we can use in case we want to use Spot to build a finite automaton that recognize some LTLf (i.e. LTL with finite semantics) property. The plan is as follows: -1. Have Spot read the input formula as if it were LTL. +1. Have Spot read the input LTLf formula as if it was LTL. 2. Rewrite this formula in a way that embeds the semantics of LTLf in LTL. First, introduce a new atomic proposition =alive= that will be true initially, but that will eventually become false forever. @@ -62,7 +62,7 @@ initially, as required in the first paper... * Shell version -The first four steps of the the above sequence of operations can be +The first four steps of the above sequence of operations can be executed as follows. Transforming LTLf to LTL can be done using [[file:ltlfilt.org][=ltlfilt=]]'s =--from-ltlf= option, translating the resulting formula into a Büchi automaton is obviously done with [[file:ltl2tgba.org][=ltl2tgba=]], and removing @@ -159,6 +159,10 @@ State: 3 {0} --END-- #+end_example +If you need to print the automaton in a custom format (some finite +automaton format probably), you should check our example of [[file:tut21.org][custom +print of an automaton]]. + * C++ version The C++ version is straightforward adaptation of the Python version. @@ -226,9 +230,12 @@ State: 3 {0} --END-- #+end_example -* Final note +Again, please check our example of [[file:tut21.org][custom print of an automaton]] if you +need to print in some format for NFA/DFA. -Spots only deal with infinite behaviors, so if you plan to use Spot to +* Final notes + +Spot only deals with infinite behaviors, so if you plan to use Spot to perform some LTLf model checking, you should stop at step 3. Keep the =alive= proposition in your property automaton, and also add it to the Kripke structure representing your system. From 5b8dbc654983eb2326fb221ac1e870713c94d28e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 6 Mar 2020 23:23:13 +0100 Subject: [PATCH 3/9] product: fix handling of operand with false acceptance * NEWS: Mention the issue. * spot/twaalgos/product.cc: Fix it. * tests/python/prodexpt.py: Test it. --- NEWS | 7 ++++++ spot/twaalgos/product.cc | 49 +++++++++++++++++++++++++++------------- tests/python/prodexpt.py | 35 ++++++++++++++++++++++++++-- 3 files changed, 73 insertions(+), 18 deletions(-) diff --git a/NEWS b/NEWS index 96e9a68fa..f4a991052 100644 --- a/NEWS +++ b/NEWS @@ -2,6 +2,13 @@ New in spot 2.8.6.dev (not yet released) Nothing yet. + Bugs fixed: + + - Building a product between two complete automata where one operand + had false acceptance could create a incomplete automaton + incorrectly tagged as complete, causing the print_hoa() function + to raise an exception. + New in spot 2.8.6 (2020-02-19) Bugs fixed: diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc index f68192d15..84efbcf32 100644 --- a/spot/twaalgos/product.cc +++ b/spot/twaalgos/product.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -285,21 +285,34 @@ namespace spot if (!res) // aborted return nullptr; - // The product of two non-deterministic automata could be - // deterministic. Likewise for non-complete automata. - if (left->prop_universal() && right->prop_universal()) - res->prop_universal(true); - if (left->prop_complete() && right->prop_complete()) - res->prop_complete(true); - if (left->prop_stutter_invariant() && right->prop_stutter_invariant()) - res->prop_stutter_invariant(true); - if (left->prop_inherently_weak() && right->prop_inherently_weak()) - res->prop_inherently_weak(true); - if (left->prop_weak() && right->prop_weak()) - res->prop_weak(true); - if (left->prop_terminal() && right->prop_terminal()) - res->prop_terminal(true); - res->prop_state_acc(left->prop_state_acc() && right->prop_state_acc()); + if (res->acc().is_f()) + { + assert(res->num_edges() == 0); + res->prop_universal(true); + res->prop_complete(false); + res->prop_stutter_invariant(true); + res->prop_terminal(true); + res->prop_state_acc(true); + } + else + { + // The product of two non-deterministic automata could be + // deterministic. Likewise for non-complete automata. + if (left->prop_universal() && right->prop_universal()) + res->prop_universal(true); + if (left->prop_complete() && right->prop_complete()) + res->prop_complete(true); + if (left->prop_stutter_invariant() && right->prop_stutter_invariant()) + res->prop_stutter_invariant(true); + if (left->prop_inherently_weak() && right->prop_inherently_weak()) + res->prop_inherently_weak(true); + if (left->prop_weak() && right->prop_weak()) + res->prop_weak(true); + if (left->prop_terminal() && right->prop_terminal()) + res->prop_terminal(true); + res->prop_state_acc(left->prop_state_acc() + && right->prop_state_acc()); + } return res; } } @@ -450,6 +463,10 @@ namespace spot { auto res = make_twa_graph(left->get_dict()); res->new_state(); + res->prop_terminal(true); + res->prop_stutter_invariant(true); + res->prop_universal(true); + res->prop_complete(false); return res; } return make_twa_graph(left, twa::prop_set::all()); diff --git a/tests/python/prodexpt.py b/tests/python/prodexpt.py index 246fccba1..098bafb26 100644 --- a/tests/python/prodexpt.py +++ b/tests/python/prodexpt.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016-2017, 2019 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2016-2017, 2019-2020 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -102,3 +102,34 @@ res = spot.product(left, right, spot.output_aborter(900, 9000)) assert res is None res = spot.product(left, right, spot.output_aborter(1000, 9000)) assert res is not None + +a, b = spot.automata("""HOA: v1 States: 1 Start: 0 AP: 0 acc-name: all +Acceptance: 0 t properties: trans-labels explicit-labels state-acc complete +properties: deterministic stutter-invariant weak --BODY-- State: 0 [t] 0 +--END-- HOA: v1 States: 1 Start: 0 AP: 0 acc-name: none Acceptance: 0 f +properties: trans-labels explicit-labels state-acc complete properties: +deterministic stutter-invariant weak --BODY-- State: 0 [t] 0 --END--""") +out = spot.product(a, b).to_str() +assert out == """HOA: v1 +States: 1 +Start: 0 +AP: 0 +acc-name: none +Acceptance: 0 f +properties: trans-labels explicit-labels state-acc deterministic +properties: stutter-invariant terminal +--BODY-- +State: 0 +--END--""" +out = spot.product_susp(a, b).to_str() +assert out == """HOA: v1 +States: 1 +Start: 0 +AP: 0 +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +properties: stutter-invariant terminal +--BODY-- +State: 0 +--END--""" From e2ec711c4037a7e930ff30195715e05995e919dc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 11 Mar 2020 23:05:15 +0100 Subject: [PATCH 4/9] autfilt: fix -u Fixes #399. * bin/autfilt.cc: Fix it. * tests/core/isomorph.test: Add test case. * NEWS: Mention the issue. --- NEWS | 3 +++ bin/autfilt.cc | 33 +++++++++++++++++++++++++++------ tests/core/isomorph.test | 8 +++++++- 3 files changed, 37 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index f4a991052..c5e90b8ca 100644 --- a/NEWS +++ b/NEWS @@ -9,6 +9,9 @@ New in spot 2.8.6.dev (not yet released) incorrectly tagged as complete, causing the print_hoa() function to raise an exception. + - autfilt --uniq was not considering differences in acceptance + conditions or number of states when discarding automata. + New in spot 2.8.6 (2020-02-19) Bugs fixed: diff --git a/bin/autfilt.cc b/bin/autfilt.cc index e0f8279b2..00b16b83d 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -419,8 +419,31 @@ static const struct argp_child children[] = }; -typedef spot::twa_graph::graph_t::edge_storage_t tr_t; -typedef std::set> unique_aut_t; +struct canon_aut +{ + typedef spot::twa_graph::graph_t::edge_storage_t tr_t; + unsigned num_states; + std::vector edges; + std::string acc; + + canon_aut(const spot::const_twa_graph_ptr& aut) + : num_states(aut->num_states()) + , edges(aut->edge_vector().begin() + 1, + aut->edge_vector().end()) + { + std::ostringstream os; + aut->get_acceptance().to_text(os); + acc = os.str(); + } + + bool operator<(const canon_aut& o) const + { + return std::tie(num_states, edges, acc) + < std::tie(o.num_states, o.edges, o.acc); + }; +}; + +typedef std::set unique_aut_t; static long int match_count = 0; static spot::option_map extra_options; static bool randomize_st = false; @@ -703,8 +726,7 @@ parse_opt(int key, char* arg, struct argp_state*) opt_max_count = to_pos_int(arg, "-n/--max-count"); break; case 'u': - opt->uniq = - std::unique_ptr(new std::set>()); + opt->uniq = std::unique_ptr(new std::set()); break; case 'v': opt_invert = true; @@ -1559,8 +1581,7 @@ namespace auto tmp = spot::canonicalize(make_twa_graph(aut, spot::twa::prop_set::all())); - if (!opt->uniq->emplace(tmp->edge_vector().begin() + 1, - tmp->edge_vector().end()).second) + if (!opt->uniq->emplace(tmp).second) return 0; } diff --git a/tests/core/isomorph.test b/tests/core/isomorph.test index 37c3e43d3..a331f7399 100755 --- a/tests/core/isomorph.test +++ b/tests/core/isomorph.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de +# Copyright (C) 2014, 2015, 2020 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -109,3 +109,9 @@ run 0 autfilt aut3 --are-isomorphic aut4 run 0 autfilt -u aut1 aut2 aut2 aut3 -c >out test 2 = "`cat out`" + +ltl2tgba -D -G GFa > aut1 +ltl2tgba -D -G FGa > aut2 +test 0 = `autfilt -c --are-isomorphic aut1 aut2` +test 2 = `ltl2tgba -D -G 'GFa' 'FG!a' | autfilt -u -c` +test 1 = `ltl2tgba -D -G 'GFa' 'GFa' | autfilt -u -c` From 7aec23f0197f196283b047b43d7a9e0fd084a6c8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 12 Mar 2020 17:00:16 +0100 Subject: [PATCH 5/9] sccinfo: fix generation of self-loop accepting runs Reported by Juraj Major. * spot/twaalgos/sccinfo.cc (scc_info::get_accepting_run): Do not assume TRACK_STATES is enabled. * tests/core/autcross5.test: New file. * tests/Makefile.am: Add it. * NEWS: Mention the bug. --- NEWS | 6 ++ spot/twaalgos/sccinfo.cc | 58 ++++++----- tests/Makefile.am | 1 + tests/core/autcross5.test | 200 ++++++++++++++++++++++++++++++++++++++ 4 files changed, 239 insertions(+), 26 deletions(-) create mode 100755 tests/core/autcross5.test diff --git a/NEWS b/NEWS index c5e90b8ca..cfcc7d15a 100644 --- a/NEWS +++ b/NEWS @@ -12,6 +12,12 @@ New in spot 2.8.6.dev (not yet released) - autfilt --uniq was not considering differences in acceptance conditions or number of states when discarding automata. + - In an automaton with acceptance condition containing some Fin, and + whose accepting cycle could be reduced to a self-loop in an + otherwise larger SCC, the generation of an accepting run could be + wrong. This could in turn cause segfaults or infinite loops while + running autcross or autfilt --stats=%w. + New in spot 2.8.6 (2020-02-19) Bugs fixed: diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 773582ea1..705325a6d 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -558,37 +558,43 @@ namespace spot }; // The SCC exploration has a small optimization that can flag SCCs - // has accepting if they contain accepting self-loops, even if the + // as accepting if they contain accepting self-loops, even if the // SCC itself has some Fin acceptance to check. So we have to // deal with this situation before we look for the more complex // case of satisfying the condition with a larger cycle. We do // this first, because it's good to return a small cycle if we // can. const acc_cond& acccond = aut_->acc(); - for (unsigned s: node.states()) - for (auto& e: aut_->out(s)) - if (e.src == e.dst && !filter(e) && acccond.accepting(e.acc)) - { - // We have found an accepting self-loop. That's the cycle - // part of our accepting run. - r->cycle.clear(); - r->cycle.emplace_front(aut_->state_from_number(e.src), - e.cond, e.acc); - // Add the prefix. - r->prefix.clear(); - if (e.src != init) - explicit_bfs_steps(aut_, init, r->prefix, - [](const twa_graph::edge_storage_t&) - { - return false; // Do not filter. - }, - [&](const twa_graph::edge_storage_t& t) - { - return t.dst == e.src; - }); - return; - } - + unsigned num_states = aut_->num_states(); + for (unsigned s = 0; s < num_states; ++s) + { + // We scan the entire state to find those in the SCC, because + // we cannot rely on TRACK_STATES being on. + if (scc_of(s) != scc) + continue; + for (auto& e: aut_->out(s)) + if (e.src == e.dst && !filter(e) && acccond.accepting(e.acc)) + { + // We have found an accepting self-loop. That's the cycle + // part of our accepting run. + r->cycle.clear(); + r->cycle.emplace_front(aut_->state_from_number(e.src), + e.cond, e.acc); + // Add the prefix. + r->prefix.clear(); + if (e.src != init) + explicit_bfs_steps(aut_, init, r->prefix, + [](const twa_graph::edge_storage_t&) + { + return false; // Do not filter. + }, + [&](const twa_graph::edge_storage_t& t) + { + return t.dst == e.src; + }); + return; + } + } // Prefix search diff --git a/tests/Makefile.am b/tests/Makefile.am index f33ca5d2c..bdb04435a 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -314,6 +314,7 @@ TESTS_twa = \ core/autcross2.test \ core/autcross3.test \ core/autcross4.test \ + core/autcross5.test \ core/complementation.test \ core/randpsl.test \ core/cycles.test \ diff --git a/tests/core/autcross5.test b/tests/core/autcross5.test new file mode 100755 index 000000000..1dc4a29d5 --- /dev/null +++ b/tests/core/autcross5.test @@ -0,0 +1,200 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2020 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs +set -e + +# Based on a report by Juraj Major. + +cat >a7.hoa <_a7.hoa < %O' 2>stderr && exit 2 +cat stderr +grep 'both automata accept the infinite word:' stderr From 0940c9a25a2281dd0220229515bac98b0e278ff4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 12 Mar 2020 21:54:13 +0100 Subject: [PATCH 6/9] stutter: fix sl, sl2 to never accept on added self-loop Fixes #401, reported by Victor Khomenko. * spot/twaalgos/stutter.cc (sl, sl2): If {} is accepting, upgrade the acceptance condition. * tests/python/stutter.py: Add test cases. --- spot/twaalgos/stutter.cc | 53 ++++++++++++++++++++++++++++++++++++---- tests/python/stutter.py | 15 +++++++++++- 2 files changed, 62 insertions(+), 6 deletions(-) diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index 0a58294c3..af47a3c50 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement de +// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -276,6 +276,19 @@ namespace spot // We use the same BDD variables as the input. res->copy_ap_of(a); res->copy_acceptance_of(a); + + // We are going to create self-loop labeled by {}, + // and those should not be accepting. If they are, + // we need to upgrade the acceptance condition. + acc_cond::mark_t toadd = {}; + if (res->acc().accepting({})) + { + unsigned ns = res->num_sets(); + auto na = res->get_acceptance() & acc_cond::acc_code::inf({ns}); + res->set_acceptance(ns + 1, na); + toadd = {ns}; + } + // These maps make it possible to convert stutter_state to number // and vice-versa. ss2num_map ss2num; @@ -318,7 +331,7 @@ namespace spot } // Create the edge. - res->new_edge(src, dest, one, t.acc); + res->new_edge(src, dest, one, t.acc | toadd); if (src == dest) self_loop_needed = false; @@ -335,6 +348,36 @@ namespace spot twa_graph_ptr sl2_inplace(twa_graph_ptr a) { + // We are going to create self-loop labeled by {}, + // and those should not be accepting. If they are, + // we need to upgrade the acceptance condition. + if (a->acc().accepting({})) + { + unsigned ns = a->num_sets(); + auto na = a->get_acceptance() & acc_cond::acc_code::inf({ns}); + a->set_acceptance(ns + 1, na); + acc_cond::mark_t toadd = {ns}; + for (auto& e: a->edges()) + e.acc |= toadd; + } + + // The self-loops we add should not be accepting, so try to find + // an unsat mark, and upgrade the acceptance condition if + // necessary. + // + // UM is a pair (bool, mark). If the Boolean is false, the + // acceptance is always satisfiable. Otherwise, MARK is an + // example of unsatisfiable mark. + auto um = a->acc().unsat_mark(); + if (!um.first) + { + auto m = a->set_buchi(); + for (auto& e: a->edges()) + e.acc = m; + um.second = {}; + } + acc_cond::mark_t unsat = um.second; + bdd atomic_propositions = a->ap_vars(); unsigned num_states = a->num_states(); unsigned num_edges = a->num_edges(); @@ -378,10 +421,10 @@ namespace spot unsigned tmp = p.first->second; // intermediate state unsigned i = a->new_edge(src, tmp, one, acc); assert(i > num_edges); - i = a->new_edge(tmp, tmp, one, {}); + i = a->new_edge(tmp, tmp, one, unsat); assert(i > num_edges); - // No acceptance here to preserve the state-based property. - i = a->new_edge(tmp, dst, one, {}); + // unsat acceptance here to preserve the state-based property. + i = a->new_edge(tmp, dst, one, unsat); assert(i > num_edges); (void)i; } diff --git a/tests/python/stutter.py b/tests/python/stutter.py index 48240f940..7a7586190 100644 --- a/tests/python/stutter.py +++ b/tests/python/stutter.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2019, 2020 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -47,3 +47,16 @@ def explain_stut(f): w1, w2 = explain_stut('{(a:b) | (a;b)}|->Gc') assert str(w1) == 'a & !b & !c; cycle{!a & b & !c}' assert str(w2) == 'a & !b & !c; a & !b & !c; cycle{!a & b & !c}' + +# Test from issue #401 +w1, w2 = explain_stut('G({x} |-> ({x[+]} <>-> ({Y1[+]} <>=> Y2)))') +assert str(w1) == 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x}' +assert str(w2) == 'cycle{!Y1 & !Y2 & x; Y1 & Y2 & x; Y1 & Y2 & x}' + +# Related to issue #401 as well. sl() and sl2() should upgrade +# the t acceptance condition into inf(0). +pos = spot.translate('Xa & XXb') +w = pos.accepting_word().as_automaton() +assert w.acc().is_t() +assert not spot.sl2(w).acc().is_buchi() +assert not spot.sl(w).acc().is_buchi() From c36890339853aa7efc8088f9161dbcbf18698e40 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 13 Mar 2020 07:52:34 +0100 Subject: [PATCH 7/9] ltlcross: detect write errors for --save-bogus and --grind * bin/ltlcross.cc: Explicitly close those files to check for error conditions. * NEWS: Mention it. --- NEWS | 3 +++ bin/ltlcross.cc | 14 ++++++++++++-- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index cfcc7d15a..f7ed80fac 100644 --- a/NEWS +++ b/NEWS @@ -18,6 +18,9 @@ New in spot 2.8.6.dev (not yet released) wrong. This could in turn cause segfaults or infinite loops while running autcross or autfilt --stats=%w. + - ltlcross was not diagnosing write errors associated to + options --grind=FILENAME and --save-bogus=FILENAME. + New in spot 2.8.6 (2020-02-19) Bugs fixed: diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index efafe7b31..ec53e1c78 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -220,6 +220,7 @@ static bool products_avg = true; static bool opt_omit = false; static const char* bogus_output_filename = nullptr; static output_file* bogus_output = nullptr; +static const char* grind_output_filename = nullptr; static output_file* grind_output = nullptr; static bool verbose = false; static bool quiet = false; @@ -507,6 +508,7 @@ parse_opt(int key, char* arg, struct argp_state*) fail_on_timeout = true; break; case OPT_GRIND: + grind_output_filename = arg; grind_output = new output_file(arg); break; case OPT_IGNORE_EXEC_FAIL: @@ -1800,8 +1802,16 @@ main(int argc, char** argv) } } - delete bogus_output; - delete grind_output; + if (bogus_output) + { + bogus_output->close(bogus_output_filename); + delete bogus_output; + } + if (grind_output) + { + grind_output->close(grind_output_filename); + delete grind_output; + } if (json_output) print_stats_json(json_output); From 32e9bd4dbfbed219a73b932bb8d5b2bbcc3bfabc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 12 Mar 2020 22:59:11 +0100 Subject: [PATCH 8/9] Release Spot 2.8.7 * NEWS, configure.ac, doc/org/setup.org: Update. --- NEWS | 18 ++++++++++++++---- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 20 insertions(+), 10 deletions(-) diff --git a/NEWS b/NEWS index f7ed80fac..150e7ab7b 100644 --- a/NEWS +++ b/NEWS @@ -1,11 +1,9 @@ -New in spot 2.8.6.dev (not yet released) - - Nothing yet. +New in spot 2.8.7 (2019-03-13) Bugs fixed: - Building a product between two complete automata where one operand - had false acceptance could create a incomplete automaton + had false acceptance could create an incomplete automaton incorrectly tagged as complete, causing the print_hoa() function to raise an exception. @@ -18,6 +16,18 @@ New in spot 2.8.6.dev (not yet released) wrong. This could in turn cause segfaults or infinite loops while running autcross or autfilt --stats=%w. + - The generic emptiness check used a suboptimal selection of "Fin" + to remove, not matching the correct line in our ATVA'19 paper. + This could cause superfluous recursive calls, however benchmarks + have shown the difference to be insignificant in practice. + + - The sl(), and sl2() functions for computing the "self-loopization" + of an automaton, and used for instance in algorithms for computing + proof of stutter-sensitiveness (e.g., in our web application), + were incorrect when applied on automata with "t" acceptance (or + more generaly, any automaton where a cycle without mark is + accepting). + - ltlcross was not diagnosing write errors associated to options --grind=FILENAME and --save-bogus=FILENAME. diff --git a/configure.ac b/configure.ac index a31561efc..ea5805ab8 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.63]) -AC_INIT([spot], [2.8.6.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.8.7], [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 ad1824c80..0527e117b 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.8.6 -#+MACRO: LASTRELEASE 2.8.6 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.8.6.tar.gz][=spot-2.8.6.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-8-6/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2020-02-19 +#+MACRO: SPOTVERSION 2.8.7 +#+MACRO: LASTRELEASE 2.8.7 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.8.7.tar.gz][=spot-2.8.7.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-8-7/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2020-03-13 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From f53338e8ad22e93d784228ee754b429dc840b54c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 13 Mar 2020 08:04:48 +0100 Subject: [PATCH 9/9] * NEWS, configure.ac: Bump version to 2.8.7.dev. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 150e7ab7b..e018ba390 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.8.7.dev (not yet released) + + Nothing yet. + New in spot 2.8.7 (2019-03-13) Bugs fixed: diff --git a/configure.ac b/configure.ac index ea5805ab8..98b8877f4 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.63]) -AC_INIT([spot], [2.8.7], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.8.7.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])