22 #include <spot/twa/twagraph.hh> 23 #include <spot/kripke/kripkegraph.hh> 24 #include <spot/misc/location.hh> 25 #include <spot/tl/defaultenv.hh> 30 #include <spot/misc/bitvect.hh> 44 struct parse_aut_error_list {};
47 enum class parsed_aut_type { HOA, NeverClaim, LBTT, DRA, DSA, Unknown };
70 parsed_aut_type type = parsed_aut_type::Unknown;
86 bool format_errors(std::ostream& os);
89 typedef std::shared_ptr<parsed_aut> parsed_aut_ptr;
90 typedef std::shared_ptr<const parsed_aut> const_parsed_aut_ptr;
94 bool ignore_abort =
false;
96 bool trust_hoa =
true;
97 bool raise_errors =
false;
98 bool want_kripke =
false;
122 spot::location last_loc;
123 std::string filename_;
149 const std::string& filename,
169 parsed_aut_ptr parse(
const bdd_dict_ptr& dict,
190 SPOT_API parsed_aut_ptr
192 const bdd_dict_ptr& dict,
static default_environment & instance()
Get the sole instance of spot::default_environment.
std::pair< spot::location, std::string > parse_aut_error
A parse diagnostic with its location.
Definition: public.hh:39
Result of the automaton parser.
Definition: public.hh:50
An environment that describes atomic propositions.
Definition: environment.hh:32
twa_graph_ptr aut
The parsed automaton.
Definition: public.hh:58
std::list< parse_aut_error > parse_aut_error_list
A list of parser diagnostics, as filled by parse.
Definition: public.hh:41
spot::location loc
Location of the automaton in the stream.
Definition: public.hh:68
kripke_graph_ptr ks
The parsed kripke structure.
Definition: public.hh:63
const std::string filename
Name of the stream (used for displaying syntax errors)
Definition: public.hh:72
parsed_aut_ptr parse_aut(const std::string &filename, const bdd_dict_ptr &dict, environment &env=default_environment::instance(), automaton_parser_options opts={})
Read the first spot::twa_graph from a file.
parse_aut_error_list errors
Syntax errors that occurred during parsing.
Definition: public.hh:77
Parse a stream of automata.
Definition: public.hh:120