f0a8d0aeb3
src/Makefile.am, src/ltlast/Makefile.am, src/ltlast/allnodes.hh, src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh, src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc, src/ltlast/constant.hh, src/ltlast/formulae.hh, src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/predecl.hh, src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlparse/Makefile.am, src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh, src/ltlparse/public.hh, src/ltlvisit/Makefile.am, src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh, src/ltlvisit/dump.cc, src/ltlvisit/dump.hh, src/ltlvisit/rewrite.cc, src/ltlvisit/rewrite.hh, src/ltltest/Makefile.am, src/ltltest/defs.in, src/ltltest/readltl.cc, src/ltltest/parse.test, src/ltltest/parseerr.test, src/misc/Makefile.am, src/misc/const_sel.hh: New files.
69 lines
1.3 KiB
C++
69 lines
1.3 KiB
C++
#include <iostream>
|
|
#include "ltlparse/public.hh"
|
|
#include "ltlvisit/dump.hh"
|
|
#include "ltlvisit/dotty.hh"
|
|
|
|
void
|
|
syntax(char *prog)
|
|
{
|
|
std::cerr << prog << " [-d] formulae" << std::endl;
|
|
exit(2);
|
|
}
|
|
|
|
int
|
|
main(int argc, char **argv)
|
|
{
|
|
int exit_code = 0;
|
|
|
|
if (argc < 2)
|
|
syntax(argv[0]);
|
|
|
|
bool debug = false;
|
|
int formulae_index = 1;
|
|
|
|
if (!strcmp(argv[1], "-d"))
|
|
{
|
|
debug = true;
|
|
if (argc < 3)
|
|
syntax(argv[0]);
|
|
formulae_index = 2;
|
|
}
|
|
|
|
spot::ltl::parse_error_list pel;
|
|
spot::ltl::formulae *f = spot::ltl::parse(argv[formulae_index],
|
|
pel, debug);
|
|
|
|
spot::ltl::parse_error_list::iterator it;
|
|
for (it = pel.begin(); it != pel.end(); ++it)
|
|
{
|
|
std::cerr << ">>> " << argv[formulae_index] << std::endl;
|
|
unsigned n = 0;
|
|
yy::Location& l = it->first;
|
|
for (; n < 4 + l.begin.column; ++n)
|
|
std::cerr << ' ';
|
|
// Write at least one '^', even if begin==end.
|
|
std::cerr << '^';
|
|
++n;
|
|
for (; n < 4 + l.end.column; ++n)
|
|
std::cerr << '^';
|
|
std::cerr << std::endl << it->second << std::endl << std::endl;
|
|
exit_code = 1;
|
|
}
|
|
|
|
if (f)
|
|
{
|
|
#ifdef DOTTY
|
|
spot::ltl::dotty(*f, std::cout);
|
|
#else
|
|
spot::ltl::dump(*f, std::cout);
|
|
std::cout << std::endl;
|
|
#endif
|
|
delete f;
|
|
}
|
|
else
|
|
{
|
|
exit_code = 1;
|
|
}
|
|
|
|
return exit_code;
|
|
}
|