Commit ecca4ba5 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

bin: factor the code to read LTL formulas from -f or -F.

* src/bin/common_finput.cc, src/bin/common_finput.hh: Define the
processor class.
* src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlfilt.cc:
Simplify accordingly.
parent 467bf378
...@@ -21,6 +21,9 @@ ...@@ -21,6 +21,9 @@
#include "common_finput.hh" #include "common_finput.hh"
#include "error.h" #include "error.h"
#include "ltlparse/public.hh"
#include <fstream>
#define OPT_LBT 1 #define OPT_LBT 1
...@@ -69,3 +72,65 @@ parse_formula(const std::string& s, spot::ltl::parse_error_list& pel) ...@@ -69,3 +72,65 @@ parse_formula(const std::string& s, spot::ltl::parse_error_list& pel)
else else
return spot::ltl::parse(s, pel); 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;
}
...@@ -51,4 +51,30 @@ const spot::ltl::formula* ...@@ -51,4 +51,30 @@ const spot::ltl::formula*
parse_formula(const std::string& s, spot::ltl::parse_error_list& error_list); 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 #endif // SPOT_BIN_COMMON_FINPUT_HH
...@@ -21,10 +21,8 @@ ...@@ -21,10 +21,8 @@
#include "common_sys.hh" #include "common_sys.hh"
#include <vector>
#include <string> #include <string>
#include <iostream> #include <iostream>
#include <fstream>
#include <argp.h> #include <argp.h>
#include "progname.h" #include "progname.h"
...@@ -36,7 +34,6 @@ ...@@ -36,7 +34,6 @@
#include "common_post.hh" #include "common_post.hh"
#include "misc/_config.h" #include "misc/_config.h"
#include "ltlparse/public.hh"
#include "ltlvisit/simplify.hh" #include "ltlvisit/simplify.hh"
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh" #include "tgbaalgos/lbtt.hh"
...@@ -131,12 +128,6 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -131,12 +128,6 @@ parse_opt(int key, char* arg, struct argp_state*)
case 'B': case 'B':
type = spot::postprocessor::BA; type = spot::postprocessor::BA;
break; break;
case 'f':
jobs.push_back(job(arg, false));
break;
case 'F':
jobs.push_back(job(arg, true));
break;
case 's': case 's':
format = Spin; format = Spin;
type = spot::postprocessor::BA; type = spot::postprocessor::BA;
...@@ -175,7 +166,7 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -175,7 +166,7 @@ parse_opt(int key, char* arg, struct argp_state*)
namespace namespace
{ {
class trans_processor class trans_processor: public job_processor
{ {
public: public:
spot::ltl::ltl_simplifier& simpl; spot::ltl::ltl_simplifier& simpl;
...@@ -189,30 +180,28 @@ namespace ...@@ -189,30 +180,28 @@ namespace
} }
int int
process_formula(const std::string& input, process_formula(const spot::ltl::formula* f,
const char* filename = 0, int linenum = 0) 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); const spot::ltl::formula* res = simpl.simplify(f);
f->destroy(); f->destroy();
f = res; f = res;
// This helps ltl_to_tgba_fm() to order BDD variables in a more // This helps ltl_to_tgba_fm() to order BDD variables in a more
// natural way (improving the degeneralization). // natural way (improving the degeneralization).
simpl.clear_as_bdd_cache(); 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; bool exprop = level == spot::postprocessor::High;
const spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict(), exprop); const spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict(), exprop);
aut = post.run(aut, f); aut = post.run(aut, f);
...@@ -251,60 +240,9 @@ namespace ...@@ -251,60 +240,9 @@ namespace
flush_cout(); flush_cout();
return 0; 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 int
main(int argc, char** argv) main(int argc, char** argv)
{ {
...@@ -323,5 +261,15 @@ 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.", error(2, 0, "No formula to translate? Run '%s --help' for usage.",
program_name); 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;
} }
...@@ -21,7 +21,6 @@ ...@@ -21,7 +21,6 @@
#include "common_sys.hh" #include "common_sys.hh"
#include <vector>
#include <string> #include <string>
#include <iostream> #include <iostream>
#include <fstream> #include <fstream>
...@@ -123,12 +122,6 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -123,12 +122,6 @@ parse_opt(int key, char* arg, struct argp_state*)
case 'B': case 'B':
type = spot::postprocessor::BA; type = spot::postprocessor::BA;
break; break;
case 'f':
jobs.push_back(job(arg, false));
break;
case 'F':
jobs.push_back(job(arg, true));
break;
case OPT_TGTA: case OPT_TGTA:
ta_type = TGTA; ta_type = TGTA;
type = spot::postprocessor::TGBA; type = spot::postprocessor::TGBA;
...@@ -164,7 +157,7 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -164,7 +157,7 @@ parse_opt(int key, char* arg, struct argp_state*)
namespace namespace
{ {
class trans_processor class trans_processor: public job_processor
{ {
public: public:
spot::ltl::ltl_simplifier& simpl; spot::ltl::ltl_simplifier& simpl;
...@@ -177,30 +170,28 @@ namespace ...@@ -177,30 +170,28 @@ namespace
} }
int int
process_formula(const std::string& input, process_formula(const spot::ltl::formula* f,
const char* filename = 0, int linenum = 0) 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); const spot::ltl::formula* res = simpl.simplify(f);
f->destroy(); f->destroy();
f = res; f = res;
// This helps ltl_to_tgba_fm() to order BDD variables in a more // This helps ltl_to_tgba_fm() to order BDD variables in a more
// natural way (improving the degeneralization). // natural way (improving the degeneralization).
simpl.clear_as_bdd_cache(); 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; bool exprop = level == spot::postprocessor::High;
const spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict(), exprop); const spot::tgba* aut = ltl_to_tgba_fm(f, simpl.get_dict(), exprop);
aut = post.run(aut, f); aut = post.run(aut, f);
...@@ -254,60 +245,9 @@ namespace ...@@ -254,60 +245,9 @@ namespace
flush_cout(); flush_cout();
return 0; 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 int
main(int argc, char** argv) main(int argc, char** argv)
{ {
...@@ -326,5 +266,15 @@ 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.", error(2, 0, "No formula to translate? Run '%s --help' for usage.",
program_name); 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;
} }
...@@ -22,7 +22,6 @@ ...@@ -22,7 +22,6 @@
#include "common_sys.hh" #include "common_sys.hh"
#include <cstdlib> #include <cstdlib>
#include <vector>
#include <string> #include <string>
#include <iostream> #include <iostream>
#include <fstream> #include <fstream>
...@@ -62,7 +61,7 @@ const char argp_program_doc[] ="\ ...@@ -62,7 +61,7 @@ const char argp_program_doc[] ="\
Read a list of formulas and output them back after some optional processing.\v\ Read a list of formulas and output them back after some optional processing.\v\
Exit status:\n\ Exit status:\n\
0 if some formulas were output (skipped syntax errors do not count)\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"; 2 if any error has been reported";
#define OPT_SKIP_ERRORS 2 #define OPT_SKIP_ERRORS 2
...@@ -348,7 +347,7 @@ typedef Sgi::hash_set<const spot::ltl::formula*, ...@@ -348,7 +347,7 @@ typedef Sgi::hash_set<const spot::ltl::formula*,
namespace namespace
{ {
class ltl_processor class ltl_processor: public job_processor
{ {
public: public:
spot::ltl::ltl_simplifier& simpl; spot::ltl::ltl_simplifier& simpl;
...@@ -360,7 +359,7 @@ namespace ...@@ -360,7 +359,7 @@ namespace
} }
int int
process_formula(const std::string& input, process_string(const std::string& input,
const char* filename = 0, int linenum = 0) const char* filename = 0, int linenum = 0)
{ {
spot::ltl::parse_error_list pel; spot::ltl::parse_error_list pel;
...@@ -385,7 +384,13 @@ namespace ...@@ -385,7 +384,13 @@ namespace
check_cout(); check_cout();
return !quiet; return !quiet;
} }
return process_formula(f, filename, linenum);
}
int
process_formula(const spot::ltl::formula* f,
const char* filename = 0, int linenum = 0)
{
if (negate) if (negate)
f = spot::ltl::unop::instance(spot::ltl::unop::Not, f); f = spot::ltl::unop::instance(spot::ltl::unop::Not, f);
...@@ -490,54 +495,9 @@ namespace ...@@ -490,54 +495,9 @@ namespace
f->destroy(); f->destroy();
return 0; 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;
}