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

bin: introduce a non-binary job_type

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2022-05-17 10:49:06 +02:00
parent 3b809c0a14
commit d697f57a97
12 changed files with 54 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

4
bin/autcross.cc
View file

@ -162,7 +162,7 @@ parse_opt(int key, char* arg, struct argp_state*)
switch (key) switch (key)
{ {
case 'F': case 'F':
jobs.emplace_back(arg, true); jobs.emplace_back(arg, job_type::AUT_FILENAME);
break; break;
case 'q': case 'q':
quiet = true; quiet = true;
@ -216,7 +216,7 @@ parse_opt(int key, char* arg, struct argp_state*)
break; break;
case ARGP_KEY_ARG: case ARGP_KEY_ARG:
if (arg[0] == '-' && !arg[1]) if (arg[0] == '-' && !arg[1])
jobs.emplace_back(arg, true); jobs.emplace_back(arg, job_type::AUT_FILENAME);
else else
tools_push_autproc(arg); tools_push_autproc(arg);
break; break;

4
bin/autfilt.cc
View file

@ -761,7 +761,7 @@ parse_opt(int key, char* arg, struct argp_state*)
automaton_format = Count; automaton_format = Count;
break; break;
case 'F': case 'F':
jobs.emplace_back(arg, true); jobs.emplace_back(arg, job_type::AUT_FILENAME);
break; break;
case 'n': case 'n':
opt_max_count = to_pos_int(arg, "-n/--max-count"); 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; opt_art_sccs_set = true;
break; break;
case ARGP_KEY_ARG: case ARGP_KEY_ARG:
jobs.emplace_back(arg, true); jobs.emplace_back(arg, job_type::AUT_FILENAME);
break; break;
default: default:

24
bin/common_finput.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012-2017, 2019, 2021 Laboratoire de Recherche et // Copyright (C) 2012-2017, 2019, 2021, 2022 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.
// //
@ -68,10 +68,10 @@ parse_opt_finput(int key, char* arg, struct argp_state*)
switch (key) switch (key)
{ {
case 'f': case 'f':
jobs.emplace_back(arg, false); jobs.emplace_back(arg, job_type::LTL_STRING);
break; break;
case 'F': case 'F':
jobs.emplace_back(arg, true); jobs.emplace_back(arg, job_type::LTL_FILENAME);
break; break;
case OPT_LBT: case OPT_LBT:
lbt_input = true; lbt_input = true;
@ -358,10 +358,18 @@ job_processor::run()
int error = 0; int error = 0;
for (auto& j: jobs) for (auto& j: jobs)
{ {
if (!j.file_p) switch (j.type)
{
case job_type::LTL_STRING:
error |= process_string(j.str); error |= process_string(j.str);
else break;
case job_type::LTL_FILENAME:
case job_type::AUT_FILENAME:
error |= process_file(j.str); error |= process_file(j.str);
break;
default:
throw std::runtime_error("unexpected job type");
}
if (abort_run) if (abort_run)
break; break;
} }
@ -376,7 +384,7 @@ void check_no_formula()
error(2, 0, "No formula to translate? Run '%s --help' for help.\n" error(2, 0, "No formula to translate? Run '%s --help' for help.\n"
"Use '%s -' to force reading formulas from the standard " "Use '%s -' to force reading formulas from the standard "
"input.", program_name, program_name); "input.", program_name, program_name);
jobs.emplace_back("-", true); jobs.emplace_back("-", job_type::LTL_FILENAME);
} }
void check_no_automaton() 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" error(2, 0, "No automaton to process? Run '%s --help' for help.\n"
"Use '%s -' to force reading automata from the standard " "Use '%s -' to force reading automata from the standard "
"input.", program_name, program_name); "input.", program_name, program_name);
jobs.emplace_back("-", true); jobs.emplace_back("-", job_type::AUT_FILENAME);
} }

14
bin/common_finput.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement // Copyright (C) 2012-2017, 2022 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.
// //
@ -25,13 +25,17 @@
#include <vector> #include <vector>
#include <spot/tl/parse.hh> #include <spot/tl/parse.hh>
enum class job_type : char { LTL_STRING,
LTL_FILENAME,
AUT_FILENAME };
struct job struct job
{ {
const char* str; 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 job(const char* str, job_type type) noexcept
: str(str), file_p(file_p) : str(str), type(type)
{ {
} }
}; };

