diff --git a/bench/dtgbasat/gen.py b/bench/dtgbasat/gen.py index e96bf2825..dabf77971 100755 --- a/bench/dtgbasat/gen.py +++ b/bench/dtgbasat/gen.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -# Copyright (C) 2016-2018 Laboratoire de Recherche et Développement de +# Copyright (C) 2016-2018, 2023 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -55,12 +55,12 @@ class BenchConfig(object): if line[0] == '#' or line.isspace(): continue elif line[0:2] == "sh": - sh = re.search('sh (.+?)$', line).group(1) + sh = re.search('sh (.+)$', line).group(1) continue else: name = re.search('(.+?):', line).group(1) code = re.search(':(.+?)>', line).group(1) - xoptions = re.search('>(.+?)$', line).group(1) + xoptions = re.search('>(.+)$', line).group(1) b = Bench(name=name, code=code, xoptions=xoptions) self.l.append(b) self.sh.append(sh) diff --git a/bin/autcross.cc b/bin/autcross.cc index 24cd9bcd4..b3e504bb3 100644 --- a/bin/autcross.cc +++ b/bin/autcross.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2020, 2022 Laboratoire de Recherche et +// Copyright (C) 2017-2020, 2022-2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -549,7 +549,7 @@ namespace { if (!quiet) std::cerr << "info: building " << autname(i, is_really_comp(i)) - << '*' << autname(j, true ^ is_really_comp(j)) + << '*' << autname(j, !is_really_comp(j)) << " requires more acceptance sets than supported\n"; return false; } @@ -557,14 +557,14 @@ namespace if (verbose) std::cerr << "info: check_empty " << autname(i, is_really_comp(i)) - << '*' << autname(j, true ^ is_really_comp(j)) << '\n'; + << '*' << autname(j, !is_really_comp(j)) << '\n'; auto w = aut_i->intersecting_word(aut_j); if (w) { std::ostream& err = global_error(); err << "error: " << autname(i, is_really_comp(i)) - << '*' << autname(j, true ^ is_really_comp(j)) + << '*' << autname(j, !is_really_comp(j)) << (" is nonempty; both automata accept the infinite word:\n" " "); example() << *w << '\n'; @@ -613,7 +613,7 @@ namespace return src.str(); }(); - input_statistics.push_back(in_statistics()); + input_statistics.emplace_back(in_statistics()); input_statistics[round_num].input_source = std::move(source); if (auto name = input->get_named_prop("automaton-name")) @@ -658,7 +658,7 @@ namespace problems += prob; } spot::cleanup_tmpfiles(); - output_statistics.push_back(std::move(stats)); + output_statistics.emplace_back(std::move(stats)); if (verbose) { diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 7cff60e8b..b55d1bc9f 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -448,7 +448,7 @@ struct canon_aut std::vector edges; std::string acc; - canon_aut(const spot::const_twa_graph_ptr& aut) + explicit canon_aut(const spot::const_twa_graph_ptr& aut) : num_states(aut->num_states()) , edges(aut->edge_vector().begin() + 1, aut->edge_vector().end()) @@ -755,6 +755,22 @@ product_or(spot::twa_graph_ptr left, spot::twa_graph_ptr right) return spot::product_or(left, right); } +static spot::twa_graph_ptr +word_to_aut(const char* word, const char *argname) +{ + try + { + return spot::parse_word(word, opt->dict)->as_automaton(); + } + catch (const spot::parse_error& e) + { + error(2, 0, "failed to parse the argument of --%s:\n%s", + argname, e.what()); + } + SPOT_UNREACHABLE(); + return nullptr; +} + static int parse_opt(int key, char* arg, struct argp_state*) { @@ -776,17 +792,14 @@ parse_opt(int key, char* arg, struct argp_state*) opt_nth = parse_range(arg, 0, std::numeric_limits::max()); break; case 'u': - opt->uniq = std::unique_ptr(new std::set()); + opt->uniq = std::make_unique(); break; case 'v': opt_invert = true; break; case 'x': - { - const char* opt = extra_options.parse_options(arg); - if (opt) - error(2, 0, "failed to parse --options near '%s'", opt); - } + if (const char* opt = extra_options.parse_options(arg)) + error(2, 0, "failed to parse --options near '%s'", opt); break; case OPT_ALIASES: opt_aliases = XARGMATCH("--aliases", arg, aliases_args, aliases_types); @@ -802,16 +815,7 @@ parse_opt(int key, char* arg, struct argp_state*) opt_art_sccs_set = true; break; case OPT_ACCEPT_WORD: - try - { - opt->acc_words.push_back(spot::parse_word(arg, opt->dict) - ->as_automaton()); - } - catch (const spot::parse_error& e) - { - error(2, 0, "failed to parse the argument of --accept-word:\n%s", - e.what()); - } + opt->acc_words.emplace_back(word_to_aut(arg, "accept-word")); break; case OPT_ACCEPTANCE_IS: { @@ -964,16 +968,7 @@ parse_opt(int key, char* arg, struct argp_state*) "%d should be followed by a comma and WORD", res); arg = endptr + 1; } - try - { - opt->hl_words.emplace_back(spot::parse_word(arg, opt->dict) - ->as_automaton(), res); - } - catch (const spot::parse_error& e) - { - error(2, 0, "failed to parse the argument of --highlight-word:\n%s", - e.what()); - } + opt->hl_words.emplace_back(word_to_aut(arg, "highlight-word"), res); } break; case OPT_HIGHLIGHT_LANGUAGES: @@ -1157,16 +1152,7 @@ parse_opt(int key, char* arg, struct argp_state*) opt_art_sccs_set = true; break; case OPT_REJECT_WORD: - try - { - opt->rej_words.push_back(spot::parse_word(arg, opt->dict) - ->as_automaton()); - } - catch (const spot::parse_error& e) - { - error(2, 0, "failed to parse the argument of --reject-word:\n%s", - e.what()); - } + opt->rej_words.emplace_back(word_to_aut(arg, "reject-word")); break; case OPT_REM_AP: opt->rem_ap.add_ap(arg); @@ -1291,7 +1277,7 @@ namespace static bool match_acceptance(spot::twa_graph_ptr aut) { - auto& acc = aut->acc(); + const spot::acc_cond& acc = aut->acc(); switch (opt_acceptance_is) { case ACC_Any: @@ -1346,8 +1332,7 @@ namespace { bool max; bool odd; - bool is_p = acc.is_parity(max, odd, true); - if (!is_p) + if (!acc.is_parity(max, odd, true)) return false; switch (opt_acceptance_is) { @@ -1460,7 +1445,7 @@ namespace if (matched && opt_acceptance_is) matched = match_acceptance(aut); - if (matched && (opt_sccs_set | opt_art_sccs_set)) + if (matched && (opt_sccs_set || opt_art_sccs_set)) { spot::scc_info si(aut); unsigned n = si.scc_count(); @@ -1540,14 +1525,14 @@ namespace && spot::contains(aut, opt->equivalent_pos); if (matched && !opt->acc_words.empty()) - for (auto& word_aut: opt->acc_words) + for (const spot::twa_graph_ptr& word_aut: opt->acc_words) if (spot::product(aut, word_aut)->is_empty()) { matched = false; break; } if (matched && !opt->rej_words.empty()) - for (auto& word_aut: opt->rej_words) + for (const spot::twa_graph_ptr& word_aut: opt->rej_words) if (!spot::product(aut, word_aut)->is_empty()) { matched = false; @@ -1681,13 +1666,13 @@ namespace aut->accepting_run()->highlight(opt_highlight_accepting_run); if (!opt->hl_words.empty()) - for (auto& word_aut: opt->hl_words) + for (auto& [word_aut, color]: opt->hl_words) { if (aut->acc().uses_fin_acceptance()) error(2, 0, "--highlight-word does not yet work with Fin acceptance"); - if (auto run = spot::product(aut, word_aut.first)->accepting_run()) - run->project(aut)->highlight(word_aut.second); + if (auto run = spot::product(aut, word_aut)->accepting_run()) + run->project(aut)->highlight(color); } timer.stop(); diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index fcc79fc3c..60f83289e 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -453,7 +453,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, const spot::const_twa_graph_ptr& aut, spot::formula f, const char* filename, int loc, - spot::process_timer& ptimer, + const spot::process_timer& ptimer, const char* csv_prefix, const char* csv_suffix) { timer_ = ptimer; @@ -633,10 +633,10 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, outputnamer.print(haut, aut, f, filename, loc, ptimer, csv_prefix, csv_suffix); std::string fname = outputname.str(); - auto p = outputfiles.emplace(fname, nullptr); - if (p.second) - p.first->second.reset(new output_file(fname.c_str())); - out = &p.first->second->ostream(); + auto [it, b] = outputfiles.try_emplace(fname, nullptr); + if (b) + it->second.reset(new output_file(fname.c_str())); + out = &it->second->ostream(); } // Output it. diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index d33b687d2..f57beae84 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2018, 2020, 2022 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2014-2018, 2020, 2022, 2023 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -155,7 +155,7 @@ public: print(const spot::const_parsed_aut_ptr& haut, const spot::const_twa_graph_ptr& aut, spot::formula f, - const char* filename, int loc, spot::process_timer& ptimer, + const char* filename, int loc, const spot::process_timer& ptimer, const char* csv_prefix, const char* csv_suffix); private: @@ -196,7 +196,7 @@ class automaton_printer std::map> outputfiles; public: - automaton_printer(stat_style input = no_input); + explicit automaton_printer(stat_style input = no_input); ~automaton_printer(); void