bin: factor exception-handling code
* bin/common_setup.cc, bin/common_setup.hh: Define a protected_main() function that deal with exceptions. * bin/autcross.cc, bin/autfilt.cc, 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/ltlgrind.cc, bin/ltlsynt.cc, bin/randaut.cc, bin/randltl.cc: Use it for all tools.
This commit is contained in:
parent
fc0ed01a45
commit
645bb55622
16 changed files with 328 additions and 386 deletions
146
bin/autcross.cc
146
bin/autcross.cc
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2017 Laboratoire de Recherche et Développement de
|
// Copyright (C) 2017, 2018 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.
|
||||||
|
|
@ -822,97 +822,97 @@ print_stats_csv(const char* filename)
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
setup(argv);
|
return protected_main(argv, [&]() -> unsigned {
|
||||||
|
const argp ap = { options, parse_opt, "[COMMANDFMT...]",
|
||||||
|
argp_program_doc, children, nullptr, nullptr };
|
||||||
|
|
||||||
const argp ap = { options, parse_opt, "[COMMANDFMT...]",
|
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
||||||
argp_program_doc, children, nullptr, nullptr };
|
exit(err);
|
||||||
|
|
||||||
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
check_no_automaton();
|
||||||
exit(err);
|
|
||||||
|
|
||||||
check_no_automaton();
|
auto s = tools.size();
|
||||||
|
if (s == 0)
|
||||||
|
error(2, 0, "No tool to run? Run '%s --help' for usage.",
|
||||||
|
program_name);
|
||||||
|
|
||||||
auto s = tools.size();
|
if (s == 1 && !opt_language_preserved && !no_checks)
|
||||||
if (s == 0)
|
error(2, 0, "Since --language-preserved is not used, you need "
|
||||||
error(2, 0, "No tool to run? Run '%s --help' for usage.",
|
"at least two tools to compare.");
|
||||||
program_name);
|
|
||||||
|
|
||||||
if (s == 1 && !opt_language_preserved && !no_checks)
|
|
||||||
error(2, 0, "Since --language-preserved is not used, you need "
|
|
||||||
"at least two tools to compare.");
|
|
||||||
|
|
||||||
|
|
||||||
setup_color();
|
setup_color();
|
||||||
setup_sig_handler();
|
setup_sig_handler();
|
||||||
|
|
||||||
autcross_processor p;
|
autcross_processor p;
|
||||||
if (p.run())
|
if (p.run())
|
||||||
return 2;
|
return 2;
|
||||||
|
|
||||||
if (round_num == 0)
|
if (round_num == 0)
|
||||||
{
|
|
||||||
error(2, 0, "no automaton to translate");
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
if (global_error_flag)
|
|
||||||
{
|
{
|
||||||
std::ostream& err = global_error();
|
error(2, 0, "no automaton to translate");
|
||||||
if (bogus_output)
|
|
||||||
err << ("error: some error was detected during the above runs.\n"
|
|
||||||
" Check file ")
|
|
||||||
<< bogus_output_filename
|
|
||||||
<< " for problematic automata.";
|
|
||||||
else
|
|
||||||
err << ("error: some error was detected during the above runs,\n"
|
|
||||||
" please search for 'error:' messages in the above"
|
|
||||||
" trace.");
|
|
||||||
err << std::endl;
|
|
||||||
end_error();
|
|
||||||
}
|
|
||||||
else if (timeout_count == 0 && ignored_exec_fail == 0)
|
|
||||||
{
|
|
||||||
std::cerr << "No problem detected." << std::endl;
|
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
std::cerr << "No major problem detected." << std::endl;
|
if (global_error_flag)
|
||||||
}
|
|
||||||
|
|
||||||
unsigned additional_errors = 0U;
|
|
||||||
additional_errors += timeout_count > 0;
|
|
||||||
additional_errors += ignored_exec_fail > 0;
|
|
||||||
if (additional_errors)
|
|
||||||
{
|
|
||||||
std::cerr << (global_error_flag ? "Additionally, " : "However, ");
|
|
||||||
if (timeout_count)
|
|
||||||
{
|
{
|
||||||
if (additional_errors > 1)
|
std::ostream& err = global_error();
|
||||||
std::cerr << "\n - ";
|
if (bogus_output)
|
||||||
if (timeout_count == 1)
|
err << ("error: some error was detected during the above "
|
||||||
std::cerr << "1 timeout occurred";
|
"runs.\n Check file ")
|
||||||
|
<< bogus_output_filename
|
||||||
|
<< " for problematic automata.";
|
||||||
else
|
else
|
||||||
std::cerr << timeout_count << " timeouts occurred";
|
err << ("error: some error was detected during the above "
|
||||||
|
"runs,\n please search for 'error:' messages"
|
||||||
|
" in the above trace.");
|
||||||
|
err << std::endl;
|
||||||
|
end_error();
|
||||||
|
}
|
||||||
|
else if (timeout_count == 0 && ignored_exec_fail == 0)
|
||||||
|
{
|
||||||
|
std::cerr << "No problem detected." << std::endl;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
std::cerr << "No major problem detected." << std::endl;
|
||||||
}
|
}
|
||||||
|
|
||||||
if (ignored_exec_fail)
|
unsigned additional_errors = 0U;
|
||||||
|
additional_errors += timeout_count > 0;
|
||||||
|
additional_errors += ignored_exec_fail > 0;
|
||||||
|
if (additional_errors)
|
||||||
{
|
{
|
||||||
if (additional_errors > 1)
|
std::cerr << (global_error_flag ? "Additionally, " : "However, ");
|
||||||
std::cerr << "\n - ";
|
if (timeout_count)
|
||||||
if (ignored_exec_fail == 1)
|
{
|
||||||
std::cerr << "1 non-zero exit status was ignored";
|
if (additional_errors > 1)
|
||||||
else
|
std::cerr << "\n - ";
|
||||||
std::cerr << ignored_exec_fail
|
if (timeout_count == 1)
|
||||||
<< " non-zero exit statuses were ignored";
|
std::cerr << "1 timeout occurred";
|
||||||
|
else
|
||||||
|
std::cerr << timeout_count << " timeouts occurred";
|
||||||
|
}
|
||||||
|
|
||||||
|
if (ignored_exec_fail)
|
||||||
|
{
|
||||||
|
if (additional_errors > 1)
|
||||||
|
std::cerr << "\n - ";
|
||||||
|
if (ignored_exec_fail == 1)
|
||||||
|
std::cerr << "1 non-zero exit status was ignored";
|
||||||
|
else
|
||||||
|
std::cerr << ignored_exec_fail
|
||||||
|
<< " non-zero exit statuses were ignored";
|
||||||
|
}
|
||||||
|
if (additional_errors == 1)
|
||||||
|
std::cerr << '.';
|
||||||
|
std::cerr << std::endl;
|
||||||
}
|
}
|
||||||
if (additional_errors == 1)
|
|
||||||
std::cerr << '.';
|
|
||||||
std::cerr << std::endl;
|
|
||||||
}
|
}
|
||||||
}
|
|
||||||
|
|
||||||
if (csv_output)
|
if (csv_output)
|
||||||
print_stats_csv(csv_output);
|
print_stats_csv(csv_output);
|
||||||
|
|
||||||
return global_error_flag;
|
return global_error_flag;
|
||||||
|
});
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1496,13 +1496,10 @@ namespace
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
setup(argv);
|
return protected_main(argv, [&] {
|
||||||
|
const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
|
||||||
|
argp_program_doc, children, nullptr, nullptr };
|
||||||
|
|
||||||
const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
|
|
||||||
argp_program_doc, children, nullptr, nullptr };
|
|
||||||
|
|
||||||
try
|
|
||||||
{
|
|
||||||
// This will ensure that all objects stored in this struct are
|
// This will ensure that all objects stored in this struct are
|
||||||
// destroyed before global variables.
|
// destroyed before global variables.
|
||||||
opt_t o;
|
opt_t o;
|
||||||
|
|
@ -1544,19 +1541,11 @@ main(int argc, char** argv)
|
||||||
|
|
||||||
// Diagnose unused -x options
|
// Diagnose unused -x options
|
||||||
extra_options.report_unused_options();
|
extra_options.report_unused_options();
|
||||||
}
|
|
||||||
catch (const std::runtime_error& e)
|
|
||||||
{
|
|
||||||
error(2, 0, "%s", e.what());
|
|
||||||
}
|
|
||||||
catch (const std::invalid_argument& e)
|
|
||||||
{
|
|
||||||
error(2, 0, "%s", e.what());
|
|
||||||
}
|
|
||||||
|
|
||||||
if (automaton_format == Count)
|
if (automaton_format == Count)
|
||||||
std::cout << match_count << std::endl;
|
std::cout << match_count << std::endl;
|
||||||
|
|
||||||
check_cout();
|
check_cout();
|
||||||
return !match_count;
|
return match_count ? 0 : 1;
|
||||||
|
});
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -169,3 +169,23 @@ const struct argp misc_argp = { options, parse_opt_misc,
|
||||||
const struct argp misc_argp_hidden = { options_hidden, parse_opt_misc,
|
const struct argp misc_argp_hidden = { options_hidden, parse_opt_misc,
|
||||||
nullptr, nullptr, nullptr,
|
nullptr, nullptr, nullptr,
|
||||||
nullptr, nullptr };
|
nullptr, nullptr };
|
||||||
|
|
||||||
|
|
||||||
|
int protected_main(char** progname, std::function<int()> mainfun)
|
||||||
|
{
|
||||||
|
try
|
||||||
|
{
|
||||||
|
setup(progname);
|
||||||
|
return mainfun();
|
||||||
|
}
|
||||||
|
catch (const std::runtime_error& e)
|
||||||
|
{
|
||||||
|
error(2, 0, "%s", e.what());
|
||||||
|
}
|
||||||
|
catch (const std::invalid_argument& e)
|
||||||
|
{
|
||||||
|
error(2, 0, "%s", e.what());
|
||||||
|
}
|
||||||
|
SPOT_UNREACHABLE();
|
||||||
|
return 2;
|
||||||
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de
|
// Copyright (C) 2012, 2013, 2018 Laboratoire de Recherche et
|
||||||
// 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.
|
||||||
//
|
//
|
||||||
|
|
@ -21,8 +21,13 @@
|
||||||
|
|
||||||
#include "common_sys.hh"
|
#include "common_sys.hh"
|
||||||
#include "progname.h"
|
#include "progname.h"
|
||||||
|
#include <functional>
|
||||||
|
|
||||||
void setup(char** progname);
|
void setup(char** progname);
|
||||||
|
|
||||||
extern const struct argp misc_argp;
|
extern const struct argp misc_argp;
|
||||||
extern const struct argp misc_argp_hidden;
|
extern const struct argp misc_argp_hidden;
|
||||||
|
|
||||||
|
|
||||||
|
// Call setup(progname) then Run mainfun() and handle exceptions.
|
||||||
|
int protected_main(char** progname, std::function<int()> mainfun);
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire de Recherche et
|
// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
|
||||||
// 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.
|
||||||
//
|
//
|
||||||
|
|
@ -136,33 +136,26 @@ namespace
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
setup(argv);
|
return protected_main(argv, [&] {
|
||||||
|
const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
|
||||||
|
argp_program_doc, children, nullptr, nullptr };
|
||||||
|
|
||||||
const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
|
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
||||||
argp_program_doc, children, nullptr, nullptr };
|
exit(err);
|
||||||
|
|
||||||
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
check_no_automaton();
|
||||||
exit(err);
|
|
||||||
|
|
||||||
check_no_automaton();
|
spot::postprocessor post(&extra_options);
|
||||||
|
post.set_pref(pref | comp | sbacc | colored);
|
||||||
|
post.set_type(type);
|
||||||
|
post.set_level(level);
|
||||||
|
|
||||||
spot::postprocessor post(&extra_options);
|
|
||||||
post.set_pref(pref | comp | sbacc | colored);
|
|
||||||
post.set_type(type);
|
|
||||||
post.set_level(level);
|
|
||||||
|
|
||||||
try
|
|
||||||
{
|
|
||||||
dstar_processor processor(post);
|
dstar_processor processor(post);
|
||||||
if (processor.run())
|
if (processor.run())
|
||||||
return 2;
|
return 2;
|
||||||
|
|
||||||
// Diagnose unused -x options
|
// Diagnose unused -x options
|
||||||
extra_options.report_unused_options();
|
extra_options.report_unused_options();
|
||||||
}
|
return 0;
|
||||||
catch (const std::runtime_error& e)
|
});
|
||||||
{
|
|
||||||
error(2, 0, "%s", e.what());
|
|
||||||
}
|
|
||||||
return 0;
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2017 Laboratoire de Recherche et Développement de
|
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
|
||||||
// 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.
|
||||||
//
|
//
|
||||||
|
|
@ -134,29 +134,22 @@ run_jobs()
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
strcpy(F_doc, "the name of the pattern");
|
return protected_main(argv, [&] {
|
||||||
strcpy(L_doc, "the argument of the pattern");
|
strcpy(F_doc, "the name of the pattern");
|
||||||
setup(argv);
|
strcpy(L_doc, "the argument of the pattern");
|
||||||
|
|
||||||
const argp ap = { options, parse_opt, nullptr, argp_program_doc,
|
const argp ap = { options, parse_opt, nullptr, argp_program_doc,
|
||||||
children, nullptr, nullptr };
|
children, nullptr, nullptr };
|
||||||
|
|
||||||
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
||||||
exit(err);
|
exit(err);
|
||||||
|
|
||||||
if (jobs.empty())
|
if (jobs.empty())
|
||||||
error(1, 0, "Nothing to do. Try '%s --help' for more information.",
|
error(1, 0, "Nothing to do. Try '%s --help' for more information.",
|
||||||
program_name);
|
program_name);
|
||||||
|
|
||||||
try
|
|
||||||
{
|
|
||||||
run_jobs();
|
run_jobs();
|
||||||
}
|
flush_cout();
|
||||||
catch (const std::runtime_error& e)
|
return 0;
|
||||||
{
|
});
|
||||||
error(2, 0, "%s", e.what());
|
|
||||||
}
|
|
||||||
|
|
||||||
flush_cout();
|
|
||||||
return 0;
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -286,27 +286,19 @@ run_jobs()
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
setup(argv);
|
return protected_main(argv, [&] {
|
||||||
|
const argp ap = { options, parse_opt, nullptr, argp_program_doc,
|
||||||
|
children, nullptr, nullptr };
|
||||||
|
|
||||||
const argp ap = { options, parse_opt, nullptr, argp_program_doc,
|
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
||||||
children, nullptr, nullptr };
|
exit(err);
|
||||||
|
|
||||||
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
if (jobs.empty())
|
||||||
exit(err);
|
error(1, 0, "Nothing to do. Try '%s --help' for more information.",
|
||||||
|
program_name);
|
||||||
|
|
||||||
if (jobs.empty())
|
|
||||||
error(1, 0, "Nothing to do. Try '%s --help' for more information.",
|
|
||||||
program_name);
|
|
||||||
|
|
||||||
try
|
|
||||||
{
|
|
||||||
run_jobs();
|
run_jobs();
|
||||||
}
|
flush_cout();
|
||||||
catch (const std::runtime_error& e)
|
return 0;
|
||||||
{
|
});
|
||||||
error(2, 0, "%s", e.what());
|
|
||||||
}
|
|
||||||
|
|
||||||
flush_cout();
|
|
||||||
return 0;
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -158,23 +158,20 @@ namespace
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
// By default we name automata using the formula.
|
return protected_main(argv, [&] {
|
||||||
opt_name = "%f";
|
// By default we name automata using the formula.
|
||||||
|
opt_name = "%f";
|
||||||
|
|
||||||
setup(argv);
|
const argp ap = { options, parse_opt, "[FORMULA...]",
|
||||||
|
argp_program_doc, children, nullptr, nullptr };
|
||||||
|
|
||||||
const argp ap = { options, parse_opt, "[FORMULA...]",
|
simplification_level = 3;
|
||||||
argp_program_doc, children, nullptr, nullptr };
|
|
||||||
|
|
||||||
simplification_level = 3;
|
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
||||||
|
exit(err);
|
||||||
|
|
||||||
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
check_no_formula();
|
||||||
exit(err);
|
|
||||||
|
|
||||||
check_no_formula();
|
|
||||||
|
|
||||||
try
|
|
||||||
{
|
|
||||||
spot::translator trans(&extra_options);
|
spot::translator trans(&extra_options);
|
||||||
trans.set_type(type);
|
trans.set_type(type);
|
||||||
trans.set_pref(pref | comp | sbacc | unambig | colored);
|
trans.set_pref(pref | comp | sbacc | unambig | colored);
|
||||||
|
|
@ -186,11 +183,6 @@ main(int argc, char** argv)
|
||||||
|
|
||||||
// Diagnose unused -x options
|
// Diagnose unused -x options
|
||||||
extra_options.report_unused_options();
|
extra_options.report_unused_options();
|
||||||
}
|
return 0;
|
||||||
catch (const std::runtime_error& e)
|
});
|
||||||
{
|
|
||||||
error(2, 0, "%s", e.what());
|
|
||||||
}
|
|
||||||
|
|
||||||
return 0;
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement
|
// Copyright (C) 2012-2018 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.
|
||||||
|
|
@ -224,20 +224,17 @@ namespace
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
setup(argv);
|
return protected_main(argv, [&] {
|
||||||
|
const argp ap = { options, parse_opt, "[FORMULA...]",
|
||||||
|
argp_program_doc, children, nullptr, nullptr };
|
||||||
|
|
||||||
const argp ap = { options, parse_opt, "[FORMULA...]",
|
simplification_level = 3;
|
||||||
argp_program_doc, children, nullptr, nullptr };
|
|
||||||
|
|
||||||
simplification_level = 3;
|
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
||||||
|
exit(err);
|
||||||
|
|
||||||
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
check_no_formula();
|
||||||
exit(err);
|
|
||||||
|
|
||||||
check_no_formula();
|
|
||||||
|
|
||||||
try
|
|
||||||
{
|
|
||||||
spot::translator trans(&extra_options);
|
spot::translator trans(&extra_options);
|
||||||
trans.set_pref(pref | comp | sbacc);
|
trans.set_pref(pref | comp | sbacc);
|
||||||
trans.set_type(type);
|
trans.set_type(type);
|
||||||
|
|
@ -248,11 +245,6 @@ main(int argc, char** argv)
|
||||||
return 2;
|
return 2;
|
||||||
// Diagnose unused -x options
|
// Diagnose unused -x options
|
||||||
extra_options.report_unused_options();
|
extra_options.report_unused_options();
|
||||||
}
|
return 0;
|
||||||
catch (const std::runtime_error& e)
|
});
|
||||||
{
|
|
||||||
error(2, 0, "%s", e.what());
|
|
||||||
}
|
|
||||||
|
|
||||||
return 0;
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
181
bin/ltlcross.cc
181
bin/ltlcross.cc
|
|
@ -1591,108 +1591,109 @@ print_stats_json(const char* filename)
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
setup(argv);
|
return protected_main(argv, [&]() -> unsigned {
|
||||||
|
const argp ap = { options, parse_opt, "[COMMANDFMT...]",
|
||||||
|
argp_program_doc, children, nullptr, nullptr };
|
||||||
|
|
||||||
const argp ap = { options, parse_opt, "[COMMANDFMT...]",
|
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
||||||
argp_program_doc, children, nullptr, nullptr };
|
exit(err);
|
||||||
|
|
||||||
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
check_no_formula();
|
||||||
exit(err);
|
|
||||||
|
|
||||||
check_no_formula();
|
if (tools.empty())
|
||||||
|
error(2, 0, "No translator to run? Run '%s --help' for usage.",
|
||||||
|
program_name);
|
||||||
|
|
||||||
if (tools.empty())
|
setup_color();
|
||||||
error(2, 0, "No translator to run? Run '%s --help' for usage.",
|
setup_sig_handler();
|
||||||
program_name);
|
|
||||||
|
|
||||||
setup_color();
|
processor p;
|
||||||
setup_sig_handler();
|
if (p.run())
|
||||||
|
return 2;
|
||||||
|
|
||||||
processor p;
|
if (formulas.empty())
|
||||||
if (p.run())
|
|
||||||
return 2;
|
|
||||||
|
|
||||||
if (formulas.empty())
|
|
||||||
{
|
|
||||||
error(2, 0, "no formula to translate");
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
if (global_error_flag)
|
|
||||||
{
|
{
|
||||||
std::ostream& err = global_error();
|
error(2, 0, "no formula to translate");
|
||||||
if (bogus_output)
|
|
||||||
err << ("error: some error was detected during the above runs.\n"
|
|
||||||
" Check file ")
|
|
||||||
<< bogus_output_filename
|
|
||||||
<< " for problematic formulas.";
|
|
||||||
else
|
|
||||||
err << ("error: some error was detected during the above runs,\n"
|
|
||||||
" please search for 'error:' messages in the above"
|
|
||||||
" trace.");
|
|
||||||
err << std::endl;
|
|
||||||
end_error();
|
|
||||||
}
|
|
||||||
else if (timeout_count == 0 && ignored_exec_fail == 0 && oom_count == 0)
|
|
||||||
{
|
|
||||||
std::cerr << "No problem detected." << std::endl;
|
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
std::cerr << "No major problem detected." << std::endl;
|
if (global_error_flag)
|
||||||
|
{
|
||||||
|
std::ostream& err = global_error();
|
||||||
|
if (bogus_output)
|
||||||
|
err << ("error: some error was detected during the above "
|
||||||
|
"runs.\n Check file ")
|
||||||
|
<< bogus_output_filename
|
||||||
|
<< " for problematic formulas.";
|
||||||
|
else
|
||||||
|
err << ("error: some error was detected during the above "
|
||||||
|
"runs,\n please search for 'error:' messages"
|
||||||
|
" in the above trace.");
|
||||||
|
err << std::endl;
|
||||||
|
end_error();
|
||||||
|
}
|
||||||
|
else if (timeout_count == 0
|
||||||
|
&& ignored_exec_fail == 0 && oom_count == 0)
|
||||||
|
{
|
||||||
|
std::cerr << "No problem detected." << std::endl;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
std::cerr << "No major problem detected." << std::endl;
|
||||||
|
}
|
||||||
|
|
||||||
|
unsigned additional_errors = 0U;
|
||||||
|
additional_errors += timeout_count > 0;
|
||||||
|
additional_errors += ignored_exec_fail > 0;
|
||||||
|
additional_errors += oom_count > 0;
|
||||||
|
if (additional_errors)
|
||||||
|
{
|
||||||
|
std::cerr << (global_error_flag ? "Additionally, " : "However, ");
|
||||||
|
if (timeout_count)
|
||||||
|
{
|
||||||
|
if (additional_errors > 1)
|
||||||
|
std::cerr << "\n - ";
|
||||||
|
if (timeout_count == 1)
|
||||||
|
std::cerr << "1 timeout occurred";
|
||||||
|
else
|
||||||
|
std::cerr << timeout_count << " timeouts occurred";
|
||||||
|
}
|
||||||
|
|
||||||
|
if (oom_count)
|
||||||
|
{
|
||||||
|
if (additional_errors > 1)
|
||||||
|
std::cerr << "\n - ";
|
||||||
|
if (oom_count == 1)
|
||||||
|
std::cerr << "1 state-space product was";
|
||||||
|
else
|
||||||
|
std::cerr << oom_count << "state-space products were";
|
||||||
|
std::cerr << " skipped by lack of memory";
|
||||||
|
}
|
||||||
|
|
||||||
|
if (ignored_exec_fail)
|
||||||
|
{
|
||||||
|
if (additional_errors > 1)
|
||||||
|
std::cerr << "\n - ";
|
||||||
|
if (ignored_exec_fail == 1)
|
||||||
|
std::cerr << "1 non-zero exit status was ignored";
|
||||||
|
else
|
||||||
|
std::cerr << ignored_exec_fail
|
||||||
|
<< " non-zero exit statuses were ignored";
|
||||||
|
}
|
||||||
|
if (additional_errors == 1)
|
||||||
|
std::cerr << '.';
|
||||||
|
std::cerr << std::endl;
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned additional_errors = 0U;
|
delete bogus_output;
|
||||||
additional_errors += timeout_count > 0;
|
delete grind_output;
|
||||||
additional_errors += ignored_exec_fail > 0;
|
|
||||||
additional_errors += oom_count > 0;
|
|
||||||
if (additional_errors)
|
|
||||||
{
|
|
||||||
std::cerr << (global_error_flag ? "Additionally, " : "However, ");
|
|
||||||
if (timeout_count)
|
|
||||||
{
|
|
||||||
if (additional_errors > 1)
|
|
||||||
std::cerr << "\n - ";
|
|
||||||
if (timeout_count == 1)
|
|
||||||
std::cerr << "1 timeout occurred";
|
|
||||||
else
|
|
||||||
std::cerr << timeout_count << " timeouts occurred";
|
|
||||||
}
|
|
||||||
|
|
||||||
if (oom_count)
|
if (json_output)
|
||||||
{
|
print_stats_json(json_output);
|
||||||
if (additional_errors > 1)
|
if (csv_output)
|
||||||
std::cerr << "\n - ";
|
print_stats_csv(csv_output);
|
||||||
if (oom_count == 1)
|
|
||||||
std::cerr << "1 state-space product was";
|
|
||||||
else
|
|
||||||
std::cerr << oom_count << "state-space products were";
|
|
||||||
std::cerr << " skipped by lack of memory";
|
|
||||||
}
|
|
||||||
|
|
||||||
if (ignored_exec_fail)
|
return global_error_flag;
|
||||||
{
|
});
|
||||||
if (additional_errors > 1)
|
|
||||||
std::cerr << "\n - ";
|
|
||||||
if (ignored_exec_fail == 1)
|
|
||||||
std::cerr << "1 non-zero exit status was ignored";
|
|
||||||
else
|
|
||||||
std::cerr << ignored_exec_fail
|
|
||||||
<< " non-zero exit statuses were ignored";
|
|
||||||
}
|
|
||||||
if (additional_errors == 1)
|
|
||||||
std::cerr << '.';
|
|
||||||
std::cerr << std::endl;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
delete bogus_output;
|
|
||||||
delete grind_output;
|
|
||||||
|
|
||||||
if (json_output)
|
|
||||||
print_stats_json(json_output);
|
|
||||||
if (csv_output)
|
|
||||||
print_stats_csv(csv_output);
|
|
||||||
|
|
||||||
return global_error_flag;
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
47
bin/ltldo.cc
47
bin/ltldo.cc
|
|
@ -445,40 +445,33 @@ namespace
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
setup(argv);
|
return protected_main(argv, [&] {
|
||||||
|
const argp ap = { options, parse_opt, "[COMMANDFMT...]",
|
||||||
|
argp_program_doc, children, nullptr, nullptr };
|
||||||
|
|
||||||
const argp ap = { options, parse_opt, "[COMMANDFMT...]",
|
// Disable post-processing as much as possible by default.
|
||||||
argp_program_doc, children, nullptr, nullptr };
|
level = spot::postprocessor::Low;
|
||||||
|
pref = spot::postprocessor::Any;
|
||||||
|
type = spot::postprocessor::Generic;
|
||||||
|
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
||||||
|
exit(err);
|
||||||
|
|
||||||
// Disable post-processing as much as possible by default.
|
check_no_formula();
|
||||||
level = spot::postprocessor::Low;
|
|
||||||
pref = spot::postprocessor::Any;
|
|
||||||
type = spot::postprocessor::Generic;
|
|
||||||
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
|
||||||
exit(err);
|
|
||||||
|
|
||||||
check_no_formula();
|
if (tools.empty())
|
||||||
|
error(2, 0, "No translator to run? Run '%s --help' for usage.",
|
||||||
|
program_name);
|
||||||
|
|
||||||
if (tools.empty())
|
setup_sig_handler();
|
||||||
error(2, 0, "No translator to run? Run '%s --help' for usage.",
|
|
||||||
program_name);
|
|
||||||
|
|
||||||
setup_sig_handler();
|
spot::postprocessor post;
|
||||||
|
post.set_pref(pref | comp | sbacc | colored);
|
||||||
|
post.set_type(type);
|
||||||
|
post.set_level(level);
|
||||||
|
|
||||||
spot::postprocessor post;
|
|
||||||
post.set_pref(pref | comp | sbacc | colored);
|
|
||||||
post.set_type(type);
|
|
||||||
post.set_level(level);
|
|
||||||
|
|
||||||
try
|
|
||||||
{
|
|
||||||
processor p(post);
|
processor p(post);
|
||||||
if (p.run())
|
if (p.run())
|
||||||
return 2;
|
return 2;
|
||||||
}
|
return 0;
|
||||||
catch (const std::runtime_error& e)
|
});
|
||||||
{
|
|
||||||
error(2, 0, "%s", e.what());
|
|
||||||
}
|
|
||||||
return 0;
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et
|
// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
|
||||||
// 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.
|
||||||
//
|
//
|
||||||
|
|
@ -795,13 +795,10 @@ namespace
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
setup(argv);
|
return protected_main(argv, [&] {
|
||||||
|
const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
|
||||||
|
argp_program_doc, children, nullptr, nullptr };
|
||||||
|
|
||||||
const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
|
|
||||||
argp_program_doc, children, nullptr, nullptr };
|
|
||||||
|
|
||||||
try
|
|
||||||
{
|
|
||||||
// This will ensure that all objects stored in this struct are
|
// This will ensure that all objects stored in this struct are
|
||||||
// destroyed before global variables.
|
// destroyed before global variables.
|
||||||
opt_t o;
|
opt_t o;
|
||||||
|
|
@ -822,19 +819,10 @@ main(int argc, char** argv)
|
||||||
ltl_processor processor(simpl);
|
ltl_processor processor(simpl);
|
||||||
if (processor.run())
|
if (processor.run())
|
||||||
return 2;
|
return 2;
|
||||||
}
|
|
||||||
catch (const std::runtime_error& e)
|
|
||||||
{
|
|
||||||
error(2, 0, "%s", e.what());
|
|
||||||
}
|
|
||||||
catch (const std::invalid_argument& e)
|
|
||||||
{
|
|
||||||
error(2, 0, "%s", e.what());
|
|
||||||
}
|
|
||||||
|
|
||||||
if (output_format == count_output)
|
if (output_format == count_output)
|
||||||
std::cout << match_count << std::endl;
|
std::cout << match_count << '\n';
|
||||||
flush_cout();
|
flush_cout();
|
||||||
|
return one_match ? 0 : 1;
|
||||||
return one_match ? 0 : 1;
|
});
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et
|
// Copyright (C) 2014, 2015, 2016, 2017, 2018 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.
|
||||||
|
|
@ -183,21 +183,21 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
int
|
int
|
||||||
main(int argc, char* argv[])
|
main(int argc, char* argv[])
|
||||||
{
|
{
|
||||||
setup(argv);
|
return protected_main(argv, [&] {
|
||||||
|
const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
|
||||||
|
argp_program_doc, children, nullptr, nullptr };
|
||||||
|
|
||||||
const argp ap = { options, parse_opt, "[FILENAME[/COL]...]", argp_program_doc,
|
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
||||||
children, nullptr, nullptr };
|
exit(err);
|
||||||
|
|
||||||
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
mut_opts |= opt_all;
|
||||||
exit(err);
|
|
||||||
|
|
||||||
mut_opts |= opt_all;
|
check_no_formula();
|
||||||
|
|
||||||
check_no_formula();
|
mutate_processor processor;
|
||||||
|
if (processor.run())
|
||||||
mutate_processor processor;
|
return 2;
|
||||||
if (processor.run())
|
flush_cout();
|
||||||
return 2;
|
return 0;
|
||||||
flush_cout();
|
});
|
||||||
return 0;
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -416,14 +416,15 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
int
|
int
|
||||||
main(int argc, char **argv)
|
main(int argc, char **argv)
|
||||||
{
|
{
|
||||||
setup(argv);
|
return protected_main(argv, [&] {
|
||||||
const argp ap = { options, parse_opt, nullptr,
|
const argp ap = { options, parse_opt, nullptr,
|
||||||
argp_program_doc, children, nullptr, nullptr };
|
argp_program_doc, children, nullptr, nullptr };
|
||||||
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
||||||
exit(err);
|
exit(err);
|
||||||
check_no_formula();
|
check_no_formula();
|
||||||
|
|
||||||
spot::translator trans;
|
spot::translator trans;
|
||||||
ltl_processor processor(trans, input_aps, output_aps);
|
ltl_processor processor(trans, input_aps, output_aps);
|
||||||
return processor.run();
|
return processor.run();
|
||||||
|
});
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
|
// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2018 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.
|
||||||
|
|
@ -276,15 +276,13 @@ parse_opt(int key, char* arg, struct argp_state* as)
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
strcpy(F_doc, "seed number");
|
return protected_main(argv, [&] {
|
||||||
strcpy(L_doc, "automaton number");
|
strcpy(F_doc, "seed number");
|
||||||
setup(argv);
|
strcpy(L_doc, "automaton number");
|
||||||
|
|
||||||
const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
|
const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
|
||||||
children, nullptr, nullptr };
|
children, nullptr, nullptr };
|
||||||
|
|
||||||
try
|
|
||||||
{
|
|
||||||
// This will ensure that all objects stored in this struct are
|
// This will ensure that all objects stored in this struct are
|
||||||
// destroyed before global variables.
|
// destroyed before global variables.
|
||||||
opt_t o;
|
opt_t o;
|
||||||
|
|
@ -404,9 +402,6 @@ main(int argc, char** argv)
|
||||||
if (opt_automata > 0 && automaton_num >= opt_automata)
|
if (opt_automata > 0 && automaton_num >= opt_automata)
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
}
|
return 0;
|
||||||
catch (const std::runtime_error& e)
|
});
|
||||||
{
|
|
||||||
error(2, 0, "%s", e.what());
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -236,13 +236,10 @@ parse_opt(int key, char* arg, struct argp_state* as)
|
||||||
int
|
int
|
||||||
main(int argc, char** argv)
|
main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
setup(argv);
|
return protected_main(argv, [&] {
|
||||||
|
const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
|
||||||
|
children, nullptr, nullptr };
|
||||||
|
|
||||||
const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
|
|
||||||
children, nullptr, nullptr };
|
|
||||||
|
|
||||||
try
|
|
||||||
{
|
|
||||||
// This will ensure that all objects stored in this struct are
|
// This will ensure that all objects stored in this struct are
|
||||||
// destroyed before global variables.
|
// destroyed before global variables.
|
||||||
opt_t o;
|
opt_t o;
|
||||||
|
|
@ -319,16 +316,7 @@ main(int argc, char** argv)
|
||||||
output_formula_checked(f, nullptr, nullptr, ++count);
|
output_formula_checked(f, nullptr, nullptr, ++count);
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
}
|
flush_cout();
|
||||||
catch (const std::runtime_error& e)
|
return 0;
|
||||||
{
|
});
|
||||||
error(2, 0, "%s", e.what());
|
|
||||||
}
|
|
||||||
catch (const std::invalid_argument& e)
|
|
||||||
{
|
|
||||||
error(2, 0, "%s", e.what());
|
|
||||||
}
|
|
||||||
|
|
||||||
flush_cout();
|
|
||||||
return 0;
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue