diff --git a/src/bin/common_finput.cc b/src/bin/common_finput.cc index bd6f92803..380b5927f 100644 --- a/src/bin/common_finput.cc +++ b/src/bin/common_finput.cc @@ -21,6 +21,9 @@ #include "common_finput.hh" #include "error.h" +#include "ltlparse/public.hh" + +#include #define OPT_LBT 1 @@ -69,3 +72,65 @@ parse_formula(const std::string& s, spot::ltl::parse_error_list& pel) else return spot::ltl::parse(s, pel); } + + +int +job_processor::process_string(const std::string& input, + const char* filename, + int linenum) +{ + spot::ltl::parse_error_list pel; + const spot::ltl::formula* f = parse_formula(input, pel); + + if (!f || pel.size() > 0) + { + if (filename) + error_at_line(0, 0, filename, linenum, "parse error:"); + spot::ltl::format_parse_errors(std::cerr, input, pel); + if (f) + f->destroy(); + return 1; + } + return process_formula(f, filename, linenum); +} + +int +job_processor::process_stream(std::istream& is, + const char* filename) +{ + int error = 0; + int linenum = 0; + std::string line; + while (std::getline(is, line)) + error |= process_string(line, filename, ++linenum); + return error; +} + +int +job_processor::process_file(const char* filename) +{ + // Special case for stdin. + if (filename[0] == '-' && filename[1] == 0) + return process_stream(std::cin, filename); + + errno = 0; + std::ifstream input(filename); + if (!input) + error(2, errno, "cannot open '%s'", filename); + return process_stream(input, filename); +} + +int +job_processor::run() +{ + int error = 0; + jobs_t::const_iterator i; + for (i = jobs.begin(); i != jobs.end(); ++i) + { + if (!i->file_p) + error |= process_string(i->str); + else + error |= process_file(i->str); + } + return error; +} diff --git a/src/bin/common_finput.hh b/src/bin/common_finput.hh index 166cf6fa7..9c01c349b 100644 --- a/src/bin/common_finput.hh +++ b/src/bin/common_finput.hh @@ -51,4 +51,30 @@ const spot::ltl::formula* parse_formula(const std::string& s, spot::ltl::parse_error_list& error_list); +class job_processor +{ +public: + virtual ~job_processor() + { + } + + virtual int + process_formula(const spot::ltl::formula* f, + const char* filename = 0, int linenum = 0) = 0; + + virtual int + process_string(const std::string& str, + const char* filename = 0, int linenum = 0); + virtual int + process_stream(std::istream& is, const char* filename); + + virtual int + process_file(const char* filename); + + virtual int + run(); +}; + + + #endif // SPOT_BIN_COMMON_FINPUT_HH diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 5e61d3847..2441a17f8 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -21,10 +21,8 @@ #include "common_sys.hh" -#include #include #include -#include #include #include "progname.h" @@ -36,7 +34,6 @@ #include "common_post.hh" #include "misc/_config.h" -#include "ltlparse/public.hh" #include "ltlvisit/simplify.hh" #include "tgbaalgos/dotty.hh" #include "tgbaalgos/lbtt.hh" @@ -131,12 +128,6 @@ parse_opt(int key, char* arg, struct argp_state*) case 'B': type = spot::postprocessor::BA; break; - case 'f': - jobs.push_back(job(arg, false)); - break; - case 'F': - jobs.push_back(job(arg, true)); - break; case 's': format = Spin; type = spot::postprocessor::BA; @@ -175,7 +166,7 @@ parse_opt(int key, char* arg, struct argp_state*) namespace { - class trans_processor + class trans_processor: public job_processor { public: spot::ltl::ltl_simplifier& simpl; @@ -189,30 +180,28 @@ namespace } int - process_formula(const std::string& input, + process_formula(const spot::ltl::formula* f, const char* filename = 0, int linenum = 0) { - spot::ltl::parse_error_list pel; - const spot::ltl::formula* f = parse_formula(input, pel); - - if (!f || pel.size() > 0) - { - if (filename) - error_at_line(0, 0, filename, linenum, "parse error:"); - spot::ltl::format_parse_errors(std::cerr, input, pel); - if (f) - f->destroy(); - return 1; - } - const spot::ltl::formula* res = simpl.simplify(f); f->destroy(); f = res; - // This helps ltl_to_tgba_fm() to order BDD variables in a more // natural way (improving the degeneralization). simpl.clear_as_bdd_cache(); + // This should not happen, because the parser we use can only + // read PSL/LTL formula, but since our ltl::formula* type can + // represent more than PSL formula, let's make this + // future-proof. + if (!f->is_psl_formula()) + { + std::string s = spot::ltl::to_string(f); + error_at_line(2, 0, filename, linenum, + "formula '%s' is not an LTL or PSL formula", + s.c_str()); + } + bool exprop = level == spot::postprocessor::High; const spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict(), exprop); aut = post.run(aut, f); @@ -251,60 +240,9 @@ namespace flush_cout(); return 0; } - - int - process_stream(std::istream& is, const char* filename) - { - int error = 0; - int linenum = 0; - std::string line; - while (std::getline(is, line)) - error |= process_formula(line, filename, ++linenum); - return error; - } - - int - process_file(const char* filename) - { - // Special case for stdin. - if (filename[0] == '-' && filename[1] == 0) - return process_stream(std::cin, filename); - - errno = 0; - std::ifstream input(filename); - if (!input) - error(2, errno, "cannot open '%s'", filename); - return process_stream(input, filename); - } }; } -static int -run_jobs() -{ - spot::ltl::ltl_simplifier simpl(simplifier_options()); - - spot::postprocessor postproc; - postproc.set_pref(pref); - postproc.set_type(type); - postproc.set_level(level); - - trans_processor processor(simpl, postproc); - - int error = 0; - jobs_t::const_iterator i; - for (i = jobs.begin(); i != jobs.end(); ++i) - { - if (!i->file_p) - error |= processor.process_formula(i->str); - else - error |= processor.process_file(i->str); - } - if (error) - return 2; - return 0; -} - int main(int argc, char** argv) { @@ -323,5 +261,15 @@ main(int argc, char** argv) error(2, 0, "No formula to translate? Run '%s --help' for usage.", program_name); - return run_jobs(); + spot::ltl::ltl_simplifier simpl(simplifier_options()); + + spot::postprocessor postproc; + postproc.set_pref(pref); + postproc.set_type(type); + postproc.set_level(level); + + trans_processor processor(simpl, postproc); + if (processor.run()) + return 2; + return 0; } diff --git a/src/bin/ltl2tgta.cc b/src/bin/ltl2tgta.cc index 359799931..f27dae450 100644 --- a/src/bin/ltl2tgta.cc +++ b/src/bin/ltl2tgta.cc @@ -21,7 +21,6 @@ #include "common_sys.hh" -#include #include #include #include @@ -123,12 +122,6 @@ parse_opt(int key, char* arg, struct argp_state*) case 'B': type = spot::postprocessor::BA; break; - case 'f': - jobs.push_back(job(arg, false)); - break; - case 'F': - jobs.push_back(job(arg, true)); - break; case OPT_TGTA: ta_type = TGTA; type = spot::postprocessor::TGBA; @@ -164,7 +157,7 @@ parse_opt(int key, char* arg, struct argp_state*) namespace { - class trans_processor + class trans_processor: public job_processor { public: spot::ltl::ltl_simplifier& simpl; @@ -177,30 +170,28 @@ namespace } int - process_formula(const std::string& input, + process_formula(const spot::ltl::formula* f, const char* filename = 0, int linenum = 0) { - spot::ltl::parse_error_list pel; - const spot::ltl::formula* f = parse_formula(input, pel); - - if (!f || pel.size() > 0) - { - if (filename) - error_at_line(0, 0, filename, linenum, "parse error:"); - spot::ltl::format_parse_errors(std::cerr, input, pel); - if (f) - f->destroy(); - return 1; - } - const spot::ltl::formula* res = simpl.simplify(f); f->destroy(); f = res; - // This helps ltl_to_tgba_fm() to order BDD variables in a more // natural way (improving the degeneralization). simpl.clear_as_bdd_cache(); + // This should not happen, because the parser we use can only + // read PSL/LTL formula, but since our ltl::formula* type can + // represent more than PSL formula, let's make this + // future-proof. + if (!f->is_psl_formula()) + { + std::string s = spot::ltl::to_string(f); + error_at_line(2, 0, filename, linenum, + "formula '%s' is not an LTL or PSL formula", + s.c_str()); + } + bool exprop = level == spot::postprocessor::High; const spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict(), exprop); aut = post.run(aut, f); @@ -254,60 +245,9 @@ namespace flush_cout(); return 0; } - - int - process_stream(std::istream& is, const char* filename) - { - int error = 0; - int linenum = 0; - std::string line; - while (std::getline(is, line)) - error |= process_formula(line, filename, ++linenum); - return error; - } - - int - process_file(const char* filename) - { - // Special case for stdin. - if (filename[0] == '-' && filename[1] == 0) - return process_stream(std::cin, filename); - - errno = 0; - std::ifstream input(filename); - if (!input) - error(2, errno, "cannot open '%s'", filename); - return process_stream(input, filename); - } }; } -static int -run_jobs() -{ - spot::ltl::ltl_simplifier simpl(simplifier_options()); - - spot::postprocessor postproc; - postproc.set_pref(pref); - postproc.set_type(type); - postproc.set_level(level); - - trans_processor processor(simpl, postproc); - - int error = 0; - jobs_t::const_iterator i; - for (i = jobs.begin(); i != jobs.end(); ++i) - { - if (!i->file_p) - error |= processor.process_formula(i->str); - else - error |= processor.process_file(i->str); - } - if (error) - return 2; - return 0; -} - int main(int argc, char** argv) { @@ -326,5 +266,15 @@ main(int argc, char** argv) error(2, 0, "No formula to translate? Run '%s --help' for usage.", program_name); - return run_jobs(); + spot::ltl::ltl_simplifier simpl(simplifier_options()); + + spot::postprocessor postproc; + postproc.set_pref(pref); + postproc.set_type(type); + postproc.set_level(level); + + trans_processor processor(simpl, postproc); + if (processor.run()) + return 2; + return 0; } diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index b747f5ea5..0f4a3edff 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -22,7 +22,6 @@ #include "common_sys.hh" #include -#include #include #include #include @@ -62,7 +61,7 @@ const char argp_program_doc[] ="\ Read a list of formulas and output them back after some optional processing.\v\ Exit status:\n\ 0 if some formulas were output (skipped syntax errors do not count)\n\ - 1 if no formula were output (no match)\n\ + 1 if no formulas were output (no match)\n\ 2 if any error has been reported"; #define OPT_SKIP_ERRORS 2 @@ -348,7 +347,7 @@ typedef Sgi::hash_setdestroy(); return 0; } - - int - process_stream(std::istream& is, const char* filename) - { - int error = 0; - int linenum = 0; - std::string line; - while (std::getline(is, line)) - error |= process_formula(line, filename, ++linenum); - return error; - } - - int - process_file(const char* filename) - { - // Special case for stdin. - if (filename[0] == '-' && filename[1] == 0) - return process_stream(std::cin, filename); - - errno = 0; - std::ifstream input(filename); - if (!input) - error(2, errno, "cannot open '%s'", filename); - return process_stream(input, filename); - } }; } -static int -run_jobs() -{ - spot::ltl::ltl_simplifier simpl(simplifier_options()); - ltl_processor processor(simpl); - - int nerror = 0; - jobs_t::const_iterator i; - for (i = jobs.begin(); i != jobs.end(); ++i) - { - if (!i->file_p) - nerror |= processor.process_formula(i->str); - else - nerror |= processor.process_file(i->str); - } - if (nerror) - return 2; - return one_match ? 0 : 1; -} - int main(int argc, char** argv) { @@ -555,5 +515,9 @@ main(int argc, char** argv) if (jobs.empty()) jobs.push_back(job("-", 1)); - return run_jobs(); + spot::ltl::ltl_simplifier simpl(simplifier_options()); + ltl_processor processor(simpl); + if (processor.run()) + return 2; + return one_match ? 0 : 1; }