diff --git a/bin/autfilt.cc b/bin/autfilt.cc index f509a0fd0..853a52de0 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -956,111 +956,21 @@ static int unused_ap(const spot::const_twa_graph_ptr& aut) namespace { - class hoa_processor final: public job_processor + + struct autfilt_processor: hoa_processor { private: spot::postprocessor& post; automaton_printer printer; public: - - hoa_processor(spot::postprocessor& post) - : post(post), printer(aut_input) + autfilt_processor(spot::postprocessor& post, spot::bdd_dict_ptr dict) + : hoa_processor(dict), post(post), printer(aut_input) { } - int - process_formula(spot::formula, const char*, int) override - { - SPOT_UNREACHABLE(); - } - - int process_string(const std::string& input, const char* filename, - int linenum) override - { - std::ostringstream loc; - loc << filename << ':' << linenum; - std::string locstr = loc.str(); - return process_automaton_stream - (spot::automaton_stream_parser(input.c_str(), locstr, opt_parse), - locstr.c_str()); - } - - int - aborted(const spot::const_parsed_aut_ptr& h, const char* filename) - { - std::cerr << filename << ':' << h->loc << ": aborted input automaton\n"; - return 2; - } - - int - process_file(const char* filename) override - { - // If we have a filename like "foo/NN" such - // that: - // ① foo/NN is not a file, - // ② NN is a number, - // ③ foo is a file, - // then it means we want to open foo as - // a CSV file and process column NN. - if (const char* slash = strrchr(filename, '/')) - { - char* end; - errno = 0; - long int col = strtol(slash + 1, &end, 10); - if (errno == 0 && !*end && col != 0) - { - struct stat buf; - if (stat(filename, &buf) != 0) - { - col_to_read = col; - if (real_filename) - free(real_filename); - real_filename = strndup(filename, slash - filename); - - // Special case for stdin. - if (real_filename[0] == '-' && real_filename[1] == 0) - return process_stream(std::cin, real_filename); - - std::ifstream input(real_filename); - if (input) - return process_stream(input, real_filename); - - error(2, errno, "cannot open '%s' nor '%s'", - filename, real_filename); - } - } - } - - return process_automaton_stream(spot::automaton_stream_parser(filename, - opt_parse), - filename); - } - - int process_automaton_stream(spot::automaton_stream_parser&& hp, - const char* filename) - { - int err = 0; - while (!abort_run) - { - auto haut = hp.parse(opt->dict); - if (!haut->aut && haut->errors.empty()) - break; - if (haut->format_errors(std::cerr)) - err = 2; - if (!haut->aut) - error(2, 0, "failed to read automaton from %s", filename); - else if (haut->aborted) - err = std::max(err, aborted(haut, filename)); - else - process_automaton(haut, filename); - } - return err; - } - - int process_automaton(const spot::const_parsed_aut_ptr& haut, - const char* filename) + const char* filename) override { process_timer timer; timer.start(); @@ -1379,7 +1289,7 @@ main(int argc, char** argv) post.set_type(type); post.set_level(level); - hoa_processor processor(post); + autfilt_processor processor(post, o.dict); if (processor.run()) return 2; diff --git a/bin/common_hoaread.hh b/bin/common_hoaread.hh index 100e675e1..2a670cafb 100644 --- a/bin/common_hoaread.hh +++ b/bin/common_hoaread.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de +// Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -20,9 +20,16 @@ #pragma once #include "common_sys.hh" +#include "error.h" #include +#include +#include +#include +#include +#include +#include "common_finput.hh" #include @@ -32,3 +39,108 @@ extern spot::automaton_parser_options opt_parse; spot::twa_graph_ptr read_automaton(const char* filename, spot::bdd_dict_ptr& dict); + + +class hoa_processor: public job_processor +{ + spot::bdd_dict_ptr dict_; +public: + + hoa_processor(spot::bdd_dict_ptr dict) + : dict_(dict) + { + } + + int + process_formula(spot::formula, const char*, int) override + { + SPOT_UNREACHABLE(); + } + + virtual int + process_automaton(const spot::const_parsed_aut_ptr& haut, + const char* filename) = 0; + + int process_string(const std::string& input, const char* filename, + int linenum) override + { + std::ostringstream loc; + loc << filename << ':' << linenum; + std::string locstr = loc.str(); + return process_automaton_stream + (spot::automaton_stream_parser(input.c_str(), locstr, opt_parse), + locstr.c_str()); + } + + int + aborted(const spot::const_parsed_aut_ptr& h, const char* filename) + { + std::cerr << filename << ':' << h->loc << ": aborted input automaton\n"; + return 2; + } + + int + process_file(const char* filename) override + { + // If we have a filename like "foo/NN" such + // that: + // ① foo/NN is not a file, + // ② NN is a number, + // ③ foo is a file, + // then it means we want to open foo as + // a CSV file and process column NN. + if (const char* slash = strrchr(filename, '/')) + { + char* end; + errno = 0; + long int col = strtol(slash + 1, &end, 10); + if (errno == 0 && !*end && col != 0) + { + struct stat buf; + if (stat(filename, &buf) != 0) + { + col_to_read = col; + if (real_filename) + free(real_filename); + real_filename = strndup(filename, slash - filename); + + // Special case for stdin. + if (real_filename[0] == '-' && real_filename[1] == 0) + return process_stream(std::cin, real_filename); + + std::ifstream input(real_filename); + if (input) + return process_stream(input, real_filename); + + error(2, errno, "cannot open '%s' nor '%s'", + filename, real_filename); + } + } + } + + return process_automaton_stream(spot::automaton_stream_parser(filename, + opt_parse), + filename); + } + + int process_automaton_stream(spot::automaton_stream_parser&& hp, + const char* filename) + { + int err = 0; + while (!abort_run) + { + auto haut = hp.parse(dict_); + if (!haut->aut && haut->errors.empty()) + break; + if (haut->format_errors(std::cerr)) + err = 2; + if (!haut->aut) + error(2, 0, "failed to read automaton from %s", filename); + else if (haut->aborted) + err = std::max(err, aborted(haut, filename)); + else + process_automaton(haut, filename); + } + return err; + } +}; diff --git a/bin/dstar2tgba.cc b/bin/dstar2tgba.cc index 505e6b303..3ecc408d4 100644 --- a/bin/dstar2tgba.cc +++ b/bin/dstar2tgba.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -108,110 +108,20 @@ parse_opt(int key, char* arg, struct argp_state*) namespace { - class dstar_processor final: public job_processor + class dstar_processor final: public hoa_processor { public: spot::postprocessor& post; automaton_printer printer; dstar_processor(spot::postprocessor& post) - : post(post), printer(aut_input) + : hoa_processor(spot::make_bdd_dict()), post(post), printer(aut_input) { } - int - process_formula(spot::formula, const char*, int) override - { - SPOT_UNREACHABLE(); - } - - int process_string(const std::string& input, const char* filename, - int linenum) override - { - std::ostringstream loc; - loc << filename << ':' << linenum; - std::string locstr = loc.str(); - return process_automaton_stream - (spot::automaton_stream_parser(input.c_str(), locstr, opt_parse), - locstr.c_str()); - } - - int - aborted(const spot::const_parsed_aut_ptr& h, const char* filename) - { - std::cerr << filename << ':' << h->loc << ": aborted input automaton\n"; - return 2; - } - - int - process_file(const char* filename) override - { - // If we have a filename like "foo/NN" such - // that: - // ① foo/NN is not a file, - // ② NN is a number, - // ③ foo is a file, - // then it means we want to open foo as - // a CSV file and process column NN. - if (const char* slash = strrchr(filename, '/')) - { - char* end; - errno = 0; - long int col = strtol(slash + 1, &end, 10); - if (errno == 0 && !*end && col != 0) - { - struct stat buf; - if (stat(filename, &buf) != 0) - { - col_to_read = col; - if (real_filename) - free(real_filename); - real_filename = strndup(filename, slash - filename); - - // Special case for stdin. - if (real_filename[0] == '-' && real_filename[1] == 0) - return process_stream(std::cin, real_filename); - - std::ifstream input(real_filename); - if (input) - return process_stream(input, real_filename); - - error(2, errno, "cannot open '%s' nor '%s'", - filename, real_filename); - } - } - } - - return process_automaton_stream(spot::automaton_stream_parser(filename, - opt_parse), - filename); - } - - int process_automaton_stream(spot::automaton_stream_parser&& hp, - const char* filename) - { - int err = 0; - while (!abort_run) - { - auto haut = hp.parse(spot::make_bdd_dict()); - if (!haut->aut && haut->errors.empty()) - break; - if (haut->format_errors(std::cerr)) - err = 2; - if (!haut->aut) - error(2, 0, "failed to read automaton from %s", filename); - else if (haut->aborted) - err = std::max(err, aborted(haut, filename)); - else - process_automaton(haut, filename); - } - return err; - } - - int process_automaton(const spot::const_parsed_aut_ptr& haut, - const char* filename) + const char* filename) override { process_timer timer; timer.start();