From d697f57a97c586afada6ff90f17bdc2cbc4cb408 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 17 May 2022 10:49:06 +0200 Subject: [PATCH] bin: introduce a non-binary job_type This will later help improve the handling of different input types of ltlsynt. * bin/common_finput.hh (job_type): New enum. (job::type): Use it. * bin/autcross.cc, bin/autfilt.cc, bin/common_finput.cc, bin/dstar2tgba.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/ltlsynt.cc: Adjust to use the job_type enum instead of a boolean. --- bin/autcross.cc | 4 ++-- bin/autfilt.cc | 4 ++-- bin/common_finput.cc | 28 ++++++++++++++++++---------- bin/common_finput.hh | 14 +++++++++----- bin/dstar2tgba.cc | 6 +++--- bin/ltl2tgba.cc | 11 +++++------ bin/ltl2tgta.cc | 11 +++++------ bin/ltlcross.cc | 4 ++-- bin/ltldo.cc | 4 ++-- bin/ltlfilt.cc | 6 +++--- bin/ltlgrind.cc | 4 ++-- bin/ltlsynt.cc | 2 +- 12 files changed, 54 insertions(+), 44 deletions(-) diff --git a/bin/autcross.cc b/bin/autcross.cc index 2aade5e49..e2224643d 100644 --- a/bin/autcross.cc +++ b/bin/autcross.cc @@ -162,7 +162,7 @@ parse_opt(int key, char* arg, struct argp_state*) switch (key) { case 'F': - jobs.emplace_back(arg, true); + jobs.emplace_back(arg, job_type::AUT_FILENAME); break; case 'q': quiet = true; @@ -216,7 +216,7 @@ parse_opt(int key, char* arg, struct argp_state*) break; case ARGP_KEY_ARG: if (arg[0] == '-' && !arg[1]) - jobs.emplace_back(arg, true); + jobs.emplace_back(arg, job_type::AUT_FILENAME); else tools_push_autproc(arg); break; diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 8fe95c396..74fe44220 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -761,7 +761,7 @@ parse_opt(int key, char* arg, struct argp_state*) automaton_format = Count; break; case 'F': - jobs.emplace_back(arg, true); + jobs.emplace_back(arg, job_type::AUT_FILENAME); break; case 'n': opt_max_count = to_pos_int(arg, "-n/--max-count"); @@ -1252,7 +1252,7 @@ parse_opt(int key, char* arg, struct argp_state*) opt_art_sccs_set = true; break; case ARGP_KEY_ARG: - jobs.emplace_back(arg, true); + jobs.emplace_back(arg, job_type::AUT_FILENAME); break; default: diff --git a/bin/common_finput.cc b/bin/common_finput.cc index 8df1fb028..559a5f312 100644 --- a/bin/common_finput.cc +++ b/bin/common_finput.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2017, 2019, 2021 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012-2017, 2019, 2021, 2022 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -68,10 +68,10 @@ parse_opt_finput(int key, char* arg, struct argp_state*) switch (key) { case 'f': - jobs.emplace_back(arg, false); + jobs.emplace_back(arg, job_type::LTL_STRING); break; case 'F': - jobs.emplace_back(arg, true); + jobs.emplace_back(arg, job_type::LTL_FILENAME); break; case OPT_LBT: lbt_input = true; @@ -358,10 +358,18 @@ job_processor::run() int error = 0; for (auto& j: jobs) { - if (!j.file_p) - error |= process_string(j.str); - else - error |= process_file(j.str); + switch (j.type) + { + case job_type::LTL_STRING: + error |= process_string(j.str); + break; + case job_type::LTL_FILENAME: + case job_type::AUT_FILENAME: + error |= process_file(j.str); + break; + default: + throw std::runtime_error("unexpected job type"); + } if (abort_run) break; } @@ -376,7 +384,7 @@ void check_no_formula() error(2, 0, "No formula to translate? Run '%s --help' for help.\n" "Use '%s -' to force reading formulas from the standard " "input.", program_name, program_name); - jobs.emplace_back("-", true); + jobs.emplace_back("-", job_type::LTL_FILENAME); } void check_no_automaton() @@ -387,5 +395,5 @@ void check_no_automaton() error(2, 0, "No automaton to process? Run '%s --help' for help.\n" "Use '%s -' to force reading automata from the standard " "input.", program_name, program_name); - jobs.emplace_back("-", true); + jobs.emplace_back("-", job_type::AUT_FILENAME); } diff --git a/bin/common_finput.hh b/bin/common_finput.hh index 5d8feb3ed..54ced7f7b 100644 --- a/bin/common_finput.hh +++ b/bin/common_finput.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012-2017, 2022 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -25,13 +25,17 @@ #include #include +enum class job_type : char { LTL_STRING, + LTL_FILENAME, + AUT_FILENAME }; + struct job { const char* str; - bool file_p; // true if str is a filename, false if it is a formula + job_type type; - job(const char* str, bool file_p) noexcept - : str(str), file_p(file_p) + job(const char* str, job_type type) noexcept + : str(str), type(type) { } }; diff --git a/bin/dstar2tgba.cc b/bin/dstar2tgba.cc index 3bf5b9393..1d5cf8762 100644 --- a/bin/dstar2tgba.cc +++ b/bin/dstar2tgba.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2019, 2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -89,7 +89,7 @@ parse_opt(int key, char* arg, struct argp_state*) switch (key) { case 'F': - jobs.emplace_back(arg, true); + jobs.emplace_back(arg, job_type::AUT_FILENAME); break; case 'x': { @@ -99,7 +99,7 @@ parse_opt(int key, char* arg, struct argp_state*) } break; case ARGP_KEY_ARG: - jobs.emplace_back(arg, true); + jobs.emplace_back(arg, job_type::AUT_FILENAME); break; default: return ARGP_ERR_UNKNOWN; diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc index f3de65a56..ee3d9f777 100644 --- a/bin/ltl2tgba.cc +++ b/bin/ltl2tgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012-2019, 2022 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -105,10 +105,9 @@ parse_opt(int key, char* arg, struct argp_state*) break; case ARGP_KEY_ARG: // FIXME: use stat() to distinguish filename from string? - if (*arg == '-' && !arg[1]) - jobs.emplace_back(arg, true); - else - jobs.emplace_back(arg, false); + jobs.emplace_back(arg, ((*arg == '-' && !arg[1]) + ? job_type::LTL_FILENAME + : job_type::LTL_STRING)); break; default: diff --git a/bin/ltl2tgta.cc b/bin/ltl2tgta.cc index ad3a64299..e3f241385 100644 --- a/bin/ltl2tgta.cc +++ b/bin/ltl2tgta.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012-2020, 2022 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -148,10 +148,9 @@ parse_opt(int key, char* arg, struct argp_state*) break; case ARGP_KEY_ARG: // FIXME: use stat() to distinguish filename from string? - if (*arg == '-' && !arg[1]) - jobs.emplace_back(arg, true); - else - jobs.emplace_back(arg, false); + jobs.emplace_back(arg, ((*arg == '-' && !arg[1]) + ? job_type::LTL_FILENAME + : job_type::LTL_STRING)); break; default: diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index d36478837..396806f96 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2020, 2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -484,7 +484,7 @@ parse_opt(int key, char* arg, struct argp_state*) break; case ARGP_KEY_ARG: if (arg[0] == '-' && !arg[1]) - jobs.emplace_back(arg, true); + jobs.emplace_back(arg, job_type::LTL_FILENAME); else tools_push_trans(arg); break; diff --git a/bin/ltldo.cc b/bin/ltldo.cc index f57a528b2..705e71105 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2020, 2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -193,7 +193,7 @@ parse_opt(int key, char* arg, struct argp_state*) break; case ARGP_KEY_ARG: if (arg[0] == '-' && !arg[1]) - jobs.emplace_back(arg, true); + jobs.emplace_back(arg, job_type::LTL_FILENAME); else tools_push_trans(arg); break; diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index af9316192..b74f7bc0c 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -387,7 +387,7 @@ parse_opt(int key, char* arg, struct argp_state*) break; case ARGP_KEY_ARG: // FIXME: use stat() to distinguish filename from string? - jobs.emplace_back(arg, true); + jobs.emplace_back(arg, job_type::LTL_FILENAME); break; case OPT_ACCEPT_WORD: try @@ -876,7 +876,7 @@ main(int argc, char** argv) exit(err); if (jobs.empty()) - jobs.emplace_back("-", 1); + jobs.emplace_back("-", job_type::LTL_FILENAME); if (boolean_to_isop && simplification_level == 0) simplification_level = 1; diff --git a/bin/ltlgrind.cc b/bin/ltlgrind.cc index 393656b00..b59569a59 100644 --- a/bin/ltlgrind.cc +++ b/bin/ltlgrind.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016, 2017, 2018, 2019 Laboratoire de Recherche et +// Copyright (C) 2014-2019, 2022 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -143,7 +143,7 @@ parse_opt(int key, char* arg, struct argp_state*) break; case ARGP_KEY_ARG: // FIXME: use stat() to distinguish filename from string? - jobs.emplace_back(arg, true); + jobs.emplace_back(arg, job_type::LTL_FILENAME); break; case OPT_AP2CONST: opt_all = 0; diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 50bae5f9e..0d89c2fc5 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -776,7 +776,7 @@ main(int argc, char **argv) static char arg4[] = "fully"; char* command[] = { arg0, arg1, arg2, arg3, arg4, opt_tlsf, nullptr }; opt_tlsf_string = read_stdout_of_command(command); - jobs.emplace_back(opt_tlsf_string.c_str(), false); + jobs.emplace_back(opt_tlsf_string.c_str(), job_type::LTL_STRING); if (!all_input_aps.has_value() && !all_output_aps.has_value()) {