From 39212bbcd27daa650f1851f57d0722424fb97ff0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 6 Jan 2023 11:55:34 +0100 Subject: [PATCH] more code smells * bin/common_file.cc, bin/common_file.hh, bin/common_finput.cc, bin/common_finput.hh, bin/common_output.cc, bin/common_setup.cc, bin/common_setup.hh, bin/common_trans.cc, bin/common_trans.hh, bin/dstar2tgba.cc, bin/genaut.cc, bin/genltl.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc, bin/ltlfilt.cc, bin/ltlsynt.cc, bin/randltl.cc: Fix minor code issues reported by sonarcloud. --- bin/common_file.cc | 7 ++-- bin/common_file.hh | 13 +++---- bin/common_finput.cc | 10 ++---- bin/common_finput.hh | 16 +++++---- bin/common_output.cc | 20 +++++------ bin/common_setup.cc | 7 ++-- bin/common_setup.hh | 6 ++-- bin/common_trans.cc | 46 ++++++++++++------------ bin/common_trans.hh | 19 +++++----- bin/dstar2tgba.cc | 4 +-- bin/genaut.cc | 4 +-- bin/genltl.cc | 6 ++-- bin/ltl2tgba.cc | 8 ++--- bin/ltl2tgta.cc | 4 +-- bin/ltlcross.cc | 86 ++++++++++++++++---------------------------- bin/ltldo.cc | 14 +++----- bin/ltlfilt.cc | 20 +++++------ bin/ltlsynt.cc | 15 ++++---- bin/randltl.cc | 6 ++-- 19 files changed, 133 insertions(+), 178 deletions(-) diff --git a/bin/common_file.cc b/bin/common_file.cc index 005bb5479..4e56c6d54 100644 --- a/bin/common_file.cc +++ b/bin/common_file.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2022 Laboratoire de Recherche et +// Copyright (C) 2015, 2016, 2022, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -21,7 +21,6 @@ #include #include - output_file::output_file(const char* name, bool force_append) { std::ios_base::openmode mode = std::ios_base::trunc; @@ -39,10 +38,10 @@ output_file::output_file(const char* name, bool force_append) os_ = &std::cout; return; } - of_ = new std::ofstream(name, mode); + of_ = std::make_unique(name, mode); if (!*of_) error(2, errno, "cannot open '%s'", name); - os_ = of_; + os_ = of_.get(); } diff --git a/bin/common_file.hh b/bin/common_file.hh index b8f9842b8..b6aa0bec3 100644 --- a/bin/common_file.hh +++ b/bin/common_file.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2022 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015-2016, 2022-2023 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -21,13 +21,13 @@ #include "common_sys.hh" #include +#include #include -#include class output_file { std::ostream* os_; - std::ofstream* of_ = nullptr; + std::unique_ptr of_; bool append_ = false; public: // Open a file for output. "-" is interpreted as stdout. @@ -37,11 +37,6 @@ public: void close(const std::string& name); - ~output_file() - { - delete of_; - } - bool append() const { return append_; diff --git a/bin/common_finput.cc b/bin/common_finput.cc index 80aca5df7..dbcdb3849 100644 --- a/bin/common_finput.cc +++ b/bin/common_finput.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2017, 2019, 2021, 2022 Laboratoire de Recherche +// Copyright (C) 2012-2017, 2019, 2021-2023 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -96,12 +96,6 @@ parse_formula(const std::string& s) (s, spot::default_environment::instance(), false, lenient); } -job_processor::job_processor() - : abort_run(false), real_filename(nullptr), - col_to_read(0), prefix(nullptr), suffix(nullptr) -{ -} - job_processor::~job_processor() { if (real_filename) @@ -370,7 +364,7 @@ int job_processor::run() { int error = 0; - for (auto& j: jobs) + for (const auto& j: jobs) { switch (j.type) { diff --git a/bin/common_finput.hh b/bin/common_finput.hh index 2a5815fc3..9ecb5b025 100644 --- a/bin/common_finput.hh +++ b/bin/common_finput.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2017, 2022 Laboratoire de Recherche et +// Copyright (C) 2012-2017, 2022, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -56,9 +56,11 @@ spot::parsed_formula parse_formula(const std::string& s); class job_processor { protected: - bool abort_run; // Set to true in process_formula() to abort run(). + bool abort_run = false; // Set to true in process_formula() to abort run(). public: - job_processor(); + job_processor() = default; + job_processor(const job_processor&) = delete; + job_processor& operator=(const job_processor&) = delete; virtual ~job_processor(); @@ -84,10 +86,10 @@ public: virtual int run(); - char* real_filename; - long int col_to_read; - char* prefix; - char* suffix; + char* real_filename = nullptr; + long int col_to_read = 0; + char* prefix = nullptr; + char* suffix = nullptr; }; // Report and error message or add a default job depending on whether diff --git a/bin/common_output.cc b/bin/common_output.cc index e9c61a513..93cb2dfaf 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2019, 2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -23,6 +23,7 @@ #include "common_setup.hh" #include #include +#include #include #include #include @@ -297,9 +298,9 @@ namespace }; } -static formula_printer* format = nullptr; +static std::unique_ptr format; static std::ostringstream outputname; -static formula_printer* outputnamer = nullptr; +static std::unique_ptr outputnamer; static std::map> outputfiles; int @@ -320,7 +321,7 @@ parse_opt_output(int key, char* arg, struct argp_state*) output_format = lbt_output; break; case 'o': - outputnamer = new formula_printer(outputname, arg); + outputnamer = std::make_unique(outputname, arg); break; case 'p': full_parenth = true; @@ -341,8 +342,7 @@ parse_opt_output(int key, char* arg, struct argp_state*) output_format = wring_output; break; case OPT_FORMAT: - delete format; - format = new formula_printer(std::cout, arg); + format = std::make_unique(std::cout, arg); break; default: return ARGP_ERR_UNKNOWN; @@ -417,10 +417,10 @@ output_formula_checked(spot::formula f, spot::process_timer* ptimer, formula_with_location fl = { f, filename, linenum, prefix, suffix }; outputnamer->print(fl, ptimer); 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_formula(*out, f, ptimer, filename, linenum, prefix, suffix); *out << output_terminator; diff --git a/bin/common_setup.cc b/bin/common_setup.cc index 24cacae85..af033a47f 100644 --- a/bin/common_setup.cc +++ b/bin/common_setup.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. @@ -20,13 +20,14 @@ #include "common_setup.hh" #include "common_aoutput.hh" -#include "argp.h" -#include "closeout.h" +#include +#include #include #include #include #include #include +#include #include static void diff --git a/bin/common_setup.hh b/bin/common_setup.hh index e2fce84e0..94cd16f4f 100644 --- a/bin/common_setup.hh +++ b/bin/common_setup.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2018, 2019 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012-2013, 2018-2019, 2023 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -34,5 +34,5 @@ int protected_main(char** progname, std::function mainfun); // Diagnose exceptions. [[noreturn]] void handle_any_exception(); -#define BEGIN_EXCEPTION_PROTECT try { (void)0; +#define BEGIN_EXCEPTION_PROTECT try { (void)0 #define END_EXCEPTION_PROTECT } catch (...) { handle_any_exception(); } diff --git a/bin/common_trans.cc b/bin/common_trans.cc index e34f3d77d..b93535173 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -53,7 +53,7 @@ struct shorthands_t }; #define SHORTHAND(PRE, POST) { PRE, std::regex("^" PRE), POST } -static shorthands_t shorthands_ltl[] = { +static const shorthands_t shorthands_ltl[] = { SHORTHAND("delag", " %f>%O"), SHORTHAND("lbt", " <%L>%O"), SHORTHAND("ltl2ba", " -f %s>%O"), @@ -73,7 +73,7 @@ static shorthands_t shorthands_ltl[] = { SHORTHAND("owl.* ltl-utilities\\b", " -f %f"), }; -static shorthands_t shorthands_autproc[] = { +static const shorthands_t shorthands_autproc[] = { SHORTHAND("autfilt", " %H>%O"), SHORTHAND("dra2dpa", " <%H>%O"), SHORTHAND("dstar2tgba", " %H>%O"), @@ -85,7 +85,7 @@ static shorthands_t shorthands_autproc[] = { " <%H>%O"), }; -static void show_shorthands(shorthands_t* begin, shorthands_t* end) +static void show_shorthands(const shorthands_t* begin, const shorthands_t* end) { std::cout << ("If a COMMANDFMT does not use any %-sequence, and starts with one of\n" @@ -100,7 +100,8 @@ static void show_shorthands(shorthands_t* begin, shorthands_t* end) } -tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end, +tool_spec::tool_spec(const char* spec, + const shorthands_t* begin, const shorthands_t* end, bool is_ref) noexcept : spec(spec), cmd(spec), name(spec), reference(is_ref) { @@ -113,15 +114,15 @@ tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end, { if (*pos == '{') ++count; - else if (*pos == '}') - if (!--count) - { - name = strndup(cmd + 1, pos - cmd - 1); - cmd = pos + 1; - while (*cmd == ' ' || *cmd == '\t') - ++cmd; - break; - } + else if (*pos == '}' && --count == 0) + { + name = strndup(cmd + 1, pos - cmd - 1); + cmd = pos + 1; + // skip leading whitespace + while (*cmd == ' ' || *cmd == '\t') + ++cmd; + break; + } } } // If there is no % in the string, look for a known @@ -147,11 +148,11 @@ tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end, auto& p = *begin++; if (std::regex_search(basename, p.rprefix)) { - int m = strlen(p.suffix); - int q = strlen(cmd); + size_t m = strlen(p.suffix); + size_t q = strlen(cmd); char* tmp = static_cast(malloc(q + m + 1)); - strcpy(tmp, cmd); - strcpy(tmp + q, p.suffix); + memcpy(tmp, cmd, q); + memcpy(tmp + q, p.suffix, m + 1); cmd = tmp; allocated = true; break; @@ -490,9 +491,8 @@ read_stdout_of_command(char* const* args) if (close(cout_pipe[1]) < 0) error(2, errno, "closing write-side of pipe failed"); - std::string buffer(32, 0); std::string results; - int bytes_read; + ssize_t bytes_read; for (;;) { static char buffer[512]; @@ -612,7 +612,7 @@ get_arg(const char*& cmd) { const char* start = cmd; std::string arg; - while (int c = *cmd) + while (char c = *cmd) { switch (c) { @@ -642,14 +642,14 @@ get_arg(const char*& cmd) goto end_loop; case '\'': { - int d = 0; + char d = '\0'; while ((d = *++cmd)) { if (d == '\'') break; arg.push_back(d); } - if (d == 0) + if (d == '\0') return nullptr; } break; diff --git a/bin/common_trans.hh b/bin/common_trans.hh index 31c88c80c..0ebe59e8c 100644 --- a/bin/common_trans.hh +++ b/bin/common_trans.hh @@ -51,7 +51,8 @@ struct tool_spec // Whether the tool is a reference. bool reference; - tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end, + tool_spec(const char* spec, + const shorthands_t* begin, const shorthands_t* end, bool is_ref) noexcept; tool_spec(const tool_spec& other) noexcept; tool_spec& operator=(const tool_spec& other); @@ -71,7 +72,7 @@ struct quoted_formula final: public spot::printable_value struct filed_formula final: public spot::printable { - filed_formula(const quoted_formula& ltl) : f_(ltl) + explicit filed_formula(const quoted_formula& ltl) : f_(ltl) { } @@ -89,9 +90,7 @@ struct filed_formula final: public spot::printable struct filed_automaton final: public spot::printable { - filed_automaton() - { - } + filed_automaton() = default; void print(std::ostream& os, const char* pos) const override; @@ -112,7 +111,7 @@ struct printable_result_filename final: unsigned translator_num; printable_result_filename(); - ~printable_result_filename(); + ~printable_result_filename() override; void reset(unsigned n); void cleanup(); @@ -126,7 +125,7 @@ protected: spot::bdd_dict_ptr dict; // Round-specific variables quoted_formula ltl_formula; - filed_formula filename_formula = ltl_formula; + filed_formula filename_formula{ltl_formula}; // Run-specific variables printable_result_filename output; public: @@ -151,9 +150,9 @@ protected: public: using spot::formater::has; - autproc_runner(// whether we accept the absence of output - // specifier - bool no_output_allowed = false); + explicit autproc_runner(// whether we accept the absence of output + // specifier + bool no_output_allowed = false); void round_automaton(spot::const_twa_graph_ptr aut, unsigned serial); }; diff --git a/bin/dstar2tgba.cc b/bin/dstar2tgba.cc index 5b60a0ecc..4b2ec9662 100644 --- a/bin/dstar2tgba.cc +++ b/bin/dstar2tgba.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2019, 2022 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2019, 2022, 2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -117,7 +117,7 @@ namespace spot::postprocessor& post; automaton_printer printer; - dstar_processor(spot::postprocessor& post) + explicit dstar_processor(spot::postprocessor& post) : hoa_processor(spot::make_bdd_dict()), post(post), printer(aut_input) { } diff --git a/bin/genaut.cc b/bin/genaut.cc index 26678c588..f8d6b93ff 100644 --- a/bin/genaut.cc +++ b/bin/genaut.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2019, 2022 Laboratoire de Recherche et +// Copyright (C) 2017-2019, 2022-2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -128,7 +128,7 @@ output_pattern(gen::aut_pattern_id pattern, int n) static void run_jobs() { - for (auto& j: jobs) + for (const auto& j: jobs) { int inc = (j.range.max < j.range.min) ? -1 : 1; int n = j.range.min; diff --git a/bin/genltl.cc b/bin/genltl.cc index 96d8bd7d3..ef8049171 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2015-2019, 2022 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2015-2019, 2022-2023 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -317,7 +317,7 @@ output_pattern(gen::ltl_pattern_id pattern, int n, int n2) static void run_jobs() { - for (auto& j: jobs) + for (const auto& j: jobs) { int inc = (j.range.max < j.range.min) ? -1 : 1; int n = j.range.min; diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc index d4fb2fc17..73a9a23c6 100644 --- a/bin/ltl2tgba.cc +++ b/bin/ltl2tgba.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2019, 2022 Laboratoire de Recherche et +// Copyright (C) 2012-2019, 2022-2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -124,10 +124,10 @@ namespace { public: spot::translator& trans; - automaton_printer printer; + automaton_printer printer{ltl_input}; - trans_processor(spot::translator& trans) - : trans(trans), printer(ltl_input) + explicit trans_processor(spot::translator& trans) + : trans(trans) { } diff --git a/bin/ltl2tgta.cc b/bin/ltl2tgta.cc index ab925c7ac..60afcf9e8 100644 --- a/bin/ltl2tgta.cc +++ b/bin/ltl2tgta.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2020, 2022 Laboratoire de Recherche et +// Copyright (C) 2012-2020, 2022-2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -168,7 +168,7 @@ namespace public: spot::translator& trans; - trans_processor(spot::translator& trans) + explicit trans_processor(spot::translator& trans) : trans(trans) { } diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 0dfa09985..3219beb75 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2020, 2022 Laboratoire de Recherche et +// Copyright (C) 2012-2020, 2022, 2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -264,55 +264,32 @@ end_error() struct statistics { - statistics() noexcept - : ok(false), - alternating(false), - status_str(nullptr), - status_code(0), - time(0), - states(0), - edges(0), - transitions(0), - acc(0), - scc(0), - nonacc_scc(0), - terminal_scc(0), - weak_scc(0), - strong_scc(0), - nondetstates(0), - nondeterministic(false), - terminal_aut(false), - weak_aut(false), - strong_aut(false) - { - } - // If OK is false, only the status_str, status_code, and time fields // should be valid. - bool ok; - bool alternating; - const char* status_str; - int status_code; - double time; - unsigned states; - unsigned edges; - unsigned long long transitions; - unsigned acc; - unsigned scc; - unsigned nonacc_scc; - unsigned terminal_scc; - unsigned weak_scc; - unsigned strong_scc; - unsigned nondetstates; - bool nondeterministic; - bool terminal_aut; - bool weak_aut; - bool strong_aut; + bool ok = false; + bool alternating = false; + const char* status_str = nullptr; + int status_code = 0; + double time = 0.0; + unsigned states = 0; + unsigned edges = 0; + unsigned long long transitions = 0; + unsigned acc = 0; + unsigned scc = 0; + unsigned nonacc_scc = 0; + unsigned terminal_scc = 0; + unsigned weak_scc = 0; + unsigned strong_scc = 0; + unsigned nondetstates = 0; + bool nondeterministic = false; + bool terminal_aut = false; + bool weak_aut = false; + bool strong_aut = false; std::vector product_states; std::vector product_transitions; std::vector product_scc; - bool ambiguous; - bool complete; + bool ambiguous = false; + bool complete = false; std::string hoa_str; static void @@ -581,7 +558,7 @@ namespace class xtranslator_runner final: public translator_runner { public: - xtranslator_runner(spot::bdd_dict_ptr dict) + explicit xtranslator_runner(spot::bdd_dict_ptr dict) : translator_runner(dict) { } @@ -1095,17 +1072,14 @@ namespace } // Make sure we do not translate the same formula twice. - if (!allow_dups) + if (!allow_dups && !unique_set.insert(f).second) { - if (!unique_set.insert(f).second) - { - if (!quiet) - std::cerr - << ("warning: This formula or its negation has already" - " been checked.\n Use --allow-dups if it " - "should not be ignored.\n\n"); - return 0; - } + if (!quiet) + std::cerr + << ("warning: This formula or its negation has already" + " been checked.\n Use --allow-dups if it " + "should not be ignored.\n\n"); + return 0; } int problems = 0; diff --git a/bin/ltldo.cc b/bin/ltldo.cc index ffbd4873e..6e7bf5ec7 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2020, 2022 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2015-2020, 2022-2023 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -209,7 +209,7 @@ namespace class xtranslator_runner final: public translator_runner { public: - xtranslator_runner(spot::bdd_dict_ptr dict) + explicit xtranslator_runner(spot::bdd_dict_ptr dict) : translator_runner(dict, true) { } @@ -224,8 +224,6 @@ namespace format(command, tools[translator_num].cmd); std::string cmd = command.str(); - //std::cerr << "Running [" << l << translator_num << "]: " - // << cmd << std::endl; timer.start(); int es = exec_with_timeout(cmd.c_str()); timer.stop(); @@ -312,7 +310,7 @@ namespace spot::printable_value inputf; public: - processor(spot::postprocessor& post) + explicit processor(spot::postprocessor& post) : runner(dict), best_printer(best_stream, best_format), post(post) { printer.add_stat('T', &cmdname); @@ -323,9 +321,7 @@ namespace best_printer.declare('f', &inputf); } - ~processor() - { - } + ~processor() override = default; int process_string(const std::string& input, diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index c9064368d..81e895d42 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.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. @@ -586,7 +586,7 @@ namespace fset_t unique_set; spot::relabeling_map relmap; - ltl_processor(spot::tl_simplifier& simpl) + explicit ltl_processor(spot::tl_simplifier& simpl) : simpl(simpl) { } @@ -722,7 +722,7 @@ namespace matched &= !syntactic_si || f.is_syntactic_stutter_invariant(); if (matched && (ap_n.min > 0 || ap_n.max >= 0)) { - auto s = atomic_prop_collect(f); + spot::atomic_prop_set* s = atomic_prop_collect(f); int n = s->size(); delete s; matched &= (ap_n.min <= 0) || (n >= ap_n.min); @@ -761,7 +761,7 @@ namespace aut = ltl_to_tgba_fm(f, simpl.get_dict(), true); 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; @@ -769,7 +769,7 @@ namespace } 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; @@ -843,12 +843,12 @@ namespace { // Sort the formulas alphabetically. std::map m; - for (auto& p: relmap) - m.emplace(str_psl(p.first), p.second); - for (auto& p: m) + for (const auto& [newformula, oldname]: relmap) + m.emplace(str_psl(newformula), oldname); + for (const auto& [newname, oldname]: m) stream_formula(opt->output_define->ostream() - << "#define " << p.first << " (", - p.second, filename, + << "#define " << newname << " (", + oldname, filename, std::to_string(linenum).c_str()) << ")\n"; } one_match = true; diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index aaea855a4..a2ec32cd1 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.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. @@ -152,7 +152,6 @@ static const struct argp_child children[] = { { &finput_argp_headless, 0, nullptr, 0 }, { &aoutput_argp, 0, nullptr, 0 }, - //{ &aoutput_o_format_argp, 0, nullptr, 0 }, { &misc_argp, 0, nullptr, 0 }, { nullptr, 0, nullptr, 0 } }; @@ -425,10 +424,6 @@ namespace auto sub_o = sub_outs_str.begin(); std::vector mealy_machines; - auto print_game = want_game ? - [](const spot::twa_graph_ptr& game)->void { dispatch_print_hoa(game); } - : [](const spot::twa_graph_ptr&)->void{}; - for (; sub_f != sub_form.end(); ++sub_f, ++sub_o) { spot::mealy_like m_like @@ -466,9 +461,11 @@ namespace assert((spptr->at(arena->get_init_state_number()) == false) && "Env needs first turn"); } - print_game(arena); if (want_game) - continue; + { + dispatch_print_hoa(arena); + continue; + } if (!spot::solve_game(arena, *gi)) { if (show_status) @@ -625,7 +622,7 @@ namespace } static void - split_aps(std::string arg, std::vector& where) + split_aps(const std::string& arg, std::vector& where) { std::istringstream aps(arg); std::string ap; diff --git a/bin/randltl.cc b/bin/randltl.cc index 986c437c1..749fcf373 100644 --- a/bin/randltl.cc +++ b/bin/randltl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2016, 2018-2019, 2022 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2012-2016, 2018-2019, 2022, 2023 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -65,7 +65,6 @@ enum { OPT_DUMP_PRIORITIES, OPT_DUPS, OPT_LTL_PRIORITIES, - OPT_PSL_PRIORITIES, OPT_SEED, OPT_SERE_PRIORITIES, OPT_TREE_SIZE, @@ -194,7 +193,6 @@ parse_opt(int key, char* arg, struct argp_state* as) case OPT_DUMP_PRIORITIES: opt_dump_priorities = true; break; - // case OPT_PSL_PRIORITIES: break; case OPT_SERE_PRIORITIES: opt_pS = arg; break;