Commit 131299d0 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

hoa: make it possible to read a stream of automata

* src/bin/autfilt.cc: Loop over all automata in a file.
* src/hoaparse/public.hh: Turn the parser into an object.
* src/hoaparse/hoaparse.yy: Adjust.
parent 5aff2628
......@@ -292,17 +292,10 @@ namespace
SPOT_UNREACHABLE();
}
int
process_file(const char* filename)
process_automaton(const spot::const_hoa_aut_ptr& haut,
const char* filename)
{
spot::hoa_parse_error_list pel;
auto haut = spot::hoa_parse(filename, pel, spot::make_bdd_dict());
if (spot::format_hoa_parse_errors(std::cerr, filename, pel))
return 2;
if (!haut)
error(2, 0, "failed to read automaton from %s", filename);
spot::stopwatch sw;
sw.start();
auto aut = post.run(haut->aut, nullptr);
......@@ -337,6 +330,32 @@ namespace
flush_cout();
return 0;
}
int
process_file(const char* filename)
{
spot::hoa_parse_error_list pel;
auto b = spot::make_bdd_dict();
auto hp = spot::hoa_stream_parser(filename);
int err = 0;
for (;;)
{
auto haut = hp.parse(pel, b);
if (!haut && pel.empty())
break;
if (spot::format_hoa_parse_errors(std::cerr, filename, pel))
err = 2;
if (!haut)
error(0, 0, "failed to read automaton from %s", filename);
else
process_automaton(haut, filename);
}
return err;
}
};
}
......
......@@ -95,6 +95,7 @@
%token <str> ANAME "alias name";
%token <str> STRING "string";
%token <num> INT "integer";
%token ENDOFFILE 0 "end of file"
%left '|'
%left '&'
......@@ -114,7 +115,8 @@
%printer { debug_stream() << $$; } <num>
%%
hoa: header "--BODY--" body "--END--"
hoa: header "--BODY--" body "--END--" { YYACCEPT; }
hoa: ENDOFFILE { YYABORT; }
string_opt: | STRING
BOOLEAN: 't' | 'f'
......@@ -464,19 +466,23 @@ hoayy::parser::error(const location_type& location,
namespace spot
{
hoa_aut_ptr
hoa_parse(const std::string& name,
hoa_parse_error_list& error_list,
const bdd_dict_ptr& dict,
ltl::environment& env,
bool debug)
hoa_stream_parser::hoa_stream_parser(const std::string& name)
{
if (hoayyopen(name))
{
error_list.emplace_back(spot::location(),
std::string("Cannot open file ") + name);
return 0;
}
throw std::runtime_error(std::string("Cannot open file ") + name);
}
hoa_stream_parser::~hoa_stream_parser()
{
hoayyclose();
}
hoa_aut_ptr
hoa_stream_parser::parse(hoa_parse_error_list& error_list,
const bdd_dict_ptr& dict,
ltl::environment& env,
bool debug)
{
result_ r;
r.h = std::make_shared<spot::hoa_aut>();
r.h->aut = make_tgba_digraph(dict);
......@@ -485,10 +491,8 @@ namespace spot
parser.set_debug_level(debug);
if (parser.parse())
r.h->aut = nullptr;
hoayyclose();
if (!r.h->aut)
return nullptr;
if (r.start != -1)
r.h->aut->set_init_state(r.start);
else
......@@ -498,7 +502,7 @@ namespace spot
r.h->aut->set_init_state(r.h->aut->new_state());
}
return r.h;
}
};
}
// Local Variables:
......
......@@ -51,7 +51,19 @@ namespace spot
typedef std::shared_ptr<hoa_aut> hoa_aut_ptr;
typedef std::shared_ptr<const hoa_aut> const_hoa_aut_ptr;
/// \brief Build a spot::tgba_digraph from ltl2hoa's output.
class SPOT_API hoa_stream_parser
{
public:
hoa_stream_parser(const std::string& filename);
~hoa_stream_parser();
hoa_aut_ptr parse(hoa_parse_error_list& error_list,
const bdd_dict_ptr& dict,
ltl::environment& env =
ltl::default_environment::instance(),
bool debug = false);
};
/// \brief Build a spot::tgba_digraph from a HOA file.
/// \param filename The name of the file to parse.
/// \param error_list A list that will be filled with
/// parse errors that occured during parsing.
......@@ -63,17 +75,29 @@ namespace spot
/// 0 if the file could not be opened.
///
/// Note that the parser usually tries to recover from errors. It can
/// return an non zero value even if it encountered error during the
/// return a non zero value even if it encountered error during the
/// parsing of \a filename. If you want to make sure \a filename
/// was parsed succesfully, check \a error_list for emptiness.
///
/// \warning This function is not reentrant.
SPOT_API hoa_aut_ptr
inline hoa_aut_ptr
hoa_parse(const std::string& filename,
hoa_parse_error_list& error_list,
const bdd_dict_ptr& dict,
ltl::environment& env = ltl::default_environment::instance(),
bool debug = false);
bool debug = false)
{
try
{
hoa_stream_parser p(filename);
return p.parse(error_list, dict, env, debug);
}
catch (std::runtime_error& e)
{
error_list.emplace_back(spot::location(), e.what());
return nullptr;
}
}
/// \brief Format diagnostics produced by spot::hoa_parse.
/// \param os Where diagnostics should be output.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment