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.
This commit is contained in:
Alexandre Duret-Lutz
parent
96c3972c5c
commit
09bbaa1e41
19 changed files with 133 additions and 178 deletions
|
|
@ -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 <error.h>
|
||||
#include <iostream>
|
||||
|
||||
|
||||
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<std::ofstream>(name, mode);
|
||||
if (!*of_)
|
||||
error(2, errno, "cannot open '%s'", name);
|
||||
os_ = of_;
|
||||
os_ = of_.get();
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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 <iosfwd>
|
||||
#include <memory>
|
||||
#include <fstream>
|
||||
#include <error.h>
|
||||
|
||||
class output_file
|
||||
{
|
||||
std::ostream* os_;
|
||||
std::ofstream* of_ = nullptr;
|
||||
std::unique_ptr<std::ofstream> 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_;
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 <iostream>
|
||||
#include <sstream>
|
||||
#include <memory>
|
||||
#include <spot/tl/print.hh>
|
||||
#include <spot/tl/length.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 formula_printer* outputnamer = nullptr;
|
||||
static std::unique_ptr<formula_printer> outputnamer;
|
||||
static std::map<std::string, std::unique_ptr<output_file>> 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<formula_printer>(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<formula_printer>(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;
|
||||
|
|
|
|||
|
|
@ -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 <argp.h>
|
||||
#include <closeout.h>
|
||||
#include <cstdlib>
|
||||
#include <unistd.h>
|
||||
#include <iostream>
|
||||
#include <signal.h>
|
||||
#include <sys/wait.h>
|
||||
#include <error.h>
|
||||
#include <spot/misc/tmpfile.hh>
|
||||
|
||||
static void
|
||||
|
|
|
|||
|
|
@ -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<int()> 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(); }
|
||||
|
|
|
|||
|
|
@ -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<char*>(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;
|
||||
|
|
|
|||
|
|
@ -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<spot::formula>
|
|||
|
||||
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);
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
{
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
{
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
{
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<double> product_states;
|
||||
std::vector<double> product_transitions;
|
||||
std::vector<double> 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;
|
||||
|
|
|
|||
14
bin/ltldo.cc
14
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<std::string> 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,
|
||||
|
|
|
|||
|
|
@ -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<std::string, spot::formula> 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;
|
||||
|
|
|
|||
|
|
@ -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<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)
|
||||
{
|
||||
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<std::string>& where)
|
||||
split_aps(const std::string& arg, std::vector<std::string>& where)
|
||||
{
|
||||
std::istringstream aps(arg);
|
||||
std::string ap;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue