diff --git a/NEWS b/NEWS index 0fe750ac4..0f5da75fa 100644 --- a/NEWS +++ b/NEWS @@ -140,7 +140,7 @@ New in spot 2.7.5.dev (not yet released) properties. This can be altered with the SPOT_PR_CHECK environment variable. - Backward incompatibilities: + Deprecation notices: - The virtual function twa::intersecting_run() no longuer takes a second "from_other" Boolean argument. This is a backward @@ -149,6 +149,11 @@ New in spot 2.7.5.dev (not yet released) call this function with two argument, a non-virtual version of the function has been introduced and marked as deprecated. + - The spot::acc_cond::format() methods have been deprecated. These + were used to display acceptance marks, but acceptance marks are + unrelated to acceptance conditions, so it's better to simply print + marks with operator<< without this extra step. + Bugs fixed: - The gf_guarantee_to_ba() is relying on an inplace algorithm that diff --git a/spot/priv/satcommon.cc b/spot/priv/satcommon.cc index 53f9a81cc..21d75eee1 100644 --- a/spot/priv/satcommon.cc +++ b/spot/priv/satcommon.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -97,7 +97,7 @@ namespace spot std::string vars_helper::format_t(bdd_dict_ptr& debug_dict, unsigned src, bdd& cond, - unsigned dst) + unsigned dst) { std::ostringstream buffer; buffer << '<' << src << ',' << bdd_format_formula(debug_dict, cond) @@ -107,31 +107,30 @@ namespace spot std::string vars_helper::format_ta(bdd_dict_ptr& debug_dict, - const acc_cond* debug_cand_acc, unsigned src, bdd& cond, unsigned dst, - const acc_cond::mark_t& acc) + unsigned src, bdd& cond, unsigned dst, + const acc_cond::mark_t& acc) { std::ostringstream buffer; buffer << '<' << src << ',' << bdd_format_formula(debug_dict, cond) - << ',' << debug_cand_acc->format(acc) << ',' << dst << '>'; + << ',' << acc << ',' << dst << '>'; return buffer.str(); } std::string - vars_helper::format_p(const acc_cond* debug_cand_acc, - const acc_cond* debug_ref_acc, unsigned src_cand, unsigned src_ref, - unsigned dst_cand, unsigned dst_ref, acc_cond::mark_t acc_cand, - acc_cond::mark_t acc_ref) + vars_helper::format_p(unsigned src_cand, unsigned src_ref, + unsigned dst_cand, unsigned dst_ref, + acc_cond::mark_t acc_cand, acc_cond::mark_t acc_ref) { std::ostringstream buffer; buffer << '<' << src_cand << ',' << src_ref << ',' << dst_cand << ',' - << dst_ref << ", " << debug_cand_acc->format(acc_cand) << ", " - << debug_ref_acc->format(acc_ref) << '>'; + << dst_ref << ", " << acc_cand << ", " + << acc_ref << '>'; return buffer.str(); } std::string vars_helper::format_p(unsigned src_cand, unsigned src_ref, unsigned dst_cand, - unsigned dst_ref) + unsigned dst_ref) { std::ostringstream buffer; buffer << '<' << src_cand << ',' << src_ref; diff --git a/spot/priv/satcommon.hh b/spot/priv/satcommon.hh index a8403bff7..653212a92 100644 --- a/spot/priv/satcommon.hh +++ b/spot/priv/satcommon.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2016, 2018 Laboratoire de Recherche et +// Copyright (C) 2013-2016, 2018, 2019 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -207,24 +207,24 @@ public: /// \brief Use this function to get a string representation of a transition. std::string format_t(bdd_dict_ptr& debug_dict, unsigned src, bdd& cond, - unsigned dst); + unsigned dst); /// \brief Use this function to get a string representation of a transition /// acc. std::string - format_ta(bdd_dict_ptr& debug_dict, const acc_cond* debug_cand_acc, - unsigned src, bdd& cond, unsigned dst, const acc_cond::mark_t& acc); + format_ta(bdd_dict_ptr& debug_dict, unsigned src, bdd& cond, unsigned dst, + const acc_cond::mark_t& acc); /// \brief Use this function to get a string representation of a path var. std::string - format_p(const acc_cond* debug_cand_acc, const acc_cond* debug_ref_acc, - unsigned src_cand, unsigned src_ref, unsigned dst_cand, - unsigned dst_ref, acc_cond::mark_t acc_cand, acc_cond::mark_t acc_ref); + format_p(unsigned src_cand, unsigned src_ref, + unsigned dst_cand, unsigned dst_ref, + acc_cond::mark_t acc_cand, acc_cond::mark_t acc_ref); /// \brief Use this function to get a string representation of a path var. std::string - format_p(unsigned src_cand, unsigned src_ref, unsigned dst_cand, - unsigned dst_ref); + format_p(unsigned src_cand, unsigned src_ref, + unsigned dst_cand, unsigned dst_ref); }; /// \brief Give a filename to save the log of the SAT minimization. diff --git a/spot/taalgos/dot.cc b/spot/taalgos/dot.cc index 91b6065a9..ba0f3d517 100644 --- a/spot/taalgos/dot.cc +++ b/spot/taalgos/dot.cc @@ -1,6 +1,7 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2014-2016, 2018 Laboratoire de Recherche -// et Developpement de l Epita (LRDE). + +// Copyright (C) 2010, 2012, 2014-2016, 2018-2019 Laboratoire de +// Recherche et Developpement de l Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -239,8 +240,7 @@ namespace spot if (!opt_hide_sets_) { label += "\n"; - label += t_automata_->acc(). - format(si->acc()); + label += si->acc().as_string(); } os_ << " " << in << " -> " << out << " [label=\""; diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 05747a29e..cad84f7da 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -406,6 +406,13 @@ namespace spot SPOT_API friend std::ostream& operator<<(std::ostream& os, mark_t m); + + std::string as_string() const + { + std::ostringstream os; + os << *this; + return os.str(); + } }; /// \brief Operators for acceptance formulas. @@ -1842,20 +1849,22 @@ namespace spot /// that the condition is satisfied. mark_t accepting_sets(mark_t inf) const; - // FIXME: deprecate? + // Deprecated since Spot 2.8 + SPOT_DEPRECATED("Use operator<< instead.") std::ostream& format(std::ostream& os, mark_t m) const { - auto a = m; // ??? - if (!a) + if (!m) return os; return os << m; } - // FIXME: deprecate? + // Deprecated since Spot 2.8 + SPOT_DEPRECATED("Use operator<< or mark_t::as_string() instead.") std::string format(mark_t m) const { std::ostringstream os; - format(os, m); + if (m) + os << m; return os.str(); } diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index cab21b276..7d5037eca 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018 Laboratoire de Recherche +// Copyright (C) 2013-2019 Laboratoire de Recherche // et Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -63,8 +63,6 @@ namespace spot namespace { static bdd_dict_ptr debug_dict = nullptr; - static const acc_cond* debug_ref_acc = nullptr; - static const acc_cond* debug_cand_acc = nullptr; struct path { @@ -333,15 +331,14 @@ namespace spot std::string fmt_ta(unsigned src, bdd& cond, unsigned dst, unsigned nacc) { - return helper.format_ta(debug_dict, debug_cand_acc, src, cond, - dst, cacc.mark(nacc)); + return helper.format_ta(debug_dict, src, cond, dst, cacc.mark(nacc)); } std::string fmt_ta(unsigned src, unsigned cond, unsigned dst, unsigned nacc) { - return helper.format_ta(debug_dict, debug_cand_acc, src, - alpha_vect[cond], dst, cacc.mark(nacc)); + return helper.format_ta(debug_dict, src, + alpha_vect[cond], dst, cacc.mark(nacc)); } std::string @@ -349,8 +346,8 @@ namespace spot unsigned dst_ref, acc_cond::mark_t acc_cand = {}, acc_cond::mark_t acc_ref = {}) { - return helper.format_p(debug_cand_acc, debug_ref_acc, src_cand, - src_ref, dst_cand, dst_ref, acc_cand, acc_ref); + return helper.format_p(src_cand, src_ref, dst_cand, dst_ref, + acc_cand, acc_ref); } acc_cond::mark_t @@ -568,8 +565,6 @@ namespace spot assert(d.cand_size > 0); #if TRACE - debug_ref_acc = &ref->acc(); - debug_cand_acc = &d.cacc; solver.comment("d.ref_size:", d.ref_size, '\n'); solver.comment("d.cand_size:", d.cand_size, '\n'); #endif diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc index 30795f812..0f044c900 100644 --- a/spot/twaalgos/emptiness.cc +++ b/spot/twaalgos/emptiness.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011-2018 Laboratoire de Recherche et +// Copyright (C) 2009, 2011-2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -632,7 +632,7 @@ namespace spot { os << "ERROR: no transition with label=" << bdd_format_formula(aut->get_dict(), label) - << " and acc=" << aut->acc().format(acc) + << " and acc=" << acc << " leaving state " << serial << " for state " << aut->format_state(next) << '\n' << "The following transitions leave state " << serial @@ -644,9 +644,7 @@ namespace spot os << " * label=" << bdd_format_formula(aut->get_dict(), j->cond()) - << " and acc=" - << (aut->acc().format - (j->acc())) + << " and acc=" << j->acc() << " going to " << aut->format_state(s2) << '\n'; s2->destroy(); } @@ -660,20 +658,19 @@ namespace spot { os << "transition with label=" << bdd_format_formula(aut->get_dict(), label) - << " and acc=" << aut->acc().format(acc) - << std::endl; + << " and acc=" << acc << std::endl; } else { os << " | "; bdd_print_formula(os, aut->get_dict(), label); - os << '\t'; - aut->acc().format(acc); + if (acc) + os << '\t' << acc; os << std::endl; } aut->release_iter(j); - // Sum acceptance conditions. + // Sum acceptance marks. // // (Beware l and i designate the next step to consider. // Therefore if i is at the beginning of the cycle, `acc' @@ -686,8 +683,8 @@ namespace spot { all_acc_seen = true; if (debug) - os << "all acceptance conditions (" - << aut->acc().format(all_acc) + os << "all acceptance marks (" + << all_acc << ") have been seen\n"; } } @@ -696,10 +693,10 @@ namespace spot if (!aut->acc().accepting(all_acc)) { if (debug) - os << "ERROR: The cycle's acceptance conditions (" - << aut->acc().format(all_acc) - << ") do not\nmatch those of the automaton (" - << aut->acc().format(aut->acc().all_sets()) + os << "ERROR: The cycle's acceptance marks (" + << all_acc + << ") do not satisfy the acceptance condition (" + << aut->get_acceptance() << ")\n"; return false; } diff --git a/tests/core/acc.cc b/tests/core/acc.cc index 9aa01b3a5..91e829724 100644 --- a/tests/core/acc.cc +++ b/tests/core/acc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*-x -// Copyright (C) 2014, 2015, 2017, 2018 Laboratoire de Recherche et +// Copyright (C) 2014, 2015, 2017, 2018, 2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -28,9 +28,7 @@ static void check(spot::acc_cond& ac, spot::acc_cond::mark_t m) { - std::cout << '#' << m.count() << ": " << ac.format(m); - if (!m) - std::cout << "empty"; + std::cout << '#' << m.count() << ": " << m; if (ac.accepting(m)) std::cout << " accepting"; std::cout << '\n'; diff --git a/tests/core/acc.test b/tests/core/acc.test index 9a33a826f..ad7f80578 100755 --- a/tests/core/acc.test +++ b/tests/core/acc.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et +# Copyright (C) 2014, 2015, 2017, 2019 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -39,7 +39,7 @@ Inf(0)&Inf(1)&Inf(2)&Inf(3) #3: {0,2,3} #1: {0} #4: {0,1,2,3} -#0: empty +#0: {} #5: {0,1,2,3,4} accepting #2: {1,2} 5 + 5 = 10 @@ -48,14 +48,14 @@ Inf(0)&Inf(1)&Inf(2)&Inf(3) #7: {0,1,2,3,4,6,7} #10: {0,1,2,3,4,5,6,7,8,9} accepting 0,1,2,3,4,5,6,7,8,9 -#0: empty accepting -#0: empty accepting +#0: {} accepting +#0: {} accepting #1: {3} #4: {0,1,2,3} #2: {0,2} stripping #2: {0,2} -#0: empty +#0: {} #2: {0,3} #1: {1} #2: {1,2}