parseaut: change the interface to allow new options
* src/parseaut/public.hh, src/parseaut/parseaut.yy: Make it easier to pass new options to the parser. * src/tests/ikwiad.cc, wrap/python/spot.py: Adjust.
This commit is contained in:
parent
b6c8a18dbc
commit
585e29e7d8
4 changed files with 52 additions and 31 deletions
|
|
@ -1890,8 +1890,8 @@ static void check_version(const result_& r,
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
automaton_stream_parser::automaton_stream_parser(const std::string& name,
|
automaton_stream_parser::automaton_stream_parser(const std::string& name,
|
||||||
bool ignore_abort)
|
automaton_parser_options opt)
|
||||||
: filename_(name), ignore_abort_(ignore_abort)
|
: filename_(name), opts_(opt)
|
||||||
{
|
{
|
||||||
if (hoayyopen(name))
|
if (hoayyopen(name))
|
||||||
throw std::runtime_error(std::string("Cannot open file ") + name);
|
throw std::runtime_error(std::string("Cannot open file ") + name);
|
||||||
|
|
@ -1899,8 +1899,8 @@ namespace spot
|
||||||
|
|
||||||
automaton_stream_parser::automaton_stream_parser(int fd,
|
automaton_stream_parser::automaton_stream_parser(int fd,
|
||||||
const std::string& name,
|
const std::string& name,
|
||||||
bool ignore_abort)
|
automaton_parser_options opt)
|
||||||
: filename_(name), ignore_abort_(ignore_abort)
|
: filename_(name), opts_(opt)
|
||||||
{
|
{
|
||||||
if (hoayyopen(fd))
|
if (hoayyopen(fd))
|
||||||
throw std::runtime_error(std::string("Cannot open file ") + name);
|
throw std::runtime_error(std::string("Cannot open file ") + name);
|
||||||
|
|
@ -1908,8 +1908,8 @@ namespace spot
|
||||||
|
|
||||||
automaton_stream_parser::automaton_stream_parser(const char* data,
|
automaton_stream_parser::automaton_stream_parser(const char* data,
|
||||||
const std::string& filename,
|
const std::string& filename,
|
||||||
bool ignore_abort)
|
automaton_parser_options opt)
|
||||||
: filename_(filename), ignore_abort_(ignore_abort)
|
: filename_(filename), opts_(opt)
|
||||||
{
|
{
|
||||||
hoayystring(data);
|
hoayystring(data);
|
||||||
}
|
}
|
||||||
|
|
@ -1923,8 +1923,7 @@ namespace spot
|
||||||
parsed_aut_ptr
|
parsed_aut_ptr
|
||||||
automaton_stream_parser::parse(parse_aut_error_list& error_list,
|
automaton_stream_parser::parse(parse_aut_error_list& error_list,
|
||||||
const bdd_dict_ptr& dict,
|
const bdd_dict_ptr& dict,
|
||||||
environment& env,
|
environment& env)
|
||||||
bool debug)
|
|
||||||
{
|
{
|
||||||
restart:
|
restart:
|
||||||
result_ r;
|
result_ r;
|
||||||
|
|
@ -1933,7 +1932,7 @@ namespace spot
|
||||||
r.env = &env;
|
r.env = &env;
|
||||||
hoayy::parser parser(error_list, r, last_loc);
|
hoayy::parser parser(error_list, r, last_loc);
|
||||||
static bool env_debug = !!getenv("SPOT_DEBUG_PARSER");
|
static bool env_debug = !!getenv("SPOT_DEBUG_PARSER");
|
||||||
parser.set_debug_level(debug || env_debug);
|
parser.set_debug_level(opts_.debug || env_debug);
|
||||||
hoayyreset();
|
hoayyreset();
|
||||||
try
|
try
|
||||||
{
|
{
|
||||||
|
|
@ -1951,7 +1950,7 @@ namespace spot
|
||||||
last_loc.step();
|
last_loc.step();
|
||||||
if (r.h->aborted)
|
if (r.h->aborted)
|
||||||
{
|
{
|
||||||
if (ignore_abort_)
|
if (opts_.ignore_abort)
|
||||||
goto restart;
|
goto restart;
|
||||||
return r.h;
|
return r.h;
|
||||||
}
|
}
|
||||||
|
|
@ -1967,11 +1966,10 @@ namespace spot
|
||||||
|
|
||||||
twa_graph_ptr
|
twa_graph_ptr
|
||||||
automaton_stream_parser::parse_strict(const bdd_dict_ptr& dict,
|
automaton_stream_parser::parse_strict(const bdd_dict_ptr& dict,
|
||||||
environment& env,
|
environment& env)
|
||||||
bool debug)
|
|
||||||
{
|
{
|
||||||
parse_aut_error_list pel;
|
parse_aut_error_list pel;
|
||||||
auto a = parse(pel, dict, env, debug);
|
auto a = parse(pel, dict, env);
|
||||||
|
|
||||||
if (!pel.empty())
|
if (!pel.empty())
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -60,33 +60,37 @@ namespace spot
|
||||||
typedef std::shared_ptr<parsed_aut> parsed_aut_ptr;
|
typedef std::shared_ptr<parsed_aut> parsed_aut_ptr;
|
||||||
typedef std::shared_ptr<const parsed_aut> const_parsed_aut_ptr;
|
typedef std::shared_ptr<const parsed_aut> const_parsed_aut_ptr;
|
||||||
|
|
||||||
|
struct automaton_parser_options
|
||||||
|
{
|
||||||
|
bool ignore_abort = false; ///< Skip aborted automata
|
||||||
|
bool debug = false; ///< Run the parser in debug mode?
|
||||||
|
};
|
||||||
|
|
||||||
class SPOT_API automaton_stream_parser
|
class SPOT_API automaton_stream_parser
|
||||||
{
|
{
|
||||||
spot::location last_loc;
|
spot::location last_loc;
|
||||||
std::string filename_;
|
std::string filename_;
|
||||||
bool ignore_abort_;
|
automaton_parser_options opts_;
|
||||||
public:
|
public:
|
||||||
automaton_stream_parser(const std::string& filename,
|
automaton_stream_parser(const std::string& filename,
|
||||||
bool ignore_abort = false);
|
automaton_parser_options opts = {});
|
||||||
// Read from an already open file descriptor.
|
// Read from an already open file descriptor.
|
||||||
// Use filename in error messages.
|
// Use filename in error messages.
|
||||||
automaton_stream_parser(int fd, const std::string& filename,
|
automaton_stream_parser(int fd, const std::string& filename,
|
||||||
bool ignore_abort = false);
|
automaton_parser_options opts = {});
|
||||||
// Read from a buffer
|
// Read from a buffer
|
||||||
automaton_stream_parser(const char* data,
|
automaton_stream_parser(const char* data,
|
||||||
const std::string& filename,
|
const std::string& filename,
|
||||||
bool ignore_abort = false);
|
automaton_parser_options opts = {});
|
||||||
~automaton_stream_parser();
|
~automaton_stream_parser();
|
||||||
parsed_aut_ptr parse(parse_aut_error_list& error_list,
|
parsed_aut_ptr parse(parse_aut_error_list& error_list,
|
||||||
const bdd_dict_ptr& dict,
|
const bdd_dict_ptr& dict,
|
||||||
environment& env =
|
environment& env =
|
||||||
default_environment::instance(),
|
default_environment::instance());
|
||||||
bool debug = false);
|
|
||||||
// Raises a parse_error on any syntax error
|
// Raises a parse_error on any syntax error
|
||||||
twa_graph_ptr parse_strict(const bdd_dict_ptr& dict,
|
twa_graph_ptr parse_strict(const bdd_dict_ptr& dict,
|
||||||
environment& env =
|
environment& env =
|
||||||
default_environment::instance(),
|
default_environment::instance());
|
||||||
bool debug = false);
|
|
||||||
};
|
};
|
||||||
|
|
||||||
/// \brief Build a spot::twa_graph from a HOA file or a neverclaim.
|
/// \brief Build a spot::twa_graph from a HOA file or a neverclaim.
|
||||||
|
|
@ -121,12 +125,12 @@ namespace spot
|
||||||
parse_aut_error_list& error_list,
|
parse_aut_error_list& error_list,
|
||||||
const bdd_dict_ptr& dict,
|
const bdd_dict_ptr& dict,
|
||||||
environment& env = default_environment::instance(),
|
environment& env = default_environment::instance(),
|
||||||
bool debug = false)
|
automaton_parser_options opts = {})
|
||||||
{
|
{
|
||||||
try
|
try
|
||||||
{
|
{
|
||||||
automaton_stream_parser p(filename);
|
automaton_stream_parser p(filename, opts);
|
||||||
return p.parse(error_list, dict, env, debug);
|
return p.parse(error_list, dict, env);
|
||||||
}
|
}
|
||||||
catch (std::runtime_error& e)
|
catch (std::runtime_error& e)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -580,8 +580,10 @@ checked_main(int argc, char** argv)
|
||||||
tm.start("reading -P's argument");
|
tm.start("reading -P's argument");
|
||||||
|
|
||||||
spot::parse_aut_error_list pel;
|
spot::parse_aut_error_list pel;
|
||||||
|
spot::automaton_parser_options opts;
|
||||||
|
opts.debug = debug_opt;
|
||||||
auto daut = spot::parse_aut(argv[formula_index] + 2, pel,
|
auto daut = spot::parse_aut(argv[formula_index] + 2, pel,
|
||||||
dict, env, debug_opt);
|
dict, env, opts);
|
||||||
if (spot::format_parse_aut_errors(std::cerr,
|
if (spot::format_parse_aut_errors(std::cerr,
|
||||||
argv[formula_index] + 2, pel))
|
argv[formula_index] + 2, pel))
|
||||||
return 2;
|
return 2;
|
||||||
|
|
@ -931,7 +933,9 @@ checked_main(int argc, char** argv)
|
||||||
{
|
{
|
||||||
spot::parse_aut_error_list pel;
|
spot::parse_aut_error_list pel;
|
||||||
tm.start("parsing hoa");
|
tm.start("parsing hoa");
|
||||||
auto daut = spot::parse_aut(input, pel, dict, env, debug_opt);
|
spot::automaton_parser_options opts;
|
||||||
|
opts.debug = debug_opt;
|
||||||
|
auto daut = spot::parse_aut(input, pel, dict, env, opts);
|
||||||
tm.stop("parsing hoa");
|
tm.stop("parsing hoa");
|
||||||
if (spot::format_parse_aut_errors(std::cerr, input, pel))
|
if (spot::format_parse_aut_errors(std::cerr, input, pel))
|
||||||
return 2;
|
return 2;
|
||||||
|
|
|
||||||
|
|
@ -297,7 +297,7 @@ class formula:
|
||||||
raise ValueError("unknown type of formula")
|
raise ValueError("unknown type of formula")
|
||||||
|
|
||||||
|
|
||||||
def automata(*sources, timeout=None):
|
def automata(*sources, timeout=None, ignore_abort=True, debug=False):
|
||||||
"""Read automata from a list of sources.
|
"""Read automata from a list of sources.
|
||||||
|
|
||||||
Parameters
|
Parameters
|
||||||
|
|
@ -309,6 +309,12 @@ def automata(*sources, timeout=None):
|
||||||
timeout_error : int, optional
|
timeout_error : int, optional
|
||||||
Number of seconds to wait for the result of a command.
|
Number of seconds to wait for the result of a command.
|
||||||
If None (the default), not limit is used.
|
If None (the default), not limit is used.
|
||||||
|
ignore_abort : bool, optional
|
||||||
|
If True (the default), skip HOA atomata that ends with
|
||||||
|
`--ABORT--`, and return the next automaton in the stream.
|
||||||
|
If False, aborted automata are reported as syntax errors.
|
||||||
|
debug : bool, optional
|
||||||
|
Whether to run the parser in debug mode.
|
||||||
|
|
||||||
Notes
|
Notes
|
||||||
-----
|
-----
|
||||||
|
|
@ -357,6 +363,9 @@ def automata(*sources, timeout=None):
|
||||||
`subprocess.CalledProcessError` is raised.
|
`subprocess.CalledProcessError` is raised.
|
||||||
"""
|
"""
|
||||||
|
|
||||||
|
o = automaton_parser_options()
|
||||||
|
o.debug = debug
|
||||||
|
o.ignore_abort = ignore_abort
|
||||||
for filename in sources:
|
for filename in sources:
|
||||||
try:
|
try:
|
||||||
p = None
|
p = None
|
||||||
|
|
@ -371,7 +380,7 @@ def automata(*sources, timeout=None):
|
||||||
stdout=subprocess.PIPE)
|
stdout=subprocess.PIPE)
|
||||||
if timeout is None:
|
if timeout is None:
|
||||||
p = automaton_stream_parser(proc.stdout.fileno(),
|
p = automaton_stream_parser(proc.stdout.fileno(),
|
||||||
filename, True)
|
filename, o)
|
||||||
else:
|
else:
|
||||||
try:
|
try:
|
||||||
out, err = proc.communicate(timeout=timeout)
|
out, err = proc.communicate(timeout=timeout)
|
||||||
|
|
@ -387,11 +396,11 @@ def automata(*sources, timeout=None):
|
||||||
filename[:-1])
|
filename[:-1])
|
||||||
finally:
|
finally:
|
||||||
proc = None
|
proc = None
|
||||||
p = automaton_stream_parser(out, filename, True)
|
p = automaton_stream_parser(out, filename, o)
|
||||||
elif '\n' in filename:
|
elif '\n' in filename:
|
||||||
p = automaton_stream_parser(filename, "<string>", True)
|
p = automaton_stream_parser(filename, "<string>", o)
|
||||||
else:
|
else:
|
||||||
p = automaton_stream_parser(filename, True)
|
p = automaton_stream_parser(filename, o)
|
||||||
a = True
|
a = True
|
||||||
while a:
|
while a:
|
||||||
# This returns None when we reach the end of the file.
|
# This returns None when we reach the end of the file.
|
||||||
|
|
@ -416,6 +425,12 @@ def automata(*sources, timeout=None):
|
||||||
del proc
|
del proc
|
||||||
if ret:
|
if ret:
|
||||||
raise subprocess.CalledProcessError(ret, filename[:-1])
|
raise subprocess.CalledProcessError(ret, filename[:-1])
|
||||||
|
# deleting o explicitely now prevents Python 3.5 from
|
||||||
|
# reporting the following error: "<built-in function
|
||||||
|
# delete_automaton_parser_options> returned a result with
|
||||||
|
# an error set". It's not clear to me if the bug is in Python
|
||||||
|
# or Swig. At least it's related to the use of generators.
|
||||||
|
del o
|
||||||
return
|
return
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue