spot::automaton_stream_parser Class Reference

Parse a stream of automata. More...

#include <spot/parseaut/public.hh>

Collaboration diagram for spot::automaton_stream_parser:

Public Member Functions
	automaton_stream_parser (const std::string &filename, automaton_parser_options opts={})
	Parse from a file. More...
	automaton_stream_parser (int fd, const std::string &filename, automaton_parser_options opts={})
	Parse from an already opened file descriptor. More...
	automaton_stream_parser (const char *data, const std::string &filename, automaton_parser_options opts={})
	Parse from a buffer. More...
parsed_aut_ptr	parse (const bdd_dict_ptr &dict, environment &env=default_environment::instance())
	Parse the next automaton in the stream. More...

Detailed Description

Parse a stream of automata.

This object should be constructed for a given stream (a file, a file descriptor, or a raw buffer), and then it parse() method may be called in a loop to parse each automaton in the stream.

Several input formats are supported, and automatically recognized: HOA, LBTT, DSTAR, or neverclaim. We recommend using the HOA format, because it is the most general.

The specification of the HOA format can be found at http://adl.github.io/hoaf/

The grammar of neverclaim will not accept every possible neverclaim output. It has been tuned to accept the output of spin -f, ltl2ba, ltl3ba, and modella. If you know of some other tool that produce Büchi automata in the form of a neverclaim, but is not understood by this parser, please report it to spot@.nosp@m.lrde.nosp@m..epit.nosp@m.a.fr.

The parser for HOA recognize a few extensions. It maps the controlled-AP: header [42] to the synthesis-output property of Spot. It also maps spot.highlight.edges:, spot.highlight.states:, and spot.state-player: to the associated automata properties.

Constructor & Destructor Documentation

automaton_stream_parser() [1/3]

spot::automaton_stream_parser::automaton_stream_parser	(	const std::string &	filename,
		automaton_parser_options	opts = {}
	)

Parse from a file.

Parameters

filename	The file to read from.
opts	Parser options.

automaton_stream_parser() [2/3]

spot::automaton_stream_parser::automaton_stream_parser	(	int	fd,
		const std::string &	filename,
		automaton_parser_options	opts = {}
	)

Parse from an already opened file descriptor.

The file descriptor will not be closed.

Parameters

fd	The file descriptor to read from.
filename	What to display in error messages.
opts	Parser options.

automaton_stream_parser() [3/3]

spot::automaton_stream_parser::automaton_stream_parser	(	const char *	data,
		const std::string &	filename,
		automaton_parser_options	opts = {}
	)

Parse from a buffer.

Parameters

data	The buffer to read from.
filename	What to display in error messages.
opts	Parser options.

Member Function Documentation

parse()

parsed_aut_ptr spot::automaton_stream_parser::parse	(	const bdd_dict_ptr &	dict,
		environment &	env = default_environment::instance()
	)

Parse the next automaton in the stream.

Note that the parser usually tries to recover from errors. It can return an automaton even if it encountered an error during parsing. If you want to make sure the input was parsed successfully, make sure errors is empty and aborted is false in the result. (Testing aborted is obviously superfluous if the parser is configured to skip aborted automata.)

The aut field of the result can be null in two conditions: some serious error occurred (in this case errors is non empty), or the end of the stream was reached.

Warning

This function is not reentrant.

---

The documentation for this class was generated from the following file:

• spot/parseaut/public.hh