alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

more code smells

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2023-01-06 11:55:34 +01:00
parent 7b0507a950
commit 39212bbcd2
19 changed files with 133 additions and 178 deletions
Download patch file Download diff file Expand all files Collapse all files

7
bin/common_file.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -21,7 +21,6 @@
#include <error.h> #include <error.h>
#include <iostream> #include <iostream>
output_file::output_file(const char* name, bool force_append) output_file::output_file(const char* name, bool force_append)
{ {
std::ios_base::openmode mode = std::ios_base::trunc; 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; os_ = &std::cout;
return; return;
} }
of_ = new std::ofstream(name, mode); of_ = std::make_unique<std::ofstream>(name, mode);
if (!*of_) if (!*of_)
error(2, errno, "cannot open '%s'", name); error(2, errno, "cannot open '%s'", name);
os_ = of_; os_ = of_.get();
} }

13
bin/common_file.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2022 Laboratoire de Recherche et Développement de // Copyright (C) 2015-2016, 2022-2023 Laboratoire de Recherche et
// l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -21,13 +21,13 @@
#include "common_sys.hh" #include "common_sys.hh"
#include <iosfwd> #include <iosfwd>
#include <memory>
#include <fstream> #include <fstream>
#include <error.h>
class output_file class output_file
{ {
std::ostream* os_; std::ostream* os_;
std::ofstream* of_ = nullptr; std::unique_ptr<std::ofstream> of_;
bool append_ = false; bool append_ = false;
public: public:
// Open a file for output. "-" is interpreted as stdout. // Open a file for output. "-" is interpreted as stdout.
@ -37,11 +37,6 @@ public:
void close(const std::string& name); void close(const std::string& name);
~output_file()
{
delete of_;
}
bool append() const bool append() const
{ {
return append_; return append_;

10
bin/common_finput.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // 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); (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() job_processor::~job_processor()
{ {
if (real_filename) if (real_filename)
@ -370,7 +364,7 @@ int
job_processor::run() job_processor::run()
{ {
int error = 0; int error = 0;
for (auto& j: jobs) for (const auto& j: jobs)
{ {
switch (j.type) switch (j.type)
{ {

16
bin/common_finput.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // 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 class job_processor
{ {
protected: 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: public:
job_processor(); job_processor() = default;
job_processor(const job_processor&) = delete;
job_processor& operator=(const job_processor&) = delete;
virtual ~job_processor(); virtual ~job_processor();
@ -84,10 +86,10 @@ public:
virtual int virtual int
run(); run();
char* real_filename; char* real_filename = nullptr;
long int col_to_read; long int col_to_read = 0;
char* prefix; char* prefix = nullptr;
char* suffix; char* suffix = nullptr;
}; };
// Report and error message or add a default job depending on whether // Report and error message or add a default job depending on whether

20
bin/common_output.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -23,6 +23,7 @@
#include "common_setup.hh" #include "common_setup.hh"
#include <iostream> #include <iostream>
#include <sstream> #include <sstream>
#include <memory>
#include <spot/tl/print.hh> #include <spot/tl/print.hh>
#include <spot/tl/length.hh> #include <spot/tl/length.hh>
#include <spot/tl/apcollect.hh> #include <spot/tl/apcollect.hh>
@ -297,9 +298,9 @@ namespace
}; };
} }
static formula_printer* format = nullptr; static std::unique_ptr<formula_printer> format;
static std::ostringstream outputname; static std::ostringstream outputname;
static formula_printer* outputnamer = nullptr; static std::unique_ptr<formula_printer> outputnamer;
static std::map<std::string, std::unique_ptr<output_file>> outputfiles; static std::map<std::string, std::unique_ptr<output_file>> outputfiles;
int int
@ -320,7 +321,7 @@ parse_opt_output(int key, char* arg, struct argp_state*)
output_format = lbt_output; output_format = lbt_output;
break; break;
case 'o': case 'o':
outputnamer = new formula_printer(outputname, arg); outputnamer = std::make_unique<formula_printer>(outputname, arg);
break; break;
case 'p': case 'p':
full_parenth = true; full_parenth = true;
@ -341,8 +342,7 @@ parse_opt_output(int key, char* arg, struct argp_state*)
output_format = wring_output; output_format = wring_output;
break; break;
case OPT_FORMAT: case OPT_FORMAT:
delete format; format = std::make_unique<formula_printer>(std::cout, arg);
format = new formula_printer(std::cout, arg);
break; break;
default: default:
return ARGP_ERR_UNKNOWN; 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 }; formula_with_location fl = { f, filename, linenum, prefix, suffix };
outputnamer->print(fl, ptimer); outputnamer->print(fl, ptimer);
std::string fname = outputname.str(); std::string fname = outputname.str();
auto p = outputfiles.emplace(fname, nullptr); auto [it, b] = outputfiles.try_emplace(fname, nullptr);
if (p.second) if (b)
p.first->second.reset(new output_file(fname.c_str())); it->second.reset(new output_file(fname.c_str()));
out = &p.first->second->ostream(); out = &it->second->ostream();
} }
output_formula(*out, f, ptimer, filename, linenum, prefix, suffix); output_formula(*out, f, ptimer, filename, linenum, prefix, suffix);
*out << output_terminator; *out << output_terminator;

7
bin/common_setup.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -20,13 +20,14 @@
#include "common_setup.hh" #include "common_setup.hh"
#include "common_aoutput.hh" #include "common_aoutput.hh"
#include "argp.h" #include <argp.h>
#include "closeout.h" #include <closeout.h>
#include <cstdlib> #include <cstdlib>
#include <unistd.h> #include <unistd.h>
#include <iostream> #include <iostream>
#include <signal.h> #include <signal.h>
#include <sys/wait.h> #include <sys/wait.h>
#include <error.h>
#include <spot/misc/tmpfile.hh> #include <spot/misc/tmpfile.hh>
static void static void

6
bin/common_setup.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2018, 2019 Laboratoire de Recherche et // Copyright (C) 2012-2013, 2018-2019, 2023 Laboratoire de Recherche
// Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -34,5 +34,5 @@ int protected_main(char** progname, std::function<int()> mainfun);
// Diagnose exceptions. // Diagnose exceptions.
[[noreturn]] void handle_any_exception(); [[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(); } #define END_EXCEPTION_PROTECT } catch (...) { handle_any_exception(); }

32
bin/common_trans.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // 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 } #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("delag", " %f>%O"),
SHORTHAND("lbt", " <%L>%O"), SHORTHAND("lbt", " <%L>%O"),
SHORTHAND("ltl2ba", " -f %s>%O"), SHORTHAND("ltl2ba", " -f %s>%O"),
@ -73,7 +73,7 @@ static shorthands_t shorthands_ltl[] = {
SHORTHAND("owl.* ltl-utilities\\b", " -f %f"), SHORTHAND("owl.* ltl-utilities\\b", " -f %f"),
}; };
static shorthands_t shorthands_autproc[] = { static const shorthands_t shorthands_autproc[] = {
SHORTHAND("autfilt", " %H>%O"), SHORTHAND("autfilt", " %H>%O"),
SHORTHAND("dra2dpa", " <%H>%O"), SHORTHAND("dra2dpa", " <%H>%O"),
SHORTHAND("dstar2tgba", " %H>%O"), SHORTHAND("dstar2tgba", " %H>%O"),
@ -85,7 +85,7 @@ static shorthands_t shorthands_autproc[] = {
" <%H>%O"), " <%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 std::cout
<< ("If a COMMANDFMT does not use any %-sequence, and starts with one of\n" << ("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 bool is_ref) noexcept
: spec(spec), cmd(spec), name(spec), reference(is_ref) : spec(spec), cmd(spec), name(spec), reference(is_ref)
{ {
@ -113,11 +114,11 @@ tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end,
{ {
if (*pos == '{') if (*pos == '{')
++count; ++count;
else if (*pos == '}') else if (*pos == '}' && --count == 0)
if (!--count)
{ {
name = strndup(cmd + 1, pos - cmd - 1); name = strndup(cmd + 1, pos - cmd - 1);
cmd = pos + 1; cmd = pos + 1;
// skip leading whitespace
while (*cmd == ' ' || *cmd == '\t') while (*cmd == ' ' || *cmd == '\t')
++cmd; ++cmd;
break; break;
@ -147,11 +148,11 @@ tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end,
auto& p = *begin++; auto& p = *begin++;
if (std::regex_search(basename, p.rprefix)) if (std::regex_search(basename, p.rprefix))
{ {
int m = strlen(p.suffix); size_t m = strlen(p.suffix);
int q = strlen(cmd); size_t q = strlen(cmd);
char* tmp = static_cast<char*>(malloc(q + m + 1)); char* tmp = static_cast<char*>(malloc(q + m + 1));
strcpy(tmp, cmd); memcpy(tmp, cmd, q);
strcpy(tmp + q, p.suffix); memcpy(tmp + q, p.suffix, m + 1);
cmd = tmp; cmd = tmp;
allocated = true; allocated = true;
break; break;
@ -490,9 +491,8 @@ read_stdout_of_command(char* const* args)
if (close(cout_pipe[1]) < 0) if (close(cout_pipe[1]) < 0)
error(2, errno, "closing write-side of pipe failed"); error(2, errno, "closing write-side of pipe failed");
std::string buffer(32, 0);
std::string results; std::string results;
int bytes_read; ssize_t bytes_read;
for (;;) for (;;)
{ {
static char buffer[512]; static char buffer[512];
@ -612,7 +612,7 @@ get_arg(const char*& cmd)
{ {
const char* start = cmd; const char* start = cmd;
std::string arg; std::string arg;
while (int c = *cmd) while (char c = *cmd)
{ {
switch (c) switch (c)
{ {
@ -642,14 +642,14 @@ get_arg(const char*& cmd)
goto end_loop; goto end_loop;
case '\'': case '\'':
{ {
int d = 0; char d = '\0';
while ((d = *++cmd)) while ((d = *++cmd))
{ {
if (d == '\'') if (d == '\'')
break; break;
arg.push_back(d); arg.push_back(d);
} }
if (d == 0) if (d == '\0')
return nullptr; return nullptr;
} }
break; break;

15
bin/common_trans.hh
View file

@ -51,7 +51,8 @@ struct tool_spec
// Whether the tool is a reference. // Whether the tool is a reference.
bool 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; bool is_ref) noexcept;
tool_spec(const tool_spec& other) noexcept; tool_spec(const tool_spec& other) noexcept;
tool_spec& operator=(const tool_spec& other); tool_spec& operator=(const tool_spec& other);
@ -71,7 +72,7 @@ struct quoted_formula final: public spot::printable_value<spot::formula>
struct filed_formula final: public spot::printable 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 struct filed_automaton final: public spot::printable
{ {
filed_automaton() filed_automaton() = default;
{
}
void print(std::ostream& os, const char* pos) const override; void print(std::ostream& os, const char* pos) const override;
@ -112,7 +111,7 @@ struct printable_result_filename final:
unsigned translator_num; unsigned translator_num;
printable_result_filename(); printable_result_filename();
~printable_result_filename(); ~printable_result_filename() override;
void reset(unsigned n); void reset(unsigned n);
void cleanup(); void cleanup();
@ -126,7 +125,7 @@ protected:
spot::bdd_dict_ptr dict; spot::bdd_dict_ptr dict;
// Round-specific variables // Round-specific variables
quoted_formula ltl_formula; quoted_formula ltl_formula;
filed_formula filename_formula = ltl_formula; filed_formula filename_formula{ltl_formula};
// Run-specific variables // Run-specific variables
printable_result_filename output; printable_result_filename output;
public: public:
@ -151,7 +150,7 @@ protected:
public: public:
using spot::formater::has; using spot::formater::has;
autproc_runner(// whether we accept the absence of output explicit autproc_runner(// whether we accept the absence of output
// specifier // specifier
bool no_output_allowed = false); bool no_output_allowed = false);
void round_automaton(spot::const_twa_graph_ptr aut, unsigned serial); void round_automaton(spot::const_twa_graph_ptr aut, unsigned serial);

4
bin/dstar2tgba.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -117,7 +117,7 @@ namespace
spot::postprocessor& post; spot::postprocessor& post;
automaton_printer printer; 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) : hoa_processor(spot::make_bdd_dict()), post(post), printer(aut_input)
{ {
} }

4
bin/genaut.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // 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 static void
run_jobs() run_jobs()
{ {
for (auto& j: jobs) for (const auto& j: jobs)
{ {
int inc = (j.range.max < j.range.min) ? -1 : 1; int inc = (j.range.max < j.range.min) ? -1 : 1;
int n = j.range.min; int n = j.range.min;

6
bin/genltl.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2015-2019, 2022 Laboratoire de Recherche et // Copyright (C) 2012, 2013, 2015-2019, 2022-2023 Laboratoire de
// Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // 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 static void
run_jobs() run_jobs()
{ {
for (auto& j: jobs) for (const auto& j: jobs)
{ {
int inc = (j.range.max < j.range.min) ? -1 : 1; int inc = (j.range.max < j.range.min) ? -1 : 1;
int n = j.range.min; int n = j.range.min;

8
bin/ltl2tgba.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -124,10 +124,10 @@ namespace
{ {
public: public:
spot::translator& trans; spot::translator& trans;
automaton_printer printer; automaton_printer printer{ltl_input};
trans_processor(spot::translator& trans) explicit trans_processor(spot::translator& trans)
: trans(trans), printer(ltl_input) : trans(trans)
{ {
} }

4
bin/ltl2tgta.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -168,7 +168,7 @@ namespace
public: public:
spot::translator& trans; spot::translator& trans;
trans_processor(spot::translator& trans) explicit trans_processor(spot::translator& trans)
: trans(trans) : trans(trans)
{ {
} }

74
bin/ltlcross.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -264,55 +264,32 @@ end_error()
struct statistics 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 // If OK is false, only the status_str, status_code, and time fields
// should be valid. // should be valid.
bool ok; bool ok = false;
bool alternating; bool alternating = false;
const char* status_str; const char* status_str = nullptr;
int status_code; int status_code = 0;
double time; double time = 0.0;
unsigned states; unsigned states = 0;
unsigned edges; unsigned edges = 0;
unsigned long long transitions; unsigned long long transitions = 0;
unsigned acc; unsigned acc = 0;
unsigned scc; unsigned scc = 0;
unsigned nonacc_scc; unsigned nonacc_scc = 0;
unsigned terminal_scc; unsigned terminal_scc = 0;
unsigned weak_scc; unsigned weak_scc = 0;
unsigned strong_scc; unsigned strong_scc = 0;
unsigned nondetstates; unsigned nondetstates = 0;
bool nondeterministic; bool nondeterministic = false;
bool terminal_aut; bool terminal_aut = false;
bool weak_aut; bool weak_aut = false;
bool strong_aut; bool strong_aut = false;
std::vector<double> product_states; std::vector<double> product_states;
std::vector<double> product_transitions; std::vector<double> product_transitions;
std::vector<double> product_scc; std::vector<double> product_scc;
bool ambiguous; bool ambiguous = false;
bool complete; bool complete = false;
std::string hoa_str; std::string hoa_str;
static void static void
@ -581,7 +558,7 @@ namespace
class xtranslator_runner final: public translator_runner class xtranslator_runner final: public translator_runner
{ {
public: public:
xtranslator_runner(spot::bdd_dict_ptr dict) explicit xtranslator_runner(spot::bdd_dict_ptr dict)
: translator_runner(dict) : translator_runner(dict)
{ {
} }
@ -1095,9 +1072,7 @@ namespace
} }
// Make sure we do not translate the same formula twice. // 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) if (!quiet)
std::cerr std::cerr
@ -1106,7 +1081,6 @@ namespace
"should not be ignored.\n\n"); "should not be ignored.\n\n");
return 0; return 0;
} }
}
int problems = 0; int problems = 0;

14
bin/ltldo.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015-2020, 2022 Laboratoire de Recherche et Développement // Copyright (C) 2015-2020, 2022-2023 Laboratoire de Recherche et
// de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -209,7 +209,7 @@ namespace
class xtranslator_runner final: public translator_runner class xtranslator_runner final: public translator_runner
{ {
public: public:
xtranslator_runner(spot::bdd_dict_ptr dict) explicit xtranslator_runner(spot::bdd_dict_ptr dict)
: translator_runner(dict, true) : translator_runner(dict, true)
{ {
} }
@ -224,8 +224,6 @@ namespace
format(command, tools[translator_num].cmd); format(command, tools[translator_num].cmd);
std::string cmd = command.str(); std::string cmd = command.str();
//std::cerr << "Running [" << l << translator_num << "]: "
// << cmd << std::endl;
timer.start(); timer.start();
int es = exec_with_timeout(cmd.c_str()); int es = exec_with_timeout(cmd.c_str());
timer.stop(); timer.stop();
@ -312,7 +310,7 @@ namespace
spot::printable_value<std::string> inputf; spot::printable_value<std::string> inputf;
public: public:
processor(spot::postprocessor& post) explicit processor(spot::postprocessor& post)
: runner(dict), best_printer(best_stream, best_format), post(post) : runner(dict), best_printer(best_stream, best_format), post(post)
{ {
printer.add_stat('T', &cmdname); printer.add_stat('T', &cmdname);
@ -323,9 +321,7 @@ namespace
best_printer.declare('f', &inputf); best_printer.declare('f', &inputf);
} }
~processor() ~processor() override = default;
{
}
int int
process_string(const std::string& input, process_string(const std::string& input,

20
bin/ltlfilt.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -586,7 +586,7 @@ namespace
fset_t unique_set; fset_t unique_set;
spot::relabeling_map relmap; spot::relabeling_map relmap;
ltl_processor(spot::tl_simplifier& simpl) explicit ltl_processor(spot::tl_simplifier& simpl)
: simpl(simpl) : simpl(simpl)
{ {
} }
@ -722,7 +722,7 @@ namespace
matched &= !syntactic_si || f.is_syntactic_stutter_invariant(); matched &= !syntactic_si || f.is_syntactic_stutter_invariant();
if (matched && (ap_n.min > 0 || ap_n.max >= 0)) 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(); int n = s->size();
delete s; delete s;
matched &= (ap_n.min <= 0) || (n >= ap_n.min); matched &= (ap_n.min <= 0) || (n >= ap_n.min);
@ -761,7 +761,7 @@ namespace
aut = ltl_to_tgba_fm(f, simpl.get_dict(), true); aut = ltl_to_tgba_fm(f, simpl.get_dict(), true);
if (matched && !opt->acc_words.empty()) 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()) if (spot::product(aut, word_aut)->is_empty())
{ {
matched = false; matched = false;
@ -769,7 +769,7 @@ namespace
} }
if (matched && !opt->rej_words.empty()) 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()) if (!spot::product(aut, word_aut)->is_empty())
{ {
matched = false; matched = false;
@ -843,12 +843,12 @@ namespace
{ {
// Sort the formulas alphabetically. // Sort the formulas alphabetically.
std::map<std::string, spot::formula> m; std::map<std::string, spot::formula> m;
for (auto& p: relmap) for (const auto& [newformula, oldname]: relmap)
m.emplace(str_psl(p.first), p.second); m.emplace(str_psl(newformula), oldname);
for (auto& p: m) for (const auto& [newname, oldname]: m)
stream_formula(opt->output_define->ostream() stream_formula(opt->output_define->ostream()
<< "#define " << p.first << " (", << "#define " << newname << " (",
p.second, filename, oldname, filename,
std::to_string(linenum).c_str()) << ")\n"; std::to_string(linenum).c_str()) << ")\n";
} }
one_match = true; one_match = true;

13
bin/ltlsynt.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // 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 }, { &finput_argp_headless, 0, nullptr, 0 },
{ &aoutput_argp, 0, nullptr, 0 }, { &aoutput_argp, 0, nullptr, 0 },
//{ &aoutput_o_format_argp, 0, nullptr, 0 },
{ &misc_argp, 0, nullptr, 0 }, { &misc_argp, 0, nullptr, 0 },
{ nullptr, 0, nullptr, 0 } { nullptr, 0, nullptr, 0 }
}; };
@ -425,10 +424,6 @@ namespace
auto sub_o = sub_outs_str.begin(); auto sub_o = sub_outs_str.begin();
std::vector<spot::mealy_like> mealy_machines; std::vector<spot::mealy_like> 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) for (; sub_f != sub_form.end(); ++sub_f, ++sub_o)
{ {
spot::mealy_like m_like spot::mealy_like m_like
@ -466,9 +461,11 @@ namespace
assert((spptr->at(arena->get_init_state_number()) == false) assert((spptr->at(arena->get_init_state_number()) == false)
&& "Env needs first turn"); && "Env needs first turn");
} }
print_game(arena);
if (want_game) if (want_game)
{
dispatch_print_hoa(arena);
continue; continue;
}
if (!spot::solve_game(arena, *gi)) if (!spot::solve_game(arena, *gi))
{ {
if (show_status) if (show_status)
@ -625,7 +622,7 @@ namespace
} }
static void static void
split_aps(std::string arg, std::vector<std::string>& where) split_aps(const std::string& arg, std::vector<std::string>& where)
{ {
std::istringstream aps(arg); std::istringstream aps(arg);
std::string ap; std::string ap;

6
bin/randltl.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012-2016, 2018-2019, 2022 Laboratoire de Recherche // Copyright (C) 2012-2016, 2018-2019, 2022, 2023 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -65,7 +65,6 @@ enum {
OPT_DUMP_PRIORITIES, OPT_DUMP_PRIORITIES,
OPT_DUPS, OPT_DUPS,
OPT_LTL_PRIORITIES, OPT_LTL_PRIORITIES,
OPT_PSL_PRIORITIES,
OPT_SEED, OPT_SEED,
OPT_SERE_PRIORITIES, OPT_SERE_PRIORITIES,
OPT_TREE_SIZE, OPT_TREE_SIZE,
@ -194,7 +193,6 @@ parse_opt(int key, char* arg, struct argp_state* as)
case OPT_DUMP_PRIORITIES: case OPT_DUMP_PRIORITIES:
opt_dump_priorities = true; opt_dump_priorities = true;
break; break;
// case OPT_PSL_PRIORITIES: break;
case OPT_SERE_PRIORITIES: case OPT_SERE_PRIORITIES:
opt_pS = arg; opt_pS = arg;
break; break;