6
bin/dstar2tgba.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // 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) switch (key)
{ {
case 'F': case 'F':
jobs.emplace_back(arg, true); jobs.emplace_back(arg, job_type::AUT_FILENAME);
break; break;
case 'x': case 'x':
{ {
@ -99,7 +99,7 @@ parse_opt(int key, char* arg, struct argp_state*)
} }
break; break;
case ARGP_KEY_ARG: case ARGP_KEY_ARG:
jobs.emplace_back(arg, true); jobs.emplace_back(arg, job_type::AUT_FILENAME);
break; break;
default: default:
return ARGP_ERR_UNKNOWN; return ARGP_ERR_UNKNOWN;

11
bin/ltl2tgba.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement // Copyright (C) 2012-2019, 2022 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.
// //
@ -105,10 +105,9 @@ parse_opt(int key, char* arg, struct argp_state*)
break; break;
case ARGP_KEY_ARG: case ARGP_KEY_ARG:
// FIXME: use stat() to distinguish filename from string? // FIXME: use stat() to distinguish filename from string?
if (*arg == '-' && !arg[1]) jobs.emplace_back(arg, ((*arg == '-' && !arg[1])
jobs.emplace_back(arg, true); ? job_type::LTL_FILENAME
else : job_type::LTL_STRING));
jobs.emplace_back(arg, false);
break; break;
default: default:

11
bin/ltl2tgta.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement // Copyright (C) 2012-2020, 2022 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.
// //
@ -148,10 +148,9 @@ parse_opt(int key, char* arg, struct argp_state*)
break; break;
case ARGP_KEY_ARG: case ARGP_KEY_ARG:
// FIXME: use stat() to distinguish filename from string? // FIXME: use stat() to distinguish filename from string?
if (*arg == '-' && !arg[1]) jobs.emplace_back(arg, ((*arg == '-' && !arg[1])
jobs.emplace_back(arg, true); ? job_type::LTL_FILENAME
else : job_type::LTL_STRING));
jobs.emplace_back(arg, false);
break; break;
default: default:

4
bin/ltlcross.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -484,7 +484,7 @@ parse_opt(int key, char* arg, struct argp_state*)
break; break;
case ARGP_KEY_ARG: case ARGP_KEY_ARG:
if (arg[0] == '-' && !arg[1]) if (arg[0] == '-' && !arg[1])
jobs.emplace_back(arg, true); jobs.emplace_back(arg, job_type::LTL_FILENAME);
else else
tools_push_trans(arg); tools_push_trans(arg);
break; break;

4
bin/ltldo.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -193,7 +193,7 @@ parse_opt(int key, char* arg, struct argp_state*)
break; break;
case ARGP_KEY_ARG: case ARGP_KEY_ARG:
if (arg[0] == '-' && !arg[1]) if (arg[0] == '-' && !arg[1])
jobs.emplace_back(arg, true); jobs.emplace_back(arg, job_type::LTL_FILENAME);
else else
tools_push_trans(arg); tools_push_trans(arg);
break; break;

6
bin/ltlfilt.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -387,7 +387,7 @@ parse_opt(int key, char* arg, struct argp_state*)
break; break;
case ARGP_KEY_ARG: case ARGP_KEY_ARG:
// FIXME: use stat() to distinguish filename from string? // FIXME: use stat() to distinguish filename from string?
jobs.emplace_back(arg, true); jobs.emplace_back(arg, job_type::LTL_FILENAME);
break; break;
case OPT_ACCEPT_WORD: case OPT_ACCEPT_WORD:
try try
@ -876,7 +876,7 @@ main(int argc, char** argv)
exit(err); exit(err);
if (jobs.empty()) if (jobs.empty())
jobs.emplace_back("-", 1); jobs.emplace_back("-", job_type::LTL_FILENAME);
if (boolean_to_isop && simplification_level == 0) if (boolean_to_isop && simplification_level == 0)
simplification_level = 1; simplification_level = 1;

4
bin/ltlgrind.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // 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.
@ -143,7 +143,7 @@ parse_opt(int key, char* arg, struct argp_state*)
break; break;
case ARGP_KEY_ARG: case ARGP_KEY_ARG:
// FIXME: use stat() to distinguish filename from string? // FIXME: use stat() to distinguish filename from string?
jobs.emplace_back(arg, true); jobs.emplace_back(arg, job_type::LTL_FILENAME);
break; break;
case OPT_AP2CONST: case OPT_AP2CONST:
opt_all = 0; opt_all = 0;

2
bin/ltlsynt.cc
View file

@ -776,7 +776,7 @@ main(int argc, char **argv)
static char arg4[] = "fully"; static char arg4[] = "fully";
char* command[] = { arg0, arg1, arg2, arg3, arg4, opt_tlsf, nullptr }; char* command[] = { arg0, arg1, arg2, arg3, arg4, opt_tlsf, nullptr };
opt_tlsf_string = read_stdout_of_command(command); 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()) if (!all_input_aps.has_value() && !all_output_aps.has_value())
{ {