fix some code smells reported by sonarcloud
* bench/dtgbasat/gen.py, bin/autcross.cc, bin/autfilt.cc, bin/common_aoutput.cc, bin/common_aoutput.hh: Various cleanups.
This commit is contained in:
parent
716bb781eb
commit
05edab3f5a
5 changed files with 51 additions and 66 deletions
|
|
@ -1,5 +1,5 @@
|
||||||
#!/usr/bin/env python3
|
#!/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).
|
# l'Epita (LRDE).
|
||||||
#
|
#
|
||||||
# This file is part of Spot, a model checking library.
|
# This file is part of Spot, a model checking library.
|
||||||
|
|
@ -55,12 +55,12 @@ class BenchConfig(object):
|
||||||
if line[0] == '#' or line.isspace():
|
if line[0] == '#' or line.isspace():
|
||||||
continue
|
continue
|
||||||
elif line[0:2] == "sh":
|
elif line[0:2] == "sh":
|
||||||
sh = re.search('sh (.+?)$', line).group(1)
|
sh = re.search('sh (.+)$', line).group(1)
|
||||||
continue
|
continue
|
||||||
else:
|
else:
|
||||||
name = re.search('(.+?):', line).group(1)
|
name = re.search('(.+?):', line).group(1)
|
||||||
code = 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)
|
b = Bench(name=name, code=code, xoptions=xoptions)
|
||||||
self.l.append(b)
|
self.l.append(b)
|
||||||
self.sh.append(sh)
|
self.sh.append(sh)
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- 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).
|
// 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.
|
||||||
|
|
@ -549,7 +549,7 @@ namespace
|
||||||
{
|
{
|
||||||
if (!quiet)
|
if (!quiet)
|
||||||
std::cerr << "info: building " << autname(i, is_really_comp(i))
|
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";
|
<< " requires more acceptance sets than supported\n";
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
@ -557,14 +557,14 @@ namespace
|
||||||
if (verbose)
|
if (verbose)
|
||||||
std::cerr << "info: check_empty "
|
std::cerr << "info: check_empty "
|
||||||
<< autname(i, is_really_comp(i))
|
<< 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);
|
auto w = aut_i->intersecting_word(aut_j);
|
||||||
if (w)
|
if (w)
|
||||||
{
|
{
|
||||||
std::ostream& err = global_error();
|
std::ostream& err = global_error();
|
||||||
err << "error: " << autname(i, is_really_comp(i))
|
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"
|
<< (" is nonempty; both automata accept the infinite word:\n"
|
||||||
" ");
|
" ");
|
||||||
example() << *w << '\n';
|
example() << *w << '\n';
|
||||||
|
|
@ -613,7 +613,7 @@ namespace
|
||||||
return src.str();
|
return src.str();
|
||||||
}();
|
}();
|
||||||
|
|
||||||
input_statistics.push_back(in_statistics());
|
input_statistics.emplace_back(in_statistics());
|
||||||
|
|
||||||
input_statistics[round_num].input_source = std::move(source);
|
input_statistics[round_num].input_source = std::move(source);
|
||||||
if (auto name = input->get_named_prop<std::string>("automaton-name"))
|
if (auto name = input->get_named_prop<std::string>("automaton-name"))
|
||||||
|
|
@ -658,7 +658,7 @@ namespace
|
||||||
problems += prob;
|
problems += prob;
|
||||||
}
|
}
|
||||||
spot::cleanup_tmpfiles();
|
spot::cleanup_tmpfiles();
|
||||||
output_statistics.push_back(std::move(stats));
|
output_statistics.emplace_back(std::move(stats));
|
||||||
|
|
||||||
if (verbose)
|
if (verbose)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- 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).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -448,7 +448,7 @@ struct canon_aut
|
||||||
std::vector<tr_t> edges;
|
std::vector<tr_t> edges;
|
||||||
std::string acc;
|
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())
|
: num_states(aut->num_states())
|
||||||
, edges(aut->edge_vector().begin() + 1,
|
, edges(aut->edge_vector().begin() + 1,
|
||||||
aut->edge_vector().end())
|
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);
|
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
|
static int
|
||||||
parse_opt(int key, char* arg, struct argp_state*)
|
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<int>::max());
|
opt_nth = parse_range(arg, 0, std::numeric_limits<int>::max());
|
||||||
break;
|
break;
|
||||||
case 'u':
|
case 'u':
|
||||||
opt->uniq = std::unique_ptr<unique_aut_t>(new std::set<canon_aut>());
|
opt->uniq = std::make_unique<unique_aut_t>();
|
||||||
break;
|
break;
|
||||||
case 'v':
|
case 'v':
|
||||||
opt_invert = true;
|
opt_invert = true;
|
||||||
break;
|
break;
|
||||||
case 'x':
|
case 'x':
|
||||||
{
|
if (const char* opt = extra_options.parse_options(arg))
|
||||||
const char* opt = extra_options.parse_options(arg);
|
error(2, 0, "failed to parse --options near '%s'", opt);
|
||||||
if (opt)
|
|
||||||
error(2, 0, "failed to parse --options near '%s'", opt);
|
|
||||||
}
|
|
||||||
break;
|
break;
|
||||||
case OPT_ALIASES:
|
case OPT_ALIASES:
|
||||||
opt_aliases = XARGMATCH("--aliases", arg, aliases_args, aliases_types);
|
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;
|
opt_art_sccs_set = true;
|
||||||
break;
|
break;
|
||||||
case OPT_ACCEPT_WORD:
|
case OPT_ACCEPT_WORD:
|
||||||
try
|
opt->acc_words.emplace_back(word_to_aut(arg, "accept-word"));
|
||||||
{
|
|
||||||
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());
|
|
||||||
}
|
|
||||||
break;
|
break;
|
||||||
case OPT_ACCEPTANCE_IS:
|
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);
|
"%d should be followed by a comma and WORD", res);
|
||||||
arg = endptr + 1;
|
arg = endptr + 1;
|
||||||
}
|
}
|
||||||
try
|
opt->hl_words.emplace_back(word_to_aut(arg, "highlight-word"), res);
|
||||||
{
|
|
||||||
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());
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
break;
|
break;
|
||||||
case OPT_HIGHLIGHT_LANGUAGES:
|
case OPT_HIGHLIGHT_LANGUAGES:
|
||||||
|
|
@ -1157,16 +1152,7 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
opt_art_sccs_set = true;
|
opt_art_sccs_set = true;
|
||||||
break;
|
break;
|
||||||
case OPT_REJECT_WORD:
|
case OPT_REJECT_WORD:
|
||||||
try
|
opt->rej_words.emplace_back(word_to_aut(arg, "reject-word"));
|
||||||
{
|
|
||||||
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());
|
|
||||||
}
|
|
||||||
break;
|
break;
|
||||||
case OPT_REM_AP:
|
case OPT_REM_AP:
|
||||||
opt->rem_ap.add_ap(arg);
|
opt->rem_ap.add_ap(arg);
|
||||||
|
|
@ -1291,7 +1277,7 @@ namespace
|
||||||
static
|
static
|
||||||
bool match_acceptance(spot::twa_graph_ptr aut)
|
bool match_acceptance(spot::twa_graph_ptr aut)
|
||||||
{
|
{
|
||||||
auto& acc = aut->acc();
|
const spot::acc_cond& acc = aut->acc();
|
||||||
switch (opt_acceptance_is)
|
switch (opt_acceptance_is)
|
||||||
{
|
{
|
||||||
case ACC_Any:
|
case ACC_Any:
|
||||||
|
|
@ -1346,8 +1332,7 @@ namespace
|
||||||
{
|
{
|
||||||
bool max;
|
bool max;
|
||||||
bool odd;
|
bool odd;
|
||||||
bool is_p = acc.is_parity(max, odd, true);
|
if (!acc.is_parity(max, odd, true))
|
||||||
if (!is_p)
|
|
||||||
return false;
|
return false;
|
||||||
switch (opt_acceptance_is)
|
switch (opt_acceptance_is)
|
||||||
{
|
{
|
||||||
|
|
@ -1460,7 +1445,7 @@ namespace
|
||||||
if (matched && opt_acceptance_is)
|
if (matched && opt_acceptance_is)
|
||||||
matched = match_acceptance(aut);
|
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);
|
spot::scc_info si(aut);
|
||||||
unsigned n = si.scc_count();
|
unsigned n = si.scc_count();
|
||||||
|
|
@ -1540,14 +1525,14 @@ namespace
|
||||||
&& spot::contains(aut, opt->equivalent_pos);
|
&& spot::contains(aut, opt->equivalent_pos);
|
||||||
|
|
||||||
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;
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
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;
|
||||||
|
|
@ -1681,13 +1666,13 @@ namespace
|
||||||
aut->accepting_run()->highlight(opt_highlight_accepting_run);
|
aut->accepting_run()->highlight(opt_highlight_accepting_run);
|
||||||
|
|
||||||
if (!opt->hl_words.empty())
|
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())
|
if (aut->acc().uses_fin_acceptance())
|
||||||
error(2, 0,
|
error(2, 0,
|
||||||
"--highlight-word does not yet work with Fin acceptance");
|
"--highlight-word does not yet work with Fin acceptance");
|
||||||
if (auto run = spot::product(aut, word_aut.first)->accepting_run())
|
if (auto run = spot::product(aut, word_aut)->accepting_run())
|
||||||
run->project(aut)->highlight(word_aut.second);
|
run->project(aut)->highlight(color);
|
||||||
}
|
}
|
||||||
|
|
||||||
timer.stop();
|
timer.stop();
|
||||||
|
|
|
||||||
|
|
@ -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.
|
||||||
|
|
@ -453,7 +453,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
|
||||||
const spot::const_twa_graph_ptr& aut,
|
const spot::const_twa_graph_ptr& aut,
|
||||||
spot::formula f,
|
spot::formula f,
|
||||||
const char* filename, int loc,
|
const char* filename, int loc,
|
||||||
spot::process_timer& ptimer,
|
const spot::process_timer& ptimer,
|
||||||
const char* csv_prefix, const char* csv_suffix)
|
const char* csv_prefix, const char* csv_suffix)
|
||||||
{
|
{
|
||||||
timer_ = ptimer;
|
timer_ = ptimer;
|
||||||
|
|
@ -633,10 +633,10 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
|
||||||
outputnamer.print(haut, aut, f, filename, loc, ptimer,
|
outputnamer.print(haut, aut, f, filename, loc, ptimer,
|
||||||
csv_prefix, csv_suffix);
|
csv_prefix, csv_suffix);
|
||||||
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 it.
|
// Output it.
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2014-2018, 2020, 2022 Laboratoire de Recherche et
|
// Copyright (C) 2014-2018, 2020, 2022, 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.
|
||||||
//
|
//
|
||||||
|
|
@ -155,7 +155,7 @@ public:
|
||||||
print(const spot::const_parsed_aut_ptr& haut,
|
print(const spot::const_parsed_aut_ptr& haut,
|
||||||
const spot::const_twa_graph_ptr& aut,
|
const spot::const_twa_graph_ptr& aut,
|
||||||
spot::formula f,
|
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);
|
const char* csv_prefix, const char* csv_suffix);
|
||||||
|
|
||||||
private:
|
private:
|
||||||
|
|
@ -196,7 +196,7 @@ class automaton_printer
|
||||||
std::map<std::string, std::unique_ptr<output_file>> outputfiles;
|
std::map<std::string, std::unique_ptr<output_file>> outputfiles;
|
||||||
|
|
||||||
public:
|
public:
|
||||||
automaton_printer(stat_style input = no_input);
|
explicit automaton_printer(stat_style input = no_input);
|
||||||
~automaton_printer();
|
~automaton_printer();
|
||||||
|
|
||||||
void
|
void
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue