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

ltlcross, ltldo: rename "translators" to "tools" in the code

Browse source 
* bin/common_trans.cc, bin/common_trans.hh, bin/ltlcross.cc,
bin/ltldo.cc: Rename translator_spec and translators to tool_spec and
tools, so that we can reuse these structures for automata tools
in a future autcross.
This commit is contained in:
Alexandre Duret-Lutz 2017-07-26 14:18:46 +02:00
parent 7bfe06b30b
commit 9690c2230d
4 changed files with 30 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

18
bin/common_trans.cc
View file

@ -73,7 +73,7 @@ static void show_shorthands()
} }
translator_spec::translator_spec(const char* spec) tool_spec::tool_spec(const char* spec)
: spec(spec), cmd(spec), name(spec) : spec(spec), cmd(spec), name(spec)
{ {
if (*cmd == '{') if (*cmd == '{')
@ -134,7 +134,7 @@ translator_spec::translator_spec(const char* spec)
cmd = strdup(cmd); cmd = strdup(cmd);
} }
translator_spec::translator_spec(const translator_spec& other) tool_spec::tool_spec(const tool_spec& other)
: spec(other.spec), cmd(other.cmd), name(other.name) : spec(other.spec), cmd(other.cmd), name(other.name)
{ {
if (cmd != spec) if (cmd != spec)
@ -143,7 +143,7 @@ translator_spec::translator_spec(const translator_spec& other)
name = strdup(name); name = strdup(name);
} }
translator_spec& translator_spec::operator=(const translator_spec& other) tool_spec& tool_spec::operator=(const tool_spec& other)
{ {
spec = other.spec; spec = other.spec;
cmd = other.cmd; cmd = other.cmd;
@ -155,7 +155,7 @@ translator_spec& translator_spec::operator=(const translator_spec& other)
return *this; return *this;
} }
translator_spec::~translator_spec() tool_spec::~tool_spec()
{ {
if (name != spec) if (name != spec)
free(const_cast<char*>(name)); free(const_cast<char*>(name));
@ -163,7 +163,7 @@ translator_spec::~translator_spec()
free(const_cast<char*>(cmd)); free(const_cast<char*>(cmd));
} }
std::vector<translator_spec> translators; std::vector<tool_spec> tools;
void void
quoted_string::print(std::ostream& os, const char*) const quoted_string::print(std::ostream& os, const char*) const
@ -296,14 +296,14 @@ translator_runner::translator_runner(spot::bdd_dict_ptr dict,
declare('T', &output); declare('T', &output);
declare('O', &output); declare('O', &output);
size_t s = translators.size(); size_t s = tools.size();
assert(s); assert(s);
for (size_t n = 0; n < s; ++n) for (size_t n = 0; n < s; ++n)
{ {
// Check that each translator uses at least one input and // Check that each translator uses at least one input and
// one output. // one output.
std::vector<bool> has(256); std::vector<bool> has(256);
const translator_spec& t = translators[n]; const tool_spec& t = tools[n];
scan(t.cmd, has); scan(t.cmd, has);
if (!(has['f'] || has['s'] || has['l'] || has['w'] if (!(has['f'] || has['s'] || has['l'] || has['w']
|| has['F'] || has['S'] || has['L'] || has['W'])) || has['F'] || has['S'] || has['L'] || has['W']))
@ -317,7 +317,7 @@ translator_runner::translator_runner(spot::bdd_dict_ptr dict,
error(2, 0, "no output %%-sequence in '%s'.\n Use " error(2, 0, "no output %%-sequence in '%s'.\n Use "
"%%O to indicate where the automaton is output.", "%%O to indicate where the automaton is output.",
t.spec); t.spec);
// Remember the %-sequences used by all translators. // Remember the %-sequences used by all tools.
prime(t.cmd); prime(t.cmd);
} }
} }
@ -675,7 +675,7 @@ static int parse_opt_trans(int key, char* arg, struct argp_state*)
switch (key) switch (key)
{ {
case 't': case 't':
translators.push_back(arg); tools.push_back(arg);
break; break;
case 'T': case 'T':
timeout = to_pos_int(arg); timeout = to_pos_int(arg);

12
bin/common_trans.hh
View file

@ -31,7 +31,7 @@
extern const struct argp trans_argp; extern const struct argp trans_argp;
extern bool opt_relabel; extern bool opt_relabel;
struct translator_spec struct tool_spec
{ {
// The translator command, as specified on the command-line. // The translator command, as specified on the command-line.
// If this has the form of // If this has the form of
@ -44,13 +44,13 @@ struct translator_spec
// name of the translator (or spec) // name of the translator (or spec)
const char* name; const char* name;
translator_spec(const char* spec); tool_spec(const char* spec);
translator_spec(const translator_spec& other); tool_spec(const tool_spec& other);
translator_spec& operator=(const translator_spec& other); tool_spec& operator=(const tool_spec& other);
~translator_spec(); ~tool_spec();
}; };
extern std::vector<translator_spec> translators; extern std::vector<tool_spec> tools;
struct quoted_string final: public spot::printable_value<std::string> struct quoted_string final: public spot::printable_value<std::string>
{ {

18
bin/ltlcross.cc
View file

@ -423,7 +423,7 @@ parse_opt(int key, char* arg, struct argp_state*)
if (arg[0] == '-' && !arg[1]) if (arg[0] == '-' && !arg[1])
jobs.emplace_back(arg, true); jobs.emplace_back(arg, true);
else else
translators.push_back(arg); tools.push_back(arg);
break; break;
case OPT_AUTOMATA: case OPT_AUTOMATA:
opt_automata = true; opt_automata = true;
@ -515,7 +515,7 @@ namespace
output.reset(translator_num); output.reset(translator_num);
std::ostringstream command; std::ostringstream command;
format(command, translators[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 << "]: " std::cerr << "Running [" << l << translator_num << "]: "
@ -985,7 +985,7 @@ namespace
// These store the result of the translation of the positive and // These store the result of the translation of the positive and
// negative formulas. // negative formulas.
size_t m = translators.size(); size_t m = tools.size();
std::vector<spot::twa_graph_ptr> pos(m); std::vector<spot::twa_graph_ptr> pos(m);
std::vector<spot::twa_graph_ptr> neg(m); std::vector<spot::twa_graph_ptr> neg(m);
// These store the complement of the above results, when we can // These store the complement of the above results, when we can
@ -1408,7 +1408,7 @@ print_stats_csv(const char* filename)
output_file outf(filename); output_file outf(filename);
std::ostream& out = outf.ostream(); std::ostream& out = outf.ostream();
unsigned ntrans = translators.size(); unsigned ntrans = tools.size();
unsigned rounds = vstats.size(); unsigned rounds = vstats.size();
assert(rounds == formulas.size()); assert(rounds == formulas.size());
@ -1427,7 +1427,7 @@ print_stats_csv(const char* filename)
out << '"'; out << '"';
spot::escape_rfc4180(out, formulas[r]); spot::escape_rfc4180(out, formulas[r]);
out << "\",\""; out << "\",\"";
spot::escape_rfc4180(out, translators[t].name); spot::escape_rfc4180(out, tools[t].name);
out << "\","; out << "\",";
vstats[r][t].to_csv(out, !opt_omit); vstats[r][t].to_csv(out, !opt_omit);
out << '\n'; out << '\n';
@ -1444,16 +1444,16 @@ print_stats_json(const char* filename)
output_file outf(filename); output_file outf(filename);
std::ostream& out = outf.ostream(); std::ostream& out = outf.ostream();
unsigned ntrans = translators.size(); unsigned ntrans = tools.size();
unsigned rounds = vstats.size(); unsigned rounds = vstats.size();
assert(rounds == formulas.size()); assert(rounds == formulas.size());
out << "{\n \"tool\": [\n \""; out << "{\n \"tool\": [\n \"";
spot::escape_str(out, translators[0].name); spot::escape_str(out, tools[0].name);
for (unsigned t = 1; t < ntrans; ++t) for (unsigned t = 1; t < ntrans; ++t)
{ {
out << "\",\n \""; out << "\",\n \"";
spot::escape_str(out, translators[t].name); spot::escape_str(out, tools[t].name);
} }
out << "\"\n ],\n \"formula\": [\n \""; out << "\"\n ],\n \"formula\": [\n \"";
spot::escape_str(out, formulas[0]); spot::escape_str(out, formulas[0]);
@ -1495,7 +1495,7 @@ main(int argc, char** argv)
check_no_formula(); check_no_formula();
if (translators.empty()) if (tools.empty())
error(2, 0, "No translator to run? Run '%s --help' for usage.", error(2, 0, "No translator to run? Run '%s --help' for usage.",
program_name); program_name);

12
bin/ltldo.cc
View file

@ -171,7 +171,7 @@ parse_opt(int key, char* arg, struct argp_state*)
if (arg[0] == '-' && !arg[1]) if (arg[0] == '-' && !arg[1])
jobs.emplace_back(arg, true); jobs.emplace_back(arg, true);
else else
translators.push_back(arg); tools.push_back(arg);
break; break;
default: default:
return ARGP_ERR_UNKNOWN; return ARGP_ERR_UNKNOWN;
@ -195,7 +195,7 @@ namespace
output.reset(translator_num); output.reset(translator_num);
std::ostringstream command; std::ostringstream command;
format(command, translators[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 << "]: " //std::cerr << "Running [" << l << translator_num << "]: "
@ -339,7 +339,7 @@ namespace
static unsigned round = 1; static unsigned round = 1;
runner.round_formula(f, round); runner.round_formula(f, round);
unsigned ts = translators.size(); unsigned ts = tools.size();
spot::twa_graph_ptr best_aut = nullptr; spot::twa_graph_ptr best_aut = nullptr;
std::string best_stats; std::string best_stats;
std::string best_cmdname; std::string best_cmdname;
@ -364,7 +364,7 @@ namespace
if (relmap) if (relmap)
relabel_here(aut, relmap.get()); relabel_here(aut, relmap.get());
cmdname = translators[t].name; cmdname = tools[t].name;
aut = post.run(aut, f); aut = post.run(aut, f);
if (best_type) if (best_type)
{ {
@ -377,7 +377,7 @@ namespace
{ {
best_aut = aut; best_aut = aut;
best_stats = aut_stats; best_stats = aut_stats;
best_cmdname = translators[t].name; best_cmdname = tools[t].name;
best_timer = timer; best_timer = timer;
} }
best_stream.str(""); best_stream.str("");
@ -421,7 +421,7 @@ main(int argc, char** argv)
check_no_formula(); check_no_formula();
if (translators.empty()) if (tools.empty())
error(2, 0, "No translator to run? Run '%s --help' for usage.", error(2, 0, "No translator to run? Run '%s --help' for usage.",
program_name); program_name);